arXiv subjects

Michael Mendler

Publications and source records attributed to Michael Mendler.

4 recordsLinked to original sources

arXiv2026

Determinacy with Priorities up to Clocks

In Milner's seminal book on communication and concurrency introducing CCS, a process algebra inherently non-deterministic, chapter 11 was completely devoted to introduce the notion of determinacy and confluence in order to identify a subcalculus of CCS in which all definable agents are confluent. At the same time, or shortly later, determinate semantics were given for programming languages that reconcile concurrency and determinacy, such as Esterel by Berry and Gonthier, or SL by Boussinot and de Simone. These dedicated semantics do not easily map to Milner's confluence theory for CCS, which is unable to express causality and shared memory multi-threading with reaction to absence in a compositional way. We present an extension of CCS with priority-guarded actions and clocks, and we exploit the added expressiveness to enrich Milner's original notion of confluence by the new concept of coherence which permits us to encode, in a compositional fashion, synchronous programming languages such as Esterel.

cs.PL↗

arXiv2025

PSM: Policy Synchronised Deterministic Memory

Concurrency and determinacy do not go well with each other when resources must be shared. Haskell provides parallel programming abstractions such as IVar and LVar in the Par monad and concurrent abstractions such as MVar and TVar in the in IO and STM monads, respectively. The former are determinate but have no destructive updates and the latter have destructive updates but do not guarantee determinacy. Programming patterns that are both concurrent and determinate, such as those provided by Kahn or Berry require memory abstractions at a higher level than is currently available. In this paper we describe a new type context PSM for policy synchronised memory in Haskell. Like STM and IO, the computations in PSM can access persistent state and, as a side-effect, update the memory in imperative style. Like the Par and IO monads, PSM supports concurrent threads and shared state. However, in contrast to IO, our PSM contexts are race-free since concurrent accesses are policy coordinated which guarantees determinacy.Well-typed transactions in the PSM context can accommodate abstract data structures that are imperative, concurrently shareable and still behave deterministically, by construction.

cs.PL↗

arXiv2024

Strong Priority and Determinacy in Timed CCS

Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called "constructive reduction" which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of "coherent" processes a confluence property for constructive reductions. We show that under some restrictions, called "pivotability", coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner's classical confluence theory for CCS without priorities.

cs.PL↗

arXiv2011

An Algebra of Synchronous Scheduling Interfaces

In this paper we propose an algebra of synchronous scheduling interfaces which combines the expressiveness of Boolean algebra for logical and functional behaviour with the min-max-plus arithmetic for quantifying the non-functional aspects of synchronous interfaces. The interface theory arises from a realisability interpretation of intuitionistic modal logic (also known as Curry-Howard-Isomorphism or propositions-as-types principle). The resulting algebra of interface types aims to provide a general setting for specifying type-directed and compositional analyses of worst-case scheduling bounds. It covers synchronous control flow under concurrent, multi-processing or multi-threading execution and permits precise statements about exactness and coverage of the analyses supporting a variety of abstractions. The paper illustrates the expressiveness of the algebra by way of some examples taken from network flow problems, shortest-path, task scheduling and worst-case reaction times in synchronous programming.

cs.LO↗