Detecting Local Channels in Distributed Poly/ML

Paul Steckler^{∗}

Keywords: static analysis, escape analysis, concurrency, communication, locality, ML

Abstract

Distributed Poly/ML is a variation on Standard ML that includes primitives for creating threads and for inter-thread communication. Threads may be spawned on remote machines. Values are sent from one thread to another over dynamically-created channels. A channel is considered local iff all its uses take place on the processor on which it was created. We present a constraint-based static analysis that detects local channels. Using a tree replacement technique, we show that constraint solutions may be maintained as invariants at each transition step in a concurrent operational semantics. Relying on such invariants, we prove the soundness of the analysis with respect to the operational semantics.

1 Introduction

Distributed Poly/ML (DP/ML) is an implementation of a variation on Standard ML [8] that provides primitives for creating threads and for communications between threads. An overview of the implementation is described in [5]. A child thread may run on the same processor as its parent thread, or on a different processor. Values are sent between threads over dynamically-created channels. Channels are themselves values and so may be passed from one thread to another. Channels may also be contained within data structures passed between threads. Therefore, a channel may be used in a thread running on a processor different than the one where it was created.

If it can be determined statically that a channel will be used only for communications on the processor on which it was created, the compiler run-time system may be able to make useful assumptions about the channel’s memory usage. DP/ML’s run-time system includes a shared distributed memory manager that is responsible for maintaining coherence among the possibly several memory spaces used by a program [6]. Creating a channel allocates a memory block on a machine. If it can be determined that a channel will only be used for communications on the same processor on which the channel was created, the run-time system can treat the channel’s memory as purely local. Another possibly beneficial consequence of locality is that all communications on a local channel are between thread pairs on a single processor. Such communications do not involve a network, so the run-time sytem may be able to use a superior protocol.

∗LFCS, Department of Computer Science, The King’s Buildings, University of Edinburgh, Edinburgh EH9 3JZ, Scotland, steck@dcs.ed.ac.uk.

One goal of this work was to see if constraint-based static analysis methods could be adapted to the concurrent setting. In [19], [16], and [15], for instance, we used constraint-based analyses to support provably-correct code transformations for closure conversion and thunk creation. In those analyses, our proofs were of partial correctness: if untransformed programs terminated, then so did their transforms, with comparable results. Also, the reduction behavior of the languages used in thoses analyses was specified by big-step, “natural”-style operational semantics. By contrast, for DP/ML, we are interested in non-terminating computations: Imagine a thread that acts as a server for other, client threads. A big-step operational semantics is too inaccurate a specification of concurrency. Therefore, we specify the behavior of programs using an interleaving small-step operational semantics. As much as the analysis itself, we regard our proof method to show the soundness of the analysis as the contribution here. The proof method essentially consists of showing that once we have a solution to the specified constraints, we can easily produce solutions at each transition step.

2 Detecting locality

A channel is local iff it is used only on the processor on which it is created. Like many static analysis problems, it is undecidable whether a given channel is local. So our approach is to determine which channels may be non-local; the remaining channels are certain to be local. In this section, we consider the situations which require us to consider channels non-local. These considerations will be reflected in the constraints.

Channels are created using the channel() primitive. A thread sends a value to another thread using the send() primitive, which takes two arguments, a channel and a value. A receiving thread uses the receive() primitive, which takes a channel argument. Threads are created using either the fork() primitive, which runs the child thread on the same processor as its parent, or the rfork() primitive, which runs the child thread on a specified processor. Both fork() and rfork() take a function argument, whose body becomes the child thread. rfork() takes an additional processor argument that specifies where the child thread is to run.

Our analysis answers two questions about channels:

1. can channels escape from the processors where they are created?

2. for channels that may escape, can they reach a send() or receive() after escaping?

The analysis considers a channel as non-local if it may escape from the processor where it is created and subsequently reach a send() or receive().

In the language we consider, there are three ways in which a channel may escape from one processor to another. One way is if the channel is a subterm of an rfork()’d function:

     let x = channel()

in rfork(ρ, fn y. ... x ...)

where the let is sugared function application. Since the rfork()’d function may run on a different processor than its parent, we conclude that the channel x may escape.

A channel is a value that may be sent over channels. Therefore, another way in which a channel may escape is if the channel itself is sent between threads running on different processors. Suppose on processor ρ, we have just:

     send(k′,k)

and on processor ρ′ we again have

     receive(k′)

where k and k′ are channel constants. Since k may be sent over k′, we conclude that k may escape from one processor to another.

A third way in which a channel may escape is if it is a proper subterm of a value sent between threads running on different processors. Suppose on processor ρ, we have the thread:

send(k′,fn x. ...k ...)

and on processor ρ′, we have:

     receive(k′)

where again k and k′ are channel constants. Since k is contained in a function that may be transmitted over the channel k′, k may escape.

These examples show how our analysis deals with question (1) above. Why do we require the additional information asked by question (2)? Simply determining whether a channel may escape from one processor to another would not capture the locality of a channel that escapes from the processor where it is created, but does not reach any communications primitive after escaping. Also, since our escape analysis is necessarily approximate, we may judge that a channel may escape, when in fact it does not. Adding the reaching information may give better results than an escape analysis alone. It may be possible to increase accuracy further by other techniques, such as folding of conditionals with known test results.

Since channels are created dynamically, our actual interest is not in which channels are local, but which occurrences of the channel() primitive produce only local channels. With that information, we can change such occurrences of channel() to occurrences of a different primitive local-channel() in DP/ML intermediate code.

3 The Language

Taking a similar tack to [4] for a partial evaluator, our analysis is performed on the untyped intermediate language of the DP/ML compiler. A simplified and idealized version of terms in that language is given by the grammar:

M ::= x | true | false | c | ρ | k | unit | fn^{ℓ} x.M | MM |

          if M then M else M | channel^{ℓ}() | fork(M) | rfork(M,M) |
          send(M,M) | receive(M)

where

• c ranges over an infinite set of constants,

• ρ ranges over a finite set of processors,

• k ranges over an infinite set of channels, and

• unit is a constant corresponding to the ML type of the same name.

Let Λ_{DP/ML} be the set of terms described by this grammar.

We will refer to terms of the form fn^{ℓ} x.M as functions. Each function occurrence and each occurrence of channel() has an associated label drawn from some alphabet, which we need not specify. We use ℓ, ℓ′, and so on as metavariables which range over the set of labels. Initially, each label in a Λ_{DP/ML} term should be distinct. Transitions in the operational semantics produce new Λ_{DP/ML} terms whose labels need not be distinct.

4 Operational Semantics

In describing the operational semantics for Λ_{DP/ML}, we use the following definitions:

Definitions 1

1. A thread is a Λ_{DP/ML} term.

2. Let TI be an infinite set of thread identifiers. We use p and q as typical elements of TI .

3. A thread map Π is a finite map from thread identifiers to pairs of processors and threads.

For a thread map Π, we may write proc_{Π}(p) for the processor associated with the thread identifier p in Π. Likewise, we may write thread_{Π}(p) for the Λ_{DP/ML} term associated with p in Π. If a thread map is indicated by the context, we may drop the subscripts and write just proc(p) and thread(p).

Our semantics is divided into a two-level execution hierarchy. We give transition relations for each level. The first level describes sequential evaluation; the corresponding one-step transition relation is ⟶_{seq} . The second level describes transitions within a thread map; the one-step transition relation for this level is

⟶_{con} .

Following [14] and [10], sequential evaluation consists of reduction within a context. Our evaluation contexts are given by the grammar:

C ::= | C M | M C |

                   if C then M else M | fork(C) |
                   rfork(C,M) | rfork(M,C) |
                   send(C,M) | send(M,C) | receive(C)

where M ranges over Λ_{DP/ML} terms. We write C[M] to indicate that the hole in the context C is filled by M. Note that a context hole cannot occur in the body of a function. Our evaluation contexts do not require a definite evaluation order. Of course, DP/ML uses a specific evaluation order, but that is not significant for our analysis.

In the sequential semantics in Figure 1, the metavariable M ranges over arbitrary Λ_{DP/ML} terms. The metavariable V is used to indicate values, which are functions and all constants.

In Figure 2, we give the rules for thread map evaluation. Within each rule, K is a set of channels.

Let ⟶^{+}_{con} be the transitive closure, and let ⟶^{∗}_{con} be the reflexive and transitive closure of ⟶_{con} . Also, Π ⟶^{n}_{con} Π′′ iff Π ⟶^{∗}_{con} Π′ in n steps.

β:

C[(fn^{ℓ} x.M) V] ⟶_{seq} C[M[V/x]]

cond-true:

C[ if true then M else N] ⟶_{seq} C[M] cond-false: C[ if false then M else N] ⟶_{seq} C[N]

Figure 1: Sequential evaluation within contexts

seq:

\frac{C[M] ⟶_{seq} C[M′]}{K, Π[ p : ρ, C[M]] ⟶_{con} K, Π[ p : ρ, C[M′]]}

channel:

\frac{k ∉ K}{K, Π[ p : ρ, C[channel^{ℓ}()]] ⟶_{con} K ∪ \{k\}, Π[ p : ρ, C[k]]}

fork:

\frac{q ∉ Dom(Π) ∪ \{p\}}{K, Π[ p : ρ, C[fork(fn^{ℓ} x.M)]] ⟶_{con} K, Π[ p : ρ, C[unit]][ q : ρ, M[unit/x]]}

rfork:

\frac{q ∉ Dom(Π) ∪ \{p\}}{K, Π[ p : ρ, C[rfork(ρ′,fn^{ℓ} x.M)]] ⟶_{con} K, Π[ p : ρ, C[unit]][ q : ρ′, M[unit/x]]}

comm:

\frac{k ∈ K}{K, Π[ p : ρ, C[send(k,V)]][ q : ρ′, C′[receive(k)]] ⟶_{con} K, Π[ p : ρ, C[unit]][ q : ρ′, C′[V]]}

Figure 2: Thread map evaluation

5 Occurrences indices; labels

Each source program occurrence has an associated string called an occurrence index. Occurrence indices are finite strings over the alphabet:

\{ \begin{matrix}bv, body, rator, rand, test, then, else, \\ ffun, rfpor, rffun, schan, sbody, rchan \end{matrix} \}

For an occurrence of a subterm within a term M, an occurrence index describes the path from the root of the parse tree for M, to the occurrence of the subterm. We may wish to refer to the occurrence indices of distinct terms in a thread map. To distinguish indices from distinct threads, we may qualify the indices by thread identifiers. For instance, we may write p : i for the occurrence i from the term with thread identifier p.

We may think of an occurrence index as a pointer into a parse tree. A dereferencing operator [[−]] may be applied to recover the underlying term: if M is a term with occurrence index i, then [[i]] = M.

For an occurrence of a function or channel() with index i, we write lab(i) to indicate the label associated with the occurrence.

The grammar of Λ_{DP/ML} terms specifies several kinds of expressions. We may use predicates such as Var, Fun, Fork, and so on to test which production in the grammar produced an occurrence of a term. The predicate Const is true given an argument that is an ordinary constant, boolean constant, processor constant, channel constant, or the unit constant.

Note that [[−]], lab(−), and the predicates just mentioned implicitly depend on particular thread maps. It should be clear from context which thread map is meant when we use these constructs.

6 Propositions

Here we describe the annotations that are associated with program occurrences:

• A flow ϕ is a finite set of function labels. For a given occurrence, its flow is a conservative estimate of the labels of functions to which that occurrence might evaluate. Our flow annotations give us what is usually referred to as a closure analysis.

• A channel set κ is a finite set of channel() labels. For an occurrence i, its channel set is a conservative estimate of the labels of channel() occurrences that produce the channels to which i may evaluate.

• An escape flag θ is an element of the set {escape^{−}, escape^{±}}, with the ordering escape^{−} ≤ escape^{±}. escape^{±} suggests that an occurrence may escape from one processor to another, while escape^{−} indicates that an occurrence certainly does not go from one processor to another.

• A reachability flag, σ, is an element of the set {reach^{−}, reach^{±}}, with the ordering reach^{−} ≤ reach^{±}. reach^{±} suggests that a value may reach the channel-part of a send() or receive() primitive, while reach^{−} suggests that a value does not reach such a channel-part.

• A linearity flag ν is an element of the set {1, ∞}, ordered 1 ≤ ∞. A linearity flag of ∞ suggests that an occurrence may be duplicated by a function application; 1 indicates that an occurrence is not duplicated.

• A locality flag ω is an element of the set {local^{+}, local^{±}}, with the ordering local^{+} ≤ local^{±}. local^{+}, when associated with an occurrence of channel(), suggests that it produces only local channels. local^{±} suggests that the primitive may produce non-local channels.

These descriptions are meant to guide the reader’s intuition. An exact semantics of the annotations will be given later, in section 11.

In a source program, each occurrence i will be annotated with a pair (P^{→}_{i}, P^{←}_{i}), which we may indicate as P_{i}. We call such a pair a proposition.

The P^{→}_{i} component of a proposition is a forwards proposition, and consists of a pair (ϕ_{i}, κ_{i}). The set of forwards propositions is partially-ordered. Say that (ϕ, κ) ≤ (ϕ′, κ′) iff ϕ ⊆ ϕ′ and κ ⊆ κ′. We define a join operation on forwards propositions: Let (ϕ, κ) ⊔ (ϕ′, κ′) = (ϕ ∪ ϕ′, κ ∪ κ′).

The P^{←}_{i} component of a proposition is a backwards proposition, and consists of a 4-tuple (θ_{i}, σ_{i}, ν_{i}, ω_{i}). The set of backwards propositions is partially-ordered. Say that (θ, σ, ν, ω) ≤ (θ′, σ′, ν′, ω′) iff θ ≤ θ′, σ ≤ σ′, ν ≤ ν′, and ω ≤ ω′. We can also define a join operation on backwards propositions. Let (θ, σ, ν, ω)⊔(θ′, σ′, ν′, ω′) = (max(θ, θ′), max(σ, σ′), max(ν, ν′), max(ω, ω′)).

By referring to the partial orders on forwards and backwards propositions, we can partially order the set of propositions. Let P = (P^{→}, P^{←}) and P′ = (P^{→}′, P^{←}′). Say that P ≤ P′ iff P^{→} ≤ P^{→}′ and P^{←} ≤ P^{←}′. This partial order allows us to identify a least element in the set of propositions.

We also want another order relation on propositions. Again let P = (P^{→}, P^{←}) and P′ = (P^{→}′, P^{←}′). Say that P ≤^{→} P′ iff P^{→} ≤ P^{→}′ and P^{←}′ ≤ P^{←}. Intuitively, this relation reflects the notion that the forwards propositions, which consist of ϕ’s and κ’s, track the forward flow of function and channel labels, while the backwards propositions, consisting of θ, σ, ν, and ω annotations, track information which gets propagated from program points back to occurrences which may reach those points.

7 Annotation maps

An annotation map Γ associates occurrence indices with propositions. Such a map associates each node i in the parse tree of a thread with a proposition P_{i}. The domain of an annotation map is prefix-closed, since each occurrence in a parse tree has an annotation. Hence, we may consider an annotation map itself as a tree.

When needed, we may write P_{i}^{Γ} for Γ(i) to indicate that it is a particular annotation map Γ that associates the occurrence i with the proposition P_{i}. We may also write P_{p:i} for the proposition for the occurrence i in the thread with thread identifier p. Similarly, we may write ϕ_{p:i} for the flow component of P_{p:i}, and so on for the other components of propositions.

For an occurrence index i, the tree Γ/i is the subtree of Γ rooted at i with domain {j | i.j ∈ Dom(Γ)}, so that for all j in the domain of the subtree, (Γ/i)(j) = Γ(i.j).

7.1 Local consistency

In Figure 3, we give constraints on the annotations in annotation maps. These constraints are presented as local conditions for each occurrence in a Λ_{DP/ML} term. We refer to certain constraints on the annotations of functions as “escape constraints”; those are presented in Figure 4.

Let us define some terminology used in the constraints. We say that an annotation map for a term M is remote-expectant at an occurrence j in M iff

∀k, m such that Send(k) ∧ Receive(m), κ_{k.schan} ∩ κ_{m.rchan} ≠ ∅, and exactly one of k and m is a subterm of j,

\begin{cases}θ_{k.sbody} = escape^{±}, \\ σ_{m} = reach^{±} ⇒ ω_{m} = local^{±} \end{cases}

where the quantifier ranges over occurrences in M. We require remote-expectancy for functions that may be rfork()’d or may otherwise escape from one processor to another. The idea is that the value sent from a send() to a receive(), where one of the communications partners is a subterm of a possibly escaping function, may be sent from one processor to another. Therefore, we tag the body of the send() with a θ-annotation of escape^{±}, which gets propagated back to any value that may be sent by that send(). Since a sent value may be a channel, in case the sent value may reach a send() or receive(), we tag the receive() partner as non-local, which gets propagated back to such a sent channel.

Similarly, an annotation map for a term M is nonlinear-expectant at an occurrence j in M iff

ν_{j} = ∞ ⇒

∀k, m such that Send(k) ∧ Receive(m), κ_{k.schan} ∩ κ_{m.rchan} ≠ ∅, and both k and m are subterms of j,

