000K utf8 1100 $c2015 1500 eng 2050 urn:nbn:de:gbv:8:1-zs-00000267-a8 3000 Aguado, Joaquin 3010 Fuhrmann, Insa 3010 Mendler, Michael 3010 von Hanxleden, Reinhard 4000 Denotational Fixed-Point Semantics for Constructive Scheduling of Synchronous Concurrency [Aguado, Joaquin] 4209 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. 4950 https://nbn-resolving.org/urn:nbn:de:gbv:8:1-zs-00000267-a8$xR$3Volltext$534 4961 https://macau.uni-kiel.de/receive/macau_mods_00002000 5051 004