Determinacy with Priorities up to Clocks Luigi Liquori
Michael Mendler
Claude Stolze
Centre Inria de l’Université Côte d’Azur
University of Bamberg
University of Bamberg
In Milner’s seminal book on communication and concurrency introducing CCS, a process algebra inherently non-deterministic, chapter 11 was completely devoted to introduce the notion of determinacy and confluence in order to identify a subcalculus of CCS in which all definable agents are confluent. At the same time, or shortly later, determinate semantics were given for programming languages that reconcile concurrency and determinacy, such as Esterel by Berry and Gonthier, or SL by Boussinot and de Simone. These dedicated semantics do not easily map to Milner’s confluence theory for CCS, which is unable to express causality and shared memory multi-threading with reaction to absence in a compositional way. We present an extension of CCS with priority-guarded actions and clocks, and we exploit the added expressiveness to enrich Milner’s original notion of confluence by the new concept of coherence which permits us to encode, in a compositional fashion, synchronous programming languages such as Esterel.
1
Introduction
According to Milner [17], the notion of determinacy is tied up with predictability: “if we perform the same experiment twice on a determinate system – starting each time in its initial state – then we expect to get the same result, or behaviour, each time.” In λ-calculus, determinacy refers to the uniqueness of normal forms which is a result of the Church-Rosser Property. In concurrency, it corresponds to the absence of race-conditions, which are the source of many bugs in concurrent programming. In this paper α we adopt the setting and notation of Milner’s CCS, where we have action-labelled transitions P − →Q (which is either the strong or weak transition), compatible with a suitable congruence that preserves normal forms. Milner defines determinacy [17] (Def. 2 and Def. 3, Chap. 11.1) as the condition that any given action can only lead to congruent continuations. Definition 1. A process P is determinate (modulo ) if for all its derivatives Q and action α ∈ Lτ , if α α Q− → Q1 and Q − → Q2 then Q1 Q2 . The problem with determinacy, defined in this way, is that it is not closed under parallel composition. The solution proposed by Milner [17] (Chap. 11.3), is to strengthen determinacy to the notion of confluence which turns out to be closed for parallel composition under natural restrictions. Definition 2. P is confluent (modulo ) if it is determinate and for every derivative Q of P with transitions α1 α2 α2 α1 Q −−→ Q1 and Q −−→ Q2 such that α1 , α2 , there exist Q′1 Q′2 such that Q1 −−→ Q′1 and Q2 −−→ Q′2 . Definition 2 subsumes strong confluence [17] (Def. 4, Chap. 11.3) when the transitions are strong and is a bisimulation (∼), and weak confluence [17] (Def. 5, Chap. 11.3) for weak transitions and observation equivalence (≈). For instance, consider the process P = (R1 | S | R2 ) \ r with components R1 = r.a.0, S = r.S , and R2 = r.b.0. Process P is not strongly confluent since it is not determinate (i.e., modulo ∼): τ
τ
P→ − (a.0 | S | r.b.0) \ r and P → − (r.a.0 | S | b.0) \ r and (a.0 | S | r.b.0) \ r / (r.a.0 | S | b.0) \ r. However, all components R1 , S , and R2 of P are strongly confluent. Hence, like determinacy, strong confluence is not closed under parallel composition. On the other hand, P is weakly confluent (i.e., Lorenzo Gheri & Kirstin Peters (Eds.): 17th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software 2026 (PLACES 2026) EPTCS 444, 2026, pp. 79–89, doi:10.4204/EPTCS.444.8
© L. Liquori, M. Mendler, C. Stolze This work is licensed under the Creative Commons Attribution License.
80
Determinacy with Priorities up to Clocks
modulo ≈) and converges weakly to the normal form (a.0 | S | b.0) \ r. Milner [17] (Prop. 17, Chap 11.4) def shows that weak confluence is preserved by confluent composition P | L Q = (P | Q) \ L, combining the parallel and restriction operator, where L is a set of restricted labels, subject to the Separation Condition that L(P) ∩ L(Q) = {} and L(P) ∩ L(Q) = L ∪ L, where L(_) is the function calculating the sort of a process. The former condition says that P and Q operate on disjoint actions and the latter says that every possible communication between P and Q is restricted by L. This is a form of sort separation, ensuring that every action has at most one synchronisation partner either inside or outside of (P | Q) \ L. It may be the case that many practical examples of determinate systems can be understood as sortseparated compositions of confluent processes, for the right choice of coding scheme. For application to synchronous programming, however, stronger compositionality arguments are needed. For instance, replace the process S in our example by S = r.S + w.0 which models a simple write-once memory with read and write actions r and w, respectively. It permits multiple readers to synchronise on r, not changing its state, and a single writer on w, leading to termination. The process P = (R1 | S | R2 ) \ {r, w} is weakly confluent but falls outside of Milner’s confluence class: Firstly, it violates the Separation Condition and secondly the subprocess S is not confluent. Milner’s result [17] (Prop. 17, Chap. 11.4) does not help us to verify that shared memory multi-threading without data races, like P, is confluent. Memory processes that permit destructive update are firstly not confluent and, secondly, Milner’s confluent composition forbids direct multi-cast communication, because labels such as r in S could not be shared by two readers R1 , R2 due to sort-separation. This means that concurrent programming languages that support shared memory and yet have determinate reduction semantics, cannot be handled. In a working paper [14], we define CCSspt , a process algebra extending Milner’s CCS with clocks and priorities on actions up-to clocks. This process algebra is able to capture multi-clock synchronous processes in a compositional way, defining the scheduling of the processes through priorities. As any process algebra, CCSspt is nondeterministic, but deterministic programs, like e.g., Esterel’s ABRO [3] can be expressed in a compositionally elegant way. Starting from a fragment of CCSspt with priority-guarded actions and a single clock, we define a new notion, coherence, that addresses the issues with the classical notions of determinacy and confluence mentioned above. It has the quite nice property that deterministic shared memory and reaction to absence, as used in synchronous programming, can be modelled. In short: CCSspt coherent expressions can set up a minimal, telescopic foundation for semantic of synchronous programming languages. We only consider a single clock in this paper for illustration and to set the scene for application in synchronous programming. Yet, even in the absence of clocks, the notion of coherence is a non-trivial extension of Milner’s confluence theory. For lack of space, all proofs are omitted and will appear in the full version of the paper.
2
The Syntax and Semantics of Single-clock CCSspt
We assume the reader is familiar with the notation of synchronous process algebras [16]. We first put in place the syntactic signature of action labels and then discuss our new enriched concept of strategic transitions that add priorities and clocks to CCS for scheduling. def Let A/A be sets of co/channel names with a, b, . . . ranging over A. We will refer to the a ∈ R = A∪A as rendezvous actions. Let C = {σ} be a singleton set of broadcast clock names, disjoint from R. For the sake of simplicity, this paper deals with a single clock σ. We have a | a = τ, σ | σ = σ and σ = σ. Let L = R ∪ C be the set of labels and let ℓ range over L, while L, H range over subsets of L. We write L for the set {ℓ | ℓ ∈ L}. Let Lτ = L ∪ {τ} be the set of all actions obtained by adjoining the silent action τ < L and let α range over Lτ . All symbols can appear indexed. CCSspt terms T = P ∪ S come in two
L. Liquori, M. Mendler, C. Stolze
81
mutually recursive syntactic forms, processes P and threads S. Let I ⊂ P be a set of process names, and let p, q . . . range over I. The process terms P, Q ∈ P and the threads terms M, N ∈ S are defined by the following abstract syntax: P, Q ::= | | |
p
P|Q P\A M
process name parallel composition restriction, A ⊆ A. thread.
M, N ::= 0C | α:L.P | M+N
inactive process prefix, α ∈ Lτ , L ⊆ L sum
Each restriction P \ A acts as a name-binder where the channels A are locally bound and thus no longer free. Each P ∈ P has an associated set of free labels L(P) ⊆ L and a clock horizon, or simply a clock, def clock(P) ∈ H where H = {{}, {σ}}. A process of horizon {σ} ∈ H has to synchronise on every tick of the clock. A process of horizon {} ∈ H does not participate in the clock and so runs asynchronously. As usual, unary operators take precedence over binary operators. The clock of a process P, is defined as clock(P) = L(P) ∩ C. Let us inspect the threads: • 0C is the inactive process indexed with its horizon C. The inactive 0{} has horizon {} and thus is asynchronous. The inactive process 0{σ} with horizon {σ} is synchronous and prevents other the synchronous processes from performing σ; • α:L.P is the process that may become P after performing the action α, and the set L ⊆ L contains all the actions taking precedence over it. An action α ∈ R denotes a CCS-style rendezvous (or handshake) action. An action α ∈ C denotes a CSP-style broadcast (or clock) action, that shall synchronise with all the surrounding processes in the scope where this clock has been declared; Where L = ∅, we often simply write the prefix as a.P instead of a:{}.P; • M + N is, as usual, the sum of M and N, that is, it progresses either as M or N. Now, let us inspect the processes: def
• p is name that refers to a predefined process. Names are used for recursion, e.g., p = a:L.p is a process that infinitely offers a with precedences L; • P | Q is, as usual, the parallel composition of P and Q; • P \ A denotes action restriction; it makes local the rendezvous action in A. A process P has to synchronise on every tick of clocks in clock(P), and only those clocks: this corresponds to what Hoare [13] calls the alphabet of a CSP process. It can be easily seen that direct subprocesses of a thread should have the same clock horizon as the thread, i.e. clock(M + N) = clock(M) = clock(N), and clock(α:L.P) = clock(P). Note also that a process P of horizon {} cannot perform σ. It can be also noted def that clock(P | Q) = clock(P) ∪ clock(Q), clock(P \ A) = clock(P), and clock(p) = clock(P) whenever p = P.
2.1
Single-clock CCSspt : Transitions under Blocking and Prediction α
We add priority-based scheduling constraints to the standard transitions P − → Q of CCS to generate strategic transitions α P− → Q B ι between processes P, Q ∈ P, expressing that “P performs the action α with blocking B and prediction ι, and becomes Q”. Formally, α ∈ Lτ is the standard action of the transition, B ⊆ H × 2L is the blocking relation, and ι ∈ H → 2L the prediction function. For compactness, we use the notation α:B[ι] for the label of a strategic transition, referred to as a strategic label.
82
Determinacy with Priorities up to Clocks
ℓ
def
p=P
α P− → Q B ι
α p− → Q B ι
P1 −− → P′ B ι1 1 1
(Con)
ℓ
eschews(iA∗− (Q), B) α P− →ι P′ α < clock(Q)
P2 −− → P′ B ι2 2 2
∀i ∈ {1, 2}, eschews(ιi , B3−i ) ℓ|ℓ P1 | P2 −− −−−→ P′ | P′2 B1 ∪B2 ι1 +ι2 1 α
α
α:L.P −− −−−−−−−−→ {} P {(clock(P),L)} ι
(Act)
M− → P B ι α
M+N − → P B ι∪(iA(N)−{α})
B
(Com) α
(Sum)
(Par)
α
∗ P|Q − → P′ | Q B ι+iA− (Q)
P− → Q B ι
α < A∪A
α
P \ A −B−− → Q\A \A ι\A
(Restr)
Figure 1: Labelled Transition System (LTS) for CCSspt . • Each element (C, L) ∈ B is a blocking constraint from a thread participating in the transition α:B[ι], that only participates provided there cannot be a synchronisation on any of the actions L, within the clock horizon C. The horizon {σ} consists of all actions possibly taken before the clock σ is executed, i.e., it does not include any action happening after the first occurrence of σ. In contrast, the horizon {} consists of all actions both before or after σ. • The prediction ι takes a clock horizon C and returns the set of action labels ι(C) ⊆ L inside P that are considered in competition to α:B[ι] within the horizon C. For instance, in (a.e + b. f ) | c.g, the action a is in competition with b, c and g, but neither e nor f . • Blocking and prediction meet each other in the scheduling of a parallel composition: The synchronisation of a transition α:B1 [ι1 ] with a concurrent partner transition α:B2 [ι2 ] is unblocked if ι1 eschews B2 and ι2 eschews B1 . More precisely, ι eschews1 B iff for all (C, L) ∈ B we have disjointness ι(C) ∩ L = {}, expressing that the prediction ι has no labels synchronising with L in horizon C. We note this property eschews(ι, B). Each blocking B induces a function [B] ∈ H → 2L collecting the blocking actions within horizon C, def defined [B](C) = {ℓ | ∃(C ′ , L) ∈ B, C ′ ⊆ C, ℓ ∈ L}. This relation is monotonic, which means that blocking constraints are preserved when we add clocks. From this we obtain a natural partial ordering B ⊑ B′ between blocking relations, as the inclusion [B](C) ⊆ [B′ ](C) for all C ∈ H. This expresses that B is less restrictive, i.e, B does not block in more contexts than B′ . The corresponding ordering on predictions is simply point-wise inclusion: ι1 ⊑ ι2 iff ι1 (C) ⊆ ι2 (C) for all C ∈ H. Observe that eschews is antitonic in its arguments, i.e., if ι′ ⊑ ι and B′ ⊑ B, then eschews(ι, B) implies eschews(ι′ , B′ ).
2.2
Labelled Transition System
Fig. 1 presents the labelled transition system (LTS) which formally has type P × Lτ × (2H×2 ) × (H → 2L ) × P. A web artefact 2 is available: it implements a parser and the LTS for CCSspt . We work under the following constructivity assumptions: L
Prediction function: iAC∗ (P) is the set of all the labels which appear syntactically in P, up-to some clock in C. For instance, iA∗{σ} (a.b.σ.c | a) = {a, b, σ, a}. Observe that c, which only occurs after σ, is 1 This term is taken from Phillips [19], where it plays essentially the same role. While in [19] the prediction (called “offer-
ings”) and blocking are simply sets of actions, in our synchronous setting they are also scoped by clock horizons. 2 https://cstolze.github.io/synpasite/
L. Liquori, M. Mendler, C. Stolze
83
not included. The presence of process names makes the definition a bit difficult, so we first define the prediction function iACn (P) ⊆ L with an upper bound n ∈ N on the number of unfoldings of process names: = {} ( {α} if α ∈ C n iAC (α:L.P) = {α} ∪ iACn (P) otherwise n (P \ A) = iAn (P)−(A ∪ A) iAC C n (0 ′ ) iAC C
We define iAC∗ (P) =
0 (p) iAC n+1 (p) iAC
= {} = iACn (P)
def
if p = P
n (P | Q) iAC
= iACn (P) ∪ iACn (Q)
n (M + N) iAC
= iACn (M) ∪ iACn (N)
n n n n+1 n∈N iAC (P), noting that iAC (P) is monotonic for n, i.e. iAC (P) ⊆ iAC (P). Initial actions: iA(M) ⊆ Lτ is the set of all the labels which appear syntactically at the beginning of a
S
thread M. For instance, iA((a.c + b.d) | a.c) = {a, b, a}. Observe that c and d, which are not initial, are not included. The initial actions are defined thus: iA(0C ) = {}, iA(α:L.P) = {α} and iA(M + N) = iA(M) ∪ iA(N). Antitonicity: If C ⊆ C ′ then ι(C ′ ) ⊆ ι(C). This can be shown be induction on the LTS rules of Fig. 1. Clock stability: The horizon clock(P) remains stable under derivations, and P can do a σ transition only if clock(P) = {σ}. This is a well-formedness condition we impose on process terms. The rules of Fig. 1 use the following auxiliary operations on blocking and predictions. We combine blocking relations by set union B1 ∪ B2 . The restriction B \ A of a blocking relation simply removes the def actions A ∪ A from each entry in B, i.e., B \ A = {(C, L−(A ∪ A)) | (C, L) ∈ B}. The empty prediction is ι{} , def defined ι{} (C) = {}. As operations on predictions we have point-wise union, written as ι1 + ι2 and defined def (ι1 + ι2 )(C) = ι1 (C) ∪ ι2 (C). We restrict a prediction ι by removing a set of actions A ⊆ A pointwise, def written ι \ A and defined as (ι \ A)(C) = ι(C)−(A ∪ A). With these definitions in place we can take a closer look at the rules in Fig. 1: • (Con) This is the standard unfolding rule for constant definitions, including blocking and predictions. • (Com) The parallel composition rule implements simultaneously the synchronisation of rendezvous actions and the clock: rendezvous synchronisations are dealt with as usual, producing a τ action. For contrast, broadcast synchronisation, via clocks, produce a clock action (since σ | σ = σ), so it remains open for more participants. In either case, the construction of blocking and prediction for the ℓ | ℓ transition is the same: We take the union B1 ∪ B2 of the blockings and the sum ι1 + ι2 of the predictions from the two participating transitions ℓ and ℓ. In addition we must check the unblocking of the synchronisation ℓ | ℓ cross-wise: the prediction ιi of Pi must eschew the blocking B3−i . We note that this works uniformly for rendezvous and clock because eschews(ι, B) is distributive in both its arguments with respect to union and summation. • (Par) This rule describes the asynchronous case where one process P in a parallel composition P | Q executes a step unsynchronised with Q. The blocking B is inherited from the transition α of P. This transition is only enabled as an asynchronous step of P in concurrency with Q, if the prediction iA∗− (Q) eschews the blocking B and if the action α is not a clock of Q. For if α = σ and clock(Q) = {σ} then P cannot proceed alone, and it must synchronise lock-step with Q via rule (Com). Since the actions predicted by iA∗− (Q) are in competition to α, they are added to the prediction ι. • (Act) The execution of a prefix α:L.P publishes the empty prediction function ι{} , because it does not have any alternative choices or concurrency that would compete. The blocking {(clock(P), L)}
84
Determinacy with Priorities up to Clocks
Figure 2: Store S , Readers Ri and Writers Wi , in CCSspt (left) and strategic transitions (right). lifts the blocking set L of the prefix to a blocking constraint in the scope of the thread’s clock. Note, by well-formedness, clock(α:L.P) = clock(P). • (Sum) The iterated application of the summation rule permits us to select any prefix αn :Ln .Pn of a P thread M = i αi :Li .Pi , generating a transition αn :B[ι] of M to Pn , with B = {(clock(Pn ), Ln )} and ι = ι{} ∪ {αi | i , n, αi , αn }. Note that by well-formedness clock(Pn ) = clock(M). The prediction ι contains the initial actions αi for all other choices i , n offered by thread M as competitors to αn . Note that αn does not count as a competitor for itself, whence we subtract it. • (Restr) The restriction rule of rendezvous actions A is as in CCS. It prunes away all local transitions with labels from A∪ A, because these are no longer available for synchronisation outside. Naturally then, we must remove these labels from the blocking and predictions as well, which is done by the operations B \ A and ι \ A, defined above. It is immediate to see that Fig. 1 is a conservative extension of Milner’s CCS [17].
2.3
Two Simple Examples
The interested reader is invited to evaluate the following examples using the LTS. Other examples can be found in [14] and with our artefact (https://cstolze.github.io/synpasite/). • A typical application of priorities is to enforce a “Read-Before-Write” policy for a memory cell. def The process S = w:w.S + r:w.S + σ:{r, w}.S implements the memory cell, with w modelling a write def def action and r a read, ignoring any data. The process R = r.0{σ} implements a reader and W = w.0{σ} a writer. The composition R | W | S will first do a write, then a read. The memory with two writers W | W | S will block and with two readers R | R | S will permit the readers to move in any order. def
• Clocks add expressivity when used with priorities. Take for instance the processes p = r:w.p and def q = w.q. The process p | q will never do r, because w is always in the prediction horizon. However, def def if you consider p′ = r:w.σ.p′ and q′ = w.σ.q′ , then the process p′ | q′ will first do w, then r, then σ, and then loop from start p | q. In this fashion we can model iterated computations on shared memory.
3
From Confluence to Coherence
We now finally come to lift and generalise Milner’s classical notion of confluence (Def. 2) for stategic transitions. For motivation we will refer to the examples in Fig. 2.
L. Liquori, M. Mendler, C. Stolze
85
Classical determinacy (Def. 1) requires that any two transitions with the same visible action must lead to congruent states, which is too strong: The composition of two readers R1 | R2 = r.P1 | r.P2 = r.a.0 | r.b.0, sharing the same memory access point generates r-labelled transitions to non-congruent successor states P1 | R2 R1 | P2 , in general. Using strategic labels we can disambiguate them. The strategic transitions r
r
3
6
R1 | R2 −− → ′ P | R and R1 | R2 −− → ′ R | P2 with ι′3 = ι3 + iA∗− (R2 ) = iA∗− (R2 ) and ι′6 = ι6 + iA∗− (R1 ) = iA∗− (R1 ) B ι3 1 2 B ι6 1 are obtained by the (Par) rule and have r in both predictions since r ∈ iA∗{σ} (R2 ) and r ∈ iA∗{σ} (R1 ). So, in each transition, the other label r is observable as a competitor within the clock horizon, i.e., r ∈ ι′3 ({σ}) and r ∈ ι′6 ({σ}). With this in mind, we replace ‘determinate’ (Def. 1) by the following notion of ‘observable’. α
1 Definition 3. A process P is observable (modulo ) if for all derivatives Q and transitions with Q −− → Q B ι1 1
α
2 and Q −− → Q , such that α1 , α2 or Q1 Q2 , if {α1 , α2 } ⊆ L then α1 ∈ ι2 ({σ}) and α2 ∈ ι1 ({σ}). B ι2 2
1
2
Note that Def. 3 permits silent transitions α1 = τ = α2 to end up in non-congruent states Q1 Q2 . This is needed for strong bisimulation. For instance, R1 | S | R2 has τ-transitions to non-bisimilar states P1 | S | R2 / R1 | S | P2 . This is non-determinate by Def. 2, but observable by Def. 3. Also, since a clock α1 = σ = α2 is never in competition with itself, i.e., σ < ιi ({σ}), then observability forces Q1 Q2 , i.e., the clock is deterministic. In this way, we capture time determinacy of timed extensions of CCS [12, 18]. The classical notion of confluence requires reconvergence for any pair of distinctly labelled transitions. This is too strong for our purposes. A shared store S , by its very nature, must offer a preempting choice for a reader (on r) and a writer (on w), generating a race that leads to incongruent successor states S S 1 . The read and the write are distincly labelled but not confluent by Def. 2. But this is no problem, if the store resolves the race by priority, giving w precedence over r (or the other way around). Technically, this is done by adding the blocking constraint ({σ}, {w}) ∈ B1 in the stategic action r:B1 [ι1 ] of the read (see Fig. 2). The presence of a concurrent writer W1 , say, with w ∈ iA∗{σ} (W1 ) in its prediction, will then block the read action r:B1 [ι1 ] in rule (Par) since eschews(iA∗− (W1 ), B1 ) is false. Hence, there is no competition between the two distinct choices r and w of S and we do not need to require reconvergence, unlike with Def. 2. The classical notion of confluence is also too weak, when it comes to sharing, as it requires reconvergence for any pair of distinctly labelled transitions. The write label w of S can be consumed only once, by a single writer. Two writers S | W1 | W2 with W1 = w.P1 and W2 = w.P2 generate a race condition. Unfortunately, the standard test for confluence will not detect the problem, because the w-transition of S is not distinct from itself. But competes against itself, because it can be consumed only once. Here, we eliminate the race by making the strategic action w:B2 [ι2 ] be self-blocking, so that w ∈ [B2 ]({σ}). This blocks the write action in the presence of a second writer. With a single writer, S | W1 reduces to S 1 | P1 but S | W1 | W2 blocks in (Par). For the reading action r we have a different situation. The store happily supports multiple readers, as r may be infinitely repeated without S changing its state. In this case, the stategic action r:B1 [ι1 ] can be such that r < [B]({σ}). In sum, we must require reconvergence not just for any pair of distinctly labelled transitions but any pair of mutually non-blocking transitions. The following notion of ‘independence’ replaces the ‘distinctness’ condition in the classical notion of confluence, taking into account the blocking relation. α
α
1 2 Definition 4 (Independence). Two transitions Q −− → Q and Q −− → Q are independent (modulo ) if B1 ι1 1 B2 ι2 2 {α1 , α2 } = {σ} or {α1 , α2 } ⊆ R ∪ {τ} and one of the following holds:
1. {α1 , α2 } , {τ} and both α1 < [B2 ]({σ}) and α2 < [B1 ]({σ}), or 2. α1 = α2 and Q1 Q2 .
86
Determinacy with Priorities up to Clocks
We now define coherence by refactoring the classical notion of confluence (Def. 2) with ‘observable’ for ‘determinate’ and ‘independent’ for ‘distinct’. In addition, we require that the reconvergence is monotonic in the blocking relations and prediction functions. Definition 5 (Coherence). A process Q satisfies the Diamond Property (DP) if, for every pair of independent transitions, α1 α2 Q −− → Q and Q −− → Q , B ι1 1 B ι2 2 1
2
called a divergence (modulo ), there exists a reconvergence (modulo ), consisting of processes Q′1 , Q′2 with Q′1 Q′2 and α1 α2 → ′ Q′ Q1 −− → ′ Q′ and Q2 −− B′ ι1 2 B′ ι2 1 2
such that B′i ⊑ Bi and if αi ∈ R then ι′i ⊑ ιi for i ∈ {1, 2}.
1
P is coherent (modulo ) if it is observable
(modulo ) and every derivative of P satisfies DP. The most important consequence of coherence is that coherent process are “determinate” under silent actions, i.e., reduce to a unique normal form. As in the λ-calculus, we call a process N in normal form if it does not have any τ-transitions. Then, it is internally stable without rendezvous synchronisations, yet may still participate in a clock step. Let us write P ⇓ N to express that P reduces to normal form N. Lemma 1. Let P be coherent. Then P ⇓ N1 and P ⇓ N2 implies N1 N2 . Lem. 1 only concerns the reductions, i.e., the τ-transitions, of a coherent process. For races between τ and σ, coherence does not imply reconvergence, for good reasons. We can thus model scenarios where a synchronous system (horizon {σ}) communicates asynchronously with a process of horizon {}. Such interactions in general create data races for good reason: A synchronous system can notice if a communication with external processes happens before or after the clock, and act differently. Our main result is the following Preservation Theorem, stating that parallel composition and restriction preserve coherence. Theorem 1 (Preservation). If P1 , P2 are coherent then P1 | P2 is coherent. If P is coherent, then P \ A is coherent. How to we establish coherence? To prove that a given process P ∈ P is coherent requires that we show DP for all derivatives of P. The general technique to prove membership then is co-induction on the immediate transitions of a process. Formally, we call a class of processes Coh ⊆ P a coherence class if it is (i) derivation closed, i.e., if Q ∈ Coh and Q → Q′ implies Q′ ∈ Coh, (ii) all Q ∈ Coh are observable and satisfy DP. It is easy to see that P is coherent iff there exists a coherence class Coh with P ∈ Coh. The standard application of this principle is to take Coh to be the set of all derivatives of P, which is trivially derivation closed, and show that each of them is observable and satisfies DP. We illustrate this technique on our store-reader-writer example which form the transition system seen in Fig. 2 with the transitions decorated with their strategic labels of shape α:B[ι]. All processes are synchronous with clock(S ) = clock(Wi ) = clock(Ri ) = {σ}, so each blocking constraint (C, L) ∈ B has C = {σ}, whence [B]({}) = {}. For notational conciseness we identify B with the set [B]({σ}) ⊆ L, i.e., the set of actions that block α, within the current clock cycle. Likewise, we can identify the prediction ι with the set ι({σ}) ⊆ L, since ι({}) = ι({σ}). The set ι({}) is not larger than ι({σ}) since there are no asynchronous actions, i.e., with clock horizon {}. The fact that our basic processes model single threads (no internal concurrency) means that the ι of an action is essentially the set of distinct actions in immediate competition with α in the respective thread, generated by rules (Sum) and (Act). For instance the initial looping transition r:B1 [ι1 ] of S in Fig. 2 has B1 = {w} because we have write-before-read and ι1 = {w} because
L. Liquori, M. Mendler, C. Stolze
87
S has an initial w-transition competing with r. The strategic label r:B1 [ι1 ] is thus r:{w}[{w}] generated from the syntactic prefix r:{w}.S of the thread S = r:{w}.S + w:{w}.S 1 . Now let us check coherence. Firstly, both derivatives S and S 1 are observable. In fact, the only two transitions to consider with α1 , α2 or Q1 Q2 are α1 = r and α2 = w out of S . But they satisfy α1 ∈ ι2 = {r} and α2 ∈ ι1 = {w}. Next we check that S satisfies DP. Since the r is blocked by w and the wtransition is self-blocking, the only pair of independent transitions out of S is the r-transition competing α1 α2 against itself, S −− → Q and S −− → Q with Q1 = S = Q2 , α1 = r = α2 and B1 = {w} = ι1 and B2 = {w} = ι2 . B ι1 1 B ι2 2 1
2
α
2 ′ S and But the r-loop can be infinitely repeated and so both have a trivial reconvergence with Q1 −− → B′ ι2
α
2
1 ′ S where B′ = {w} = ι′ and B′ = {w} = ι′ which trivially satisfies S S , B′ ⊑ Bi and ι′ ⊑ ι′ as Q2 −− → i i i 1 1 2 2 B′1 ι1 required by Def. 5. Finally note that S 1 has a single σ-transition which is self-blocking and thus trivially satisfies DP. In the same fashion, one verifies that all processes and derivatives of Fig. 2 are observable and satisfy DP. Observe that the priority system allows us to check for absence: if α:L.P can proceed, we are sure that none of the actions in L can synchronise up to clock(P). Using τ prefixes allows us to check for absence without doing anything else: For instance, a:{}.P + τ:{a}.Q intuitively means “if a is feasible in the current cycle, then do a then P, else do Q”.
4
Conclusion
In this paper we propose the novel concept of coherence to strengthen the notion of confluence from Milner’s classical theory [17]. It is based on the mechanism of strategic action labels that generalises earlier work on priority-guarded CCS [7, 20, 19]. Our Preservation Theorem 1 is a significant advance. It holds without additional conditions unlike Milner’s notion of confluence, which needs sort separation. In addition, it applies to P | Q and P \ A separately, unlike confluence that only holds for a combination of both, and it applies to any congruence . This extends the confluence theory of Chap. 11 of Milner’s book. By adding clocks we can treat determinacy compositionally in multi-threaded shared memory and synchronous programming with reaction to absence à la Esterel. Previous attempts such as the Sπ language [1], or SPL [15] do not adequatly encode Esterel constructs. For example, Sπ does not deal with immediate reaction to absence and SPL only encodes local consistency rather than Esterel’s global consistency. It is known from priority-guarded extensions of CCS that strategic action labels add expressiveness [21]. In the case of CCSspt it is easy to see that there is no compositional encoding into CCS. Consider the terms a:a and a:a which have one transition each, with action a and a, respectively. When composed in parallel, a:a | a:a has only one possible transition, performing τ. However, there are no CCS processes P and Q which perform one transition each, and, put in parallel, only perform one transition, because parallel composition in CCS preserves the transitions of the composed processes. What is noteworthy is that unlike in traditional priority-guarded CCS such as CPG, there does not seem to be a natural expansion lemma for the stategic labels of CCSspt under the scheduling rules of Fig. 1, i.e., we cannot hope to rewrite every parallel composition as a single thread. The reason is that a self-blocking prefix a:L.P with a ∈ L will block when put in parallel with two consumer threads M1 and M2 with a ∈ iA∗ (Mi ), but it does not block with only one of them. So, if the composition M1 | M2 was expandable to a congruent single-threaded process M, then (a:L) | M1 | M2 (a:L) | M and so (a:L) | M1 | M2 should not block. Interestingly, self-blocking prefixes have not been considered in the classical theories [7, 20, 19], while here they naturally play an important role. They bring about a true-concurrency semantics.
88
Determinacy with Priorities up to Clocks
Moreover, in these classical approaches, prediction is based on the immediate actions iA of a process, with the effect that the scheduling priorities can change with each transition. Here, we use iA∗ in the scheduling rules which is more conservative (Constructivity Assumption) and enjoys a useful monotonicity property: once an action is unblocked, it remains unblocked until the clock horizon is reached. This has the interesting consequence that summation + does not seem to be expressible anymore, in terms of prioritised prefixes and restricted parallel composition, unlike in CPG. To be specific, define a.P ⊕ b.Q as an abbreviation of (a:c.(P | c)) | (b:c.(Q | c)) \ c. Then, in CPG this sum ⊕ indeed acts like a non-deterministic free choice a.P + b.Q [19]. In our semantics, however, ⊕ behaves deterministically. It blocks, because of the conservative “up-to-clocks” predictions {a, c} ⊆ iA∗ (a:c.(P | c)) which can see the blocking action c even though it is guarded by the a action. Moving away from immediate enabling based on iA to up-to-clocks enabling based on iA∗ is the cornerstone for modelling the synchronous micro-macro step abstraction of the constructive semantics of Esterel-style languages [3, 11, 6]. Let us note that the classical immediate enabling iA can be used to code synchronous Statecharts as has been shown by [15] using a CCS-style algebra. But this only captures a weak form of reaction to absence (with local consistency rather than global consistency) and depends on special syntactic operators. We leave the exact characterisation of expressiveness of CCSspt as an open problem. We also plan to expand our theory by standard instruments such as notions of bisimulation, observational congruence, and associated algebraic axiomatisations. We are also working on extending the theory to other static operators such as clock hiding (for time abstraction) and to multiple clocks which will apply to globallyasynchronous, locally-synchronous programming and extend our earlier work on PMC [2] and CSA [8]. In PMC there are no priorities and the timeout behaves simply like a choice P + σ:{}.Q in CCSspt . For contrast, CSA uses a fixed priority scheme that makes rendezvous actions take priority over any clock. In CCSspt the timeout can be coded, too, as a sum P + σ:L.Q. Thus, by permitting general priority schemes as in CPG, which has no clocks, CCSspt is likely more expressive than any of these prior systems. We point out that the general principle of LTS with negative premises has been studied in [5]. The priority guards here and in Phillips’ work are special, however, because they are not negations of the transition relation itself but they are defined independently via predicates such as iA and iA∗ . This avoids many a complication of the general theory. Priorities as negative premises for system specification are also fundamental in the BIP algebra of interactions proposed in [4] which present a generic and compositional paradigm of coordination protocols for parallel languages. The synchronisation mechanisms of CCS rendezvous and CSP broadcast actions (clocks) are but special cases of interactions on BIP connectors. BIP interactions (defined on distinct alphabets of components) can distinguish the identity of threads. Hence, BIP can capture the semantics of self-blocking as in CCSspt , where a:a | a is not blocking while a:a | a | a is blocking. This is not possible in CPG, which does not have self-blocking at all. However, in BIP we would still only capture CPG-style local priorities, based on immediate initial actions, not priorities “up-to-clocks” like in CCSspt . An even more important open question on BIP expressiveness stems from the nature of BIP priorities, which require that an interaction has to be maximal in some strict “priority” ordering. It will be interesting to investigate if priorities in the style of CCSspt (and a fortiori of prioritised CCS) can actually be expressed in this way. We are not aware of any comparison of BIP [4] with prioritised CCS [7, 8, 9, 19]. Reciprocally, we leave it to future work to explore how our notion of coherence carry over to general coordination languages such as BIP or REO [10]. Acknowledgements. The authors are grateful to Martin Steffen, Gerald Lüttgen, Robert de Simone, Adrien Guatto, and Furio Honsell for useful discussions and comments. Michael Mendler and Claude Stolze are funded by DFG under grant number ME 1427/7-1, Luigi Liquori is funded by ETSI under grant number STF 655.
L. Liquori, M. Mendler, C. Stolze
89
References [1] R. M. Amadio (2007): A Synchronous π-Calculus. Information and Computation 9(205), pp. 1470–1490, doi:10.1016/j.ic.2007.02.002. [2] H. R. Andersen & M. Mendler (1994): An asynchronous process algebra with multiple clocks. Proc. ESOP, pp. 58–73, doi:10.1007/3-540-57880-3_4.
In:
[3] G. Berry (1999): The Constructive Semantics of Pure Esterel. Draft Book. [4] S. Bliudze & J. Sifakis (2007): The algebra of connectors: structuring interaction in BIP. In: Proc. of EMSOFT, ACM, pp. 11–20, doi:10.1145/1289927.1289935. [5] R. Bol & J. F. Groote (1996): The Meaning of Negative Premises in Transitions System Specifications. JACM 43(5), pp. 863–914, doi:10.1145/234752.234756. [6] F. Boussinot & R. de Simone (1996): The SL synchronous language. IEEE Transactions on Software Engineering 22(4), pp. 256–266, doi:10.1109/32.491649. [7] J. Camilleri & G. Winskel (1995): CCS with priority choice. Information and Computation 116(1), pp. 26– 37, doi:10.1006/INCO.1995.1003. [8] R. Cleaveland, G. Lüttgen & M. Mendler (1997): An Algebraic Theory of Multiple Clocks. In: Proc. of CONCUR, LNCS 1243, pp. 166–180, doi:10.1007/3-540-63141-0_12. [9] R. Cleaveland, G. Lüttgen & V. Natarajan (1998): A Process Algebra with Distributed Priorities. Theor. Comput. Sci. 195(2), pp. 227–258, doi:10.1016/S0304-3975(97)00221-1. [10] K. Dokter, S.-S. Jongmans, F. Arbab & S. Bliudze (2017): Combine and Conquer: Relating BIP and Reo. Journal of Logical and Algebraic Methods in Programming 86, pp. 134–156, doi:10.1016/j.jlamp.2016.09.008. [11] R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer & O. O’Brien (2014): SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications. In: Proc. of PLDI, ACM, pp. 372–383, doi:10.1145/2594291.2594310. [12] M. Hennessy & T. Regan (1995): A process algebra for timed system. Information and Computation 117, pp. 221–239, doi:10.1006/INCO.1995.1041. [13] C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice-Hall. 256 pages. [14] L. Liquori, M. Mendler & C. Stolze (2026): A process calculus with clocks and priorities. https://inria. hal.science/hal-05497982. [15] G. Lüttgen, M. von der Beeck & R. Cleaveland (1999): Statecharts Via Process Algebra. In: Proc. of CONCUR, LNCS 1664, Springer, pp. 399–414, doi:10.1007/3-540-48320-9_28. [16] R. Milner (1983): Calculi for Synchrony and Asynchrony. doi:10.1016/0304-3975(83)90114-7.
Theor. Comput. Sci. 25, pp. 267–310,
[17] R. Milner (1989): Communication and Concurrency. Prentice Hall. [18] X. Nicollin & J. Sifakis (1994): The Algebra of Timed Processes, ATP: Theory and Application. Inf. Comput. 114(1), pp. 131–178, doi:10.1006/INCO.1994.1083. [19] I. Phillips (2008): CCS with priority guards. The Journal of Logic and Algebraic Programming 75(1), pp. 139–165, doi:10.1016/J.JLAP.2007.06.005. [20] G. Lüttgen R. Cleaveland & V. Natarajan (2001): Priority in Process Algebra. In: Handbook of Process Algebra, North-Holland / Elsevier, pp. 711–765, doi:10.1016/B978-044482830-9/50030-8. [21] C. Versari, M. Busi & R. Gorrieri (2009): An expressiveness study of priority in process calculi. Mathematical Structures in Computer Science 6(19), pp. 1161—-1189, doi:10.1017/S0960129509990168.