\begin{cases}θ_{k.sbody} = escape^{±}, \\ σ_{m} = reach^{±} ⇒ ω_{m} = local^{±} \end{cases}

where the quantifier ranges over occurrences in M. We also require nonlinearexpectancy of functions that may be rfork()’d or may otherwise escape. If we have possibly-communicating send() and receive() subterms of a function that may escape, and that function may be duplicated, values may sent between duplicates running on different processors. Therefore, we tag the send() and receive() in anticipation of that possibility.

The constraints may be solved by iteration. We may start off by annotating each occurrence with a proposition that is ≤-minimal. Suppose we have a constraint P ≤^{→} P′ that is not satisfied. Since our analysis mixes forwards and backwards components, we may need to adjust both P and P′ by propagating forwards information from P to P′ and backwards information from P′ to P. More specifically, suppose P = (P^{→}, P^{←}), P′ = (P^{→}′, P^{←}′). If P ≰^{→} P′, then we may enforce the constraint by setting P = (P^{→}, P^{←} ⊔P^{←}′) and setting P′ = (P^{→} ⊔P^{→}′, P^{←}′). Propagating information in this way moves both P and P′ up the ≤ order, not the ≤^{→} order. Termination is assured because the height of any chain is finite.

An annotation map gives the annotations of a particular term. An annotation map is locally consistent for a term M iff the constraints in Figure 3 are satisfied at all the occurrence indices of M. The universal quantified indices specified in the constraints range over the indices in M. Explicitly, an annotation map may have extra elements in its domain that are not indices in a given term; those extra elements are irrelevant when considering the local consistency of the annotation map for that term.

Since channels in DP/ML programs are created dynamically, they do not occur in source programs. Therefore, the DP/ML compiler does not have to solve the constraint on annotations of channel subterms of functions given in Figure 3.

A useful result about local consistency is:

Lemma 1 Let Γ be a locally consistent annotation for a term M. Then for any i that is the index of a subterm of M, Γ/i is locally consistent for the subterm rooted at i.

Var(i) ⇒ if j is the binding occurrence for i, then P_{j} ≤^{→} P_{i}

Channel(i) ⇒ lab(i) ∈ κ_{i}

Fun(i) ⇒ lab(i) ∈ ϕ_{i}, no. of free occurrences of [[i.bv]] in [[i.body]] > 1 ⇒ ν_{i.bv} = ∞, θ_{i} = escape^{±} ⇒ escape constraints hold at i ν_{i} = ∞ ⇒ for all free variable and function occurrences i.q, ν_{i.q} = ∞

App(i) ⇒ ∀j such that lab(j) ∈ ϕ_{i.rator}, \begin{cases}P_{i.rand} ≤^{→} P_{j.bv}, \\ P_{j.body} ≤^{→} P_{i} \end{cases}

Cond(i) ⇒ P_{i.then}, P_{i.else} ≤^{→} P_{i}

RFork(i) ⇒ ∀j such that lab(j) ∈ ϕ_{i.rffun}, escape constraints hold at j

Send(i) ⇒ σ_{i.schan} = reach^{±}

Receive(i) ⇒ σ_{i.rchan} = reach^{±}, ∀j such that Send(j) ∧ κ_{j.schan} ∩ κ_{i.rchan} ≠ ∅, P_{j.sbody} ≤^{→} P_{i}

Figure 3: Local consistency constraints

∀j such that i.j is a free variable occurrence in i, θ_{i.j} = escape^{±} σ_{i.j} = reach^{±} ⇒ ω_{i.j} = local^{±} ∀m such that ChanConst(i.m), σ_{i.m} = reach^{±} ⇒ ω_{i.m} = local^{±}

Γ is remote-expectant at i, Γ is nonlinear-expectant at i

Figure 4: Escape constraints for a function i Proof. By the local consistency of Γ/i at each node of the subtree.

The preceding lemma is slightly less obvious than it sounds. The essential observation is that there are possibly fewer constraints on the annotations for the subterm of M than for M itself. For instance, suppose that in the subtree rooted at i contains an application with index j. By the local consistency conditions, we have constraints involving all k such that lab(k) ∈ ϕ_{j.rator}. The same application appears in M, with index, say, m. The comparable constraint involves all k′ such that lab(k′) ∈ ϕ_{m.rator}. Note that the sets of k’s and k′’s are not necessarily the same, because the term and its subterm may be different. But any function occurrence with a given label in the subterm is also in M. Therefore, if the constraints at m were satisfied in Γ for M, the constraints at j are also satisfied in Γ/i for the subterm. Similar considerations arise when considering the other constraints involving a universal quantifier, such as those for rfork()’s and receive()’s. Also, taking a subtree may take a variable out of the lexical scope of its binder. That has the effect of removing the constraint on the variable’s annotation.

Similarly:

Lemma 2 Let Γ be a locally consistent annotation map for a term M. Suppose we substitute a constant, other than a channel constant (an ordinary constant, boolean constant, processor constant, or the unit constant) for a subterm N of M. Then Γ is locally consistent for the substituted term.

Proof. By considering the constraints for each occurrence in the substituted term.

Observe that there are no constraints on the kinds of constants we have indicated, so that a substitution does not introduce any new constraints. Any constraints that applied to occurrences in the replaced subterm no longer apply in the substituted term.

Corollary Suppose Γ is a locally consistent annotation map for a term M with zero or more free occurrences of a variable x. Let c be any constant other than a channel constant. Then Γ is locally consistent for M[c/x].

We can handle channel constants, too, by making a slight restriction:

Lemma 3 Let Γ be a locally consistent annotation map for a term M. Suppose we substitute a channel constant for a subterm N of M, where N is not a subterm of any function body. Then Γ is locally consistent for the substituted term.

Proof. By considering the constraints for each occurrence in the substituted term.

Observe that the only possible constraints on constants are for channel constants in function bodies, so that a substitution as we have indicated does not introduce any new constraints.

A thread map associates thread identifiers with threads, that is, with Λ_{DP/ML} terms. Therefore, for a given thread map, we have a family of annotation maps indexed by the domain of the thread map. We write Γ_{p} to indicate the annotation map for the thread associated with thread identifier p. We say that such a family of annotation maps is locally consistent for a thread map Π iff for each thread identifier p in the domain of Π, the annotation map Γ_{p} is locally consistent for thread_{Π}(p).

7.2 Communicative consistency

Local consistency imposes constraints on the annotations of a particular term. Since data may be sent between threads, we use the additional notion of communicative consistency to account for those data flows. The communicative consistency constraints for annotations of occurrences in thread maps are given in Figure 5.

Most of the communicative consistency constraints are essentially the same as local consistency constraints, except that they hold between occurrences from different threads. As an example, we need the “communicative analogue” of remoteexpectancy. Say that a family of annotation maps G is distributed remote-expectant at an occurrence p : j iff

∀k, m such that Send(k) ∧ Receive(m), κ_{k.schan} ∩ κ_{m.rchan} ≠ ∅ and exactly one of k and m is a subterm of p : j,

\begin{cases}θ_{k.sbody} = escape^{±}, \\ σ_{m} = reach^{±} ⇒ ω_{m} = local^{±} \end{cases}

This definition is essentially the same as that for remote-expectancy. The difference is that while remote-expectancy constrains the annotations on send()’s and receive()’s in a particular thread, distributed remote-expectancy constrains the annotations on send()’s and receive()’s in possibly different threads.

Observe:

Lemma 4 Any family of annotation maps that is locally consistent for the empty thread map, or for a thread map with exactly one element in its domain, is communicative consistent for that thread map.

Proof. True trivially.

The significance of Lemma 4 is that the DP/ML compiler, which optimizes code for just an initial thread, only has to solve the local consistency constraints.

Fun(p : i) ⇒

θ_{p:i} = escape^{±} ⇒ G is distributed remote-expectant at p : i

App(p : i) ⇒

∀q ≠ p,

∀j such that lab(q : j) ∈ ϕ_{p:i.rator},

P_{p:i.rand} ≤^{→} P_{q:j.bv},

P_{q:j.body} ≤^{→} P_{p:i}

RFork(p : i) ⇒

∀q, j such that lab(q : j) ∈ ϕ_{p:i.rffun},

G is distributed remote-expectant at q : j, ∀q ≠ p,

∀k such that lab(q : k) ∈ ϕ_{p:i.rffun}, escape constraints hold at q : k

Receive(p : i) ⇒
∀q ≠ p,

∀j such that Send(q : j) ∧ κ_{p:i.rchan} ∩ κ_{q:j.schan} ≠ ∅,

P_{q:j.sbody} ≤^{→} P_{p:i}, and

proc(p) ≠ proc(q) ⇒

\begin{cases}θ_{q:j.sbody} = escape^{±}, \\ σ_{p:i} = reach^{±} ⇒ ω_{p:i} = local^{±} \end{cases}

Figure 5: Communicative consistency constraints

8 A coherence condition

The κ component of a proposition is a set of labels of channel() occurrences, and intended to indicate which occurrences of channel() may have produced a channel constant. Since channels are fresh when created, we would expect that if we saw two occurrences of the same channel constant in a program, at least one channel() label would be common to the κ annotations for those occurrences.

To enforce this property, we impose an additional condition on families of annotation maps:

Definition 1 A family of annotation maps for a thread map is κ-coherent iff for all pairs of distinct occurrences p : i, q : j of channel constants, where p may be the same as q, such that [[p : i]] = [[q : j]], κ_{p:i} ∩ κ_{q:j} ≠ ∅.

In an actual DP/ML program, there are no channel constants when the program is started, so the family of annotation maps for the thread map containing just an initial thread is necessarily κ-coherent.

A send() and receive() can only communicate if they share a channel. Therefore, we expect that the channel-parts of a send() and receive() which may communicate will have κ-annotations whose intersection is non-empty. This related notion is captured by:

Definition 2 An occurrence i of send() and an occurrence j of receive() are possible communications partners iff κ_{i.schan} ∩ κ_{j.rchan} ≠ ∅.

9 Transitions and annotation map updates

Given a family of annotation maps for the thread map on the left-hand side of a ⟶_{con} -transition, we would like to produce another family of annotation maps for the thread map on the right-hand side that preserves the consistency and coherence conditions we have stated. Such preservation may be likened to familiar subject reduction properties for typed languages.

9.1 Tree replacement and merger

How may annotation maps be updated? We first present the usual notion of tree replacement.

For two annotation maps Γ, Γ′, and an index i, Γ[i ← Γ′] indicates the tree obtained by replacing the subtree of Γ rooted at i with Γ′. The updated tree is a function defined by:

Γ[i ← Γ′](j) = \begin{cases}Γ′(k) & if j = i.k \\ Γ(j) & otherwise \end{cases}

Note that Γ′ may itself be a subtree of Γ.

For updating annotation maps, we will also want to perform a variation of tree replacement in which the updated tree retains its annotation at the replacement node. In this variation, the updated tree is a function defined by:

Γ[i ↩ Γ′](j) = \begin{cases}Γ′(k) & if j = i.k, k ≠ ϵ \\ Γ(j) & otherwise \end{cases}

We call this operation tree merger. We can simultaneously merge several subtrees Γ/i_{1}, …, Γ/i_{n} of Γ with a single subtree Γ′. The updated tree has the expected definition:

Γ[i_{1}, …, i_{n} ↩ Γ′](j) = \begin{cases}Γ′(k) & if j = i_{s}.k, 1 ≤ s ≤ n, k ≠ ϵ \\ Γ(j) & otherwise \end{cases}

10 Specifying the updates

Given a family of annotation maps for a thread map on the left-hand side of a ⟶_{con} transition, we can obtain a family of annotation maps for the thread map on the right-hand side. How to obtain the new family depends on the particular transition taken. In Figures 6 through 12, we present rules for annotation map updates for each kind of ⟶_{con} transition. In these figures, the unprimed Γ’s are the left-hand side annotation maps, and the Γ′’s are the updated, right-hand side maps. Also in these figures, we define the notion of occurrence predecessor for right-hand side occurrences.

The occurrence predecessor of an occurrence on the right-hand side of a transition is some occurrence on the left-hand side. We may think of the occurrence predecessor of a right-hand side occurrence as the “same” occurrence on the lefthand side. Most, but not all all right-hand side occurrences have an occurrence predecessor. The exceptions are the fresh unit constants on the right-hands sides of fork, rfork, and comm transitions, and the fresh channel constant on the right-hand side of a channel transition. If a right-hand side occurrence has an occurrence predecessor, it is unique. We write opred(i) for the occurrence predecessor of an occurrence i.

If we have a reduction sequence, rather than a single transition, we can compose opred maps. Define opred^{0} to be the identity on occurrence indices, and for n > 0, opred^{n} = opred ∘ opred^{n−1}. When we write, say, opred(p : i), we contemplate an underlying transition step; so when we write, say, opred^{n}(p : i), we contemplate an underlying reduction sequence. In later discussion, we may also refer to opred^{n}(p : i), for n > 1, as an occurrence predecessor of p : i, as well as in the case for n = 1.

We have used tree merger in only two places in the update specifications. Notice which right-hand side annotations affected by that choice:

Definition 3 Let i be the index of the left-hand side context hole in a ⟶_{con} - transition. Say that an occurrence j from the left-hand side is a value substitution iff the transition is a

• seq/β transition, and j = i.rand, or a

• comm transition, and j = i.sbody Transition:

Π[ p : ρ, C[(fn^{ℓ} x.M) V]] ⟶_{con} Π[ p : ρ, C[M[V/x]]]

Let i be the occurrence index of the context hole,

i.rator.body.m_{1}, …, i.rator.body.m_{j} be the free occurrences of [[i.rator.bv]] in i.rator.body

For thread p :

Γ′_{p} = Γ_{p}[i ← Γ_{p}/i.rator.body[m_{1}, …, m_{j} ↩ Γ_{p}/i.rand]]

for any RHS occurrence n,

opred(n) = \begin{cases}i.rand.k & if n = i.m.k, m ∈ \{m_{1}, …, m_{j}\} \\ i.rator.body.k & if n = i.k \\ n & otherwise \end{cases}

For any thread q ∈ Dom(Π), other than p : Γ′_{q} = Γ_{q}, for any RHS occurrence n, opred(n) = n

Figure 6: Updates for seq/β transition

Because we use tree merger at these points, a right-hand side occurrence whose occurrence predecessor is a value substitution retains the annotation of the the left-hand side occurrence where the value was substituted.

We are also interested in where substitutions occur:

Definition 4 In a ⟶_{con} -transition, a left-hand side occurrence i is a substitution site iff any of the following is true:

1. i is the index of a context hole

2. in the case of a seq/β transition, i is the index of a free occurrence of the operator binder in the operator body

3. in the case of a fork or an rfork transition, i is the index of a free occurrence of the spawned function’s binder in the function body

Observe:

Transition:

Π[ p : ρ, C[ if true then M else N]] ⟶_{con} Π[ p : ρ, C[M]]

Let i be the occurrence index of the context hole

For thread p :

Γ′_{p} = Γ_{p}[i ← Γ_{p}/i.then]

for any RHS occurrence n,

