λ_{S}: an Implicitly Parallel λ-Calculus with Letrec, Synchronization and Side-Effects

Computation Structure Group Memo 393 November 25, 1996

Arvind  MIT Lab for Computer Science
J-W. Maessen  MIT Lab for Computer Science
R.S. Nikhil  Digital Equipment Corp., Cambridge Research Lab
J.E. Stoy  Oxford University Computing Laboratory

Submitted to ICFP ’97

This research was conducted at the MIT Laboratory for Computer Science. Funding for this project was provided in part by the Advanced Research Projects Agency of the Department of Defense under Ft. Huachuca contract C-DABT63-95-C0150.

λ_{S}: an Implicitly Parallel λ-Calculus with Letrec, Synchronization and Side-Effects

Arvind  MIT Lab for Computer Science
J-W. Maessen  MIT Lab for Computer Science
R.S. Nikhil  Digital Equipment Corp., Cambridge Research Lab
J.E. Stoy  Oxford University Computing Laboratory

November 25, 1996

Abstract

λ_{S} extends the λ-calculus with letrecs, barriers, and updateable memory cells with synchronized operations. The calculus is designed to be useful for reasoning about compiler optimizations and, thus, allows reductions anywhere, even inside λ’s. Despite the presence of side-effects, the calculus retains fine-grained, implicit parallelism and non-strict functions; there is no global, sequentializing store. Barriers, for sequencing, capture a robust notion of termination. Although λ_{S} was developed as a foundation for the parallel functional languages pH and Id, we believe that barriers give it wider applicability– to sequential and explicitly parallel languages. In this paper we describe the λ_{S}-calculus and its properties which are based on a notion of observable information in a term. We also describe reduction strategies to compute the maximal observable information.

1 Introduction

The λ-calculus [9] and its variants have been invaluable in capturing the essence of languages such as Haskell [13], SML [17] and Scheme [11], providing the theoretical foundation for reasoning about and transforming programs in these languages. In this paper we describe the λ_{S}-calculus, another variant, intended as the formal basis for the parallel programming languages pH [2] (an extension of Haskell) and Id [18].

λ_{S} incorporates implicit parallelism, letrecs, synchronization and side-effects. The fine-grained parallelism evident in functional (especially non-strict) languages is exploited by default. Together with letrec, it permits programs with dynamic cyclic dependencies, a popular technique in lazy programs. The barrier is a control mechanism for sequencing. Side-effects are bundled with dataoriented synchronization in two mechanisms called I-structures [8] and M-structures [10]. We believe λ_{S} meets the following goals:

• An easy-to-understand operational semantics of pH. This includes a definition of observable values and a standard parallel reduction strategy to compute these values.

• Maximum flexibility, in order to reason about compiler optimizations. For example, it should permit reductions inside λ’s and conditionals (because this is what compilers do) even though such reductions may not occur during execution.

The novelty of λ_{S} lies in the way it treats barriers and side-effects. In the FP literature, introduction of side-effects is usually in the context of a sequential operational semantics (see, for example,

[12] and [16] for call-by-value languages, or state monads in Haskell [15]), and state is often modeled by a single global store with sequential operations. λ_{S}, on the other hand, introduces no such sequentialization, nor a separate store. The “store” is distributed throughout the term and we give small-step semantics for its manipulation. This is crucial for preserving implicit, fine-grained parallelism. Our barrier semantics captures a robust notion of “termination”. We believe it is powerful enough to explain call-by-value languages and sequential languages extended with concurrency primitives, and raw (unsynchronized) side-effects. Despite the presence of side-effects, our calculus places no restrictions on where reductions may take place in the term.

The introduction of side-effects requires a precise definition of sharing. There is a large body of literature dealing with sharing, such as [20], [14], [5] and [1]; these are motivated not by side-effects but by efficiency considerations (graph reduction, optimality, etc.), and often do not address letrecs and parallelism.

In this paper, we build up to λ_{S} in three stages. §2 describes λ_{C}, extending the λ-calculus with letrecs, conditionals, constants and functional data structures. The technical results of λ_{C} have already been achieved by Ariola and Blom [4]; we use this section to introduce our (somewhat different) notation and machinery. The results are similar for the functional subset, but the Ariola and Blom semantic model does not carry over to barriers and side-effects. §3 describes λ_{B}, adding sequencing barriers to λ_{C}. §4 describes λ_{S}, the full calculus, adding side-effects and data-oriented synchronization. In §5 we discuss parallel reduction strategies.

In each proposition we present, we follow the convention that, unless a limitation is explicitly stated, it holds for λ_{C}, λ_{B} and λ_{S}. Due to space limits, we omit all proofs, deferring them to a companion technical report [7] (in preparation). Furthermore, we assume that λ_{S} terms are generated from a statically typed language (like pH), and thus ignore reductions precluded by static type-checking.

2 λ_{C}: Letrecs, Constants and Functional Data Structures

λ_{C} is purely functional (no side-effects). Letrecs allow sharing of computations by binding an expression to an identifier which may be used in a number of places—including recursively in its own definition. While this may be viewed as merely an optimization in a purely functional language, it is semantically essential for barriers and side-effects. Theoretically, we could work without conditionals, constants and functional data structures, but we include them to improve intuition.

The calculus will be presented by describing the syntax of terms, equivalence rules for ignoring trivial syntactic differences between terms, and reduction rules.^{1} Then, we discuss equivalence between terms using a notion of printable observations. Finally, we discuss garbage collection, or erasure of irrelevant terms, which other authors often include in their reduction rules.

1As usual, the “e ⟶ e_{1}” denotes one application of a reduction rule; “e ⟶ ⟶ e_{1}” denotes a finite sequence (zero or more) of reductions. A redex is a term or subterm which is capable of reduction by one of the rules.

Syntax of λ_{C}

Expressions:

E ::= x | E E | λx.E  Identifiers, applications, abstractions
| { S in E }  Letrec blocks
| Cond(E,E,E) | PF_{k}(E_{1},⋯,E_{k})  Conditionals, primitive fn of arity k
| CN_{0} | CN_{k}(E_{1},⋯ E_{k})  Constants, constructors of arity k

