Joaquín Aguado

Michael Mendler

Marc Pouzet

Partha Roop

Reinhard Von Hanxleden

Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach

Keywords: synchronous programming, data abstraction, clock-synchronised shared memory, determinacy, concurrency, constructive semantics

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 clock-synchronised shared memory (csm) data types, such as data-flow 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 policy-coherent, 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 policy-constructive system, all access methods can be scheduled in a policy-conformant way for all the types without deadlocking. In this paper, we show that a policy-constructive program exhibits deterministic concurrency in the sense that all policyconformant interleavings produce the same input-output behaviour. Policies are conservative and support the csm types existing in current SP languages. Technically, we introduce a kernel SP language that uses arbitrary policy-driven csm types. A big-step fixed-point semantics for this language is developed for which we prove determinism and termination of constructive programs.

Introduction

Concurrent programming is challenging. Arbitrary interleavings of concurrent threads lead to non-determinism with data races imposing significant integrity and consistency issues [START_REF] Lee | The problem with Threads[END_REF]. 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 run-time 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 safety-critical systems for avionics, automotive, energy and nuclear industries. Right now SP-generated code is flying on the Airbus 380 in systems like flight control, cockpit display, flight warning, and anti-icing just to mention a few. The SP mathematical theory has been fundamental for implementing correct-by-construction program-derivation algorithms and establishing formal analysis, verification and testing techniques [START_REF] Benveniste | The Synchronous Languages Twelve Years Later[END_REF]. For SCADE2 , 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 DO-178B/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) [START_REF] Colaço | SCADE 6: A Formal Language for Embedded Critical Software Development[END_REF].

Synchronous Programming in a Nutshell. At the top level, we can imagine an SP system as a black-box 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 macro-step or (synchronous) instant, appears instantaneous (has zero-delay) to the environment. Since each system reaction takes exactly one clock tick, we describe the evolution of the system-environment interaction as a synchronous (lock-step) sequence of macro-steps. The SP theory guarantees that all externally observable interaction sequences derived from the macro-step reactions define a functional input-output relation.

The fact that the sequences of macro-steps take place in time and space (memory) has motivated two orthogonal developments of SP. The data-flow view regards input-output sequences as synchronous streams of data changing over time and studies the functional relationships between streams. Dually, the control-flow approach projects the information of the input-output 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 [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF], Quartz [START_REF] Schneider | The Synchronous Programming Language Quartz[END_REF] and SC [START_REF] Von Hanxleden | SyncCharts in C -A Proposal for Light-Weight, Deterministic Concurrency[END_REF] in the imperative control-flow style and languages like Signal [START_REF] Guernic | Programming real time applications with SIGNAL[END_REF], Lustre [START_REF] Halbwachs | The synchronous data-flow programming language LUSTRE[END_REF] and Lucid Synchrone [START_REF] Pouzet | Lucid Synchrone, un langage synchrone d'ordre supérieur[END_REF] that support the declarative data-flow view. There are even mixed control-data flow language such as Esterel V7 [START_REF]The Esterel v7 Reference Manual Version[END_REF] or SCADE [START_REF] Colaço | SCADE 6: A Formal Language for Embedded Critical Software Development[END_REF]. 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 white-box where inside we find (graphical or textual) code. In the SP domain, the program must be divided into fragments corresponding to the macro-step reactions that will be executed instantaneously at each tick. Declarative languages usually organise these macro-steps by means of (internally generated) activation clocks that prescribe the blocks (nodes) that are performed at each tick. Instead, imperative textual languages provide a pause statement for explicitly delimiting code execution within a synchronous instant. In either case, the Synchrony Hypothesis conveniently abstracts away all the, typically concurrent, low-level micro-steps needed to produce a system reaction. The SP theory explains how the micro-step accesses to shared memory must be controlled so as to ensure that all internal (white-box) behaviour eventually stabilises, completing a deterministic macrostep (black-box) response. For more details on SP, the reader is referred to [START_REF] Benveniste | The Synchronous Languages Twelve Years Later[END_REF].

State of the Art. Traditional imperative SP languages provide constructs to model control-dominated 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 macro-step 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 s can be explicitly emitted with the statement s. emit() which atomically sets its status to 1. We can read the status of s with the statement s. pres(), so the control-flow can branch depending on run-time signal statuses. Specifically, inside programs, if-then-else 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 emit, pres are scheduled matters for the final result. The usual SP rule for ensuring determinism is that the pres test must wait until the final signal status is decided. If all sig-nal accesses can be scheduled in this decide-then-read way then the program is constructive. All schedules that keep the decide-then-read order will produce the same input-output 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 must-can analysis [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF][START_REF] Aguado | Constructive Semantics for Instantaneous Reactions[END_REF][START_REF] Aguado | Grounding Synchronous Deterministic Concurrency in Sequential Programming[END_REF][START_REF] Talpin | Constructive polychronous systems[END_REF] 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 control-flow languages also support other restricted csm types such valued signals and arrays [START_REF]The Esterel v7 Reference Manual Version[END_REF] or sequentially constructive variables [START_REF] Von Hanxleden | SyncCharts in C -A Proposal for Light-Weight, Deterministic Concurrency[END_REF].

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 shared-memory communication to occur at higher levels of abstraction than currently supported. In particular, our approach subsumes both the notions of Berry-constructiveness [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF] for Esterel and sequential constructiveness for SCL [START_REF] Von Hanxleden | Sequentially Constructive Concurrency-A conservative extension of the synchronous model of computation[END_REF]. This is the first time that these SP communication principles are combined side-by-side in a single language. Moreover, our theory permits other predefined communication structures to coexist safely under the same uniform framework, such as data-flow variables [START_REF] Halbwachs | The synchronous data-flow programming language LUSTRE[END_REF], registers [START_REF] Pouzet | Modular static scheduling of synchronous data-flow networks -An efficient symbolic representation[END_REF], Kahn channels [START_REF] Kahn | The Semantics of Simple Language for Parallel Programming[END_REF], priority queues, arrays as well as other csm types currently unsupported in SP.

Synopsis and Overview. The core of our approach is presented in Sec. 2 where policies are introduced as a (constructive) synchronisation mechanism for arbitrary abstract data types (ADT). For instance, the policy of a pure signal is depicted in Fig. 1. It has two control states 0 and 1 corresponding to the two possible signal statuses. Transitions are decorated with method names pres, emit or with σ to indicate a clock tick. The policy tells us whether a given method or tick is admissible, i. e., if it can be scheduled from a particular state3 . 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 ∅ indicates no precedences. To improve visualisation, we highlight precedences by dotted (red) arrows tagged prec4 . The policy interface in Fig. 1 specifies the decide-thenread protocol of pure signals as follows. At any instant, if the signal status is 0 then the pres test can only be scheduled if there are no more potential emit statements that can still update the status to 1. This explains the precedence of the emit transition over the self loop with action label pres : {emit} from state 0. Conversely, transitions pres and emit from state 1 have no precedences, meaning that the pres and 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 σ transition go to the initial state 0 since at each tick the SP system enters a new macro-step where all pure signals get initialised to the 0 status.

