Matthieu Perrin
email: matthieu.perrin@univ-nantes.fr

Claude Jard
email: claude.jard@univ-nantes.fr

Achour Mostéfaoui
email: achour.mostefaoui@univ-nantes.fr

Proof of the Instrumented Semantics for Orc

Keywords: Preemption, Conflict, Concurrency, Orc, Semantics, Causality, Asymmetric event structure EXTCALL

This report shows how the operational semantics of a language like ORC can be instrumented so that the execution of a program produces information on the causal dependencies between events. The concurrent semantics we obtain is based on labeled asymetric event structures. This report contains the complete demonstration of correctness of this approach.

Introduction

The standard form for describing the semantics of a computer language is the structural operational semantics (SOS) [START_REF] Gordon D Plotkin | The origins of structural operational semantics[END_REF]. SOS specifications take the form of a set of inference rules that define the valid transitions of a composite piece of syntax in terms of the transitions of its components. Rewriting transforms terms by executing a rule (it may be a non-deterministic transition in case of multiple alternatives). The successive transitions represent the program behavior. This may produce a sequence of values, that can be brought by the labelling of rules. In this vision, the behaviors are therefore defined sequentially, even for languages describing parallel behaviors.

This vision is consequently limited for modern languages comprising parallelism. Indeed, in these languages, the concepts of concurrency, causality and conflict are important to explicit (for example, to answer questions on root causes analysis, debugging&replay, race detection, QoS assessment, etc.). This is the role of a concurrent semantics. In such semantics, behaviors are seen as partial orders (encoding the causality between the events produced by a given program), optionally augmented by the notion of conflict identifying non-deterministic choices that have been made (e.g. event structures [START_REF] Winskel | Event structures[END_REF]).

The method used in this article is to extend the standard SOS semantics to rewrite extended expressions, in which additional information has been added to compute causal and weakly-causal dependencies. This information is also made visible by extending the labelling of transitions. Concurrency is just the complement of the weakly-causal relation, and conflict is defined by cycles in this relation.

Capturing causality and concurrency by instrumenting the semantics rules is a difficult job. This is mainly because these relationships are global and are difficult to locate on the syntactic forms. The solution is to keep information about the causal past in a context associated with each rule being careful to build the necessary links between different contexts during the execution of rules. The aim is that such instrumented semantics reproduces the standard behavior of the program while calculating the additional information needed to find concurrency, causality and conflict between events produced by the execution.

The proposed approach is illustrated on the Orc language [START_REF] Kitchin | The orc programming language[END_REF]. Orc is a novel language, formally defined and specially adapted to program across the Web in a highly parallel and distributed context. A first attempt of concurrent semantics based on event structures has already been published [START_REF] Rosario | Event structure semantics of orc[END_REF], but using an ad-hoc connection of Petri net diagrams. A similar approach was used in [START_REF] Bruni | Translating Orc features into Petri nets and the Join calculus[END_REF] to compare Orc with the Join calculus. Here, the approach appears to us more simple and elegant. It is especially dynamic in the sense that it can produce online information, interesting feature in practice for many above-mentioned applications. To our knowledge, the only attempt to use an instrumentation to track causality online in a multithreaded program is [START_REF] Grigore | An instrumentation technique for online analysis of multithreaded programs[END_REF] for the C language, but the instrumentation is made by a program transformation, which excludes the possibility to explore further than causality.

Our contribution in this article consists in two new semantics for the Orc language. The first one is an instrumentation of the standard semantics that preserves the behavior of Orc while tracking causal and weakly-causal relations between the events. The second semantics, the concurrent semantics, is an extension of the instrumented semantics that generates all possible events for an Orc expression, so every execution represents all possible sequential executions of the program. These two semantics are complementary, as the first one is lighter and respects the standard notion of execution, while the second one provides more information.

The reminder of the article is organized as follows. We start with a presentation of the Orc language in Section 2. In Section 3, we introduce the labelled asymmetric event structures, used to represent concurrent executions. Section 4 and 5 detail our two contributions: respectively the instrumented and the concurrent semantics. The proof of there properties are are given in Section 6. Finally, section 7 discusses how to combine the two semantics and concludes the paper.

The Orc Programming Language 2.1 Wide-area computing

The Orc language was initially designed to orchestrate web sites. Its underlying philosophy is that modularity is essential to the construction of large modern programs. Such programs may be composed out of several components, possibly written in a variety of languages, that cannot work together without a conductor that orchestrates their executions. In Orc, these components, called sites, can be any kind of externally defined service as well as encapsulations of Orc expressions. Unlike functions in functional programming languages, Orc sites cannot return a result. Instead, they publish zero, one or more values. Sites can be higher-ordered, so values can be sites themselves. This allows the use of complex shared data types; each instance of which is viewed as a different site. A standard library of sites is defined to handle many aspects of everyday programming such as complex data types features, clocks and timers to define some synchrony in programs. How the sites interact is the heart of the Orc language. To this end, it provides the developers with a series of control structures. Some of them, like the conditional structure, are very classical, while others, designed to express concurrency, are more original. These are formally defined in a mathematical abstract programming language: the Orc core calculus, from which the full language is defined as syntactic sugar.

Core calculus

As the higher-level constructions of the language are defined from the Orc core calculus, we only consider this well-defined calculus in the remaining of this paper. The expressions of the calculus, grouped in the set Orcs, is defined as follows:

= ?V k (v) ?D h(ω) h(!v) l ∈ Label ::= !v n ω
The expressions of the calculus that correspond to real Orc programs, in the set Orc, are those that do not contain ?k and ⊥ expressions. Here are the rules of the standard semantics :

(PUBLISH) v !v -→ stop v closed (DEFDECLARE) [D/y]f l -→ f ′ D#f l -→ f ′ D is def y(x) = g (STOP) stop ω -→ ⊥ (INTCALL) D(p) ?D --→ [D/y][p/x]g D is def y(x) = g (STOPCALL) stop(p) ω -→ ⊥ (EXTCALL) V (v) ?V k (v) ----→?k k fresh (EXTSTOP) V (stop) ω -→ ⊥ (OTHERN) f n -→ f ′ f ; g n -→ f ′ ; g (OTHERV) f !v -→ f ′ f ; g !v -→ f ′ (OTHERSTOP) f ω -→ ⊥ f ; g h(ω) ---→ g (NTRES) ?k receives N T (v) ?k !v -→?k (TRES) ?k receives T (v) ?k !v -→ stop (NEGRES) ?k receives N eg ?k ω -→ ⊥ (SEQN) f n -→ f ′ f >x> g n -→ f ′ >x> g (SEQV) f !v -→ f ′ f >x> g h(!v) ---→ (f ′ >x> g)|[v/x]g (SEQSTOP) f ω -→ ⊥ f >x> g ω -→ ⊥ (PARLEFT) f l -→ f ′ f |g l -→ f ′ |g l = ω (PARRIGHT) g l -→ g ′ f |g l -→ f |g ′ l = ω (PARSTOP) f ω -→ ⊥ g ω -→ ⊥ f |g ω -→ ⊥ (PRUNEN) g n -→ g ′ f <x< g n -→ f <x< g ′ (PRUNELEFT) f l -→ f ′ f <x< g l -→ f ′ <x< g l = ω (PRUNEV) g !v -→ g ′ f <x< g h(!v) ---→ [v/x]f (PRUNESTOP) g ω -→ ⊥ f <x< g h(ω) ---→ [stop/x]f
The only values considered in the Orc core calculus are sites. They can be external, which is denoted V in the syntax, or internally defined (D). For the sake of clarity, we consider in this work that the sites are curryfied. An internal site can be defined as def y(x) = f #g where f is the body of the site and g is the remaining of the program in which y can be used as any site. Site definitions are recursive, which allows the same expressivity as any functional language. Both kinds of sites can be called with their argument using the classical functional notation. However, their behaviors are different, as we can see on the operational semantics. The main difference is that calls to external sites are strict, i.e. their arguments have to be bounded before the site can be called, while an internal site can be called immediately, and its arguments are evaluated lazily. When an external site is called, it sends its responses to a placeholder ?k. A response can be either a non-terminating value N T (v) if further responses are expected, or a terminating value T (v) if this is the last publication of the site or N eg if the site terminates without publishing any value.

Besides sites, four combinators are provided by core calculus. The parallel composition expresses pure concurrency. In f |g, f and g are run in parallel, their events are interleaved and the expression stops when both f and g have terminated. As suggested by its name, the sequential operator expresses sequentiality. In the expression f > x > g, the variable x can be used in g. Here, f is started first, and then a new instance of g[v/x], where x is bounded to v, is launched as a consequence of each publication of v. The third operator, called pruning, expresses preemption. In f <x< g, the variable x can be used in f . Both f and g are started at once, but f is paused when it needs to evaluate x. When g publishes a value, it is bounded to x in f and g is stopped. The other events that could have been produced by g are preempted by the publication. For example, if g is supposed to publish two values a and b, only one will be selected and published in each execution. We say that these two events are in conflict. The last operator is called otherwise. In f ; g, f is first started alone and g is started if and only if f stops without publishing any value.

Finally, the stop symbol can be used by the programmer exactly like a site or a variable to denote a terminated program. stop still produces an event ω to notify its parent expression that it has terminated. It then evolves into ⊥, the inert final expression. Just like ?k, ⊥ cannot be used directly.

Illustration

We will now illustrate the Orc core calculus on an example. Let us consider a program f0 defined as

f0 = y + z <y< ((2|3) >x> x) <z< 1.
The left hand side causally depends on y and z, its execution is thus delayed. Two conflictual values are possible for y. In this example, both 2 and 3 can be published concurrently in the left hand side of the sequential operator, but when a value is published for the second time, it is bounded to y and the remainder of the execution is preempted. Finally, the value of z is defined by the publication of a constant value, the execution of which is concurrent to the computation of y. The following is a possible execution.

f0 h(2) ---→ y + z <y< ((stop|3) >x> x|2) <z< 1 h(1) ---→ y + 1 <y< ((stop|3) >x> x|2) h(3) ---→ y + 1 <y< ((stop|stop) >x> x|3|2) h(3) ---→ 3 + 1 ?+(3,1) -----→?k !4 -→ stop ω -→ ⊥
Many executions are possible for the standard semantics. A few of them are given below.

                       h(!

1).h(!3).h(!3).? + (3, 1).!4.ω, h(!3).h(!1).h(!3).? + (3, 1).!4.ω, h(!3).h(!3).h(!1).? + (3, 1).!4.ω, h(!2).h(!1).h(!3).h(!3).? + (3, 1).!4.ω, h(!1).h(!2).h(!3).h(!2).? + (2, 1).!3.ω, h(!2).h(!1).h(!3).h(ω).h(!3).? + (3, 1).!4.ω, h(!2).h(!1).h(!3)

.h(ω), . . .

                       ⊂ f0
It is possible to do some observation on these executions. For example, all the executions that contain the event !4 also contain one event h(!1) and two instances of h(!3), that appear before the publication !4. This hides a relation of causality between these events. Moreover, no execution contains both the events ? + (2, 1) and ? + (3, 1), which denotes conflict. However, it is very difficult to use these observations in practice for two reasons. First, the number of executions is too large, and even infinite very often, to test even simple properties. Secondly, we lost all the information of how to identify events from different executions. We cannot say that the two instances of h(!3) are in the same order in the two first executions, so we can say nothing about there causal dependencies. This is why it is necessary to aggregate the information of many executions into a unique object.

Labelled Asymmetric Event Structure

The explosion of the number of possible executions is due to their representation as sequences of events: parallel executions are interleaved, creating an exponential number of possibilities. A natural objects to represent concurrent events in a compact way are labelled asymmetric event structures (LAES). Definition 1 (Labelled asymmetric event structure). A labelled asymmetric event structure (LAES) is a tuple (E, L, ≤, ր, Λ).

