Well-Founded Touch Optimization for Futures

Cormac Flanagan Matthias Felleisen

Rice COMP TR94-239

October 1994

Department of Computer Science Rice University P.O. Box 1892 Houston, TX 77251-1892

Copyright \begin{matrix}c \\ ◯ \end{matrix}1994 by

Cormac Flanagan and Matthias Felleisen

Cormac Flanagan^{∗} Matthias Felleisen^{∗}

Department of Computer Science, Rice University, Houston, TX 77251-1892

Abstract

The future annotations of MultiLisp provide a simple method for taming the implicit parallelism of functional programs, but require touch operations at all placeholderstrict positions of program operations to ensure proper synchronization between threads. These touch operations contribute substantially to a program’s execution time. We use an operational semantics of future, developed in a previous paper, to derive a program analysis algorithm and an optimization algorithm based on the analysis that removes provably-redundant touch operations. Experiments with the Gambit compiler indicate that this optimization significantly reduces the overhead imposed by touch operations.

∗Supported in part by NSF grant CCR 91-22518 and a sabbatical at Carnegie Mellon University.

Contents

1 Futures, Touches and Transparency 1 2 Review: The Language and Its Parallel Semantics 2 3 Touch Optimization 4

3.1 Non-touching Primitives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 The Touch Optimization Algorithm . . . . . . . . . . . . . . . . . . . . . . . 7

4 Set-Based Analysis for Futures 11 4.1 Deriving Set Constraints for Program Variables . . . . . . . . . . . . . . . . 11 4.2 Soundness of the Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . 15 4.3 From Set Constraints to Set-Based Analysis . . . . . . . . . . . . . . . . . . 19 4.4 Performing Set-Based Analysis . . . . . . . . . . . . . . . . . . . . . . . . . 20

5 Experimental Results 23 6 Related Work 25 7 Conclusion 26 A Correctness Proof for Representation 26 B Set Based Analysis Algorithm 31

1 Futures, Touches and Transparency

Programs in functional languages offer numerous opportunities for executing program components in parallel. In a call-by-value language, for example, the evaluation of every function application could spawn a parallel thread for each argument expression. However, if such a strategy were applied indiscriminately, the execution of a program would generate far too many parallel threads. The overhead of managing these threads would clearly outweigh any benefits from parallel execution.

The future annotations of MultiLisp and its Scheme successors [2, 11] provide a simple method for taming the implicit parallelism of functional programs. If a programmer believes that the parallel evaluation of some expression outweighs the overhead of creating a separate task, he may annotate the expression with the keyword future. An annotated functional program has the same observable behavior as the original program, but the run-time system may choose to evaluate the future expression in parallel to the rest of the program. If it does, the evaluation will proceed as if the annotated expression had immediately returned. Instead of a proper value though, it returns a placeholder, which contains enough information for retrieving the actual result of the annotated expression when needed. When a program operation requires specific knowledge about the value of some subcomputation but finds a placeholder, the run-time system performs a touch operation, which synchronizes the appropriate parallel threads, and eventually retrieves the necessary information.

The standard way of implementing touch operations on placeholders requires a modification of all program operations that need to know specific aspects of values. For example, procedure application must know that the value of the first sub-expression is a procedure; an if-expression demands a proper value in the test position, not only a placeholder; and, addition can only add its inputs if they are numbers. Hence, these operations must be modified so that they first check whether the appropriate arguments are placeholders or proper values and must possibly perform some synchronization.

Past research on futures has concentrated on the efficient implementation of the underlying task creation mechanism [6, 16, 22, 23, 24] and on the extension of the language with higher-order control constructs [18, 25]. Little effort has gone into the development of a semantic characterization of the idea or the use of such a semantic framework for the optimization of task creation or coordination. In contrast, the driving force behind our effort is the desire to develop semantically well-founded optimizations for the execution of futures. The specific example we choose to consider is the development of an algorithm that safely eliminates as many touch operations as possible. Other optimizations will be the subject of future efforts.

In a previous paper [8], we developed a series of semantics for an idealized functional language with future. The last semantics is particularly suited to the development of analysis and optimization algorithms, because it exposes appropriate details regarding program executions. Here we use that semantics to derive a program analysis algorithm, and a provably-correct touch optimization algorithm based on the analysis. An implementation of the optimization on the Gambit Scheme compiler [6] produced significant speedups on a standard set of benchmarks. We believe that this development can be extended to larger languages and other implementation techniques.

The presentation of our results proceeds as follows. The second section introduces a simple, functional language with futures, and recalls the low-level parallel abstract machine for the language [8]. The third section discusses the cost of touch operations and presents a provably correct algorithm for eliminating unnecessary touch operations. The latter is based on the set-based analysis algorithm of the fourth section. The fifth section describes the implementation of these algorithms on the Gambit compiler and compares the modified compiler to the original compiler on a standard set of benchmarks. The sixth section discusses related work. This technical report is an expansion of a preliminary conference report [9].

2 Review: The Language and Its Parallel Semantics

Given the goal of developing a semantics that is useful for proving the soundness of optimizations, we develop the definitional semantics for futures for an intermediate representation of an idealized functional language. Specifically, we use the subset of A-normal forms [10] of an extended λ-calculus-like language that includes conditionals and a future construct: see Figure 1.

M ∈ Λ_{a}  ::= x  (Terms)

| (let (x V) M)

| (let (x (future M)) M) | (let (x (car y)) M) | (let (x (cdr y)) M) | (let (x (if y M M)) M) | (let (x (apply y z)) M)

V ∈ Value ::= c | x | (λx. M) | (cons x y)  (Values)
x ∈ Vars =  {x, y, z, …}  (Variables)
c ∈ Const =  {nil, 0, 1, …}  (Constants)

Figure 1: The A-normalized Language Λ_{a}

In a previous paper [8], we developed a series of abstract machines, each specifying the semantics of futures at a different level of abstraction. The last of these machines, called the P (CEK)-machine, is particularly well-suited for the development of program analyses, since it contains explicit binding information relating program variables to their values. The machine is also will-suited for the development of a touch optimization algorithm, since it exposes the use of explicit placeholder objects and performs touch operations on these objects. We use this machine, defined in Figures 2 and 3, as the basis for the development of this paper.

Notation We use the following notations throughout the paper: P denotes the power-set constructor; f : A ⟶ B denotes that f is a total function from A to B; f : A ⟶_{f} B denotes that f is a finite map from A to B; M ∈ P denotes that the term M occurs in the

Well-Founded Touch Optimization for Futures 3

Evaluator:

