Grounding Synchronous Deterministic Concurrency in Sequential Programming

Professorship/Faculty: Foundations of Computer Science  
Author(s): Aguado, Joaquin ; Mendler, Michael ; von Hanxleden, Reinhard; Fuhrmann, Insa
Publisher Information: Bamberg : opus
Year of publication: 2014
Pages: 86 ; Illustrationen
Series ; Volume: Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik ; 94 
Language(s): English
Licence: German Act on Copyright 
URN: urn:nbn:de:bvb:473-opus4-250905
In this report, we introduce an abstract interval domain I(D; P) and associated fixed point semantics for reasoning about concurrent and sequential variable accesses within a synchronous cycle-based model of computation. The interval domain captures must (lower bound) and cannot (upper bound) information to approximate the synchronisation status of variables consisting of a value status D and an init status P. We use this domain for a new behavioural definition of Berry’s causality analysis for Esterel. This gives a compact and uniform understanding of Esterel-style constructiveness for shared-memory multi-threaded programs. Using this 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 sequentially constructive, i.e., deterministic and deadlock-free under sequentially admissible scheduling. This gives, for the first time, a natural interpretation of Berry-constructiveness for main-stream imperative programming in terms of scheduling, where previous results were cast in terms of synchronous circuits. It also opens the door to a direct mapping of Esterel’s signal mechanism into boolean variables that can be set and reset arbitrarily 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 complexity that is linear in program
SWD Keywords: Esterel |Programmiersprache| ; Berry, Gerald ; Parallelverarbeitung ; Online-Publikation
Keywords: Concurrency, determinism, constructiveness, Mealy reactive systems, synchronous programming
DDC Classification: 004 Computer science  
RVK Classification: ST 240   
Document Type: Other
Year of publication: 25. May 2016

File SizeFormat  
BBWIAI94MendlerseA2.pdf1.67 MBPDFView/Open