Denotational Fixed Point Semantics for Constructive Scheduling of Synchronous Concurrency

Professorship/Faculty: Foundations of Computer Science  
Author(s): Mendler, Michael ; von Hanxleden, Reinhard; Fuhrmann, Insa; Aguado, Joaquin
Publisher Information: Bamberg : opus
Year of publication: 2016
Pages: 76, 7 ; Illustrationen
Series ; Volume: Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik ; 96 
Year of first publication: 2015
Language(s): English
Licence: German Act on Copyright 
URN: urn:nbn:de:bvb:473-opus4-265444
The synchronous model of concurrent computation (SMoCC) is well established for programming languages in the domain of safety-critical reactive and embedded systems.
Translated into mainstream C/Java programming, the SMoCC corresponds to a cyclic execution model in which concurrent threads are synchronised on a logical clock that cuts system computation into a sequence of macro-steps. A causality analysis verifies the existence of a schedule on memory accesses to ensure each macro-step is deadlock-free and determinate.
We introduce an abstract semantic domain I(D,P) and an associated denotational fixed point semantics for reasoning about concurrent and sequential variable accesses within a synchronous cycle-based model of computation. We use this domain for a new and extended behavioural definition of Berry’s causality analysis in terms of approximation intervals. The domain I(D,P) extends the domain I(D) from our previous work and fixes a mistake in the treatment of initialisations.
Based on this fixed point semantics the notion of Input Berry-constructiveness (IBC) for synchronous programs is proposed. This new IBC class lies properly between strong (SBC) and normal Berry-constructiveness (BC) defined in previous work. SBC and BC are two ways to interpret the standard constructive semantics of synchronous programming, as exemplified by imperative SMoCC languages such as Esterel or Quartz.
SBC is often too restrictive as it requires all variables to be initialised by the program.
BC can be too permissive because it initialises all variables to a fixed value, by default.
Where the initialisation happens through the memory, e.g., when carrying values from one synchronous tick to the next, then IBC is more appropriate.
IBC links two levels of execution, the macro-step level and the micro-step level. We prove that the denotational fixed point analysis for IBC, and hence Berry’s causality analysis, is sound with respect to operational micro-level scheduling. The denotational model can thus be viewed as a compositional presentation of a synchronous scheduling strategy that ensures reactiveness and determinacy for imperative concurrent programming.
SWD Keywords: Nebenläufigkeit ; Verteilte Programmierung ; Denotation ; Funktionale Semantik ; Determinismus
Keywords: Denotational semantics, concurrency, determinism, constructiveness, Mealy reactive systems, synchronous programming, Esterel
DDC Classification: 004 Computer science  
RVK Classification: ST 233   
Document Type: Other
Year of publication: 9. November 2018