Compiler Correctness for Concurrent Languages (Extended Abstract)

David S. Gladstein^{∗}^{†}^{†} and Mitchell Wand^{∗}^{‡}

Northeastern University College of Computer Science

March 6, 1995

Abstract This paper extends previous work in compiler derivation and verification to languages with true-concurency semantics. We extend the λ-calculus to model process-centered concurrent computation, and give the semantics of a small language in terms of this calculus. We then define a target abstract machine whose states have denotations in the same calculus. We prove the correctness of a compiler for our language: the denotation of the compiled code is shown to be strongly bisimilar to the denotation of the source program, and the abstract machine running the compiled code is shown to be branching-bisimilar to the source program’s denotation.

1 Introduction

1.1 Compiler derivation methodology

A recipe [8, 28, 19] for compiling a source language into a target machine language is as follows: The semantics of the source language is given as a compositional translation E[[·]] from the source language to some metalanguage. The compiler is defined by a compositional translation C[[·]] from the source language to a target language. This target language has a denotational semantics \overline{·} in the same metalanguage as the source semantics. It also has a plausibly implementable operational semantics, typically given as an abstract machine for which the target code is the machine language. The correctness of the compiler is expressed as the equality of the denotational semantics of any source program p and the denotational semantics of its translation:

E[[p]] = \overline{C[[p]]}  (1)

The correctness of the abstract machine is expressed as an adequacy theorem relating the operational and denotational semantics of the target language:

\overline{Q} = N iff Q →^{∗} F and \overline{F} = N  (2)

∗Work supported by the National Science Foundation under grant numbers CCR-901463 and CCR-9304144

†To whom correspondence should be addressed. Author’s address: Invertebrates Department, American Museum of Natural History, Central Park West at 79^{th} Street, New York, NY 10024, USA. Internet: daveg@amnh.org.

Telephone: 212–769–5639. Fax: 212–769–5495.

‡Author’s address: College of Computer Science, Northeastern University, 360 Huntington Avenue 161 CN, Boston, MA 02115, USA. Internet: wand@ccs.neu.edu.

for some final configuration F of the abstract machine. Combined, these theorems relate the denotational meaning of the source program to the answer obtained by executing the compiled code on the abstract machine:

E[[p]] = N iff \overline{C[[p]]} = N iff C[[p]] →^{∗} F and \overline{F} = N  (3)

For the case of sequential languages, the metalanguage is usually some version of the λ-calculus, and the notion of equivalence is equality modulo α-renaming and β-reduction, which we write =^{β}.

In [27] this methodology is adapted to languages with parallelism. The metalanguage is chosen to be the λ-calculus extended with special operators that turn it into a process calculus. It is shown that β-equivalence =^{β} extends to a strong bisimulation ≃^{β}. This reduces the problem of ensuring bisimilarity to that of ensuring equality in the λ-calculus.

1.2 The present work

We want to derive and verify a compiler for a realistic concurrent language, so that running programs will be similar to those written, for example, using PVM [10] or Erlang [4]. Specifically, we shall include asynchronous buffered communication, and we shall allow for execution on multiple computers.

In [27], the calculus has an interleaving semantics, as does the abstract machine. Since we are interested in multicomputer implementations, the present work uses a true-concurrency model of computation. We show how to model concurrency in such a way as to retain the technical developments of [27], while also getting an abstract machine model which is plausibly implementable on a multicomputer.

The rest of the paper is organized as follows: Section 2 describes our conceptual model for true concurrency and gives the details of our metalanguage. Section 3 describes a small source language and gives its denotational semantics in the metalanguage. Section 4 specifies a target machine language and its denotational semantics, presents the compiler, and shows that the compiler preserves denotational semantics up to strong bisimulation (Theorem 2); this corresponds to condition (1). Section 5 presents an abstract machine that executes the target language, and proves its adequacy with respect to the denotational semantics (Theorem 3); this corresponds to condition (2). These theorems are combined in Theorem 4, which corresponds to condition (3). Section 6 briefly discusses a multicomputer Concert/C implementation of the abstract machine. Section 7 briefly considers related work. Section 8 outlines some possibilities for further research.

2 True concurrency and our metalanguage

2.1 The conceptual model

Suppose we have a system with two states, and that the system evolves from one state to the other via some time consuming action. We might reasonably model this as a transition system with two states X and Y and a transition X →^{a} Y.

Suppose now that we have two independent copies of that system, with transitions X_{1} →^{a_{1}} Y_{1} and X_{2} →^{a_{2}} Y_{2}. To model their independent, concurrent operation, we might form their product as follows:

X_{1}  ⟶^{a_{1}}  Y_{1}
X_{2} (X_{1}, X_{2}) ⟶^{a_{1}} (Y_{1}, X_{2})
↓^{a_{2}} ↓^{a_{2}}  ↓^{a_{2}}
Y_{2} (X_{1}, Y_{2}) ⟶^{a_{1}} (Y_{1}, Y_{2})

This is surely not what we want, since there is no concurrency. Even if we add a diagonal transition (X_{1}, X_{2}) ⟶^{a_{1}a_{2}} (Y_{1}, Y_{2}), there is a problem: the startings and endings of the activities represented by the transitions a_{i} are synchronized.

Rather than move to another mathematical representation of computation, we can recode our understanding by splitting the transitions, following [15]. Whenever we have a durational action a represented by a transition X →^{a} Y, we replace it with a new state ⟨a, X⟩ and two new new transitions X →^{a^{+}} ⟨a, X⟩ and ⟨a, X⟩ →^{a^{−}} Y. Here the a^{+} and a^{−} transitions are instantaneous, and the state ⟨a, X⟩ is a durational state, representing the time during which the system is doing the action a. If we apply this transformation to the previous example and take the interleaving product, we ge the following:

X_{1}  ⟶^{a_{1}^{+}}  ⟨a_{1}, X_{1}⟩  ⟶^{a_{1}^{−}}  Y_{1}
X_{2}  (X_{1}, X_{2}) ⟶^{a_{1}^{+}} (⟨a_{1}, X_{1}⟩, X_{2}) ⟶^{a_{1}^{−}} (Y_{1}, X_{2})
↓^{a_{2}^{+}} ↓^{a_{2}^{+}} ↓^{a_{2}^{+}} ↓^{a_{2}^{+}}
⟨a_{2}, X_{2}⟩ (X_{1}, ⟨a_{2}, X_{2}⟩) ⟶^{a_{1}^{+}} (⟨a_{1}, X_{1}⟩, ⟨a_{2}, X_{2}⟩) ⟶^{a_{1}^{−}} (Y_{1}, ⟨a_{2}, X_{2}⟩)
↓^{a_{2}^{−}}  ↓^{a_{2}^{−}}  ↓^{a_{2}^{−}}  ↓^{a_{2}^{−}}
Y_{2}  (X_{1}, Y_{2})  ⟶^{a_{1}^{+}}  (⟨a_{1}, X_{1}⟩, Y_{2})  ⟶^{a_{1}^{−}}  (Y_{1}, Y_{2})

Here the two processes may start and stop their activities independently, and furthermore we have explicitly represented the possiblity that the two processes will be active at the same time.

2.2 The calculus

Figure 1 shows the syntax of our calculus, which is based on an infinite set PID of process identifiers. The usual terms of the λ-calculus are extended with constants for each PID, as well as four communication operators. We also define four activity markers, to annotate processes engaged in durational activity. A process consists of a term (or a term together with an activity marker) and an input buffer. A program is a finite labelled collection of processes. The label of a program transition tells which process made a transition, as well as describing the transition.

Figure 2 gives the transition relation of our calculus; corresponding ^{+} and ^{−} transitions are grouped. The ^{+} transitions are “instantaneous computation” rules [7], in that the terms appearing in the transition may be related by an arbitrary number of β reductions. Within such a reduction sequence, the communication operators are uninterpreted; this trick of separating computational reductions from communication is due to [18]. We now describe each communication operation in turn.

The c_{receive} operation fetches the head of the input queue, should it be nonempty. A process may try to read its input buffer at any time, but of course the operation cannot terminate until there is input. This is modelled by the ⟨receive⟩^{+} transition always being enabled, and the ⟨receive⟩^{−} transition requiring a nonempty input queue.

The c_{examine} operation examines the input queue, returning true for empty and false otherwise. (The quasiquotation marks · indicate a λ-calculus encoding of the datum, the details of which we leave unspecified.) The ⟨examine⟩^{+} transition takes a snapshot of the state of the buffer, storing

Syntactic domains

Term ::= c_{p}  A constant for each p ∈ PID
| c_{send} | c_{receive} | c_{examine} | c_{spawn}  Communication operators
| v  Variable
| λv.Term  Abstraction
| (Term Term)  Application
Value = {M ∈ Term | M has no free variables} Closed terms
Activity ::= c_{sending} | c_{receiving}  Activity markers
| ⟨c_{examining} Value⟩ | ⟨c_{spawning} c_{p}⟩
Active term = Activity × Term
Buffer = Value^{∗}
Process = (Term ∪ Active term) × Buffer
Program = PID →^{fin} Process
Event ::= ⟨send p⟩^{±} | ⟨receive⟩^{±}
| ⟨examine⟩^{±} | ⟨spawn p⟩^{±}
± ::= + | −
Action = PID × Event  Transition labels
Transition = Program × Action × Program

Typical variables

p ∈ PID  Process ids
M, N, P ∈ Term ∪ Active term
V ∈ Value
B ∈ Buffer
X ∈ Process
Π ∈ Program

Figure 1: Syntactic domains and typical variables for the calculus

it in the activity marker. This snapshot is returned by the ⟨examine⟩^{−} transition, rather than the actual state of the buffer. Thus this test is conservative: a result of true may or may not indicate an empty buffer, but a result of false always indicates a nonempty buffer.

The c_{send} operation sends a value to a process, or more accurately, puts it into the buffer of a process. Like the ⟨receive⟩^{+} transition, the ⟨send⟩^{+} transition is always enabled. The ⟨send⟩^{−} transition is only enabled when the receiving process actually exists.

The c_{spawn} operation forks another process. The ⟨spawn⟩^{+} transition is nondeterministic, because the process does not determine the PID of the new process in advance. The process makes a nondeterministic transition into the activity, recording the new, unused PID in the activity marker. Note that a process id is considered to be in use once it is assigned to a fork activity. The ⟨spawn⟩^{−} activity actually establishes the new process.

A notion of equivalence for process-oriented calculi, called β-bisimilarity and written ≃^{β}, was introduced in [27]. There the processes were λ-terms; two programs Π and Π′ were related by ≃^{β} if dom Π = dom Π′, and for each process p in the common domain, Π(p) =^{β} Π′(p). This equivalence was proved to be a strong bisimulation.

The processes of our calculus are more complicated, being constructed of tuples and sequences

\frac{M =^{β} (c_{receive} N)}{Π[p : ⟨M, B⟩] ⟶^{p:⟨receive⟩^{+}} Π[p : ⟨⟨c_{receiving}, (c_{receive} N)⟩, B⟩]}

\frac{X = ⟨⟨c_{receiving}, (c_{receive} N)⟩, (V::B′)⟩}{Π[p : X] ⟶^{p:⟨receive⟩^{−}} Π[p : ⟨(N V), B′⟩]}

