Denotational Fixed Point Semantics for Constructive Scheduling of Synchronous Concurrency

  • 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 notionThe 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.show moreshow less

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Institutes:Fakultät Wirtschaftsinformatik und Angewandte Informatik / Professur für Grundlagen der Informatik
Author:Joaquín Aguado, Michael Mendler, Reinhard von Hanxleden, Insa Fuhrmann
Place of publication:Bamberg
Publisher:opus
Year of publication:2016
Pages / Size:76, 7 Seiten : Illustrationen
Collections (Serial Number):Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik (96)
Year of first publication:2015
SWD-Keyword:Nebenläufigkeit ; Verteilte Programmierung ; Denotation ; Funktionale Semantik ; Determinismus
Keywords:Denotational semantics; Mealy reactive systems, synchronous programming, Esterel; concurrency; constructiveness; determinism
DDC-Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
RVK-Classification:ST 233
URN:urn:nbn:de:bvb:473-opus4-265444
ISSN:0937-3349
Document Type:Variety of texts
Language:English
Publishing Institution:Otto-Friedrich-Universität Bamberg
Release Date:2018/11/09
Licence (German):License LogoDeutsches Urheberrecht