Non-initial expressions:

| \underline{CN_{k}}(SE_{1},⋯ SE_{k})  Constructor values of arity k

Statements (in blocks):

S ::= ϵ  Empty statements
| x = E  Bindings
| S ; S  Parallel statements

The syntax of λ_{C} is shown above. Constants CN_{0} include numbers and booleans; functional data structure constructors CN_{k} include “cons”; primitives PF_{k} include arithmetic operators and projection functions (Proj_{j}) to select components of functional data structures. Non-initial expressions do not appear in user-written programs, but only as part of the reduction process. Arguments of \underline{CN_{k}}() are always simple expressions (SE, defined shortly: identifiers and values); with recursive blocks, this allows us to write cyclic data structures finitely. In a letrec block “{ S in E }”, E is called its return expression. We use the general term “statement” for S because λ_{S} will later introduce components that just perform side-effects. Empty statements are a technical convenience that become useful in λ_{B} and λ_{S}. The left-hand side identifiers in the bindings of S must be pair-wise distinct. The block has recursive scoping rules—any left-hand side identifier may be referred to in any right-hand side expression, as well as in the return expression.

Syntax of Values and Simple Expressions in λ_{C}: During reduction we need to instantiate an identifier’s use with its definition. We cannot instantiate arbitrary expressions, as this may replicate work and destroy sharing. We identify two subsets of λ_{C}, Values and Identifiers, together known as Simple Expressions, that are substitutable:

SE ::= x | V  Identifiers and values
V ::= λx.E | CN_{0} | \underline{CN_{k}}(SE_{1},⋯ SE_{k})

2.1 λ_{C} Syntactic Equivalence Rules

As in λ-calculus, bound variable names are just dummy names—their exact choice does not matter. Further, the exact textual order of statements in a parallel composition does not matter:

α-renaming:

λx.e  ≡ λt.(e[t/x])
{ x = e ; S in e_{0} } ≡ { t = e ; S in e_{0} }[t/x]

Equivalence properties of “;”

ϵ ; S  ≡ S
S_{1} ; S_{2}  ≡ S_{2} ; S_{1}
S_{1} ; (S_{2} ; S_{3})  ≡ (S_{1} ; S_{2}) ; S_{3}

α-renaming is done in the standard way; we omit details here. We use “e[t/x]” to denote expression e with all free occurrences of identifier x replaced by identifier t. We use e′ and S′ to denote renamed versions of e and S. t is always an identifier which does not otherwise occur in the left-hand term of the rule.

2.2 λ_{C} Reduction Rules

Function Application (β-reduction):

(λx.e_{1}) e_{2} ⟶ { t = e_{2} in e_{1}[t/x] } (β_{let})

There are two things to note about β_{let}. First, e_{2} can be an arbitrary expression, not just a value— this makes it non-strict. Second, we always preserve exactly one copy of e_{2}—unlike traditional β, which may copy or erase e_{2} depending on the number of uses of x in e_{1}. Together with the restricted instantiation rule below, this preserves sharing and side-effects, and is important for the semantics of barriers. β_{let} produces graph structured terms, whereas traditional β produces trees.

Instantiation (Substitution): Given x = a in a letrec block, where a is a simple expression, these reduction rules specify that we can replace uses of x by a:

{ x = a ; S in C[x] } ⟶ { x = a ; S in C[a] }  (Inst1)
x = a ; SC[x]  ⟶ x = a ; SC[a]  (Inst2)
x = a  ⟶ x = C[a]  (Inst3)
where a = C[x]

For lack of space we omit the obvious definitions of C[ ] and SC[ ] which are contexts (expressions and statements, respectively, into which we can plug an expression). There are no restrictions– substitutions can even occur inside λ’s. The calculus thus permits infinite unfolding of cyclic terms; we leave it to reduction strategies to control this.

Block flattening:

x = { S in e } ⟶ x = e′ ; S′  (Flat)

Expression lifting: Each rule below “lifts out” a nested expression by giving it a name (using α-renaming where necessary to avoid name conflicts). To prevent instantiation and lifting from alternating forever, lifting rules are inapplicable when e is a simple expression.

{ S in e }  ⟶ { S ; t = e in t }  (LiftB)
(e e_{2})  ⟶ { t = e in t e_{2} }  (LiftAp1)
(e_{1} e)  ⟶ { t = e in e_{1} t }  (LiftAp2)
Cond(e, e_{1}, e_{2})  ⟶ { t = e in Cond(t, e_{1}, e_{2}) }  (LiftCond)
P F_{k}(⋯, e, ⋯) ⟶ { t = e in P F_{k}(⋯, t, ⋯) }  (LiftPF)

Flattening and lifting produce new juxtapositions that trigger other reductions. For example:

f = { S_{1} in λx.e_{1} };  x = f a;      ⟶^{(Flat)}  f = λx.e′_{1} ; S′_{1};  x = f a;

which then allows us to instantiate f by λx.e′_{1} in the application. Note that we do not lift expressions from λ bodies, nor from the arms of a conditional. While safe in λ_{C}, such rules would be incorrect in λ_{B} and λ_{S} because they would “expose” (make observable) potential non-terminations or sideeffects that would normally be protected by those contexts.

Constants, conditionals, delta rules: As usual, we regard constants (CN_{0}) as already evaluated, and:

Cond(True, e_{1}, e_{2})  ⟶ e_{1}  (CondT)
Cond(False, e_{1}, e_{2})  ⟶ e_{2}  (CondF)
PF_{k}(v_{1},⋯,v_{k})  ⟶ w  (δ)  e.g., +(\underline{n},\underline{m}) ⟶ \underline{n + m}
proj_{j}(\underline{CN_{k}}(e_{1}, ⋯, e_{j}, ⋯)) ⟶ e_{j}  (Proj)

Constructors: Constructor terms in the initial program are reduced to constructor values:

CN_{k}(⋯, e_{j}, ⋯) ⟶ \{ ⋯; t_{j} = e_{j}; ⋯ in \underline{CN_{k}}( ⋯, t_{j}, ⋯) \}  (Cons)

Here, e_{j} need not be a simple expression. The resulting “\underline{CN_{k}}()” term has identifier arguments and, thus, there are no lifting rules for constructors.