\frac{M =^{β} (c_{examine} N) V = \{ \begin{matrix}true & B = [ ] \\ false & B ≠ [ ] \end{matrix}}{Π[p : ⟨M, B⟩] ⟶^{p:⟨examine⟩^{+}} Π[p : ⟨⟨⟨c_{examining} V ⟩, (c_{examine} N)⟩, B⟩]}

\frac{M = ⟨⟨c_{examining} V ⟩, (c_{examine} N)⟩}{Π[p : ⟨M, B⟩] ⟶^{p:⟨examine⟩^{−}} Π[p : ⟨(N V), B⟩]}

\frac{M =^{β} (c_{send} c_{p′} V N) V a closed value}{Π[p : ⟨M, B⟩] ⟶^{p:⟨send p′⟩^{+}} Π[p : ⟨⟨c_{sending}, (c_{send} c_{p′} V N)⟩, B⟩]}

\frac{M = ⟨c_{sending}, (c_{send} c_{p′} V N)⟩}{Π[p : ⟨M, B⟩][p′ : ⟨M′, B′⟩] ⟶^{p:⟨send p′⟩^{−}} Π[p : ⟨N, B⟩][p′ : ⟨M′, (B′@[V])⟩]}

\frac{M =^{β} (c_{spawn} N P) p′ ∉ procs Π}{Π[p : ⟨M, B⟩] ⟶^{p:⟨spawn p′⟩^{+}} Π[p : ⟨⟨⟨c_{spawning} c_{p′}⟩, (c_{spawn} N P)⟩, B⟩]}

\frac{M = ⟨⟨c_{spawning} c_{p′}⟩, (c_{spawn} N P)⟩}{Π[p : ⟨M, B⟩] ⟶^{p:⟨spawn p′⟩^{−}} Π[p : ⟨(P c_{p′}), B⟩][p′ : ⟨(N c_{p′}), [ ]⟩]}

where

procs Π = dom Π ∪ {p | ∃q: Π(q) = ⟨⟨⟨c_{spawning} c_{p}⟩, M⟩, B⟩}

Figure 2: Communication rules

of λ-terms. We therefore extend =^{β} to cover tuples and sequences: ⟨M, N⟩ =^{β} ⟨M′, N′⟩ exactly when

M =^{β} M′ and N =^{β} N′, and [M_{1} … M_{n}] =^{β} [M′_{1} … M′_{n′}] exactly when n = n′ and each M_{i} =^{β} M′_{i}.

With this convention, we may write the definition of equivalence for our calculus:

Definition 1 (β-bisimilarity) Write Π ≃^{β} Π′ if dom Π = dom Π′, and at each p, Π(p) =^{β} Π′(p).

We can then prove the following for ≃^{β}:

Theorem 1 ≃^{β} is a strong bisimulation. Proof: Let Π ≃^{β} Π′ be given, and consider each rule for the transitions other than ⟨spawn⟩^{+}. The programs’ corresponding processes are =^{β}, so by the transitivity of =^{β}, any rule which applies to Π applies to Π′.

For ⟨spawn⟩^{+}, the antecedent of the rule has the extra side condition p′ ∉ procs Π. Clearly procs Π = procs Π′, so any ⟨spawn⟩^{+} transition open to one program is open to the other.

3 Source language syntax and semantics

The syntax of our source language is shown in Figure 3, in which i ranges over identifiers and n over integers. We have the usual pieces of a functional language, namely identifiers, constants, primitives, abstractions, and applications, as well as four new operators (put, get, empty?, and spawn) corresponding to the communication primitives.

p ::= a  Program
a ::= (rec i(i) e)  Abstraction
e ::= n | i | a | (if e e e) | (e e) | (− e e)  Expressions
| (put e e) | (get) | (empty?) | (spawn e)

Figure 3: Source language syntax

The semantics of the language is given in Figure 4. Expressions are translated compositionally into terms of our calculus, while programs are translated into entire programs. The environment is a map from identifiers to values; it represents the bindings of variables at the time the expression is evaluated. The continuation is a function mapping the value of the expression to the result of the program; it represents the remainder of the computation, which is waiting for the value of the expression. The translation is essentially a standard continuation-passing semantics; see [8, 20, 21] for detailed expositions. In what follows, when we have a term (M_{1} … M_{n}), we will say that M_{1} is in head position, or function position, and that M_{n} is in continuation position.

E[[i]] = λρκ.κ(ρ i)
E[[n]] = λρκ.κ(in_{int} n)
E[[(rec i_{1}(i_{2}) e)]] = λρκ.κ(in_{clo}(fix (λp.λvκ.E[[e]](ρ[(in_{clo} p)/i_{1}][v/i_{2}])κ)))
E[[(if e_{1} e_{2} e_{3})]] = λρκ.E[[e_{1}]]ρ(λb.(branch b E[[e_{2}]] E[[e_{3}]]) ρ κ)
E[[(e_{1} e_{2})]] = λρκ.E[[e_{1}]]ρ(λf.E[[e_{2}]]ρ(λa.applicate f a κ))
E[[(− e_{1} e_{2})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.E[[e_{2}]]ρ(λv_{2}.subtract v_{1} v_{2} κ))
E[[(put e_{1} e_{2})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.E[[e_{2}]]ρ(λv_{2}.send v_{1} v_{2} κ))
E[[(get)]] = λρκ.c_{receive}κ
E[[(empty?)]] = λρκ.c_{examine}κ
E[[(spawn e)]] = λρκ.E[[e]]ρ(λf.c_{spawn}(λp′.boot f p′) (λp′.κ (in_{pid} p′)))
P[[a]] = [p_{0} : E[[a]]ρ_{0}(λf.boot f c_{p_{0}})]

Figure 4: Source language semantics

The clause for (− e_{1} e_{2}) is typical. Each subexpression is evaluated, the value being bound to the argument variable of an explicit continuation. The values, together with the expression’s continuation, are passed to the auxiliary term subtract. The auxiliary unboxes the values as necessary for the operation it implements, appeals to another term to do the actual arithmetic, and finally calls the continuation on the appropriately boxed result.

The put clause similarly evaluates its arguments and hands them to the term send, which proceeds as follows. The first argument should be a process id; it is unboxed, yielding a process term with c_{send} in function position. When the send operation has been completed, computation can continue as specified by the put expression’s continuation. put expressions return unit.

The get clause is simply the process term with c_{receive} in function position and the expression’s continuation in continuation position. Thus upon completion of the receive operation, the expression will return the received value.

The empty? clause similarly returns the boolean value generated by the c_{examine} primitive. The c_{spawn} primitive operates on two arguments: a function to be spawned as a new process,

and a continuation. Both arguments are functions, and both are to be called on the process id of the newly created process. The spawn clause evaluates its argument, which should yield a closure value representing the function to be spawned. The closure value itself is not of the right form for use by the c_{spawn} primitive, but the spawn clause wraps it in an abstraction which is; that abstraction handles the administrative task of boxing the new process id, and also providing the deadlocking continuation †. Likewise, the spawn expression’s continuation is wrapped in an abstraction which boxes up the new process id before feeding it to the continuation.

The clause for an entire program expects that the program is in the form of a function to be spawned. It specifies that the function should be applied to an initial process id and installed as the one and only process, labelled with that process id.

We now turn to the auxiliaries, which are shown in Figure 5. In the interest of brevity, we stop short of showing how to encode all of the auxiliary terms into λ-calculus; rather we state the properties the encodings are expected to have. The term 0 implements deadlock; it cannot communicate. The term † is then a deadlocking continuation.

The language uses four value domains (integers, PIDs, closures, and booleans), and a one-point domain unit for representing unspecified values. We omit definitions of the injection and projection terms; encodings as higher-order abstract syntax terms are given in [13]. Taken together, the injection (boxing) terms in_{i} and the projection (unboxing) terms out_{j} should have the property

out_{j} (in_{i}x)κ =^{β} \{ \begin{matrix}κx & if i = j \\ 0 & otherwise \end{matrix}

Thus runtime type errors lead to immediate deadlock, while in the absence of type errors unboxing a value simply passes it to the current continuation. We also require that any attempt to unbox unit also leads to deadlock.

The term subtract makes use of a term primitive sub, which we assume to have the property (primitive sub m n) =^{β} m − n. The term branch makes use of a term primitive if which should have the property that (primitive if true M N) =^{β} M and (primitive if false M N) =^{β} N.

For later developments, we require an encoding of stacks: an infix constructor ::, an empty stack ⟨⟩, and a deconstructor pop. We also omit these encodings (which can be found in [13]), but they should have the property

pop v κ =^{β} \{ \begin{matrix}κ a x & if v =^{β} (a::x) \\ 0 & if v =^{β} ⟨⟩ \end{matrix}

0 = λv.v
† = λv.0
applicate = λvaκ.out_{clo} v (λf.f a κ)
branch = λb e_{t}e_{f}.out_{bool} b (λv.(primitive if v e_{t} e_{f}))
subtract = λv_{1}v_{2}κ.out_{int} v_{1}(λn_{1}.out_{int} v_{2} (λn_{2}.κ(in_{int} (primitive sub n_{1} n_{2}))))
send = λv_{1}v_{2}κ.out_{pid} v_{1} (λp.c_{send} p v_{2} (κ unit))
boot = λfp.applicate f (in_{pid} p) †

Figure 5: Auxiliaries

4 Target language syntax and semantics

To the extent that we could execute our calculus via an interpreter, the semantic map E gives an interpreter for our source language. To move towards a compiler, we separate the information which is known at compilation time from that which is not known until run time. In particular, we split the environment into a compile-time symbol table and a run-time display, and we split continuations into static instruction sequences and dynamic sequences of activation records. Furthermore, we introduce a run-time stack for storing intermediate results, instead of using continuations as, for instance, in the rule for E[[(− e_{1} e_{2})]] where two explicit continuations were needed to bind the values of the subexpressions. This leads us to an abstract target machine whose state is a 4-tuple: a current instruction, a display of local variable bindings, a local stack of intermediate results, and a stack of suspended activation records.

The syntax of the target machine language and associated structures is given in Figure 6. A system state is a finite map from process ids to process states. A process state is either a start state, a stopped state, or a computational state. A computational state consists of a control tuple and an input buffer. The control tuple may stand alone, or may be adjoined to an activity marker; its components were described in the previous paragraph.

The denotations of target machine language programs and states are given in Figures 6 and 7, as a syntax-directed translation into the metalanguage. The translation follows the pattern established in [8].

The compiler of Figure 8 translates source terms to target terms. To be correct, the denotation of the compiled code for an expression must match the denotation of the expression itself, after the difference between the compiled and “interpreted” codes’ execution contexts are taken into account: the denotation of the compiled code CE[[e]] for any expression e, symbol table Γ and instruction sequence π, when applied to a display u, local stack ζ, and continuation κ, must be equivalent to the semantic definition E[[e]] when applied to the environment u ∘ Γ and a continuation that takes the value returned by e, pushes it on the local stack, and then executes the code sequence π on the resulting register values. This is expressed in the following induction hypothesis:

(\overline{CE[[e]]Γπ}) =^{β} λuζκ.E[[e]](u ∘ Γ)(λz.\overline{π}u(z::ζ)κ)  (4)

This condition is easily verified by structural induction on e, after which the strong bisimilarity of the compiled code’s denotation and the semantic definition follows directly:

Theorem 2 (Compiler Correctness) For any program p, [p_{0} : start \overline{CP[[p]]}] ≃^{β} P[[p]].

Syntax  Denotation
Q = [p : s] …  [p : \overline{s}] …  System states
s ::= ⟨start, π⟩  start \overline{π}  Process states
| ⟨t, b⟩  ⟨\overline{t}, \overline{b}⟩

| ⟨stopped⟩  0

t ::= c  \overline{c}  Idle computation
| ⟨⟨computing⟩, c⟩  \overline{c}  Active computation
| ⟨m, c⟩  ⟨\overline{m}, \overline{c}⟩  Active communication
c ::= ⟨π, u, z, k⟩  \overline{π} \overline{u} \overline{z} \overline{k}  Computation state
π ::= ⟨fetch, n, π⟩  fetch n \overline{π}  Code sequences
| ⟨pushint, n, π⟩  pushint n \overline{π}
| ⟨pushclosure, π, π⟩ pushclosure \overline{π′} \overline{π}
| ⟨return⟩  return
| ⟨call, π⟩  call \overline{π}
| ⟨brtrue, π, π⟩  brtrue \overline{π}_{t} \overline{π}_{f}
| ⟨sub, π⟩  sub \overline{π}
| ⟨put, π⟩  put \overline{π}
| ⟨get, π⟩  get \overline{π}
| ⟨empty, π⟩  empty \overline{π}
| ⟨spawn, π⟩  spawn \overline{π}
| ⟨swap, π⟩  swap \overline{π}
u ::= z  \overline{z}  Displays
z ::= ⟨⟩  ⟨⟩  Stacks
| ⟨v, z⟩  (\overline{v}::\overline{z})
k ::= ⟨halt⟩ † Continuations
| ⟨frame, π, u, z, k⟩  λv.\overline{π} \overline{u}(v::\overline{z})\overline{k}
b ::= z  \overline{z}  Buffers
v ::= ⟨int, n⟩  in_{int} n  Values
| ⟨pid, p⟩  in_{pid} c_{p}
| ⟨closure, π, u⟩  in_{clo}(λvκ.\overline{π}(v::\overline{u})⟨⟩κ)
| ⟨bool, 0⟩  in_{bool} false
| ⟨bool, 1⟩  in_{bool} true
| ⟨unit⟩  unit
m ::= ⟨receiving⟩ ⟨c_{receiving}⟩ Activity markers
| ⟨emptying, v⟩  ⟨c_{examining} \overline{v}⟩
| ⟨sending⟩  ⟨c_{sending}⟩
| ⟨spawning, v⟩  ⟨c_{spawning} \overline{v}⟩

| ⟨computing⟩

Figure 6: System state syntax and denotations. Note that the rule for ⟨⟨computing⟩, c⟩ takes precedence over the rule for ⟨m, c⟩ which follows it.

5 The target machine and its correctness

We now present a small-step operational semantics for our abstract machine. We may separate the purely sequential rules from the communicating rules. The sequential rules, which only affect the

fetch n π = λuζκ.πu((dlookup u n)::ζ)κ
pushint v π = λuζκ.πu((in_{int} v)::ζ)κ
pushclosure π′π = λuζκ.πu(in_{clo}(fix (λp.λvκ.π′((in_{clo} p)::v::u)⟨⟩κ)::ζ)κ)
return = λuζκ.pop ζ(λvζ.κv)
call π = λuζκ.pop ζ(λaζ.pop ζ(λfζ.applicate f a (λv.πu(v::ζ)κ)))
brtrue π_{t} π_{f} = λuζκ.pop ζ(λvζ.(out_{bool} v (λb.(primitive if b (π_{t}uζκ) (π_{f}uζκ)))))
sub π = λuζκ.pop ζ(λv_{1}ζ.pop ζ(λv_{2}ζ.subtract v_{1} v_{2}(λv.πu(v::ζ)κ)))
put π = λuζκ.pop ζ(λv_{1}ζ.out_{pid} v_{1}(λp.c_{send} p v_{2}(πu(unit::ζ)κ)))
get π = λuζκ.c_{receive}(λv.πu(v::ζ)κ)
empty π = λuζκ.c_{empty}(λv.πu(v::ζ)κ)
spawn π = λuζκ.pop ζ(λfζ.c_{spawn}(λp′.boot f †)(λp′.πu((in_{pid} p′)::ζ)κ))
start = λπ.π⟨⟩((in_{pid} c_{p_{0}})::⟨⟩)†
swap π = λuζκ.pop ζ(λv_{1}ζ_{1}.pop ζ_{1}(λv_{2}ζ_{2}.πu(v_{2}::(v_{1}::ζ_{2}))κ))

Figure 7: Denotational semantics of instructions

CE[[i]]Γπ = ⟨fetch, (slookup Γi), π⟩
CE[[n]]Γπ = ⟨pushint, n, π⟩
CE[[(rec i_{1}(i_{2}) e)]]Γπ = ⟨pushclosure, (CE[[e]](i_{1}::i_{2}::Γ)⟨return⟩), π⟩
CE[[(if e_{1} e_{2} e_{3})]]Γπ = CE[[e_{1}]]Γ⟨brtrue, (CE[[e_{2}]]Γπ), (CE[[e_{3}]]Γπ)⟩
CE[[(e_{1} e_{2})]]Γπ = CE[[e_{1}]]Γ(CE[[e_{2}]]Γ⟨call, π⟩)
CE[[(− e_{1} e_{2})]]Γπ = CE[[e_{1}]]Γ(CE[[e_{2}]]Γ⟨sub, π⟩)
CE[[(put e_{1} e_{2})]]Γπ = CE[[e_{1}]]Γ(CE[[e_{2}]]Γ⟨put, π⟩)
CE[[(get)]]Γπ = ⟨get, π⟩
CE[[(empty?)]]Γπ = ⟨empty, π⟩
CE[[(spawn e)]]Γπ = CE[[e]]Γ⟨spawn, π⟩
CP[[e]] = (CE[[e]]⟨⟩⟨swap, ⟨call, ⟨return⟩⟩⟩)

Figure 8: The compiler

“computational” part of a process state and not the buffer, may be conveniently expressed as rules for a 4-register machine, and then lifted to a rule expressing the transition of the entire process state. The computation rules and the lifting rule are given in Figure 9. In addition, we assume that if the instruction is one of the ones in the figure, but the pattern for the rule does not match, we execute the default rule ⟨⟨π, u, z, k⟩, b⟩ →_{1} ⟨stopped⟩.

Figure 10 gives the small-step semantics for our abstract machine. Every durational action of each process of the machine is modelled by a pair of transitions, representing the start and end of the action. The pair of rules for τ transitions lifts the computation rules into the instantaneous transition model of computation, making explicit the possibility of the entire machine getting into

⟨start, π⟩  →_{0} ⟨π, ⟨⟩, ⟨⟨pid, p_{0}⟩, ⟨⟩⟩, ⟨halt⟩⟩
⟨⟨fetch, n, π⟩, u, z, k⟩  →_{0} ⟨π, u, ⟨(clookup u n), z⟩, k⟩
⟨⟨pushint, n, π⟩, u, z, k⟩  →_{0} ⟨π, u, ⟨⟨int, n⟩, z⟩, k⟩
⟨⟨pushclosure, π′, π⟩, u, z, k⟩  →_{0} ⟨π, u, ⟨⟨closure, π′, u⟩, z⟩, k⟩
⟨⟨return⟩, u, ⟨v, z⟩, ⟨frame, π′, u′, z′, k′⟩⟩ →_{0} ⟨π′, u′, ⟨v, z′⟩, k′⟩
⟨⟨call, π⟩, u, ⟨v, ⟨⟨closure, π′, u′⟩, z⟩⟩, k⟩ →_{0} ⟨π′, ⟨⟨closure, π′, u′⟩, ⟨v, u′⟩⟩, ⟨⟩, ⟨frame, π, u, z, k⟩⟩
⟨⟨brtrue, π_{t}, π_{f}⟩, u, ⟨⟨bool, true⟩, z⟩, k⟩ →_{0} ⟨π_{t}, u, z, k⟩
⟨⟨brtrue, π_{t}, π_{f}⟩, u, ⟨⟨bool, false⟩, z⟩, k⟩ →_{0} ⟨π_{f}, u, z, k⟩
⟨⟨sub, π⟩, u, ⟨⟨int, n⟩, ⟨⟨int, m⟩, z⟩⟩, k⟩ →_{0} ⟨π, u, ⟨⟨int, (m − n)⟩, z⟩, k⟩
⟨⟨swap, π⟩, u, ⟨v, ⟨w, z⟩⟩, k⟩  →_{0} ⟨π, u, ⟨w, ⟨v, z⟩⟩, k⟩

\frac{⟨π, u, z, k⟩ →_{0} ⟨π′, u′, z′, k′⟩}{⟨⟨π, u, z, k⟩, b⟩ →_{1} ⟨⟨π′, u′, z′, k′⟩, b⟩}

Figure 9: Computation rules

states where many processes are computing (that is, in ⟨computing, X⟩ states) simultaneously. The other eight rules correspond in a straightforward way to the communication rules of Figure 2.

In the previous section, we showed that the denotation of a compiled program matched the denotation of the program itself. This idea is captured in the following definition:

Definition 2 We say that a program Π in our calculus and a system state Q correspond if Π ≃^{β} \overline{Q}. We write Π ≃ Q.

The goal now is to show that the successive states of a target machine running the compiled code for a program always correspond to the program’s denotation. This amounts to showing that ≃ is a branching bisimulation. We break the proof into several lemmas: we show first that silent transitions of the abstract machine correspond to β-reduction of terms in our calculus, and then that each observable transition of one system is justified by a corresponding transition in the other.

Lemma 1 If s →_{1} s′ then \overline{s} →_{β}^{+} \overline{s′} via a reduction sequence containing at least one leftmost step.

Lemma 2 (Sequential Simulation) If Q →^{τ} Q′ then \overline{Q} ≃^{β} \overline{Q′}.

Lemma 3 (Communicating Simulation) If a ≠ τ, Q →^{a} Q′ and Π ≃ Q, then there is a Π′ with

Π →^{a} Π′ and Π′ ≃ Q′.

Lemma 4 (Completeness) If Π →^{a} Π′ and Π ≃ Q then there is a Q_{1} and a Q′ with Q →^{τ} … →^{τ}

Q_{1} →^{a} Q′, Π ≃ Q_{1}, and Π′ ≃ Q′.

The proofs of Lemmas 1–3 are straightforward. The proof of Lemma 4 uses Lemma 1 and the completeness of quasi-leftmost reduction sequences for head normal forms; see [6, 27, 13] for details. Combining the lemmas gives the following:

Theorem 3 (Abstract Machine Correctness) ≃ is a branching bisimulation.

\frac{X →_{1} X′}{Q[p : X] →^{τ} Q[p : ⟨computing, X⟩]}

\frac{X →_{1} X′}{Q[p : ⟨computing, X⟩] →^{τ} Q[p : X′]}

\frac{X = ⟨⟨⟨get, π⟩, u, z, k⟩, b⟩}{Q[p : X] ⟶^{p:⟨receive⟩^{+}} Q[p : ⟨⟨receiving⟩, X⟩]}

\frac{X = ⟨⟨receiving⟩, ⟨⟨⟨get, π⟩, u, z, k⟩, ⟨v, b⟩⟩⟩}{Q[p : X] ⟶^{p:⟨receive⟩^{−}} Q[p : ⟨⟨π, u, ⟨v, z⟩, k⟩, b⟩]}

\frac{X = ⟨⟨⟨empty, π⟩, u, z, k⟩, b⟩ i = \{ \begin{matrix}1 & b = ⟨⟩ \\ 0 & b ≠ ⟨⟩ \end{matrix}}{Q[p : X] ⟶^{p:⟨examine⟩^{+}} Q[p : ⟨⟨emptying, ⟨int, i⟩⟩, X⟩]}

\frac{X = ⟨⟨emptying, v⟩, ⟨⟨⟨empty, π⟩, u, z, k⟩, b⟩⟩}{Q[p : X] ⟶^{p:⟨examine⟩^{−}} Q[p : ⟨⟨π, u, ⟨v, z⟩, k⟩, b⟩]}

\frac{X = ⟨⟨⟨put, π⟩, u, ⟨v, ⟨⟨pid, p′⟩, z⟩⟩, k⟩, b⟩}{Q[p : X] ⟶^{p:⟨send p′⟩^{+}} Q[p : ⟨sending, X⟩]}

\frac{X = ⟨sending, ⟨⟨⟨put, π⟩, u, ⟨v, ⟨⟨pid, p′⟩, z⟩⟩, k⟩, b⟩⟩}{Q[p : X][p′: ⟨Y, b′⟩] ⟶^{p:⟨send p′⟩^{−}} Q\begin{matrix}[p : ⟨⟨π, u, ⟨⟨unit⟩, z⟩, k⟩, b⟩] \\ [p′: ⟨Y, b′@⟨v, ⟨⟩⟩⟩] \end{matrix}}

\frac{X = ⟨⟨⟨spawn, π⟩, u, ⟨⟨closure, π′, u′⟩, z⟩, k⟩, b⟩ p′ ∉ procs Q}{Q[p : X] ⟶^{p:⟨spawn p′⟩^{+}} Q[p : ⟨⟨spawning, ⟨pid, p′⟩⟩, X⟩]}

\frac{X = ⟨⟨spawning, ⟨pid, p′⟩⟩, ⟨⟨⟨spawn, π⟩, u, ⟨⟨closure, π′, u′⟩, z⟩, k⟩, b⟩⟩}{Q[p : X] ⟶^{p:⟨spawn p′⟩^{−}} Q[p : ⟨⟨π, u, ⟨⟨pid, p′⟩, z⟩, k⟩, b⟩] [p′: ⟨⟨⟨call, return⟩, ⟨⟩, ⟨⟨pid, p′⟩, ⟨⟨closure, π′, u′⟩, ⟨⟩⟩⟩, ⟨halt⟩⟩, [ ]⟩]}

Figure 10: Small step semantics

Combining Theorems 2 and 3 we get: Theorem 4 (Combined Correctness) For any program e, P[[e]] is branching-bisimilar to [p_{0} : ⟨start, CP[[e]]⟩].

This shows that the behavior given by the semantics is similar to the behavior of the target machine running the compiled program, as desired.

6 Implementation

To demonstrate that the small-step semantics is plausible, we coded an implementation in Concert/C [5], an extension of C which provides facilities for transmitting data structures between processes. Each process of the target machine program was represented by a separate Concert/C process. The target machine states of Figure 6 were transliterated into C structs. A straightforward interpreter implements those process transitions which do not involve interprocess communication, while message sending and spawning are implemented by the corresponding Concert/C facilities.

Taking the state of a Concert/C process to consist of its program counter together with the values of its program variables, we were able to argue that the collection of Concert/C processes is a simulation of the target machine: each state and transition of the collection of processes corresponds to a legal move of the target machine. Since we could not guarantee anything about the way our processes would be scheduled by the operating system, we were not able to argue that our implementation is complete for the target machine; however, we were able to show that the implementation cannot deadlock unless the target machine can do so.

The complete implementation is given in [13].

7 Related work

A number of small-to-moderate sized compiler correctness proofs have been accomplished using the techniques sketched in the introduction: a simple functional language [25, 24], a language with while-expressions [26], a language obeying stack-discipline [28], and core Scheme [8]. More recently, this technique has been used for two large proofs: one for a very detailed proof of a complete Scheme system [14], and one for a detailed proof of a compiler for PreScheme, a Schemelike language designed for systems programming [19].

There is, of course, a vast literature on the semantics of concurrency, but very little of it has been directed toward compiler correctness. Most of this work can be thought of as investigations of the algebraic and mathematical properties of alternative intermediate metalanguages. We discuss here a few papers that are more closely related.

The formulation of our calculus is greatly indebted to the Nielsons’ formulation of process algebras for CML [18]. The trick of having the computation treat the communications primitives as uninterpreted constants is due to them. They use a small-step semantics for both computation and communication, whereas we use a version of the instantaneous computation rule, which allows us to revert to the λ-calculus when considering computation alone.

Facile [11, 12] is intended as a source language; it is specified by a compositional translation into “core Facile,” which is more like an intermediate language. Core Facile is based on a typed callby-value λ-calculus with channel-based communications and a call/cc operator. Amadio [1] gives translations between several versions of this language, including a translation into an environmentbased machine similar to ours. He shows that his translations are adequate in the sense that they do not confuse distinguishable programs. The semantics of core Facile is given as a pure small-step semantics, for both computation and communication steps. This complicates the notion of observability, and requires considerable reasoning about administrative reductions, etc. Our formulation, in which β-equivalence is automatically a bisimulation, seems easier to reason about.

Flanagan and Felleisen [9] consider a sequential functional language with a future construct that allows possible speculative computation. The language is more like an intermediate language than a source language, and the goal is to compute a single answer, rather than to realize some behavior. The semantics are specified as labelled transition systems in which the labels are not observable actions but step counts, so q ⟶^{n,m} q′ iff q can go to q′ via n steps, of which m are nonspeculative. The resulting labelled transition systems are highly non-deterministic but are shown confluent.

Milner has shown how to translate the λ-calculus into the π-calculus in a way that preserves and reflects β-convertibility [16, 17]. Walker [23] shows how two languages similar to POOL [2] can be compositionally translated into the π-calculus, but he gives no relation between this translation and any other semantics for the language. Thomsen’s original article on CHOCS also illustrates the use of CHOCS as an intermediate language [22]. Thomsen translates the λ-calculus into CHOCS and shows that the translation preserves, but does not reflect, β-convertibility. He also gives a compositional translation from a toy language with procedures into CHOCS.

However, neither the π-calculus nor CHOCS seems so well suited as the λ-calculus for generating reasonable code for the sequential portions of the language, as we have described; by using the λ-calculus as an intermediate language, we get to reuse large amounts of reasoning from sequentiallanguage compiler proofs. Other arguments for the use of λ-calculus as an intermediate language are given by Appel [3].

8 Future work

In the course of this work, several avenues of further research became apparent.

Our account of asynchronous message passing is somewhat inaccurate, in that a process is blocked from the time it sends a message until the time the message is enqueued at the receiver’s input buffer. We believe that this can be fixed by giving an account in which buffers and communication paths are reified, and all communication is synchronous.

So far the communication and process control operations of our semantics have been equivalent to those provided by the underlying implementation system, in our case Concert/C. We need to give an account of high-level operations in terms of lower-level ones; refinement methods such as those of [19, 7] should be applicable.

References

[1] R. M. Amadio. Translating core Facile. Technical Report ECRC-1994-3, ECRC, Feb. 1994.

[2] P. America, J. de Bakker, J. N. Kok, and J. Rutten. Operational semantics of a parallel object-oriented language. In Conf. Rec. 13th ACM Symposium on Principles of Programming Languages, pages 194–208, 1986.

[3] A. W. Appel. Compiling with Continuations. Cambridge University Press, Cambridge, 1992.

[4] J. Armstrong, R. Virding, and M. Williams. Concurrent Programming in Erlang. Prentice Hall, 1993.

[5] J. S. Auerbach et al. Concurrent/C Tutorial and User’s Guide: An Introduction to a Language for Distributed C Programming. IBM T. J. Watson Research Center, June 1994.

[6] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1984.

[7] B. Bloom. Chocolate: Calculi of higher order communication and lambda terms. In Conf. Rec. 21st ACM Symposium on Principles of Programming Languages, pages 339–347, 1994.

[8] W. Clinger. The Scheme 311 compiler: An exercise in denotational semantics. In Proc. 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, Aug. 1984.

[9] C. Flanagan and M. Felleisen. The semantics of future. Technical Report COMP TR94-238, Rice University, Department of Computer Science, Oct. 1994.

[10] A. Geist et al. PVM 3 User’s Guide and Reference Manual. Oak Ridge National Laboratory, May 1993.

[11] A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming, 18(2):121–160, 1989.

[12] A. Giacalone, P. Mishra, and S. Prasad. Operational and algebraic semantics for facile: A symmetric integration of concurrent and functional programming. In Proc. ICALP ’90, volume 443 of Lecture Notes in Computer Science, pages 765–7780, Berlin, Heidelberg, and New York, 1990. Springer-Verlag.

[13] D. Gladstein. Compiler Correctness for Concurrent Languages. PhD thesis, Northeastern University,

Dec. 1994. Available via anonymous ftp from ftp.ccs.neu.edu as /pub/people/daveg/thesis.ps.Z.

[14] J. D. Guttman, V. Swarup, and J. Ramsdell. The VLISP verified scheme system. Lisp and Symbolic Computation, 8(1/2), 1995. to appear.

[15] C. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985.

[16] R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2:119–141, 1992.

[17] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (parts i and ii). Information and Computation, 100:1–77, 1992.

[18] F. Nielson and H. R. Nielson. From CML to process algebras. In Proceesings of CONCUR ’93, pages 493–508, Berlin, Heidelberg, and New York, 1993. Springer-Verlag.

[19] D. P. Oliva, J. D. Ramsdell, and M. Wand. The VLISP verified PreScheme compiler. Lisp and Symbolic Computation, 8(1/2), 1995. to appear.

[20] J. C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6(3/4):233–248, 1993.

[21] G. Springer and D. P. Friedman. Scheme and the Art of Programming. MIT Press, 1989.

[22] B. Thomsen. A calculus of higher order communicating systems. In Conf. Rec. 16th ACM Symposium on Principles of Programming Languages, pages 143–154, 1989.

[23] D. Walker. π-calculus semantics of object-oriented programming languages. In Proc. Conference on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Berlin, Heidelberg, and New York, 1991. Springer-Verlag.

[24] M. Wand. Deriving target code as a representation of continuation semantics. ACM Transactions on Programming Languages and Systems, 4(3):496–517, July 1982.

[25] M. Wand. Semantics-directed machine architecture. In Conf. Rec. 9th ACM Symposium on Principles of Programming Languages, pages 234–241, 1982.

[26] M. Wand. Loops in combinator-based compilers. Information and Control, 57(2–3):148–164, May/June 1983.

[27] M. Wand. Compiler correctness for parallel languages. In 1995 Symposium on Functional Languages and Computer Architecture, June 1995. To appear. Preliminary version available via anonymous ftp

from ftp.ccs.neu.edu as /pub/people/wand/papers/parallel-compilers.ps.

[28] M. Wand and D. P. Oliva. Proving the correctness of storage representations. In Proc. 1992 ACM Symposium on Lisp and Functional Programming, pages 151–160, 1992.