Sec. 2 describes in detail the idea of a scheduling policy on general csm types. This leads to a type-level coherence property, which is a local form of determinism. Specifically, a csm type is policy-coherent if it satisfies the (policy) specification of admissibility and precedence of its access methods. The point is that a policy-coherent 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 (policy-coherent) in the first place permits techniques such as the must-can analysis to get constructive information about deterministic programs. We show how policy-coherence implies a global determinacy property called commutation. Now, in a policy-constructive program all access methods can be scheduled in a policy-conforming way for all the csm types without deadlocking. We also show that, for policy-coherent types, a policy-constructive program exhibits deterministic concurrency in the sense that all policy-conforming interleavings produce the same input-output 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 Sec. 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 Sec. 3 presents its policy-driven operational semantics for which determinacy and termination is proven. Sec. 3 also explains how this model generalises existing notions of constructiveness. We discuss related work in Sec. 4 and present our conclusions in Sec. 5.

A companion of this paper is the research report [START_REF] Aguado | Clock-Synchronised Shared Objects for Deterministic Concurrency[END_REF] which contains detailed proofs and additional examples of csm types.

Synchronous Policies

This section introduces a kernel synchronous Deterministic Concurrent Language (DCoL) for policy-conformant constructive scheduling which integrates policy-controlled csm types within a simple syntax. DCoL is used to discuss the behavioural (clock) abstraction limitations of current SP. Then policies are in-troduced as a mechanism for specifying the scheduling discipline for csm types which, in this form, can encapsulate arbitrary ADTs.

Syntax

The syntax of DCoL is given by the following operators: This syntax seems minimalistic compared to existing SP languages. For instance, it does not provide primitives for pre-emption, suspension or traps as in Quartz or Esterel. Recent work [START_REF] Rathlev | SCEst: sequentially constructive esterel[END_REF] 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 policy-controlled csm variables, DCoL is at least as expressive as SCL.

P ::= skip

Limited Abstraction in SP

The pertinent feature of standard SP languages is that they do not permit the programmer to express sequential execution order inside a tick, for destructive updates of signals. All such updates are considered concurrent and thus must either be combined or concern distinct signals. For instance, in languages such as Esterel V7 or Quartz, a parallel composition

(v = xs.read() ; ys. emit(v + 1)) | |(xs. emit(1) ; xs. emit(5)) (1)
of signal emissions is only constructive if a commutative and associative function is defined on the shared signal xs to combine the values assigned to it. But then, by the properties of this combination function, we get the same behaviour if we swap the assignments of values 1 and 5, or execute all in parallel as in [START_REF] Schneider | The Synchronous Programming Language Quartz[END_REF].

v = xs.read() | | ys. emit(v + 1) | | xs. emit(1) | | xs. emit
If what we intended with the second emission xs. emit( 5) in ( 1) was to override the first xs. emit(1) like in normal imperative programming so that the concurrent thread v = xs.read() ; ys. emit(v + 1) will read the updated value as v = 5? Then we need to introduce a pause statement to separate the emissions by a clock tick and delay the assignment to ys as in

(pause ; v = xs.read() ; ys. emit(v + 1)) | |(xs. emit (1)
; pause ; xs. emit( 5)).

This makes behavioural abstraction difficult. For instance, suppose nats is a synchronous reaction module, possibly composite and with its own internal clocking, which returns the stream of natural numbers. Every time its step function nats.step() is called it returns the next number and increments its internal state. If we want to pair up two successive numbers within one tick of an outer clock and emit them in a single signal ys we would write something like x 1 = nats.step() ; x 2 = nats.step() ; y. emit(x 1 , x 2 ) where x 1 , x 2 are threadlocal value variables. This over-clocking is impossible in traditional SP because there is no imperative sequential composition by virtue of which we can call the step function of the same module instance twice within a tick. Instead, the two calls nats.step() are considered concurrent and thus create non-determinacy in the value of y. 5 To avoid a compiler error we must separate the calls by a clock as in x 1 = nats.step() ; pause ; x 2 = nats.step() ; y. emit(x 1 , x 2 ) which breaks the intended clock abstraction.

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 decide-then-read signal protocol must be generalised, in particular, to distinguish between concurrent and sequential accesses to the shared data structure. A concurrent access x 1 = nats.step() | |

x 2 = nats.step() must give the same value for x 1 and x 2 , while a sequential access x 1 = nats.step() ; x 2 = nats.step() must yield successive values of the stream. In a sequence x = xs.read() ; xs. emit(v) the x does not see the value v but in a parallel x = xs.read() | | xs. emit(v) 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 Sec. 2.6.

Concurrent Access Policies

In the white-box 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 : 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 : L, a silent action τ : L or a clock tick σ : L. A transition m : 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 τ : L internalises method calls by the tuc's concurrent environment which are uncontrollable for the tuc. In the sequel, the actions in M c ∪ {σ} will be called observable. A transition σ : 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 τ -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. A concurrent access policy ( cap) c of a csm variable c with (access) methods M c is a state machine consisting of a set of control states P c , an initial state ε ∈ P c and a labelled transition relation

→ ⊆ P c × A c × P c with action labels A c = (M c ∪ {τ, σ}) × 2 Mc . Instead of (µ 1 , (a, L), µ 2 ) ∈ → we write µ 1 -a:L→ µ 2 .
We then say action a is admissible in state µ 1 and blocked by all methods m ∈ L ⊆ M c . When the blocking set L is irrelevant we drop it and write µ 1 -a→ µ 2 . A cap must satisfy the following conditions:

-Determinacy. If µ -a:L 1 → µ 1 and µ -a:L 2 → µ 2 then L 1 = L 2 and µ 1 = µ 2 provided a is observable, i. e., a = τ . -Confluence. If µ -m 1 :L 1 → µ 1 and µ -m 2 :L 2 → µ 2 do not block each other, i. e., m 1 ∈ M c \ L 2 and m 2 ∈ M c \ L 1 , then for some µ both µ 1 -m 2 → µ and µ 2 -m 1 → µ . -Maximal Progress. µ -a:L 1 → µ 1 and µ -σ:L 2 → µ 2 imply a is observable and a ∈ L 2 ∪ {σ}.
A policy is a cap without any (concurrent) τ activity, i. e., every µ -a→ µ implies that a is observable.

The use of a cap as a concurrent policy arises from the notion of enabling. Informally, an observable action a ∈ M c ∪ {σ} is enabled in a state µ of a cap if it is admissible in µ and in all subsequent states reachable under arbitrary silent steps not blocked by a. To formalise this we define weak transitions µ 1 =L⇒ µ 2 inductively to express that either µ 1 = µ 2 and L = ∅ or µ 1 =L 1 ⇒ µ and µ -τ :L 2 → µ 2 and L = L 1 ∪ L 2 . We exploit the determinacy for observable actions a ∈ M c ∪ {σ} and write µ a for the unique µ such that µ -a→ µ , if it exists. Example 1. Consider the policy s in Fig. 1 of an Esterel pure signal s. An edge labelled a:L from state µ 1 to µ 2 corresponds to a transition µ 1 -a:L→ µ 2 in s . The start state is ε = 0 and the methods M s = {pres, emit} are always admissible, i. e., µ m is defined in each state µ for all methods m. The presence test does not change the state and any emission sets it to 1, i. e., µ pres = µ and µ emit = 1 for all µ ∈ P s . Each signal status is reset to 0 with the clock tick, i. e., µ σ = 0. Clearly, s satisfies Determinacy. A presence test on a signal that is not emitted yet has to wait for all pending concurrent emissions, that is emit blocks pres in state 0, i. e., 0 -pres :{emit}→ 0. Otherwise, no transition is blocked. Also, all competing transitions µ -m 1 :L 1 → µ 1 and µ -m 2 :L 2 → µ 2 that do not block each other, are of the form µ 1 = µ 2 , from which Confluence follows. As the clock transitions σ are implicitly blocked by all methods and since there are no silent transitions, Maximal Progress is always fulfilled too. Moreover, an action sequence is enabled in a state µ (Def. 2) iff it corresponds to a path in the automaton starting from µ. Hence, for m ∈ M * s we have 0 s ↓ m iff m is in the regular language6 pres * + pres * emit(pres + emit) * and 1 s ↓ m for all m ∈ M * s .