2.3 Comparing terms for information content

Having presented the calculus for λ_{C}, we must now ask if there is a non-trivial notion of the “meaning” of a term that is preserved under reduction. It is traditional here to discuss the “normal form” of a term and reduction strategies to achieve it.^{2} Unfortunately, because of letrec blocks, direct syntactic characterizations (such as normal forms) are problematic. First, terms may contain irrelevant clutter (since β_{let} does not discard argument expressions). But even if we are tempted to use “garbage collection” rules to erase clutter, the following result suggests that letrec blocks make syntactic comparisons futile:

Proposition 1 (Non-confluence (Ariola and Klop [6])) λ_{C} is not confluent.

To see this, consider this term, which represents an infinite list of alternating 1’s and 2’s:

    \{ x  =  \underline{Cons}(1, y) ; y  =  \underline{Cons}(2, x)    in    x \}

Let us take two paths, by substituting for x and for y, respectively. The resulting terms are:

    \{ x  =  \underline{Cons}(1, y) ; y  =  \underline{Cons}(2, \underline{Cons}(1, y))    in    x \}  (M_{1})
    \{ x  =  \underline{Cons}(1, \underline{Cons}(2, x)) ; y  =  \underline{Cons}(2, x)    in    x \}  (M_{2})

From this point on, in M_{1} the y definition will always contain y, whereas in M_{2} the y definition will always contain x, i.e., we can never bring these two terms together syntactically again. However, M_{1} and M_{2} will behave identically in all contexts.

Thus, instead of syntactic comparisions, we compare observable behavior. We first discuss the “instantaneous print” or Print[[]] of a term. Then we discuss the “full print” or Print*[[]] of a term, i.e., what can be observed about a term after reduction.

2.3.1 Print[[]]: instantaneous observable information in a term

Print[[e]] transforms a term into the syntax E_{P}. It preserves constants and constructors; replaces applications, conditionals and nested letrecs by the symbol “⊥”; replaces any λ-expression with the symbol “λ” (and ignores the λ-body), and so on.

To handle cyclic terms, we define printing in two stages: a Print[[]] function captures the graph structure of the term, and an Unfold() function flattens graphs into trees that can be compared. Print[[]] produces terms with the following syntax:

\begin{aligned}E_{P} & ::= & V_{P} & | & \{ S_{P} in SE_{P} \} \\ S_{P} & ::= & ϵ & | & x = V_{P} | S_{P} ; S_{P} \\ SE_{P} & ::= & x & | & V_{P} \\ V_{P} & ::= & ⊥ & | & λ | CN_{0} | CN_{k}(SE_{P_{1}}, ⋯ SE_{P_{k}}) \end{aligned}

2It is also possible to map terms to a separate space of denotational meanings (see, e.g., [19]), but for λ_{B} and λ_{S} this is quite complicated and (for λ_{S}) rather indirect.

Print[[]] simply discards λ bodies, applications, conditionals, nested blocks, etc.:

Print[[{ S in E }]]  = { Print_{S}[[S]] in Print_{SE}[[E]] }
Print[[E]]  = Print_{V} [[E]]  otherwise
Print_{S}[[ϵ]]  = ϵ
Print_{S}[[x = E]]  = x = Print_{V} [[E]]
Print_{S}[[S_{1}; S_{2}]]  = Print_{S}[[S_{1}]] ; Print_{S}[[S_{2}]]
Print_{V} [[λx.E ]]  = λ
Print_{V} [[CN_{0} ]]  = CN_{0}
Print_{V} [[\underline{CN_{k}}(⋯, e_{j}, ⋯)]] = CN_{k}(⋯, Print_{SE}[[e_{j}]], ⋯)
Print_{V} [[E]]  = ⊥  otherwise
Print_{SE}[[x]]  = x
Print_{SE}[[E]]  = Print_{V} [[E]]

Unfold_{n}() does a finite unfolding of outputs of Print[[]], producing trees with the following syntax:

T_{P} ::= ⊥ | λ | Ω | CN_{0} | CN_{k}(T_{P 1}, ⋯ T_{P k})

It prints values, and follows bindings (including arguments of data structures) by keeping an environment of bindings. However, it follows bindings through the environment only up to a finite depth n, bottoming out by printing Ω. Ω is equivalent to ⊥, but we use it as a technical convenience to distinguish partially-unfolded printable terms from unevaluated printable terms.

Unfold_{n}({S_{P} in SE_{P} })  = Unfold′_{n}(SE_{P}) (Env S_{P} {∀x.x ↦ ⊥}) generate nodes
Unfold_{n}(V_{P})  = V_{P}
Unfold′_{0}(x) ρ  = Ω
Unfold′_{n}(x) ρ = Unfold′_{n−1}(ρ(x)) ρ one unfolding
Unfold′_{n}(CN_{k}(⋯, e_{j}, ⋯)) ρ = CN_{k}(⋯, Unfold′_{n}(e_{j}) ρ, ⋯)
Unfold′_{n}(V_{P}) ρ  = V_{P}  otherwise
Env(ϵ) ρ  = ρ
Env(x = V_{P}) ρ  = ρ{x ↦ V_{P} }
Env(S_{P 1}; S_{P 2}) ρ  = Env(S_{P 1}) (Env(S_{P 2}) ρ)

Because Print[[]] does not unfold cyclic terms, it always terminates. When we Print[[]] these terms representing an infinite list of ones:

{ x  =  Cons(1, x)                       in    x }
{ x  =  Cons(1, y);  y  =  Cons(1, x)    in    x }

we get E_{P} terms that look the same as the original E terms. When we then Unfold_{n}() them, we obtain a list of n ones terminated by Ω:

Cons(1, Cons(1, Cons(1, . . . Ω). . .)

In order to compare T_{P} trees, we define the following ordering:

Ω  = ⊥
⊥  ⊑ T_{P}
λ  ⊑ λ
CN_{0}  ⊑ CN_{0}
CN_{k}(v_{1}, ⋯, v_{j} ⋯, v_{k}) ⊑ CN_{k}(v_{1}, ⋯, v′_{j} ⋯, v_{k})  if v_{j} ⊑ v′_{j}

We now have a way to compare E_{P} terms. A term E_{1} “contains less information” than another term E_{2} if each finite unfolding of E_{1} is less than some finite unfolding of E_{2}; and, equivalence of two E_{P} terms can be derived in the usual way from this ordering:

E_{P 1} ⊑ E_{P 2}  ⇔  ∀n.∃m.Unfold_{n}(E_{P 1}) ⊑ Unfold_{m}(E_{P 2})
E_{P 1} = E_{P 2}  ⇔  E_{P 1} ⊑ E_{P 2} and E_{P 2} ⊑ E_{P 1}

Proposition 2 (Print monotonicity) If e ⟶ ⟶ e_{1} then Print[[e]] ⊑ Print[[e_{1}]]

λ_{C} is not confluent, but two reduction paths can always be reunited so their print values match:

Proposition 3 (Print confluence in λ_{C}) If e ⟶ ⟶ e_{1} and e ⟶ ⟶ e_{2}, then there exist e′_{1} and e′_{2} such that e_{1} ⟶ ⟶ e′_{1} and e_{2} ⟶ ⟶ e′_{2}, and Print[[e′_{1}]] = Print[[e′_{2}]]

The following theorem is very important: it assures us that we have not lost any computational power by enforcing sharing using letrec blocks and restricted substitution.

Definition (λ_{0}): Let λ_{0} be the calculus without any restriction on instantiation, i.e., an identifier may be instantiated by an arbitrary expression, not just a simple expression.

Proposition 4 (Fundamental theorem of graph reduction in λ_{C} (Ariola and Blom [4]))

If e ⟶ ⟶ e_{1} in λ_{0}, then ∃e_{2} such that e ⟶ ⟶ e_{2} in λ_{C}, and Print[[e_{1}]] ⊑ Print[[e_{2}]].

2.3.2 Print*: all potentially observable information in a term

Print*[[]] is a set of printed terms representing the maximal printable information that can be obtained from a term or any of its reductions. We obtain Print*[[e]] by looking at the outcome of every possible reduction sequence starting at e. A reduction sequence of a term e is a partial function from natural numbers N to E. It is partially defined up to some n (with s_{0} being e itself), and it is a reduction sequence in that for any two adjacent defined elements s_{j−1}, s_{j}, the former reduces in one step to the latter. We write s_{j}↑ or s_{j}↓ when s is defined or undefined, respectively, at j.

Definition (Reduction Sequence):

RS(e) = {s | s_{0} = e ∧ ∀j.s_{j}↓⇒ s_{j+1}↓ ∧ ∀j > 0.s_{j}↑⇒ s_{j−1} ⟶ s_{j}}

The Complete Reduction Sequences for an expression e are all reduction sequences starting at e which are either infinte, or whose final term contains no redexes:

Definition (Complete Reduction Sequences):

CRS(e) = {s ∈ RS(e) | ∀j > 0.s_{j}↑∧ s_{j+1}↓⇒∄e′.s_{j} ⟶ e′)}

If we Print[[]] each term in a sequence, we get an ascending chain of E_{P} terms (monotonicity). Intuitively, we want the least upper bound of this chain as the “final” print value. However, since chains may be infinite and E_{P} terms only form a preorder, we use the domain E_{P}^{∗} ⊃ E_{P} which is isomorphic to the ideal completion of E_{P} (and where the isomorphism preserves E_{P}), in which we can take least upper bounds:

Definition (Print*[[]]): Print*[[e]] = { ⨆_{j∈ω,s_{j}↑} Print[[s_{j}]] | s ∈ CRS(e) }

Proposition 5 (Print* determinacy in λ_{C}) In λ_{C}, Print*[[e]] has precisely one element.

Proposition 6 (Print* preservation in λ_{C}) In λ_{C}, if e ⟶ ⟶ e_{1} then Print*[[e]] = Print*[[e_{1}]].

2.3.3 Termination

A stable term is one whose Print[[]] no longer changes under further reduction:

Definition (stable terms): A term e is stable if Print*[[e]] = { Print[[e]] }.

It is undecidable in general whether a term is stable; this motivates the identification of the following classes of stable terms.

Definition (terminated terms): Terminated terms are described by the following syntax:

\begin{aligned}ET & ::= & V | \{ H in SE \} \\ H & ::= & x = V | H ; H \end{aligned}

A terminated expression contains no applications, conditionals, etc., unless they are inside a λabstraction or arm of a conditional.

Proposition 7 (Stability of terminated terms) If e ∈ ET, then e is stable.

Consider the following two terms:

    x = ⊥  and  { x = Cons(1,x)    in    x }

When we Print[[]] and unfold them, the former gives ⊥, whereas the latter gives Cons(1, Cons(⋯,Ω)). It is for this reason alone that we make a distinction between ⊥ and Ω, and this motivates the following:

Definition (ground-printing terms): In a ground-printing term e, Unfold_{n}(Print[[e]]) does not contain ⊥ for every n larger than some m.

Note that a ground-printing term is always stable, but it may not have terminated; this is possible because Print[[]] does not explore “irrelevant” computations, which may never terminate.

2.4 Garbage Collection of irrelevant terms in λ_{C}

Our β_{let} rule does not discard argument terms, even if the formal parameter is unused. Thus, terms may contain irrelevant clutter. Our calculus is free of GC rules, and we can study GC as a separate topic.

Definition (garbage collection, or GC): GC is a transformation from E to E that erases part of a term,^{3} such that for any context C, Print*[[C[e]]] = Print*[[C[GC[[e]]]]]

The following is a proposed garbage collection process:^{4}

Definition (garbage collection rule GC_{0}):

{ S_{G} ; S in e } ⟶{ S in e }  where  ∀x ∈ FV(S) ∪ FV(e): x ∉ BV(S_{G})

In other words, if S and e do not use any identifier defined by S_{G}, then S_{G} can safely be erased. GC_{0} can be applied anywhere (including inside λ bodies).

Proposition 8 (GC of unreachable terms (in λ_{C})) In λ_{C}, GC_{0} is a correct rule.

