Grounding Synchronous Deterministic Concurrency in Sequential Programming
Using a new domain-theoretic characterisation we show that Berry’s constructive semantics is a conservative approximation of the recently proposed sequentially constructive (SC) model of computation. We prove that every Berry-constructive program is deter
- PDF / 449,859 Bytes
- 20 Pages / 439.363 x 666.131 pts Page_size
- 99 Downloads / 208 Views
Otto-Friedrich-Universit¨ at Bamberg, Germany Christian-Albrechts-Universit¨ at zu Kiel, Germany
Abstract. Using a new domain-theoretic characterisation we show that Berry’s constructive semantics is a conservative approximation of the recently proposed sequentially constructive (SC) model of computation. We prove that every Berry-constructive program is deterministic and deadlock-free under sequentially admissible scheduling. This gives, for the first time, a natural interpretation of Berry-constructiveness for shared-memory, multi-threaded programming in terms of synchronous cycle-based scheduling, where previous results were cast in terms of synchronous circuits. This opens the door to a direct mapping of Esterel’s signal mechanism into boolean variables that can be set and reset under the programmer’s control within a tick. We illustrate the practical usefulness of this mapping by discussing how signal reincarnation is handled efficiently by this transformation, which is of linear complexity in program size, in contrast to earlier techniques that had quadratic overhead. Keywords: Concurrency, Constructiveness, Determinism, Mealy Reactive Systems, Synchronous Programming, Esterel.
1
Introduction
If traditional main-stream programming was largely single-threaded and sequential, the new multi-core processing age raises the incentives for concurrent programming. However, multi-threaded, shared memory programming is notoriously difficult because of data races (write-write, read-write conflicts) which jeopardise the functional correctness and predictability of program behaviour. The main-stream answer to avoid the non-determinism are elementary synchronisation primitives, such as monitors, semaphores and locks. Stemming from the early days of concurrent programming, these general-purpose operators are safe in the hands of an expert, at least for systems of limited complexity, but not necessarily in the hands of the novice or for complex systems [1,2]. An approach which does not rely on synchronisation through low-level primitives is the synchronous model of computation (SMoC). SMoC is a disciplined
This work is part of the PRETSY project and supported by the German Science Foundation (DFG HA 4407/6-1 and ME 1427/6-1).
Z. Shao (Ed.): ESOP 2014, LNCS 8410, pp. 229–248, 2014. c Springer-Verlag Berlin Heidelberg 2014
230
J. Aguado et al.
scheduling regime based on logical clocks and signals as the key synchronisation mechanisms. To ensure determinism and bounded response, it enforces a strict cycle-based communication pattern between concurrent threads, which abstracts the principle of deterministic input-output Mealy machines. A synchronous computation, consisting of a system and an environment, is generally described by an ordered sequence of reaction instants, each one occurring at a global clock tick acting as a synchronisation barrier. In a synchronous program, these ticks are derived from explicit clocks, as in Lustre [3] or Signal [4], or from statements such as Esterel’s [5] pause, which establish precisely
Data Loading...