• E is a set of events, • L is a set of labels, • ≤, causality is a partial order on E, • ր, weak causality is a binary relation on E, • Λ : E → L is the labelling function, • each e ∈ E has a finite causal history [e] = {e ′ ∈ E|e ′ ≤ e},
• for all events e < e ′ ∈ E, e ր e ′ , where < is the irreflexive restriction of ≤,

• for all e ∈ E, ր ∩[e] 2 is acyclic.

A LAES can encode many relations between events in concurrent systems. Let (E, L, ≤, ր, Λ) be an asymmetric event structure and e, e ′ ∈ E two events. We say that: We also define an induced conflict relation #a as the smallest set of finite parts of E such that: for E ′ ⊂ E and e0, e1, ..., en ∈ E,

• e is a cause of e ′ ,
• if e0 ր e1 ր • • • ր en ր e0 then {e0, e1, • • • , en} ∈ #a • if E ′ ∪ {e0} ∈ #a and e0 ≤ e1 then E ′ ∪ {e1} ∈ #a.
Informally, two events are conflictual if they cannot occur together in the same execution.

A LAES can be seen as a structure that encodes concisely several sequential executions; each of them being a linearization of the LAES. Definition 2 (Linearization). Let E = (E, L, ≤, ր, Λ) be a LAES. A finite linearization of E is a word w = Λ(e0) . . . Λ(en) where the different ei ∈ E are distinct and such that:

• it is left-closed for causality:

∀e ∈ E, ∀e ′ ∈ {e0, . . . , en}, e ≤ e ′ ⇒ e ∈ {e0, . . . , en},

• the weak causality is respected: ∀ei, ej ∈ {e0, . . . , en}, ei ր ej ⇒ i < j

We denote Lin(E ) as the set of all finite linearizations of E .

The last definition allows to compare two LAESs. There is an injection between two LAESs if one contains at least the information of the other one. In that case, there is an inclusion between the set of linearizations. Two LAESs are isomorphic if they encode the same information. Definition 3 (Injection). Let E1 = (E1, L1, ≤1, ր1, Λ1) and E2 = (E2, L2, ≤2, ր2, Λ2) be two LAESs. An injection from E1 to E2 is an injective function f : E1 → E2 such that:

• ∀e ∈ E1, Λ1(e) = Λ2(f (e)), • ∀e ≤1 e ′ ∈ E1, f (e) ≤2 f (e ′ ), • ∀e ր1 e ′ ∈ E1, f (e) ր2 f (e ′ ). • ∀e2 ≤2 f (e) ∈ E2, ∃e1 ∈ E1, e2 = f (e1).
We write E1 < E2 if there is an injection from E1 to E2 and we say that E1 and E2 are isomorphic, denoted E1 ≡ E2, if E1 < E2 and E2 < E1.

Instrumented Semantics

Method

The principle of an operational semantics is to produce the set of events that may occur during an execution and to publish them as transition labels. Total ordering of events is not relevant for concurrent programs. Our approach does not affect the successive enforcement of the rules, but adds additional information in the labels that allows to track the partial order.

Actually, a label in the instrumented semantics is a tuple e = (e k , e l , ec, ea), where e k is an identifier taken in a countable set K, that is unique for the execution, e l is a label similar to those of the standard semantics and ec and ea contain the finite sets of the identifiers of the causes and the week causes of the event, respectively.

In order to record the information concerning the past of an expression, we enrich the language with a new syntactic construction: f, c, a L means that c and a are the causes of the Orc instrumented expression f . Thus, if f has c and a as causes and if it can evolve into f ′ , this transition should also have c and a as causes. The index L expresses the kind of events that can activate the rule: !v matches any publication, l stands for any label and ω means that c and a are only the causes of the termination of the program. This new construction is formally defined by two new rules in the semantics: CAUSEYES and CAUSENO.

We also consider that the external sites track themselves causality, as an internally-defined function would do. It makes sense as some sites (e.g. +) handle their calls independently, while others (e.g. shared registers, management library) induce more complex causality patterns between the calls. Hence, the responses we get include this additional information. The verification of these responses is not the subject here, and we suppose them correct by hypothesis.

The instrumented semantics is defined on the set Orci of expressions of this extended syntax:

f, g, h ∈ Expression ::= p p(p) ?k f |g f >x> g f <x< g f ; g D#f ⊥ f, K, K L D ∈ Definition ::= def y(x) = f v ∈ Orc Value ::= V D p ∈ Parameter ::= v stop x p, K, K L w ∈ Response ::= N T (v, K, K) T (v, K, K) N eg(K, K) n ∈ Hidden Label ::= ?V k (v) ?D h(ω) h(!v) l ∈ Label ::= !v n ω

Rules

The rules of the instrumented semantics are given Thereafter.

(PUBLISH) v k,!v,∅,∅ -----→i stop, {k}, ∅ l v closed k fresh (STOP) stop k,ω,∅,∅ ----→i ⊥ k fresh (DEFDECLARE) [D/y]f k,l,c,a ----→i f ′ D#f k,l,c,a ----→i f ′ D is def y(x) = g (STOPCALL) P k,ω,c,a ----→i ⊥ P (p) k,ω,c,a ----→i ⊥ (INTCALL) P k,!D,c,a -----→i P ′ P (p) k,?D,c,a -----→i [D/y][p/x]g, c ∪ {k}, a l D is def y(x) = g (EXTCALL) P k,!V,c,a -----→i P ′ p k ′ ,!v,c ′ ,a ′ ------→i p ′ P (p) k,?V k (v),c∪c ′ ,a∪a ′ ------------→i ?k, c ∪ c ′ ∪ {k}, a ∪ a ′ l (EXTSTOP) P k,!V,c,a -----→i P ′ p k ′ ,ω,c ′ ,a ′ ------→i p ′ P (p) k,ω,c∪c ′ ,a∪a ′ ---------→i ⊥ (OTHERN) f k,n,c,a ----→i f ′ f ; g k,n,c,a ----→i f ′ ; g (RESNT) ?k receives N T (v, c, a) ?k j,!v,c,a∪c ------→i?k j fresh (OTHERV) f k,!v,c,a -----→i f ′ f ; g k,!v,c,a -----→i f ′ (REST) ?k receives T (v, c, a) ?k j,!v,c,a∪c ------→i stop, c ∪ {j}, a ω j fresh (OTHERSTOP) f k,ω,c,a ----→i ⊥ f ; g k,h(ω),c,a ------→i g, c ∪ {k}, a l (RESNEG) ?k receives N eg(c, a) ?k j,ω,c,a∪c ------→i ⊥ j fresh (SEQN) f k,n,c,a ----→i f ′ f >x> g k,n,c,a ----→i f ′ >x> g (PARLEFT) f k,l,c,a ----→i f ′ f |g k,l,c,a ----→i f ′ |g l = ω (SEQV) f k,!v,c,a -----→i f ′ f >x> g k,h(!v),c,a -------→i (f ′ >x> g)| [v/x]g, c ∪ {k}, a l (PARRIGHT) g k,l,c,a ----→i g ′ f |g k,l,c,a ----→i f |g ′ l = ω (SEQSTOP) f k,ω,c,a ----→i ⊥ f >x> g k,ω,c,a ----→i ⊥ (PARSTOP) f k,ω,c,a ----→i f ′ g k ′ ,ω,c ′ ,a ′ ------→i g ′ f |g k,ω,c∪c ′ ,a∪a ′ ---------→i ⊥ (PRUNEN) g k,n,c,a ----→i g ′ f <x< g k,n,c,a ----→i f <x< g ′ , ∅, {k} !v (PRUNELEFT) f k,l,c,a ----→i f ′ f <x< g k,l,c,a ----→i f ′ <x< g l = ω (PRUNEV) g k,!v,c,a -----→i g ′ f <x< g k,h(!v),c,a -------→i [ v, c ∪ {k}, a l /x]f, c ∪ {k}, a ω (PRUNESTOP) g k,ω,c,a ----→i ⊥ f <x< g k,h(ω),c,a ------→i [ stop, c ∪ {k}, a l /x]f, c ∪ {k}, a ω (CAUSEYES) f k,l,c,a ----→i f ′ f, c ′ , a ′ L k,l,c∪c ′ ,a∪a ′ ∪c ′ ----------→i f ′ , c ′ , a ′ L l ∈ L (CAUSENO) f k,l,c,a ----→i f ′ f, c ′ , a ′ L k,l,c,a ----→i f ′ , c ′ , a ′ L l ∈ L
Let us comment the more relevant ones.

Let us consider the rule SEQV. When a value is published, a new instance of the right hand side expression is created. All the events produced by this new expression need the former publication to have occured before them, i.e. they are consequences of this publication. This is why the new expression is instrumented.

Even if PRUNEV is syntactically very similar to SEQV, the fact that both hand sides of the pruning operator are run in parallel makes them very different in terms of causality. In the expression (1|x) < x< 2, the second publication of 2 is a consequence of the first one, but not the publication of 1. This is why the instrumentation covers the occurrences of the newly bounded variable. However, this is not sufficient. Let us consider the program (stop < x < 2); 3. The publication of 3 must wait the end of the left hand side (i.e the publication of 2). However, this publication is useless, in the sense that no variable x can be bounded to its value. To handle this case, we add an instrumentation to the whole expression that is only triggered when the expression stops. Note that this instrumentation would not have been needed if another rule allowed to terminate the expression just by knowing that stop would never produce a value. This means that the instrumentation of a rule does not only depend on this rule, but also on the other rules of the semantics.

Finally, the rule PRUNEN is also interesting as it generates weak causality. Indeed, in the program x < s < (1 + 1|3), the left hand side can call site + and then publish 3, or publish 3 directly, but can never publish 3 and then call site +, because a publication preempts any other event. Of course, it could also wait for the answer of the site and then publish 2, which would preempt the publication of 3. This preemption relation is operated by an instrumentation that contains k as weak causes and that is triggered only in case of publication.

Concurrent executions

Like all operational semantics, this set of rules defines a transition system →i and a sequential semantics • i. In order to capture concurrency, we want to express an execution as a LAES, hence the following definition of concurrent executions.

Definition 4 (Concurrent execution). Let σ = σ 1 . . . σ n ∈ f0 i. We define the concurrent execution of σ as the tuple σ = ({σ 1 k , . . . , σ n k }, {σ 1 l , . . . , σ n l }, ≤, ր, Λ)
where for all i, j ∈ {1, . . . , n}:

• σ i k ≤ σ j k if σ i k ∈ σ j c or i = j, • σ i k ր σ j k if σ i k ∈ σ j a , • Λ(σ i k ) = σ i l .

Correctness

In this section, we prove the main result: the behavior of a program is preserved by the instrumented semantics. It is established through two properties. The first one justifies the name of the instrumented semantics and the second one proves that the instrumentation is correct, i.e. that it does not define incorrect behaviors.

Property 1 (Instrumentation).

Let

( f i) | l = {σ| l = σ[1] l ...σ[n] l |σ ∈ f i}
be the set of projections of the executions by the instrumented semantics on their labels. We have:

∀f ∈ O, ( f i) | l = f .
In other words, it is always possible to instrument a standard execution to get a concurrent execution, and conversely we can get a standard execution from an instrumented execution by a simple projection.

Theorem 1 (Correctness). The behaviors that can be observed from an execution in the instrumented semantics are correct with respect to the standard semantics:

∀f ∈ Orc, ∀σi ∈ f i, Lin(σi) ⊂ f .

Illustration