eval_{pcek} : Λ_{a}^{0} ⟶ Answers ∪ {error, ⊥}
eval_{pcek}(P) = \{ \begin{matrix}unload_{pcek}[E(x)] & if ⟨P, ∅, ϵ⟩ ⟼_{pcek}^{∗} ⟨x, E, ϵ⟩ \\ error & if ⟨P, ∅, ϵ⟩ ⟼_{pcek}^{∗} error \\ ⊥ & if ∀i ∈ N ∃S_{i} ∈ State_{pcek}, n_{i}, m_{i} ∈ N such that \\ & m_{i} > 0, S_{0} = ⟨P, ∅, ϵ⟩ and S_{i} ⟼_{pcek}^{n_{i},m_{i}} S_{i+1} \end{matrix}

Data Specifications:

S ∈ State_{pcek} ::= ⟨M, E, K⟩ | error | (f-let (p S) S) (States)
M ∈ Λ_{a}  (A-nf Language)
E ∈ Env_{pcek}  ::= Vars ⟶_{f} Value_{pcek}  (Environments)
V ∈ Value_{pcek}  ::= PValue_{pcek} | Ph-Obj_{pcek}  (Run-Time Values)
PValue_{pcek}  ::= c | Cl_{pcek} | Pair_{pcek}  (Proper Values)
Cl_{pcek}  ::= ⟨(λx. M), E⟩  (Closures)
Pair_{pcek}  ::= (cons V V)  (Pairs)
Ph-Obj_{pcek}  ::= ⟨ph p ∘⟩ | ⟨ph p V ⟩  (Placeholder Values)
K ∈ Cont_{pcek}  ::= ϵ | ⟨ar x, M, E⟩.K | ⟨ar† x, M, E⟩.K  (Continuations)
F ∈ FinalState_{pcek} ::= ⟨x, E, ϵ⟩ | error  (Final States)

Auxiliary Functions:

unload_{pcek} : Value_{pcek}^{0} ⟶ Answers
unload_{pcek}[c] = c
unload_{pcek}[⟨(λx. M), E⟩] = procedure
unload_{pcek}[(cons V_{1} V_{2})] = (cons V′_{1} V′_{2})
where V′_{i} = unload_{pcek}[V_{i}]
unload_{pcek}[⟨ph p V ⟩] = unload_{pcek}[V]

touch_{pcek} : Value_{pcek} ⟶ PValue_{pcek} ∪ {∘}
touch_{pcek}[⟨ph p ∘⟩] = ∘
touch_{pcek}[⟨ph p V ⟩] = touch_{pcek}[V]
touch_{pcek}[V] = V if V ∈ PValue_{pcek}

Placeholder Substitution S[p := V], E[p := V], K[p := V]:

(f-let (p′ S_{1}) S_{2})[p := V] = \{ \begin{matrix}(f-let (p′ S_{1}[p := V]) S_{2}) & if p = p′ \\ (f-let (p′ S_{1}[p := V]) S_{2}[p := V]) & if p ≠ p′ \end{matrix}
⟨M, E, K⟩[p := V] = ⟨M, E[p := V], K[p := V]⟩

                 error[p := V] = error

E[p := V] = E′ such that E′(x) = \{ \begin{matrix}⟨ph p V ⟩ & if E(x) = ⟨ph p ∘⟩ \\ E(x) & otherwise \end{matrix}
ϵ[p := V] = ϵ
(⟨ar x, M, E⟩.K)[p := V] = ⟨ar x, M, E[p := V]⟩.K[p := V]
(⟨ar† x, M, E⟩.K)[p := V] = ⟨ar† x, M, E[p := V]⟩.K[p := V]

Figure 2: The P (CEK)-machine: Evaluator and Data Specifications

program P; and ⟨ar? x, M, E⟩ refers to either a normal activation record ⟨ar x, M, E⟩ or a tagged activation record ⟨ar† x, M, E⟩.

4 C. Flanagan, M. Felleisen

Transition Rules:

⟨(let (x c) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨M, E[x ← c], K⟩  (bind-const)
⟨(let (x y) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨M, E[x ← E(y)], K⟩  (bind-var)
⟨(let (x (λy. N)) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨M, E[x ← ⟨(λy. N), E′⟩], K⟩  (bind-lam)

where E′ = E|_{F V [(λy. N)]}

⟨(let (x (cons y z)) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨M, E[x ← (cons E(y) E(z))], K⟩  (bind-cons)
⟨x, E, ⟨ar y, M, E′⟩.K⟩ ⟼_{pcek}^{1,1} ⟨M, E′[y ← E(x)], K⟩  (return)
⟨(let (x (car y)) M), E, K⟩ ⟼_{pcek}^{1,1}
\{ \begin{matrix}⟨M, E[x ← V_{1}], K⟩ & if touch_{pcek}[E(y)] = (cons V_{1} V_{2}) \\ error & if touch_{pcek}[E(y)] ∉ Pair_{pcek} ∪ \{∘\} \end{matrix}  (car)
⟨(let (x (cdr y)) M), E, K⟩ ⟼_{pcek}^{1,1} analogous to car  (cdr)
⟨(let (x (if y M_{1} M_{2})) M), E, K⟩ ⟼_{pcek}^{1,1}
\{ \begin{matrix}⟨M_{1}, E, ⟨ar x, M, E⟩.K⟩ & if touch_{pcek}[E(y)] ∉ \{nil, ∘\} \\ ⟨M_{2}, E, ⟨ar x, M, E⟩.K⟩ & if touch_{pcek}[E(y)] = nil \end{matrix}  (if )
⟨(let (x (apply y z)) M), E, K⟩ ⟼_{pcek}^{1,1}
\{ \begin{matrix}⟨N, E′[x′ ← E(z)], ⟨ar x, M, E⟩.K⟩ & if touch_{pcek}[E(y)] = ⟨(λx′. N), E′⟩ \\ error & if touch_{pcek}[E(y)] ∉ Cl_{pcek} ∪ \{∘\} \end{matrix}  (apply)
⟨(let (x (future N)) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨N, E, ⟨ar† x, M, E⟩.K⟩  (future)
⟨x, E, ⟨ar† y, M, E′⟩.K⟩ ⟼_{pcek}^{1,1} ⟨M, E′[y ← E(x)], K⟩  (future-id)
⟨M, E, K_{1}.⟨ar† x, N, E′⟩.K_{2}⟩ ⟼_{pcek}^{1,0}
(f-let (p ⟨M, E, K_{1}⟩) ⟨N, E′[x ← ⟨ph p ∘⟩], K_{2}⟩) p ∉ F P (E′) ∪ F P (K_{2})  (fork)
(f-let (p ⟨x, E, ϵ⟩) S) ⟼_{pcek}^{1,1} S[p := E(x)]  (join)
(f-let (p error) S) ⟼_{pcek}^{1,1} error  (join-error)
(f-let (p_{2} (f-let (p_{1} S_{1}) S_{2})) S_{3}) ⟼_{pcek}^{1,1} (f-let (p_{1} S_{1}) (f-let (p_{2} S_{2}) S_{3}))  (lift)

p_{1} ∉ F P (S_{3})

(f-let (p S_{1}) S_{2}) ⟼_{pcek}^{a+c,b} (f-let (p S′_{1}) S′_{2})  (parallel)

if S_{1} ⟼_{pcek}^{a,b} S′_{1}, S_{2} ⟼_{pcek}^{c,d} S′_{2}

S ⟼_{pcek}^{0,0} S  (reflexive)
S ⟼_{pcek}^{a+c,b+d} S′′  (transitive)

if S ⟼_{pcek}^{a,b} S′, S′ ⟼_{pcek}^{c,d} S′′, a, c > 0

Figure 3: The P (CEK)-machine: Transition Rules

3 Touch Optimization

The P (CEK)-machine performs touch operations on arguments in placeholder-strict positions of all program operations. These implicit touch operations guarantee the transparency of placeholders, which makes future-based parallelism so convenient to use. Unfortunately, these compiler-inserted touch operations impose a significant overhead on the execution of annotated programs. For example, an annotated doubly-recursive version of fib (see Figure 4) performs 1.2 million touch operations during the computation of (fib 25).

(define fib

(lambda (n)

(if (< n 2)

1

(let ([r1 (future (fib (− n 1)))]) (let ([r2 (fib (− n 2))]) (+ r1 r2 ))))))

Figure 4: The definition of fib.

Due to the dynamic typing of Scheme, the cost of each touch operation depends on the program operation that invoked it. If a program operation already performs a type dispatch to ensure that its arguments have the appropriate type, e.g., car, cdr, apply, etc, then a touch operation is free. Put differently, an implementation of (car x) in pseudo-code is:

(if (pair? x) (unchecked-car x)

(error ’car "Not a pair"))

Extending the semantics of car to perform a touch operation on placeholders is simple:

(if (pair? x) (unchecked-car x)
(let ([y (touch x)]) (if (pair? y) (unchecked-car y)

(error ’car "Not a pair"))))

The touching version of car incurs an additional overhead only in the error case or when x is a placeholder. For the interesting case when x is a pair, no overhead is incurred. Since the vast majority of Scheme operations already perform a type-dispatch on their arguments,^{1} the overhead of performing implicit touch operations appears to be acceptable at first glance.

However, a standard technique for increasing execution speed in Scheme systems is to disable type-checking typically based on informal correctness arguments or based on type verifiers for the underlying sequential language [29, 1]. When type-checking is disabled, most program operations do not perform a type-dispatch on their arguments. Under these circumstances, the source code (car x) translates to the pseudo-code:

(unchecked-car x)

Extending the semantics of car to perform a touch operation on placeholders is now quite expensive, since it then performs an additional check for every execution:

(if (placeholder? x) (unchecked-car (touch x)) (unchecked-car x))

1Two notable exceptions are if, which does not perform a type-dispatch on the value of the test expression, and the equality predicate eq?, which is implemented as a pointer comparison.

Performing these placeholder? checks can add a significant overhead to the execution time. Kranz [21] and Feeley [6] estimated this cost at nearly 100% of the (sequential) execution time, and our experiments confirm these results (see below).

The classical solution for avoiding this overhead is to provide a compiler switch that disables the automatic insertion of touches, and a touch primitive so that programmers can insert touch operations explicitly where needed [6, 19, 27]. We believe that this solution is flawed for several reasons. First, it clearly destroys the transparent character of future annotations. Instead of an annotation that only affects executions on some machines, future is now a task creation construct and touch is a synchronization tool. Second, to use this solution safely, the programmer must know where placeholders can appear instead of regular values and must add touch operations at these places in the program. In contrast to the addition of future annotations, the placement of touch operations is far more difficult: while the former requires a prediction concerning computational intensity, the latter demands a full understanding of the data flow properties of the program. Since we believe that an accurate prediction of data flow by the programmer is only possible for small programs, we reject this traditional solution.

A better approach than explicit touches is for the compiler to use information provided by a data-flow analysis of the program to remove unnecessary touches wherever provably possible^{2}. This approach substantially reduces the overhead of touch operations without sacrificing the simplicity or transparency of future annotations.

3.1 Non-touching Primitives

The current language does not provide primitives that do not touch arguments in placeholderstrict positions. To express and verify an algorithm that replaces touching primitives by non-touching primitives, we extend the language Λ_{a} with non-touching forms of the placeholder-strict primitive operations, denoted \underline{car}, \underline{cdr}, \underline{if} and \underline{apply}, respectively:

M ::= …
| (let (x (\underline{car} y)) M)
| (let (x (\underline{cdr} y)) M)
| (let (x (\underline{if} y M M)) M)
| (let (x (\underline{apply} y z)) M)

As their name indicates, a non-touching operation behaves in the same manner as the original version as long as its argument in the placeholder-strict position is not a placeholder. If the argument is a place-holder, the behavior of the non-touching variant is unspecified, and any arbitrary state may be produced. The extended language is called \underline{Λ_{a}}.

We define the semantics of the extended language \underline{Λ_{a}} by extending the P (CEK)-machine with the additional transition rules described in Figure 5. The evaluator for the extended language, \underline{eval_{pcek}}, is defined in the usual way (cmp. Figures 2). Unlike eval_{pcek}, the evaluator \underline{eval_{pcek}} is no longer a function. There are programs in \underline{Λ_{a}} for which the evaluator

2This approach is similar in character to optimization techniques such as soft-typing [29, 1] and tagging optimization [14], which remove the type-dispatches required in dynamically-typed languages wherever possible. However, touch-optimization also applies to a statically-typed language with futures, where soft-typing and tagging optimization techniques are not as useful.

⟨(let (x (\underline{car} y)) M), E, K⟩  ⟼_{pcek}^{1,1}
\{ \begin{matrix}⟨M, E[x ← V_{1}], K⟩ & if E(y) = (cons V_{1} V_{2}) \\ unspecified & if E(y) ∈ Ph-Obj_{pcek} \\ error & otherwise \end{matrix}  (\underline{car})

⟨(let (x (\underline{cdr} y)) M), E, K⟩  ⟼_{pcek}^{1,1} analogous to \underline{car}  (\underline{cdr})
⟨(let (x (\underline{if} y M_{1} M_{2})) M), E, K⟩ ⟼_{pcek}^{1,1}
\{ \begin{matrix}⟨M_{2}, E, ⟨ar x, M, E⟩.K⟩ & if E(y) = nil \\ unspecified & if E(y) ∈ Ph-Obj_{pcek} \\ ⟨M_{1}, E, ⟨ar x, M, E⟩.K⟩ & otherwise \end{matrix}  (\underline{if})

⟨(let (x (\underline{apply} y z)) M), E, K⟩ ⟼_{pcek}^{1,1}
\{ \begin{matrix}⟨N, E′[x′ ← E(z)], ⟨ar x, M, E⟩.K⟩ & if E(y) = ⟨(λx′. N), E′⟩ \\ unspecified & if E(y) ∈ Ph-Obj_{pcek} \\ error & otherwise \end{matrix} (\underline{apply})

Figure 5: Non-touching transition rules

\underline{eval_{pcek}} can either return a value or can be unspecified because of the application of a nontouching operation to a placeholder. Still, the two evaluators clearly agree on programs in Λ_{a}.

Lemma 3.1 For P ∈ Λ_{a}, \underline{eval_{pcek}}(P) = eval_{pcek}(P).

3.2 The Touch Optimization Algorithm

The goal of touch optimization is to replace the touching operations car, cdr, if and apply by the corresponding non-touching operation whenever possible, without changing the semantics of programs. For example, suppose that a program contains (let (x (car y)) M) and we can prove that y is never bound to a placeholder. Then we can replace the expression with (let (x (\underline{car} y)) M), which the machine can execute without performing a test for placeholdership on y.

This optimization technique relies on a detailed data-flow analysis of the program that determines a conservative approximation to the set of run-time values for each variable. More specifically, we assume that the analysis returns a valid set environment, which is a table mapping program variables to a set of run-time values^{3} that subsumes the set of values associated with that variable during an execution.

Definition 3.2. (Set environments, E ⊧ E, S ⊧ E, P ⊧ E) Let P be a program and let Vars_{P} be the set of variables occurring in P.

• A mapping E : Vars_{P} → P(Value_{pcek}) is a set environment for P.

3Or a least a representation of this set that provides the appropriate information.

T_{E} : Λ_{a} ⟶ \underline{Λ_{a}}
T_{E}[x] = x
T_{E}[(let (x c) M)] = (let (x c) T_{E}[M])
T_{E}[(let (x y) M)] = (let (x y) T_{E}[M])
T_{E}[(let (x (λy. N)) M)] = (let (x (λy. T_{E}(N))) T_{E}[M])
T_{E}[(let (x (cons y z)) M)] = (let (x (cons y z)) T_{E}[M])
T_{E}[(let (x (future N)) M)] = (let (x (future T_{E}[N])) T_{E}[M])
T_{E}[(let (x (car y)) M)] = \{ \begin{matrix}(let (x (\underline{car} y)) T_{E}[M]) & if E(y) ⊆ PValue_{pcek} \\ (let (x (car y)) T_{E}[M]) & if E(y) ⊈ PValue_{pcek} \end{matrix}
T_{E}[(let (x (cdr y)) M)] = analogous to car
T_{E}[(let (x (if y M_{1} M_{2})) M)] = \{ \begin{matrix}(let (x (\underline{if} y M_{1} M_{2})) T_{E}[M]) & if E(y) ⊆ PValue_{pcek} \\ (let (x (if y M_{1} M_{2})) T_{E}[M]) & if E(y) ⊈ PValue_{pcek} \end{matrix}

T_{E}[(let (x (apply y z)) M)] = \{ \begin{matrix}(let (x (\underline{apply} y z)) T_{E}[M]) & if E(y) ⊆ PValue_{pcek} \\ (let (x (apply y z)) T_{E}[M]) & if E(y) ⊈ PValue_{pcek} \end{matrix}

Figure 6: The touch optimization algorithm T

• E ⊧ E (read E validates E) if for all x ∈ dom(E), E(x) ∈ E(x).

• The relation S ⊧ E (read S validates E) is defined inductively:

– ⟨M, E, K⟩ ⊧ E if E ⊧ E.

– (f-let (p S_{1}) S_{2}) ⊧ E if S_{1} ⊧ E and S_{2} ⊧ E.

• P ⊧ E (read P validates E) if for every state S such that ⟨P, ∅, ϵ⟩ ⟼_{pcek}^{∗} S, S ⊧ E.

The basic idea behind touch optimization is now easy to explain. If a valid set environment shows that the argument of a touching version of car, cdr, if or apply can never be a placeholder, the optimization algorithm replaces the operation with its non-touching version. The optimization algorithm T , parameterized over a set environment E, is defined in Figure 6. If E is valid for the program being optimized, then the touch optimization algorithm T_{E} preserves the meaning of that program. For every transition step of the source program P there exists a corresponding transition step for the optimized program T_{E}(P). We extend T_{E} in a natural manner to states to aid in the proof of this correspondence.

Lemma 3.3 (Step Correspondence) Let P be a program with a set environment E, and let S be a state for which E is valid.

1. Suppose S ⟼_{pcek}^{n,m} S′. Then T_{E}(S) ⟼_{pcek}^{n,m} T_{E}(S′).

2. Suppose T_{E}(S) ⟼_{pcek}^{n,m} S′′. Then S ⟼_{pcek}^{n,m} S′ where T_{E}(S′) = S′′.

Proof: We prove the first part by induction on n and by case analysis of S ⟼_{pcek}^{n,m} S′.

• We first consider the case where S ⟼_{pcek}^{1,1} S′ via the transition rule car. Then S = ⟨(let (x (car y)) M), E, K⟩. There are four sub-cases to consider, depending on whether or not E(y) contains placeholders and whether or not E(y) is a pair.

– Assume E(y) ⊈ PValue_{pcek} and touch_{pcek}[E(y)] = (cons V_{1} V_{2}). Then:

S′ = ⟨M, E[x ← V_{1}], K⟩
T_{E}(S) = ⟨(let (x (car y)) T_{E}(M)), T_{E}(E), T_{E}(K)⟩
touch_{pcek}[(T_{E}(E))(y)] = (cons T_{E}(V_{1}) T_{E}(V_{2}))
T_{E}(S′) = ⟨T_{E}(M), T_{E}(E[x′ ← V_{1}]), T_{E}(K)⟩

Hence T_{E}(S) ⟼_{pcek}^{1,1} T_{E}(S′) via the rule car.

– Assume E(y) ⊈ PValue_{pcek} and touch_{pcek}[E(y)] ∉ Pair_{pcek}∪{∘}. Then:

S′ = ⟨error, ∅, ϵ⟩
T_{E}(S) = ⟨(let (x (car y)) T_{E}(M)), T_{E}(E), T_{E}(K)⟩
touch_{pcek}[(T_{E}(E))(y)] ∉ Pair_{pcek} ∪ {∘}
T_{E}(S′) = ⟨error, ∅, ϵ⟩

Hence T_{E}(S) ⟼_{pcek}^{1,1} T_{E}(S′) via the rule car.

– Assume E(y) ⊆ PValue_{pcek} and touch_{pcek}[E(y)] = (cons V_{1} V_{2}). Then:

S′ = ⟨M, E[x ← V_{1}], K⟩
T_{E}(S) = ⟨(let (x (\underline{car} y)) T_{E}(M)), T_{E}(E), T_{E}(K)⟩
E(y) = (cons V_{1} V_{2})  since S ⊧ E
(T_{E}(E))(y) = (cons T_{E}(V_{1}) T_{E}(V_{2}))
T_{E}(S′) = ⟨T_{E}(M), T_{E}(E[x′ ← V_{1}]), T_{E}(K)⟩

Hence E(y) ⊆ PValue_{pcek} via the rule \underline{car}.

– Finally, if E(y) ⊆ PValue_{pcek} and touch_{pcek}[E(y)] ∉ Pair_{pcek} ∪ {∘}, then:

S′ = ⟨error, ∅, ϵ⟩
T_{E}(S) = ⟨(let (x (\underline{car} y)) T_{E}(M)), T_{E}(E), T_{E}(K)⟩
E(y) ∉ Pair_{pcek} ∪ {∘}  since S ⊧ E
(T_{E}(E))(y) ∉ Pair_{pcek} ∪ {∘}
T_{E}(S′) = ⟨error, ∅, ϵ⟩

Hence T_{E}(S) ⟼_{pcek}^{1,1} T_{E}(S′) via the rule \underline{car}.

Hence if S ⟼_{pcek}^{1,1} S′ via the rule car, then T_{E}(S) ⟼_{pcek}^{1,1} T_{E}(S′) via one of the rules car or \underline{car}.

• The other cases are similar.

The second part of the proof proceeds in a similar manner by induction on n and by case analysis of T_{E}(S) ⟼_{pcek}^{n,m} S′′.

• Consider the case where T_{E}(S) ⟼_{pcek}^{1,1} S′′ via the transition rule \underline{car}.

T_{E}(S) = ⟨(let (x (\underline{car} y)) T_{E}(M)), T_{E}(E), T_{E}(K)⟩
S = ⟨(let (x (car y)) M), E, K⟩ by the definition of T_{E}
E(y) ⊆ PValue_{pcek}
– Suppose that (T_{E}(E))(y) = (cons T_{E}(V_{1}) T_{E}(V_{2})). Then:

\begin{aligned}S′′ & = & ⟨T_{E}(M), T_{E}(E)[x ← T_{E}(V_{1})], T_{E}(K)⟩ \\ E(y) & = & (cons V_{1} V_{2}) \\ S′ & = & ⟨M, E[x ← V_{1}], K⟩ \end{aligned}

Hence S ⟼_{pcek}^{1,1} S′ via the rule car, and T_{E}(S′) = S′′.

– Alternatively suppose that (T_{E}(E))(y) ∉ Pair_{pcek}. Then:

touch_{pcek}[E(y)] ∉ Pair_{pcek} ∪ {∘}
S′′ = ⟨error, ∅, ϵ⟩
S′ = ⟨error, ∅, ϵ⟩

Hence S ⟼_{pcek}^{1,1} S′ via the rule car, and T_{E}(S′) = S′′.

• The other cases are similar.

The Step Correspondence Lemma implies that a touch optimized program exhibits the same behavior as the corresponding unoptimized program.

Main Lemma 3.4 For P ∈ Λ_{a}^{0}, if P ⊧ E then \underline{eval_{pcek}}(T_{E}(P)) = eval_{pcek}(P).

Proof: Both the fact that \underline{eval_{pcek}} is well-defined on T_{E}(P) and that the equality holds follow from Lemma 3.3.

In summary, the touch optimization algorithm we present removes redundant touch operations from programs based on the information provided by a valid set environment. This optimization algorithm is provably-correct with respect to the semantics of future as specified by the extended evaluator \underline{eval_{pcek}}. Any implementation that realizes \underline{eval_{pcek}} correctly can therefore make use of our optimization technique.

4 Set-Based Analysis for Futures

The development of a sound program analysis proceeds in two stages. First, we use the transition rules of the P (CEK)-machine to derive constraints on the sets of run-time values that variables in a given program may assume. Any set environment satisfying these constraints is a valid set environment. Second, we develop an algorithm for finding the minimal (i.e., most accurate) set environment satisfying these constraints. Our set constraints are similar to the constraints in Heintze’s work on set-based analysis for SML [13], but our derivation substantially differs from his.

4.1 Deriving Set Constraints for Program Variables

Given a program P, a set constraint is of the form:

\frac{A_{P}}{B}

where A_{P} and B are statements concerning set environments, and A_{P} also depends on the program. A set environment E satisfies this constraint if whenever A holds for E and P, then B also holds for E.

We derive constraints on E sufficient to ensure that each transition during the evaluation of P preserves the validity of E. Suppose the evaluation of P involves the transition S⟼_{pcek}^{n,m} S′. Then we require that the constraints on E imply that if S ⊧ E then S′ ⊧ E. We proceed by case analysis on the last transition rule used for S⟼_{pcek}^{n,m}S′ and present six representative cases:

1. Suppose S ⟼_{pcek}^{1,1} S′ via the transition rule (bind-const):

⟨(let (x c) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨M, E[x ← c], K⟩

The transition pairs x with the constant c in the extended environment. To ensure that the set E(x) includes c, only need to ensure that for each term of the form (let (x c) M) occurring in P, the constant c must be recorded in E as one of the possible values of the variable x. This suggests the constraint:

\frac{(let (x c) M) ∈ P}{c ∈ E(x)}  (C_{1}^{P})

2. Suppose S⟼_{pcek}^{1,1}S′ via the transition rule (apply). In the interesting case, y is bound, either directly or via a placeholder object, to a closure ⟨(λx′. N), E′⟩, which implies that:

⟨(let (x (apply y z)) M), E, K⟩ ⟼_{pcek}^{1,1} ⟨N, E′[x′ ← E(z)], ⟨ar x, M, E⟩.K⟩

A transition according to this rule binds x′ to the value E(z). To ensure that the set E(x′) includes the value E(z), we demand that E(x′) satisfy the constraint:

\frac{(let (x (apply y z)) M) ∈ P  V_{y} ∈ E(y) touch_{pcek}[V_{y}] = ⟨(λx′. N), E⟩  V ∈ E(z)}{V ∈ E(x′)}  (C_{7}^{P})

3. Suppose S ⟼_{pcek}^{1,1} S′ via the transition rule (return):

⟨x, E′, ⟨ar y, M, E⟩.K⟩ ⟼_{pcek}^{1,1} ⟨M, E[y ← E′(x)], K⟩

To account for transitions according to (return), our constraint system must ensure that E(y) includes the value E′(x). However, a syntax-directed program analysis cannot extract the possible activation records that may receive the value of the final variable in a procedure from the variable or its immediate context. Instead, it can determine all potential call sites of the procedure and can enforce a relationship between the “return” variable of the procedure and the variable that receives the result of the function call. Thus, if FinalVar[ N ] is a function that determines the innermost (“result”) variable of N, then the crucial constraint on this variable is as follows:

(let (x (apply y z)) M) ∈ P V_{y} ∈ E(y)
touch_{pcek}[V_{y}] = ⟨(λx′. N), E⟩ V ∈ E(FinalVar[ N ])

V ∈ E(x) (C_{8}^{P})

The definition of FinalVar is straightforward.

Definition 4.1. (FinalVar)

FinalVar : Λ_{a} ⟶ Vars
FinalVar[ x] = x
FinalVar[ (let (x V) M) ] = FinalVar[ M ]
FinalVar[ (let (x (future N)) M) ] = FinalVar[ M ]
FinalVar[ (let (x (car y)) M) ] = FinalVar[ M ]
FinalVar[ (let (x (cdr y)) M) ] = FinalVar[ M ]
FinalVar[ (let (x (if y M_{1} M_{2})) M) ] = FinalVar[ M ]
FinalVar[ (let (x (apply y z)) M) ] = FinalVar[ M ]

4. Suppose S ⟼_{pcek}^{1,1} S′ via the transition rule (future-id):

⟨x, E, ⟨ar† y, M, E′⟩.K⟩ ⟼_{pcek}^{1,1} ⟨M, E′[y ← E(x)], K⟩

A transition according to this rule returns the current value of x to a tagged activation record. As with the previous case, our analysis cannot extract the possible tagged activation records that may receive the value of x from the variable or its immediate context. Instead, by examining each future-expression (let (x (future N)) M), the analysis determines which variable x may receive the value of FinalVar[ N ] via a (future-id) transition. The following constraint then ensures that E accounts for these bindings:

\frac{(let (x (future N)) M) ∈ P  V ∈ E(FinalVar[ N ])}{V ∈ E(x)}  (C_{10}^{P})

\frac{(let (x c) M) ∈ P}{c ∈ E(x)}  (C_{1}^{P})
\frac{(let (x y) M) ∈ P  V ∈ E(y)}{V ∈ E(x)}  (C_{2}^{P})
\frac{(let (x (λy. N)) M) ∈ P dom(E) = F V [(λy. N)] ∀x ∈ dom(E). E(x) ∈ E(x)}{⟨(λy. N), E⟩ ∈ E(x)}  (C_{3}^{P})
\frac{(let (x (cons y_{1} y_{2})) M) ∈ P  V_{1} ∈ E(y_{1})  V_{2} ∈ E(y_{2})}{(cons V_{1} V_{2}) ∈ E(x)}  (C_{4}^{P})
\frac{(let (x (car y)) M) ∈ P  V_{y} ∈ E(y)  touch_{pcek}[V_{y}] = (cons V_{1} V_{2})}{V_{1} ∈ E(x)}  (C_{5}^{P})
\frac{(let (x (cdr y)) M) ∈ P  V_{y} ∈ E(y)  touch_{pcek}[V_{y}] = (cons V_{1} V_{2})}{V_{2} ∈ E(x)}  (C_{6}^{P})

\frac{(let (x (apply y z)) M) ∈ P  V_{y} ∈ E(y) touch_{pcek}[V_{y}] = ⟨(λx′. N), E⟩  V ∈ E(z)}{V ∈ E(x′)}  (C_{7}^{P})

(let (x (apply y z)) M) ∈ P V_{y} ∈ E(y) touch_{pcek}[V_{y}] = ⟨(λx′. N), E⟩ V ∈ E(FinalVar[ N ])

V ∈ E(x) (C_{8}^{P})

\frac{(let (x (if y M_{1} M_{2})) M) ∈ P  V ∈ E(FinalVar[ M_{1} ]) ∪ E(FinalVar[ M_{2} ])}{V ∈ E(x)}  (C_{9}^{P})
\frac{(let (x (future N)) M) ∈ P  V ∈ E(FinalVar[ N ])}{V ∈ E(x)}  (C_{10}^{P})
\frac{(let (x (future N)) M) ∈ P}{⟨ph p ∘⟩ ∈ E(x)}  (C_{11}^{P})
\frac{(let (x (future N)) M) ∈ P  V ∈ E(FinalVar[ N ])}{⟨ph p V ⟩ ∈ E(x)}  (C_{12}^{P})

Figure 7: Set Constraints on E with respect to P.

5. Suppose S ⟼_{pcek}^{1,0} S′ via the transition rule (fork):

⟨M, E, K_{1}.⟨ar† x, N, E′⟩.K_{2}⟩⟼_{pcek}^{1,0}(f-let (p ⟨M, E, K_{1}⟩) ⟨N, E′[x ← ⟨ph p ∘⟩], K_{2}⟩)
p ∉ F P (E′) ∪ F P (K_{2})

Transitions according to this rule return an undetermined placeholder ⟨ph p ∘⟩ to the continuation ⟨ar† x, N, E′⟩.K_{2} of a future expression. To ensure that \overline{E} accounts for bindings created by such transitions, we impose a second constraint on futureexpressions:

\frac{(let (x (future N)) M) ∈ P}{⟨ph p ∘⟩ ∈ E(x)}  (C_{11}^{P})

6. A transition according to the rule (join) replaces each occurrence of an undetermined placeholder with a determined placeholder containing the result of the appropriate future expression:

(f-let (p ⟨x, E, ϵ⟩) S) ⟼_{pcek}^{1,1} S[p := E(x)]

As with cases 3 and 4, our analysis cannot determine the possible placeholders that may receive the value of a variable x from the variable or its immediate context. Instead, to account for the environment bindings that are modified by (join) transitions, we introduce a third constraint on future expressions:

\frac{(let (x (future N)) M) ∈ P  V ∈ E(FinalVar[ N ])}{⟨ph p V ⟩ ∈ E(x)}  (C_{12}^{P})

Examining each of the transition rules of the machine in a similar manner results in twelve program-based set constraints C_{1}^{P} , …, C_{12}^{P}: see Figure 7.

Set Constraints for a Sample Program To illustrate how the set constraints determine valid set environments, consider the following program cons-it. The program defines a function cons-it that returns a cons-cell containing two copies of it’s argument, and the program then applies this function to the numbers 1 and 2, producing results pair_{1} and pair_{2} respectively.

(let (cons-it

(lambda x . (let (r (cons x x)) r))) (let (t_{1} 1)

(let (pair_{1} (cons-it t_{1}))

(let (t_{2} 2)

(let (pair_{2} (cons-it t_{2}))

pair_{2})))))

Instantiating the set constraints for this program produces the following constraints:

From C_{3}^{P}:  ⟨(λx. (let (r (cons x x)) r)), ∅⟩ ∈ E(cons-it)  (1)
From C_{4}^{P}:  \frac{V_{1} ∈ E(x)  V_{2} ∈ E(x)}{(cons V_{1} V_{2}) ∈ E(r)}  (2)
From C_{1}^{P}:  1 ∈ E(t_{1})  (3)
From C_{7}^{P}:  \frac{⟨(λx′. N), E⟩ ∈ E(cons-it)  V ∈ E(t_{1})}{V ∈ E(x′)}  (4)
From C_{8}^{P}:  \frac{⟨(λx′. N), E⟩ ∈ E(cons-it)  V ∈ E(FinalVar[ N ])}{V ∈ E(pair_{1})}  (5)
From C_{1}^{P}:  2 ∈ E(t_{2})  (6)
From C_{7}^{P}:  \frac{⟨(λx′. N), E⟩ ∈ E(cons-it)  V ∈ E(t_{2})}{V ∈ E(x′)}  (7)
From C_{8}^{P}:  \frac{⟨(λx′. N), E⟩ ∈ E(cons-it)  V ∈ E(FinalVar[ N ])}{V ∈ E(pair_{2})}  (8)

We can solve these constraints by starting with an empty set environment E and repeatedly extending E as required by the constraints until all the constraints are satisfied, as follows:

From (1) :  ⟨(λx. (let (r (cons x x)) r)), ∅⟩ ∈ E(cons-it)  (9)
From (3) :  1 ∈ E(t_{1})  (10)
From (4), (9), (10) :  1 ∈ E(x)  (11)
From (2), (11) :  (cons 1 1) ∈ E(r)  (12)
From (5), (9), (12) :  (cons 1 1) ∈ E(pair_{1})  (13)
From (6) :  2 ∈ E(t_{2})  (14)
From (9), (7), (14) :  2 ∈ E(x)  (15)
From (2), (15) :  (cons 2 2) ∈ E(r)  (16)
From (2), (11), (15) :  (cons 1 2) ∈ E(r)  (17)
From (2), (11), (15) :  (cons 2 1) ∈ E(r)  (18)
From (5), (9), (16) :  (cons 2 2) ∈ E(pair_{1})  (19)
From (5), (9), (17) :  (cons 1 2) ∈ E(pair_{1})  (20)
From (5), (9), (18) :  (cons 2 1) ∈ E(pair_{1})  (21)
From (8), (9), (12) :  (cons 1 1) ∈ E(pair_{2})  (22)
From (8), (9), (16) :  (cons 2 2) ∈ E(pair_{2})  (23)
From (8), (9), (17) :  (cons 1 2) ∈ E(pair_{2})  (24)
From (8), (9), (18) :  (cons 2 1) ∈ E(pair_{2})  (25)

At this stage E is the set environment:

E(cons-it) = {⟨(λx. (let (r (cons x x)) r)), ∅⟩}
E(x) = {1, 2}
E(t_{1}) = {1}
E(t_{2}) = {2}
E(r) = E(pair_{1}) = E(pair_{2}) = {(cons 1 1), (cons 2 2), (cons 1 2), (cons 2 1)}

A quick examination of the set constraints shows that this set environment satisfies the constraints for the program cons-it. Furthermore, since each binding in E is required by the set constraints, E is the smallest set environment satisfying the set constraints. Of course, E is not the smallest valid set environment. For example, E(pair_{1}) contains the value (cons 2 2), even though that value would never be associated with pair_{1} during an execution.

4.2 Soundness of the Set Constraints

Proving the soundness of the set constraints requires showing that if a set environment E satisfies the set constraints for a given program P, then E must be valid for P.

Assume that E satisfies C_{1}^{P} , …, C_{12}^{P}. To prove that P ⊧ E, we need to show that ⟨P, ∅, ϵ⟩ ⟼_{pcek}^{n,m} S implies S ⊧ E. The natural approach is to proceed by induction on n. As part of the proof, we will need to consider intermediate transitions starting from states other than ⟨P, ∅, ϵ⟩. Therefore, we need to strengthen the induction hypothesis to:

S ⊧_{P} E and S ⟼_{pcek}^{n,m} S′ implies S′ ⊧_{P} E

where the invariant S ⊧_{P} E is an appropriately chosen relation. This invariant relation needs to assert a number of properties about the state S in order to support the proof of the induction hypothesis:

• First, the invariant relation needs to assert that the terms contained in S must occur in P, i.e., the evaluation of programs does not involve the creation of new terms.

• Next, the invariant relation needs to assert that S can only contain values and environments that are compatible with P and E. A run-time value V is compatible with P and E, written V ⊧_{P} E, if each syntactic term occurring in the run-time value V also occurs in P and each environment in V is compatible with P and E. Similarly, an environment E is compatible with P and E, written E ⊧_{P} E, if each binding in E occurs in E and each value in E is compatible with P and E.

Definition 4.2. (V ⊧_{P} E, E ⊧_{P} E)

– The relation V ⊧_{P} E is the smallest relation satisfying the following clauses:

c ⊧_{P} E if c occurs in P
x ⊧_{P} E if x occurs in P
⟨(λx. M), E⟩ ⊧_{P} E if (λx. M) ∈ P, dom(E) = F V [(λx. M)] and E ⊧_{P} E
(cons V_{1} V_{2}) ⊧_{P} E if V_{1} ⊧_{P} E and V_{2} ⊧_{P} E
⟨ph p ∘⟩ ⊧_{P} E
⟨ph p V ⟩ ⊧_{P} E if V ⊧_{P} E

– E ⊧_{P} E holds if for all x ∈ dom(E), E(x) ∈ E(x) and E(x) ⊧_{P} E.

• The invariant relation must also assert that E already contains the bindings that could be created during a subsequent (return) or (future-id) transition to an existing activation record. This requirement is necessary to support the induction hypothesis in the case of a (return) or (future-id) transition, and is specified in Definition 4.4 below by the clause:

if K = ⟨ar? x_{1}, M_{1}, E_{1}⟩. · · · .⟨ar? x_{n}, M_{n}, E_{n}⟩
then …
and E(final-var(M_{i})) ⊆ E(x_{i+1}) for 1 ≤ i < n
and E(final-var(M)) ⊆ E(x_{1}) if n > 0

• Similarly, the invariant relation must assert that E already contains the bindings that could be created during a subsequent (fork) or (join) transition. This requirement is specified in Definition 4.4 below by the clause for f-let states and by the clause:

if K = K_{1}.⟨ar† x, M, E⟩.K_{2}
then ∀p ∈ Ph-Vars, ⟨ph p ∘⟩ ∈ E(x)
and ∀V ∈ E(ResultVar[ ⟨M, E, K_{1}⟩]), ⟨ph p V ⟩ ∈ E(x)

The auxiliary function ResultVar[ S] returns determines the variable whose value will be returned as the result of S.

Definition 4.3. (ResultVar)

ResultVar : State_{pcek} ⟶ Vars
ResultVar[ ⟨M, E, ϵ⟩] = FinalVar[ M ]
ResultVar[ ⟨M, E, K.⟨ar? x, N, E′⟩⟩] = FinalVar[ N ]
ResultVar[ (f-let (p S_{1}) S_{2}) ] = ResultVar[ S_{2} ]

• Finally, to allow for error transitions, the invariant relation must hold for the error state error.

The complete invariant relation, which asserts all of the above properties about S, P and E, is defined by induction on the size of states.

Definition 4.4. (S ⊧_{P} E)

(f-let (p S_{1}) S_{2}) ⊧_{P} E ⇔ \{ \begin{matrix}S_{1} ⊧_{P} E, S_{2} ⊧_{P} E \\ and ∀V ∈ E(ResultVar[ S_{1} ]), S_{2}[p := V] ⊧_{P} E \end{matrix}

⟨M, E, K⟩ ⊧_{P} E ⇔ \{ \begin{matrix}M ∈ P, E ⊧_{P} E \\ and if K = ⟨ar? x_{1}, M_{1}, E_{1}⟩. · · · .⟨ar? x_{n}, M_{n}, E_{n}⟩ \\ then x_{i} ∈ P, M_{i} ∈ P, E_{i} ⊧_{P} E for 1 ≤ i ≤ n \\ and E(final-var(M_{i})) ⊆ E(x_{i+1}) for 1 ≤ i < n \\ and E(final-var(M)) ⊆ E(x_{1}) if n > 0 \\ and if K = K_{1}.⟨ar† x, M, E⟩.K_{2} \\ then ∀p ∈ Ph-Vars, ⟨ph p ∘⟩ ∈ E(x) \\ and ∀V ∈ E(ResultVar[ ⟨M, E, K_{1}⟩]), ⟨ph p V ⟩ ∈ E(x) \end{matrix}

         error ⊧_{P} E

The invariant relation is a stronger relation than the plain “validates” relation, i.e., if a state satisfies the invariant relation for a set environment with respect to a given program, then that state obviously validates the set environment.

Lemma 4.5 S ⊧_{P} E implies S ⊧ E

Proof: By induction on the structure of S.

Our chosen invariant relation supports the proof of the induction hypothesis: if the invariant holds for a given state S, then the invariant also holds for the successors of S.

Lemma 4.6 Suppose E satisfies C_{1}^{P} , …, C_{12}^{P}. Then S ⊧_{P} E and S ⟼_{pcek}^{n,m} S′ implies S′ ⊧_{P} E.

Proof: By induction on n and by case analysis of the last transition rule for S ⟼_{pcek}^{n,m} S′. We present the cases for the transition rules (bind-const), (apply) and (return) in detail.

• Suppose S ⟼_{pcek}^{1,1} S′ via the transition rule (bind-const). Then:

\begin{aligned}S & = & ⟨(let (x c) M), E, K⟩ \\ S′ & = & ⟨M, E[x ← c], K⟩ \end{aligned}

Since S ⊧_{P} E, we know that (let (x c) M) ∈ P, E ⊧_{P} E and the conditions on K in the definition of the invariant are satisfied. Also, E satisfies C_{1}^{P} implies that c ∈ E(x). By definition, c ⊧_{P} E. Therefore E[x ← c] ⊧_{P} E, which implies S′ ⊧_{P} E.

• Suppose S ⟼_{pcek}^{1,1} S′ via the transition rule (apply). Then:

S = ⟨(let (x (apply y z)) M), E, K⟩

Since the analysis of the error case is trivial, we only consider the case where y is bound, either directly or via a placeholder object, to a closure ⟨(λx′. N), E′⟩. In this case:

\begin{aligned}touch_{pcek}[E(y)] & = & ⟨(λx′. N), E′⟩ \\ S′ & = & ⟨N, E′[x′ ← E(z)], ⟨ar x, M, E⟩.K⟩ \end{aligned}

Obviously N ∈ P. To show that the new environment E′[x′ ← E(z)] is compatible with P and E, we proceed as follows: From S ⊧_{P} E we know that E ⊧_{P} E. But E ⊧_{P} E implies that E(y) ⊧_{P} E, which in turn implies E′ ⊧_{P} E. Also, E ⊧_{P} E shows that E(z) ∈ E(z), which, since E satisfies C_{7}^{P}, implies that E(z) ∈ E(x′). Finally, E ⊧_{P} E implies that E(z) ⊧_{P} E. Combining the facts E′ ⊧_{P} E, E(z) ∈ E(x′), and E(z) ⊧_{P} E yields E′[x′ ← E(z)] ⊧_{P} E, i.e., the new environment is compatible with P and E. Finally, we must show that the appropriate conditions on the new continuation ⟨ar x, M, E⟩.K hold. That E(FinalVar[ N ]) ⊆ E(x) follows from C_{8}^{P}, and the remaining conditions on the continuation are implied by the relation S ⊧_{P} E. Therefore, the invariant holds for S′.

• The final case we consider is for the transition rule (return). For this case:

\begin{aligned}S & = & ⟨x, E′, ⟨ar y, M, E⟩.K⟩ \\ S′ & = & ⟨M, E[y ← E′(x)], K⟩ \end{aligned}

That M ∈ P follows from the relation S ⊧_{P} E. To show that the new environment E[y ← E′(x)] is compatible with P and E we proceed as follows: From S ⊧_{P} E we know that E′ ⊧_{P} E, and hence E′(x) ⊧_{P} E. The invariant also implies that E(x) ⊆ E(y), which in turn implies that E′(x) ∈ E(y). Finally, the invariant implies that E ⊧_{P} E. Combining the facts E′(x) ⊧_{P} E, E′(x) ∈ E(y), and E ⊧_{P} E shows that E[y ← E′(x)] ⊧_{P} E, i.e., the new environment is compatible with P and E. The required conditions on K follow from the relation S ⊧_{P} E. Therefore, the invariant holds for S′.

The remaining cases have similar proofs.

Since the invariant trivially holds for the initial state ⟨P, ∅, ϵ⟩, it follows that the set constraints are sound, i.e., if E satisfies the set constraints relative to P, then E is a valid set environment for P.

Main Lemma 4.7 (Soundness of Constraints) If E satisfies C_{1}^{P} , …, C_{12}^{P}, then P ⊧ E.

Proof: Suppose E satisfies C_{1}^{P} , …, C_{12}^{P}. Let S be a state such that ⟨P, ∅, ϵ⟩⟼_{pcek}^{n,m} S. By the definition of the invariant relation, ⟨P, ∅, ϵ⟩ ⊧_{P} E. Therefore Lemma 4.6 implies that S ⊧_{P} E, and hence by Lemma 4.5, S ⊧ E. The latter is true for any state derivable from the initial state ⟨P, ∅, ϵ⟩, hence P ⊧ E.

In summary, any set environment satisfying the set constraints with respect to a program P is a conservative approximation to the set of bindings created during the execution of P.

4.3 From Set Constraints to Set-Based Analysis

The class of set environments for a given program P, denoted SetEnv_{P}, forms a complete lattice under the natural pointwise partial ordering ⊑ defined by:

E_{1} ⊑ E_{2} if and only if ∀x ∈ Vars_{P} . E_{1}(x) ⊆ E_{2}(x)

The least set environment ⊥_{E} in the lattice is the trivial mapping such that ⊥_{E}(x) = ∅. Each approximation constraint C_{i}^{P} can be interpreted as a function, also denoted by C_{i}^{P}, on this lattice. Since the presence of each binding in C_{i}^{P} (E) depends only on the presence of a finite number of bindings in E, it follows that the functions C_{i}^{P} are both monotonic and continuous. We define the function C_{P} to be the lub of the functions C_{1}^{P} , …, C_{12}^{P}:

C_{P} : SetEnv_{P} ⟶ SetEnv_{P}
C_{P} (E) = C_{1}^{P} (E) ⊔ ⋯ ⊔ C_{12}^{P}(E)

Since the combined function C_{P} is also monotonic and continuous, the least fixpoint given by ⨆_{n∈N} C_{P}^{n}(⊥_{E}) exists. We define set-based analysis as the function that returns this least fixpoint.

Definition 4.8. (sba) The function sba : Λ_{a} ⟶ SetEnv_{P} is given by:

sba(P) = ⨆_{n∈N} C_{P}^{n}(⊥_{E})

Since the fixpoints of C_{P} are exactly the solutions to the set constraints C_{1}^{P} , …, C_{12}^{P}, it follows that sba(P) is the least solution to the set constraints, and hence that sba(P) is a valid set environment for P.

Main Lemma 4.9 (Correctness of sba) P ⊧ sba(P)

Combining this lemma with the previous Lemma 3.4 proves that the touch optimization algorithm, parameterized over the results of set-based analysis, always preserves the meaning of programs.

Theorem 4.10 (Correctness of Touch Optimization) For P ∈ Λ_{a},

\underline{eval_{pcek}}(T_{sba(P)}(P)) = eval_{pcek}(P).

This theorem shows that our touch optimizing transformation is provably-correct with respect to the semantics of programs as specified by the evaluators eval_{pcek} and \underline{eval_{pcek}}.

4.4 Performing Set-Based Analysis

Since sba(P) typically maps variables to infinite sets of possible values, we need a finite representation for these infinite sets. To derive such a finite representation, we simply remove the redundant information contained in these infinite sets. To illustrate this idea, consider the source program expression:

(let (x (cons y_{1} y_{2})) M)

According to C_{4}^{P}, sba(P)(x) must contain at least all the cons-cells (cons V_{1} V_{2}) such that V_{1} ∈ sba(P)(y_{1}) and V_{2} ∈ sba(P)(y_{2}). A more compact representation for the same information would be to use the program term (cons y_{1} y_{2}) to represent the set {(cons V_{1} V_{2}) | V_{1} ∈ sba(P)(y_{1}), V_{2} ∈ sba(P)(y_{2})}. The possible values of x can then be reconstructed from (cons y_{1} y_{2}) and from the possible values for the variables y_{1} and y_{2}.

In a similar manner, we can use the λ-expression (λx. M) to represent all closures of the form ⟨(λx. M), E⟩, since the possible environments in the closure can easily be reconstructed from the set environment. A systematic inspection of the set constraints produces the following set of representation values for a program P:

W ∈ RepValue_{P} ::= c_{P} | (λx. M)_{P} | (cons x y)_{P} | ⟨ph x_{P} ⟩ | ⟨ph ∘⟩

where the constant c_{P}, the λ-expression (λx. M)_{P}, the pair (cons x y)_{P} and the variable x_{P} are all the respective subterms of P. The size of RepValue_{P} is O(|P |), where |P | is the length of P.

Representation values provide a finite representation for the infinite set environments encountered in set-based analysis. Specifically, a representation environment \overline{E} is a mapping from variables in P to finite sets of representation values. Each representation value W ∈ \overline{E}(x) represents a set of run-time values V (depending on \overline{E}) according to the relation V in\overline{E} W. In a similar manner, each set \overline{E}(x) of representation values represents a set of run-time values according to the relation V in\overline{E} x:

c in\overline{E} c
⟨(λx. M), E⟩ in\overline{E} (λx. M)  ⇔ \{ \begin{matrix}dom(E) = F V [(λx. M)] \\ and ∀y ∈ dom(E). E(y) in\overline{E} y \end{matrix}
(cons V_{1} V_{2}) in\overline{E} (cons y_{1} y_{2}) ⇔ V_{1} in\overline{E} y_{1}, V_{2} in\overline{E} y_{2}
⟨ph p V ⟩ in\overline{E} ⟨ph y⟩  ⇔ V in\overline{E} y
⟨ph p ∘⟩ in\overline{E} ⟨ph ∘⟩
V in\overline{E} x  ⇔ ∃W ∈ \overline{E}(x) with V in\overline{E} W

\frac{(let (x c) M) ∈ P}{c ∈ \overline{E}(x)}  (\overline{C_{1}^{P}})
\frac{(let (x y) M) ∈ P  W ∈ \overline{E}(y)}{W ∈ \overline{E}(x)}  (\overline{C_{2}^{P}})
\frac{(let (x (λy. N)) M) ∈ P  ∀z ∈ F V [(λy. N)]. \overline{E}(z) ≠ ∅}{(λy. N) ∈ \overline{E}(x)}  (\overline{C_{3}^{P}})
\frac{(let (x (cons y_{1} y_{2})) M) ∈ P  \overline{E}(y_{1}) ≠ ∅  \overline{E}(y_{2}) ≠ ∅}{(cons y_{1} y_{2}) ∈ \overline{E}(x)}  (\overline{C_{4}^{P}})
\frac{(let (x (car y)) M) ∈ P  W_{y} ∈ \overline{E}(y)  (cons z_{1} z_{2}) ∈ \overline{touch}[\overline{E}, W_{y} ]  W ∈ \overline{E}(z_{1})}{W ∈ \overline{E}(x)} (\overline{C_{5}^{P}})
\frac{(let (x (cdr y)) M) ∈ P  W_{y} ∈ \overline{E}(y)  (cons z_{1} z_{2}) ∈ \overline{touch}[\overline{E}, W_{y} ]  W ∈ \overline{E}(z_{2})}{W ∈ \overline{E}(x)} (\overline{C_{6}^{P}})

\frac{(let (x (apply y z)) M) ∈ P  W_{y} ∈ \overline{E}(y) (λx′. N) ∈ \overline{touch}[\overline{E}, W_{y} ]  W ∈ \overline{E}(z)}{W ∈ \overline{E}(x′)}  (\overline{C_{7}^{P}})

(let (x (apply y z)) M) ∈ P W_{y} ∈ \overline{E}(y) (λx′. N) ∈ \overline{touch}[\overline{E}, W_{y} ] W ∈ \overline{E}(FinalVar[ N ])

W ∈ \overline{E}(x) (\overline{C_{8}^{P}})

\frac{(let (x (if y M_{1} M_{2})) M) ∈ P  W ∈ \overline{E}(FinalVar[ M_{1} ]) ∪ \overline{E}(FinalVar[ M_{2} ])}{W ∈ \overline{E}(x)}  (\overline{C_{9}^{P}})
\frac{(let (x (future N)) M) ∈ P  W ∈ \overline{E}(FinalVar[ N ])}{W ∈ \overline{E}(x)}  (\overline{C_{10}^{P}})
\frac{(let (x (future N)) M) ∈ P}{⟨ph ∘⟩ ∈ \overline{E}(x)}  (\overline{C_{11}^{P}})
\frac{(let (x (future N)) M) ∈ P  \overline{E}(FinalVar[ N ]) ≠ ∅}{⟨ph FinalVar[ N ]⟩ ∈ \overline{E}(x)}  (\overline{C_{12}^{P}})

Auxiliary Function:

\overline{touch} : RepEnv_{P} × RepValue_{P} ⟶ P(RepValue_{P})

\overline{touch}[\overline{E}, W ] = \{ \begin{matrix}\{W \}  if W = c or W = (λx. M) or W = (cons x y) \\ \{\overline{W} | \overline{U} ∈ \overline{E}(y) and \overline{W} ∈ \overline{touch}[\overline{E}, \overline{U} ]\}  if W = ⟨ph y⟩ \end{matrix}

Figure 8: Representation Constraints on \overline{E} with respect to P.

The class of all representation environments for a program P is denoted RepEnv_{P}. Each representation environment \overline{E} is a finite representation of a potentially infinite set environment, according to the following function:

F : RepEnv_{P} ⟶ SetEnv_{P}
F (\overline{E}) (x) = \{V | V in\overline{E} x\}

Reformulating the set constraints from Figure 7 for representation environments produces the representation constraints \overline{C_{1}^{P}} , …, \overline{C_{12}^{P}} on \overline{E} with respect to P: see Figure 8. As before, we can interpret each constraint as a monotonic and continuous function on the lattice of representation environments. We define \overline{sba}(P) to be the least fixpoint of the lub of these functions.

Definition 4.11. (\overline{sba}) The function \overline{sba} : Λ_{a} ⟶ RepEnv_{P} is given by:

\overline{sba}(P) = ⨆_{n∈N} \overline{C_{P}} ^{n}(⊥_{E})

where the function \overline{C_{P}} : RepEnv_{P} ⟶ RepEnv_{P} denotes the lub of the representation constraints interpreted as functions, i.e.,

\overline{C_{P}} (E) = \overline{C_{1}^{P}} (E) ⊔ ⋯ ⊔ \overline{C_{12}^{P}}(E).

The correspondence between set constraints and representation constraints implies that \overline{sba}(P) is a finite representation for sba(P). In particular, our change of representation does not introduce any extra notion of approximation.

Theorem 4.12 (Correctness of Representation) sba(P) = F(\overline{sba}(P))

Proof: See Appendix A.

Since the set of representation values is finite, we can calculate \overline{sba}(P) in an iterative manner. Appendix B contains an O(|P |^{3}) time algorithm that performs this calculation.

Optimization algorithms can interpret the representation environment \overline{sba}(P) in a straightforward manner. For example, the query on sba(P) from the touch optimization algorithm:

sba(P)(y) ⊆ PValue_{pcek}

is equivalent to the following query on \overline{sba}(P):

\overline{sba}(P)(y) ⊆ \{c, (λx. M), (cons x y)\}

In a similar manner other queries on sba(P) can easily be reformulated in terms of \overline{sba}(P).

Representation Constraints for a Sample Program In Section 4.1, we derived a set environment E satisfying the set constraints with respect to the program cons-it. We now illustrate how to calculate \overline{sba}(cons-it).

Instantiating the representation constraints with respect to the program produces the following constraints:

From \overline{C_{3}^{P}}:  (λx. (let (r (cons x x)) r)) ∈ \overline{E}(cons-it)  (1)
From \overline{C_{4}^{P}}:  (cons x x) ∈ \overline{E}(r)  (2)
From \overline{C_{1}^{P}}:  1 ∈ \overline{E}(t_{1})  (3)
From \overline{C_{7}^{P}}:  \frac{(λx′. N) ∈ \overline{E}(cons-it)  W ∈ \overline{E}(t_{1})}{W ∈ \overline{E}(x′)}  (4)
From \overline{C_{8}^{P}}:  \frac{(λx′. N) ∈ \overline{E}(cons-it)  W ∈ \overline{E}(FinalVar[ N ])}{W ∈ \overline{E}(pair_{1})}  (5)
From \overline{C_{1}^{P}}:  2 ∈ \overline{E}(t_{2})  (6)
From \overline{C_{7}^{P}}:  \frac{(λx′. N) ∈ \overline{E}(cons-it)  W ∈ \overline{E}(t_{2})}{W ∈ \overline{E}(x′)}  (7)
From \overline{C_{8}^{P}}:  \frac{(λx′. N) ∈ \overline{E}(cons-it)  W ∈ \overline{E}(FinalVar[ N ])}{W ∈ \overline{E}(pair_{2})}  (8)

We solve these constraints by repeatedly extending \overline{E} until all the constraints are satisfied, as follows:

From (1) :  (λx. (let (r (cons x x)) r)) ∈ \overline{E}(cons-it)  (9)
From (2) :  (cons x x) ∈ \overline{E}(r)  (10)
From (3) :  1 ∈ \overline{E}(t_{1})  (11)
From (4), (9), (11) :  1 ∈ \overline{E}(x)  (11)
From (5), (9), (10) :  (cons x x) ∈ \overline{E}(pair_{1})  (12)
From (6) :  2 ∈ \overline{E}(t_{2})  (13)
From (7), (9), (13) :  2 ∈ \overline{E}(x)  (15)
From (8), (9), (11) :  (cons x x) ∈ \overline{E}(pair_{1})  (16)

At this stage we have the representation environment given by:

\overline{E}(cons-it) = \{(λx. (let (r (cons x x)) r))\}
\overline{E}(x) = \{1, 2\}
\overline{E}(t_{1}) = \{1\}
\overline{E}(t_{2}) = \{2\}
\overline{E}(r) = \overline{E}(pair_{1}) = \overline{E}(pair_{2}) = \{(cons x x)\}

This representation environment satisfies the representation constraints with respect to the program cons-it. A quick examination verifies that F (\overline{E}) is the set environment E we derived previously for the program.

5 Experimental Results

We extended the Gambit compiler [6, 7], which makes no attempt to remove touch operations from programs, with a preprocessor that implements the set-based analysis algorithm and the touch optimization algorithm. The analysis and the optimization algorithm are

24 C. Flanagan, M. Felleisen

Program  Description
fib  Computes the 25^{th} fibonacci number using a doubly-recursive algorithm.
queens  Computes the number of solutions to the n-queens problem, for n = 10.
rantree Traverses a binary tree with 32768 nodes.
mm  Multiplies two 50 by 50 matrices of integers.
scan  Computes the parallel prefix sum of a vector of 32768 integers.
sum  Uses a divide-and-conquer algorithm to sum a vector of 32768 integers.
tridiag Solves a tridiagonal system of 32767 equations.
allpairs Parallel Floyd’s algorithm, finds shortest path between all pairs in a 117 node graph.
abisort Sorts 16384 integers using the adaptive bitonic sort algorithm.
mst  Computes the minimum spanning tree of a 1000 node graph.
qsort  Uses a parallel Quicksort algorithm to sort 1000 integers.
poly  Computes the square of a 200 term polynomial, and evaluates the result.

Figure 9: Description of the Benchmark Programs

standard compiler  touch optimized compiler
Benchmark  touch operations  touch operations  performance increase
Program  (n = 1)  (n = 1)  over standard (%)
count(K) overhead(%) count(K) overhead(%)  n = 1  n = 4 n = 16
fib  1214  85.0  122  10.2  68  66  58
queens  2116  41.2  35  1.5  39  44  39
rantree  327  67.5  14  2.6  63  59  37
mm  1828  121.0  3  <1  121  79  31
scan  1278  126.8  66  4.1  118  77  23
sum  525  107.3  33  6.1  95  61  25
tridiag  811  110.8  7  <1  109  42  6
allpairs  32360  150.4  14  <1  150  66  <1
abisort  5751  106.5  9  <1  105  45  32
mst  20422  91.4  750  5.3  82  21  <1
qsort  253  43.3  78  19.9  20  <1  <1
poly  526  65.3  121  16.2  42  14  <1

Figure 10: Benchmark Results

as described in the previous sections extended to a sufficiently large subset of functional Scheme.^{4} We used the extended Gambit compiler to test the effectiveness of touch optimization on the suite of benchmarks contained in Feeley’s Ph.D. thesis [6] on a GP1000 shared-memory multiprocessor [3]. Figure 9 describes these benchmarks.

4Five of the benchmarks include a small number (one or two per benchmark) of explicit touch operations for coordinating side-effects. They do not affect the validity of the analysis and touch optimization algorithms.

Each benchmark was tested on the original compiler (standard) and on the modified compiler (touch optimized). The results of the test runs are documented in Figure 10. The first two columns present the number of touch operations performed during the execution of a benchmark using the standard compiler (column 1), and the sequential execution overhead of these touch operations (column 2). To determine the absolute overhead of touch, we also ran the programs on a single processor after removing all touch operations. The next two columns contain the corresponding measurements for the touch optimizing compiler. The touch optimization algorithm reduces the number of touch operations to a small fraction of the original number (column 3), thus reducing the average overhead of touch operations from approximately 90% to less than 10% (column 4).

The last three columns show the relative speedup of each benchmark for one, four, and 16 processor configurations, respectively. The number compares the running time of the benchmarks using the standard compiler with the optimizing compiler. As expected, the relative speedup decreases as the number of processors increases, because the execution time is then dominated by other factors, such as memory contention and communication costs. For most benchmarks, the benefit of our touch optimization is still substantial, producing an average speedup over the standard compiler of 37% on four processors, and of 20% on 16 processors. The exceptions are the last three benchmarks, mst, qsort, and poly. However, even Feeley [6] described these as “poorly parallel” programs, in which the effects of memory contention and communication costs are especially visible. It is therefore not surprising that our optimizing compiler does not improve the running time in these cases.

6 Related Work

Kranz et al. [15, 22] briefly describe a simplistic algorithm for touch optimization based on a first-order type analysis. The algorithm lowers the touch overhead to 65% from 100% in standard benchmarks, that is, it is significantly less effective than our touch optimization. The paper does not address the semantics of future or the well-foundedness of the optimizations. Knopp [20] reports the existence of a touch optimization algorithm based on abstract interpretation. His paper presents neither a semantics nor the abstract interpretation. He only reports the reduction of static counts of touch operations for an implementation of Common Lisp with future. Neither paper gives an indication concerning the expense of the analysis algorithms.^{5}

At LFP’94, Jaganathan and Weeks [17] described an analysis for explicitly parallel symbolic programs, which they intend to use in a forthcoming compiler. They remark that the analysis could be used for touch optimizations. Their semantics and their derivation of the analysis significantly differ from ours so that we have not been able to compare the two analyses in detail.

Much work has been done on the static analysis of sequential programs, including abstract interpretation [4] and 0CFA [26]. Our analysis most closely follows Heintze’s work on set-based analysis for the sequential language ML [12], but the extension of this technique to parallel languages requires a substantial reformulation of the derivation and correctness proof. Specifically, Heintze uses the “natural” semantics framework to define a set-based “natural” semantics, from which he reads off “safeness” conditions on set environments. He then presents set constraints whose solution is the minimal safe set environment. We start from an parallel abstract machine and avoid Heintze’s intermediate steps by deriving our set constraints and proving their correctness directly from the abstract machine semantics.

5Ito’s group [Ito: personal communication, April 22, 1994] reports an attempt at touch optimization based on abstract interpretation. His group abandoned the effort due to the exponential cost of the abstract interpretation algorithm.

Other techniques for static analysis of sequential programs include abstract interpretation [4, 5] and Shivers’ 0CFA [26]. The relationship between abstract interpretation and set-based analysis was covered by Heintze [12].

Sequential optimization techniques such as tagging optimization [14] and soft-typing [29, 1] are similar in character to touch optimization. Both techniques remove the type-dispatches required for dynamic type-checking wherever possible, without changing the behavior of programs, in the same fashion as we remove touch operations. However, the analyses relys on conventional type inference techniques, whereas ours exploits the Scheme view of types as sets directly.

7 Conclusion

The development of a semantics for futures directly leads to the derivation of a powerful program analysis. The analysis is computationally inexpensive but yields enough information to eliminate numerous implicit touch operations. We believe that the construction of this simple touch optimization algorithm clearly illustrates how semantics can contribute to the development of advanced compilers. We intend to use our semantic characterization for the derivation of other program optimizations in Gambit and for the design of truly transparent future annotations for languages with imperative constructs.

Acknowledgments We thank Marc Feeley for discussions concerning touch optimizations and for his assistance in testing the effectiveness of our algorithm, and Nevin Heintze for discussions on set-based analysis and for access to his implementation of set based analysis for ML.

A Correctness Proof for Representation

We use in_{P} as shorthand for in_{\overline{sba}(P)}. The following theorem shows that \overline{sba}(P) produces a representation of sba(P).

Theorem 4.12 (Correctness of Representation) F (\overline{sba}(P)) = sba(P)

Proof: We show the equivalence of sba(P) and F (\overline{sba}(P)) by proving the set inclusion in both directions. Let x be a variable in Vars. Then:

V ∈ F (\overline{sba}(P)) (x)
implies V in_{P} x  by definition of F
implies V ∈ sba(P)(x)  by Lemma A.1

Also:

V ∈ sba(P)(x)
implies ∃W ∈ \overline{sba}(P)(x) with V in_{P} W  by Lemma A.5
implies V in_{P} x
implies V ∈ F (\overline{sba}(P)) (x)  by definition of F

Hence F (\overline{sba}(P)) = sba(P).

Lemma A.1 (\overline{sba} includes sba) V in_{P} x implies V ∈ sba(P)(x).

Proof: Assume that V in_{P} x (by a formal derivation). Then for some representation value W, V in_{P} W and W ∈ \overline{sba}(P)(x). We proceed by induction on the length of the derivation that V in_{P} x, and by case analysis on the last representation constraint used in the sub-derivation proving W ∈ \overline{sba}(P)(x):

\overline{C_{1}^{P}}: Then W = c, V = c and (let (x c) M) occurs in P. Hence by C_{1}^{P} we have V ∈ sba(P)(x).

\overline{C_{2}^{P}}: Then (let (x y) M) occurs in P. Also, since W ∈ \overline{sba}(P)(y) via a subderivation, by induction we have V ∈ sba(P)(y). Constraint C_{2}^{P} then shows that V ∈ sba(P)(x).

\overline{C_{3}^{P}}: Then (let (x (λy. N)) M) occurs in P, W = (λy. N) and V = ⟨(λy. N), E⟩, with dom(E) = F V [(λx. M)]. The derivation for V in_{P} W includes, for each z ∈ dom(E), a sub-derivation showing that E(z) in_{P} z. Therefore by induction we have that for each z ∈ dom(E), E(z) ∈ sba(P)(z). Using constraint C_{3}^{P} then shows that V ∈ sba(P)(x).

\overline{C_{4}^{P}}: Then (let (x (cons y_{1} y_{2})) M) occurs in P, W = (cons y_{1} y_{2}) and V = (cons V_{1} V_{2}). Since the derivation for V in_{P} W includes sub-derivations showing that V_{i} in_{P} y_{i}, by induction we have that V_{i} ∈ sba(P)(y_{i}). Using constraint C_{4}^{P} then shows that V ∈ sba(P)(x).

\overline{C_{5}^{P}}: We first consider the case where W_{y} is not a representation placeholder, i.e., where W_{y} = (cons z_{1} z_{2}). Then (let (x (car y)) M) occurs in P, (cons z_{1} z_{2}) ∈ \overline{sba}(P)(y), and W ∈ \overline{sba}(P)(z_{1}). Since V in_{P} W, by induction V ∈ sba(P)(z_{1}). By Lemma A.2, there exists V′ such that V′ in_{P} (cons z_{1} z_{2}) via a derivation of the same or smaller length than the derivation that (cons z_{1} z_{2}) ∈ \overline{sba}(P)(y). Because V′ in_{P} (cons z_{1} z_{2}), V′ must be of the form (cons V_{1} V_{2}). Hence V_{2} in_{P} z_{2} via a shorter derivation, and therefore by induction V_{2} ∈ sba(P)(z_{2}). Given that V ∈ sba(P)(z_{1}) and V_{2} ∈ sba(P)(z_{2}), Lemma A.3 proves that (cons V V_{2}) ∈ sba(P)(y). Using constraint C_{5}^{P} gives V ∈ sba(P)(x). The case where W_{y} is a representation placeholder follows by a similar argument.

\overline{C_{6}^{P}}: The analysis for the constraint \overline{C_{6}^{P}} is similar to the previous case.

\overline{C_{7}^{P}}: Suppose W ∈ \overline{sba}(P)(x′) via constraint \overline{C_{7}^{P}}. Again, we first deal with the case where W_{y} is not a representation placeholder, i.e., where W_{y} = (λx′. N). Then (let (x (apply y z)) M) occurs in P and (λx′. N) ∈ \overline{sba}(P)(y) via a sub-derivation. By Lemma A.4, there exists an environment E′ such that ⟨(λx′. N), E′⟩ ∈ sba(P)(y). Also, W ∈ \overline{sba}(P)(z) via a sub-derivation, so by induction we have that V ∈ sba(P)(z). An application of C_{7}^{P} proves that V ∈ sba(P)(x′). The case where W_{y} is a representation placeholder follows by a similar argument.

\overline{C_{8}^{P}}: The analysis for the constraint \overline{C_{8}^{P}} is similar to the previous case.

\overline{C_{9}^{P}} , \overline{C_{10}^{P}}: The analysis for the constraints \overline{C_{9}^{P}} and \overline{C_{10}^{P}} is similar to the analysis for \overline{C_{2}^{P}}.

\overline{C_{11}^{P}}: The analysis for the constraint \overline{C_{11}^{P}} is trivial.

\overline{C_{12}^{P}}: Then (let (x (future N)) M) occurs in P, W = ⟨ph FinalVar[ N ]⟩ and V = ⟨ph p V_{N}⟩. Since the derivation for V in_{P} W includes a subderivation showing that V_{N} in_{P} FinalVar[ N ], by induction we have that V_{N} ∈ sba(P)(FinalVar[ N ]). Using constraint C_{12}^{P} then shows that V ∈ sba(P)(x).

Lemma A.2 (Non-emptiness of representation values) If W ∈ \overline{sba}(P)(x) via a derivation of length n, then there exists some V such that V in_{P} W via a derivation of length ≤ n.

Proof: The proof is by induction on the length of the derivation that W ∈ \overline{sba}(P)(x). We proceed by case analysis on the last constraint used in the derivation:

\overline{C_{1}^{P}}: Then W = c, and c in_{P} W.

\overline{C_{2}^{P}}: Then W ∈ \overline{sba}(P)(y) via a sub-derivation, and the lemma holds by induction.

\overline{C_{3}^{P}}: Then W = (λy. M) and hence ⟨(λy. M), ∅⟩ in_{P} W.

\overline{C_{4}^{P}}: Then W = (cons y_{1} y_{2}), and W_{i} ∈ \overline{sba}(P)(y_{i}), for some V_{i}, i = 1, 2, via sub-derivations. Therefore by induction, there exists V_{i} in_{P} W_{i}, and hence (cons V_{1} V_{2}) in_{P} W.

• The analysis of the constraints \overline{C_{5}^{P}}, \overline{C_{6}^{P}}, \overline{C_{7}^{P}}, \overline{C_{8}^{P}}, \overline{C_{9}^{P}} and \overline{C_{10}^{P}} is similar to the analysis for \overline{C_{2}^{P}}.

\overline{C_{11}^{P}}: The analysis of the constraint \overline{C_{11}^{P}} is similar to the analysis for \overline{C_{1}^{P}}.

\overline{C_{12}^{P}}: Then W = ⟨ph FinalVar[ N ]⟩ ∈ \overline{sba}(P)(x), W_{N} ∈ \overline{sba}(P)(FinalVar[ N ]) via a sub-derivation, so by induction there exists V in_{P} W_{N}. Hence we have that ⟨ph p V ⟩ in\overline{E} ⟨ph FinalVar[ N ]⟩.

Lemma A.3 If V_{1} ∈ sba(P)(z_{1}), V_{2} ∈ sba(P)(z_{2}) and (cons z_{1} z_{2}) ∈ \overline{sba}(P)(x) then (cons V_{1} V_{2}) ∈ sba(P)(x).

Proof: The proof is by induction on the length of the derivation that (cons z_{1} z_{2}) ∈ \overline{sba}(P)(x). We proceed by case analysis on the last constraint used in the derivation:

\overline{C_{2}^{P}}: Suppose (cons z_{1} z_{2}) ∈ \overline{sba}(P)(x) via constraint \overline{C_{2}^{P}}. Then (cons z_{1} z_{2}) ∈ \overline{sba}(P)(y) via a sub-derivation, hence (cons V_{1} V_{2}) ∈ sba(P)(y) by induction, and therefore (cons V_{1} V_{2}) ∈ sba(P)(x) via C_{2}^{P}.

\overline{C_{4}^{P}}: Suppose (cons z_{1} z_{2}) ∈ \overline{sba}(P)(x) via constraint \overline{C_{4}^{P}}. Then (cons V_{1} V_{2}) ∈ sba(P)(x) via C_{4}^{P}.

• The cases for the constraints \overline{C_{5}^{P}}, \overline{C_{6}^{P}}, \overline{C_{7}^{P}}, \overline{C_{8}^{P}}, \overline{C_{9}^{P}} and \overline{C_{10}^{P}} follow by similar reasoning to the case for \overline{C_{2}^{P}}.

• The last constraint in the derivation of (cons z_{1} z_{2}) ∈ \overline{sba}(P)(x) cannot be one of \overline{C_{1}^{P}}, \overline{C_{3}^{P}}, \overline{C_{11}^{P}} or \overline{C_{12}^{P}}.

Lemma A.4 If (λx′. N) ∈ \overline{sba}(P)(x) then there exists some environment E′ such that ⟨(λx′. N), E′⟩ ∈ sba(P)(x).

Proof: The proof is by induction on the length of the derivation that (λx′. N) ∈ \overline{sba}(P)(x). We proceed by case analysis on the last constraint used in the derivation:

\overline{C_{2}^{P}}: Suppose (λx′. N) ∈ \overline{sba}(P)(x) via constraint \overline{C_{2}^{P}}. Then (λx′. N) ∈ \overline{sba}(P)(y) via a sub-derivation, hence ⟨(λx′. N), E′⟩ ∈ sba(P)(y) by induction, and therefore ⟨(λx′. N), E′⟩ ∈ sba(P)(x) via C_{2}^{P}.

\overline{C_{3}^{P}}: Suppose (λx′. N) ∈ \overline{sba}(P)(x) via constraint \overline{C_{3}^{P}}. Let the free variables of (λx′. N) be called z_{1}, …, z_{n}. For each z_{i} there exists W_{i} ∈ \overline{sba}(P)(z_{i}). Hence by Lemma A.2, there exists V_{i} ∈ sba(P)(z_{i}). Let E′ be the environment ⟨z_{1} ↦ V_{1}, …, z_{n} ↦ V_{n}⟩, and we have by C_{3}^{P} that ⟨(λx′. N), E′⟩ ∈ sba(P)(x).

• The cases for the constraints \overline{C_{5}^{P}}, \overline{C_{6}^{P}}, \overline{C_{7}^{P}}, \overline{C_{8}^{P}}, \overline{C_{9}^{P}} and \overline{C_{10}^{P}} follow by similar reasoning to the case for \overline{C_{2}^{P}}.

• The last constraint in the derivation of (λx′. N) ∈ \overline{sba}(P)(x) cannot be one of \overline{C_{1}^{P}}, \overline{C_{4}^{P}}, \overline{C_{11}^{P}} or \overline{C_{12}^{P}}.

Lemma A.5 (sba includes \overline{sba}:) V ∈ sba(P)(x) implies there exists W ∈ \overline{sba}(P)(x) with V in_{P} W.

Proof: Assume that V ∈ sba(P)(x). Then there exists a derivation that proves that V ∈ sba(P)(x). We proceed by induction on the length of this derivation, and by case analysis on the last step set constraint used in the derivation:

C_{1}^{P}: We take W = c, and the lemma holds. C_{2}^{P}: For this case V ∈ sba(P)(y) via a sub-derivation, so by induction there

exists W ∈ \overline{sba}(P)(y) with V in_{P} W. Then \overline{C_{2}^{P}} implies that W ∈ \overline{sba}(P)(x). C_{3}^{P}: In this case, V = ⟨(λy. N), E⟩, where dom(E) ⊆ F V [(λx. M)], and for each

z_{i} ∈ dom(E) we have E(z_{i}) ∈ sba(P)(z_{i}) via sub-derivations. Therefore, there exist W_{i} such that W_{i} ∈ \overline{sba}(P)(z_{i}) and E(z_{i}) in_{P} W_{i}. Now take W = (λy. N), then V in_{P} W and by \overline{C_{3}^{P}}, W ∈ \overline{sba}(P)(x).

C_{4}^{P}: In this case, V = (cons V_{1} V_{2}), and V_{i} ∈ sba(P)(y_{i}) via sub-derivations. Therefore, there exist W_{i} ∈ \overline{sba}(P)(y_{i}) with V_{i} in_{P} W_{i}. Now take W = (cons y_{1} y_{2}), then by \overline{C_{4}^{P}} we have that W ∈ \overline{sba}(P)(x).

C_{5}^{P}: Suppose V_{1} ∈ sba(P)(x) via constraint C_{5}^{P}. For simplicity, we consider only the case where V_{y} is not a placeholder, since the case involving placeholder is similar but more complicated. Thus V_{y} = (cons V_{1} V_{2}) ∈ sba(P)(y) via a sub-derivation. By induction there exists W_{y} such that W_{y} ∈ \overline{sba}(P)(y) and V_{y} in_{P} W_{y}. Hence W_{y} = (cons z_{1} z_{2}), W_{1} ∈ \overline{sba}(P)(z_{1}) and V_{1} in_{P} W_{1}. From \overline{C_{5}^{P}} we can prove W_{1} ∈ \overline{sba}(P)(x), and the lemma holds for this case.

C_{6}^{P}: This case is analogous to the previous case. C_{7}^{P}: Suppose V ∈ sba(P)(x′) via constraint C_{7}^{P}. For simplicity, we consider only

the case where V_{y} is not a placeholder, since the case involving placeholder is similar but more complicated. Thus V_{y} = ⟨(λx′. N), E⟩ ∈ sba(P)(y) via a sub-derivation. By induction there exists W_{y} such that W_{y} ∈ \overline{sba}(P)(y) and V_{y} in_{P} W_{y}. Hence W = (λx′. N). Also, V ∈ sba(P)(z) via a sub-derivation, so by induction there exists W such that W ∈ \overline{sba}(P)(y) and V in_{P} W. Hence, by \overline{C_{7}^{P}} we have W ∈ \overline{sba}(P)(x′).

C_{8}^{P}: Again, we consider only the case where V is not a placeholder. Thus V_{y} = ⟨(λx′. N), E⟩, and V_{y} ∈ sba(P)(y) via a sub-derivation. By induction there exists W_{y} such that W_{y} ∈ \overline{sba}(P)(y) and V_{y} in_{P} W_{y}. Hence W_{y} = (λx′. N). Also, V ∈ sba(P)(FinalVar[ N ]) via a sub-derivation, so by induction there exists W such that W ∈ \overline{sba}(P)(FinalVar[ N ]) and V in_{P} W. Hence, by \overline{C_{8}^{P}} we have W ∈ \overline{sba}(P)(x).

C_{9}^{P} , C_{10}^{P}: The analysis for the constraints C_{9}^{P} and C_{10}^{P} is similar to the analysis for C_{2}^{P}.

C_{12}^{P}: In this case V = ⟨ph p V_{N}⟩ ∈ sba(P)(x) via C_{12}^{P}, V_{N} ∈ sba(P)(FinalVar[ N ])

via a sub-derivation, so by induction there exists W_{N} ∈ \overline{sba}(P)(FinalVar[ N ]) with V_{N} in_{P} W_{N}. By \overline{C_{12}^{P}} we have that ⟨ph FinalVar[ N ]⟩ ∈ \overline{sba}(P)(x), and ⟨ph p V_{N}⟩ in_{P} ⟨ph FinalVar[ N ]⟩.

C_{11}^{P}: This case is trivial.

B Set Based Analysis Algorithm

A complete O(|P |^{3}) time set-based analysis algorithm^{6} for the intermediate language Λ_{a} is included in Figures 11 through 13. The algorithm is written in Scheme extended with a special form match for pattern matching [28].

The function SBA traverses an expression to derive the representation constraints for that expression. Certain representation constraints cannot be satisfied immediately. For example, the constraint \overline{C_{2}^{P}} requires that all representation values in \overline{E}(y) must be in \overline{E}(x), but the algorithm may not yet know all the representation values that may be added to \overline{E}(y). Therefore, the function SBA associate a constraint ‘(propagate-to ,x) with the variable y. This constraint then gets applied (via the function interpret-constraint) to each representation value that is added to \overline{E}(y), and propagates that representation value to \overline{E}(x).

The functions new-repvalue! and new-constraint! associate representation values and constraints, respectively, with variables. To ensure that the constraints are satisfied, the function interpret-constraint is called for each constraint and representation value associated with a given variable. This function ensures that the constraint is satisfied, by creating new representation values or new constraints as necessary.

The O(|P |^{3}) time bound can be verified as follows: We assume that the functions in-\overline{E}?, add-to-\overline{E}!, in-C? and add-to-C! operate in constant time, and that the functions foreach-in-\overline{E} and foreach-in-C operate in time linear in the number of elements in the appropriate set.

Each call of the functions new-absvalue! and new-constraint! takes constant time, excluding the time spent in the body of the respective unless expressions. The number of variables, the number of representation values, and the number of constraints are all O(|P |). Therefore the test conditions of the two unless expressions succeed at most O(|P |^{2}) times

6For clarity of presentation, the algorithm implements simpler versions of the representation constraints \overline{C_{3}^{P}}, \overline{C_{4}^{P}} and \overline{C_{12}^{P}} that do not include that non-emptyness conditions. We believe the extra degree of approximation introduced by this simplification is minor, and extending the algorithm to include these conditions is not difficult.

;; inputs: a Λ_{a} term M
;; outputs: calculates FinalVar[ M ]
;; effects: derives the representation constraints for M,
;;  and invokes a constraint solver on these constraints

(define SBA

(lambda (M )

(match M [(? variable? x) x] [‘(let (,x ,exp) ,body) (begin

(match exp [(? constant? c) (new-repvalue! x c)] [(? variable? y) (new-constraint! y ‘(propagate-to ,x))] [‘(cons ,y1 ,y2 ) (new-repvalue! x ‘(cons ,y1 ,y2 ))] [‘(lambda ,y ,N ) (let ([finalvar-N (SBA N )])

(new-repvalue! x ‘(lambda ,y ,N ,finalvar-N )))] [‘(future ,N ) (let ([finalvar-N (SBA N )])

(new-constraint! finalvar-N ‘(propagate-to ,x))

(new-repvalue! x ‘(ph ,finalvar-N ))

(new-repvalue! x ’(ph-circ)))] [‘(car ,y) (new-constraint! y ‘(propagate-car-to ,x))] [‘(cdr ,y) (new-constraint! y ‘(propagate-cdr-to ,x))] [‘(if ,y ,M1 ,M2 ) (let ([finalvar-M1 (SBA M1 )][finalvar-M2 (SBA M2 )])

(new-constraint! finalvar-M1 ‘(propagate-to ,x))

(new-constraint! finalvar-M2 ‘(propagate-to ,x)))] [‘(apply ,y ,z) (new-constraint! y ‘(application ,x ,z))])

(SBA body)]))))

Figure 11: The Set-Based Analysis Algorithm

each. Hence the body of each unless expression is executed at most O(|P |^{2}) times, and function interpret-constraint is called at most O(|P |^{3}) times. Each call of interpret-constraint terminates in constant time. Therefore, the entire algorithm takes O(|P |^{3}) time.

References

[1] Aiken, A., and Wimmers, E. L. Soft typing with conditional types. In POPL (1994), pp. 163–173.

[2] Baker, H., and Hewitt, C. The incremental garbage collection of processes. In Proceedings of the Symposium on Artificial Intelligence and Programming Languages (1977), vol. 12(8) of SIGPLAN Notices, pp. 55–59.

;; inputs: a variable and a representation value
;; outputs: void
;; effects: adds the value to \overline{E}(var), and applies the appropriate constraints to that value

(define new-repvalue!

(lambda (var repvalue)

(unless (in-\overline{E}? var repvalue) (add-to-\overline{E}! var repvalue) (foreach-in-C var (lambda (constraint) (interpret-constraint constraint repvalue))))))

;; inputs: a variable and a constraint
;; outputs: void
;; effects: associates the constraint with var, and applies the constraint to all values in \overline{E}(var)

(define new-constraint!

(lambda (var constraint)

(unless (in-C? var constraint) (add-to-C! var constraint) (foreach-in-\overline{E} var (lambda (repvalue) (interpret-constraint constraint repvalue))))))

;; inputs: a constraint and a representation value
;; outputs: void
;; effects: ensures that the constraint is satisfied, given that the constraint
;;  and the representation value are associated with the same variable

(define interpret-constraint

(lambda (constraint repvalue)

(match (cons constraint repvalue) [‘((propagate-to ,x) . ,v) (new-repvalue! x v)] [‘((propagate-car-to ,x) . (cons ,y1 ,y2 )) (new-constraint! y1 ‘(propagate-to ,x))] [‘((propagate-cdr-to ,x) . (cons ,y1 ,y2 )) (new-constraint! y2 ‘(propagate-to ,x))] [‘((application ,result ,arg) . (lambda ,para , ,finalvar)) (new-constraint! finalvar ‘(propagate-to ,result)) (new-constraint! arg ‘(propagate-to ,para))] [ (void)])))

Figure 12: The Set-Based Analysis Algorithm: Auxiliary Functions 1

[3] BBN Advanced Computers, Inc., Cambridge, MA. Inside the GP1000. 1989.

[4] Cousot, P., and Cousot, R. Abstract interpretation: A unified lattice model for static analyses of programs by construction or approximation of fixpoints. In POPL (1977), pp. 238–252.

[5] Cousot, P., and Cousot, R. Higer order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). ICCL (1994), 95–112.

[6] Feeley, M. An Efficient and General Implementation of Futures on Large Scale Shared-Memory Multiprocessors. PhD thesis, Department of Computer Science, Brandeis University, 1993.

;; The following three functions maintain a mapping \overline{E} from program ;; variables to sets of representation values

;; inputs: a variable and a representation value
;; outputs: returns true if \overline{E}(var) contains the representation value
;; effects: none

(define in-\overline{E}? (lambda (var repvalue) …))

;; inputs: a variable and a representation value
;; outputs: void
;; effects: adds repvalue to \overline{E}(var)

(define add-to-\overline{E}! (lambda (var repvalue) …))

;; inputs: a variable and a function
;; outputs: none
;; effects: applies fn to each representation value in E(var)

(define foreach-in-\overline{E} (lambda (var fn) …))

;; The following three functions maintain a mapping C from program ;; variables to sets of constraints

;; inputs: a variable and a constraint
;; outputs: returns true if C(var) contains the constraint
;; effects: none

(define in-C? (lambda (var constraint) …))

;; inputs: a variable and a constraint
;; outputs: void
;; effects: adds constraint to C(var)

(define add-to-C! (lambda (var constraint) …))

;; inputs: a variable and a function
;; outputs: none
;; effects: applies fn to each constraint in E(var)

(define foreach-in-C (lambda (var fn) …))

Figure 13: The Set-Based Analysis Algorithm: Auxiliary Functions 2

[7] Feeley, M., and Miller, J. S. A parallel virtual machine for efficient scheme compilation. In LFP (1990).

[8] Flanagan, C., and Felleisen, M. The semantics of Future. Rice University Computer Science TR94-238.

[9] Flanagan, C., and Felleisen, M. The semantics of future and its use in program optimizations. In POPL (Jan. 1995).

[10] Flanagan, C., Sabry, A., Duba, B. F., and Felleisen, M. The essence of compiling with continuations. In PLDI (1993), pp. 237–247.

[11] Halstead, R. Multilisp: A language for concurrent symbolic computataion. ACM Transactions on Programming Languages and Systems 7, 4 (1985), 501–538.

[12] Heintze, N. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, 1992.

[13] Heintze, N. Set-based analysis of ML programs. In LFP (1994), pp. 306–317.

[14] Henglein, F. Global tagging optimization by type inference. In LFP (1992), pp. 205– 215.

[15] Ito, T., and Halstead, R., Eds. Parallel Lisp: Languages and Systems. Springer-Verlag Lecture Notes in Computer Science 441, 1989.

[16] Ito, T., and Matsui, M. A parallel lisp language: Pailisp and its kernel specification. [15:58–100].

[17] Jagannathan, S., and Weeks, S. Analyzing stores and references in a parallel symbolic language. In LFP (1994), pp. 294–305.

[18] Katz, M., and Weise, D. Continuing into the future: on the interaction of futures and first-class continuations. In LFP (1990).

[19] Kessler, R.R., and R. Swanson. Concurrent scheme. [15:200–234].

[20] Knopp, J. Improving the performance of parallel lisp by compile time analysis. [15:271–277].

[21] Kranz, D., Halstead, R., and Mohr, E. Mul-T: A high-performance parallel lisp. [15:306–321].

[22] Kranz, D., Halstead, R., and Mohr, E. Mul-T: A high-performance parallel lisp. In PLDI (1989), pp. 81–90.

[23] Miller, J. MultiScheme: A Parallel Processing System. PhD thesis, MIT, 1987.

[24] Mohr, E., Kranz, R., and Halstead, R. Lazy task creation: A technique for increasing the granularity of parallel programs. In LFP (1990).

[25] Moreau, L. Sound Evaluation of Parallel Functional Programs with First-Class Continuations. PhD thesis, Universite de Liege, 1994.

[26] Shivers, O. Control-flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, Carnegie-Mellon University, 1991.

[27] Swanson, M., Kessler, R., and Lindstrom, G. An implementation of portable standard lisp on the BBN butterfly. In LFP (1988), pp. 132–142.

[28] Wright, A. K., and Duba, B. F. Pattern matching for Scheme. Unpublished manuscript, 1993.

[29] Wright, A. and R. Cartwright. A practical soft type system for scheme. In LFP (1994), pp. 250–262.