3The Print[[]] function, of course, erases irrelevant differences, but it transforms E to E_{P} and does not preserve deep structure (e.g., λ bodies).

4FV(e) are the free variables of e. BV(s) are the top-level bound variables of statement s, i.e., the left-hand sides of all bindings comprising s. FV(s) are the free variables of statement s, i.e., the free variables of the right-hand sides of all bindings comprising s, minus the variables that s itself defines (i.e., minus BV(s)).

3 λ_{B}: adding Barriers to λ_{C}

We now add a control mechanism called the barrier, which sequences statements in a letrec block. λ_{B} remains purely functional (no side-effects). Barriers get their practical motivation from controlling side-effects which are discussed later, but their semantic implications are evident in a purely functional setting. Since λ_{B} differs from λ_{C} in only a small way, we present it here informally.^{5} The new syntax is:

S ::= S_{1} --- S_{2}  Barriers

S_{1} (the pre-region) must terminate before S_{2} (the post-region) is visible to the rest of the term. The sequencing involves only these two subterms. Our static recursive scoping rule for letrec bindings remains the same—in this respect, there is no difference between barriers and semicolons. To α-renaming and semicolon equivalences, we add a new syntactic equivalence:

((H ; S_{1}) --- S_{2}) ≡ H ; (S_{1} --- S_{2})

(Recall, from our discussion on terminated terms, that: H ::= x = V | H ; H). This allows value bindings to escape from pre-regions. The escaped bindings may enable other instantiations in the surrounding context. When all such bindings escape, the barrier can be discharged:

\begin{matrix}ϵ --- S & ⟶ & S & (BAR1) \\ S --- ϵ & ⟶ & S & (BAR2) \end{matrix}

It follows that the barrier can be discharged as soon as the pre-region has terminated:

(H --- S) ⟶ (H ; S)

In Print[[]], we add a clause that omits statements from post-regions:

Print_{S}[[ S_{1} --- S_{2} ]] = Print_{S}[[S_{1}]]

A terminated term in λ_{B} contains no barriers unless it is inside a λ or conditional (just as it contains no application unless it is inside such sub-terms).

All λ_{C} propositions hold in λ_{B} except for Prop. 8 (correctness of GC_{0}). The post-region of a barrier has no effect on the computation until the barrier is discharged:

Proposition 9 (Opacity of post-regions) If C[S_{1} --- S_{2}] ⟶ ⟶ C′[S′_{1} --- S′_{2}] then ∃ C′′ such that C[S_{1}---S_{2}] ⟶ ⟶ C′′[S′_{1}---S_{2}] ⟶ ⟶ C′[S′_{1}---S′_{2}]

i.e., it is always possible to concentrate on S_{1} and ignore S_{2} until the barrier is discharged.

Proposition 10 (Barrier associativity) In all contexts, S_{1}---(S_{2}---S_{3}) ≡ (S_{1}---S_{2})---S_{3}

The sole difference between λ_{C} and λ_{B} is this:

Proposition 11 (Barriers constrain results) Print*[[C[S_{1}---S_{2}]]] ⊑ Print*[[C[S_{1};S_{2}]]]

where the P_{1}⊑P_{2} means that for every p_{1} in P_{1}, there is a p_{2} in P_{2} such that p_{1}⊑p_{2}. Barriers essentially make it possible to observe non-termination. When placed before a barrier, the lefthand term below will allow the barrier to discharge, whereas the right-hand term will not:

5However, it should be noted that this presentation and the semantics of barriers themselves differ from indirect semantics given previously [3].

Expressions:

E ::= x | E E | λx.E | { S in E } | Cond(E,E,E) (as before)
| PF_{k}(E_{1},⋯,E_{k}) | CN_{0} | CN_{k}(E_{1},⋯ E_{k})  (as before)
| allocate()  Cell allocation
| I-Fetch(E) | M-Fetch(E)  I- and M-structure fetch

Non-initial expressions:

| \underline{CN_{k}}(SE_{1},⋯ SE_{k})  (as before)
| O_{j}  Cell identifiers

Statements (in blocks):

S ::= ϵ | x = E | S ; S | S --- S  (as before)
| S-Store(E,E)  Synchronized store

Non-initial statements:

| heap  Heap allocator
| empty(O_{j}) | error(O_{j}) | full(O_{j},V)  Empty, error, full cells

Figure 1: Syntax of λ_{S}

     5  { x = ⊥ in 5 }

Garbage collection of irrelevant terms in λ_{B}: Because GC_{0} can affect termination, which is now observable, GC_{0} is no longer correct for λ_{B}. We constrain the GC rule so that only unreachable bindings which have terminated are erased.

Definition (garbage collection rule GC_{v}):

\{ B ; S in e \} ⟶\{ S in e \} \begin{matrix}where ∀x ∈ FV(S) ∪ FV(e): x ∉ BV(B) \\ and B is defined by the syntax: B ::= x = V | B ; B \end{matrix}

Proposition 12 (GC of unreachable terminated terms) GC_{v} is a correct rule.

4 λ_{S}: adding side-effects and data-oriented synchronization

λ_{S} is the full calculus, obtained by adding updateable memory cells that are dynamically allocated in a heap.^{6} Each cell can be in a full or empty state, which affects the behavior of cell operations. Our formulation preserves small-step semantics (local rules) for fine-grain parallelism; there is no global “store”.

The syntax of λ_{S} is shown in Figure 1. allocate() produces a new, empty cell named by a cell identifier O_{j}. S-Store, I-Fetch and M-Fetch are cell operations that depend on and affect the cell state. Just before execution, we introduce a “heap” term as follows:

e ⟶ { heap in e }  (e is the entire program)

This is not a reduction rule; it just prepares the orginal program for execution.

Syntax of Values and Simple Expressions in λ_{S}: we add cell identifiers:

V ::= λx.E | CN_{0} | \underline{CN_{k}}(x_{1},⋯ x_{k})  (as before)
| O_{j}  Cell identifiers

6Functional data structures in λ_{C} could also have been explained with an explicit heap.

Heap Terms in λ_{S}: as before, heap terms are “quiescent” (including value statements):