To illustrate the behavior of the instrumented semantics, we reuse the example f0 = y + z < y < ((2|3) >x> x) <z< 1. The instrumented version of the execution presented in section 2.3 is labelled by the sequence:

(k1, h(2), ∅, ∅). (k2, h(1), ∅, ∅). (k3, h(3), ∅, ∅).
(k4, h(3), {k3}, {k1, k3}). (k5, ? + (3, 1), {k2, k3, k4}, {k2, k3, k4}). (k6, !4, {k2, k3, k4, k5}, {k2, k3, k4, k5}). (k7, ω, {k2, k3, k4, k5, k6}, {k2, k3, k4, k5, k6}).

We represent the LAES of this execution thereafter. The events of the execution are depicted by their labels, that are not unique (two events are denoted h(!3)). The solid arrows (→) represent direct causality, i.e. the smallest relation that has ≤ as transitive and reflexive closure. The twisty arrows ( ) denote passive direct preemption. By definition, a is preempted by b if they resp. have a ′ and b ′ as causes and those are related by a twisty arrow.

h(!3) h(!3) h(!2) ? + (3, 1) h(!1) !4 ω
We observe that the events labelled h(!3) and h(!2), that correspond to the computation of y, are concurrent with the event labelled h(!1), and the first publication of 3 is concurrent with the publication of 2, which corresponds to our analysis. Moreover, the second event h(!3) preempts the occurrence of h(!2), which explains why h(!

3).h(!1).h(!3).h(!2).? + (3, 1).!4.ω is invalid.

There is no conflict in this execution. This is due to the fact that the instrumented semantics is based on the same set of executions as the standard semantics, in which there cannot be conflictual events.

Concurrent Semantics

Method

By introducing concurrency and preemption between events that were arbitrarily ordered by the standard semantics, the instrumented semantics heavily reduces the number of different executions. However, there may remain as many others (because of preemption) which are difficult to link in a reasoning. For this reason, the instrumented semantics is not well suited for studying race conditions for example.

Our strategy to add information about conflicts is to keep firing transitions even if they are preempted by a previous event. Thereby, it becomes possible to observe conflictual events in the same execution. The difficulty is to adapt the rest of the program so that it can also generate recursively the consequences of these conflictual events. Let us illustrate this problem on the program (1 > x > x + y) < y < 2|3. In the concurrent semantics, the publication of 2 and 3 will both occur even though they are conflictual. The variable y will then be bounded to 2 values. Note that it is not possible to duplicate the whole expression at the left hand side of the pruning operator because the publication of 1 is a single event concurrent to the computation of y.