opred(n) = \{ \begin{matrix}i.then.k & if n = i.k \\ n & otherwise \end{matrix}

For any thread q ∈ Dom(Π), other than p :

Γ′_{q} = Γ_{q},

for any RHS occurrence n, opred(n) = n

Figure 7: Updates for seq/cond-true transition

Lemma 5 Let Π and Π′ be thread maps, and suppose Π ⟶_{con} Π′. Let s be a symbol in Σ and let i be an occurrence index such that i.s is an occurrence in Π′. In Π, opred(i).s is a substitution site iff opred(i.s) is undefined or opred(i.s) ≠ opred(i).s.

Proof.

Note that at substitution sites, either (1) a left-hand side occurrence is substituted, so that on the right-hand side, the substituted occurrence has an occurrence predecessor, or (2) some fresh occurrence is substituted (a unit constant or a fresh channel constant), which has no occurrence predecessor.

⟹

Suppose opred(i).s is a substitution site. Then i.s may be a fresh unit constant or a fresh channel constant, so that opred(i.s) is undefined. But suppose opred(i.s) is defined. Then opred(k.s) must be the substituted term, so opred(k).s ≠ opred(k.s).

⟸

Suppose opred(k.s) is undefined. By the definitions of opred for the various ⟶_{con} transition rules, the only occurrences k.s without occurrence predecessors Transition: Π[ p : ρ, C[ if true then M else N]] ⟶_{con} Π[ p : ρ, C[N]]

Let i be the occurrence index of the context hole

For thread p :

Γ′_{p} = Γ_{p}[i ← Γ_{p}/i.else]

for any RHS occurrence n,

opred(n) = \{ \begin{matrix}i.else.k & if n = i.k \\ n & otherwise \end{matrix}

For any thread q ∈ Dom(Π), other than p :

Γ′_{q} = Γ_{q},

for any RHS occurrence n, opred(n) = n

Figure 8: Updates for seq/cond-false transition

Transition:

Π[ p : ρ, C[channel^{ℓ}()]] ⟶_{con} Π[ p : ρ, C[k]] where k is a fresh channel constant

Let i be the occurrence index of the context hole

For thread p: Γ′_{p} = Γ_{p} for any RHS occurrence n, other than n = i,

opred(n) = n For any thread q ∈ Dom(Π), other than p :

Γ′_{q} = Γ_{q},

for any RHS occurrence n, opred(n) = n

Figure 9: Updates for channel transition Transition: Π[ p : ρ, C[fork(fn^{ℓ} x.M)]] ⟶_{con} Π[ p : ρ, C[unit]][ q : ρ, M[unit/x]]

where q is a fresh process identifier

Let i be the occurrence index of the context hole in thread p

For thread p:

Γ′_{p} = Γ_{p}

for any RHS occurrence p : n, other than n = i,

opred(p : n) = p : n

For thread q:

Γ′_{q} = Γ_{p}/i.ffun.body

for any occurrence q : n,

opred(q : n) = p : i.ffun.body.n, unless that is a free occurrence of [[p : i.ffun.bv]]

For any thread r ∈ Dom(Π), other than p or q:

Γ′_{r} = Γ_{r},

for any RHS occurrence r : n, opred(r : n) = r : n

Figure 10: Updates for fork transition

are unit constants and fresh channel constants. By the ⟶_{con} transition rules and the definitions of opred, opred(k).s must be the substitution site for such occurrences.

On the other hand, suppose opred(k).s ≠ opred(k.s). Then some occurrence must have been substituted at opred(k).s. The definition of substitution site covers all the possibilities.

By our specifications of annotation map updates, we have:

Lemma 6 Let Π be a thread map with a locally consistent, communicative consistent, and κ-coherent family of annotation maps G. Suppose that Π ⟶_{con} Π′, and let G′ be the updated family of annotation maps for Π′ for the particular transition Transition: Π[ p : ρ, C[rfork(ρ′,fn^{ℓ} x.M)]] ⟶_{con} Π[ p : ρ, C[unit]][ q : ρ′, M[unit/x]]

where q is a fresh process identifier

Let i be the occurrence index of the context hole

For process p:

Γ′_{p} = Γ_{p}

for any RHS occurrence p : n, other than n = i,

opred(p : n) = p : n

For process q:

Γ′_{q} = Γ_{p}/i.rffun.body

for any occurrence q : n,

opred(q : n) = p : i.rffun.body.n, unless that is a free occurrence of [[p : i.rffun.bv]]

For any process r ∈ Dom(Π), other than p or q:

Γ′_{r} = Γ_{r}, for any RHS occurrence r : n, opred(r : n) = r : n

Figure 11: Updates for rfork transition

involved. Let p : j be an occurrence in Π′, so that Γ′_{p} is the annotation map for the thread in which p : j occurs. If opred(p : j) is defined, let Γ_{q} be the annotation map for the thread in Π in which opred(p : j) occurs.

1. if opred(j) is defined, then [[opred(j)]] is generated by the same production in the DP/ML grammar as [[j]].

2. if p : j is the index of a function occurrence or an occurrence of channel(), then opred(p : j) is defined and lab(p : j) = lab(opred(p : j)).

3. if p : j is the index of a constant other than the unit constant, then opred(p : j) is defined and [[p : j]] = [[opred(p : j)]], unless the ⟶_{con} - transition is a channel transition and p : j is a fresh channel constant.

Transition:

Π[ p : ρ, C[send(k,V)]][ q : ρ′, C′[receive(k)]] ⟶_{con}

Π[ p : ρ, C[unit]][ q : ρ′, C′[V]]
Let i, i′ be the occurrence indices of the holes in the contexts C[ ], C′[ ]

For process p, Γ′_{p} = Γ_{p}, and

for any RHS occurrence p : n, other than n = i,

opred(p : n) = p : n

For process q, Γ′_{q} = Γ_{q}[i′ ↩ Γ_{p}/p : i.sbody], and

for any RHS occurrence q : n,

opred(q : n) = \{ \begin{matrix}p : j.sbody & if n = i′.j \\ q : n & otherwise \end{matrix}

For any process r ∈ Dom(Π), other than p or q:

Γ′_{r} = Γ_{r},

for any RHS occurrence r : n, opred(r : n) = r : n

Figure 12: Updates for comm transition

4. if opred(p : j) is defined, then P_{opred(p : j)}^{Γ_{q}} ≤^{→} P_{p:j}^{Γ′_{p}}.

5. if opred(p : j) is defined and opred(p : j) is not a a value substitution in the transition, then P_{opred(p : j)}^{Γ_{q}} = P_{p:j}^{Γ′_{p}}.

Proof. By the definition of opred for each ⟶_{con} -transition rule, the annotation map updates for each such rule, and the definitions of local consistency, communicative consistency, and κ-coherence.

Lemma 6 is the key lemma in our proofs of invariance properties. The following two lemmas will also be useful.

Lemma 7 Let Π be a thread map with a locally consistent, communicative consistent, and κ-coherent family of annotation maps G. Suppose that Π ⟶_{con} Π′ and there is an updated family of annotation maps for Π′. For any occurrence i from Π′, and for any symbol s ∈ Σ such that i.s is also an occurrence in Π′, P_{i.s} ≤^{→} P_{opred(i).s}.

Proof. By Lemma 6, local consistency, and the specifications of annotation map updates.

First assume that opred(i).s is not a substitution site. By Lemma 5, opred(i).s = opred(i.s), so also P_{opred(i).s} = P_{opred(i.s)}. Suppose opred(i.s) is not a value substitution, then by Lemma 6(5), P_{opred(i.s)} = P_{i.s}, so P_{i.s} = P_{opred(i).s}, hence P_{i.s} ≤^{→} P_{opred(i).s}. Assume instead opred(i.s) = opred(i).s is a value substitution. We shall show that this assumption leads to a contradiction. Then either (1) the transition is a seq/β transition, and opred(i) is the reduced application, or (2) the transition is a comm transition, and opred(i) is the communicating send(). But by the definitions of opred for seq/β and comm transitions, there is no right-hand side occurrence i such that opred(i) is the reduced application (in the case of (1)) or the communicating send() (in the case of (2)).

Now suppose opred(i).s is the site of a substitution. At the substitution site, either (1) the annotation map is unchanged, or tree merger is used, so that the annotation at the substitution site is unchanged, or (2) tree replacement is used, so that the annotation at the substitution site is the annotation of the substituted occurrence. In case (1) we have P_{i.s} = P_{opred(i).s}; in case (2) we have P_{i.s} ≤^{→} P_{opred(i).s}, by the local consistency of G. To verify the second of these, the reader may check that in all cases where the update is specified using tree replacement, there is a constraint that the proposition at the root of the substituted tree is ≤^{→} the proposition at the substitution site.

Lemma 8 Let Π be a thread map with a locally consistent, communicative consistent, and κ-coherent family of annotation maps G. Suppose that Π ⟶_{con} Π′ and there is an updated family of annotation maps for Π′. For any occurrence k from Π′, and for any symbol s ∈ Σ such that k.s is also an occurrence in Π′, if either (1) opred(k.s) is a value substitution, or (2) opred(k).s is not the site of a substitution, then P_{k.s} = P_{opred(k).s}.

Proof. By the specifications of annotation map updates.

(1): In the specifications of annotation map updates for seq/β and comm transitions, the use of tree merger preserves the annotation at the site opred(k).s where opred(k.s) is substituted.

(2): By Lemma 5, opred(k).s = opred(k.s), hence P_{opred(k).s} = P_{opred(k.s)}. Since opred(k).s is not the site of a substitution, opred(k.s) must not be a value substitution. By Lemma 6(5), P_{k.s} = P_{opred(k.s)}. Hence, P_{k.s} = P_{opred(k).s}.

Another useful result is:

Lemma 9 Let G be a locally consistent, communicative consistent, and κ-coherent family of annotation maps for a thread map Π, and suppose Π ⟶_{con} Π′. Let G′ be the updated family of annotation maps for Π′. Suppose also that p : i is an occurrence of a send() and q : j is an occurrence of a receive() in Π′ that are possible communications partners. Then in Π, opred(p : i) and opred(q : j) were occurrences of a send() and a receive() that were possible communications partners.

Proof. By Definition 2 and Lemma 6.

Suppose p : i and q : j are possible communications partners. Then in G′, by Definition 2, κ_{p:i.schan} ∩ κ_{q:j.rchan} ≠ ∅. By Lemma 6(1), opred(p : i) is also an occurrence of a send(), and opred(q : j) is also an occurrence of a receive(). By Lemma 7, P_{p:i.schan} ≤^{→} P_{opred(p : i).schan} and P_{q:j.rchan} ≤^{→} P_{opred(q : j).rchan}. Therefore, κ_{opred(p : i).schan} ∩ κ_{opred(q : j).rchan} ≠ ∅. By Definition 2, opred(p : i) and opred(q : j) were possible communications partners.

11 Semantics of propositions

Recall, the goal of our analysis is to determine which occcurrences of channel() produce channels that are used only locally, meaning that those channels participate in communications only on the processor on which they are created. Therefore, the meaning we give to propositions has an operational basis.

We need the following:

Definition 5 Suppose for some n ≥ 0, Π ⟶^{n}_{con} Π′. An occurrence q : j in Π′ is traceable to an occurrence p : i in Π, iff opred^{n}(q : j) = p : i.

Also:

Definition 6 Suppose Π ⟶^{+}_{con} Π′. Let p : i be an occurrence of channel() in Π. An occurrence q : j of a channel constant k in Π′ is produced by p : i iff for some Π′′ intermediate in the evaluation

• there exists a channel() occurrence r : m in Π′′ that is traceable to p : i in Π,

• in one channel step involving r : m, Π′′ ⟶_{con} Π′′′, so that r : m is also the occurrence index of k in Π′′′, and

• q : j in Π′ is traceable to r : m in Π′′′.

We say that q : j in Π′ is directly produced by r : m in Π′′.

The picture is:

Π ⟶^{∗}_{con} Π′′ \underbrace{⟶_{con}}_{channel} Π′′′ ⟶^{∗}_{con} Π′

Now we give our notion of satisfaction:

Definition 7 Let Π be a thread map, and let G be a family of annotation maps, with one family member for each thread identifier in the domain of Π. Say that an evaluation Π ⟶^{∗}_{con} Π′ satisfies G, written

Π ⟶^{∗}_{con} Π′ ⊧ G

iff for any channel() occurrence p : i in Π, if ω_{p:i} = local^{+}, then for any intermediate Π′′ in the evaluation, including Π′, for any occurrence s : n of a channel constant in Π′′ produced by p : i in Π, such that s : n is a channel-part subterm of either a send() or a receive() in Π′′, and such that s : n was directly produced by an occurrence r : m in a thread map Π′′′ preceding Π′′ in the evaluation, we have

proc_{Π′′}(s) = proc_{Π′′′}(r)

We will use this notion of satisfaction as the criterion of the soundness of our analysis. Note that this semantics ignores all but the ω component of propositions. While we could have mentioned the other components in our semantics, since they do provide useful information about annotated programs, we do not need to do so for our local channel analysis.

12 Invariance results

If we use the annotation map updates specified, then local consistency, communicative consistency, κ-coherence, and ω-coherence are maintained across ⟶_{con} - transitions.

The invariance of κ-coherence is the easiest of these results:

Theorem 1 Let Π be a thread map with a locally consistent, communicative consistent, and κ-coherent family of annotation maps G. Suppose Π ⟶_{con} Π′, and let G′ be the updated family of annotation maps for Π′. Then G′ is κ-coherent.

Proof. By Lemma 6.

Suppose i and j are distinct occurrences of the same channel constant on the right-hand side.

We note that opred(i) and opred(j) are both defined. Assume that, say, opred(i) is undefined, but opred(j) is defined. The reverse case is similar. Then i must be an occurrence of a fresh channel constant. By Lemma 6(1), opred(j) is also a channel constant. By Lemma 6(3), [[opred(j)]] = [[j]]. Since we assumed [[i]] = [[j]], i is not fresh, a contradiction. Assume now that both opred(i) and opred(j) are undefined. Then i and j are both occurrences of a fresh channel constant. But we assumed [[i]] = [[j]], and the ⟶_{con} rules provide no way to create more than one occurrence of a fresh channel constant.

By Lemma 6(1), opred(i) and opred(j) are both channel constants. By Lemma 6(3), [[opred(i)]] = [[i]] and [[opred(j)]] = [[j]], so [[opred(i)]] = [[opred(j)]]. Therefore, by the κ-coherence of G, κ_{opred(i)} ∩ κ_{opred(j)} ≠ ∅. But by Lemma 6(4), κ_{opred(i)} ⊆ κ_{i} and κ_{opred(j)} ⊆ κ_{j}, so κ_{i} ∩ κ_{j} ≠ ∅.

Now we give our more significant invariance results.

Theorem 2 Let Π be a thread map with a family of annotation maps G that is locally consistent, communicative consistent, and κ-coherent. Suppose Π ⟶_{con} Π′. Then the updated family of annotation maps G′ is locally consistent for Π′.

Proof. By considering each possible ⟶_{con} -transition and G′, the updated family of annotation maps.

For each possible ⟶_{con} -transition, we check the local consistency of the annotation map or maps at each occurrence j on the right-hand side from those threads which change from the left-hand side. Assume each transition is as in Figures 6 to 12.

case seq/β

Let Γ be the left-hand side annotation map for the thread p; let Γ′ be the updated right-hand side annotation map for the same thread.

Suppose Var(j).

The only constraint is that if k is the binding occurrence for j, then P_{k}^{Γ′} ≤^{→} P_{j}^{Γ′}. If j has no binding occurrence, we are done. Otherwise, assume k is the binding occurrence for j. By Lemma 6(1), Var(opred(j)). Since substitution does not cause variable capture, opred(k) must have been the binding occurrence for opred(j). By the local consistency of Γ, P_{opred(k)}^{Γ} ≤^{→} P_{opred(j)}^{Γ}. Now, neither opred(k) nor opred(j) is a value, so neither was a value substitution. By Lemma 6(5), P_{k}^{Γ′} = P_{opred(k)}^{Γ} and P_{opred(j)}^{Γ} = P_{j}^{Γ′}. Hence, P_{k}^{Γ′} ≤^{→} P_{j}^{Γ′}.

Suppose Channel(j).

By Lemma 6(1), also Channel(opred(j)). Therefore, by the local consistency of Γ, lab(opred(j)) ∈ κ_{opred(j)}^{Γ}. By Lemma 6(4), P_{opred(j)}^{Γ} ≤^{→} P_{j}^{Γ′}, so κ_{opred(j)}^{Γ} ⊆ κ_{j}^{Γ′}. Therefore, lab(opred(j)) ∈ κ_{j}^{Γ′}. By Lemma 6(2), lab(j) = lab(opred(j)). Hence lab(j) ∈ κ_{j}^{Γ′}.

Suppose Fun(j).

The first constraint is that lab(j) ∈ ϕ_{j}^{Γ′}. The analysis follows that for

channel() labels.

The next constraint is, if the number of free occurrences of the procedure binder in the procedure body is greater than 1, then ν_{j.bv}^{Γ′} = ∞. Suppose the condition holds. By Lemma 6(1), also Fun(opred(j)). Now, suppose β-reduction did not substitute the application operand in [[opred(j)]]. Then [[opred(j)]] = [[j]], so in opred(j), the number of free occurrences of the procedure binder in the procedure body is also greater than 1. So by the local consistency of Γ, ν_{opred(j).bv}^{Γ} = ∞.

By Lemma 7, P_{j.bv}^{Γ′} ≤^{→} P_{opred(j).bv}^{Γ}. By the ≤^{→}-order on propositions, also ν_{j.bv}^{Γ′} = ∞. Suppose instead that β-reduction did substitute the application operand in [[opred(j)]]. Then [[j]] is a substitution instance of [[opred(j)]]. It is easy to show that in opred(j), the number of free occurrences of its binder in its body is the same as for j; so the result follows as before.

The escape constraints are triggered in case θ_{j}^{Γ′} = escape^{±}. Assume that condition holds, else we are done. By Lemma 6, P_{opred(j)}^{Γ} ≤^{→} P_{j}^{Γ′}, so by the ≤^{→}-

order on propositions, θ_{j}^{Γ′} ≤^{→} θ_{opred(j)}^{Γ}. Therefore, θ_{opred(j)}^{Γ} = escape^{±}, so the escape constraints held in Γ.

We now examine each of the escape constraints.

Let j.k be a free variable occurrence in j. We want to show two things, that θ_{j.k}^{Γ′} = escape^{±}, and that if σ_{j.k}^{Γ′} = reach^{±}, then ω_{j.k}^{Γ′} = local^{±}. For the latter constraint, assume the condition holds.

By Lemma 6(1), also Var(opred(j.k)). Since j.k is a subterm of j, opred(j.k) may have been a subterm of opred(j), that is, opred(j.k) = opred(j).k, but it may instead be that opred(j.k) was a subterm of the substituted application operand.

First suppose that opred(j.k) = opred(j).k; then opred(j.k) was also a free variable occurrence in opred(j). By the local consistency of Γ, θ_{opred(j.k)}^{Γ} = escape^{±}, and, if σ_{opred(j.k)}^{Γ} = reach^{±}, then ω_{opred(j.k)}^{Γ} = local^{±}. Since it is not a value, opred(j.k) cannot have been a value substitution. So by Lemma 6(5), P_{opred(j.k)}^{Γ} = P_{j.k}^{Γ′}, and θ_{j.k}^{Γ′} = escape^{±}, as desired. Under our assumption that σ_{j.k}^{Γ′} = reach^{±}, also σ_{opred(j.k)}^{Γ} = reach^{±}. Therefore, by the local consistency of Γ, ω_{opred(j.k)}^{Γ} = local^{±}. Again using Lemma 6(5), ω_{j.k}^{Γ′} = local^{±}.

Suppose instead that opred(j.k) was a subterm of the substituted operand. The operand was substituted for an occurrence of a free variable subterm of opred(j), say opred(j).m. By the local consistency of Γ, θ_{opred(j).m}^{Γ} = escape^{±}.

Now consider the substituted operand i.rand. Since the operand contained a variable subterm, it must have been a function. We can show that P_{i.rand}^{Γ} ≤^{→} P_{opred(j).m}^{Γ} (we omit the straightforward details). Therefore, θ_{i.rand}^{Γ} = escape^{±}. Since opred(j.k) was a free variable occurrence in i.rand, from here, the analysis is the same as in the case that opred(j.k) was a subterm of opred(j).

Next, we wish to show that for all channel constant occurrences j.m, if σ_{j.m}^{Γ′} = reach^{±}, then ω_{j.m}^{Γ′} = local^{±}. Observe that a channel constant is a value, so in contrast to a variable, it may be a value substitution. If opred(j.m) is not a value substitution, the analysis is identical to the free variable case for the comparable constraint. If opred(j.m) is a value substitution, then it must have been the application operand i.rand, and it was substituted for some free variable in opred(j). Observe that opred(j).m must have been the index of the substituted free variable. By Lemma 8(1), P_{j.m}^{Γ′} = P_{opred(j).m}^{Γ}. So assume the condition in the constraint holds. Therefore, σ_{opred(j).m}^{Γ} = reach^{±}. Since opred(j).m was a free variable in opred(j), by the local consistency of Γ, ω_{opred(j).m}^{Γ} = local^{±}. Therefore, ω_{j.m}^{Γ′} = local^{±}.

We now want to show that Γ′ is remote-expectant at j. Consider any pair of possible communications partners in the p thread such that exactly one of the pair is a subterm of j. We want to show that in Γ′, the body of the send() occurrence has a θ annotation of escape^{±}, and that if the σ annotation of the receive() occurrence is reach^{±}, then its ω annotation is local^{±}. By Lemma 9, the occurrence predecessors of the pair were possible communications partners.

Suppose it is the send() that is a subterm of j, and the receive() is not. The reverse situation is similar, and we will not analyze it further. Let these be j.k and m, respectively. Now, opred(j.k) was a subterm of either opred(j) or the substituted operand, i.rand. In the first case, opred(j) had a θ-annotation of escape^{±}, so Γ was remote-expectant at opred(j). In the second case, we can show, as we did for free variable subterms, that i.rand had a θ-annotation of escape^{±}, so Γ was remote-expectant at i.rand. We will look just at the first case.

Consider opred(m). If opred(m) was not a subterm of opred(j), then by the remote-expectancy of Γ, θ_{opred(j.k).sbody}^{Γ} = escape^{±}. By Lemma 7, P_{j.k.sbody}^{Γ′} ≤^{→} P_{opred(j.k).sbody}^{Γ}, hence θ_{j.k.sbody}^{Γ′} = escape^{±}. Now assume that σ_{m}^{Γ′} = reach^{±}. By

Lemma 6(4), P_{opred(m)}^{Γ} ≤^{→} P_{m}^{Γ′}. By the ≤^{→}-order on propositions, σ_{m}^{Γ′} ≤ σ_{opred(m)}^{Γ}, so σ_{opred(m)}^{Γ} = reach^{±}. So by the local consistency of Γ, ω_{opred(m)}^{Γ} = local^{±}. Since a receive() cannot be a value substitution, by Lemma 6(5), also ω_{m}^{Γ′} = local^{±}.

But it may have been that opred(m) was also a subterm of opred(j). In that case, it must have been that the β-reduction duplicated the operand i.rand, and opred(m) was a subterm of i.rand. In fact, in that case, opred(j) was either the same as i.rand, or a proper subterm of it. To see this, note that opred(m) was a subterm of both i.rand and opred(j), hence one must have been a subterm of the other; but reduction cannot occur in a function body, hence i.rand cannot have been a proper subterm of opred(j). The β-reduction duplicates i.rand, so the number of free occurrences of the binder of the application operator, [[i.bv]], in its body, [[i.body]], must have been greater than 1. Hence, by the local consistency of Γ, ν_{i.bv}^{Γ} = ∞. Also by local consistency, we can show that ν_{i.rand}^{Γ} = ∞; since opred(j) is either the same as i.rand, or a function subterm of i.rand, ν_{opred(j)}^{Γ} = ∞. By the nonlinear-expectancy of Γ at opred(j), θ_{opred(j.k).sbody}^{Γ} = escape^{±}. So by Lemma 7, also θ_{j.k.sbody}^{Γ′} = escape^{±}. Again assume that σ_{m}^{Γ′} = reach^{±}, so σ_{opred(m)}^{Γ} = reach^{±}, and again by the nonlinear-expectancy of Γ at opred(j), ω_{opred(m)}^{Γ} = local^{±}. Again by Lemma 6(5), ω_{m}^{Γ′} = local^{±}.

Next we show the nonlinear-expectancy of Γ′ at j. Assume ν_{j}^{Γ′} = ∞, otherwise we are done. By Lemma 6(4), also ν_{opred(j)}^{Γ} = ∞. We have already shown that Γ was nonlinear-expectant at opred(j). Consider a send() occurrence j.k and a receive() occurrence m that are possible communications partners, and also both subterms of j. We wish to show that θ_{j.k.sbody}^{Γ′} = escape^{±} and, if σ_{m}^{Γ′} = reach^{±}, then ω_{m}^{Γ′} = local^{±}. By Lemma 9, opred(j.k) and opred(m) were possible communications partners. On the left-hand side, opred(j.k) was either a subterm of opred(j) or a subterm of i.rand; similarly for opred(m). We consider each of the four possibilities. By Lemma 7, P_{j.k.sbody}^{Γ′} ≤^{→} P_{opred(j.k).sbody}^{Γ}, so for each of the four cases, it suffices to prove that θ_{opred(j.k).sbody}^{Γ} = escape^{±}. We assume that

σ_{m}^{Γ′} = reach^{±}. By Lemma 6(4), P_{opred(m)}^{Γ} ≤^{→} P_{m}^{Γ′}, so by the ≤^{→}-order on propositions, also σ_{opred(m)}^{Γ} = reach^{±}. Since a receive() cannot be a value substitution, by Lemma 6(5), ω_{m}^{Γ′} = ω_{opred(m)}^{Γ}. Therefore, for each of the four cases, it suffices to prove that ω_{opred(m)}^{Γ} = local^{±}.

1. Suppose both opred(j.k) and opred(m) were subterms of opred(j). By the nonlinear-expectancy of Γ at opred(j), θ_{opred(j.k).sbody}^{Γ} = escape^{±} and ω_{opred(m)}^{Γ} = local^{±}.

2. If both opred(j.k) and opred(m) were subterms of i.rand, and neither was a subterm of opred(j), then the operand must have been substituted for a free variable in opred(j). Since ν_{opred(j)}^{Γ} = ∞, also that free variable occurrence must have had a ν-annotation of ∞; since θ_{opred(j)}^{Γ} = escape^{±}, the free variable occurrence also had a θ-annotation of escape^{±}. It is straightforward to show that ν_{i.rand}^{Γ} = ∞ and θ_{i.rand}^{Γ} = escape^{±}. Therefore, Γ was nonlinearexpectant at i.rand, so θ_{opred(j.k).sbody}^{Γ} = escape^{±} and ω_{opred(m)}^{Γ} = local^{±}.

3. Suppose opred(j.k) was a subterm of opred(j), and not a subterm of i.rand, but opred(m) was a subterm of i.rand, and not a subterm of opred(j). Then by the remote-expectancy of Γ at j, we have θ_{opred(j.k).sbody}^{Γ} = escape^{±}

and ω_{opred(m)}^{Γ} = local^{±}.

4. Suppose opred(j.k) was a subterm of i.rand, and not a subterm of opred(j), but opred(m) was a subterm of opred(j), and not a subterm of i.rand. In this case, too, the operand must have been substituted for a free variable in opred(j), and by the local consistency of Γ, such a free variable occurrence had a θ-annotation of escape^{±}. Therefore, θ_{i.rand}^{Γ} = escape^{±}, so Γ was remote-expectant at i.rand. By the definition of remote-expectancy, θ_{opred(j.k).sbody}^{Γ} = escape^{±} and ω_{opred(m)}^{Γ} = local^{±}.

Finally for the Fun(j) subcase, we have the constraint that if ν_{j}^{Γ′} = ∞, then all free variable and function occurrence subterms of j have a ν-annotation of ∞. Suppose the condition holds. By Lemma 6(4) and the ≤^{→}-order on propositions, also ν_{opred(j)}^{Γ} = ∞. We shall soon deal with free variable subterms of j, but consider first a function subterm of j, say j.k. opred(j.k) may have been a subterm of opred(j), or it may have been a subterm of i.rand. In the first case, by the local consistency of Γ, ν_{opred(j.k)}^{Γ} = ∞. Such a subterm was not a value substitution. Therefore, by Lemma 6(5), ν_{j.k}^{Γ′} = ∞.

In the second case, it must be that the operand was substituted for a free variable occurrence in opred(j). By the local consistency of Γ, that free variable occurrence had a ν-annotation of ∞, hence ν_{i.rand}^{Γ} = ∞ (we omit the details). opred(j.k) may have been the operand itself, or a proper subterm of the operand. If opred(j.k) = i.rand, then opred(j.k) was a value substitution, so by Lemma 8(1), P_{j.k}^{Γ′} = P_{opred(j).k}^{Γ}. Now, opred(j).k was the substituted free variable, which, as we stated, had a ν-annotation of ∞. So also ν_{j.k}^{Γ′} = ∞. Otherwise, opred(j.k) is a proper subterm of i.rand, and so not a value substitution. The only kind of value that may have proper subterms is a function. By the local consistency of Γ, such a function subterm of i.rand has a ν-annotation of ∞. So by Lemma 6(5), ν_{j.k}^{Γ′} = ν_{opred(j.k)}^{Γ} = ∞.

Now consider a free variable subterm of j, say j.m. We want to show that j.m has a ν-annotation of ∞. opred(j.m) may have been a subterm of opred(j), or it may have been a subterm of i.rand. In the first case, opred(j.m) was also free in opred(j), so by the local consistency of Γ, ν_{opred(j.m)}^{Γ} = ∞. By Lemma 6(5), ν_{j.m}^{Γ′} = ∞. In the second case, we can show that ν_{i.rand}^{Γ} = ∞. opred(j.m) must have been a proper subterm of the operand and so not a value substitution. opred(j.m) was also a free variable subterm of i.rand. By the local consistency of Γ, opred(j.m) had a ν-annotation of ∞. By Lemma 6(5), ν_{j.m}^{Γ′} = ν_{opred(j.m)}^{Γ} = ∞.

Suppose App(j).

We have the constraints that for all k such that lab(k) ∈ ϕ_{j.rator}^{Γ′}, P_{j.rand}^{Γ′} ≤^{→} P_{k.bv}^{Γ′} and P_{k.body}^{Γ′} ≤^{→} P_{j}^{Γ′}. Since App(j), also App(opred(j)), by Lemma 6(1). Therefore, by the local consistency of Γ, for all k such that lab(k) ∈ ϕ_{opred(j).rator}^{Γ}, P_{opred(j).rand}^{Γ} ≤^{→} P_{k.bv}^{Γ}, and P_{k.body}^{Γ} ≤^{→} P_{opred(j)}^{Γ}.

By Lemma 7, ϕ_{j.rator}^{Γ′} ⊆ ϕ_{opred(j).rator}^{Γ}. Consider any function occurrence k from the right-hand side term such that lab(k) ∈ ϕ_{j.rator}^{Γ′}. Since lab(opred(k)) = lab(k), lab(opred(k)) ∈ ϕ_{opred(j).rator}^{Γ}. By the local consistency of Γ, lab(opred(k)) ∈ ϕ_{opred(j).rator}^{Γ} implies P_{opred(j).rand}^{Γ} ≤^{→} P_{opred(k).bv}^{Γ} and P_{opred(k).body}^{Γ} ≤^{→} P_{opred(j)}^{Γ}. Since opred(k).bv cannot have been the site of a substitution, by Lemma 8(2), P_{k.bv}^{Γ′} = P_{opred(k).bv}^{Γ}. By Lemma 7, P_{j.rand}^{Γ′} ≤^{→} P_{opred(j).rand}^{Γ}. Therefore, P_{j.rand}^{Γ′} ≤^{→} P_{k.bv}^{Γ′}. Also by Lemma 7, P_{k.body}^{Γ′} ≤^{→} P_{opred(k).body}^{Γ}. By Lemma 6(4), P_{opred(j)}^{Γ} ≤^{→} P_{j}^{Γ′}. Hence, P_{k.body}^{Γ′} ≤^{→} P_{j}^{Γ′}.

Suppose Cond(j).

By Lemma 6(1), also Cond(opred(j)). By the local consistency of Γ, P_{opred(j).then}^{Γ}, P_{opred(j).else}^{Γ} ≤^{→} P_{opred(j)}^{Γ}. By Lemma 7, P_{j.then}^{Γ′} ≤^{→} P_{opred(j).then}^{Γ}, and P_{j.else}^{Γ′} ≤^{→} P_{opred(j).else}^{Γ}. By Lemma 6(4), P_{opred(j)}^{Γ} ≤^{→} P_{j}^{Γ′}. Hence P_{j.then}^{Γ′},

P_{j.else}^{Γ′} ≤^{→} P_{j}^{Γ′}.

Suppose RFork(j).

In this case, for all k such that lab(k) ∈ ϕ_{j.rffun}^{Γ′}, we require that the escape constraints hold at k. Consider such a k. By Lemma 6(2), lab(k) = lab(opred(k)). By Lemma 6(1), also RFork(opred(j)). By Lemma 7, ϕ_{j.rffun}^{Γ′} ≤^{→} ϕ_{opred(j).rffun}^{Γ}. Hence, lab(opred(k)) ∈ ϕ_{opred(j).rffun}^{Γ}. Therefore, in Γ, the escape constraints held at opred(k).

Now consider the reasoning we used in the Fun subcase to show that the escape constraints held at function j′ in Γ′. We began by assuming the condition θ_{j′}^{Γ′} = escape^{±}. Using Lemma 6(4), we had that θ_{opred(j′)}^{Γ} = escape^{±}. By local consistency, the escape constraints held in Γ at opred(j′). That was sufficient to show that the escape constraints held in Γ′ at j′. Here, for the RFork subcase, we have shown that the escape constraints hold in Γ at opred(k), using the local consistency of Γ at opred(j). Therefore, the same reasoning we used in the Fun subcase can be used to show that the escape constraints hold in Γ′ at k.

Suppose Send(j).

The only constraint is that σ_{j.schan}^{Γ′} = reach^{±}. By Lemma 6(1), also Send(opred(j)). Since Γ is locally consistent, we have σ_{opred(j).schan}^{Γ} = reach^{±}. By Lemma 7, P_{j.schan}^{Γ′} ≤^{→} P_{opred(j).schan}^{Γ}. By the ≤^{→}-order on propositions, σ_{j.schan}^{Γ′} = reach^{±}.

Suppose Receive(j).

The first constraint is that σ_{j.rchan}^{Γ′} = reach^{±}. We can use the similar reasoning as in the Send subcase for the constraint on σ annotations.

The other constraint is that for all k such that Send(k) and κ_{k.schan}^{Γ′} ∩κ_{j.rchan}^{Γ′} ≠ ∅, P_{k.sbody}^{Γ′} ≤^{→} P_{j}^{Γ′}. Choose any such k. By Lemma 9, opred(j) and opred(k) were possible communications partners on the left-hand side. Also, both those occurrences were in the p thread on the left-hand side. So by the local consistency of Γ, P_{opred(k).sbody}^{Γ} ≤^{→} P_{opred(j)}^{Γ}. By Lemma 7, P_{k.sbody}^{Γ′} ≤^{→} P_{opred(k).sbody}^{Γ}; by Lemma 6(4),

P_{opred(j)}^{Γ} ≤^{→} P_{j}^{Γ′}. So P_{k.sbody}^{Γ′} ≤^{→} P_{j}^{Γ′}.

case seq/cond-true

We shall omit the proof of local consistency for the seq/cond-false case, which is similar. As in the case for a seq/β transition, we omit the thread identifier subscripts on annotation maps; let Γ be the left-hand side annotation map for the thread p, and let Γ′ the annotation map for the right-hand side thread p.

Suppose Var(j).

The one constraint is that if k is the binding occurrence for j, then P_{k}^{Γ′} ≤^{→} P_{j}^{Γ′}. Use the same reasoning as in the seq/β case.

Suppose Channel(j).

The only constraint is that lab(j) ∈ ϕ_{j}^{Γ′}. Use the same reasoning as in the seq/β case.

Suppose Fun(j).

The first constraint is that lab(j) ∈ ϕ_{j}^{Γ′}. This can be shown using the same reasoning as in the seq/β case for channel() labels.

Next, we have the constraint that if the number of free occurrences of the procedure binder in the procedure body is greater than 1, then ν_{j}^{Γ′} = ∞. A conditional redex cannot occur in a function body, so [[j]] = [[opred(j)]]. Therefore, in opred(j), the number of free occurrences of its binder in its body is the same as for j. Assume the condition holds. By the local consistency of Γ, ν_{opred(j).bv}^{Γ} = ∞.

By Lemma 7, P_{j.bv}^{Γ′} ≤^{→} P_{opred(j).bv}^{Γ}, so also ν_{j.bv}^{Γ′} = ∞.

Next we consider the escape constraints that are triggered if θ_{j}^{Γ′} = escape^{±}. Assume the condition holds. By Lemma 6(1), also Fun(opred(j)); by Lemma 6(5), also θ_{opred(j)}^{Γ} = escape^{±}.

The first constraints triggered by the condition are that for all free variable occurrences j.k, θ_{j.k}^{Γ′} = escape^{±}, and, if σ_{j.k}^{Γ′} = reach^{±}, then ω_{j.k}^{Γ′} = local^{±}. Assume the condition holds for the latter constraint. Observe that opred(j.k) must have been a free variable occurrence in opred(j). So by the local consistency of Γ, θ_{opred(j.k)}^{Γ} = escape^{±}. Since opred(j.k) is not a value, it cannot have been a value substitution. By Lemma 6(5), P_{opred(j.k)}^{Γ} = P_{j.k}^{Γ′}, so θ_{j.k}^{Γ′} = θ_{opred(j.k)}^{Γ}.

Therefore, θ_{j.k}^{Γ′} = escape^{±}. Similarly, σ_{opred(j.k)}^{Γ} = reach^{±}, so by local consistency, ω_{opred(j.k)}^{Γ} = local^{±}. So also ω_{j.k}^{Γ′} = local^{±}.

Next we consider the constraint that for any channel constant occurrence j.k, if σ_{j.k}^{Γ′} = reach^{±}, then ω_{j.k}^{Γ′} = local^{±}. We can use almost the same reasoning as we just used for free variables. Although channel constants are values, unlike variables, opred(j.k) cannot have been a value substitution. For a seq/cond-true transition, no left-hand side occurrence is a value substitution.

Next we show that Γ′ is remote-expectant at j. Consider any pair of possible communications partners such that exactly one of the pair is a subterm of j. We want to show that in Γ′, the body of the send() occurrence has a θ annotation of escape^{±}, and that if the σ annotation of the receive() occurrence is reach^{±}, then its ω annotation is local^{±}. By Lemma 9, the occurrence predecessors of the pair were possible communications partners. Both occurrence predecessors were in the p thread on the left-hand side.

Suppose it is the send() that is a subterm of j, and the receive() is not. As in the seq/β case, the reverse situation is similar, so we will not discuss it. Let these occurrences be j.k and m, respectively. opred(j.k) must have been a subterm of opred(j). Now, opred(j) had a θ-annotation of escape^{±}, so Γ was remote-expectant at opred(j).

Consider opred(m). opred(m) must not have been a subterm of opred(j). So by the remote-expectancy of Γ, θ_{opred(j.k).sbody}^{Γ} = escape^{±}. By Lemma 7,

P_{j.k.sbody}^{Γ′} ≤^{→} P_{opred(j.k).sbody}^{Γ}, so also θ_{j.k.sbody}^{Γ′} = escape^{±}. Assume that σ_{m}^{Γ′} =

reach^{±}. By Lemma 6(4), P_{opred(m)}^{Γ} ≤^{→} P_{m}^{Γ′}. By the ≤^{→}-order on propositions, also σ_{opred(m)}^{Γ} = reach^{±}. By the local consistency of Γ, ω_{opred(m)}^{Γ} = local^{±}. Since a receive() cannot be a value substitution, by Lemma 6(5), also ω_{m}^{Γ′} = local^{±}.

Next we show the nonlinear-expectancy of Γ′ at j. Assume ν_{j}^{Γ′} = ∞, otherwise we are done. By Lemma 6(4), P_{opred(j)}^{Γ} ≤^{→} P_{j}^{Γ′}, so ν_{opred(j)}^{Γ} = ∞. Since also θ_{opred(j)}^{Γ} = escape^{±}, Γ was nonlinear-expectant at opred(j). Consider a send() occurrence j.k with a possible communications partner m that is also a subterm of j. We wish to show that θ_{j.k.sbody}^{Γ′} = escape^{±}, and that if σ_{m}^{Γ′} = reach^{±}, then ω_{m}^{Γ′} = local^{±}. By Lemma 9, opred(j.k) and opred(m) were possible communications partners. On the left-hand side, opred(j.k) and opred(m) must both have been subterms of opred(j). By the nonlinear-expectancy of Γ at opred(j), θ_{opred(j.k).sbody}^{Γ} = escape^{±}. By Lemma 7, P_{j.k.sbody}^{Γ′} ≤^{→} P_{opred(j.k).sbody}^{Γ}. By the ≤^{→}- order on propositions, also θ_{j.k.sbody}^{Γ} = escape^{±}. Assume that σ_{m}^{Γ′} = reach^{±}. By Lemma 6(4), P_{opred(m)}^{Γ} ≤^{→} P_{m}^{Γ′}, so σ_{m}^{Γ′} ≤ σ_{opred(m)}^{Γ}, hence σ_{opred(m)}^{Γ} = reach^{±}. By the nonlinear-expectancy of Γ at opred(j), ω_{opred(m)}^{Γ} = local^{±}. A receive() cannot be a value substitution, so by Lemma 6(5), also ω_{m}^{Γ′} = local^{±}.

Last for the Fun subcase, we have the constraint that if ν_{j}^{Γ′} = ∞, then all free variable and function subterms of j have a ν-annotation of ∞. Suppose the condition holds. By Lemma 6(4), also ν_{opred(j)}^{Γ} = ∞. Consider a free variable or function subterm j.k of j. opred(j.k) must have been a subterm of opred(j). If j.k is a free variable in j, then opred(j.k) was a free variable in opred(j). So by the local consistency of Γ, ν_{opred(j.k)}^{Γ} = ∞. opred(j.k) cannot have been a value substitution, so by Lemma 6(5), also ν_{j.k}^{Γ′} = ∞.

Suppose App(j).

Use the same reasoning as in the App subcase for seq/β transitions.

Suppose Cond(j).

Use the same reasoning as in the Cond subcase for seq/β transitions.

Suppose RFork(j).

We want to show that for all k such that lab(k) ∈ ϕ_{j.rffun}^{Γ′}, the escape constraints hold at k. Consider such a k. By Lemma 6(2), lab(k) = lab(opred(k)). By Lemma 6(1), also RFork(opred(j)). By Lemma 7, P_{j.rffun}^{Γ′} ≤^{→} P_{opred(j).rffun}^{Γ}. Hence, lab(opred(k)) ∈ ϕ_{opred(j).rffun}^{Γ}. Therefore in Γ, the escape constraints held at opred(k). Using the same reasoning we used in the Fun subcase, above, we can show that the escape constraints hold in Γ′ at k.

Suppose Send(j).

Use the same reasoning as in the Send subcase for seq/β transitions.

Suppose Receive(j).

Use the same reasoning as in the Receive subcase for seq/β transitions.

case channel

The context hole cannot be in a function body, therefore local consistency follows by Lemma 3.

case fork

Let Γ be the annotation map for the parent thread p on the left-hand side of the transition, let Γ′ be the annotation map for the p thread on the right-hand side, and let Γ′′ be the annotation map for the child thread q on the right-hand side.

The local consistency of Γ′ follows by Lemma 2.

Since the function body M is a subterm of the left-hand side term containing the fork(), by Lemma 1, Γ′′ is locally consistent for M. By the Corollary to Lemma 2, Γ′′ is locally consistent for M[unit/x]. case rfork

This case is nearly identical to that for fork.

case comm

Let Γ_{p} be the annotation map for the p thread on the left-hand side of the transition. Γ_{q} is the annotation map for the q thread on the left-hand side of the transition. Γ′_{p} and Γ′_{q} are the updated annotation maps for the corresponding right-hand side threads.

The local consistency of Γ′_{p} follows by Lemma 2.

For Γ′_{q}, we need to show local consistency at each occurrence q : j. Since the thread q is understood, we write j instead of q : j in the following discussion.

Suppose Var(j).

The only constraint is that if k is the binding occurrence for j, then P_{k}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}}. If j has no binding occurrence, the constraint is satisfied. Otherwise, let k be the binding occurrence for j. Since the context hole in C′[ ] is not in a function body, either j and k are both in the context C′[ ], otherwise both are occurrences in the transmitted value V. In either case, by Lemma 6(1), Var(opred(j)). Suppose both j and k are occurrences in the context. opred(k) must have been the binding occurrence for opred(j), and by the local consistency of Γ_{q}, P_{opred(k)}^{Γ_{q}} ≤^{→} P_{opred(j)}^{Γ_{q}}.

Since neither opred(j) nor opred(k) is a value substitution, P_{k}^{Γ′_{q}} = P_{opred(k)}^{Γ_{q}}, and

P_{j}^{Γ′_{q}} = P_{opred(j)}^{Γ_{q}}. Hence, P_{k}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}}. A similar analysis holds if both j and k are occurrences in V, using the local consistency of Γ_{p}.