Contrast s with the policy c of a synchronous immutable variable (IVar) c shown in Fig. 2 with methods M c = {get, 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, µ c ↓ put iff µ = 0, where 0 is the initial empty state and µ c ↓ get iff µ = 1, where 1 is the filled state. The transition 0 -put:{put}→ 1 switches to filled state where get is admissible but put is not, anymore. The blocking {put} means there cannot be other concurrent threads writing c at the same time.

Enabling and Policy Conformance

A policy describes what a single thread can do to a csm variable c when it operates alone. In a cap all potential activities of the environment are added as τtransitions to block the tuc's accesses. To implement this τ -locking we define an operation that generates a cap [µ, γ] out of a policy. In this construction, µ ∈ P c is a policy state recording the history of methods that have been performed on c so far (must information). The second component γ ⊆ M * c is a prediction for the sequences of methods that can still potentially be executed by the concurrent environment (can information). Definition 3. Let (P c , ε, →) be a policy. We define a cap c where states are pairs [µ, γ] such that µ ∈ P c is a policy state and γ ⊆ M * c is a prediction. The initial state is [ε, M * c ] and the transitions are as follows:

1. The observable transitions [µ 1 , γ 1 ] -m:L→ [µ 2 , γ 2 ] are such that γ 1 = γ 2 and µ 1 -m:L→ µ 2 provided that for all sequences n n ∈ γ 1 with µ 1 -n→ µ we have n ∈ L.

The silent transitions are

[µ 1 , γ 1 ] -τ :L→ [µ 2 , γ 2 ] such that ∅ = m γ 2 ⊆ γ 1 and µ 1 -m:L→ µ 2 . 3. The clock transitions are [µ 1 , γ 1 ] -σ:L→ [µ 2 , γ 2 ] such that γ 1 = ∅ and µ 1 -σ:L→ µ 2 .
Silent steps arise from the concurrent environment: A step [µ 1 , γ 1 ] -τ :L→ [µ 2 , γ 2 ] removes some prefix method m from the environment prediction γ 1 , which contracts to an updated suffix prediction γ 2 with m γ 2 ⊆ γ 1 . This method m is executed on the csm variable, changing the policy state to

µ 2 = µ 1 m. A method m is enabled, [µ, γ] c ↓ m, if for all [µ 1 , γ 1 ] which are τ -reachable from [µ, γ] and not blocked by a, method m is admissible, i. e., [µ 1 , γ 1 ] -m→ [µ 2 , γ 1 ] for some µ 2 .
Example 2. Consider concurrent threads P 1 | | P 2 , where P 2 = zs.put(5) ; u = ys.get() and P 1 = v = zs.get() ; ys.put(v + 1) with IVars zs, ys according to Ex. 1. Under the IVar policy the execution is deterministic, so that first P 2 writes on zs, then P 1 reads from zs and writes to ys, whereupon finally P 1 reads ys. Suppose the variables have reached policy states µ zs and µ ys and the threads are ready to execute the residual programs P i waiting at some method call c i .m i (v i ), respectively. Since thread P i is concurrent with the other P 3-i , it can only proceed if m i is not blocked by P 3-i , i. e., if [µ ci , can ci (P 3-i )] ci ↓ m i , where can c (P ) ⊆ M * c is the set of method sequences predicted for P on c. Initially we have µ zs = 0 = µ ys . Since method get is not admissible in state 0, we get [0, can zs (P 2 )] zs ↓ get by Def. 3 and Def. 2. So, P 1 is blocked. The zs.put of P 2 , however, can proceed. First, since no predicted method sequence can zs (P 1 ) = {get} of P 1 starts with put, the transition 0 -put:{put}→ 1 implies that [0, can zs (P 1 )] -put:{put}→ [1, can zs (P 1 )] by Def. 3 [START_REF] Lee | The problem with Threads[END_REF]. Moreover, since get of P 1 is not admissible in 0, there are no silent transitions out of [0, can zs (P 1 )] according to Def. 3 [START_REF] Benveniste | The Synchronous Languages Twelve Years Later[END_REF]. Thus, [0, can zs (P 1 )] zs ↓ put, as claimed.

When the zs.put is executed by P 2 it turns into P 2 = u = ys.get() and the policy state for zs advances to µ zs = 1, while ys is still at µ ys = 0. Now ys.get of P 2 blocks for the same reason as zs was blocked in P 1 before. But since P 2 has advanced, its prediction on zs reduces to can zs (P 2 ) = ∅. Therefore, the transition 1 -get:∅→ 1 implies [1, can zs (P 2 )] -get:∅→ [1, can zs (P 2 )] by Def. 3(1). Also, there are no silent transitions out of [1, can zs (P 2 )] by Def. 3(2) and so [µ zs , can zs (P 2 )] zs ↓ get by Def. 2. This permits P 1 to execute zs.get() and proceed to P 1 = ys.put(5+1). The policy state of zs is not changed by this, neither is the state of ys, whence P 2 is still blocked. Yet, we have [µ ys , can zs (P 2 )] ys ↓ put which lets P 1 complete ys.put. It reaches P 1 with can ys (P 1 ) = ∅ and changes the policy state of ys to µ ys = 1. At this point, [µ ys , can zs (P 1 )] ys ↓ get which means P 2 unblocks to execute ys.get. Our operational semantics will only let a tuc execute a sequence m provided [µ, γ] c ↓ m, where µ is the current policy state of c and γ the predicted activity in the tuc's concurrent environment. Symmetrically, the environment will execute any n ∈ γ only if it is enabled with respect to m, i. e., if [µ, {m}] ↓ n. This means µ c m n. Policy coherence (Def. 5 below) then implies that every interleaving of the sequences m and any n ∈ γ leads to the same return values and final variable state (Prop. 1).

Coherence and Determinacy

A method call m(v) combines a method m ∈ M c with a method parameter7 v ∈ D, where D is a universal domain for method arguments and return values, including the special don't care value ∈ D. We denote by For policy-based scheduling we assume an abstraction function mapping a memory state s ∈ S c into a policy state s # ∈ P c . Specifically, init # c = ε. 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 α) # = s # α # for all s ∈ S c and α ∈ A * Example 3. Esterel pure signals do not carry any data value, so their memory state coincides with the policy state, S s = P s = {0, 1} and s # = s. An emission emit does not return any value but sets the state of s to 1, i. e., s. emit( ) = ∈ D and s emit( ) = 1 ∈ S s . A present test returns the state, s. pres( ) = s, but does not modify it, s pres( ) = s. From the policy Fig. 1 we find that the concurrent enablings s # s a # b # according to Def. 4 are (i) a = b ∈ {pres( ), emit( )} for arbitrary s, or (ii) s = 1, a = emit( ) and b = pres( ). In each of these cases we verify s.a = (s b).a, s.b = (s a).b and s a b = s b a without difficulty. Note that 1 s emit pres since the order of execution is irrelevant if s = 1. On the other hand, 0 s emit pres because in state 0 both methods are not confluent. Specifically, 0. pres( ) = 0 = 1 = (0 emit( )). pres( ).

A c = {m(v) | m ∈ M c , v
A special case are linear precedence policies where µ c ↓ m for all m ∈ M c and µ c m → n is a linear ordering on M c , for all policy states µ. Then, for no state we have µ c m 1 m 2 , so there is no concurrency and thus no confluence requirement to satisfy at all. Coherence of 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., µ c m 1 m 2 for all policy states µ 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 [START_REF] Burckhardt | Eventually Consistent Transactions[END_REF]. 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 policy-conformant 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 un-scheduleable.

Whatever the policies, if the variables are coherent, then all policy-conformant 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 Proposition 1 (Commutation). Let all csm variables be policy-coherent and Σ a α for a memory Σ ∈ S, method call a ∈ V and sequences of method calls α ∈ V * . Then, Σ a α = Σ α a and Σ.a = (Σ α).a.

A = {c.m(v) | c ∈ O, m(v) ∈ A c }. For a given sequence α ∈ A * let π c (α) ∈ A * c be the projection of α on c, formally π c (ε) = ε, π c (c.m(v) α) = m(v) π c (α)

Policies and Modularity

Consider the synchronous data-flow 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 ys a stream of consecutive integers, incremented with each clock tick. The wires ys, zs and ws are IVars (see Ex. 2) carrying a single integer value per tick. The input xs is a pure Esterel signal (see Ex. 1). The counter state is stored by reg in a local variable xv with read and 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 ys is stored. The inc takes the value at zs and increments it. When the signal xs is absent, mux passes the incremented value on ws to ys for the next tick. Otherwise, if xs is present then mux resets ys.

The evaluation order is implemented by the policies of the IVars ys, zs and ws. In each case the put method takes precedence over get which makes sure that the latter is blocked until the former has been executed. The causality cycle of the feedback loop is broken by the fact that the reg node first sends the current counter value to zs before it waits for the new value at ys. The other nodes mux and inc, in contrast, first read their inputs and then send to their output. Now suppose, for modularity, the reg node is pre-compiled into a synchronous IO automaton to be used by mux and inc as black box component. Then, reg must be split into three modes [START_REF] Caspi | Synchronous Objects with Scheduling Policies: Introducing Safe Shared Memory in Lustre[END_REF] reg.init, reg.get and reg.set that can be called independently in each instant. The init mode initialises the register memory with 0. The get mode extracts the buffered value and 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 reg.get is executed to place the output on zs. Then, reg waits for mux to produce the next value of ys from xs or ws. Finally, reg.set is executed to store the current value of 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 P reg = {0, 1} with initial ε = 0 and admissibility such that 0 reg ↓ m iff m = init and 1 reg ↓ m for all m. The transitions are 0 init = 1 and 1 m = 1 for all m ∈ M 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 reg m → set for all m ∈ {get, set}. Fig. 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 Ex. 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 reg.set, reg.get) in the same module are coupled via common shared memory (here the local variable xs) while mode calls in distinct modules are isolated from each other [START_REF] Pouzet | Modular static scheduling of synchronous data-flow networks -An efficient symbolic representation[END_REF][START_REF] Caspi | Synchronous Objects with Scheduling Policies: Introducing Safe Shared Memory in Lustre[END_REF].

Constructive Semantics of DCoL

To formalise our semantics it is technically expedient to keep track of the completion status of each active thread inside the program expression. This results in a syntax for processes distinguished from programs in that each parallel composition P 1 k1 | | k2 P 2 is labelled by completion codes k i ∈ {⊥, 0, 1} which indicate whether each thread is waiting k i = ⊥, terminated 0 or pausing k i = 1. Since we remove a process from the parallel as soon as it terminates then the code k i = 0 cannot occur. An expression P 1 | | P 2 is considered a special case of a process with k i = ⊥. The formal semantics is given by a reduction relation on processes

Σ; Π P m = ⇒ Σ k P (2)
specified by the inductive rules in Fig. 4 and Fig. 5. The relation (2) determines an instantaneous sequential reduction step of process P , called an sstep, that follows a sequence of enabled method calls m ∈ M * in sequential program order in P . This does not include any context switches between concurrent threads inside P . For thread communication, several ssteps must be chained up, as described later. The sstep (2) results in an updated memory Σ and residual process P . The subscript k is a completion code, described below. The reduction (2) is performed in a context consisting of a global memory Σ ∈ S (must context) containing the current state of all csm variables and an environment prediction Π ⊆ M * (can context). The prediction records all potentially outstanding methods sequences from threads running concurrently with P . We write π c (m) ∈ M * c for the projection of a method sequence m ∈ M * to variable c and write π c (Π) for its lifting to sets of sequences. Prefixing is lifted, too, i. e., c.m

Π = {c.m m | m ∈ Π} for any c.m ∈ M. Performing a method call c.m(v) in Σ; Π advances the must context to Σ c.m(v) but leaves Π unchanged. The sequence of methods m ∈ M * in (2) is enabled in Σ; Π, written [Σ, Π] ↓ m meaning that [(Σ.c) # , π c (Π)] c ↓ π c (m)
for all c ∈ O. In this way, the context [Σ, Π] forms a joint policy state for all variables for the tuc P , in the sense of Sec. 2 (Def. 3).

Most of the rules in Figs. 4 and5 should be straightforward for the reader familiar with structural operational semantics. Seq 1 is the case of a sequential P ; where P pauses or waits (k = 0) and Seq 2 is where P terminates and control passes into Q. The statements skip and pause are handled by rules Cmp 1 and Cmp 2 . The rule Rec explains recursion rec p.P by syntactic unfolding of the recursion body P . All interaction with the memory takes place in the method calls let x = c.m(e) in P . Rule Let 1 is applicable when the method call is enabled, i. e., [Σ, Π] ↓ c.m. Since processes are closed, the argument expression e must evaluate, eval (e) = v, and we obtain the new memory Σ c.m(v) and return value Σ.c.m(v). The return value is substituted for the local (stack allocated) identifier x, giving the continuation process P {Σ.c.m(v)/x} which is run in the updated context Σ c.m(v); Π. The prediction Π remains the same. The second rule 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 Cnd 1 , Cnd 2 are canonical. More interesting are the rules Par 1 -Par 4 for parallel composition, which implement non-deterministic thread switching. It is here where we need to generate predictions and pass them between the threads to exercise the policy control.

Q Sequence Σ; Π P m = ⇒ Σ k P k = 0 Seq 1 Σ; Π P ; Q m = ⇒ Σ k P ; Q Σ; Π P m 1 = = ⇒ Σ 0 P Σ ; Π Q m 2 = = ⇒ Σ k Q Seq 2 Σ; Π P ; Q m 1 m 2 = === ⇒ Σ k Q Completion Cmp 1 Σ; Π skip ε = ⇒ Σ 0 skip Cmp 2 Σ; Π pause ε = ⇒ Σ 1 pause
The key operation is the computation of the can-prediction of a process P to obtain an over-approximation of the set of possible method sequences potentially executed by P . For compositionality we work with sequences can s (P ) ⊆ M * × {0, 1} stoppered with a completion code 0 if the sequence ends in termination or 1 if it ends in pausing. The symbols ⊥ 0 , ⊥ 1 and are the terminated, paused and fully unconstrained can contexts, respectively, with

⊥ 0 = {(ε, 0)}, ⊥ 1 = {(ε, 1)} and = M * × {0, 1}. The set can s (P ), defined in Fig 6, is extracted from the structure of P using prefixing c.m Π , choice Π 1 ⊕ Π 2 = Π 1 ∪ Π 2 , parallel Π 1 ⊗ Π 2 and sequential composition Π 1 • Π 2 . Sequential composition is obtained pairwise on stoppered sequences such that (m, 0)•(n, c) = (m n, c) and (m, 1)•(n, c) = (m, 1). As a consequence, ⊥ 0 •Π = Π and ⊥ 1 •Π = ⊥ 1 .
Parallel composition is pairwise free interleaving with synchronisation on completion codes. Specifically, a product (m, c) ⊗ (n, d) generates all interleavings of m Method Call and n with a completion that models a parallel composition that terminates iff both threads terminate and pauses if one pauses. Formally, (m, c)

[Σ, Π] ↓ c.m eval (e) = v Σ c.m(v); Π P {Σ.c.m(v)/x} m = ⇒ Σ k P Let1 Σ; Π let x = c.m(e) in P c.m m = === ⇒ Σ k P Let2 Σ; Π let x = c.m(e) in P ε = ⇒ Σ ⊥ let x = c.m(e) in P Conditional eval (e) = true Σ; Π P m = ⇒ Σ k P Cnd1 Σ; Π if e then P else Q m = ⇒ Σ k P eval (e) = false Σ; Π Q m = ⇒ Σ k Q Cnd2 Σ; Π if e then P else Q m = ⇒ Σ k Q Parallel Σ; Π ⊗ can(Q) P m = ⇒ Σ k P k = 0 Par1 Σ; Π P k | | k Q Q m = ⇒ Σ k k Q P k | | k Q Q Σ; Π ⊗ can(Q) P m = ⇒ Σ 0 P Par2 Σ; Π P k | | k Q Q m = ⇒ Σ k Q Q Σ; Π ⊗ can(P ) Q m = ⇒ Σ k Q k = 0 Par3 Σ; Π P k P | | k Q m = ⇒ Σ k P k P k P | | k Q Σ; Π ⊗ can(P ) Q m = ⇒ Σ 0 Q Σ; Π P k P | k Q m = ⇒ Σ k P P
⊗ (n, d) = {(c, max(c, d)) | c ∈ m ⊗ n}. Thus, Π P ⊗ Π Q = ⊥ 0 iff Π P = ⊥ 0 = Π Q and Π P ⊗ Π Q = ⊥ 1 if Π P = ⊥ 1 = Π Q , or Π P = ⊥ 0 and Π Q = ⊥ 1 , or Π P = ⊥ 1 and Π Q = ⊥ 0 .
From can s (P ) we obtain can(P ) ⊆ M * by dropping all stopper codes, i.e., can(P ) = {m | ∃d. (m, d) ∈ can s (P )}. The rule Par 1 exercises a parallel P k | | k Q Q by performing an sstep in P . This sstep is taken in the extended context Σ; Π ⊗ can(Q) in which the prediction of the sibling Q is added to the method prediction Π for the outer environment in which the parent P | | Q is running. In this way, Q can block method calls of P . When P finally yields as P with a non-terminating completion code, 0 = k ∈ {⊥, 1}, the parallel completes as stable. A process is stable if it is 0-stable or 1-stable. A process expression is wellif in each sub-expression P 1 k1 | | k2 P 2 of P the completion annotations are matching with the processes, i. e., if k i = ⊥ then P i is k i -stable. Stable processes are well-formed 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 σ(skip) = skip, σ(pause) = skip, σ(P 1 ; P 2 ) = σ(P 1 ) ; P 2 and σ(P [START_REF] Von Hanxleden | Sequentially Constructive Concurrency-A conservative extension of the synchronous model of computation[END_REF] (see [START_REF] Aguado | Clock-Synchronised Shared Objects for Deterministic Concurrency[END_REF][Sec. 5.7]) is called a DCoL-SC program. DCoL programs using only pure signals subject to the policy of Ex. 1 (Fig. 1) are expressive complete for the pure instantaneous fragment of Esterel [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF]. Esterel signal emissions emit s are syntactic sugar for s. emit();. A presence test pres s then P else Q abbreviates if s. pres() then P else Q. Sequential composition P ; 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 (P ;s . emit();) | | (s . pres() then Q else skip) with fresh signal s not occurring in either P or Q. This suggests the following definition: A program P is a (pure instantaneous) DCoL-Esterel program if (i) P only uses pure signals and (ii) P does not use pause or rec and (iii) P does not contain sequentially nested occurrences of signal accesses.

P k | | k Q Q with code k k Q . This operation is defined k 1 k 2 = 1 if k 1 = 1 = k 2 and k 1 k 2 = ⊥,
1 k1 | | k2 P 2 ) = σ(P 1 )| | σ(P 2 ).
Theorem 4 (Esterel and Sequential Constructiveness).

1. If an DCoL-Esterel program P is policy-constructive according to Def. 7 iff it is Berry-constructive in the sense of [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF]. 2. If a DCoL-SC program P is policy-constructive according to Def. 7 then it is sequentially constructive in the sense of [START_REF] Von Hanxleden | Sequentially Constructive Concurrency-A conservative extension of the synchronous model of computation[END_REF].

It is interesting to note that the second statement in Thm. 4 is not invertible (for a counter example see [START_REF] Aguado | Clock-Synchronised Shared Objects for Deterministic Concurrency[END_REF]). Hence, policy-constructiveness for SC-variables induced by our semantics is more restrictive than that given in [START_REF] Von Hanxleden | Sequentially Constructive Concurrency-A conservative extension of the synchronous model of computation[END_REF].

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 [START_REF] Vasudevan | Efficient, Deterministic and Deadlock-free Concurrency[END_REF] provides a model for combined hardware software systems typically of embedded systems. Here, the concurrent processes communicate using point-to-point (restricted) Kahn channels with blocking reads and writes. SHIM programs are shown to be deterministicby-construction as the states of each process are finite and deterministic and the data produced-consumed over any channel is also deterministic.

Concurrent revisions [START_REF] Burckhardt | Eventually Consistent Transactions[END_REF] introduce a generic and deterministic programming model for parallel programming. This model supports fork-join 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 [START_REF] Benveniste | The Synchronous Languages Twelve Years Later[END_REF], both SHIM and concurrent revisions lack support for more expressive shared ADTs essential for programming complex systems. Caromel et al. [START_REF] Caromel | Asynchronous and Deterministic Objects[END_REF], 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 Kahn-MacQueen co-routines [START_REF] Kahn | Coroutines and Networks of Parallel Processes[END_REF] for deterministic data exchange. Our approach subsumes Kahn buffers of SHIM and the local-copy-merge protocol of concurrent revisions by an appropriate choice of method interface and policy. None of these approaches [START_REF] Burckhardt | Eventually Consistent Transactions[END_REF][START_REF] Vasudevan | Efficient, Deterministic and Deadlock-free Concurrency[END_REF][START_REF] Caromel | Asynchronous and Deterministic Objects[END_REF] uses a clock as a central barrier mechanism like our approach does.

In the Java-derived language X10, clocks are a form of synchronisation barrier for supporting deterministic and deadlock-free patterns of common parallel computations [START_REF] Charles | X10: An Object-oriented Approach to Non-uniform Cluster Computing[END_REF]. This allows multiple-clocks 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 error-prone as other unsafe low-level 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 (data-flow, sequentially constructive variables, Kahn channels, signals) such csm types can be obtained from existing research on coherent memory models [START_REF] Bocchino | A type and effect system for deterministic parallel Java[END_REF][START_REF] Flanagan | A type and effect system for atomicity[END_REF]. Unlike the protocol-oriented approaches above, some approaches have been developed based on coherency of the underlying memory models [START_REF] Flanagan | A type and effect system for atomicity[END_REF] especially for shared objects.

Bocchino et al. [START_REF] Bocchino | A type and effect system for deterministic parallel Java[END_REF] 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 non-overlapping regions.

Grace [START_REF] Berger | Grace: Safe multithreaded programming for C/C++[END_REF] promises a deterministic run-time 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. [START_REF] Kuper | Freeze after writing: Quasideterministic parallel programming with LVars[END_REF]. They introduce lattice-based 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 read-specific threshold. Each variable's domain is organised as a lattice of states with ⊥ and 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 threshold-determined policy. Note that [START_REF] Bocchino | A type and effect system for deterministic parallel Java[END_REF][START_REF] Flanagan | A type and effect system for atomicity[END_REF][START_REF] Berger | Grace: Safe multithreaded programming for C/C++[END_REF][START_REF] Kuper | Freeze after writing: Quasideterministic parallel programming with LVars[END_REF] do not consider csm types and [START_REF] Kuper | Freeze after writing: Quasideterministic parallel programming with LVars[END_REF] also do not treat destructive sequential updates as we do.

Recently Haller et al. [START_REF] Haller | Reactive Async: Expressive deterministic concurrency[END_REF] have developed Reactive Async, a new event-based asynchronous concurrent programming model that improves on LVars. This approach extends futures and promises 8 with lattice-based 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 mul-tiple 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 prediction-dependent 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 inter-cell dependencies which might support global policies between different csm variables in our setting. Clock-driven encapsulation. Encapsulation is not entirely unknown in reactive programming. The idea of reactive object model (ROM) [START_REF] Boussinot | Reactive Objects[END_REF] was first introduced by Boussinot et al. and subsequently refined [START_REF] Talpin | BDL, a language of distributed reactive objects[END_REF] and combined with standards such as UML [START_REF] André | Integrating the Synchronous Paradigm into UML: Application to Control-Dominated Systems[END_REF]. 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. [START_REF] André | Objects and Synchronous Programming[END_REF] 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 Esterel-style 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 [START_REF] Passerone | Modeling reactive systems in Java[END_REF]. Here, a run-time 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 [START_REF] Boussinot | The SL synchronous language[END_REF]) and so does not support instantaneous communication like we do.

Synchronous objects arise naturally in modular compilation [START_REF] Pouzet | Modular static scheduling of synchronous data-flow networks -An efficient symbolic representation[END_REF][START_REF] Biernacki | Clock-directed Modular Code Generation of Synchronous Data-flow Languages[END_REF][START_REF] Hainque | Cronos: A Separate Compilation Toolset for Modular Esterel Applications[END_REF]. The first time these have been exposed at the language level is in [START_REF] Caspi | Synchronous Objects with Scheduling Policies: Introducing Safe Shared Memory in Lustre[END_REF]. That work has inspired our use of policies. While [START_REF] Caspi | Synchronous Objects with Scheduling Policies: Introducing Safe Shared Memory in Lustre[END_REF] offers a mechanism for deterministic management of shared variables through ADT-like interfaces it has three serious limitations: (1) Modes express data-flow equations rather than imperative method procedures and so are not directly suitable for control-flow 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 [START_REF] Von Hanxleden | Sequentially Constructive Concurrency-A conservative extension of the synchronous model of computation[END_REF] and, most importantly, (3) the notion of policy-soundness 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 [START_REF] Caspi | Synchronous Objects with Scheduling Policies: Introducing Safe Shared Memory in Lustre[END_REF] cannot be used to generalise the semantics of SP signals to shared ADTs.

The sequentially constructive model of synchronous computation [START_REF] Von Hanxleden | Sequentially Constructive Concurrency-A conservative extension of the synchronous model of computation[END_REF] 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 [START_REF] Von Hanxleden | SCCharts: Sequentially Constructive Statecharts for safety-critical applications[END_REF] and the textual language SCEst [START_REF] Rathlev | SCEst: sequentially constructive esterel[END_REF] which are proposed as sequentially constructive extensions of the well-known control-flow languages SyncCharts [START_REF] André | Semantics of SyncCharts[END_REF] and Esterel [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF]. 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 [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF]. In [START_REF] Aguado | Denotational fixedpoint semantics for constructive scheduling of synchronous concurrency[END_REF] it was shown how it can be recoded as a fixed-point in an interval domain which we generalise here to policy states [µ, γ]. Talpin et al. [START_REF] Talpin | Constructive polychronous systems[END_REF] recently gave a constructive semantics of multi-clock synchronous programs. It is an open problem how our approach could be generalised to multiple clocks.

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 SP-notion 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 non-atomic 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 µ 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 over-approximation for can information.

Fig. 1 :

 1 Fig. 1: Pure Signal Policy.

Definition 2 .Fig. 2 :

 22 Fig. 2: Synchronous IVar.

Definition 4 .

 4 Let c be a policy for c. A method sequence m 1 blocks another m 2 in state µ, written µ c m 1 → m 2 , if µ c ↓ m 2 but [µ, {m 1 }] c ↓ m 2 . Two method sequences m 1 and m 2 are concurrently enabled, denoted µ c m 1 m 2 if µ c ↓ m 1 , µ c ↓ m 2 and both µ c m 1 → m 2 and µ c m 2 → m 1 .

∈

  D} the set of all method calls on object c. Sequences of method calls α ∈ A * c can be abstracted back into sequences of methods α # ∈ M * c by dropping the method parameters: ε # = ε and (m(v) α) # = m α # . Coherence concerns the semantics of method calls as state transformations. Let S c be the domain of memory states of the object c with initial state init c ∈ S c . Each method call m(v) ∈ A c corresponds to a semantical action [[m(v)]] c ∈ S c → (D × S c ). If s ∈ S c is the current state of the object then executing a call m(v) on c returns a pair (u, s ) = [[m(v)]] c (s) where the first projection u ∈ D is the return value from the call and the second projection s ∈ S c is the new updated state of the variable. For convenience, we will denote u = π 1 [[m(v)]] c (s) by u = s.m(v) and s = π 2 [[m(v)]] c (s) by s = s m(v). The action notation is extended to sequences of calls α ∈ A * c in the natural way: s ε = s and s (m(v) α) = (s m(v)) α.

  c . Definition 5 (Coherence). A csm variable c is policy-coherent if for all method calls a, b ∈ A c whenever s # c a # b # for a state s ∈ S c , then a and b are confluent in the sense that s.a = (s b).a, s.b = (s a).b and s a b = s b a.

  and π c (c .m(v) α) = π c (α) for c = c. A global memory Σ ∈ S = c∈O S c assigns a local memory Σ.c ∈ S c to each variable c. We write init for the initial memory that has init.c = init c and (init.c) # = ε ∈ P c . Given a global memory Σ ∈ S and sequences α, β ∈ A * of method calls, we extend the independence relation of Def. 4 variable-wise, defining Σ α β iff (Σ.c) # c (π c (α)) # (π c (β)) # . The application of a method call a ∈ A to a memory Σ ∈ S is written Σ.a ∈ S and defined (Σ.(c.m(v))).c = (Σ.c).m(v) and (Σ.(c.m(v))).c = Σ.c for c = c. Analogously, method actions are lifted to global memories, i. e., (Σ c.m(v)).c = Σ.c if c = c and (Σ c.m(v)).c = Σ.c m(v).

