Communications - September 2011

continuation pointer) machine.

ς ∈ å = Exp × Env × Store × Addr
s ∈ Storable = Val × Env + Cont
k ∈ Cont = mt | ar(e, r, a) | fn(v, r, a).

The transition function for the CESK* machine is defined in Figure 2. The initial state for a program is given by the injCESK* function, which combines the expression with the empty environment and a store with a single pointer to the empty continuation, whose address serves as the initial continuation pointer:

injCESK*(e) = áe, 0/, [a0

mt], a0ñ.

An evaluation function based on this machine is defined following the template of the CEK evaluation given in Section 2.2:

evalCESK*(e) = real(v, r, s ), where
inj CESK*(e) → CESK áv, r, s, a0ñ,
where the real function is suitably extended to follow the
environment’s indirection through the store.

CESK*(e) = {ς| injCESK*(e) →CESK*ς}.

Observe that for any program, the CEK and CESK* machines operate in lock-step: each machine transitions, by the corresponding rule, if and only if the other machine transitions.

Lemma 2 CESK (e) CEK (e)

The above lemma implies correctness of the machine.

Lemma 3 (CESK* Correctness) evalCESK* = eval.

addresses, abstraction and allocation: The CESK* machine, as defined in Figure 2, nondeterministically chooses addresses when it allocates a location in the store, but because machines are identified up to consistent renaming of addresses, the transition system remains deterministic.

Looking ahead, an easy way to bound the state space of this machine is to bound the set of addresses. But once

figure 2. CesK* machine.

ς;−→CESK∗ ς ;, where κ = σ(a), b∈ ; dom(σ)

;x, ρ, σ, a;
;(e0e1), ρ, σ, a;
;v, ρ, σ, a;
if κ = ar(e, ρ;, c)
if κ = fn((λx.e), ρ;, c)

;v, ρ;, σ, a; where (v, ρ;) = σ(ρ(x))

;e0, ρ, σ[b ;→ ar(e1, ρ, a)], b; ;e, ρ;, σ[b ;→ fn(v, ρ, c)], b; ;e, ρ;[x ;→ b], σ[b ;→ (v, ρ)], c;

the store is finite, locations may need to be reused and when multiple values are to reside in the same location; the store will have to soundly approximate this by joining the values.

In our concrete machine, all that matters about an allocation strategy is that it picks an unused address. In the abstracted machine however, the strategy will all but certainly have to reuse previously allocated addresses. The abstract allocation strategy is therefore crucial to the design of the analysis—it indicates when finite resources should be doled out and decides when information should deliberately be lost in the service of computing within bounded resources. In essence, the allocation strategy is the heart of an analysis.

For this reason, concrete allocation deserves a bit more attention in the machine. An old idea in program analysis is that dynamically allocated storage can be represented by the state of the computation at allocation time10; Section 1. 2. 2 of Midtgaard. 13 That is, allocation strategies can be based on a (representation) of the machine history. Since machine histories are always fresh, we call them time-stamps.

A common choice for a time-stamp, popularized by Shivers, 21 is to represent the history of the computation as contours, finite strings encoding the calling context. We present a concrete machine that uses a general time-stamp approach and is parameterized by a choice of tick and alloc functions.

2. 4. time-stamPeD CesK* maChine

The machine states of the time-stamped CESK* machine include a time component, which is intentionally left unspecified:

t, u ∈ Time
ς ∈ å = Exp × Env × Store × Addr × Time.

The machine is parameterized by the functions:

tick : å → Time alloc : å → Addr.

The tick function returns the next time; the alloc function allocates a fresh address for a binding or continuation. We require of tick and alloc that for all t and ς, t  tick(ς) and alloc (ς) ∉ s where ς = á_, _, s, _, tñ.

The time-stamped CESK* machine is defined in Figure 3. Note that occurrences of ς on the right-hand side of this definition are implicitly bound to the state occurring on the left-hand side. The evaluation function evalCESK*t and reachable states CESK*t are defined following the same outline as before and omitted for space. The initial machine state is defined as