Suppose Channel(j).

By Lemma 6(1), also Channel(opred(j)). opred(j) may have been the transmitted value or a subterm of the transmitted value, so opred(j) may have been an occurrence in either p or q. Assume opred(j) was in p; the case for q is similar. By the local consistency of Γ_{p}, lab(opred(j)) ∈ κ_{opred(j)}^{Γ_{p}}. By Lemma 6(4),

P_{opred(j)}^{Γ_{p}} ≤^{→} P_{j}^{Γ′_{q}}, so κ_{opred(j)}^{Γ_{p}} ⊆ κ_{j}^{Γ′_{q}}. Therefore, lab(opred(j)) ∈ κ_{j}^{Γ′_{q}}. By

Lemma 6(2), lab(j) = lab(opred(j)). Hence lab(j) ∈ κ_{j}^{Γ′_{q}}.

Suppose Fun(j).

We have the constraint that lab(j) ∈ ϕ_{j}^{Γ′_{q}}. We can use similar reasoning as just presented for occurrences of channel().

The next constraint is that if the number of free occurrences of the procedure binder in the procedure body is greater than 1, then ν_{j.bv}^{Γ′_{q}} = ∞. Again we observe that opred(j) is an occurrence in one of the left-hand side terms q or p. We claim that in opred(j), the number of free occurrences of its binder in its body is the same as for j. To see this, note that the context hole in C′[ ] cannot be in the body of a function; hence j and opred(j) must be occurrences of the same function. So suppose that opred(j) is an occurrence from the p term; in this case, j must be a subterm of V. By the local consistency of Γ_{p}, ν_{opred(j).bv}^{Γ_{p}} = ∞. By Lemma 6(4),

