Deterministic Concurrency: A ClockSynchronised Shared Memory Approach
Abstract
Synchronous Programming (SP) is a universal computational principle that provides deterministic concurrency. The same input sequence with the same timing always results in the same externally observable output sequence, even if the internal behaviour generates uncertainty in the scheduling of concurrent memory accesses. Consequently, SP languages have always been strongly founded on mathematical semantics that support formal program analysis. So far, however, communication has been constrained to a set of primitive clocksynchronised shared memory (csm) data types, such as dataflow registers, streams and signals with restricted read and write accesses that limit modularity and behavioural abstractions.
This paper proposes an extension to the SP theory which retains the advantages of deterministic concurrency, but allows communication to occur at higher levels of abstraction than currently supported by SP data types. Our approach is as follows. To avoid data races, each csm type publishes a policy interface for specifying the admissibility and precedence of its access methods. Each instance of the csm type has to be policycoherent, meaning it must behave deterministically under its own policy—a natural requirement if the goal is to build deterministic systems that use these types. In a policyconstructive system, all access methods can be scheduled in a policyconformant way for all the types without deadlocking. In this paper, we show that a policyconstructive program exhibits deterministic concurrency in the sense that all policyconformant interleavings produce the same inputoutput behaviour. Policies are conservative and support the csm types existing in current SP languages. Technically, we introduce a kernel SP language that uses arbitrary policydriven csm types. A bigstep fixedpoint semantics for this language is developed for which we prove determinism and termination of constructive programs.
Keywords
Synchronous programming Data abstraction Clocksynchronised shared memory Determinacy Concurrency Constructive semantics1 Introduction
Concurrent programming is challenging. Arbitrary interleavings of concurrent threads lead to nondeterminism with data races imposing significant integrity and consistency issues [1]. Moreover, in many application domains such as safetycritical systems, determinism is indeed a matter of life and death. In a medicaldevice software, for instance, the same input sequence from the sensors (with the same timing) must always result in the same output sequence for the actuators, even if the runtime software architecture regime is unpredictable.
Synchronous programming (SP) delivers deterministic concurrency out of the box^{1} which explains its success in the design, implementation and validation of embedded, reactive and safetycritical systems for avionics, automotive, energy and nuclear industries. Right now SPgenerated code is flying on the Airbus 380 in systems like flight control, cockpit display, flight warning, and antiicing just to mention a few. The SP mathematical theory has been fundamental for implementing correctbyconstruction programderivation algorithms and establishing formal analysis, verification and testing techniques [2]. For SCADE^{2}, the SP industrial modelling language and software development toolkit, the formal SP background has been a key aspect for its certification at the highest level A of the aerospace standard DO178B/C. This SP rigour has also been important for obtaining certifications in railway and transportation (EN 50128), industry and energy (IEC 61508), automotive (TÜV and ISO 26262) as well as for ensuring full compliance with the safety standards of nuclear instrumentation and control (IEC 60880) and medical systems (IEC 62304) [3].
Synchronous Programming in a Nutshell. At the top level, we can imagine an SP system as a blackbox with inputs and outputs for interacting with its environment. There is a special input, called the clock, that determines when the communication between system and environment can occur. The clock gets an input stimulus from the environment at discrete times. At those moments we say that the clock ticks. When there is no tick, there is no possible communication, as if system and environment were disconnected. At every tick, the system reacts by reading the current inputs and executing a step function that delivers outputs and changes the internal memory. For its part, the environment must synchronise with this reaction and do not go ahead with more ticks. Thus, in SP, we assume (Synchrony Hypothesis) that the time interval of a system reaction, also called macrostep or (synchronous) instant, appears instantaneous (has zerodelay) to the environment. Since each system reaction takes exactly one clock tick, we describe the evolution of the systemenvironment interaction as a synchronous (lockstep) sequence of macrosteps. The SP theory guarantees that all externally observable interaction sequences derived from the macrostep reactions define a functional inputoutput relation.
The fact that the sequences of macrosteps take place in time and space (memory) has motivated two orthogonal developments of SP. The dataflow view regards inputoutput sequences as synchronous streams of data changing over time and studies the functional relationships between streams. Dually, the controlflow approach projects the information of the inputoutput sequences at each point in time and studies the changes of this global state as time progresses, i.e., from one tick to the next. The SP paradigm includes languages such as Esterel [4], Quartz [5] and SC [6] in the imperative controlflow style and languages like Signal [7], Lustre [8] and Lucid Synchrone [9] that support the declarative dataflow view. There are even mixed controldata flow language such as Esterel V7 [10] or SCADE [3]. Independently of the execution model, the common strength to all of these SP languages is a precise formal semantics—an indispensable feature when dealing with the complexities of concurrency.
At a more concrete level, we can visualise an SP system as a whitebox where inside we find (graphical or textual) code. In the SP domain, the program must be divided into fragments corresponding to the macrostep reactions that will be executed instantaneously at each tick. Declarative languages usually organise these macrosteps by means of (internally generated) activation clocks that prescribe the blocks (nodes) that are performed at each tick. Instead, imperative textual languages provide a \(\mathop {\mathtt {pause}}\) statement for explicitly delimiting code execution within a synchronous instant. In either case, the Synchrony Hypothesis conveniently abstracts away all the, typically concurrent, lowlevel microsteps needed to produce a system reaction. The SP theory explains how the microstep accesses to shared memory must be controlled so as to ensure that all internal (whitebox) behaviour eventually stabilises, completing a deterministic macrostep (blackbox) response. For more details on SP, the reader is referred to [2].
State of the Art. Traditional imperative SP languages provide constructs to model controldominated systems. Typically, these include a concurrent composition of threads (sequential processes) that guarantees determinism and offers signals as the main means for data communication between threads. Signals behave like shared variables for which the concurrent accesses occurring within a macrostep are scheduled according to the following principles: A pure signal has a status that can be present (1) or absent (0). At the beginning of each macrostep, pure signals have status 0 by default. In any instant, a signal \({\texttt {s}} \) can be explicitly emitted with the statement \({\texttt {s}}.\mathop {\mathtt {emit}} ()\) which atomically sets its status to 1. We can read the status of \({\texttt {s}} \) with the statement \({\texttt {s}}.\mathop {\mathtt {pres}} ()\), so the controlflow can branch depending on runtime signal statuses. Specifically, inside programs, ifthenelse constructions await for the appropriate combination of present and absent signal statuses to emit (or not) more signals. The main issue is to avoid inconsistencies due to circular causality resulting from decisions based on absent statuses. Thus, the order in which the access methods \(\mathop {\mathtt {emit}}\), \(\mathop {\mathtt {pres}}\) are scheduled matters for the final result. The usual SP rule for ensuring determinism is that the \(\mathop {\mathtt {pres}} \) test must wait until the final signal status is decided. If all signal accesses can be scheduled in this decidethenread way then the program is constructive. All schedules that keep the decidethenread order will produce the same inputoutput result. This is how SP reconciles concurrency and observable determinism and generates much of its algebraic appeal. Constructiveness of programs is what static techniques like the mustcan analysis [4, 11, 12, 13] verify although in a more abstract manner. Pure signals are a simple form of clocksynchronised shared memory (csm) data types with access methods (operations) specific to this csm type. Existing SP controlflow languages also support other restricted csm types such valued signals and arrays [10] or sequentially constructive variables [6].
Contribution. This paper proposes an extension to the SP model which retains the advantages of deterministic concurrency while widening the notion of constructiveness to cover more general csm types. This allows sharedmemory communication to occur at higher levels of abstraction than currently supported. In particular, our approach subsumes both the notions of Berryconstructiveness [4] for Esterel and sequential constructiveness for SCL [14]. This is the first time that these SP communication principles are combined sidebyside in a single language. Moreover, our theory permits other predefined communication structures to coexist safely under the same uniform framework, such as dataflow variables [8], registers [15], Kahn channels [16], priority queues, arrays as well as other csm types currently unsupported in SP.
The policy tells us whether a given method or tick is admissible, i.e., if it can be scheduled from a particular state^{3}. In addition, transitions include a blocking set of method names as part of their action labels. This set determines a precedence between methods from a given state. A label m : L specifies that all methods in L take precedence over m. An empty blocking set \(\emptyset \) indicates no precedences. To improve visualisation, we highlight precedences by dotted (red) arrows tagged \(\mathop {\mathtt {prec}}\)^{4}. The policy interface in Fig. 1 specifies the decidethenread protocol of pure signals as follows. At any instant, if the signal status is 0 then the \(\mathop {\mathtt {pres}}\) test can only be scheduled if there are no more potential \(\mathop {\mathtt {emit}}\) statements that can still update the status to 1. This explains the precedence of the \(\mathop {\mathtt {emit}}\) transition over the self loop with action label \(\mathop {\mathtt {pres}} \mathrel {:}\{\mathop {\mathtt {emit}} \}\) from state 0. Conversely, transitions \(\mathop {\mathtt {pres}}\) and \(\mathop {\mathtt {emit}}\) from state 1 have no precedences, meaning that the \(\mathop {\mathtt {pres}}\) and \(\mathop {\mathtt {emit}}\) methods are confluent so they can be freely scheduled (interleaved). The reason is that a signal status 1 is already decided and can no longer be changed by either method in the same instant. In general, any two admissible methods that do not block each other must be confluent in the sense that the same policy state is reached independently of their order of execution. Note that all the \(\sigma \) transition go to the initial state 0 since at each tick the SP system enters a new macrostep where all pure signals get initialised to the 0 status.
Section 2 describes in detail the idea of a scheduling policy on general csm types. This leads to a typelevel coherence property, which is a local form of determinism. Specifically, a csm type is policycoherent if it satisfies the (policy) specification of admissibility and precedence of its access methods. The point is that a policycoherent csm type per se behaves deterministically under its own policy—a very natural requirement if the goal is to build deterministic systems that use this type. For instance, the fact that Esterel signals are deterministic (policycoherent) in the first place permits techniques such as the mustcan analysis to get constructive information about deterministic programs. We show how policycoherence implies a global determinacy property called commutation. Now, in a policyconstructive program all access methods can be scheduled in a policyconforming way for all the csm types without deadlocking. We also show that, for policycoherent types, a policyconstructive program exhibits deterministic concurrency in the sense that all policyconforming interleavings produce the same inputoutput behaviour.
To implement a constructive scheduling mechanism parameterised in arbitrary csm type policies, we present the synchronous kernel language, called Deterministic Concurrent Language (DCoL), in Sect. 2.1. DCoL is both a minimal language to study the new mathematical concepts but can also act as an intermediate language for compiling existing SP Sect. 3 presents its policydriven operational semantics for which determinacy and termination is proven. Section 3 also explains how this model generalises existing notions of constructiveness. We discuss related work in Sect. 4 and present our conclusions in Sect. 5.
A companion of this paper is the research report (https://www.unibamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/reportWIAI102Feb2018.pdf) [17] which contains detailed proofs and additional examples of csm types.
2 Synchronous Policies
This section introduces a kernel synchronous Deterministic Concurrent Language (DCoL) for policyconformant constructive scheduling which integrates policycontrolled csm types within a simple syntax. DCoL is used to discuss the behavioural (clock) abstraction limitations of current SP. Then policies are introduced as a mechanism for specifying the scheduling discipline for csm types which, in this form, can encapsulate arbitrary ADTs.
2.1 Syntax
This syntax seems minimalistic compared to existing SP languages. For instance, it does not provide primitives for preemption, suspension or traps as in Quartz or Esterel. Recent work [18] has shown how these control primitives can be translated into the constructs of the SCL language, exploiting destructive update of sequentially constructive (SC) variables. Since SC variables are a special case of policycontrolled csm variables, DCoL is at least as expressive as SCL.
2.2 Limited Abstraction in SP
The data abstraction limitation of traditional SP is that it is not directly possible to encapsulate a composite behaviour on synchronised signals as a shared synchronised object. For this, the simple decidethenread signal protocol must be generalised, in particular, to distinguish between concurrent and sequential accesses to the shared data structure. A concurrent access \(x_1 {{\texttt {\,=\,}}} {{\texttt {nats}}}.{{\texttt {step}}} () \mathop {{\texttt {\!\!}}}\) \(x_2 {{\texttt {\,=\,}}} {{\texttt {nats}}}.{{\texttt {step}}} ()\) must give the same value for \(x_1\) and \(x_2\), while a sequential access \(x_1 {{\texttt {\,=\,}}} {{\texttt {nats}}}.{{\texttt {step}}} () \mathop {{\texttt {;}}} x_2 {{\texttt {\,=\,}}} {{\texttt {nats}}}.{{\texttt {step}}} ()\) must yield successive values of the stream. In a sequence \(x {{\texttt {\,=\,}}} {\texttt {xs}}.{{\texttt {read}}} () \mathop {{\texttt {;}}} {\texttt {xs}}.\mathop {\mathtt {emit}} (v)\) the x does not see the value v but in a parallel Open image in new window we may want the read to wait for the emission. The rest of this section covers our theory on policies in which this is possible. The modularity issue is reconsidered in Sect. 2.6.
2.3 Concurrent Access Policies
In the whitebox view of SP, an imperative program consists of a set of threads (sequential processes) and some csm variables for communication. Due to concurrency, a given thread under control (tuc) has the chance to access the shared variables only from time to time. For a given csm variable, a concurrent access policy (cap) is the locking mechanism used to control the accesses of the current tuc and its environment. The locking is to ensure that determinacy of the csm type is not broken by the concurrent accesses. A cap is like a policy which has extra transitions to model potential environment accesses outside the tuc. Concretely, a cap is given by a state machine where each transition label \(a \mathrel {:}L\) codifies an action a taking place on the shared variable with blocking set L, where L is a set of methods that take precedence over a. The action is either a method \(m \mathrel {:}L\), a silent action \(\tau \mathrel {:}L\) or a clock tick \(\sigma \mathrel {:}L\). A transition \(m \mathrel {:}L\) expresses that in the current cap control state, the method m can be called by the tuc, provided that no method in L is called concurrently. There is a Determinacy Requirement that guarantees that each method call by the tuc has a blocking set and successor state. Additionally, the execution of methods by the cap must be confluent in the sense that if two methods are admissible and do not block each other, then the cap reaches the same policy state no matter the order in which they are executed. This is to preserve determinism for concurrent variable accesses. A transition \(\tau \mathrel {:}L\) internalises method calls by the tuc ’s concurrent environment which are uncontrollable for the tuc. In the sequel, the actions in \(\textsf {M}_{\texttt {c}} \cup \{\sigma \}\) will be called observable. A transition \(\sigma \mathrel {:}L\) models a clock synchronisation step of the tuc. Like method calls, such clock ticks must be determinate as stated by the Determinacy Requirement. Additionally, the clock must always wait for any predicted concurrent \(\tau \)activity to complete. This is the Maximal Progress Requirement. Note that we do not need confluence for clock transitions since they are not concurrent.
Definition 1

Determinacy. If Open image in new window and Open image in new window then \(L_1 = L_2\) and \(\mu _1 = \mu _2\) provided a is observable, i.e., \(a \ne \tau \).

Confluence. If Open image in new window and Open image in new window do not block each other, i.e., \(m_1 \in \textsf {M}_{\texttt {c}} \setminus L_2\) and \(m_2 \in \textsf {M}_{\texttt {c}} \setminus L_1\), then for some \(\mu '\) both Open image in new window and Open image in new window .

Maximal Progress. Open image in new window and Open image in new window imply a is observable.
A policy is a cap without any (concurrent) \(\tau \) activity, i.e., every Open image in new window implies that a is observable. \(\square \)
The use of a cap as a concurrent policy arises from the notion of enabling. Informally, an observable action \(a \in \textsf {M}_{\texttt {c}} \cup \{ \sigma \}\) is enabled in a state \(\mu \) of a cap if it is admissible in \(\mu \) and in all subsequent states reachable under arbitrary silent steps. To formalise this we define weak transitions \(\mu _1 \Rightarrow \mu _2\) inductively to express that either \(\mu _1 = \mu _2\) or \(\mu _1 \Rightarrow \mu '\) and Open image in new window . We exploit the determinacy for observable actions \(a \in \textsf {M}_{\texttt {c}} \cup \{ \sigma \}\) and write \(\mu \odot a\) for the unique \(\mu '\) such that Open image in new window , if it exists.
Definition 2
Given a cap \(\Vdash _{\texttt {c}} = (\mathbb {P} _{\texttt {c}}, \varepsilon , \mathrel {{\mathop {\longrightarrow }\limits ^{}}})\), an observable action \(a \in \textsf {M}_{\texttt {c}} \cup \{ \sigma \}\) is enabled in state \(\mu \in \mathbb {P} _{\texttt {c}} \), written \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }a\), if \(\mu ' \odot a\) exists for all \(\mu '\) such that \(\mu \Rightarrow \mu '\). A sequence \({{\varvec{a}}} \in (\textsf {M}_{\texttt {c}} \cup \{ \sigma \})^*\) of observable actions is enabled in \(\mu \in \mathbb {P} _{\texttt {c}} \), written \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{a}}}\), if (i) \({{\varvec{a}}} = \varepsilon \) or (ii) \({{\varvec{a}}} = a\, {{\varvec{b}}}\), \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }a\) and \(\mu \odot a \Vdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{b}}}\). \(\square \)
Example 1
Consider the policy \(\Vdash _{\texttt {s}} \) in Fig. 1 of an Esterel pure signal \({\texttt {s}} \). An edge labelled a : L from state \(\mu _1\) to \(\mu _2\) corresponds to a transition Open image in new window in \(\Vdash _{\texttt {s}} \). The start state is \(\varepsilon = 0\) and the methods \(\textsf {M}_{\texttt {s}} = \{ \mathop {\mathtt {pres}}, \mathop {\mathtt {emit}} \}\) are always admissible, i.e., \(\mu \odot m\) is defined in each state \(\mu \) for all methods m. The presence test does not change the state and any emission sets it to 1, i.e., \(\mu \odot \mathop {\mathtt {pres}} = \mu \) and \(\mu \odot \mathop {\mathtt {emit}} = 1\) for all \(\mu \in \mathbb {P} _{\texttt {s}} \). Each signal status is reset to 0 with the clock tick, i.e., \(\mu \odot \sigma = 0\). Clearly, \(\Vdash _{\texttt {s}} \) satisfies Determinacy. A presence test on a signal that is not emitted yet has to wait for all pending concurrent emissions, that is \(\mathop {\mathtt {emit}}\) blocks \(\mathop {\mathtt {pres}}\) in state 0, i.e., Open image in new window . Otherwise, no transition is blocked. Also, all competing transitions Open image in new window and Open image in new window that do not block each other, are of the form \(\mu _1 = \mu _2\), from which Confluence follows. Note that since there are no silent transitions, Maximal Progress is always fulfilled too. Moreover, an action sequence is enabled in a state \(\mu \) (Definition 2) iff it corresponds to a path in the automaton starting from \(\mu \). Hence, for \({{\varvec{m}}} \in \textsf {M}_{\texttt {s}} ^*\) we have \(0 \Vdash _{\texttt {s}} \mathop {\downarrow }{{\varvec{m}}}\) iff \({{\varvec{m}}}\) is in the regular language^{6} \(\mathop {\mathtt {pres}} ^{*} + \mathop {\mathtt {pres}} ^{*} \mathop {\mathtt {emit}} (\mathop {\mathtt {pres}} + \mathop {\mathtt {emit}})^{*}\) and \(1 \Vdash _{\texttt {s}} \mathop {\downarrow }{{\varvec{m}}}\) for all \({{\varvec{m}}} \in \textsf {M}_{\texttt {s}} ^{*}\).
Contrast \(\Vdash _{\texttt {s}} \) with the policy \(\Vdash _{\texttt {c}} \) of a synchronous immutable variable (IVar) \({\texttt {c}}\) shown in Fig. 2 with methods \(\textsf {M}_{\texttt {c}} = \{ {{\texttt {get}}}, {{\texttt {put}}} \}\). During each instant an IVar can be written (put) at most once and cannot be read (get) until it has been written. No value is stored between ticks, which means the memory is only temporary and can be reused, e. g., IVars can be implemented by wires. Formally, \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }{{\texttt {put}}} \) iff \(\mu = 0\), where 0 is the initial empty state and \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }{{\texttt {get}}} \) iff \(\mu = 1\), where 1 is the filled state. The transition Open image in new window switches to filled state where get is admissible but put is not, anymore. The blocking \(\{ {{\texttt {put}}} \}\) means there cannot be other concurrent threads writing \({\texttt {c}}\) at the same time. \(\square \)
2.4 Enabling and Policy Conformance
A policy describes what a single thread can do to a csm variable \({\texttt {c}}\) when it operates alone. In a cap all potential activities of the environment are added as \(\tau \)transitions to block the tuc ’s accesses. To implement this \(\tau \)locking we define an operation that generates a cap \([\mu , \gamma ]\) out of a policy. In this construction, \(\mu \in \mathbb {P} _{\texttt {c}} \) is a policy state recording the history of methods that have been performed on \({\texttt {c}}\) so far (\( must \) information). The second component \(\gamma \subseteq \textsf {M}_{\texttt {c}} ^*\) is a prediction for the sequences of methods that can still potentially be executed by the concurrent environment (\( can \) information).
Definition 3
 1.