Fig. 3 :

 3 Fig. 3: Synchronous data-flow network cnt built from control-flow processes.

Fig. 4 :

 4 Fig. 4: SStep Reductions for Sequence, Completion and Recursion.

Fig. 5 :

 5 Fig. 5: SStep Reductions for Method Calls, Conditional and Parallel.

  otherwise. When P terminates its sstep with code k = 0 then we need rule Par 2 which removes child P from the parallel composition. The rules Par 3 , Par 4 are symmetrical to Par 1 , Par 2 . They run the right child Q of a parallel P k P | | k Q.Completion and Stability. A process P is 0-stable if P = skip and 1-stable if P = pause or P = P 1 ; P 2 and P 1 is 1-stable, or P = P 1 1 | | 1 P 2 , and P i are 1-can s (skip) = can s (p) = ⊥0 can s (pause) = ⊥1 can s (rec p. P ) = can s (P ) can s (P | | Q) = can s (P ) ⊗ can s (Q) can s (P ; Q) = can s (P ) if can s (P ) ⊆ M * × {1} can s (P ) • can s (Q) otherwise can s (let x = c.m(e) in P ) = c.m can s (P ) can s (if e then P else Q) s (P ) if eval (e) = true can s (Q)if eval (e) = false can s (P ) ⊕ can s (Q) otherwise.