P_{j.bv}^{Γ′_{q}} ≤^{→} P_{opred(j).bv}^{Γ_{p}}. By the ≤^{→}-order on propositions, ν_{opred(j).bv}^{Γ_{p}} ≤ ν_{j.bv}^{Γ′_{q}}, so ν_{j.bv}^{Γ′_{q}} = ∞. A similar analysis works for the case that opred(j) is an occurrence from the q thread, using the local consistency of Γ_{q}.

Next consider the escape constraints that are triggered if θ_{j}^{Γ′_{q}} = escape^{±}. Assume the condition holds. Suppose that opred(j) is an occurrence from the p thread on the left-hand side. Since P_{opred(j)}^{Γ_{p}} ≤^{→} P_{j}^{Γ′_{q}}, we have θ_{j}^{Γ′_{q}} ≤ θ_{opred(j)}^{Γ_{p}}. Therefore, θ_{opred(j)}^{Γ_{p}} = escape^{±}, and the escape constraints hold in Γ_{p} at opred(j). The analysis to show that θ_{opred(j)}^{Γ_{q}} = escape^{±} is similar in the case that opred(j) is an occurrence from the q thread on the left-hand side; the analysis to show the escape constraints hold in Γ′_{q} at opred(j) as a consequence is similar to the analysis in the following discussion.

We begin by showing that for all free variable occurrences j.k, θ_{j.k}^{Γ′_{q}} = escape^{±},

and, if σ_{j.k}^{Γ′_{q}} = reach^{±}, then ω_{j.k}^{Γ′_{q}} = local^{±}. Assume the condition holds for the latter constraint. Now, opred(j.k) was a free variable occurrence in opred(j), since, as we reasoned earlier, j and opred(j) are occurrences of the same function. By the local consistency of Γ_{p}, θ_{opred(j.k)}^{Γ_{p}} = escape^{±}. Since it is a variable and not a value, opred(j.k) cannot have been a value substitution. By Lemma 6(5), P_{opred(j.k)}^{Γ_{p}} = P_{j.k}^{Γ′_{q}}, so also θ_{j.k}^{Γ′_{q}} = escape^{±}. Also by Lemma 6(5), σ_{opred(j.k)}^{Γ_{p}} = reach^{±}. By the local consistency of Γ_{p}, ω_{opred(j.k)}^{Γ_{p}} = local^{±}. Once more by

Lemma 6(5), ω_{j.k}^{Γ′_{q}} = local^{±}.

Next is the constraint for all channel constant occurrences j.m that if σ_{j.m}^{Γ′_{q}} =

reach^{±}, then ω_{j.m}^{Γ′_{q}} = local^{±}. We can use the same reasoning as for the comparable constraint for free variables. However, since it is a value, a channel constant may be a value substitution. But opred(j.m) cannot have been a value substitution here, since j and opred(j) are the same function. So the analysis we used for free variables remains valid for channel constants.

Next we show that Γ′_{q} is remote-expectant at j. Consider any pair of possible communications partners such that exactly one of the pair is a subterm of j. We want to show that in Γ′_{q}, the body of the send() occurrence has a θ annotation of escape^{±}, and that if the receive() occurrence has a σ annotation of reach^{±}, then its ω annotation is local^{±}. By Lemma 9, the occurrence predecessors of the pair were possible communications partners.

Suppose it is the send() that is a subterm of j, and the receive() is not. The reverse situation is similar. Let these be j.k and m, respectively. opred(j.k) was a subterm of opred(j), so by our assumption that opred(j) was in the p thread, so was opred(j.k). Since opred(j) also had a θ-annotation of escape^{±}, Γ_{p} was remote-expectant at opred(j).

Now consider opred(m), which cannot have been a subterm of opred(j). However, opred(m) may have been from either the p or q threads.

Suppose opred(m) is from p. Then by the remote-expectancy of Γ_{p} at opred(j), θ_{opred(j.k).sbody}^{Γ_{p}} = escape^{±}. By Lemma 7, P_{j.k.sbody}^{Γ′_{q}} ≤^{→} P_{opred(j.k).sbody}^{Γ_{p}},

so by the ≤^{→}-ordering on propositions, θ_{j.k.sbody}^{Γ′_{q}} = escape^{±}. Now assume that

σ_{m}^{Γ′_{q}} = reach^{±}. By Lemma 6(4), P_{opred(m)}^{Γ_{p}} ≤^{→} P_{m}^{Γ′_{q}}. By the ≤^{→}-ordering on propositions, also σ_{opred(m)}^{Γ_{p}} = reach^{±}. So by the remote-expectancy of Γ_{p}, ω_{opred(m)}^{Γ_{p}} = local^{±}. Since a receive() cannot be a value substitution, by

Lemma 6(5), also ω_{m}^{Γ′_{q}} = local^{±}.

Now suppose opred(m) is from q. We can use similar reasoning as just presented for the case that opred(m) is from p, except that we rely on the distributed remote-expectancy of G at opred(j).

Last for the escape constraints, we show the nonlinear-expectancy of Γ′_{q} at j.

Assume ν_{j}^{Γ′_{q}} = ∞, else we are done. By Lemma 6(4), P_{opred(j)}^{Γ_{p}} ≤^{→} P_{j}^{Γ′_{q}}, so also θ_{opred(j)}^{Γ_{p}} = ∞. Therefore, Γ_{p} was nonlinear-expectant at opred(j). Consider now a send() occurrence j.k with a possible communications partner m also a subterm of j. Both opred(j.k) and opred(m) must have been subterms of opred(j). By Lemma 9, opred(j.k) and opred(m) were possible communications partners. By the nonlinear-expectancy of Γ_{p} at opred(j), θ_{opred(j.k).sbody}^{Γ_{p}} was escape^{±}. By