The observable transitions Open image in new window are such that \(\gamma _1 = \gamma _2\) and Open image in new window provided that for all sequences \(n\,{{\varvec{n}}} \in \gamma _1\) with Open image in new window we have \(n \not \in L\).
 2.
The silent transitions are Open image in new window such that \(\emptyset \ne m\, \gamma _2 \subseteq \gamma _1\) and Open image in new window .
 3.
The clock transitions are Open image in new window such that \(\gamma _1 = \emptyset \) and Open image in new window . \(\square \)
Silent steps arise from the concurrent environment: A step Open image in new window removes some prefix method m from the environment prediction \(\gamma _1\), which contracts to an updated suffix prediction \(\gamma _2\) with \(m\, \gamma _2 \subseteq \gamma _1\). This method m is executed on the csm variable, changing the policy state to \(\mu _2 = \mu _1 \odot m\). A method m is enabled, \([\mu , \gamma ] \Vdash _{\texttt {c}} \mathop {\downarrow }m\), if for all \([\mu _1, \gamma _1]\) which are \(\tau \)reachable from \([\mu , \gamma ]\), method m is admissible, i.e., Open image in new window for some \(\mu _2\).
Example 2
Consider concurrent threads Open image in new window , where \(P_2 = {\texttt {zs}}.{{{\texttt {put}}} (5)} \mathop {{\texttt {;}}} u {{\texttt {\,=\,}}} \) \({\texttt {ys}}.{{{\texttt {get}}}}()\) and \(P_1 = v {{\texttt {\,=\,}}} {\texttt {zs}}.{{{\texttt {get}}}}() \mathop {{\texttt {;}}} {\texttt {ys}}.{{\texttt {put}}} (v+1)\) with IVars \({\texttt {zs}} \), \({\texttt {ys}} \) according to Example 1. Under the IVar policy the execution is deterministic, so that first \(P_2\) writes on \({\texttt {zs}}\), then \(P_1\) reads from \({\texttt {zs}}\) and writes to \({\texttt {ys}}\), whereupon finally \(P_1\) reads \({\texttt {ys}}\). Suppose the variables have reached policy states \(\mu _{\texttt {zs}} \) and \(\mu _{\texttt {ys}} \) and the threads are ready to execute the residual programs \(P_i'\) waiting at some method call \({\texttt {c}} _i.m_i(v_i)\), respectively. Since thread \(P_i'\) is concurrent with the other \(P_{3i}'\), it can only proceed if \(m_i\) is not blocked by \(P_{3i}'\), i.e., if \([\mu _{{\texttt {c}} _i}, can _{{\texttt {c}} _i}(P_{3i}') ] \Vdash _{{\texttt {c}} _i} \mathop {\downarrow }m_i\), where \( can _{{\texttt {c}}}(P) \subseteq \textsf {M}_{\texttt {c}} ^*\) is the set of method sequences predicted for P on \({\texttt {c}} \).
Initially we have \(\mu _{\texttt {zs}} = 0 = \mu _{\texttt {ys}} \). Since method \({{\texttt {get}}} \) is not admissible in state 0, we get \([0, can _{{\texttt {zs}}}(P_{2}) ] \nVdash _{{\texttt {zs}}} \mathop {\downarrow }{{\texttt {get}}} \) by Definitions 3 and 2. So, \(P_1\) is blocked. The \({\texttt {zs}}.{{\texttt {put}}} \) of \(P_2\), however, can proceed. First, since no predicted method sequence \( can _{{\texttt {zs}}}(P_{1}) = \{ {{\texttt {get}}} \}\) of \(P_1\) starts with \({{\texttt {put}}} \), the transition Open image in new window implies that Open image in new window by Definition 3(1). Moreover, since get of \(P_1\) is not admissible in 0, there are no silent transitions out of \([0, can _{{\texttt {zs}}}(P_{1}) ]\) according to Definition 3(2). Thus, \([0, can _{{\texttt {zs}}}(P_{1}) ] \Vdash _{\texttt {zs}} \mathop {\downarrow }{{\texttt {put}}} \), as claimed.
When the \({\texttt {zs}}.{{\texttt {put}}} \) is executed by \(P_2\) it turns into \(P_2' = u {{\texttt {\,=\,}}} {\texttt {ys}}.{{\texttt {get}}} ()\) and the policy state for \({\texttt {zs}} \) advances to \(\mu _{\texttt {zs}} ' = 1\), while \({\texttt {ys}} \) is still at \(\mu _{\texttt {ys}} = 0\). Now \({\texttt {ys}}.{{\texttt {get}}} \) of \(P_2'\) blocks for the same reason as \({\texttt {zs}} \) was blocked in \(P_1\) before. But since \(P_2\) has advanced, its prediction on \({\texttt {zs}} \) reduces to \( can _{{\texttt {zs}}}(P_2') = \emptyset \). Therefore, the transition Open image in new window implies Open image in new window by Definition 3(1). Also, there are no silent transitions out of \([1, can _{{\texttt {zs}}}(P_2') ]\) by Definition 3(2) and so \([\mu _{\texttt {zs}} ', can _{{\texttt {zs}}}(P_2') ] \Vdash _{\texttt {zs}} \mathop {\downarrow }{{\texttt {get}}} \) by Definition 2. This permits \(P_1\) to execute \({\texttt {zs}}.{{\texttt {get}}} ()\) and proceed to \(P_1' = {\texttt {ys}}.{{\texttt {put}}} (5+1)\). The policy state of \({\texttt {zs}} \) is not changed by this, neither is the state of \({\texttt {ys}}\), whence \(P_2'\) is still blocked. Yet, we have \([\mu _{\texttt {ys}}, can _{{\texttt {zs}}}(P_2') ] \Vdash _{\texttt {ys}} \mathop {\downarrow }{{\texttt {put}}} \) which lets \(P_1'\) complete \({\texttt {ys}}.{{\texttt {put}}} \). It reaches \(P_1''\) with \( can _{{\texttt {ys}}}(P_1'') = \emptyset \) and changes the policy state of \({\texttt {ys}}\) to \(\mu _{\texttt {ys}} ' = 1\). At this point, \([\mu _{\texttt {ys}} ', can _{{\texttt {zs}}}(P_1'') ] \Vdash _{\texttt {ys}} \mathop {\downarrow }{{\texttt {get}}} \) which means \(P_2'\) unblocks to execute \({\texttt {ys}}.{{\texttt {get}}} \). \(\square \)
Definition 4
Let \(\Vdash _{\texttt {c}} \) be a policy for \({\texttt {c}}\). A method sequence \({{\varvec{m}}}_{1}\) blocks another \({{\varvec{m}}}_{2}\) in state \(\mu \), written \(\mu \Vdash _{\texttt {c}} {{\varvec{m}}}_{1} \rightarrow {{\varvec{m}}}_{2}\), if \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{m}}}_{2}\) but \([\mu , \{ {{\varvec{m}}}_{1} \}] \nVdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{m}}}_{2}\). Two method sequences \({{\varvec{m}}}_{1}\) and \({{\varvec{m}}}_{2}\) are concurrently enabled, denoted \(\mu \Vdash _{\texttt {c}} {{\varvec{m}}}_{1} \mathrel {\diamond _{}} {{\varvec{m}}}_{2}\) if \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{m}}}_{1}\), \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{m}}}_{2}\) and both \(\mu \nVdash _{\texttt {c}} {{\varvec{m}}}_{1} \rightarrow {{\varvec{m}}}_{2}\) and \(\mu \nVdash _{\texttt {c}} {{\varvec{m}}}_{2} \rightarrow {{\varvec{m}}}_{1}\). \(\square \)
Our operational semantics will only let a tuc execute a sequence \({{\varvec{m}}}\) provided \([\mu , \gamma ] \Vdash _{\texttt {c}} \mathop {\downarrow }{{\varvec{m}}}\), where \(\mu \) is the current policy state of \({\texttt {c}} \) and \(\gamma \) the predicted activity in the tuc ’s concurrent environment. Symmetrically, the environment will execute any \({{\varvec{n}}} \in \gamma \) only if it is enabled with respect to \({{\varvec{m}}}\), i.e., if \([\mu , \{{{\varvec{m}}}\}] \Vdash \mathop {\downarrow }{{\varvec{n}}}\). This means \(\mu \Vdash _{\texttt {c}} {{\varvec{m}}} \mathrel {\diamond _{}} {{\varvec{n}}}\). Policy coherence (Definition 5 below) then implies that every interleaving of the sequences \({{\varvec{m}}}\) and any \({{\varvec{n}}} \in \gamma \) leads to the same return values and final variable state (Proposition 1).
2.5 Coherence and Determinacy
A method call m(v) combines a method \(m \in \textsf {M}_{\texttt {c}} \) with a method parameter^{7} \(v \in \mathbb {D} \), where \(\mathbb {D} \) is a universal domain for method arguments and return values, including the special don’t care value \( {\_} \in \mathbb {D} \). We denote by \(\textsf {A}_{\texttt {c}} = \{ m(v) \mid m \in \textsf {M}_{\texttt {c}}, v \in \mathbb {D} \}\) the set of all method calls on object \({\texttt {c}} \). Sequences of method calls \(\alpha \in \textsf {A}_{\texttt {c}} ^*\) can be abstracted back into sequences of methods \(\alpha ^\# \in \textsf {M}_{\texttt {c}} ^*\) by dropping the method parameters: \(\varepsilon ^\# = \varepsilon \) and \((m(v)\, \alpha )^\# = m\, \alpha ^\#\).
Coherence concerns the semantics of method calls as state transformations. Let \(\mathbb {S} _{\texttt {c}} \) be the domain of memory states of the object \({\texttt {c}} \) with initial state \( init _{\texttt {c}} \in \mathbb {S} _{\texttt {c}} \). Each method call \(m(v) \in \textsf {A}_{\texttt {c}} \) corresponds to a semantical action \([\![m(v)]\!]_{\texttt {c}} \in \mathbb {S} _{\texttt {c}} \rightarrow (\mathbb {D} \times \mathbb {S} _{\texttt {c}})\). If \(s \in \mathbb {S} _{\texttt {c}} \) is the current state of the object then executing a call m(v) on \({\texttt {c}} \) returns a pair \((u, s') = [\![m(v)]\!]_{\texttt {c}} (s)\) where the first projection \(u \in \mathbb {D} \) is the return value from the call and the second projection \(s' \in \mathbb {S} _{\texttt {c}} \) is the new updated state of the variable. For convenience, we will denote \(u = \pi _1 [\![m(v)]\!]_{\texttt {c}} (s)\) by \(u = s.m(v)\) and \(s' = \pi _2[\![m(v)]\!]_{\texttt {c}} (s)\) by \(s' = s \odot m(v)\). The action notation is extended to sequences of calls \(\alpha \in \textsf {A}_{\texttt {c}} ^*\) in the natural way: \(s \odot \varepsilon = s\) and \(s \odot (m(v)\,\alpha ) = (s \odot m(v)) \odot \alpha \).
For policybased scheduling we assume an abstraction function mapping a memory state \(s \in \mathbb {S} _{\texttt {c}} \) into a policy state \(s^\# \in \mathbb {P} _{\texttt {c}} \). Specifically, \( init _{\texttt {c}} ^\# = \varepsilon \). Further, we assume the abstraction commutes with method execution in the sense that if we execute a sequence of calls and then abstract the final state, we get the same as if we executed the policy automaton on the abstracted state in the first place. Formally, \((s \odot \alpha )^\# = s^\# \odot \alpha ^\#\) for all \(s \in \mathbb {S} _{\texttt {c}} \) and \(\alpha \in A_{\texttt {c}} ^*\).
Definition 5
(Coherence). A csm variable \({\texttt {c}} \) is policycoherent if for all method calls \(a, b \in \textsf {A}_{\texttt {c}} \) whenever \(s^\# \Vdash _{\texttt {c}} a^\# \mathrel {\diamond _{}} b^\#\) for a state \(s \in \mathbb {S} _{\texttt {c}} \), then a and b are confluent in the sense that \(s.a = (s \odot b).a\), \(s.b = (s \odot a).b\) and \(s \odot a \odot b = s \odot b \odot a\). \(\square \)
Example 3
Esterel pure signals do not carry any data value, so their memory state coincides with the policy state, \(\mathbb {S} _{\texttt {s}} = \mathbb {P} _{\texttt {s}} = \{ 0, 1 \}\) and \(s^\# = s\). An emission \(\mathop {\mathtt {emit}} \) does not return any value but sets the state of \({\texttt {s}} \) to 1, i.e., \(s.\mathop {\mathtt {emit}} ( {\_} ) = {\_} \in \mathbb {D} \) and \({s}{\odot }{\mathop {\mathtt {emit}} ( {\_} ) = 1 \in \mathbb {S} _{\texttt {s}}}\). A present test returns the state, \(s.\mathop {\mathtt {pres}} ( {\_} ) = s\), but does not modify it, \({s}{\odot }{\mathop {\mathtt {pres}} ( {\_} ) = s}\). From the policy Fig. 1 we find that the concurrent enablings \(s^\# \Vdash _{\texttt {s}} a^\# \mathrel {\diamond _{}} b^\#\) according to Definition 4 are (i) \(a = b \in \{ \mathop {\mathtt {pres}} ( {\_} ), \mathop {\mathtt {emit}} ( {\_} ) \}\) for arbitrary s, or (ii) \(s = 1\), \(a = \mathop {\mathtt {emit}} ( {\_} )\) and \(b = \mathop {\mathtt {pres}} ( {\_} )\). In each of these cases we verify \(s.a = (s \odot b).a\), \(s.b = (s \odot a).b\) and \(s \odot a \odot b = s \odot b \odot a\) without difficulty. Note that \(1 \Vdash _{\texttt {s}} \mathop {\mathtt {emit}} \mathrel {\diamond _{}} \mathop {\mathtt {pres}} \) since the order of execution is irrelevant if \(s = 1\). On the other hand, \(0 \nVdash _{\texttt {s}} \mathop {\mathtt {emit}} \mathrel {\diamond _{}} \mathop {\mathtt {pres}} \) because in state 0 both methods are not confluent. Specifically, \(0.\mathop {\mathtt {pres}} ( {\_} ) = 0 \ne 1 = (0 \odot \mathop {\mathtt {emit}} ( {\_} )).\mathop {\mathtt {pres}} ( {\_} )\). \(\square \)
A special case are linear precedence policies where \(\mu \Vdash _{\texttt {c}} \mathop {\downarrow }m\) for all \(m \in \textsf {M}_{\texttt {c}} \) and \(\mu \Vdash _{\texttt {c}} m \rightarrow n\) is a linear ordering on \(\textsf {M}_{\texttt {c}} \), for all policy states \(\mu \). Then, for no state we have \(\mu \Vdash _{\texttt {c}} m_{1} \mathrel {\diamond _{}} m_2\), so there is no concurrency and thus no confluence requirement to satisfy at all. Coherence of \({\texttt {c}} \) is trivially satisfied whatever the semantics of method calls. For any two admissible methods one takes precedence over the other and thus the enabling relation becomes deterministic. There is however a risk of deadlock which can be excluded if we assume that threads always call methods in order of decreasing precedence.
The other extreme case is where the policy makes all methods concurrently enabled, i.e., \(\mu \Vdash _{\texttt {c}} m_1 \mathrel {\diamond _{}} m_2\) for all policy states \(\mu \) and methods \(m_1\), \(m_2\). This avoids deadlock completely and gives maximal concurrency but imposes the strongest confluence condition, viz. independently of the scheduling order of any two methods, the resulting variable state must be the same. This requires complete isolation of the effects of any two methods. Such an extreme is used, e. g., in the CR library [19]. The typical csm variable, however, will strike a tradeoff between these two extremes. It will impose a sensible set of precedences that are strong enough to ensure coherent implementations and thus determinacy for policyconformant scheduling, while at the same time being sufficiently relaxed to permit concurrent implementations and avoiding unnecessary deadlocks risking that programs are rejected by the compiler as unscheduleable.
Whatever the policies, if the variables are coherent, then all policyconformant interleavings are indistinguishable for each csm variable. To state schedule invariance in its general form we lift method actions and independence to multivariable sequences of methods calls \(\textsf {A} = \{ {\texttt {c}}.m(v) \mid {\texttt {c}} \in \textsf {O}, m(v) \in \textsf {A}_{\texttt {c}} \}\). For a given sequence \(\alpha \in \textsf {A}^*\) let \(\pi _{\texttt {c}} (\alpha ) \in \textsf {A}_{\texttt {c}} ^*\) be the projection of \(\alpha \) on \({\texttt {c}} \), formally \(\pi _{\texttt {c}} (\varepsilon ) = \varepsilon \), \(\pi _{\texttt {c}} ({\texttt {c}}.m(v)\, \alpha ) = m(v)\, \pi _{\texttt {c}} (\alpha )\) and \(\pi _{\texttt {c}} ({\texttt {c}} '.m(v)\, \alpha ) = \pi _{\texttt {c}} (\alpha )\) for \({\texttt {c}} ' \ne {\texttt {c}} \). A global memory \({\varSigma } \in \mathbb {S} = \prod _{{\texttt {c}} \in \textsf {O}} \mathbb {S} _{\texttt {c}} \) assigns a local memory \({\varSigma }.{\texttt {c}} \in \mathbb {S} _{\texttt {c}} \) to each variable \({\texttt {c}} \). We write \( init \) for the initial memory that has \( init .{\texttt {c}} = init _{\texttt {c}} \) and \(( init .{\texttt {c}})^\# = \varepsilon \in \mathbb {P} _{\texttt {c}} \).
Given a global memory \({\varSigma } \in \mathbb {S} \) and sequences \(\alpha , \beta \in \textsf {A}^*\) of method calls, we extend the independence relation of Definition 4 variablewise, defining \({\varSigma } \Vdash \alpha \mathrel {\diamond _{}} \beta \) iff \(({\varSigma }.{\texttt {c}})^\# \Vdash _{\texttt {c}} (\pi _{\texttt {c}} (\alpha ))^\# \mathrel {\diamond _{}} (\pi _{\texttt {c}} (\beta ))^\#\). The application of a method call \(a \in \textsf {A}\) to a memory \({\varSigma } \in \mathbb {S} \) is written \({\varSigma }.a \in \mathbb {S} \) and defined \(({\varSigma }.({\texttt {c}}.m(v))).{\texttt {c}} = ({\varSigma }.{\texttt {c}}).m(v)\) and \(({\varSigma }.({\texttt {c}}.m(v))).{\texttt {c}} ' = {\varSigma }.{\texttt {c}} '\) for \({\texttt {c}} ' \ne {\texttt {c}} \). Analogously, method actions are lifted to global memories, i.e., \(({\varSigma } \odot {\texttt {c}}.m(v)).{\texttt {c}} ' = {\varSigma }.{\texttt {c}} '\) if \({\texttt {c}} ' \ne {\texttt {c}} \) and \(({\varSigma } \odot {\texttt {c}}.m(v)).{\texttt {c}} = {\varSigma }.{\texttt {c}} \odot m(v)\).
Proposition 1
(Commutation). Let all csm variables be policycoherent and \({\varSigma } \Vdash a\mathrel {\diamond _{}} \alpha \) for a memory \({\varSigma } \in \mathbb {S} \), method call \(a \in \textsf {V}\) and sequences of method calls \(\alpha \in \textsf {V}^*\). Then, \({\varSigma } \odot a \odot \alpha = {\varSigma } \odot \alpha \odot a\) and \({\varSigma }.a = ({\varSigma } \odot \alpha ).a\).
2.6 Policies and Modularity
Consider the synchronous dataflow network cnt in Fig. 3b with three process nodes, a multiplexer mux, a register reg and an incrementor inc. Their DCoL code is given in Fig. 3a. The network implements a settable counter, which produces at its output \({\texttt {ys}}\) a stream of consecutive integers, incremented with each clock tick. The wires \({\texttt {ys}}\), \({\texttt {zs}}\) and \({\texttt {ws}}\) are IVars (see Example 2) carrying a single integer value per tick. The input \({\texttt {xs}}\) is a pure Esterel signal (see Example 1). The counter state is stored by reg in a local variable xv with \({{\texttt {read}}} \) and \({{\texttt {write}}} \) methods that can be called by a single thread only. The register is initialised to value 0 and in each subsequent tick the value at \({\texttt {ys}}\) is stored. The inc takes the value at \({\texttt {zs}}\) and increments it. When the signal \({\texttt {xs}}\) is absent, mux passes the incremented value on \({\texttt {ws}}\) to \({\texttt {ys}}\) for the next tick. Otherwise, if \({\texttt {xs}}\) is present then mux resets \({\texttt {ys}}\).
Now suppose, for modularity, the reg node is precompiled into a synchronous IO automaton to be used by mux and inc as a black box component. Then, \({{\texttt {reg}}} \) must be split into three modes [20] \({{\texttt {reg}}}.{{\texttt {init}}} \), \({{\texttt {reg}}}.{{\texttt {get}}} \) and \({{\texttt {reg}}}.{{\texttt {set}}} \) that can be called independently in each instant. The init mode initialises the register memory with 0. The \({{\texttt {get}}} \) mode extracts the buffered value and \({{\texttt {set}}} \) stores a new value into the register. Since there may be data races if get and set are called concurrently on reg, a policy must be imposed. In the scheduling of Fig. 3b, first \({{\texttt {reg}}}.{{\texttt {get}}} \) is executed to place the output on \({\texttt {zs}}\). Then, \({{\texttt {reg}}} \) waits for \({{\texttt {mux}}} \) to produce the next value of \({\texttt {ys}}\) from \({\texttt {xs}}\) or \({\texttt {ws}}\). Finally, \({{\texttt {reg}}}.{{\texttt {set}}} \) is executed to store the current value of \({\texttt {ys}}\) for the next tick. Thus, the natural policy for the register is to require that in each tick set is called by at most one thread and if so no concurrent call to get by another thread happens afterwards. In addition, the policy requires init to take place at least once before any set or get. Hence, the policy has two states \(\mathbb {P} _{{\texttt {reg}}} = \{ 0, 1 \}\) with initial \(\varepsilon = 0\) and admissibility such that \(0 \Vdash _{{\texttt {reg}}} \mathop {\downarrow }m\) iff \(m = {{\texttt {init}}} \) and \(1 \Vdash _{{\texttt {reg}}} \mathop {\downarrow }m\) for all m. The transitions are \(0 \odot {{\texttt {init}}} = 1\) and \(1 \odot m = 1\) for all \(m \in \textsf {M}_{{\texttt {reg}}} \). Further, for coherence, in state 1 no set may be concurrent and every get must take place before any concurrent set. This means, we have \(1 \Vdash _{{{\texttt {reg}}}} m \rightarrow {{\texttt {set}}} \) for all \(m \in \{ {{\texttt {get}}}, {{\texttt {set}}} \}\). Figure 3c shows the partially compiled code in which reg is treated as a compiled object. The policy on reg makes sure the accesses by mux and inc are scheduled in the right way (see Example 4). Note that reg is not an IVar because it has memory.
The cnt example exhibits a general pattern found in the modular compilation of SP: Modules (here reg) may be exercised several times in a synchronous tick through modes which are executed in a specific prescribed order. Mode calls (here \({{\texttt {reg}}}.{{\texttt {set}}} \), \({{\texttt {reg}}}.{{\texttt {get}}} \)) in the same module are coupled via common shared memory (here the local variable \({\texttt {xs}}\)) while mode calls in distinct modules are isolated from each other [15, 20].
3 Constructive Semantics of DCoL
We write \(\pi _{\texttt {c}} ({{\varvec{m}}}) \in \textsf {M}_{\texttt {c}} ^*\) for the projection of a method sequence \({{\varvec{m}}} \in \textsf {M}^*\) to variable \({\texttt {c}} \) and write \(\pi _{\texttt {c}} (\varPi )\) for its lifting to sets of sequences. Prefixing is lifted, too, i.e., \({\texttt {c}}.m \odot \varPi = \{ {\texttt {c}}.m\, {{\varvec{m}}} \mid {\varvec{m}} \in \varPi \}\) for any \({\texttt {c}}.m \in \textsf {M}\).
Most of the rules in Figs. 4 and 5 should be straightforward for the reader familiar with structural operational semantics. \(\textsf {Seq} _1\) is the case of a sequential P; Q where P pauses or waits (\(k' \ne 0\)) and \(\textsf {Seq} _2\) is where P terminates and control passes into Q. The statements \(\mathop {\mathtt {skip}} \) and \(\mathop {\mathtt {pause}} \) are handled by rules \(\textsf {Cmp} _1\) and \(\textsf {Cmp} _2\). The rule \(\textsf {Rec} \) explains recursion \(\mathop {\textsf {rec}} p. P\) by syntactic unfolding of the recursion body P. All interaction with the memory takes place in the method calls \(\mathop {{\texttt {let}}} x = {\texttt {c}}.m(e)\; \mathop {{\texttt {in}}} P\). Rule \(\textsf {Let} _1\) is applicable when the method call is enabled, i.e., \([{\varSigma }, \varPi ] \Vdash \mathop {\downarrow }{\texttt {c}}.m\). Since processes are closed, the argument expression e must evaluate, \( eval (e) = v\), and we obtain the new memory \({\varSigma } \odot {\texttt {c}}.m(v)\) and return value \({\varSigma }.{\texttt {c}}.m(v)\). The return value is substituted for the local (stack allocated) identifier x, giving the continuation process \(P\{{\varSigma }.{\texttt {c}}.m(v)/x\}\) which is run in the updated context \({\varSigma } \odot {\texttt {c}}.m(v); \varPi \). The prediction \(\varPi \) remains the same. The second rule \(\textsf {Let} _2\) is used when the method call is blocked or the thread wants to wait and yield to the scheduler. The rules for conditionals \(\textsf {Cnd} _1\), \(\textsf {Cnd} _2\) are canonical. More interesting are the rules \(\textsf {Par} _1\)–\(\textsf {Par} _4\) for parallel composition, which implement nondeterministic thread switching. It is here where we need to generate predictions and pass them between the threads to exercise the policy control.
The key operation is the computation of the \( can \)prediction of a process P to obtain an overapproximation of the set of possible method sequences potentially executed by P. For compositionality we work with sequences \( can ^s(P) \subseteq \textsf {M}^*\times \{ 0 , 1 \}\) stoppered with a completion code 0 if the sequence ends in termination or 1 if it ends in pausing. The symbols \(\bot _0\), \(\bot _1\) and \(\top \) are the terminated, paused and fully unconstrained \( can \) contexts, respectively, with \(\bot _0 = \{ (\varepsilon , 0) \}\), \(\bot _1 = \{ (\varepsilon , 1) \}\) and \(\top = \textsf {M}^*\times \{ 0 , 1 \}\). The set \( can ^s(P) \), defined in Fig. 6, is extracted from the structure of P using prefixing \({\texttt {c}}.m \odot \varPi '\), choice \(\varPi _1' \oplus \varPi _2' = \varPi _1' \cup \varPi _2'\), parallel \(\varPi _1' \otimes \varPi _2'\) and sequential composition \(\varPi _1' \cdot \varPi _2'\). Sequential composition is obtained pairwise on stoppered sequences such that \(({{\varvec{m}}}, 0) \cdot ({{\varvec{n}}}, c) = ({{\varvec{m}}}\, {\varvec{n}}, c)\) and \(({{\varvec{m}}}, 1) \cdot ({{\varvec{n}}}, c) = ({{\varvec{m}}}, 1)\). As a consequence, \(\bot _0 \cdot \varPi ' = \varPi '\) and \(\bot _1 \cdot \varPi ' = \bot _1\). Parallel composition is pairwise free interleaving with synchronisation on completion codes. Specifically, a product \(({{\varvec{m}}}, c) \otimes ({{\varvec{n}}}, d)\) generates all interleavings of \({{\varvec{m}}}\) and \({{\varvec{n}}}\) with a completion that models a parallel composition that terminates iff both threads terminate and pauses if one pauses. Formally, \(({{\varvec{m}}}, c) \otimes ({{\varvec{n}}}, d) = \{ ({{\varvec{c}}}, \textit{max} (c, d)) \mid {{\varvec{c}}} \in {\varvec{m}} \otimes {{\varvec{n}}} \}\). Thus, \(\varPi _P' \otimes \varPi _Q' = \bot _0\) iff \(\varPi _P' = \bot _0 = \varPi _Q'\) and \(\varPi _P' \otimes \varPi _Q' = \bot _1\) if \(\varPi _P' = \bot _1 = \varPi _Q'\), or \(\varPi _P' = \bot _0\) and \(\varPi _Q' = \bot _1\), or \(\varPi _P' = \bot _1\) and \(\varPi _Q' = \bot _0\). From \( can ^s(P) \) we obtain \( can (P) \subseteq \textsf {M}^*\) by dropping all stopper codes, i.e., \( can (P) = \{ {{\varvec{m}}} \mid \exists d.\, ({{\varvec{m}}}, d) \in can ^s(P) \}\).
The rule \(\textsf {Par} _1\) exercises a parallel Open image in new window by performing an sstep in P. This sstep is taken in the extended context \({\varSigma }; \varPi \otimes can (Q)\) in which the prediction of the sibling Q is added to the method prediction \(\varPi \) for the outer environment in which the parent Open image in new window is running. In this way, Q can block method calls of P. When P finally yields as \(P'\) with a nonterminating completion code, \(0 \ne k' \in \{ \bot , 1 \}\), the parallel completes as Open image in new window with code \(k' \sqcap k_Q\). This operation is defined \(k_1 \sqcap k_2 = 1\) if \(k_1 = 1 = k_2\) and \(k_1 \sqcap k_2 = \bot \), otherwise. When P terminates its sstep with code \(k' = 0\) then we need rule \(\textsf {Par} _2\) which removes child \(P'\) from the parallel composition. The rules \(\textsf {Par} _3, \textsf {Par} _4\) are symmetrical to \(\textsf {Par} _1, \textsf {Par} _2\). They run the right child Q of a parallel Open image in new window .
Completion and Stability. A process \(P'\) is 0stable if \(P' = \mathop {\mathtt {skip}} \) and 1stable if \(P' = \mathop {\mathtt {pause}} \) or \(P' = P_1' \mathop {{\texttt {;}}} P_2'\) and \(P_1'\) is 1stable, or Open image in new window , and \(P_i'\) are 1stable. A process is stable if it is 0stable or 1stable. A process expression is wellformed if in each subexpression Open image in new window of P the completion annotations are matching with the processes, i.e., if \(k_i \ne \bot \) then \(P_i\) is \(k_i\)stable. Stable processes are wellformed by definition. For stable processes we define a (syntactic) tick function which steps a stable process to the next tick. It is defined such that \(\mathop {\sigma }(\mathop {\mathtt {skip}}) = \mathop {\mathtt {skip}} \), \(\mathop {\sigma }(\mathop {\mathtt {pause}}) = \mathop {\mathtt {skip}} \), \(\mathop {\sigma }(P_1' \mathop {{\texttt {;}}} P_2') = \mathop {\sigma }(P_1') \mathop {{\texttt {;}}} P_2'\) and Open image in new window .
Example 4
where \(m_5 = {\texttt {ws}}.{{\texttt {get}}} \) and \(m_6 = {{\texttt {reg}}}.{{\texttt {set}}} \). To justify the rule \(\textsf {Par} _2\) consider that \(\{\epsilon \} \otimes can (\mathop {\mathtt {pause}}; I) = \{\epsilon \} \otimes \{\epsilon \} = \{\epsilon \}\). At this point we have reached a 1stable process. With the tick function we advance to the next tick, Open image in new window which behaves like Open image in new window . \(\square \)
3.1 Determinacy, Termination and Constructiveness
Determinacy of DCoL is a result of two components, monotonicity of policyconformant scheduling and csm coherence. Monotonicity ensures that whenever a method is executable and policyenabled, then it remains policyenabled under arbitrary ssteps of the environment. Symmetrically, the environment cannot be blocked by a thread taking policyenabled computation steps.
The second building block for determinacy is csm variable coherence. Consider a context \({\varSigma }; \varPi _Q\) in which we run an sstep of P with prediction \(\varPi _Q\) for concurrent process Q, resulting in a final memory \({\varSigma } _P'\) arising from executing a sequence \({{\varvec{m}}}_{P}\) of method calls from P. Because of the policy constraint, the sequence \({{\varvec{m}}}_{P}\) must be enabled under all predictions \({{\varvec{n}}} \in \varPi _Q\), i.e., \([{\varSigma }, {{\varvec{n}}}] \Vdash \mathop {\downarrow }{{\varvec{m}}}_{P}\). Suppose, on the other side, we sstep the process Q in the same memory \({\varSigma } \) with prediction \(\varPi _P\) for P, resulting in an action sequence \({{\varvec{m}}}_{Q}\) and final memory \({\varSigma } _Q'\). Then, by the same reasoning, \([{\varSigma }, {{\varvec{n}}}] \Vdash \mathop {\downarrow }{{\varvec{m}}}_{Q}\) for all \({{\varvec{n}}} \in \varPi _P\). But since \({{\varvec{m}}}_{P}\) is an actual execution of P it must be in the prediction for P, i.e., \({{\varvec{m}}}_{P} \in \varPi _P\) and symmetrically, \({{\varvec{m}}}_{Q} \in \varPi _Q\). But then we have \([{\varSigma }, {{\varvec{m}}}_{Q}] \Vdash \mathop {\downarrow }{{\varvec{m}}}_{P}\) and \([{\varSigma }, {{\varvec{m}}}_{P}] \Vdash \mathop {\downarrow }{{\varvec{m}}}_{P}\) which means \({\varSigma } \Vdash {{\varvec{m}}}_{P} \mathrel {\diamond _{}} {{\varvec{m}}}_{Q}\). Now if the semantics of method calls is policycoherent then the Monotonicity can be exploited to derive a confluence property for processes which guarantees that \({{\varvec{m}}}_{P}\) can still be executed by P in state \({\varSigma } _Q'\) and \({{\varvec{m}}}_{Q}\) by Q in state \({\varSigma } _P'\), and both lead to the same final memory.
Theorem 1
(Diamond Property). If all csm variables are policycoherent then the sstep semantics is confluent. Formally, given two derivations Open image in new window and Open image in new window , Then, there exist \({\varSigma } '\), \(k'\) and \(P'\) such that Open image in new window and Open image in new window .
Theorem 1 shows that no matter how we schedule the ssteps of local threads to create an sstep of a parallel composition, the final result will not diverge. This does not guarantee completion of a process. However, it implies that the question of whether P blocks or makes progress does not depend on the order in which concurrent threads are scheduled. Either a process completes or it does not. All ssteps in a process can be scheduled with maximal parallelism without interference.
Theorem 2
(Termination). Let \(P_0, P_1, P_2, \ldots \) and \({\varSigma } _0, {\varSigma } _1, {\varSigma } _2, \ldots \) be infinite sequences of processes and memories, respectively, with Open image in new window . If \(P_0\) is clockguarded then there is \(n \ge 0\) with \({\varSigma } _n = {\varSigma } _i\), \(P_{n} = P_i\) for all \(i \ge n\).
The fixed point semantics will iterate (3) until it reaches a \(P^*\) such that Open image in new window . By Termination Theorem 2 this must exist for clockguarded processes. If \( can ^s(P^*) = \bot _0\) then \(P^*\) is 0stable and the program P has terminated. If \( can ^s(P^*) = \bot _1\), the residual \(P^*\) is pausing.
Definition 6
Given a pausing macrostep Open image in new window , then the next tick starts with process \(\sigma (P')\) in memory \({\varSigma } ''\) such that Open image in new window for all \({\texttt {c}} \in \textsf {O}\). This only constrains the abstract policy state of each variable in \({\varSigma } ''\) not their memory content. In this way, csm variables can introduce an arbitrary new memory \({\varSigma } ''\) with every clock tick.
Theorem 3
(Macrostep Determinism). If all csm variables are policycoherent then for two macro steps Open image in new window and Open image in new window we have \({\varSigma } _1 = {\varSigma } _2\) and \(P_1 = P_2\).
Definition 7
(Constructiveness). A program P is policyconstructive, for a set of policy coherent csm variables, if for arbitrary initial memory \({\varSigma } \) all reachable macrosteps of P are stabilising. \(\square \)
A nonconstructive program will, after some tick, end up in a fixed point \(P^*\) with \( can ^s(P^*) \not \in \{ \bot _0, \bot _1 \}\). Then \(P^*\) is stuck involving a set of active child threads waiting for each other in a policyinduced cycle.
Finally, we present two important results for DCoL showing that we are conservatively extending existing SP semantics. A DCoL program using only sequentially constructive variables [14] (see [17] Sec. 5.7]) is called a DCoLSC program. DCoL programs using only pure signals subject to the policy of Example 1 (Fig. 1) are expressive complete for the pure instantaneous fragment of Esterel [4]. Esterel signal emissions \(\mathop {\mathtt {emit}} \, {\texttt {s}} \) are syntactic sugar for \({\texttt {s}}.\mathop {\mathtt {emit}} () {\mathop {{\texttt {;}}}}\). A presence test \(\mathop {\mathtt {pres}} \, {\texttt {s}} \, {{\texttt {then}}} \, P\, {{\texttt {else}}} \, Q\) abbreviates \(\mathop {\mathtt {{if}}}\, {\texttt {s}}.\mathop {\mathtt {pres}} () \, \mathop {\mathtt {then}}\, P\, \mathop {\mathtt {else}}\, Q \). Sequential composition \(P \mathop {{\texttt {;}}} Q\) in Esterel behaves like a parallel composition in which the schedule is forced to run P to termination before it can pass control to Q. In DCoL this is Open image in new window with fresh signal \({\texttt {s}} '\) not occurring in either P or Q. This suggests the following definition: A program P is a (pure instantaneous) DCoLEsterel program if (i) P only uses pure signals and (ii) P does not use \(\mathop {\mathtt {pause}}\) or \(\mathop {\textsf {rec}} \) and (iii) P does not contain sequentially nested occurrences of signal accesses.
Theorem 4
It is interesting to note that the second statement in Theorem 4 is not invertible (for a counter example see [17]). Hence, policyconstructiveness for SCvariables induced by our semantics is more restrictive than that given in [14].
4 Related Work
Many languages have been proposed to offer determinism as a fundamental design principle. We consider these attempts under several categories.
Fixed Protocol for Shared Data. These approaches introduce an unique protocol for data exchange between concurrent processes. SHIM [21] provides a model for combined hardware software systems typically of embedded systems. Here, the concurrent processes communicate using pointtopoint (restricted) Kahn channels with blocking reads and writes. SHIM programs are shown to be deterministicbyconstruction as the states of each process are finite and deterministic and the data producedconsumed over any channel is also deterministic.
Concurrent revisions [19] introduce a generic and deterministic programming model for parallel programming. This model supports forkjoin parallelism and processes are allowed to make concurrent modifications to shared data by creating local copies that are eventually merged using suitable (programmer specified) merge functions at join boundaries.
However, like the deterministic SP model [2], both SHIM and concurrent revisions lack support for more expressive shared ADTs essential for programming complex systems. Caromel et al. [22], on the other hand, offer determinism with asynchronously communicating active objects (ADTs) equipped with a process calculus semantics. Here, an active object is a sequential thread. Active objects communicate using futures and synchronise via KahnMacQueen coroutines [23] for deterministic data exchange. Our approach subsumes Kahn buffers of SHIM and the localcopymerge protocol of concurrent revisions by an appropriate choice of method interface and policy. None of these approaches [19, 21, 22] uses a clock as a central barrier mechanism like our approach does.
In the Javaderived language X10, clocks are a form of synchronisation barrier for supporting deterministic and deadlockfree patterns of common parallel computations [24]. This allows multipleclocks in contrast to our approach. These, however, are not abstracted in the objects in contrast to our clocks that are encapsulated inside the csm types. Hence X10 clocks are invoked directly by the activities (i.e., concurrent threads) of programs and this manual synchronisation is as errorprone as other unsafe lowlevel primitives such as locks.
Coherent Memory Models for Shared Data. Whether clocked or not, our approach depends on the availability of csm types that are provably coherent for their policy. Besides the standard types of SP (dataflow, sequentially constructive variables, Kahn channels, signals) such csm types can be obtained from existing research on coherent memory models [25, 26]. Unlike the protocoloriented approaches above, some approaches have been developed based on coherency of the underlying memory models [26] especially for shared objects.
Bocchino et al. [25] propose deterministic parallel Java (DPJ) which has a type and effect system to ensure that parallel heap accesses remain safe. Data structures such as arrays, trees, and sets can be accessed in parallel as long as accesses can be shown to use nonoverlapping regions.
Grace [27] promises a deterministic runtime through the adoption of forkjoin parallelism combined with memory protection and a sequential commit protocol. However, there is no guarantee on the determinism of such custom synchronisation protocols. These must be verified using expensive proof systems.
A powerful technique to generate coherent shared memory structure for functional programs has recently been proposed by Kuper et al. [28]. They introduce latticebased data structures, called LVars, in which all write accesses produce a monotonic value increase in the lattice and all read accesses are blocked until the memory value has passed a readspecific threshold. Each variable’s domain is organised as a lattice of states with \(\bot \) and \(\top \) representing an empty new location and an error, respectively. Because of monotonicity all writes are confluent with each other. Since reads are blocked each LVar data type can thus be used in DCoL as a coherent csm type of variables with a thresholddetermined policy. Note that [25, 26, 27, 28] do not consider csm types and [28] also do not treat destructive sequential updates as we do.
Recently Haller et al. [29] have developed Reactive Async, a new eventbased asynchronous concurrent programming model that improves on LVars. This approach extends futures and promises^{8} with latticebased operations in order to support destructive updates (refinement of results) in a deterministic concurrent setting. The basic abstractions are: cells which define interfaces for reading a value that is asynchronously computed and (ii) cell completers that allow multiple monotonic updates of values taken from a lattice type class. The model supports concurrent programming with cyclic data dependencies in contrast to LVars. The mechanism for resolving cycles combines the lattices with quiescence detection on a handler pool (execution context). The quiescence concept refers to a state where the cell values are not going to be changed anymore. The thread pool is able to detect this quiescent (synchronisation) phase and when this is the case the resolution of cyclic dependencies and reading of cells can take place. This is similar to our policies, where enabling of methods (e. g., read) is a state and predictiondependent notion. Our developments may offer a theoretical background for the cell interfaces of this model. In Reactive Async the concurrent code is guaranteed to be deterministic provided that the API is used appropriately but this is not checked statically. It would be interesting to investigate whether our theory can contribute on this front. In the other direction, Reactive Async manages intercell dependencies which might support global policies between different csm variables in our setting.
ClockDriven Encapsulation. Encapsulation is not entirely unknown in reactive programming. The idea of reactive object model (ROM) [30] was first introduced by Boussinot et al. and subsequently refined [31] and combined with standards such as UML [32]. Here a program is a collection of reactive objects that operate synchronously relative to a global clock, similar to SP. Each object encapsulates a set of methods and data, where the methods share this data. ROM relied on a simplified assumption, where each method invocation is separated into instants.
André et al. [33] generalised the ROM idea to that of synchronous objects, which behave like synchronous modules (in Esterel or Lustre). The program is divided into a collection of synchronous and standard objects. While the latter interact using messages, the former use signals like in SP. Communication between standard and synchronous objects has to be managed using special interface objects. The framework supports features such as aggregation, encapsulation and inheritance yet communication is restricted to standard Esterelstyle signals. However, the issue of determinism for the composition of synchronous objects with standard objects is not considered.
A concrete implementation of synchronous objects in Java is proposed in [34]. Here, a runtime system is used to provide a cyclic schedule of the objects during an instant. This approach assumes that outputs from the objects can be read only in the next instant (similar to the SL programming language [35]) and so does not support instantaneous communication like we do.
Synchronous objects arise naturally in modular compilation [15, 36, 37]. The first time these have been exposed at the language level is in [20]. That work has inspired our use of policies. While [20] offers a mechanism for deterministic management of shared variables through ADTlike interfaces it has three serious limitations: (1) Modes express dataflow equations rather than imperative method procedures and so are not directly suitable for controlflow programming; (2) Policies do not distinguish between two modes being called sequentially by the same thread, which can be permitted, and two methods being called by different threads in parallel, which may have to be prohibited. This makes policies too restrictive in the light of the recent more liberal notion of sequential constructiveness [14] and, most importantly, (3) the notion of policysoundness does not use policies prescriptively as a contract to be fulfilled by the scheduler but instead only descriptively as an invariant of the program code. Hence, policies in [20] cannot be used to generalise the semantics of SP signals to shared ADTs.
The sequentially constructive model of synchronous computation [14] has shown how the constructive semantics of Esterel can be reconstructed from a scheduling view as standard destructive variables plus synchronisation protocol. SCL acts as an intermediate language for the graphical language SCCharts [38] and the textual language SCEst [18] which are proposed as sequentially constructive extensions of the wellknown controlflow languages SyncCharts [39] and Esterel [4]. By presenting our new analysis of sequential constructiveness for SCL our results become applicable both for SCCharts and SCEst.
The term ‘constructive’ semantics has been coined by Berry [4]. In [40] it was shown how it can be recoded as a fixedpoint in an interval domain which we generalise here to policy states \([\mu , \gamma ]\). Talpin et al. [13] recently gave a constructive semantics of multiclock synchronous programs. It is an open problem how our approach could be generalised to multiple clocks.
5 Conclusion
This work extends the SP theoretical foundations to allow communication at higher levels of abstraction. The paper explains deterministic concurrency of SP as a derived property from csm types. Our results extend the SPnotion of constructiveness to general shared csm types. We have made some simplifying assumptions that render the theory somewhat less general than it could be. A first limitation is our assumption that all method calls are atomic. We believe the theory can be generalised for nonatomic methods albeit at the price of a significant increase in the complexity of calculating \( can \) predictions. Second, method parameters are passed “by value” rather than “by reference”. This is necessary for having types as black boxes ready to use. Method parameters passing variables “by reference” would also introduce aliasing issues which we do not address. Third, in our present setting the policy update \(\mu \odot m\) does not observe method parameters. This is an abstraction to facilitate static analyses. In principle, to increase expressiveness, the method parameters could be included, too, but again complicate overapproximation for \( can \) information.
Footnotes
 1.
Milner’s distinction between determinacy and determinism is that a computation is determinate if the same input sequence produces the same output sequence, as opposed to deterministic computations which in addition have identical internal behaviour/scheduling. In this paper we use both terms synonymously to mean determinacy in Milner’s sense, i.e., observable determinism.
 2.
SCADE is a product of ANSYS Inc. (http://www.estereltechnologies.com/).
 3.
The signal policy in Fig. 1 does not impose any admissibility restriction since methods \(\mathop {\mathtt {pres}}\) and \(\mathop {\mathtt {emit}}\) can be scheduled from every policy state.
 4.
We tacitly assume that the tick transitions \(\sigma \) have the lowest priority since only when the reaction is over, the clock may tick. We could be more explicit and write \(\sigma \mathrel {:}\{\mathop {\mathtt {pres}},\mathop {\mathtt {emit}} \}\) as action labels for these transitions.
 5.
In Esterel V7 it is possible to use a module twice in a “sequential” composition \(x_1 = {{\texttt {nats}}}.{{\texttt {step}}} () ; x_2 = {{\texttt {nats}}}.{{\texttt {step}}} ()\). However, the two occurrences of nats are distinct instances with their own internal state. Both calls will thus return the same value.
 6.
We are more liberal than Esterel where \(\mathop {\mathtt {emit}} \) cannot be called sequentially after \(\mathop {\mathtt {pres}} \).
 7.
This is without loss of generality since \(\mathbb {D} \) may contain value tuples.
 8.
A future can asynchronously be completed with a value of the appropriate type or it can fail with an exception. A promise allows completing a future at most once.
Notes
Acknowledgement
We thank Philipp Haller, Adrien Guatto and the three anonymous reviewers for their insightful comments and suggestions helping us improving the paper. This work has been supported by the German Research Council (DFG) under grant number ME1427/62.
References
 1.Lee, E.: The problem with threads. Computer 39(5), 33–42 (2006)CrossRefGoogle Scholar
 2.Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Guernic, P.L., de Simone, R.: The synchronous languages twelve years later. Proc. IEEE 91(1), 64–83 (2003)CrossRefGoogle Scholar
 3.Colaço, J., Pagano, B., Pouzet, M.: SCADE 6: a formal language for embedded critical software development. In: TASE 2017, Sophia Antipolis, France, September 2017Google Scholar
 4.Berry, G.: The Constructive Semantics of Pure Esterel. Draft Book (1999)Google Scholar
 5.Schneider, K.: The synchronous programming language quartz. Internal report 375, Department of Computer Science, University of Kaiserslautern, Germany, December 2009Google Scholar
 6.von Hanxleden, R.: SyncCharts in C – a proposal for lightweight, deterministic concurrency. In: EMSOFT 2009, Grenoble, France, pp. 225–234, October 2009Google Scholar
 7.Guernic, P.L., Goutier, T., Borgne, M.L., Maire, C.L.: Programming real time applications with SIGNAL. Proc. IEEE 79, 1321–1336 (1991)CrossRefGoogle Scholar
 8.Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. Proc. IEEE 79(9), 1305–1320 (1991)CrossRefGoogle Scholar
 9.Pouzet, M.: Lucid Synchrone, un langage synchrone d’ordre supérieur. Mémoire d’habilitation, Université Paris 6, November 2002Google Scholar
 10.The Esterel v7 Reference Manual Version v7_30, November 2005Google Scholar
 11.Aguado, J., Mendler, M.: Constructive semantics for instantaneous reactions. Theor. Comput. Sci. 412, 931–961 (2011)MathSciNetCrossRefGoogle Scholar
 12.Aguado, J., Mendler, M., von Hanxleden, R., Fuhrmann, I.: Grounding synchronous deterministic concurrency in sequential programming. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 229–248. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642548338_13CrossRefzbMATHGoogle Scholar
 13.Talpin, J., Brandt, J., Gemünde, M., Schneider, K., Shukla, S.: Constructive polychronous systems. Sci. Comput. Prog. 96(3), 377–394 (2014)CrossRefGoogle Scholar
 14.von Hanxleden, R., Mendler, M., Aguado, J., Duderstadt, B., Fuhrmann, I., Motika, C., Mercer, S., O’Brien, O., Roop, P.: Sequentially constructive concurrency—a conservative extension of the synchronous model of computation. ACM TECS 13(4s), 144:1–144:26 (2014)Google Scholar
 15.Pouzet, M., Raymond, P.: Modular static scheduling of synchronous dataflow networks  an efficient symbolic representation. Des. Autom. Embed. Syst. 14(3), 165–192 (2010)CrossRefGoogle Scholar
 16.Kahn, G.: The semantics of simple language for parallel programming. In: IFIP Congress 1974, Stockholm, Sweden, pp. 471–475, August 1974Google Scholar
 17.Aguado, J., Mendler, M., Pouzet, M., Roop, P., von Hanxleden, R.: Clocksynchronised shared objects for deterministic concurrency. Research report 102, University of Bamberg, Germany, July 2017. https://www.unibamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/reportWIAI102Feb2018.pdf
 18.Rathlev, K., Smyth, S., Motika, C., von Hanxleden, R., Mendler, M.: SCEst: sequentially constructive esterel. ACM TECS 17(2), 33:1–33:26 (2018)Google Scholar
 19.Burckhardt, S., Leijen, D., Fähndrich, M., Sagiv, M.: Eventually consistent transactions. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 67–86. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642288692_4CrossRefGoogle Scholar
 20.Caspi, P., Cola\(\tilde{{\rm c}}\)o, J., Gérard, L., Pouzet, M., Raymond, P.: Synchronous objects with scheduling policies: introducing safe shared memory in lustre. In: LCTES 2009, Dublin, Ireland, pp. 11–20, June 2009Google Scholar
 21.Vasudevan, N.: Efficient, deterministic and deadlockfree concurrency. Ph.D. thesis, Department of Computer Science, Columbia University, March 2011Google Scholar
 22.Caromel, D., Henrio, L., Serpette, B.: Asynchronous and deterministic objects. In: POPL 2004, Venice, Italy, pp. 123–134, January 2004CrossRefGoogle Scholar
 23.Kahn, G., MacQueen, D.: Coroutines and networks of parallel processes. In: IFIP Congress 1977, Toronto, Canada, pp. 993–998, August 1977Google Scholar
 24.Charles, P., Grothoff, C., Saraswat, V., Donawa, C., Kielstra, A., Ebcioglu, K., von Praun, C., Sarkar, V.: X10: an objectoriented approach to nonuniform cluster computing. In: OOPSLA 2005, San Diego, USA, pp. 519–538, October 2005Google Scholar
 25.Bocchino, R., Adve, V., Dig, D., Adve, S., Heumann, S., Komuravelli, R., Overbey, J., Simmons, P., Sung, H., Vakilian, M.: A type and effect system for deterministic parallel Java. In: OOPSLA 2009, Orlando, USA, pp. 97–116, October 2009Google Scholar
 26.Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI 2003, San Diego, USA, pp. 338–349, June 2003Google Scholar
 27.Berger, E., Yang, T., Liu, T., Novark, G.: Grace: safe multithreaded programming for C/C++. In: OOPSLA 2009, Orlando, USA, pp. 81–96, October 2009CrossRefGoogle Scholar
 28.Kuper, L., Turon, A., Krishnaswami, N., Newton, R.: Freeze after writing: quasideterministic parallel programming with LVars. In: POPL 2014, San Diego, USA, pp. 257–270, January 2014Google Scholar
 29.Haller, P., Geries, S., Eichberg, M., Salvaneschi, G.: Reactive Async: expressive deterministic concurrency. In: SCALA 2016, Amsterdam, Netherlands, pp. 11–20, October 2016Google Scholar
 30.Boussinot, F., Doumenc, G., Stefani, J.: Reactive objects. Annales des télécommunications 51(9–10), 459–473 (1996)Google Scholar
 31.Talpin, J., Benveniste, A., Caillaud, B., Jard, C., Bouziane, Z., Canon, H.: BDL, a language of distributed reactive objects. In: IEEE ISORC 1998, Kyoto, Japan, pp. 196–205, April 1998Google Scholar
 32.André, C., PeraldiFrati, M.A., Rigault, J.P.: Integrating the synchronous paradigm into UML: application to controldominated systems. In: Jézéquel, J.M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 163–178. Springer, Heidelberg (2002). https://doi.org/10.1007/354045800X_15CrossRefzbMATHGoogle Scholar
 33.André, C., Boulanger, F., Péraldi, M., Rigault, J., VidalNaquet, G.: Objects and synchronous programming. RAIROAPIIJESAJ. Eur. Syst. Autom. 31(3), 417–432 (1997)Google Scholar
 34.Passerone, C., Sansoe, C., Lavagno, L., McGeer, R., Martin, J., Passerone, R., SangiovanniVincentelli, A.: Modeling reactive systems in Java. ACM TODAES 3(4), 515–523 (1998)CrossRefGoogle Scholar
 35.Boussinot, F., Simone, R.D.: The SL synchronous language. IEEE TSE 22(4), 256–266 (1996)Google Scholar
 36.Biernacki, D., Colaço, J., Hamon, G., Pouzet, M.: Clockdirected modular code generation of synchronous dataflow languages. In: LCTES 2008, Tucson, USA, pp. 121–130, June 2008Google Scholar
 37.Hainque, O., Pautet, L., Le Biannic, Y., Nassor, É.: Cronos: a separate compilation tool set for modular Esterel applications. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1836–1853. Springer, Heidelberg (1999). https://doi.org/10.1007/3540481184_47CrossRefGoogle Scholar
 38.von Hanxleden, R., Duderstadt, B., Motika, C., Smyth, S., Mendler, M., Aguado, J., Mercer, S., O’Brien, O.: SCCharts: sequentially constructive statecharts for safetycritical applications. SIGPLAN Not. 49(6), 372–383 (2014)CrossRefGoogle Scholar
 39.André, C.: Semantics of SyncCharts. Technical report ISRN I3S/RR200324FR, I3S Laboratory, SophiaAntipolis, France, April 2003Google Scholar
 40.Aguado, J., Mendler, M., von Hanxleden, R., Fuhrmann, I.: Denotational fixedpoint semantics for constructive scheduling of synchronous concurrency. Acta Informatica 52(4), 393–442 (2015)MathSciNetCrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.