H ::= x = V | H ; H  (as before)
| heap  Heap allocator
| empty(O_{j}) | error(O_{j}) | full(O_{j},V)  Empty, error, full cells

The syntactic equivalence rules (α-renaming, semicolons, barriers) remain unchanged.

4.1 λ_{S} Reduction Rules

New lifting rules: Here, t represents a variable which does not otherwise occur, and e ∉ SE:

     S-Store(e,e_{2}) ⟶ ( t = e ; S-Store(t,e_{2}) )  (LiftS-Store1)
     S-Store(e_{1},e) ⟶ ( t = e ; S-Store(e_{1},t) )  (LiftS-Store2)

Cell operations: allocate() creates a new memory cell, named by a new cell identifier:

     ( heap ; x = allocate() ) ⟶ ( heap ; empty(O_{j}); x = O_{j} )  (Alloc)

where O_{j} is a new cell identifier

The heap term remains unchanged; it merely enables allocation. Because there are no rules to move the heap term into λ’s, into conditionals or below barriers, allocation cannot occur in such regions; allocation can only occur in “exposed” computations. This rule also sequentializes: only one allocation can occur at a time. This can be trivially relaxed to a fixed degree of parallelism p by introducing p heap terms at the start. It can even be relaxed to an unlimited degree of parallelism by adding the reduction rule:

    heap ⟶ heap ; heap

(we merely have to ensure that our standard reduction strategy does not get stuck in this rule.) We can store a value into an empty cell, but not into a full cell:

     (empty(O_{j}); S-Store(O_{j}, v))  ⟶ full(O_{j}, v)  (S-Store)
     (full(O_{j}, v); S-Store(O_{j}, w)) ⟶ error(O_{j})  (S-StoreErr)

The argument terms must be a cell identifier and a value, not arbitrary expressions, i.e., a cell can only store a value. The I-Fetch and M-Fetch rules say that a value can be extracted from a full cell. However, they differ in the resulting state of the cell:

     (full(O_{j}, v); x = I-Fetch(O_{j})) ⟶ (full(O_{j}, v); x = v)  (I-Fetch)
     (full(O_{j}, v); x = M-Fetch(O_{j})) ⟶ (empty(O_{j}); x = v)  (M-Fetch)

I-Fetch leaves the cell unchanged, allowing further reads. M-Fetch empties the cell, requiring another S-Store before further reads. This captures the “I-structure” and “M-structure” synchronization behavior in pH. These rules make λ_{S} non-deterministic. Consider these two program fragments:

           empty(O_{1}) ;                                   empty(O_{1}) ;
           S-Store(O_{1}, v) ;                              S-Store(O_{2}, m) ;
           S-Store(O_{1}, w) ;                             S-Store(O_{2}, n) ;
           x = I-Fetch(O_{1})                               y = M-Fetch(O_{2})

Since “;” permits various orderings, we can produce any of the following outcomes (respectively):

     ⟶ ⟶ Error(O_{1}); x = I-Fetch(O_{1})  ⟶ ⟶ Error(O_{2}); y = M-Fetch(O_{1})
     or  Error(O_{1}); x = v  or  Full(O_{2}, m); y = n
     or  Error(O_{1}); x = w  or  Full(O_{2}, n); y = m

4.2 Properties of λ_{S}

Print[[]] and Print*[[]] remain unchanged. Print*[[]] can now contain more than one element. Print monotonicity (Prop. 2) continues to hold, but Print confluence (Prop. 3), Print* determinacy (Prop. 5), and Print* preservation (Prop. 6) no longer hold; performing an M-Fetch may preclude certain reductions that would have been possible by doing that M-Fetch later. The net effect is that the set of reachable values becomes smaller. Thus, Print* preservation (Prop. 6) must be weakened:

Proposition 13 (Print* contraction) If e ⟶ ⟶ e_{1} then Print*[[e_{1}]] ⊆ Print*[[e]]

All other propositions continue to hold: Stability of terminated terms (Prop. 7); Opacity of postregions (Prop. 9); Barrier associativity (Prop. 10); Barriers constrain results (Prop. 11), and GC_{v} of unreachable terminated terms (Prop. 12). A more aggressive GC rule could also eliminate S-Store’s and full cells for which it can be shown that no matching I- or M-Fetch is possible.

4.3 I-Structure Subset of λ_{S}

Definition (I-structure subset): λ_{I} is λ_{S} without the M-Fetch syntax and rules.

This subset is important because cells with S-Store and I-Fetch operations express the same idea as “logic variables”, “single-assignment variables”, “communication variables”, etc. found in logic and constraint programming languages. If a reduction sequence terminates without a store error, then the print-result is unique:

Proposition 14 (Termination is unique (in λ_{I})) If e ⟶ ⟶ e′ and e′ is terminated and errorfree,

then Print*[[e]] = { Print[[e′]] }

and all reduction sequences produce a store error on a location O_{j} if any one of them does:

Proposition 15 (Store error confluence (in λ_{I})) If e ⟶ ⟶ e_{1} and e ⟶ ⟶ e_{2}, and e_{1} is C[error(O_{j})], then e_{2} ⟶ ⟶ e′_{2}, where e′_{2} is C′[error(O_{j})]

Thus, although λ_{I} is non-deterministic (as demonstrated in the left column of the example in Section 4.1), it is more benign: if we consider all programs containing any error() as equivalent, then λ_{I} can be considered to produce deterministic results (this is exactly the view taken in the language pH).

5 Reduction Strategies for λ_{S}

A reduction strategy is a method to choose amongst many available redexes. Traditionally, a standard reduction strategy σ produces a term with at least as much information as is obtainable from any other strategy, i.e., if e ⟶ ⟶ e_{1} in the calculus, then there is an e_{2} such that e ⟶ ⟶^{σ}e_{2} according to the standard reduction strategy σ, and Print[[e_{1}]] ⊑ Print[[e_{2}]]. This notion needs elaboration in the presence of non-determinism. Consider the following example (let x be an empty cell):

    { S-Store(x,1);
       (  y1 = M-Fetch(x)  ---  S-Store(x,2) );  (F_{1})
       y2 = M-Fetch(x)  (F_{2})
    in
       (y1, y2) }