Lemma 7 and the ≤^{→}-order on propositions, also θ_{j.k.sbody}^{Γ′_{q}} = escape^{±}. Now assume

σ_{m}^{Γ′_{q}} = reach^{±}. By Lemma 6(4), P_{opred(m)}^{Γ_{p}} ≤^{→} P_{m}^{Γ′_{q}}, hence σ_{m}^{Γ′_{q}} ≤ σ_{opred(m)}^{Γ_{p}}. So also σ_{opred(m)}^{Γ_{p}} = reach^{±}, and by the nonlinear-expectancy of Γ_{p} at opred(j), ω_{opred(m)}^{Γ_{p}} = local^{±}. Since a receive() cannot be a value substitution, by

Lemma 6(5), also ω_{m}^{Γ′_{q}} = local^{±}.

Finally, we have the constraint that if ν_{j}^{Γ′_{q}} = ∞, then all free variable and function subterms of j have a ν-annotation of ∞. Suppose the condition holds. Again, opred(j) may have been in the p or q threads on the left-hand side. Assume opred(j) was in the q thread; the analysis for the case that it was in the p thread is similar. By Lemma 6(4) and the ≤^{→}-order on propositions, also ν_{opred(j)}^{Γ_{q}} = ∞. Let j.k be a free variable or function occurrence in j. Now, opred(j.k) = opred(j).k, since j and opred(j) are the same function. If j.k is a free variable in j, then opred(j.k) was a free variable in opred(j). By the local consistency of Γ_{q}, opred(j).k had a ν-annotation of ∞. opred(j.k) was not a value substitution, so by Lemma 6(5), P_{j.k}^{Γ′_{q}} = P_{opred(j.k)}^{Γ_{q}} = P_{opred(j).k}^{Γ_{q}}. Hence ν_{j.k}^{Γ′_{q}} = ∞.

Suppose App(j).

The first set of constraints requires that for all k such that lab(k) ∈ ϕ_{j.rator}^{Γ′_{q}}, P_{j.rand}^{Γ′_{q}} ≤^{→} P_{k.bv}^{Γ′_{q}} and P_{k.body}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}}. By Lemma 6(1), App(opred(j)).

Consider any function occurrence k from the right-hand side thread q such that lab(k) ∈ ϕ_{j.rator}^{Γ′_{q}}. Now, opred(j).rator may be an occurrence in either the p or q threads. Assume it is in p; the case for q is similar. By Lemma 7, P_{j.rator}^{Γ′_{q}} ≤^{→} P_{opred(j).rator}^{Γ_{p}}. By the ≤^{→}-order on propositions, ϕ_{j.rator}^{Γ′_{q}} ⊆ ϕ_{opred(j).rator}^{Γ_{p}}, so lab(k) ∈ ϕ_{opred(j).rator}^{Γ_{p}}. By Lemma 6(2), lab(k) = lab(opred(k)), so lab(opred(k)) ∈ ϕ_{opred(j).rator}^{Γ_{p}}. opred(k) need not be an occurrence in p; it may be from q.

First suppose opred(k) is from p. Then by the local consistency of Γ_{p}, P_{opred(j).rand}^{Γ_{p}} ≤^{→} P_{opred(k).bv}^{Γ_{p}} and P_{opred(k).body}^{Γ_{p}} ≤^{→} P_{opred(j)}^{Γ_{p}}. Since opred(k).bv is not the site of a substitution, by Lemma 8(2), P_{k.bv}^{Γ′_{q}} = P_{opred(k).bv}^{Γ_{p}}. By Lemma 7, P_{j.rand}^{Γ′_{q}} ≤^{→} P_{opred(j).rand}^{Γ_{p}}. Hence, P_{j.rand}^{Γ′_{q}} ≤^{→} P_{k.bv}^{Γ′_{q}}. By Lemma 7, P_{k.body}^{Γ′_{q}} ≤^{→} P_{opred(k).body}^{Γ_{p}}. By Lemma 6(4), P_{opred(j)}^{Γ_{p}} ≤^{→} P_{j}^{Γ′_{q}}. Hence, P_{k.body}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}}.

Now suppose opred(k) is from q. Then by the communicative consistency of G, P_{opred(j).rand}^{Γ_{p}} ≤^{→} P_{opred(k).bv}^{Γ_{q}} and P_{opred(k).body}^{Γ_{q}} ≤^{→} P_{opred(j)}^{Γ_{p}}. From here, we may reason as in the case that opred(k) is from p, mutatis mutandis.

Suppose Cond(j).

By Lemma 6(1), also Cond(opred(j)). Now, opred(j) is either from p or from q. Suppose opred(j) is from q; the other case is similar. So also opred(j).then and opred(j).else are from q. Because Γ_{q} is locally consistent, P_{opred(j).then}^{Γ_{q}} ≤^{→} P_{opred(j)}^{Γ_{q}} and P_{opred(j).else}^{Γ_{q}} ≤^{→} P_{opred(j)}^{Γ_{q}}. By Lemma 7, P_{j.then}^{Γ′_{q}} ≤^{→} P_{opred(j).then}^{Γ_{q}} and P_{j.else}^{Γ′_{q}} ≤^{→} P_{opred(j).else}^{Γ_{q}}. By Lemma 6(4), P_{opred(j)}^{Γ_{q}} ≤^{→} P_{j}^{Γ′_{q}}. Hence, P_{j.then}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}} and

P_{j.else}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}}.

Suppose RFork(j).

In the Fun subcase above, under the assumption that θ_{j}^{Γ′_{q}} = escape^{±}, we showed that θ for opred(j) was also escape^{±}. By the local consistency of Γ_{p}, or Γ_{q}, depending on the location of opred(j), we showed that the escape constraints held for opred(j) and its subterms. That was sufficient to show that the escape constraints held for j and its subterms.

We want to show that for all k such that lab(k) ∈ ϕ_{j.rffun}^{Γ′_{q}}, the escape constraints hold at k. Consider such a k. By Lemma 6(2), lab(k) = lab(opred(k)). By Lemma 6(1), also RFork(opred(j)). If opred(j).rffun is from p, we have by Lemma 7, ϕ_{j.rffun}^{Γ′_{q}} ⊆ ϕ_{opred(j).rffun}^{Γ_{p}}, so lab(opred(k)) ∈ ϕ_{opred(j).rffun}^{Γ_{p}}. Therefore, if opred(k) is also in p, we have satisfaction of the escape constraints in Γ_{p} at opred(k). By the same reasoning we used in the Fun subcase above, we also have satisfaction of the escape constraints in Γ′_{q} at k. The case that both opred(j).rffun and opred(k) are in q is similar, using the local consistency of Γ_{q}.

However, the quantification over all k in the constraint introduces a slight difficulty. It might be that opred(j).rffun is from p, but opred(k) is from q, or vice-versa. In those cases, the local consistency of Γ_{p} and Γ_{q} does not tell us that the escape constraints held at opred(k). Recall, universal quantifiers appearing in the local constraints range over occurrences in individual threads. Therefore, for these cases, we rely on the comparable communicative consistency constraint for RFork(j) to show that the escape constraints hold at opred(k). So in these cases also, the escape constraints hold in Γ′_{q} at k.

Suppose Send(j).

The constraint is that σ_{j.schan}^{Γ′_{q}} = reach^{±}. By Lemma 6(1), also Send(opred(j)). Suppose opred(j) is from q. Since Γ_{q} is locally consistent, σ_{opred(j).schan}^{Γ_{q}} = reach^{±}. By Lemma 7, P_{j.schan}^{Γ′_{q}} ≤^{→} P_{opred(j).schan}^{Γ_{q}}. By the ≤^{→}-order on propositions, σ_{j.schan}^{Γ′} = reach^{±}. The case that opred(j) is from p is similar.

Suppose Receive(j).

The first constraint is that σ_{j.rchan}^{Γ′_{q}} = reach^{±}. Use similar reasoning as in the Send subcase for the constraint on σ annotations.

Now consider a k from the right-hand side q term, such that Send(k), κ_{k.schan}^{Γ′_{q}} ∩ κ_{j.rchan}^{Γ′_{q}} ≠ ∅. By Lemma 6(1), also Send(opred(k)). By Lemma 9, opred(j) and opred(k) were communications partners.

Suppose first that opred(j) and and opred(k).sbody were both from q. By the local consistency of Γ_{q}, P_{opred(k).sbody}^{Γ_{q}} ≤^{→} P_{opred(j)}^{Γ_{q}}. By Lemma 7, P_{k.sbody}^{Γ′_{q}} ≤^{→}

P_{opred(k).sbody}^{Γ_{q}}, and by Lemma 6(4) P_{opred(j)}^{Γ_{q}} ≤^{→} P_{j}^{Γ′_{q}}. Hence, P_{k.sbody}^{Γ′_{q}} ≤^{→} P_{j}^{Γ′_{q}}. The case that both opred(j) and and opred(k).sbody were from p is similar.

Suppose instead that opred(j) was from p, but opred(k).sbody was from q. By the communicative consistency of G, P_{opred(k).sbody}^{Γ_{q}} ≤^{→} P_{opred(j)}^{Γ_{p}}. By Lemma 7,

P_{k.sbody}^{Γ′_{q}} ≤^{→} P_{opred(k).sbody}^{Γ_{q}} and by Lemma 6(4), P_{opred(j)}^{Γ_{p}} ≤^{→} P_{j}^{Γ′_{q}}. Hence, P_{k.sbody}^{Γ′_{q}} ≤^{→}

P_{j}^{Γ′_{q}}. The case that opred(j) was from q and opred(k).sbody was from p is similar.

Our last invariance result is:

Theorem 3 Let Π be a thread map with a family of annotation maps G that is locally consistent, communicative consistent, and κ-coherent. Suppose Π ⟶_{con} Π′.

Then the updated family of annotation maps G′ is communicative consistent for Π′.

Proof. By considering each possible ⟶_{con} -transition and G′, the updated family of annotation maps.

For each possible ⟶_{con} -transition, we check the communicative consistency of the annotation map or maps at each occurrence r : j on the right-hand side, where r is an arbitrary thread. Assume each transition is as in Figures 6 to 12. As before, an unprimed Γ_{s} is the annotation map for a left-hand side thread s; Γ′_{s} is the updated annotation map for s on the right-hand side.

case seq/β

As shown in Figure 6, the β-reduction occurs in thread p.

Suppose Fun(r : j).

We want to show that if θ_{r:j}^{Γ′_{r}} = escape^{±}, then G′ is distributed remoteexpectant at r : j. Assume the condition holds. Since no communication between threads occurs, opred(r : j) is in the thread r on the left-hand side. By Lemma 6(4), P_{opred(r : j)}^{Γ_{r}} ≤^{→} P_{r:j}^{Γ′_{r}}, so by the ≤^{→}-order on propositions, also θ_{opred(r : j)}^{Γ_{r}} = escape^{±}. Since also Fun(opred(r : j)), by the communicative consistency of G, G was distributed remote-expectant at opred(r : j).

Consider a receive() that is a subterm of r : j, say r : j.k, and a send(), say s : m, such that r : j.k and s : m are possible communications partners. By Lemma 9, opred(r : j.k) and opred(s : m) were possible communications partners. Note that r : j.k and s : m may be in the same or in different threads.

Suppose that opred(r : j.k) was a subterm of opred(r : j).

Suppose first that opred(s : m) was not a subterm of opred(r : j), including the possibility the two occurrences were in different threads. By the distributed remote-expectancy of G at opred(r : j), θ_{opred(s : m).sbody}^{Γ_{s}} = escape^{±}. By

Lemma 7, P_{s:m.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : m).sbody}^{Γ_{s}}, so θ_{opred(s : m).sbody}^{Γ_{s}} ≤ θ_{s:m.sbody}^{Γ′_{s}}. Therefore,

θ_{s:m.sbody}^{Γ′_{s}} = escape^{±}. Assume that σ_{r:j.k}^{Γ′_{r}} = reach^{±}. Since a receive() is not a value, by Lemma 6(5), P_{opred(r : j.k)}^{Γ_{r}} = P_{r:j.k}^{Γ′_{r}}. Hence, σ_{opred(r : j.k)}^{Γ_{r}} = reach^{±}. Then by the distributed remote-expectancy of G at opred(r : j), ω_{opred(r : j.k)}^{Γ_{r}} = local^{±}.

So also ω_{r:j.k}^{Γ′_{r}} = local^{±}.

Now suppose that opred(s : m) was a subterm of opred(r : j). Therefore, s = r. In this case, it must have been that opred(r : j) was duplicated by the β-reduction. The application operand i.rand must have contained opred(r : j), and the operand must have been substituted for a pair of free occurrences of the operator binder [[i.rator.bv]] in the operator body. By the local consistency of Γ_{r}, ν_{i.rator.bv}^{Γ_{r}} = ∞. By the nonlinear-expectancy of Γ_{r} at r : j, θ_{opred(r : m).sbody}^{Γ_{r}} = escape^{±}. By Lemma 7, P_{r:m.sbody}^{Γ′_{r}} ≤^{→} P_{opred(r : m).sbody}^{Γ_{r}},

so θ_{opred(r : m).sbody}^{Γ_{r}} ≤ θ_{r:m.sbody}^{Γ′_{r}}. So also θ_{r:m.sbody}^{Γ′_{r}} = escape^{±}. Now assume

that σ_{r:j.k}^{Γ′_{r}} = reach^{±}. Since a receive() is not a value, by Lemma 6(5), P_{opred(r : j.k)}^{Γ_{r}} = P_{r:j.k}^{Γ′_{r}}. Hence also σ_{opred(r : j.k)}^{Γ_{r}} = reach^{±}. Then by the nonlinear-

expectancy of Γ_{r} at opred(r : j), ω_{opred(r : j.k)}^{Γ_{r}} = local^{±}. So also ω_{r:j.k}^{Γ′_{r}} = local^{±}.

Suppose instead that opred(r : j.k) was a subterm of the substituted operand. We can show that in Γ_{r}, the operand had a θ-annotation of escape^{±}. Therefore, G was distributed remote-expectant at the operand. From here, we can reason as in the case that opred(r : j.k) was a subterm of opred(r : j). We can distinguish the situations where opred(s : m) was and was not a subterm of the operand.

We may reverse the roles of r : j.k and s : m, so that the former is a send() and the latter is a receive(). A similar analysis gives the desired result.

Suppose App(r : j).

We wish to show that for all s ≠ r, for all k such that lab(s : k) ∈ ϕ_{r:j.rator}^{Γ′_{r}},

that P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{s:k.bv}^{Γ′_{s}} and P_{s:k.body}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Consider such a function occurrence s : k. By Lemma 7 and the ≤^{→}-order on propositions, ϕ_{r:j.rator}^{Γ′_{r}} ⊆ ϕ_{opred(r : j).rator}^{Γ_{r}}. By Lemma 6(2), lab(s : k) = lab(opred(s : k)), so lab(opred(s : k)) ∈ ϕ_{opred(r : j).rator}^{Γ_{r}}. Note that opred(s : k) and opred(r : j) were in different threads on the left-hand side. By the communicative consistency of G, P_{opred(r : j).rand}^{Γ_{r}} ≤^{→} P_{opred(s : k).bv}^{Γ_{s}} and P_{opred(s : k).body}^{Γ_{s}} ≤^{→}

P_{opred(r : j)}^{Γ_{r}}. By Lemma 7, P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{opred(r : j).rand}^{Γ_{r}}. Since opred(s : k).bv can-

not have been the site of a substitution, by Lemma 8(2), P_{s:k.bv}^{Γ′_{s}} = P_{opred(s : k).bv}^{Γ_{s}}.

Therefore, P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{s:k.bv}^{Γ′_{s}}. By Lemma 7, P_{s:k.body}^{Γ_{s}} ≤^{→} P_{opred(s : k).body}^{Γ_{s}}. By

Lemma 6(4), P_{opred(r : j)}^{Γ_{r}} ≤^{→} P_{r:j}^{Γ′_{r}}. Hence P_{s:k.body}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Suppose RFork(r : j).

First we want to show that for all s and k such that lab(s : k) ∈ ϕ_{r:j.rffun}^{Γ′_{r}}, that G′ is distributed remote-expectant at s : k.

Choose any such occurrence s : k. opred(r : j) was an occurrence of an rfork() in the r thread on the left-hand side. By Lemma 7, P_{r:j.rffun}^{Γ′_{r}} ≤^{→} P_{opred(r : j).rffun}^{Γ_{r}}. Therefore, ϕ_{r:j.rffun}^{Γ′_{r}} ⊆ ϕ_{opred(r : j).rffun}^{Γ_{r}}. Also, by Lemma 6(2), lab(s : k) = lab(opred(s : k)). So lab(opred(s : k)) ∈ ϕ_{opred(r : j).rffun}^{Γ_{r}}. By the communicative consistency of G, G was distributed remote-expectant at opred(s : k). From here, we may reason as we did in the Fun subcase for the distributed remote-expectancy constraint.

Next we want to show that for all s ≠ r, for all k such that lab(s : k) ∈ r : j.rffun, that the escape constraints hold in Γ′_{s} at s : k.