Fig. 6 :

 6 Fig. 6: Computing the can Prediction.

Example 4 .

 4 The data-flow cnt-cmp from Fig. 3c can be represented as a DCoL process in the form C = reg.init(0); (M ⊥ | | ⊥ I) with sequentially constructive variables

  skip terminates instantaneously and pause waits for the logical clock to terminate. The operators P | |Q and P ; Q are parallel interleaving and imperative sequential composition of threads with the standard operational interpretation. Reading and destructive updating is performed through the execution of method calls c.m(e) on a csm variable c ∈ O with a method m ∈ M c . The sets O and M c define the granularity of the available memory accesses. The construct let x = c.m(e) in P calls m on c with an input parameter determined by value expression e. It binds the return value to variable x and then executes program P , which may depend on x, sequentially afterwards.

		instantaneous termination
	| pause	wait for next instant (clock tick)
	| P | | P	parallel composition
	| P ; P	sequential composition
	| let x = c.m(e) in P	access method call, x value variable
	| if e then P else P	conditional branching, e value expression
	| rec p. P	recursive closure
	| p	process variable
	The first two statements correspond to the two forms of immediate comple-
	tion: The execution of
	c.m(e) in general has the side-effect of changing the internal memory of c. In
	contrast, the evaluation of expression e is side-effect free. For convenience we
	write x = c.m(e);P for let x = c.m(e) in P . When P does not depend on x then
	we write c.m(e);P and c.m(e); for c.m(e); skip. The exact syntax of value
	expressions e is irrelevant for this work and left open. It could be as simple as
	permitting only constant value literals or a full-fledged functional language. The
	conditional if e then P else P has the usual interpretation. For simplicity, we
	may write if c.m(e) then P else Q to mean x = c.m(e); if x then P else Q.
	The recursive closure rec p. P binds the behaviour P to the program label p so
	it can be called from within P . Using this construct we can build iterative be-
	haviours. For instance, loop P end = df rec p. P ; pause ;p indefinitely repeats P
	in each tick. We assume that in a closure rec p. P the label p is (i) clock guarded,
	i. e., it occurs in the scope of at least one pause (meaning no instantaneous
	loops) and (ii) all occurrences of p are in the same thread. Thus, rec p. p is illegal
	because of (i) and rec p. (pause ;p | | pause ;p) is not permitted because of (ii).

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.esterel-technologies.com/)