The two M-Fetch operations may execute in any order. If F_{1} executes first, the result of the block will be (1,2). If F_{2} executes first, then F_{1} waits on an empty cell, and the result is (⊥,1). No deterministic strategy can produce both outcomes. This motivates the following two variants of standard reduction. Let Print∗ σ[[]] be a version of Print*[[]] that uses only reductions permitted by the strategy.

Definition (Strong and Weak standard reduction): A reduction strategy σ is strongly standard when ∀e. Print∗ σ[[e]] = Print*[[e]] and weakly standard when ∀e. Print∗ σ[[e]] ⊆ Print*[[e]].

Any deterministic strategy can only hope to be weakly standard. But even such a strategy is non-trivial. If we threw in the (irrelevant) statement “y3=⊥_{y}” in the above example, it must not get stuck in ⊥_{y} and produce (⊥,⊥); it must still produce either (1,2) or (⊥,1).

In this section, we develop a weakly standard parallel strategy. We first define a kernel language, a subset of E (assuring ourselves that we have not thereby lost expressive power). Then, we limit instantiation and reduction to the outermost parts of the term. This enforces the barrier synchronization discipline and prevents infinite recursion; it also harmlessly postpones some operations which can safely be left until they appear in an exposed context. Finally, we ensure that we choose fairly among available instantiations, to avoid getting stuck in an infinite sequence of reductions that are irrelevant to the observable part of a term.

The kernel language is defined by the following (compare with Fig. 1):

Kernel Terms:

E ::= x | SE SE | λx.E | { S in SE }
| Cond(SE,E,E) | PF_{k}(SE_{1},⋯,SE_{k}) | CN_{0} | \underline{CN_{k}}(x_{1},⋯ x_{k})

         | allocate() | O_{j} | I-Fetch(SE) | M-Fetch(SE)

S ::= ϵ | x = E | S ; S | S --- S

         | heap | S-Store(SE,SE) | empty(O_{j}) | error(O_{j}) | full(O_{j},V)

An initial term can be kernelized by repeated application of the “lifting” rules: LiftB, LiftAp1, LiftAp2, LiftCond, LiftPF, LiftS-Store1, LiftS-Store2, and Cons.

Proposition 16 (Kernelization confluence) kernelization is confluent up to syntactic equivalence (α-renaming, properties of “;” and “---”) and is strongly normalizing (always terminates).

Proposition 17 (Kernelization is static) A kernel expression remains a kernel expression after further reduction.

Proposition 18 (Expressivity of kernel language) If e_{k} is the kernelized version of e, then Print*[[e]] = Print*[[e_{k}]].

The remaining reduction rules are called dynamic rules: β_{let}, Inst2, Flat, CondT, CondF, δ, Proj, BAR1, Alloc, S-Store, S-StoreErr, I-Fetch, M-Fetch.

Limited contexts for instantiation and reduction: We want to perform reductions only where computations are “exposed” (avoiding λ-bodies, arms of conditionals, and post-regions) and we want to prevent useless unfolding of cyclic data structures. We thus limit the contexts^{7} where an identifier may be instantiated and where reductions may occur:

Limited instantiation contexts:

C[ ] ::= [ ] | [ ] SE | Cond([ ],E,E) | PF_{k}(⋯,[ ],⋯)
SC[ ] ::= x = C[ ] | SC[ ] ; S | SC[ ] --- S | S-Store(C[ ], E) | S-Store(E, C[ ])

Limited reduction contexts:

C[ ] ::= [ ] | { SC[ ] in SE }
SC[ ] ::= [ ] | x = [ ] | SC[ ] ; S | SC[ ] --- S

Fairness: The only remaining way to get stuck in an irrelevant sequence of reductions is by repeatedly applying recursive λ-expressions. We avoid this by insuring that we instantiate only a finite amount before turning our attention to other reductions. We decorate a λ-expression with a positive integer, decrementing it each time we instantiate it. Eventually, the decoration reaches zero, disallowing further instantiation:

x = a ; SC[x]  ⟶ x = a ; SC[a]  a ≠ λ^{n}y.e  (Inst2a)
x = λ^{n}y.e ; SC[x] ⟶ x = λ^{n−m}y.e ; SC[λ^{m}y.e]  n ≥ m > 0  (Inst2b)

Definition (σ_{n}, the weak standard reduction strategies for λ_{S})

1. Compute the kernel form of the initial term.

2. While the term is not a terminated term: 2.1 Decorate all λ abstractions with the positive integer n > 0. 2.2 Apply the dynamic rules (with limited contexts, etc.), in any order, even in parallel,

until no longer possible.

This is a family of strategies, parameterized by n and by the choices in Step 2.2. Still, for any n, each invocation of this step will always terminate. The choices in this step represent a kind of non-determinism. For λ_{C} and λ_{B}, this non-determinism is benign—there is still a unique outcome, and this strategy will find it, even if n = 1 (and so it is strongly standard). However in λ_{S} any particular choice of n, no matter how large, can force the program’s non-determinism to be resolved too early, thereby ruling out some outcomes. Consider this variant on our previous example:

    { f = λj. if (j > 1) then f (j-1)
                else { (  y = M-Fetch(x) --- S-Store(x,2)) (F_{1})
                     in
                        y }
       S-Store(x,1);
       y1 = f m;
       y2 = M-Fetch(x)  (F_{2})
    in
       (y1, y2) }

Now f must be instantiated m times before F_{1} executes. Again, if F_{1} executes before F_{2}, the result is (1,2), but if F_{2} executes first, the result is (⊥,1). However, if n < m, it forces us to execute F_{2} first, so the only possible outcome is (⊥,1).

Other interesting reduction strategies: Closely related is the strategy σ which non-deter-ministically chooses the n used to annotate the λ’s at each step. By choosing a sufficiently large n at each step we insure that every possible outcome can be reached by some choice of reductions within the strategy. Thus, σ is strongly standard.

7Technically we need to specify, separately, contexts for plugging in an E given an E, for plugging in an S given an E, for plugging in an E given an S, and so on. We overload things, hoping the meaning is always clear.

