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. duce 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. Bas...

• Type: Journal
• Year: 2015
• Where: ACTA
• Authors: Joaquin Aguado, Michael Mendler, Reinhard von Hanxleden, Insa Fuhrmann
• Keywords: ACTA 2015