To circumvent this difficulty, we propose a new way to bound variables. Instead of replacing the free occurrences of a x by p in f , [p//x]f adds p in a bag maintained by the free occurrences of x in f . Specifically, [p//x]x = x {p} and [p//x]xP = x P ∪{p} . If p can evolve into p ′ , x P ∪{p} can evolve into x P ∪{p ′ } .

In the standard semantics, an expression terminates when it is preempted in the pruning operator or when it produces an ω event. In the concurrent semantics, preempted expressions are not stopped and an expression may produce several conflictual ω events. It is then difficult -and not necessary -to know when an expression terminates and inactive sub-expressions cannot be removed.

It is yet still necessary to generate ω events, for example to know when the right hand side of the otherwise operator should be started. Let us consider again the program (stop <x< 1|2|3)|(stop <y< 4|5|6). In the standard semantics, the program terminates by a unique ω event when two publications are caught and ignored. In the concurrent semantics, each side of the main parallel operator produces three conflictual ω events. The global expression must produce nine conflictual ω events due to the distributivity of their causes. We introduce a new distributivity structure, that is a pair (KL, KR) of sets of pairs (e, L) where e is an event and L the set of the events that must be distributed on e. We introduce the notation e ⊲ (KL, KR) meaning that the event e happened on the left hand side. It is distributed on all of the events that have already happened on the right hand side and it gets an entry on the left hand side to the future events. A similar notation exists for the symmetric case. More formally:

e ⊗ ∅ = ∅ e ⊗ ({(e ′ , L)} ∪ K ′ ) = {(e ′ , L ∪ {e})} ∪ (e ⊗ K ′ ) e ⊲ (KL, KR) = ({(e, ∅)} ∪ KL, e ⊗ KR) (KL, KR) ⊳ e = (e ⊗ KL, {(e, ∅)} ∪ KR)
A distributivity structure is used with the parallel operator as well as the pruning operator to manage the stopping of expressions. This is done in three steps. Both sides generate ω events when they are ready; these are stored into the distributivity structure before the whole expression can generate an ω event. The two first events have a new empty label ε that is just ignored as an event.

There is no possible conflict in x < x < 1, so we want to produce the same execution as in the instrumented semantics. In particular, the right hand side of the pruning operator never produces an ω event. More generally, the consequences of a publication in the left hand side of a pruning operator can be ignored. We introduce the syntax f \ k to say that the consequences of k must be ignored in the execution of f .

Until now, we have only presented how to generate the events of all the possible executions produced by the standard semantics in a single execution. These events are instrumented in a way similar to the instrumented semantics. The only new difficulty is that the weak causes of an event e can now happen after e. We added a field e b in the transition labels and in the f, c, a, b L structure to represent weak consequences.

The concurrent semantics is defined on the set Orcic of expressions of this extended syntax:

f, g, h ∈ Expression ::= p p(p) ?k f |g f | (K L ,K R ) g f >x> g f <x< g f <x, (KL, KR)< g f ; g f ;K g D#f ⊥ f, K, K, K L f \ k D ∈ Definition ::= def y(x) = f v ∈ Orc Value ::= V D p ∈ Parameter ::= v stop x xP p, K, K, K L w ∈ Response ::= N T (v, K, K, K) T (v, K, K, K) N eg(K, K, K) n ∈ Hidden Label ::= ?V k (v) ?D h(ω) h(!v) l ∈ Label ::= !v n ω ε

Rules

The rules of the instrumented semantics are presented thereafter.

(PUBLISH) v k,!v,∅,∅,∅ ------→ic stop, {k}, ∅, ∅ l v closed k fresh (STOP) stop k,ω,∅,∅,∅ ------→ic ⊥ k fresh (DEFDECLARE) [D/y]f k,l,c,a,b -----→ic f ′ D#f k,l,c,a,b -----→ic f ′ D is def y(x) = g (VAR) p k,l,c,a,b -----→ic p ′ x P ∪{p} k,l,c,a,b -----→ic x P ∪{p ′ } (CALLSTART) P k,!v,c,a,b ------→ic P ′ P (p) k,ε,∅,∅,∅ -----→ic (P ′ (p) \ k)| v(p), c, a, b l P = v (CALLN) P k,l,c,a,b -----→ic P ′ P (p) k,l,c,a,b -----→ic P ′ (p) l is n, ω or ε (INTCALL) D(p) k,?D,∅,∅,∅ -------→ic [D/y][p/x]g, {k}, ∅, ∅ l D is def y(x) = g (EXTE) p k,ε,c,a,b -----→ic p ′ V (p) k,ε,c,a,b -----→ic V (p ′ ) (EXTCALL) p k,!v,c,a,b ------→ic p ′ V (p) k,?V k (v),c,a,b ---------→ic (V (p ′ ) \ k)| ?k, c ∪ {k}, a, b l (EXTSTOP) p k,ω,c,a,b -----→ic p ′ V (p) k,ω,c,a,b -----→ic V (p ′ ) \ k (NTRES) ?k receives N T (v, c, a, b) ?k j,!v,c,a,b -----→ic?k j fresh (OTHERSTART) f ; ∅ g k,l,c,a,b -----→ic f ′ f ; g k,l,c,a,b -----→ic f ′ (TRES) ?k receives T (v, c, a, b) ?k j,!v,c,a,b -----→ic?k| stop, c ∪ {j}, a, b l j fresh (OTHERN) f k,n,c,a,b -----→ic f ′ f ;K g k,n,c,a,b -----→ic f ′ ;K g (NEGRES)
?k receives N eg(c, a, b)

?k j,ω,c,a,b -----→ic?k j fresh (OTHERV) f k,!v,c,a,b ------→ic f ′ f ;K g k,!v,c,a,b ------→ic f ′ ; K∪{k} g (OTHERSTOP) f k,ω,c,a,b -----→ic f ′ f ;K g k,h(ω),c,a,b -------→ic f ′ ;K g| g, c ∪ {k}, a, b l c ∩ K = ∅ (OTHERHALT) f k,ω,c,a,b -----→ic f ′ f ;K g k,h(ω),c,a,b -------→ic f ′ ;K g c ∩ K = ∅ (SEQN) f k,l,c,a,b -----→ic f ′ f >x> g k,l,c,a,b -----→ic f ′ >x> g l is n or ω (PARSTART) f | (∅,∅) g k,l,c,a,b -----→ic f ′ f |g k,l,c,a,b -----→ic f ′ (SEQV) f k,!v,c,a,b ------→ic f ′ f >x> g k,h(!v),c,a,b --------→ic (f ′ >x> g)| [v/x]g, c ∪ {k}, a, b l (PARLEFTSTOP) f k,ω,c,a,b -----→ic f ′ f |K g k,ε,∅,∅,∅ -----→ic f ′ | (c,a,b)⊲K g (PRUNESTART) f <x, (∅, ∅)< g k,l,c,a,b -----→ic f ′ f <x< g k,l,c,a,b -----→ic f ′ (PARRIGHTSTOP) g k,ω,c,a,b -----→ic g ′ f |K g k,ε,∅,∅,∅ -----→ic f ′ | K⊳(c,a,b) g (PRUNELEFT) f k,l,c,a,b -----→ic f ′ f <x, K< g k,l,c,a,b -----→ic f ′ <x, K< g l = ω (PARLEFT) f k,l,c,a,b -----→ic f ′ f |K g k,l,c,a,b -----→ic f ′ |K g l = ω (PRUNELEFTSTOP) f k,ω,c,a,b -----→ic f ′ f <x, K< g k,ε,∅,∅,∅ -----→ic f ′ <x, (c, a, b) ⊲ K< g (PARMID) K k,ω,c,a,b -----→ic K ′ f |K g k,ω,c,a,b -----→ic f | K ′ g (PRUNEMID) K k,l,c,a,b -----→ic K ′ f <x, K< g k,l,c,a,b -----→ic f <x, K ′ < g (PARRIGHT) g k,l,c,a,b -----→ic g ′ f |K g k,l,c,a,b -----→ic f |K g ′ l = ω (PRUNESTOP) g k,ω,c,a,b -----→ic g ′ f <x, K< g k,h(ω),c,a,b -------→ic [ stop, c ∪ {k}, a, b l //x]f <x, K ⊳ (c, a, b)< g ′ (PRUNEN) g k,n,c,a,b -----→ic g ′ f <x, K< g k,n,c,a,b -----→ic f <x, K< g ′ , ∅, {k}, ∅ !v (PRUNEE) g k,ε,c,a,b -----→ic g ′ f <x, K< g k,ε,c,a,b -----→ic f <x, K< g ′ (PRUNEV) g k,!v,c,a,b ------→ic g ′ f <x, K< g k,h(!v),c,a,b --------→ic [ v, c ∪ {k}, a, b l //x]f <x, K ⊳ (c, a, b)< g ′ \ k, ∅, {k}, {k} !v (DISTLEFT) ({(e, {e ′ } ∪ L)} ∪ KL, KR) k,ω,ec∪e ′ c ,ea∪e ′ a ,e b ∪e ′ b ---------------→ic ({(e, L)} ∪ KL, KR) k fresh ec ∩ e ′ b = ∅ e ′ c ∩ e b = ∅ (DISTRIGHT) (KL, {(e, {e ′ } ∪ L)} ∪ KR) k,ω,ec∪e ′ c ,ea∪e ′ a ,e b ∪e ′ b ---------------→ic (KL, {(e, L)} ∪ KR) k fresh ec ∩ e ′ b = ∅ e ′ c ∩ e b = ∅ (CAUSEYES) f k,l,c,a,b -----→ic f ′ f, c ′ , a ′ , b ′ L k,l,c∪c ′ ,a∪a ′ ∪c ′ ,b∪b ′ --------------→ic f ′ , c ′ , a ′ , b ′ L l ∈ L c ∩ b ′ = ∅ c ′ ∩ b = ∅ (CAUSENO) f k,l,c,a,b -----→ic f ′ f, c ′ , a ′ , b ′ L k,l,c,a,b -----→ic f ′ , c ′ , a ′ , b ′ L l ∈ L (HIDE) f k,l,c,a,b -----→ic f ′ f \ k ′ k,l,c,a,b∪{k} --------→ic f ′ \ k ′ k ′ ∈ c
The first remark is the far bigger number of rules compared to the other semantics. For example, it requires twice as much rules to define the parallel and pruning operators. For the parallel operator, for example, only two rules have their counterparts in the standard semantics. The rule PARSTART is introduced only for adding an empty distributivity structure. The rules PARLEFTSTOP, PARRIGHTSTOP and PARMID illustrate the problem explained above. The program stop| (∅,∅) Stop needs three steps to generate an ω event. The first two, generated by PARLEFTSTOP and PARRIGHTSTOP are labelled by ε and put in the distributivity structure. Then rule PARMID is used to generate ω with the correct causes.

The same approach is used for the pruning operator, explaining the high number of rules. Let us now consider the rule PRUNEV. The right hand side is no longer destroyed when it publishes a value. Instead, a stop event is added into the distributivity structure to allow the future publications of ω, and the right hand side expression is instrumented in two ways. First, the consequences of the publication are ignored, and the future publications are considered as both weak causes and consequences of this event, to enforce a cycle in the weak causality relation, i.e. a conflict.

Surprisingly, the definition of the sequential operator is simpler in the concurrent semantics. This is due to the fusion of the rules SEQN and SEQSTOP, since nothing needs to be destroyed anymore when an ω event is observed.

Concurrent executions

The rules presented in Figure ?? define the transition system →ic and the sequential semantics • ic. To define our concurrent semantics, we also need to consider the infinite executions. The set of all the -finite and infinite -executions starting from f0 is denoted f0 ∞ ic . Definition 5 (Concurrent execution). Let σ ∈ f0 ∞ ic . We define the concurrent execution of σ as the tuple

σ = ({σ[i] k |i ≤ |σ|σ[i] l = ε}, {σ[i] l |i ≤ |σ|} \ {ε}, ≤, ր, Λ)
where for all i, j:

• σ i k ≤ σ j k if σ i k ∈ σ j c or i = j, • σ i k ր σ j k if σ i k ∈ σ j a or σ i b ∩ (σ j c ∪ {σ j k }) = ∅ • Λ(σ i k ) = σ i l .
In this semantics, we expect the LAES obtained from an execution to be complete. To this purpose, we need to consider the executions that contain all the possible events. However, there is no guaranty on the choices made by the system if several events can be fired concurrently. For example, if two Orc programs are run in parallel, it is possible for a scheduler to ignore one of them and to only execute the other. We remove the starvation cases by introducing a fairness property. Intuitively, the concurrent semantics is confluent, in the sense that if two transitions are possible from an expression, they can be drawn in any order, which gives two similar expressions. The fairness property means that if a transition is enabled at one time, it will be eventually fired.

Definition 6 (Fair execution). A fair execution is a (possibly infinite) execution σ ∈ f0 ∞

ic such that, for any prefix γ of σ, γ ∈ f0 ic, and for any event e such that γ.e ∈ f0 ic, there is an injection from γ.e to σ that preserves γ.

The set of all fair executions starting from f0 is denoted f0 ω ic .

Justification

In the remainder of this section, we limit our analysis to fair executions. Even though the technique is classic to avoid degenerate cases such as those mentioned above, we have to justify that it is not too restrictive. Property 2 claims that all finite executions can be completed into a fair execution. In other words, it is still possible to chose the event one wants to fire at any time as the other events will still be enabled afterwards. As a direct consequence, still the empty execution belongs to f0 ic, every Orc program has at least one fair execution. Another consequence is that maximal finite executions, if they do exist, are fair.

Property 2 (Fair completion). For all γ ∈ f0 ic, there is a (possibly infinite) word of events σ such that γ.σ ∈ f0 ω ic . The goal of a concurrent semantics is to define a unique object that contains all the information on the execution of a distributed program. As we have seen above, it is possible to generate a lot of fair executions by completing different finite executions. Property 3 claims that all these fair executions actually define the same object: the concurrent semantics of an Orc program.

Property 3 (fairness equivalence). Two fair executions define equivalent LAESs

: ∀f ∈ Orc, ∀σ, τ ∈ f ω ic , σ ≡ τ .
The proof of the correctness of this concurrent semantics consists of two points (1) the semantics is sound, as it does not introduce new behaviors like the instrumented semantics, and (2) the linearizations represent sequential executions of the standard semantics. It is also complete; all the behaviors are encoded in the linearizations of the concurrent semantics.

Theorem 2 (Correctness). Fair executions are sound and complete: ∀f ∈ Orc, ∀σ ∈ f ω ic , Lin(σ) = f .

Illustration

Any fair execution of the concurrent semantics of the program f0 = y + z <y< ((2|3) >x> x) <z< 1 now gives the same LAES:

h(!2) h(!2) ? + (2, 1) !3 ω ω h(!1) h(!3) h(!3) ? + (3, 1) !4 ω
The first observation is that we can obtain the LAES of the instrumented semantics (Figure 4.5) by simply removing the second h(!2) and all its consequences as well as the first ω. This is an example of LAES injection.

Let us now observe the first instance of h(!2). It is a cause of the second one and is preempted by the second instance of h(!3), so both are in relation of weak causality. By symmetry, the second instance of h(!3) is also a weak cause of those of h(!2). It follows a cycle in the weak causality relation, hence a conflict.

Proof

In this section, we prove the theorems stated above. Theorem 1 appears to be a consequence of Theorem 2, in which we use the properties concerning the instrumented semantics. This section is organized as follows: first, we define few lemmas about the links that the two semantics have with each other and how the events can be reordered in different executions. Then, the asserted properties and theorems are recalled and proved.

Lemma 1. ∀f ∈ Orc, ∀σ ∈ f , ∃σi ∈ f i, σi| l = σ.
Proof. This lemma is shown by induction on the length of the execution. What we actually prove is a bit more general, as the intermediate expressions contain more information in the instrumented than in the standard semantics.

Let fi ∈ Orci be an instrumented program. We define its projection π i s (fi) on Orcs as as the same expression in which the angle brackets are removed, i.e.

π i s ( f, c, a L) = π i s (f ) π i s (def y(x) = f ) = def y(x) = π i s (f ) π i s (p) = p π i s (p(q)) = π i s (p)(π i s (q)) π i s (?k) = ?k π i s (f |g) = π i s (f )|π i s (g) π i s (f >x> g) = π i s (f ) >x> π i s (g) π i s (f <x< g) = π i s (f ) <x< π i s (g) π i s (f ; g) = π i s (f ); π i s (g) π i s (D#f ) = π i s (D)#π i s (f ) π i s (⊥) = ⊥.
Let f0 ∈ Orc. For all n ∈ N, P (n) designates the following property: For all execution f0 --→i F1...

σ[n]

--→i Fn such that for all i, σ[i] l = li and π i s (Fi) = fi. P (0) is true because π i s (f0) = f0. Suppose P (n) and we prove P (n + 1). The induction hypothesis can be applied on the first n steps, and we have Fn such that π i s (Fn) = fn l n+1

---→ fn+1. To exhibit the last step, we also have to be more general, by proving that for all step f l -→ f ′ and all F with π i s (F ) = f , there is a step F k,l,c,a ----→i F ′ with π i s (F ′ ) = f ′ . This is shown by induction on the derivation tree of the transition.

There is a finite m ∈ N such that F

= ... G, c m l , c m ω L m ... L 2 , c 1 l , c 1 ω L 1 where G is not of the form G ′ , c l , cω L. Moreover, π i s (G) = π i s (F ) = f l -→ f ′ .
We now considere the step π i s (g) l -→ f ′ . The rule in the root of the tree can be anything different from CAUSALYES and CAUSALNO. It can have zero, one or two premises of the form h l ′ -→ h ′ . Moreover, there is a rule with the same name in the instrumented semantics, with the same number of premises, of the form H k,l ′ ,c,a ----→ H ′ , with π i s (H) = h. By induction, the premise can be satisfied with π i s (H ′ ) = h ′ , and we can apply the rule, which gives

G k,l,c ′ ,a ′ -----→ G ′ with G ′ = f ′ .
Finally, we can apply m times the rule CAUSALYES or CAUSALNO depending on l, and get

F k,l,c ′′ ,a ′′ ------→ F ′ = ... G, c m l , c m ω L m ... L 2 , c 1 l , c 1 ω L 1 , with F ′ = G ′ = f ′ .
This proves P (n + 1), so P (n) for all n.

Lemma 2. ∀f ∈ Orc, ∀σi ∈ f i, ∃σic ∈ f ic, σi < σic. Moreover, for all i, σic[i] b = ∅ and σic| l = σi| l Proof. The proof for this lemma is very similar to the previous one. It consist of an induction on the length of the execution where each intermediate expression has some property, namely the projection of the expressions of the concurrent semantics are those of the instrumented semantics (π ic i (F ) = f ) and the expressions of the concurrent semantics are non-conflictual, which means that they were obtained from an execution where no conflict was observed.

Here is the full definition of π ic i :

π ic i (stop) = stop π ic i (V ) = V π ic i (def y(x) = f ) = def y(x) = π ic i (f ) π ic i ( p, c, a, b L) = π ic i (p), c, a L π ic i (x) = x π ic i (xp) = π ic i (p) π ic i (xp 1 ,p 2 ,...) = ⊥ π ic i ( f, c, a, b L) = π ic i (f ), c, a L π ic i (f \ k) = ⊥ π ic i (p(p ′ )) = π ic i (p)(π ic i (p ′ )) if π ic i (p) = ⊥ = π ic i (p ′ ) ⊥ otherwise π ic i (?k) = ?k π ic i (⊥) = ⊥ π ic i (D#f ) = π ic i (D)#π ic i (f ) π ic i (f |g) = π ic i (f )|π ic i (g) if π ic i (p) = ⊥ = π ic i (p ′ ) ⊥ otherwise π ic i (f |K 0 g) = π ic i (f |g) π ic i (f |e⊲K 0 g) = stop, ec, ea ω |π ic i (g) if π ic i (g) = ⊥ π ic i (f |K 0 ⊳eg) = π ic i (f )| stop, ec, ea ω if π ic i (f ) = ⊥ π ic i (f | e⊲K 0 ⊳e ′ g) = stop, ec ∪ e ′ c , ea ∪ e ′ a ω π ic i (f |K g) = ⊥ otherwise π ic i (f >x> g) = π ic i (f ) >x> g if π ic i (f ) = ⊥ ⊥ otherwise π ic i (f <x< g) = π ic i (f ) <x< π ic i (g) if π ic i (p) = ⊥ = π ic i (p ′ ) ⊥ otherwise π ic i (f <x, K0< g) = π ic i (f <x< g) π ic i (f <x, e ⊲ K0< g) = stop, ec, ea ω <x< π ic i (g) if π ic i (f ) = ⊥ π ic i (f <x, K0 ⊳ e< g) = π ic i (f ) <x< stop, ec, ea ω if π ic i (g) = ⊥ π ic i (f <x, e ⊲ K0 ⊳ e ′ < g) = stop, ec ∪ e ′ c , ea ∪ e ′ a ω π ic i (f <x, K< g) = ⊥ otherwise π ic i (f ; g) = π ic i (f ); π ic i (g) π ic i (f ; ∅ g) = π ic i (g) if π ic i (f ) = ⊥ π ic i (f ); π ic i (g) otherwise π ic i (f ;K g) = π ic i (f )
We now give the full definition of non-conflictuality. A parameter p is non-conflictual if it is of the form

• def y(x) = f , where f is non-conflictual • p, c, a, b L where p is non-conflictual • V , stop, x • x {p} where p is non-conflictual A program F is non-conflictual if it is of the form • ?k, ⊥,
• p, P (p) where p and P are non-conflictual

• f \ k, f, c, a, ∅ L where f is non-conflictual • f |g, f |K 0 g, f >x> g, f <x< g, f <x, K0 < g, f ; g, f ;K g, def y(x) = f #g, where f and g are non-conflictual • f |K 3 g, f <x, K3< g where π ic i (f ) = π ic i (g) = ⊥ • f | K ⊳ 1 g, where f is non-conflictual and π ic i (g) = ⊥
The last definition is a notation: we denote F k,l,c,a,∅ -----→ n ic F ′ if there are F1, ..., Fn and identifiers k1, ..., kn such that F

k 1 ,ǫ,∅,∅,∅ ------→i F1... kn,ǫ,∅,∅,∅ ------→i Fn k,l,c,a,∅ -----→ic F ′ . We write F k,l,c,a,∅ -----→ ⋆ ic F ′ if this is true for some n.
Let f0 be an Orc program and σi ∈ f0 i. Let f1, ..., fn such that f0

σ i [1]
---→i f1...fn-1

σ i [n]
---→i fn. We prove that there are F0, ..., Fn such that for all i, Fi is non-conflictual and π ic i (Fi) ≡ fi, and f0 = F0

σ i [1] ---→ ⋆ ic F1...Fn-1 σ i [n] ---→ ⋆ ic
Fn by induction on n.

If n = 0, we just have to take F0 = f0, that is trivially non-conflictual and f0 = π ic i (f0). We suppose the property true for all σi of length n, and suppose σi is of length n + 1. By induction, we know that there is Fn non-conflictual such that π ic i (Fn) ≡ fn. As they are equivalent, π ic i (Fn)

σ i [n+1]
-----→i g ≡ fn+1. We must now prove that there is Fn+1 non-conflictual such that π ic i (Fn+1) ≡ gfn+1 and Fn

σ i [n+1] k ,σ i [n+1] l ,σ i [n+1]c,σ i [n+1]a,∅ -------------------------→ ⋆ ic Fn+1.
To this extend, we prove the property P: for all f , f ′ , (k, l, c, a) such that f k,l,c,a ----→i f ′ , for all non-conflictual F such that

π ic i (F ) = f , there is a non-conflictual F ′ such that π ic i (F ′ ) ≡ f ′ and F k,l,c,a,∅ -----→ n ic F ′ .
We prove P by induction on the derivation tree of the step, i.e. we prove this for the axioms, and supposing P for the premises of the other rules (induction hypothesis H1), we prove it for these rules. We can remark that the base cases are exactely those in which no hypothesis is made, so we do not separate this cases.

Let f k,l,c,a ----→i f ′ , that was generated by rule R and F non-conflictual such that π ic i (F ) = f . The proof is made by induction on the syntax of F . Similarly, we have the induction hypothesis H2: if G is a non-conflictual sub-expression of F and

π ic i (G) k ′ ,l ′ ,c ′ ,a ′
------→i g ′ , then there is G ′ non-conflictual with

π ic i (G ′ ) ≡ g ′ such that G k ′ ,l ′ ,c ′ ,a ′ ,∅ -------→ m i G ′ .
Here are listed the possible cases for F :

stop (idem for v) : f = stop, so R is STOP, the transition is stop k,ω,∅,∅
----→i ⊥, and we can apply rule STOP on F , so stop

k,ω,∅,∅,∅ ------→ic ⊥ where F ′ = ⊥ is non-conflictual and π ic i (⊥) = ⊥ = f ′ . xp: f = π ic i (p), so we have π ic i (p) k,l,c,a
----→i p ′ and by H1,

p k,l,c,a,∅ -----→ n ic P ′ with π ic i (P ′ ) ≡ p ′ . It is possible to apply rule VAR n + 1 times, so xp k,l,c,a ----→ n ic x P ′ . P (p): f = π ic i (P )(π ic i (P )), R
F ′ = (P ′ (p) \ k ′ )| (∅,K R ) [D/y][p/x]g, {k}, ∅, ∅ l , c, a, ∅ l , with π ic i (F ′ ) = [D/y][p/x]g, {k}, ∅ l , c, a l ≡ [D/y][p/x]g, c ∪ {k}, a l = f ′ .
?k : f =?k, so R can only be one of NTRES, TRES or NEGRES, and we can apply the same rule in the concurrent semantics.

G, c, a, ∅ L: g is non-conflictual and

π ic i (F ) = π ic i (G), c, a L. Using H1, we have G k,ω,c ′ ,a ′ ,∅
-------→ n ic and we can apply rules CAUSEYES or CAUSENO n + 1 times depending on l and L. G| (∅,∅) H: as F is non-conflictual, G and H are different from ⊥, and R was one of: -------→ n ic H ′ . We can apply rule PARLEFT m times, rule PARLEFTSTOP once, rule PARRIGHT n times, rule PARRIGHTSTOP once and rule PARMID once, to get

PARLEFT (idem for PARRIGHT):

π ic i (G) k,l,c,a ----→ g ′ . By H1, we have G k,l,c,a,∅ -----→ n ic G ′ , so we can apply rule PARLEFT n + 1 times, which gives G| (∅,∅) H k,l,c,a,∅ -----→ n i G ′ | (∅,∅) H. PARSTOP: π ic i (G) k,ω,c,a ----→ ⊥ and π ic i (H) k,ω,c ′ ,a ′ -----→ ⊥. By H1, we have G k,ω,c,a,∅ ------→ m ic G ′ and H k,ω,c ′ ,a ′ ,∅
F k,ω,c∪c ′ ,a∪a ′ ,∅ ----------→ m+n+2 ic F ′ = G ′ | ({((a,c,∅),∅)},{((a ′ ,c ′ ,∅),∅)}) H ′ , with π ic i (F ′ ) ≡ ⊥. G| (K L ,K R ) H:
The other cases are either conflictual, or π ic i (F ) = ⊥. G <x, (∅, ∅)< H: as F is non-conflictual, G and H are different from ⊥, and R is one of:

PRUNELEFT: π ic i (G) k,l,c,a ----→ g ′ . By H1, G k,l,c,a,∅ -----→ n ic G ′ , so we can apply rule PRUNELEFT n + 1 times, which gives G <x, (∅, ∅)< H k,l,c,a,∅ -----→ n i G ′ <x, (∅, ∅)< H. PRUNEN: π ic i (H) k,n,c,a ----→i h ′ . By H1, H k,n,c,a,∅ ------→ n ic
H ′ , so we can apply PRUNEE n times and PRUNEN once, so

F k,l,c,a,∅ -----→ n ic G <x, (∅, ∅)< H ′ , ∅, {k}, ∅ . PRUNEV: π ic i (H) k,!v,c,a -----→i h ′ . By H1, H k,!v,c,a,∅ ------→ n ic
H ′ , so we can apply PRUNEE n times and PRUNEV once, which gives

F k,l,c,a,∅ -----→ n i F ′ = [x| v, c ∪ {k}, a, b l /x]G < x, (∅, {((c, a, b), ∅)})< H ′ , ∅, {k}, {k} !v . F ′ is non-conflictual and π ic i (F ′ ) = π ic i ([x| v, c ∪ {k}, a, b l /x]G) = [v/x]π ic i (G) ≡ f ′ . PRUNESTOP: π ic i (H) k,ω,c,a
----→i ⊥. By H1, we have H k,ω,c,a,∅ ------→ n ic H ′ , so we can apply PRUNEE n times and PRUNESTOP once, which gives

F k,h(ω),c,a,∅ --------→ n i F ′ = [x| stop, c ∪ {k}, a, b l /x]G < x, (∅, {((c, a, b), ∅)}) < H ′ with π ic i (H ′ ) ≡ ⊥. F ′ is non-conflictual and π ic i (F ′ ) = π ic i ([x| stop, c ∪ {k}, a, b l /x]G) = [stop/x]π ic i (G) ≡ f ′ .
G <x, (KL, KR)< H: the only other cases that is not conflictual, where

π ic i (F ) = ⊥ is π ic i (H) = ⊥, KR = {(c, a, b), ∅}. We have π ic i (F ) = π ic i (G), so by H2, G k,l,c,a,∅ -----→ n ic G ′ . We can use rule PRUNELEFT n + 1 times, which gives G <x, (KL, KR)< H k,l,c,a,∅ -----→ n i G ′ <x, (KL, KR)< H.
G; ∅ H: G and H are non-conflictual, and R is one of:

OTHERN: We have π ic i (G) k,n,c,a ----→i π ic i (G ′ ) with G ′ non-conflictual. We can apply OTHERN, so F k,n,c,a,∅ ------→i G ′ ; ∅ H = F ′ . OTHERV: We have π ic i (G) k,!v,c,a -----→i π ic i (G ′ ) with G ′ non-conflictual. We can apply OTHERV, so F k,!v,c,a,∅ ------→i G ′ ; {k} H = F ′ , with F ′ non-conflictual and π ic i (F ′ ) = π ic i (G ′ ) ≡ f ′ . OTHERSTOP: We have π ic i (G) k,ω,c,a ----→i π ic i (G ′ ) = ⊥ with G ′ non-conflictual. We can apply OTHERSTOP, so F k,!v,c,a,∅ ------→i G ′ ; ∅ H| H, c ∪ {k}, a, b l = F ′ , with F ′ non-conflictual and π ic i (F ′ ) = π ic i (H), c ∪ {k}, a l ≡ f ′ . G;K H: π ic i (G) = f k,l,c,a ----→ f ′ = π ic i (G ′ ).
We can apply one of the rules depending on l. If l = ω, there was a publication, that is a cause of ω, so c ∩ K = ∅. We can build F ′ as an application of OTHERN, OTHERV or OTHERHALT, and in all these cases, G >x> H: as a step is possible, π ic i (G) = ⊥ and f = π ic i (G) >x> H. R can be the following rules:

π ic i (F ′ ) = π ic i (G ′ ) is non-conflictual. G|H, resp G <x<
SEQN: by H1, G k,l,c,a,∅ -----→ n i G ′ , so we can apply SEQN n + 1 times, which gives G > x > H k,l,c,a,∅ -----→ n i G ′ >x> H. SEQV: by H1, G k,!v,c,a,∅ ------→ n i G ′ ,
so we can apply SEQN n times and SEQV once, which gives

G > x > H k,!v,c,a,∅ ------→ n i G ′ > x > H| [v/x]g, c ∪ {k}, a, ∅ l and π ic i (G ′ > x > H| [v/x]g, c ∪ {k}, a, ∅ l ) = π ic i (G ′ ) >x> H| [v/x]g, c ∪ {k}, a l ≡ f ′ . SEQSTOP: by H1, G k,ω,c,a,∅ ------→ n i G ′ , with π ic i (G ′ ) = ⊥, so we can apply SEQN n + 1 times, which gives G >x> H k,ω,c,a,∅ ------→ n ic G ′ >x> H. As π ic i (G ′ ) = ⊥, π ic i (G ′ >x> H) ≡ ⊥ = f ′ . def y(x) = G#H: we have f is def y(x) = π ic i (G)#π ic i (H), so R is DEFDECLARE. By H1, [D/y]H k,l,c,a,∅ -----→ n ic H ′ . We can apply DEFDECLARE, so D#H k,l,c,a,∅ -----→ n ic H ′ .
Let us denotate the execution we just built by σic. We have σic ∈ f0 ic and σi = σic. Lemma 3. Let f ∈ Orc and σ ∈ f ic such that for all i, σ[i] b = ∅. Let σ| l the word constituted of the labels of σ different from ε. We have σ| l ∈ f . Proof. This proof is very similar to the previous ones, and we have similar notions of projection π ic s and non-conflictuality. We define the projection π ic s (f ) as :

π ic s (stop) = stop π ic s (V ) = V π ic s (def y(x) = f ) = def y(x) = π ic s (f ) π ic s ( p, c, a, b L) = π ic s (p) π ic s (x) = x π ic s (xp) = π ic s (p) π ic s (xp 1 ,p 2 ,...) = ⊥ π ic s ( f, c, a, b L) = π ic s (f ) π ic s (f \ k) = ⊥ π ic s (p(p ′ )) = π ic s (p)(π ic s (p ′ )) if π ic s (p) = ⊥ = π ic s (p ′ ) ⊥ otherwise π ic s (⊥) = ⊥ π ic s (D#f ) = π ic s (D)#π ic s (f ) π ic s (f |g) = π ic s (f )|π ic s (g) if π ic s (p) = ⊥ = π ic s (p ′ ) ⊥ otherwise π ic s (f |K 0 g) = π ic s (f |g) π ic s (f |e⊲K 0 g) = stop, ec, ea ω |π ic s (g) if π ic s (g) = ⊥ π ic s (f |K 0 ⊳eg) = π ic s (f )| stop, ec, ea ω if π ic s (f ) = ⊥ π ic s (f | e⊲K 0 ⊳e ′ g) = stop, ec ∪ e ′ c , ea ∪ e ′ a ω π ic s (f |K g) = ⊥ otherwise π ic s (f >x> g) = π ic s (f ) >x> g if π ic s (f ) = ⊥ ⊥ otherwise π ic s (f <x< g) = π ic s (f ) <x< π ic s (g) if π ic s (p) = ⊥ = π ic s (p ′ ) ⊥ otherwise π ic s (f <x, K0< g) = π ic s (f <x< g) π ic s (f <x, e ⊲ K0< g) = stop, ec, ea ω <x< π ic s (g) if π ic s (f ) = ⊥ π ic s (f <x, K0 ⊳ e< g) = π ic s (f ) <x< stop, ec, ea ω if π ic s (g) = ⊥ π ic s (f <x, e ⊲ K0 ⊳ e ′ < g) = stop, ec ∪ e ′ c , ea ∪ e ′ a ω π ic s (f <x, K< g) = ⊥ otherwise π ic s (f ; g) = π ic s (f ); π ic s (g) π ic s (f ; ∅ g) = π ic s (g) if π ic s (f ) = ⊥ π ic s (f ); π ic s (g) otherwise π ic s (f ;K g) = π ic s (f )
π ic s (?k) is not defined and the proof will not be done for NTRES, TRES and NEGRES, which are correct by hypothesis.

We now give the full definition of non-conflictuality. The non-conflictual parameters are of the form:

• def y(x) = f , where f is non-conflictual • p, c, a, b L where p is non-conflictual • V , stop, x • x {p} where p is non-conflictual A program F is non-conflictual if it is of the form: • ?k, ⊥,
• p, P (p) where p and P are non-conflictual

• f \ k, f, c, a, ∅ L where f is non-conflictual • f |g, f |K 0 g, f >x> g, f <x< g, f <x, K0 < g, f ; g, f ;K g, def y(x) = f #g, where f and g are non-conflictual • f |K 3 g, f <x, K3< g where π ic i (f ) = π ic i (g) = ⊥ • f | K ⊳ 1 g
, where f is non-conflictual and π ic i (g) = ⊥

We will now show by induction on n that for all execution f = f0

σ[1]
--→ic f1...

σ[n]

--→ic fn such that

for all i, σ[i] b = ∅, fi is non-conflictual and pi ic s (fi) = pi ic s (fi-1) if σ[i] l = ε and pi ic s (fi-1) σ[i] l ---→ pi ic s (fi) otherwise (denoted pi ic s (fi-1) σ[i] l ==⇒ pi ic s (fi)).
It is true for n = 0 as f ∈ Orc. Suppose the property holds for a given n. This is a corollary of the following property: for all F e -→ic F ′ such that e b = ∅ and F is non-conflictual, pi ic s (F )

e l = ⇒ pi ic s (F ′
). This is done by induction on the derivation tree of the step. The rule that generated it can be:

PUBLISH (idem for STOP, INTCALL) : we have

v k,!v,∅,∅,∅ ------→ic stop, {k}, ∅, ∅ and v !v -→ stop with stop, {k}, ∅, ∅ non-conflictual. DEFDECLARE : suppose D#f k,l,c,a,∅ -----→ic f ′ where D#f is non-conflictual. [D/y]f is non- conflictual and [D/y]f k,l,c,a,∅ -----→ic f ′ . By induction, f ′ is non-conflictual and π ic s ([D/y]f ) = [π ic s (D)/y]π ic s (f ) l -→ π ic s (f ′
), so we can apply rule DEFDECLARE, and

π ic s (D#f ) = π ic s (D)#π ic s (f ) l -→ π ic s (f ′ ). VAR : F is not conflictual, so F = x {p} and π ic s (F ) = π ic s (p). By induction, π ic s (p) l -→ π ic s (p ′ ). More- over, p ′ is non-conflictual so x {p ′ } is non-conflictual.
CALLSTART : we have P k,!v,c,a,∅ ------→ic P ′ , and P is non-conflictual, so P = x ... v,c ′ ,a ′ ,∅ L ... L ′ . We have that g = (P

′ (p) \ k)| v(p), c,
(p ′ ) = stop. g = (V (p ′ ) \ k)| ?k, c ∪ {k}, a, b l is non-conflictual and EXTCALL can be applied on π ic s (V (p)) = V (v), so π ic s (V (p)) ?V k (v)
----→?k = π ic s (g). OTHERSTART: π ic s (f ; ∅ g) = π ic s (f ; g), so the result is true by induction. OTHERN : f is non-conflictual and π ic s (f ) = ⊥. By induction, we have π ic s (f ) n -→ π ic s (f ′ ) and f ′ non-conflictual. If K = ∅, it is the point, otherwise, we can apply OTHERN, so π ic s (f ;K g) = π ic s (f ); π ic s (g)

n -→ π ic s (f ′ ); π ic s (g) = π ic s (f ′ ;K g).
OTHERV : f is non-conflictual and π ic s (f ) = ⊥. By induction, we have π ic s (f )

!v
-→ π ic s (f ′ ) and f ′ non-conflictual. If K = ∅, it is the point, otherwise, we can apply OTHERV, so π ic s (f ;K g) = π ic s (f ); π ic s (g)

!v -→ π ic s (f ′ ) = π ic s (f ′ ; K∪{k} g). OTHERSTOP : f is non-conflictual and π ic s (f ) = ⊥. By induction, π ic s (f ) ω -→ ⊥ = π ic s (f ′ ) and f ′ is non-conflictual. If K ∩ c = ∅, we can apply rule OTHERSTOP, so π ic s (f ; ∅ g) = π ic s (f ); π ic s (g) h(ω) ---→ π ic s (g) = π ic s ((f ′ ; g \ k)| g, c ∪ {k}, a, b l ).
Otherwise, π ic s (f ;K g) = π ic s (f ), so the result is true. OTHERHALT : K = ∅, so π ic s (f ;K g) = π ic s (f ), and the result is true by induction.

SEQN : f > x > g is non-conflictual, so is f . By induction, we have

π ic s (f ) l -→ π ic s (f ′ ) and f ′ non- conflictual. If l = n, we can apply rule SEQN, so π ic s (f >x> g) = π ic s (f ) >x> g l -→ π ic s (f ′ ) >x> g = π ic
s (f ′ >x> g) and f ′ >x> g non-conflictual. Otherwise, l = ω, and π ic s (f ′ ) = ⊥. We can apply rule SEQSTOP, and

π ic s (f >x> g) = π ic s (f ) >x> g ω -→ ⊥ = π ic s (f ′ >x> g). SEQV : f > x > g is non-conflictual, so is f . By induction, we have π ic s (f ) !v -→ π ic s (f ′ ) and f ′ non- conflictual. We can apply rule SEQV, so π ic s (f > x > g) = π ic s (f ) > x > g v -→ π ic s (f ′ ) > x > g|[v/x]g = π ic s (f ′ >x> g| [v/x]g, c ∪ {k}, a, b l ). PARSTART: π ic s (f | (∅,∅) g) = π ic s (f |g)
, so the result is true by induction. PARLEFTSTOP (same reasoning for PARRIGHTSTOP) : f is non-conflictual, so by induction,

π ic s (f ) ω -→ π ic s (f ′ ) and we have π ic s (f ) ≡ stop and π ic s (f ′ ) = ⊥. f ′ | (c,a,b)⊲K g is non-conflictual, and π ic s (f ′ | (c,a,b)⊲K g) = stop|π ic s (g) ≡ π ic s (f )|π ic s (g) = π ic s (f |g).
PARLEFT (same reasoning for PARRIGHT) : f is non-conflictual, so by induction, π ic s (f )

l -→ π ic s (f ′ ). Moreover, KL = ∅. If π ic s (g) = ⊥, we have directly π ic s (f |K g) = π ic s (f ) l -→ π ic s (f ′ ) = π ic s (f ′ |K g).
Otherwise, we can apply rule PARLEFT, and

π ic s (f |K g) = l -→ π ic s (f ′ |K g). PARMID : as K k,ω,c,a,b -----→ic K ′ , π ic s (f |K g) = stop, and as f |K g is non-conflictual, K ′ is inert, so π ic s (f | K ′ g) = ⊥.
We can apply rule STOP, which gives

π ic s (f |K g) = stop ω -→ ⊥ = π ic s (f | K ′ g). PRUNESTART : π ic s (f <x, (∅, ∅)< g) = π ic s (f <x< g)
, so the result is true by induction.

PRUNELEFT : f is non-conflictual, so by induction, π ic s (f )

l -→ π ic s (f ′ ). Moreover, KL = ∅. If KR = ∅, we have directly π ic s (f <x, K < g) = π ic s (f ) l -→ π ic s (f ′ ) = π ic s (f ′ <x, K < g).
Otherwise, we can apply rule PRUNELEFT, and π ic s (f <x, K< g) = l -→ π ic s (f ′ <x, K< g). PRUNELEFTSTOP : f is non-conflictual, so by induction, π ic s (f ) ω -→ π ic s (f ′ ) and we have π ic s (f ) ≡ stop and π ic s (f ′ ) = ⊥. f ′ <x, (c, a, b) ⊲ K < g is non-conflictual, and π ic s (f ′ <x, (c, a, b) ⊲ K < g) = stop <x< π ic s (g) ≡ π ic s (f ) <x< π ic s (g) = π ic s (f <x, K< g).

PRUNEMID : as

K k,ω,c,a,b
-----→ic K ′ , π ic s (f < x, K < g) = stop, and as f |K g is non-conflictual, K ′ is inert, so π ic s (f < x, K ′ < g) = ⊥. We can apply rule STOP, which gives π ic s (f < x, K < g) = stop ω -→ ⊥ = π ic s (f <x, K ′ < g). PRUNESTOP : g is non-conflictual, so by induction, π ic s (g) ω -→ π ic s (g ′ ) and we have π ic s (g) ≡ stop and -→ π ic s (f <x, K< g ′ ).

π ic s (g ′ ) = ⊥. h = [x| stop, c ∪ {k}, a, b l /x]f <x, K ⊳ (c, a, b)< g ′ is non-conflictual,
PRUNEV : g is non-conflictual, so by induction, π ic s (g)

!v -→ π ic s (g ′ ) with π ic s (g) = ⊥. Let h = [x| v, c ∪ {k}, a, b l /x]f < x, K ⊳ (c, a, b) < g ′ , ∅, {k}, {k} !v . By rule PRUNEV, we have π ic s (f < x, K < g) = π ic s (f ) <x< π ic s (g) h(!v) ---→ [v/x]π ic s (f ) = π ic s (h)
. DISTLEFT, DISTRIGHT : the left hand side of the rule does not match a valid program

CAUSEYES, CAUSENO : f, c, a, b l is non-conflictual, so is f . By induction, π ic s ( f, c, a, b l ) = π ic s (f ) l -→ π ic s (f ′ ) = π ic s ( f ′ , c, a, b l ) and π ic s ( f ′ , c, a, b l ) is non-conflictual. HIDE : σ[n + 1] b = ∅.
Finally, we were able to create an execution labelled by σ| l dependless of the size of σ, so σ| l ∈ f0 .

Property 1 (Instrumentation

). ∀f ∈ O, ( f i) | l = f
Proof. Let σi ∈ f i. By lemmas 2 and 3, there is σic ∈ f ic such that σi| l = σic| l ∈ f . Then

( f i) | l ⊂ f Let σ ∈ f . By lemma 1, there is σi ∈ f i such that σi| l = σ. Then f ⊂ ( f i) | l . Lemma 4. Let γabδ ∈ f0 ω ic such that a ≤ b. There are a ′ , b ′ with a ′ k = a k and b ′ k = b k
such that the identity on k defines an injection from γabδ to γb ′ a ′ δ.

Proof. Let us consider two consecutive causally-independant steps

f k 1 ,l 1 ,c 1 ,a 1 ,b 1 ---------→ic f ′ 1 k ′ 1 ,l ′ 1 ,c ′ 1 ,a ′ 1 ,b ′ 1 ---------→ic f ′′ 1 .
We prove that there are programs f ′′ 2 and f ′ 2 and sets of identifiers a2, b2, a

′ 2 , b ′ 2 such that f k ′ 1 ,l ′ 1 ,c ′ 1 ,a ′ 2 ,b ′ 2 ---------→ic f ′ 2 k 1 ,l 1 ,c 1 ,a 2 ,b 2 ---------→ic f ′′ 2 and f ′′ 2 is equivalent to f ′′ 1 in which a1, b1, a ′ 1 , b ′ 1 have been replaced respectively by a2, b2, a ′ 2 , b ′ 2 , with: a2, b2, a ′ 2 , b ′ 2 =        a1, b1, a ′ 1 , b ′ 1 if k ∈ a ′ ∪ b ′ a1, b1 ∪ {k ′ }, a ′ 1 \ {k}, b ′ 1 if k ∈ a ′ \ b ′ a1 ∪ {k ′ }, b1, a ′ 1 , b ′ 1 \ {k} if k ∈ b ′ \ a ′ a1 ∪ {k ′ }, b1 ∪ {k ′ }, a ′ 1 \ {k}, b ′ 1 \ {k} if k ∈ b ′ ∪ a ′
This is shown by induction on the derivation tree of the first step, and there is no other choice than the complete enumeration of the possible pairs of following steps. The items of first level are the possibilities for the rule of the first step, and those of second level are the possibilities for the second step.

PUBLISH, STOP, INTCALL :

there is no causaly-independant possible second step.

DEFDECLARE f = D#g k 1 ,l 1 ,c 1 ,a 1 ,b 1 ---------→ic f ′ 1 k ′ 1 ,l ′ 1 ,c ′ 1 ,a ′ 1 ,b ′ 1 ---------→ic f ′′ 1 . We have [D/y]g k 1 ,l 1 ,c 1 ,a 1 ,b 1 ---------→ic f ′ 1 k ′ 1 ,l ′ 1 ,c ′ 1 ,a ′ 1 ,b ′ 1 ---------→ic f ′′ 1 . By induction, [D/y]g k ′ 1 ,l ′ 1 ,c ′ 1 ,a ′ 2 ,b ′ PARLEFT (idem for PARRIGHT, PARLEFTSTOP, PARRIGHTSTOP, PARMID) f = g|K h k,c,a,b ----→ f ′ 1 = g ′ |K h
PARRIGHT (idem PARMID, PARRIGHTSTOP) We can apply PARRIGHT on the premise of the second step to build the first step and then PARLEFT on the premise of the first step. PARLEFT (idem PARLEFTSTOP) We can applyinduction on the left hand side and apply PAR-LEFT twice.

PRUNESTART By induction, g <x, (∅, ∅)< h

k ′ 1 ,l ′ 1 ,c ′ 1 ,a ′ 2 ,b ′ 2 ---------→ic f ′ 2 k 1 ,l 1 ,c 1 ,a 2 ,b 2 ---------→ic f ′′ 2 ,
and we can apply PRUNESTART on the first step.

PRUNELEFT (idem for PRUNELEFTSTOP

) f = g <x, K<, h k,c,a,b ----→ f ′ 1 = g ′ <x, K< h PRUNELEFT (idem for PRUNELEFTSTOP)
We can apply the induction on the premises and PRUNELEFT twice.

PRUNEN (idem for PRUNEMID, PRUNEE)

We have g

′ < x, K < h k ′ ,c ′ ,a ′ ,b ′ ------→ f ′′ 1 = g ′ < x, K < h ′ , ∅, {k ′ }, ∅ !v .
The same rules can be applied in reverse order, which gives f = g <x, K< , h

k ′ ,c ′ ,a ′ ,b ′ ------→ f ′ 2 = g <x, K< h ′ , ∅, {k ′ }, ∅ !v k,c,a,b ----→ f ′′ 2 = f ′′ 1 .
PRUNEV: τ (T, T ′ ) = PRUNEV(CAUSEYES(HIDE(τ (p(T ), p(T ′ ))))). HIDE is possible because k2 ∈ c1.

Anything else: τ (T, T ′ ) = R ′ (CAUSENO(HIDE(τ (p(T ), p(T ′ ))))).

DISTLEFT, DISTRIGHT: f = K, so R ′ is also DISTLEFT or DISTRIGHT. These rules just remove different elements in the structure, so they can be applied in any order.

CAUSEYES, CAUSENO: R ′ is CAUSEYES or CAUSENO and τ (T, T ′ ) = R ′ (τ (p(T ), p(T ′ ))).

HIDE: f = g \ k ′′ , so R ′ = HIDE and τ (T, T ′ ) = R ′ (τ (p(T ), p(T ′ ))).
Property 2 (Fair completion). For all γ ∈ f ic , there is a (possibly infinite) word of events σ such that γ.σ ∈ f ω ic .

Proof. The idea of this proof is to use a first-in-first-out list of possible steps in which we push the transitions as soon as they become available. Once γ has been executed, we fire the steps in the order where they are poped from the list. As the list remains finite, every event will eventually be fired. We build a sequence (τn, fn, Ln) n∈N such that, for all n:

• τn ∈ f ic. Informally, it is the prefixe of size n of the fair execution we are building. We expect, for all n ≥ 1, τn-1 = τn[1...n] and τ |γ| = γ;

• fn ∈ Orcic. It is the expression obtained after τn, i.e. for all n, f = f0

τ 1 [1]
---→ f1...

τn[n]

---→ fn.

• Ln is an ordered list of transitions (i.e. there derivation trees) that contains exactly the set of transitions that are valid in the instrumented semantics and that have fn as the left-hand side of the conclusion.

The sequence is built by induction on n. We initialize as follows: τ0 is the empty execution, f0 = f and L0 contains all the transitions starting from f . Suppose we have built (τn, fn, Ln) for a given n.

We chose a transition T in Ln as:

• if n < |γ|, we have f = f0 γ[1]
--→ f1...

γ[n]

--→ fn and there is g such that fn

γ[n+1]
----→ g. As all the transitions available from fn, fn

γ[n+1]
----→ g is contained into Ln, and it defines T .

• if Ln is not empty, we take the first transition for T

• otherwise, τn is fair. We will consider this case later.

The conclusion of T is fn e -→ g. We define fn+1 = g and τn+1 = e. Ln+1 is built as follows:

• L ′ n is Ln in which T was removed. • L ′′ n is a list of the same size as L ′ n . For all i, we have τn.T ∈ f ic and τn.L ′ n [i] ∈ f ic . By lemma 5, there is an event T ′ such that γ.T.T ′ ∈ f ic and γ.L ′ n [i] < γ.T.T ′ . We pose L ′′ n [i] = T ′ . • L ′′′ n can be any ordered list that contains all the transitions that can be fired from fn+1 and are absent from L ′′ n . • Ln+1 is the concatenation of L ′′ n and L ′′′ n . This defines the sequence by induction.

There are two cases:

• if there is n ≥ |γ| such that Ln is empty, we pose τ = τn;

• otherwise, for all n ∈ N, we pose τ

[n] = τn[n].
In both cases, γ is a prefix of τ , and τ is fair, since for all n and all transition T that can be fired after τn, τ [1...n] = τn ∈ f and T is in Ln at a finite position p, so it will be fired after at most |σ|n + p steps.

Property 3 (Equivalence of fair executions). Two fair executions define equivalent LAES:

∀f ∈ Orc, ∀σ, τ ∈ f ω ic , σ ≡ τ .
Proof. Let σ, τ ∈ f0 ω ic . We prove the following property (P (n)) by induction on n: for all n, there is γ n ∈ f0 ω ic such that id k : k → k defines an isomorphism in both directions between γ n and τ (i.e. γ n ≡ τ ) and id n i : σ

[i] k → γ n [i] k defines an injection from σ[1...n] to γ n . Moreover, if n > 0, γ n-1 [1...n -1] = γ n [1...n -1].
P (0) is true with γ 0 = τ . We suppose now P (n) for a given n, and we prove P (n + 1).

The only restriction on the identifiers is that they must be unique in the execution. In particular, there is no link between the choice of the rules and of the identifier in a transition. Let δ n be the same execution as γ n , but where the identifiers appear in the same order as in σ. Let us compare δ n ,j) [i] k ≤ γ max(i,j) γ max(i,j) [j] k , so τ [i] k ≤τ τ [j] k ; similarly, if σ[i] k րσ σ[j] k , γ max(i,j) [i] k ր γ max(i,j) γ max(i,j) [j] k , so

τ [i] k րτ τ [j] k .
Finally, f defines an injection from σ to τ and σ < τ . By symmetry, τ < σ, and τ ≡ σ.

Theorem 2 (Correctness). The fair executions are sound and complete:

∀f ∈ Orc, ∀σ ∈ f ω ic , Lin(σ) = f .

Proof. Let f ∈ Orc and σ ∈ f ω ic . Let σo ∈ f0 o. By lemma 1, there is σi ∈ f0 i such that σo ∈ Lin(σi). By lemma 2 and property 2, there is σic ∈ f0 ω ic such that σi < σic. We have σo ∈ Lin(σic). Moreover by property 3, σ ≡ σic so σo ∈ Lin(σic). This proves that f o ⊂ Lin(σ).

We now prove the converse. Let w = Λ(k 0 )...Λ(k n ) ∈ Lin(σ). We define L as the set of finite executions according to the concurrent semantics that contain w in there linearizations:

L = {γ ∈ f ic|γ < σ ∧ w ∈ Lin(γ)}.
Let γ ∈ L and f be the injection from γ to σ. We define:

D(γ) = |{i < i ′ |∃j > j ′ , f (γ[i] k ) = k j ∧ f (γ[i ′ ] k ) = k j ′ }| + i| ∃j,f (γ[i] k )=k j |{i ′ |∃j, f (γ[i ′ ] k ) = k j }| +|γ| -n.
As w is finite, there is a finite prefixe γ of σ that contains all the events of identifiers k 0 , ..., k n . We have σ0 ∈ L, so L = ∅, and we can consider δ ∈ L for which D(δ) is minimal, and we suppose (ad absurdum) that D(δ) > 0. f is the injection from δ to σ and m = |δ|.

1. Suppose that for all j, f (δ[m] k ) = k j . δ[1, ..., m -1] ∈ L and D(δ[1, ..., m -1]) = D(δ) -1 which is in contradiction with the fact that D(δ) is minimal.

2. Otherwise, if m = n, there is i such that δ[i] k has no antecedant by f . Let i0 be the biggest such i. i0 = m so δ[i0 + 1] k is defined and has an antecedant k j by f . As w is a linearization, the causal history of k j is contained into {k 1 , ..., k n }, so δ

[i0] k ≤ δ[i0 + 1] k .
We can apply lemma 4, which gives δ ′ ∈ f0 ic with δ ′ ≡ δ. We have δ ′ ∈ L and D(δ ′ ) = D(δ)-1, which is impossible by definition of δ.

3. Otherwise, m = n and f is bijective, so

U = {i < i ′ |∃j > j ′ , f (γ[i] k ) = k j ∧ f (γ[i ′ ] k ) = k j ′ } = ∅ Let (i, i ′ ) ∈ U such that i ′ -i is minimal. Suppose i ′ -i > 1.
There is i ′′ such that i < i ′′ < i. As f is bijective, there is j ′′ such that f (γ[i ′′ ] k ) = k j ′′ and either (i, i ′′ ) ∈ U or (i ′′ , i ′ ) ∈ U , which is impossible as i ′i is minimal. So i ′ = i + 1, and there are j > j ′ such that f (γ[i] k ) = k j and f (σ

[i + 1] k ) = k j ′ .
As w is a linearization, we have ¬(k j ր k j ′ ), so k j ≤ k j ′ , and by injection, σ[i] k ≤ σ[i + 1] k . We can apply lemma 4, which gives σ ′ ∈ f0 ic with σ ′ ≡ σ. We have σ ′ ∈ L and D(σ ′ ) = D(σ) -1, which is impossible by definition of σ.

All three cases are impossible, so D(δ) = 0. We have m = n and for all i ≤ n, f (δ i ) = k i . As w ∈ Lin(δ), we can conclude by lemma 3 that w ∈ f0 . This proves, Lin(σ) ⊂ f o.

Theorem 1 (Correctness). The behaviors that can be observed from an execution in the instrumented semantics are correct with respect to the standard semantics:

∀f ∈ O, ∀σi ∈ f i, Lin(σi) ⊂ f

Proof. Let σi ∈ f0 i. By lemma 2, and property 2, there is a fair execution σic ∈ f0 ic such that σi < σic. Let w ∈ Lin(σi). We have w ∈ Lin(σic), so by theorem 2, w ∈ f0 .

Discussion and Conclusion

This paper addresses the problem of the formal definition of an operational semantics for a distributed programming language. We based our work on a case study: the Orc language, as it is expressive enough to easily generate many situations found in distributed systems, such as causality, concurrency, preemption and conflict, and remains simple enough to be tractable in a formal work as this one. Our contribution consists of two new semantics for the Orc language. An instrumentation of the standard semantics that extracts as much information as possible from a unique execution and a full concurrent semantics that sums up all the possible behaviors of a program. Debugging is a direct application of our work, as it requires root causes analysis, replay and even race detection. From the user point of view, a debugger should give the possibility to execute a program, (which is the role of the instrumented semantics), but should also give the possibility to explore more than one possibility in conflictual choices (here, the concurrent semantics becomes necessary). Lemma 2 gives an early response. As the semantics are compatible, it is possible to let the instrumented semantics drive the execution of the concurrent semantics, and to introduce conflicts only when the programmers want to point them out explicitly.

Beyond the Orc language, we think that this work presents a general approach that can be used for other non-deterministic languages with concurrency operators.

Causality often operates through values and variables. It might be possible to use this remark to track causality by a program transformation. This could be useful to improve the efficiency of an implementation.

  f, g, h ∈ Expression::= p p(p) ?k f |g f >x> g f <x< g f ; g D#f ⊥ D ∈ Definition ::= def y(x) = f v ∈ Orc Value ::= V D p ∈ Parameter ::= v stop x w ∈ Response ::= N T (v) T (v) N eg n ∈ Hidden Label ::

  of the standard semantics, there is an execution F0 σ[START_REF] Bruni | Translating Orc features into Petri nets and the Join calculus[END_REF]

  can be one of these rules: STOPCALL: by H1, P k,ω,c,a,∅ ------→ n ic P ′ , so we can apply rule CALLN n + 1 times in the concurrent semantics. INTCALL (idem for EXTCALL and EXTSTOP): F = P (p ′ ). If P = D, we can apply rule INTCALL in the instrumented semantics. Otherwise, by H1, P k,!D,c,a,∅ ------→ic P ′ , so we can apply rule CALLN n times, then rule CALLSTART once and rule INTCALL as a premise of CAUSEYES, PARRIGHT or PARRIGHTSTOP and PARSTART, which gives F k,?D,c,a,∅ ------→ n+1 ic

  H, resp G; H: the previous reasonings gives us the properties for G| (∅,∅) H, G < x, (∅, ∅)< H and G; ∅ H. If we also apply rule PARSTART, resp PRUNESTART, resp OTHERSTART on the first step, we have the property for G|H, G <x< H and G; H.

  [1...n] and σ[1...n]. Let i ∈ {1, ..., n}. By construction of γ n , we have δ n [i] k = σ[i] k . Moreover, since id n i is an injection from σ[1...n] to γ n , we have δ n [i] l = σ[i] l and as the fields c, a and b are contained into{δ n [1] k , ..., δ n [i -1] k }, (δ n [i]c, δ n [i]a, δ n [i] b ) = (σ[i]c, σ[i]a, σ[i] b ). Thus, δ n [1...n] = σ[1...n]. Moreover, δ n is fair, so σ[1...n + 1] < δ n , where f is the injection. Let p such that δ[p] k = f (σ[n + 1] k ). As σ[1...n] ∈ f0 ic, for all n < i < p, δ n [i] k ≤ δ n [p] k , so γ n [i] k ≤ γ n [p] k .We can apply lemma 4 pn -1 times on γ n at positions p -1, p -2, ..., n + 1 to move γ n [p] k at position n + 1 in γ n+1 , id k is an isomorphism between γ n+1 and τ and id n+1 i is an injection from σ[1...n + 1] to γ n+1 . Moreover, γ n [1...n] = γ n+1 [1...n], which is P (n + 1).This proves P (n) for all n. For all n, we definef (σ[n] k ) = γ n [n] k . Let n < p.By unicity of the identifier in a sequence, we havef (σ[n] k ) = γ n [n] k = γ p [n] k = γ p [p] k = f (σ[p] k ), so f is injective. Moreover,for all n, we have Λσ(σ[n] k ) = Λγn (γ n [n] k ) = Λτ (τ [n] k ); for all i and j, if σ[i] k ≤σ σ[j] k , γ max(i

  if e happens before e ′ in all executions; • e is a weak cause of e ′ , if there is no execution in which e happens after e ′ ; • e and e ′ are concurrent, denoted e||e ′ , if they can occur in either order. Formally, e||e ′ if neither e ր e ′ nor e ′ ր e. • e is preempted by e ′ , denoted e e ′ , if e ′ can occur independently from e, but after that, e cannot occur anymore. Formally, e e ′ if e ր e ′ and e ≤ e ′ ,

  ′ , and P is non-conflictual, so P is either stop or x ... stop,c ′ ,a ′ ,∅ L ... L ′ and π ic s (P (p)) = stop(π ic s (p)). Moreover, P ′ is stop or x ... ⊥,c ′ ,a ′ ,∅ L ... L ′ so P ′ (p) is non-conflictual. We can apply axiom STOPCALL, and π ic s (P (p))

		a, b l is non-conflictual and π ic s (P (p)) = π ic s (g) = v(π ic s (p)).
	CALLSTOP: we have P	k,ω,c,a,∅ ------→ic P ω -→ ⊥ = π ic s (P ′ (p)).
	CALLE: by induction, P ′ is not conflictual and π ic s (P ′ ) = π ic s (P ), so P ′ (p) is not conflictual and π ic s (P ′ (p)) = π ic s (P (p)).
	EXTE: by induction, p ′ is not conflictual and π ic s (p ′ ) = π ic s (p), so V (p ′ ) is not conflictual and π ic s (V (p ′ )) = π ic s (V (p)).
	EXTCALL (same reasoning for EXTSTOP): we have π ic s (p) = v and by induction, p ′ is non-conflictual
	and π ic s

  ′ ). Moreover, KR = ∅. Otherwise, we can apply rule PRUNEN, and π ic s (f <x, K< g) =

			and by rule
	PRUNESTOP, we have π ic s (f <x, K< g) ≡ π ic s (f ) <x< stop	h(ω) ---→ [stop/x]π ic s (f ) = π ic s (h).
	PRUNEN : g is non-conflictual, so by induction, π ic s (g)	n -→ π ic s (g l

PRUNEV (idem for PRUNESTOP) the premise of the second step is indepentant of the premise of the first step, so it can be applied, and we have

We also know that g

-------→ g ′ . All the transitions that are possible from g are also possible from

]g, so we can apply PRUNELEFT on it for the second step.

′ < h PRUNEMID we can apply the induction on the premises and apply PRUNEMID twice. anything else the steps are totally independant.

DISTLEFT, DISTRIGHT : the two steps concern different elements, so they can occure in any order.

HIDE (idem for CAUSEYES, CAUSENO) HIDE :

We can apply the induction for the premise and apply the same rules.

The full lemma is just a corollary.

Lemma 5. Let γ ∈ f ic and two events e1 and e2 such that γ.e1, γ.e2 ∈ f ic .

There is an event e ′ 2 such that γ.e1.e ′ 2 ∈ f ic and γ.e2 < γ.e1.e ′ 2 .

Proof. This lemma is a kind of converse of the previous one. What we realy prove is that for any f ∈ Orcic and any transitions f

We introduce a few notations:

• if T is the derivation tree of a transition, p(T ) is the premise if it has a unique one, p1(T ) and p2(T ) are respectively the left hand side and right hand side premises if they exist.

• if the derivation trees of the steps k1, c1, a1, b1 and k2, c2, a2, b2 are denoted T1 and T2, the deriva-

and whom root is generated by rule R. τ (T, T ′ ) = R(T ′′ ) means that there is a transition τ (T, T ′ ) that the root is generated by R, has f ′ 1 as left hand side and T ′′ as premise. Similarly, we write R(T, T ′ ) if R has two premises.

Just like above, we prove the result by induction on the derivation tree of (k1, c1, a1, b1). We should differentiate the base cases and the induction cases. However, by sake of clarity, we give a unique list of possibilities. The first-level items are for rules that can generate (k1, c1, a1, b1) and the second-level items are the remaining possibilities for the other steps. Of course, we never use the induction hypothesis on case bases. Let T and T ′ be the transitions of the steps f