Suppose we ignore fairness; call this strategy σ_{0}. This would have the same termination behavior as σ_{n}, but may print less of an answer than σ_{n}. Consider this program:

    { K = λx.λy.x ;   loop = λx.loop x    in    K v (loop a) }

Neither σ_{n} nor σ_{0} will terminate; however, under σ_{n} we will eventually print (the value of) v, whereas under σ_{0} we may print ⊥ forever by never reducing the K application. For programs that do have a terminal form, σ_{0} is adequate—fairness is not necessary:

Proposition 19 (σ_{0} is standard for terminating terms)

If e ⟶ ⟶ e_{1} and e_{1} ∈ ET, then e ⟶ ⟶^{σ_{0}} e_{2} and Print[[e_{1}]] ⊑ Print[[e_{2}]]

Recall that λ_{C} (purely functional) is deterministic. A lazy reduction strategy focuses on “outermost” redexes, always picking one that is needed to produce the answer. Ariola et al. [4] show such a strategy, and show that it is standard for λ_{C}. We can give a parallel strategy σ_{plazy} identical to σ_{n}, except that we continue evaluation only while the term is not ground-printing (defined in Sec. 2.3.3). The final term may still contain redexes, but further reductions will not affect the printed value (and so termination here makes sense). Indeed, σ_{plazy} finds answers equivalent to those found by lazy reduction.

6 Conclusion

In this paper, we have described λ_{S}, a fine-grained parallel extension of the λ-calculus with letrec, barriers (for sequencing), and synchronized side-effects. The calculus avoids any encoding into the reduction rules of considerations inspired by reduction strategy. This makes the calculus more flexible and, therefore, more useful for reasoning about program transformations.

Based on the notion of observable information, we have discussed a number of important properties of λ_{S} and its important sub-calculi, λ_{C}, λ_{B} and λ_{I}. We have described parallel strong and weak standard reduction strategies to compute the maximum information in a term. A simple variation of our strategy subsumes traditional lazy evaluation.

Our barrier semantics capture a robust notion of termination: in (S_{1} --- S_{2}), we wait for all of the dynamic computation in S_{1}. We believe that this gives λ_{S} wide applicability, and will allow us to model a spectrum of languages: fine-grained implicitly parallel languages like pH and Id; totally sequential languages (by inserting barriers everywhere); and points in between, such as Scheme extended with futures. Barrier sequencing also makes raw (unsynchronized) side effects manageable locally without compromising parallelism globally.

We believe that λ_{S} is a simple, flexible, and powerful calculus that will facilitate the study of realistic parallel languages with side-effects.

References

[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. J. of Functional Programming, 1(4):375–416, 1991.

[2] S. Aditya, Arvind, L. Augustsson, J.-W. Maessen, and R. S. Nikhil. Semantics of pH: A Parallel Dialect of Haskell. In Proc. Haskell Wkshp. (FPCA 95), La Jolla CA, USA, June 1995.

[3] S. Aditya, Arvind, and J. Stoy. Semantics of barriers in a non-strict, implicitly-parallel language. In Functional Programming and Computer Architecture, 1995.

[4] Z. M. Ariola and S. Blom. Cyclic lambda calculi. Technical Report CIS-TR-96-13, Dept. of Computer and Information Sciences, Univ. of Oregon, Eugene OR, USA, 1996.

[5] Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. The call-by-need lambda calculus. In Proc. ACM Conf. on Principles of Programming Languages, pages 233–246, 1995.

[6] Z. M. Ariola and J. W. Klop. Cyclic lambda graph rewriting. In Proc. Ninth Symp. on Logic in Computer Science (LICS’94), Paris, France, pages 416–425, 1994.

[7] Arvind, J.-W. Maessen, R. S. Nikhil, and J. E. Stoy. λ_{S}: An implicitly parallel λ-calculus with letrec, synchronization and side-effects. Technical report, MIT Laboratory for Computer Science, 545 Technology Square, Cambridge MA 02139, USA, in preparation. (Full version with proofs).

[8] Arvind, R. S. Nikhil, and K. K. Pingali. I-Structures: Data Structures for Parallel Computing. ACM Trans. on Programming Languages and Systems, 11(4):598–632, October 1989.

[9] H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North Holland, Amsterdam, 1981.

[10] P. Barth, R. S. Nikhil, and Arvind. M-Structures: Extending a Parallel, Non-strict, Functional Language with State. In Springer Verlag LNCS 523 (Proc. Functional Programming and Computer Architecture, Cambridge MA, USA), pages 538–568, 1991.

[11] W. Clinger and J. Rees (eds.). Revised^{4} Report on the Algorithmic Language Scheme. Technical report, MIT AI Laboratory, November 2 1991.

[12] M. Felleisen and D. P. Friedman. A syntactic theory of sequential state. Theoretical Computer Science, 69:243–287, 1989.

[13] P. Hudak et.al. Report on the Programming Language Haskell, A Non-strict, Purely Functional Language, Version 1.2. ACM SIGPLAN Notices, 27(5), May 1992.

[14] J. Launchbury. A Natural Semantics for Lazy Evaluation. In Proc. ACM Conf. on Principles of Programming Languages, pages 144–154, 1993.

[15] J. Launchbury and S. L. Peyton Jones. Lazy Functional State Threads. In Proc. ACM SIGPLAN ’94 Conf. on Programming Language Design and Implementation, Orlando FL, USA, pages 24–35, June 22-24 1994.

[16] I. A. Mason and C. L. Talcott. Equivalence in Functional Languages with Effects. J. of Functional Programming, 1(3):287–327, July 1991.

[17] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, Cambridge MA, USA, 990.

[18] R. S. Nikhil. Id (Version 90.1) Language Reference Manual. Technical Report CSG Memo 284-2, MIT Lab for Computer Science, 545 Technology Square, Cambridge MA 02139, USA, July 15 1991.

[19] J. E. Stoy. The Semantics of Id. In A Classical Mind: Essays in Honor of C.A.R.Hoare (A.W.Roscoe, ed.), pages 379–404. Prentice Hall, New York, 1994.

[20] C. P. Wadsworth. Semantics and Pragmatics of the Lambda-calculus, 1971. D.Phil. thesis, University of Oxford.