Consider such a function occurrence s : k. By Lemma 7, P_{r:j.rffun}^{Γ′_{r}} ≤^{→} P_{opred(r : j).rffun}^{Γ_{r}}. So ϕ_{r:j.rffun}^{Γ′_{r}} ⊆ ϕ_{opred(r : j).rffun}^{Γ_{r}}. Also, by Lemma 6(2), lab(opred(s : k)) = lab(s : k), so lab(opred(s : k)) ∈ ϕ_{opred(r : j).rffun}^{Γ_{r}}. By the communicative consistency of G, the escape constraints held at opred(s : k). Now, if s ≠ p, then the s thread is the same on both sides of the transition, and Γ_{s} = Γ′_{s}, so clearly the escape constraints must also hold at s : k. But suppose s = p. In this case, as we showed for Theorem 2 in the Fun case for a seq/β transition, if the escape constraints held at the occurrence predecessor of a right-hand side function occurrence, then the escape constraints also hold at the function occurrence itself.

Suppose Receive(r : j).

We want to show that for all s ≠ r, for all k such that Send(s : k), if r : j and s : k are possible communications partners, then (1) P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}, and (2) proc_{Π′}(r) ≠ proc_{Π′}(s) implies θ_{s:k.sbody}^{Γ′_{s}} = escape^{±}, and if σ_{r:j}^{Γ′_{s}} = reach^{±}, then ω_{r:j}^{Γ′_{s}} = local^{±}.

By Lemma 9, opred(r : j) and opred(s : k) were also communications partners. Since these occurrence predecessors were also in the r and s threads, respectively, by the communicative consistency of G, P_{opred(s : k).sbody}^{Γ_{s}} ≤^{→} P_{opred(r : j)}^{Γ_{r}}.

By Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{s}}. By Lemma 6(4), P_{opred(r : j)}^{Γ_{r}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Hence, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Now suppose proc_{Π′}(r) ≠ proc_{Π′}(s). Then also proc_{Π}(r) ≠ proc_{Π}(s). By the communicative consistency of G, θ_{opred(s : k).sbody}^{Γ_{s}} = escape^{±}. By Lemma 7,

P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{s}}. By the ≤^{→}-order on propositions, also θ_{s:k.sbody}^{Γ′_{s}} =

escape^{±}. Since a receive() cannot be a value substitution, P_{opred(r : j)}^{Γ_{s}} = P_{r:j}^{Γ′_{s}}.

Assume σ_{r:j}^{Γ′_{s}} = reach^{±}. Then also σ_{opred(r : j)}^{Γ_{s}} = reach^{±}. By the communicative

consistency of G, ω_{opred(r : j)}^{Γ_{s}} = local^{±}. So also ω_{r:j}^{Γ′_{s}} = local^{±}.

case seq/cond-true

We omit the similar seq/cond-false case.

Suppose Fun(r : j).

We want to show that if θ_{r:j}^{Γ′_{r}} = escape^{±}, then G′ is distributed remoteexpectant at r : j. We can use almost the same analysis as in the seq/β case. Since the conditional reduction does not involve substitution for a free variable, if we have an occurrence r : j.k that is a subterm of r : j, then opred(r : j.k) is certainly a subterm of opred(r : j). Also, if an occurrence s : m is not a subterm of r : j, then opred(s : m) is certainly not a subterm of opred(r : j). Therefore, we can exclude some of the possibilities we considered in the seq/β case. In particular, we need not consider the possibility of duplicated terms.

Suppose App(r : j).

Use the same reasoning as in the App subcase for seq/β transitions.

Suppose RFork(r : j).

First we wish to show that for all s and k such that lab(s : k) ∈ ϕ_{r:j.rffun}^{Γ′_{r}}, that G′ is distributed remote-expectant at s : k. As in the Fun subcase above, we may follow the reasoning used in the seq/β case for the Fun and RFork subcases, excluding the irrelevant situations.

Next, we wish to show that for all s ≠ r, for all k such that lab(s : k) ∈ r : j.sbody, that the escape constraints hold in Γ′_{s} at s : k.

Consider such a function occurrence s : k. We can show that lab(opred(s : k)) ∈ ϕ_{opred(r : j).sbody}^{Γ_{r}}. By the communicative consistency of G, the escape constraints held at opred(s : k). If s ≠ p, then the s term is the same on both sides of the transition, also Γ_{s} = Γ′_{s}, so the escape constraints hold at s : k. Suppose instead s = p. As we showed in Theorem 2 in the Fun subcase for a seq/cond-true transition, if the escape constraints held at the occurrence predecessor of a right-hand function occurrence, such as s : k, then the escape constraints also hold at the function occurrence itself.

Suppose Receive(r : j).

Use the same reasoning as in the Receive subcase for seq/β transitions.

case channel

We have G = G′. All that is different between the left-hand and right-hand sides is the fresh channel constant in the thread p, which replaces an occurrence of channel(). The only communicative consistency constraint that might apply to that channel constant is the escape constraint that applies to channel constants in function bodies. Since the context hole in the p thread cannot be in the body of the function, in fact that constraint does not apply. Since G was communicative consistent, so is G′.

case fork

Suppose Fun(r : j).

We want to show that if θ_{r:j}^{Γ′_{r}} = escape^{±}, then G′ is distributed remoteexpectant at r : j. Assume the condition holds. Now, opred(r : j) may be from the thread r, but if r is the child thread, then opred(r : j) is an occurrence in the parent thread. In Figure 10, p is the parent thread. Let r′ be the left-hand side thread containing opred(r : j), so either r′ = r or r′ = p. By Lemma 6(4), P_{opred(r : j)}^{Γ_{r′}} ≤^{→} P_{r:j}^{Γ′_{r}}, so also θ_{opred(r : j)}^{Γ_{r′}} = escape^{±}. By the communicative consistency of G, G was distributed remote-expectant at opred(r : j).

Consider a receive() that is a subterm of r : j, say r : j.k, and a send() occurrence, say s : m, that is not a subterm of r : j. As usual, the situation where the send() is a subterm of r : j and the receive() is not a subterm is similar. Assume the occurrences are possible communications partners. By Lemma 9, opred(r : j.k) and opred(s : m) were possible communications partners.

Now, opred(r : j.k) and opred(s : m) may have been in in the same or in distinct threads on the left-hand side. In either case, however, opred(r : j.k) is certainly a subterm of opred(r : j), and opred(s : m) was certainly not a subterm of opred(r : j). This is the same situation we had in the seq/cond-true case, so the reasoning we used there for this constraint applies.

Suppose App(r : j).

We want to show that for all s ≠ r, for all k such that lab(s : k) ∈ ϕ_{r:j.rator}^{Γ′_{r}},

that P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{s:k.bv}^{Γ′_{s}} and P_{s:k.body}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Consider a function occurrence s : k such that lab(s : k) ∈ ϕ_{r:j.rator}^{Γ′_{r}}. If opred(r : j) and opred(s : k) are in distinct threads on the left-hand side, then use the same reasoning as in the App subcases for seq/β and seq/cond-true transitions.

If opred(r : j) and opred(s : k) are not in distinct threads, then they must both have been occurrences in the parent thread p. We know App(opred(r : j)). By Lemma 7 and the ≤^{→}-order on propositions, ϕ_{r:j.rator}^{Γ′_{r}} ⊆ ϕ_{opred(r : j).rator}^{Γ_{p}}. By Lemma 6(2), lab(s : k) = lab(opred(s : k)), so lab(opred(s : k)) ∈ ϕ_{opred(r : j).rator}^{Γ_{p}}. Therefore, by the local consistency of Γ_{p}, P_{opred(r : j).rand}^{Γ_{p}} ≤^{→}

P_{opred(s : k).bv}^{Γ_{p}} and P_{opred(s : k).body}^{Γ_{p}} ≤^{→} P_{opred(r : j)}^{Γ_{p}}. By Lemma 7, P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{opred(r : j).rand}^{Γ_{p}}. opred(s : k).bv cannot have been the site of a substitution,

so by Lemma 8(2), P_{s:k.bv}^{Γ′_{s}} = P_{opred(s : k).bv}^{Γ_{p}}. Therefore, P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{s:k.bv}^{Γ′_{s}}. By

Lemma 7, P_{s:k.body}^{Γ_{s}} ≤^{→} P_{opred(s : k).body}^{Γ_{p}}. By Lemma 6(4), P_{opred(r : j)}^{Γ_{p}} ≤^{→} P_{r:j}^{Γ′_{r}}. Hence,

P_{s:k.body}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Suppose RFork(r : j).

First we wish to show that for all s and k such that lab(s : k) ∈ ϕ_{r:j.rffun}^{Γ′_{r}}, that G′ is distributed remote-expectant at s : k.

Choose any such occurrence s : k. As in the seq/β and seq/cond-true cases, we can show that G was distributed remote-expectant at opred(s : k). From here, we may reason as in the seq/cond-true case, observing that there is no possibility of term duplication.

Next, we show that for all s ≠ r and all k such that lab(s : k) ∈ ϕ_{r:j.rffun}^{Γ′_{r}}, that the escape constraints hold in Γ′_{s} at s : k.

Consider such a function occurrence s : k. Let r′ be the thread where opred(r : j) occurred on the left-hand side. We can show, as in the seq/β and seq/cond-true cases, that lab(opred(s : k)) ∈ ϕ_{opred(r : j).rffun}^{Γ_{r′}}.

Suppose opred(r : j) and opred(s : k) were occurrences in distinct threads on the left-hand side. Then by the communicative consistency of G, the escape constraints held at opred(s : k). As we showed in Theorem 2 in the Fun subcase for fork transitions, since the escape constraints held at opred(s : k), the escape constraints also hold at s : k.

On the other hand, suppose opred(r : j) and opred(s : k) were both in the parent thread p on the left-hand side. Then by the local consistency of Γ_{p}, the escape constraints held at opred(s : k). So again, the escape constraints also hold at s : k.

Suppose Receive(r : j).

We want to show that for all s ≠ r, for all k such that Send(s : k), if r : j and s : k are possible communications partners, then (1) P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}, and (2) proc_{Π′}(r) ≠ proc_{Π′}(s) implies that θ_{s:k.sbody}^{Γ′_{s}} = escape^{±} and that σ_{r:j}^{Γ′_{s}} = reach^{±} implies ω_{r:j}^{Γ′_{s}} = local^{±}.

By Lemma 9, opred(r : j) and opred(s : k) were also possible communications partners. Suppose these occurrence predecessors were in distinct threads. Then by the communicative consistency of G, P_{opred(s : k).sbody}^{Γ_{s′}} ≤^{→} P_{opred(r : j)}^{Γ_{r′}}, where s′ and r′ are the appropriate left-hand side threads. By Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{s′}}. By Lemma 6(4), P_{opred(r : j)}^{Γ_{r′}} ≤^{→} P_{r:j}^{Γ′_{r}}. Therefore,

P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Suppose instead that these occurrence predecessors were both in the parent thread p. So by the local consistency of Γ_{p}, P_{opred(s : k).sbody}^{Γ_{p}} ≤^{→} P_{opred(r : j)}^{Γ_{p}}. By

Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{p}}. By Lemma 6(4), P_{opred(r : j)}^{Γ_{p}} ≤^{→} P_{r:j}^{Γ′_{r}}. So

P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Now suppose proc_{Π′}(r) ≠ proc_{Π′}(s). Suppose that r and s were also threads on the left-hand side. In that case, opred(r : j) was in the r thread on the lefthand side, and opred(s : k) was in the s thread. Also, proc_{Π}(r) ≠ proc_{Π}(s), so we may reason as in the seq/β and seq/cond-true cases for the same constraint.

But suppose that not both of r and s were threads on the left-hand side. One of r and s must be the child thread, and the other is a thread other than the parent thread. Suppose r is the child thread. Then on the left-hand side, opred(r : j) was an occurrence in the parent thread and opred(s : k) was an occurrence in the s thread. Since proc_{Π′}(r) ≠ proc_{Π′}(s) and the child thread runs on the same processor as its parent, we have proc_{Π}(p) ≠ proc_{Π}(s). Suppose instead that s is the child thread. Then on the left-hand side, opred(s : k) was an occurrence in the parent thread and opred(r : j) was an occurrence in the r thread. So again proc_{Π}(p) ≠ proc_{Π}(r). From this point, we may reason much as in the seq/β and seq/cond-true cases for this same constraint. Since the occurrence predecessor of the child thread is in the parent thread, we just need to substitute Γ_{p} at relevant points in the proof in place of Γ_{r} or Γ_{s}.

case rfork

Suppose Fun(r : j).

Use the same reasoning as in the Fun subcase for fork transitions.

Suppose App(r : j).

Use the same reasoning as in the App subcase for fork transitions.

Suppose RFork(r : j).

Use the same reasoning as in the RFork subcase for fork transitions.

Suppose Receive(r : j).

We want to show that for all s ≠ r, for all k such that Send(s : k), if r : j and s : k are possible communications partners, then (1) P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}, and (2) proc_{Π′}(r) ≠ proc_{Π′}(s) implies θ_{s:k.sbody}^{Γ′_{s}} = escape^{±}, and σ_{r:j}^{Γ′_{s}} = reach^{±} implies ω_{r:j}^{Γ′_{s}} = local^{±}.

For (1), we may reason exactly as in the Receive subcase for fork transitions.

Suppose that proc_{Π′}(r) ≠ proc_{Π′}(s). Suppose also that r and s were distinct threads on the left-hand side. Then proc_{Π}(r) ≠ proc_{Π}(s). From here, we may reason as in the seq/β, seq/cond-true, and fork cases for the same constraint.

But suppose that not both of r and s were threads on the left-hand side. One of r and s must be the child thread; the other may be the parent thread, or another thread. If opred(r : j) and opred(s : k) occurred in threads on different processors, then again we may reason as in the seq/β, seq/cond-true, and fork cases.

Suppose now that the two occurrence predecessors were in threads on the same processor.

Suppose that r is the child thread. Then opred(r : j) must have been a subterm of the rfork()’d function.

One possibility is that opred(s : k) is also an occurrence in the parent thread. opred(s : k) was not a subterm of the rfork()’d function. By the local consistency of Γ_{p}, Γ_{p} was remote-expectant at the rfork()’d function. By Lemma 9, opred(r : j) and opred(s : k) were possible communications partners. By the remote-expectancy of Γ_{p}, θ_{opred(s : k).sbody}^{Γ_{p}} = escape^{±}. By Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{p}}. By the ≤^{→}-order on propositions, also θ_{s:k.sbody}^{Γ′_{s}} = escape^{±}.

Assume σ_{r:j}^{Γ′_{r}} = reach^{±}. Since a receive() is not a value, by Lemma 6(5),

P_{r:j}^{Γ_{r}} = P_{opred(r : j)}^{Γ′_{p}}. So also σ_{opred(r : j)}^{Γ_{p}} = reach^{±}. By the remote-expectancy

of Γ_{p}, ω_{opred(r : j)}^{Γ_{p}} = local^{±}. So also ω_{r:j}^{Γ′_{r}} = local^{±}.

The other possibility is that opred(s : k) is an occurrence in a thread different from the parent thread, but running on the same processor as the parent thread. In this case, the distributed remote-expectancy of G at the rfork()’d function gives the desired results.

Suppose s is the child thread. Therefore, opred(s : k) must have been a subterm of the rfork()’d function.

One possibility is that opred(r : j) is also an occurrence in the parent thread. opred(r : j) was not a subterm of the rfork()’d function. From here, we may reason as in the case that r is the child thread, and opred(s : k) was also in the parent thread.

The other possibility is that opred(r : j) is an occurrence in a thread different than the parent thread, but running on the same processor as the parent thread. Once more, the distributed remote-expectancy of G at the rfork()’d function gives the desired results.

case comm

Suppose Fun(r : j).

We want to show that if θ_{r:j}^{Γ′_{r}} = escape^{±}, then G′ is distributed remoteexpectant at r : j. Assume the condition holds. Since a value is transmitted, opred(r : j) may be from a left-hand side thread other than r. Let r′ be the thread in which opred(r : j) occurs. By Lemma 6(4), P_{opred(r : j)}^{Γ_{r′}} ≤^{→} P_{r:j}^{Γ′_{r}}, so by

the ≤^{→}-order on propositions, also θ_{opred(r : j)}^{Γ_{r′}} = escape^{±}. By the communicative consistency of G, G was distributed remote-expectant at opred(r : j).

Consider a receive() that is a subterm of r : j, say r : j.k, and a send() occurrence, say s : m, that is not a subterm of r : j. As in the seq/cond-true, fork, and rfork cases, opred(r : j.k) must have been a subterm of opred(r : j), and opred(s : m) must not have been a subterm of opred(r : j). Therefore, we may use the same reasoning as in those cases for this constraint. Reversing the roles of r : j.k and s : m allows to obtain the desired results by a similar analysis.

Suppose App(r : j).

We wish to show that for all s ≠ r, for all k such that lab(s : k) ∈ ϕ_{r:j.rator}^{Γ′_{r}},