The signal policy in Fig.1does not impose any admissibility restriction since methods pres and emit can be scheduled from every policy state.

[START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF] We tacitly assume that the tick transitions σ have the lowest priority since only when the reaction is over, the clock may tick. We could be more explicit and write σ : {pres, emit} as action labels for these transitions.

In Esterel V7 it is possible to use a module twice in a "sequential" composition x1 = nats.step(); x2 = nats.step(). However, the two occurrences of nats are distinct instances with their own internal state. Both calls will thus return the same value.

We are more liberal than Esterel where emit cannot be called sequentially after pres.

This is without loss of generality since D may contain value tuples.

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.

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 ME-1427/6-2.

M = df rec p. v = xs. pres(); P (v); pause; p P (v) = df if v then reg.set(0); else Q Q = df u = ws.get(); reg.set(u); I = df rec q. v = reg.get(); ws.put(v + 1); pause; q.

Let us evaluate process C from an initialised memory Σ 0 such that Σ 0 .xs = 0 = Σ 0 .ws, and empty environment prediction { }.

The first sstep is executed from the context Σ 0 ; { } with empty can prediction. Note that reg.init(0); (M ⊥ | | ⊥ I) abbreviates let = reg.init(0) in (M ⊥ | | ⊥ I). In context Σ 0 ; { } the method call reg.init(0) is enabled, i.e., [Σ 0 , { }] ↓ reg.init. Since eval (0) = 0, we can execute the first method call of C using rule Let 1 . This advances the memory to Σ 1 = Σ 0 reg.init(0). The continuation process M ⊥ | | ⊥ I is now executed in context Σ 1 ; ⊥ 0 . The left child M starts with method call xs. pres() and the right child I with reg.get(). The latter is admissible, since (Σ 1 .reg) # = 1. Moreover, get does not need to honour any precedences, whence it is enabled, [Σ 1 , Π] ↓ reg.get for any Π. On the other hand, xs. pres in M is enabled only if (Σ 1 .xs) # = 1 or if there is no concurrent emit predicted for xs. Indeed, this is the case: The concurrent context of M is

↓ xs. pres. Hence, we have a nondeterministic choice to take an sstep in M or in I. Let us use rule Par 1 /Par 2 to run M in context Σ; Π I . By loop unfolding Rec and rule Let 1 we execute the present test of M which returns the value Σ 1 .xs. pres() = false. This leads to an updated memory Σ 2 = Σ 1 xs. pres() = Σ 1 and continuation process P (false); pause; M . In this (right associated) sequential composition we first execute P (false) where the conditional rule Cnd 2 switches to the else branch Q which is u = ws.get(); reg.set(u);, still in the context Σ 2 , Π I . The reading of the data-flow variable ws, however, is not enabled, [Σ 2 , Π I ] ↓ ws.get, because (Σ 2 .ws) # = 0 and thus get not admissible. The sstep blocks with rule Let 2 :

where m 1 = reg.init and m 2 = xs. pres. In the next sstep, from Σ

set} we let the process I execute its reg.get() with rules Rec and Let 1 . The return value is v = Σ 2 .reg.get() = 0. Then, from the updated memory Σ 3 = Σ 2 reg.get() we run the continuation process ws.put(0 + 1); pause; I. The ws.put is enabled if the IVar is empty and there is no concurrent put on ws predicted from M . Both conditions hold since (Σ 3 .ws) # = (Σ.ws) # = 0 and π ws (Π