that P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{s:k.bv}^{Γ′_{s}} and P_{s:k.body}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Consider such a function occurrence s : k. Now, opred(r : j) could have been in a thread other than r on the left-hand side. Let r′ be that thread. By Lemma 7 and the ordering on propositions, ϕ_{r:j.rator}^{Γ′_{r}} ≤^{→} ϕ_{opred(r : j).rator}^{Γ_{r′}}. By Lemma 6(2), lab(s : k) = lab(opred(s : k)), so lab(opred(s : k)) ∈ ϕ_{opred(r : j).rator}^{Γ_{r′}}. Note that opred(s : k) and opred(r : j) may have been in the same or in different threads on the left-hand side.

Suppose opred(s : k) and opred(r : j) were in different threads on the lefthand side. Let s′ be the thread in which opred(s : k) occurs. By the communicative consistency of G, P_{opred(r : j).rand}^{Γ_{r′}} ≤^{→} P_{opred(s : k).bv}^{Γ_{s′}} and P_{opred(s : k).body}^{Γ_{s′}} ≤^{→}

P_{opred(r : j)}^{Γ_{r′}}. By Lemma 7, P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{opred(r : j).rand}^{Γ_{r′}}. Since opred(s : k).bv can-

not have been the site of a substitution, by Lemma 8(2), P_{s:k.bv}^{Γ′_{s}} = P_{opred(s : k).bv}^{Γ_{s′}}.

Therefore, P_{r:j.rand}^{Γ′_{r}} ≤^{→} P_{s:k.bv}^{Γ′_{s}}. By Lemma 7, P_{s:k.body}^{Γ_{s}} ≤^{→} P_{opred(s : k).body}^{Γ_{s′}}; by

Lemma 6(4), P_{opred(r : j)}^{Γ_{r′}} ≤^{→} P_{r:j}^{Γ′_{r}}. Hence, P_{s:k.body}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Now suppose opred(s : k) and opred(r : j) were in the same thread on the left-hand side. Let t be that thread. The analysis is similar to that in the last paragraph, except that we rely on the local consistency of Γ_{t} instead of the communicative consistency of G.

Suppose RFork(r : j).

We wish to show that for all s and k such that lab(s : k) ∈ ϕ_{r:j.rffun}^{Γ′_{r}}, that G′ is distributed remote-expectant at s : k.

Choose any such occurrence s : k. Let r′ be the thread in which opred(r : j) occurred. We can show that lab(opred(s : k)) ∈ ϕ_{opred(r : j).rffun}^{Γ_{r′}}, so G was distributed remote-expectant at opred(s : k). From here, the analysis is as in the Fun subcase for this constraint.

Next, we wish to show that for all s ≠ r, for all k such that lab(s : k) ∈ r : j.sbody, that the escape constraints hold at s : k.

Consider such a function occurrence s : k. Let r′ be the left-hand side thread where opred(r : j) occurs. We can show, as in previous cases for the same constraint, that lab(opred(s : k)) ∈ ϕ_{opred(r : j).sbody}^{Γ_{r′}}. If opred(r : j) and opred(s : k) were in different threads, then by the communicative consistency of G, the escape constraints held at opred(s : k). If they were in the same thread r′, then the escape constraints held at opred(s : k) by the local consistency of Γ_{r′}. As we showed in Theorem 2 in the Fun subcase for a comm transition, if the escape constraints held at the occurrence predecessor of a right-hand function occurrence, such as s : k, then the escape constraints also hold at the function occurrence itself.

Suppose Receive(r : j).

We want to show that for all s ≠ r, for all k such that Send(s : k), and r : j and s : k are possible communications partners, that (1) P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}, and (2) proc_{Π′}(r) ≠ proc_{Π′}(s) implies θ_{s:k.sbody}^{Γ′_{s}} = escape^{±}, and if σ_{r:j}^{Γ′_{s}} = reach^{±}, then ω_{r:j}^{Γ′_{s}} = local^{±}.

Choose any such s : k. By Lemma 9, opred(r : j) and opred(s : k) were also communications partners. Suppose these occurrence predecessors were in different threads. Then by the communicative consistency of G, P_{opred(s : k).sbody}^{Γ_{s′}} ≤^{→} P_{opred(r : j)}^{Γ_{r′}}, where s′ and r′ are the appropriate left-hand side threads. By

Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{s′}}. By Lemma 6(4), P_{opred(r : j)}^{Γ_{r′}} ≤^{→} P_{r:j}^{Γ′_{r}}. There-

fore, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

The only other possibility is that the occurrence predecessors were both in the send()’ing thread p. So by the local consistency of Γ_{p}, P_{opred(s : k).sbody}^{Γ_{p}} ≤^{→}

P_{opred(r : j)}^{Γ_{p}}. By Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{p}}. By Lemma 6(4),

P_{opred(r : j)}^{Γ_{p}} ≤^{→} P_{r:j}^{Γ′_{r}}. Hence P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{r:j}^{Γ′_{r}}.

Suppose that proc_{Π′}(r) ≠ proc_{Π′}(s). Suppose also that opred(r : j) and opred(s : k) were in distinct threads on different processors on the left-hand side. Then we may reason as in previous cases for the same constraint.

Suppose instead that opred(r : j) and opred(s : k) were in the same thread, or in different threads on the same processor, on the left-hand side. Then on the right-hand side, at least one of r : j and s : k must be running on a processor different than its occurrence predecessor. Therefore, at least one of opred(r : j) and opred(s : k) must have been a subterm of the transmitted value. But if both opred(r : j) and opred(s : k) were such subterms, then on the right-hand side, r : j and s : k would be occurrences in the same thread. Therefore, exactly one of opred(r : j) and opred(s : k) was a subterm of transmitted value. Also, the transmitted value must have been a function.

Consider the communicating send() and receive() on the left-hand side. They must have been in distinct threads on different processors. By the κcoherence of G, the intersection of the κ annotations of the channel-parts of the send() and receive() was non-empty. So by the communicative consistency of G, the transmitted function, which was the body of the send(), had a θ annotation of escape^{±}.

There are now two possibilities to consider: (1) that opred(r : j) and opred(s : k) were both occurrences in the send()’ing thread p, and (2) that one of opred(r : j) and opred(s : k) was an occurrence in p, and the other occurred in some other left-hand side thread.

In the case of (1), by local consistency, Γ_{p} was remote-expectant at the transmitted function. Regardless of which of opred(r : j) and opred(s : k) was the subterm of the transmitted function, by remote-expectancy, θ_{opred(s : k).sbody}^{Γ_{p}} = escape^{±}. By Lemma 7, P_{s:k.sbody}^{Γ′_{s}} ≤^{→} P_{opred(s : k).sbody}^{Γ_{p}}, so θ_{s:k.sbody}^{Γ′_{s}} = escape^{±}.

Assume now that σ_{r:j}^{Γ′_{r}} = reach^{±}. Since a receive() is not a value, P_{r:j}^{Γ′_{r}} = P_{opred(r : j)}^{Γ_{p}}. Hence, by remote-expectancy, ω_{opred(r : j)}^{Γ_{p}} = local^{±}, and also ω_{r:j}^{Γ′_{r}} = local^{±}.

For (2), by the communicative consistency of G, G was distributed remoteexpectant at the transmitted function. From here, we may reason as we did for (1), except that the annotation for one of the occurrence predecessors is not given by Γ_{p}, but by the annotation map for some other left-hand side thread.

13 Soundness

Any solution to the local consistency and communicative consistency constraints that is also κ-coherent is sound. Our main result is:

Theorem 4 (Soundness) Let Π be a thread map with a family of annotation maps G that is locally consistent, communicative consistent, and κ-coherent. If

Π ⟶^{∗}_{con} Π′, then Π ⟶^{∗}_{con} Π′ ⊧ G.

Proof. By Theorems 2 and 3.

Let p : i be an occurrence of channel() in Π that G gives a ω annotation of local^{+}. Let Π′′ be any intermediate thread map in the evaluation, possibly the same as Π′. Suppose there is an occurrence s : n of a channel constant k in Π′′, such that s : n was produced by p : i in Π, and s : n is the channel-part subterm of a send() or the channel-part subterm of a receive(). Suppose further that s : n was directly produced by some r : m in a thread map Π′′′ preceding Π′′ in the evaluation. Then proc_{Π′′}(s) = proc_{Π′′′}(r).

Assume instead that proc_{Π′′}(s) ≠ proc_{Π′′′}(r). Then at least one of the following must occur in the evaluation Π′′′ ⟶^{+}_{con} Π′′:

1. an occurrence of k was a subterm of an rfork()’d function

2. an occurrence of k was a subterm of a function transmitted between threads on different processors

3. an occurrence of k itself was transmitted between threads on different processors

Each of (1), (2), and (3) represents a ⟶_{con} -transition with an occurrence of k in a thread on the left-hand side. Consider the family of annotation maps for the thread map on the left-hand side of the transition, given by updating the family of annotation maps at each preceding step, starting with G. We claim that in each of these situations, the σ annotation for the occurrence of k must be reach^{±}. By iterating Theorem 2, we can produce a locally consistent family of annotation maps for Π′′. In Π′′, since k is a channel-part subterm of a send() or receive(), it has a σ annotation of reach^{±}. The occurrence of k in (1), (2), or (3) is an occurrence predecessor of the k in Π′′. By iterating Lemma 6(4), and using the ≤^{→}-order on propositions, the occurrence of k in (1), (2), or (3) also has a σ annotation of reach^{±}, as claimed.

Suppose (1) happens.

By Theorem 2, we can obtain a locally-consistent annotation map for the thread containing the rfork(). By local consistency, the label of the rfork()’d function must have been an element of ϕ for the function-part of the rfork(). As we have stated, the σ annotation for the occurrence of k in that function was reach^{±}. By local consistency, that occurrence of k also had a ω-annotation of local^{±}. By Lemma 6(4) and the transitivity of the ≤^{→} relation on propositions, any occurrence predecessor of this k also had a ω-annotation of local^{±}. In particular, the occurrence of k in the thread map where it was created had a ω-annotation of local^{±}. By the specification of annotation map updates, the occurrence r : m of channel() also had a ω-annotation of local^{±}. By Lemma 6(4) and the transitivity of the ≤^{→} relation on propositions, any occurrence predecessor of r : m, including p : i, also must have had a ω-annotation of local^{±}. This contradicts our supposition that p : i had a ω annotation of local^{+}. So (1) cannot happen.

Suppose (2) happens.

Consider the transmitted function that is the body of the send(). By the κ-coherence and communicative consistency of the family of annotation maps in which the send()’ing thread occurs, the θ annotation for the transmitted function is escape^{±}. So by the local consistency of the annotation map for that thread, the ω annotation for the occurence of k in the function body must be local^{±}. From here, we can reason as in the previous case to derive a contradiction. Therefore,

(2) cannot happen.

Suppose (3) happens.

Consider the occurrence of the receive() that participates in the communication. By the κ-coherence and communicative consistency of the family of annotation maps in which the send()’ing thread occurs, if the σ annotation for the receive() is reach^{±}, then its ω annotation is local^{±}. By the specification of annotation map updates, the proposition for a transmitted value on the right-hand side of a comm transition is the same as that for the participating receive() occurrence. We have shown that the σ annotation for the channel constant on the right-hand side of the transition is reach^{±}. Therefore, the σ annotation for the receive() on the left-hand side of the transition is reach^{±}. By the κ-coherence and communicative consistency of the family of annotation maps in which the receive() thread occurs, the receive()’s ω annotation is local^{±}. Therefore, the ω annotation for the channel constant k on the right-hand side of the transition is also local^{±}. Again we can derive a contradiction, so (3) cannot happen.

14 Related work

Many authors have described constraint-based static analyses. Besides our own work already cited, see, for example, Heintze’s Ph.D. work on set-based analysis [2] and Palsberg and Schwartzbach’s safety analysis [11].

Most work on static analysis for concurrent programs is relatively new. Peng and Purushothaman presented a dataflow analysis to detect deadlock for communicating automata [12]. Reif and Smolka describe analyses for a language of communicating processes with both fixed and dynamic communication topologies [13]. Their methods are extensions of conventional dataflow analysis techniques for sequential languages. Mercouroff used abstract interpretation to determine which processes may communicate in a CSP-like language [7]. More recently, Jagannathan and Weeks have used abstract interpretation to analyze a higher-order language with communication using shared locations [3]. Nielson and Nielson have done a variety of recent work using enhanced type systems [10][9]. Colby uses abstract interpretation to determine the communications topology of concurrent programs [1]. Our κ annotations give us similar information, although Colby’s is a finer, polyvariant analysis.

The linearity component of our propositions is similar in spirit to the usage analysis of Turner, et al., which tracks the number of uses of a term using an extended Hindley-Milner type system [18], although our purposes are quite different.

To aid in source-level debugging of programs, Tip associates terms with earlier terms in a rewrite system [17]. This technique appears similar to our use of occurrence predecessors.

15 Conclusion

We have given a constraint-based static analysis for programs in a concurrent language that is provably sound. As far as we know, this is the first constraint-based static analysis for a concurrent language. Our proof method relies on showing that given a solution to the constraints for the original program, we may produce solutions at every transition step. As usual in such analyses, there are constraints between the annotations of occurrences in individual terms. Because data flows between threads, there are also constraints between the annotations of occurrences in different threads.

We think this style of proof can support many different analyses for languages with small-step operational behavior, whether sequential or concurrent. An open challenge is whether such an analysis can justify more complex program transformations.

Our analysis detects occurrences of the channel() primitive that produce dynamic channels certain to be used only on the same processor where they are created. Another useful analysis would be to detect local references – those references which are read or mutated only on the processor where they are created. Such an analysis would be very similar to the one here.

16 Acknowledgments

David N. Turner pointed us to the right notion of locality and convinced us to formulate the analysis using a value-passing operational semantics.

References

[1] Christopher Colby. Analyzing the communication topology of concurrent programs. In ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manupulation, pages 202–14, June 1995.

[2] Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie-Mellon University, October 1992.

[3] Suresh Jagannathan and Stephen Weeks. Analyzing stores and references in a parallel symbolic language. In Proc. ACM Conf. on Lisp and Functional Programming, pages 294–306, 1994.

[4] Karoline Malmkjaer, Nevin Heintze, and Olivier Danvy. ML partial evaluation using set-based analysis. In 1994 ACM SIGPLAN Workshop on ML and its Applications, pages 112–19, Orlando, Florida, June 1994.

[5] David C.J. Matthews. A distributed concurrent implementation of standard ML. LFCS Report Series ECS-LFCS-91-174, University of Edinburgh, August 1991.

[6] David C.J. Matthews and Thierry Le Sergent. LEMMA: A distributed shared memory with global and local garbage collection. In Henry Baker, editor, Proc. Intl. Workshop in Memory Management, Lecture Notes in Computer Science, pages 297–311. Springer-Verlag, September 1995.

[7] N. Mercouroff. An algorithm for analyzing communicating processes. In Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 312–25, Berlin, Heidelberg, and New York, 1991. Springer-Verlag.

[8] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, MA, 1989.

[9] Flemming Nielson and Hanne Riis Nielson. Constraints for polymorphic behaviours of concurrent ML. In Proc. Constraints in Computational Logic ’94, number 845 in Lecture Notes in Computer Science, pages 73–88, Berlin, Heidelberg, and New York, September 1994. Springer-Verlag.

[10] Hanne Riis Nielson and Flemming Nielson. Higher-order concurrent programs with finite communication topology. In Conference Record of 21st ACM Symposium on Principles of Programming Languages, pages 84–97, January 1994.

[11] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128–41, April 1995.

[12] Wuxu Peng and S. Purushothaman. Towards dataflow analysis of communicating finite state machines. In Proc. 8th Annual ACM Symposium on Principles of Distributed Computing, pages 45–58, August 1989.

[13] John H. Reif and Scott A. Smolka. Data flow analysis of distributed communicating processes. Intl. J. of Parallel Programming, 19(1):1–30, 1990.

[14] J.H. Reppy. Higher-Order Concurrency. PhD thesis, Cornell University, 1992. Report 92-1285.

[15] Paul Steckler and Mitchell Wand. Selective thunkification. In Baudouin Le Charlier, editor, Proceedings of the 1st International Static Analysis Symposium, volume 864 of Lecture Notes in Computer Science, pages 162–78, Berlin, Heidelberg, and New York, 1994. Springer-Verlag.

[16] Paul Steckler and Mitchell Wand. Tracking available values for lightweight closures (summary). In Neil Jones and Carolyn Talcott, editors, Proc. Atlantique Workshop on Semantics Based Program Manipulation, pages 63–70, 1994. Available as DIKU Report No. 94/12, University of Copenhagen.

[17] Frank Tip. Generic techniques for source-level debugging and dynamic program slicing. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors, Proc. TAPSOFT ’95, number 915 in Lecture Notes in Computer Science, pages 516–30, Berlin, Heidelberg, and New York, May 1995. Springer-Verlag.

[18] David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In Proc. 7th Intl. Conf. on Functional Programming and Computer Architecture, pages 1–11, June 1995.

[19] Mitchell Wand and Paul Steckler. Selective and lightweight closure conversion. In Conference Record of 21st ACM Symposium on Principles of Programming Languages, pages 435–45, 1994.