↓ ws.put. With the evaluation eval (0 + 1) = 1 the rule Let 1 permits us to update the memory as Σ 4 = Σ 3 ws.put(1) and continue with process pause; I which completes by pausing. Formally, this sstep is:

where m 3 = reg.get and m 4 = ws.put. In the next sstep the waiting method u = ws.get in Q is now admissible and can proceed, (Σ 4 .ws) # = ((Σ 3 ws.put(1)).ws) # = 1 and thus [Σ 4 , Π] ↓ ws.get for all Π. The return value is u = Σ 4 .ws.get() = 1, the updated memory Σ 5 = Σ 4 ws.put(1) and the continuation process reg.set [START_REF] Lee | The problem with Threads[END_REF]; pause; M . The register set method is admissible since (Σ 4 .reg) # = 1 and also enabled because there is no get predicted in the concurrent environment ⊥ 0 . Thus, [Σ 5 , ⊥ 0 ] ↓ reg.set. The execution of the method yields the memory Σ 6 = Σ 5 reg.set(1) with continuation process pause ; M which completes by pausing. This yields the derivation tree:

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 policy-enabled, then it remains policy-enabled under arbitrary ssteps of the environment. Symmetrically, the environment cannot be blocked by a thread taking policy-enabled computation steps.

The second building block for determinacy is csm variable coherence. Consider a context Σ; Π Q in which we run an sstep of P with prediction Π Q for concurrent process Q, resulting in a final memory Σ P arising from executing a sequence m P of method calls from P . Because of the policy constraint, the sequence m P must be enabled under all predictions n ∈ Π Q , i. e., [Σ, n] ↓ m P . Suppose, on the other side, we sstep the process Q in the same memory Σ with prediction Π P for P , resulting in an action sequence m Q and final memory Σ Q . Then, by the same reasoning, [Σ, n] ↓ m Q for all n ∈ Π P . But since m P is an actual execution of P it must be in the prediction for P , i. e., m P ∈ Π P and symmetrically, m Q ∈ Π Q . But then we have [Σ, m Q ] ↓ m P and [Σ, m P ] ↓ m P which means Σ m P 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 m P can still be executed by P in state Σ Q and m Q by Q in state Σ P , and both lead to the same final memory.

Theorem 1 (Diamond Property). If all csm variables are policy-coherent then the sstep semantics is confluent. Formally, given two derivations Σ; Π P m1 = = ⇒ Σ 1 k1 P 1 and Σ; Π P m2 = = ⇒ Σ 2 k2 P 2 , Then, there exist Σ , k and P such that

Thm. 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.

A main program P is run at the top level in an "environmentally closed" form of ssteps [START_REF] Benveniste | The Synchronous Languages Twelve Years Later[END_REF] where the prediction is empty Π = { } and thus acts neutrally. We iterate such ssteps to construct a macro-step reaction. Let us write

if there exists k , m such that Σ; ⊥ 0 P m = ⇒ Σ k P . The relation = ⇒ is wellfounded for clock-guarded processes in the sense that it has no infinite chains.

Theorem 2 (Termination). Let P 0 , P 1 , P 2 , . . . and Σ 0 , Σ 1 , Σ 2 , . . . be infinite sequences of processes and memories, respectively, with Σ i P i = ⇒ Σ i+1 P i+1 . If P 0 is clock-guarded then there is n ≥ 0 with Σ n = Σ i , P n = P i for all i ≥ n.

The fixed point semantics will iterate (3) until it reaches a P * such that Σ * P * = ⇒ Σ * P * . By Termination Thm. 2 this must exist for clock-guarded processes. If can s (P * ) = ⊥ 0 then P * is 0-stable and the program P has terminated. If can s (P * ) = ⊥ 1 , the residual P * is pausing.

Definition 6 (Macro Step).

A run Σ P ⇒ ⇒ Σ P is a sequence of ssteps with processes P 0 , P 1 , P 2 , . . . , P n and sequences of method calls m 1 , m 2 , . . . m n such that for all

where P 0 = P , Σ 0 = Σ, Σ n = Σ and P n = P . A run is called a macro-step if it is maximal, i. e., if Σ P = ⇒ Σ P implies Σ = Σ and P = P . The macro-step is called stabilising if the final P is stable, i. e., k n = ⊥ and the clock is admissible, i. e., if (Σ .c) # σ is defined for all c ∈ O. The macro-step is pausing if k n = 1 and terminating if k n = 0.

Given a pausing macro-step Σ P ⇒ ⇒ Σ P , then the next tick starts with process σ(P ) in memory Σ such that (π c (Σ )) # -σ→ (π c (Σ )) # for all c ∈ O. This only constrains the abstract policy state of each variable in Σ not their memory content. In this way, csm variables can introduce an arbitrary new memory Σ with every clock tick.

Theorem 3 (Macro-step Determinism). If all csm variables are policycoherent then for two macro steps Σ P ⇒ ⇒ Σ 1 P 1 and Σ P ⇒ ⇒ Σ 2 P 2 we have Σ 1 = Σ 2 and P 1 = P 2 .

Definition 7 (Constructiveness). A program P is policy-constructive, for a set of policy coherent csm variables, if for arbitrary initial memory Σ all reachable macro-steps of P are stabilising.

A non-constructive program will, after some tick, end up in a fixed point P * with can s (P * ) ∈ {⊥ 0 , ⊥ 1 }. Then P * is stuck involving a set of active child threads waiting for each other in a policy-induced cycle.

Finally, we present two important results for DCoL showing that we are conservatively extending existing SP semantics. A DCoL program using only