Abstract Machines for Memory Management

Christopher Walton

Laboratory for Foundations of Computer Science Division of Informatics The University of Edinburgh

                cdw@dcs.ed.ac.uk

June 17, 1999

Abstract

In composing the Definition of Standard ML [1], the authors chose not to give an account of the operation of memory management. This was the right decision when focussing upon the abstract description of a sophisticated high-level language. However, the issues associated with memory management cannot be ignored by the compiler writer who must make decisions which have a great impact on the performance of the compiled code.

In the first half of this report, an abstract machine formalism of an efficient tag-free garbage-collector is presented which exposes many important memory management details such at the heaps, stacks, and environments. This model provides an implementor with an unambiguous and precise description of a memory management strategy for Standard ML. The second half of the report extends the abstract machine model to provide a formalism of distributed memory management in the LEMMA interface [2]. The extended model provides an appropriate setting for an implementation of Concurrent ML [3].

Keywords: Memory Management; Abstract Machines; Concurrent ML

1 Introduction

A significant advantage of high-level programming languages, such as Standard ML, is that the programmer is freed from the error-prone tasks associated with memory management. This is reflected in The Definition of Standard ML [1] which avoids an explicit treatment of memory management except to say that “there are no [semantic] rules concerning the disposal of inaccessible addresses”.

For many purposes, such as reasoning about programs, this approach is entirely suitable. Nonetheless, the issues of memory management cannot be entirely overlooked. An important use of the Definition is to serve as a guide for the compiler writer who must make memory management decisions that critically affect the performance of compiled code. Other authors have also argued for the usefulness of a semantic model in making precise the important notions of space-safety and data sharing [4].

In a previous paper [5] a novel abstract machine, with an explicit treatment of memory management, was presented for the purpose of describing a runtime code-replacement operation. The intention of this report is to extend this model to provide a complete semantic account of memory management in both a sequential and distributed setting.

Memory is typically modelled using a stack and a heap. The stack holds temporary values of known size whose lifetime is determined by function applications, e.g. function parameters and local variables. The heap holds all other values, e.g. closures and dynamic data structures. Memory management of the stack is relatively straightforward as values are simply added or removed from the top of the stack. By contrast, memory management of the heap is considerably more challenging.

Without a system for automatic memory management, the programmer is left to manage the heap using explicit allocation and de-allocation facilities, e.g. malloc and free in C. For non-trivial programs this can be a very significant burden as it is, in general, very hard to ensure that an area of memory will not be required by a later computation. If memory is de-allocated too hastily, then the program will fail when it requires a value that has been removed. Conversely, if memory is de-allocated too conservatively, then the program may exhaust the supply of memory available.

The prevailing technique for automatic memory management of the heap is garbage collection. Heap allocation is performed (implicitly) by the programmer, and de-allocation by the garbage collector. Garbage collection is based on the idea that if a value is reachable, either from the stack or from a set of roots, then it must not be discarded. A survey of different garbage collection techniques is presented in [6].

It is also worth noting that an alternative, called region based memory management, has recently been developed [7]. In this scheme, the memory is modelled using multiple stacks each containing values of a single type. A sophisticated region inference algorithm is used to determine the memory requirements of the program at compile-time, thereby avoiding the need for run-time garbage collection. Although this technique appears to be the ideal solution for memory management, it will not be used in this report as the inference algorithm is primarily designed for sequential operation and contains no obvious method of integration into a distributed environment.

The semantic account of sequential memory management in the first half of this report consists of a formalisation of the two-space copying garbage collection technique which extends the tag-free algorithm presented in [8]. The advantages of the two-space technique are well known, for example, the data is compacted during collection which improves locality, and cyclic garbage is removed. However, the primary reason for selecting this algorithm is that it extends naturally into a distributed setting.

In the distributed case, it is not enough to simply formalise the garbage collection operation. A number of additional operations are also required for distributed memory management, e.g. data sharing between processors. These operations are presented in the LEMMA interface definition [2]. Thus, the second-half of this report will concentrate on a formalisation of this interface.

The LEMMA memory interface was created to support a distributed concurrent extension of Standard ML [3]. In that extension, the language is augmented with a number of constructs for communication and concurrency (Figure 1).

                  channel : ∀ α . unit → α channel
                  send  : ∀ α . α channel × α → unit
                  receive : ∀ α . α channel → α
                  fork  : (unit → unit) → unit
                  rfork  : int × (unit → unit) → unit

Figure 1: Concurrency Primitives.

Communication channels are created using the channel primitive. A thread sends a value to another thread using the send primitive, which takes two arguments: a channel and a value. The receiving thread uses the receive primitive, which takes a channel argument. Both threads are blocked until the value is passed, which happens atomically. Channels are typed, that is the type system ensures that values sent and received on a particular channel have the same type. Threads are created either using the fork primitive, which runs the child thread on the same processor as its parent, or the rfork primitive, which runs the child process on a specified processor. Both fork and rfork take a function argument, whose body is evaluated in the child thread. When the function returns, the thread is terminated. The rfork primitive takes an additional argument which specifies where the child thread is to run. An example illustrating the concurrency primitives is shown in Figure 2. In this example, a thread is created on processor 2 that simply waits for an integer value on channel c, then returns the value, incremented by 3, on the same channel. The example concludes by sending the value 7 to the thread, and returns the response (which will be 10).

          let val c = channel()
              val   = rfork(2, fn   => send(c, receive(c) + 3))
              val   = send(c, 7)
          in
              receive(c)
          end

Figure 2: Concurrent ML Example.

2 The MΛ Language

Throughout this report, the formalisation of memory management is illustrated with respect to a typed call-by-value lambda language. The language is representative of a typical intermediate language used in a modern ML compiler. By basing the formalisation on such an intermediate language, it is possible to demonstrate that the memory-management operations are applicable to the whole of Standard ML (with the exception on the module system) without encountering a great deal of the complexity. For example, Standard ML pattern matching appears as simpler switch statements in the intermediate language, having been converted by a higher-level match compiler.

Type  τ ::= tn | tn(τ) | \overline{τ}^{k} | τ_{1} → τ_{2} | tv
Type Scheme σ ::= τ | ∀ \overline{tv}^{k}. τ
Program  P ::= (\overline{\overline{D}}, \overline{\overline{X}}, Λ)
Datatype  D ::= datatype tn of \overline{(con, τ)}^{k}
| datatype (\overline{tv}^{k}, tn) of \overline{(con, τ)}^{l}
Exception  X ::= exception (con, τ)
Expression  Λ ::= scon scon
| con con | con (con, Λ)
| con (con, \overline{τ}^{k}) | con (con, \overline{τ}^{k}, Λ)
| decon (con, Λ) | decon (con, \overline{τ}^{k}, Λ)
| assign (Λ_{1}, Λ_{2})
| tuple \overline{Λ}^{k} | select (i, Λ)
| prim (op, \overline{Λ}^{k})
| var lv | var (lv, \overline{τ}^{k})
| let (lv, σ) = Λ_{1} in Λ_{2} | let \overline{(lv, σ)}^{k} = Λ_{1} in Λ_{2}
| fix \overline{(lv, σ) = Λ_{1}} ^{k} in Λ_{2}
| fn (lv, τ_{1} → τ_{2}) = Λ | fn (\overline{lv}^{k}, \overline{τ_{1}} ^{k} → τ_{2}) = Λ
| app (Λ_{1}, Λ_{2}) | app (Λ_{1}, \overline{Λ_{2}} ^{k})
| switch Λ_{1} case (c ↦^{map} Λ_{2}, Λ_{3})
| raise (Λ, τ) | handle Λ_{1} with Λ_{2}
| fork Λ | rfork (Λ_{1}, Λ_{2})
| channel ()
| send (Λ_{1}, Λ_{2}) | receive Λ

Figure 3: MΛ Abstract Syntax.

Notation: A set is defined by enumerating its members in braces, such as \overline{\overline{x}} = \{a, b, c\} with ∅ for the empty set. A sequence is an ordered list of members of a set, e.g. \overline{x}^{k} = (a, b, c, a). The ith element of a non-empty sequence is written x^{i}, where 0 < i ≤ k. A finite map from \overline{x}^{k} to \overline{y}^{k} is defined: x ↦^{map} y = \{x^{1} ↦ y^{1}, …, x^{k} ↦ y^{k}\} (the elements of \overline{x}^{k} must be unique). The domain Dom and range Rng are the sets of elements of \overline{x}^{k} and \overline{y}^{k} respectively. A stack is written as a dotted sequence, e.g. S = (a·b·c). The left-most element of the sequence is the top of the stack, and a pair of adjacent brackets () is used to represent the empty stack.

The syntax of the MΛ language is shown in Figure 3. The syntactic categories of the language include special constants scon (unit, integer, word, real, character, and string) and constructors con such as c true and e match, with c ranging over both of these, and i over special constants of integer type. The meta-variables tn, tv, and lv are used for type names, type variables, and lambda variables. Type variables tv are bound to types, and lambda variables lv are bound uniquely to values generated by the evaluation of expressions.

The types τ are either constructor types (which may be nullary or unary), tuple types, functional types, or type variables. Expressions are provided for creating values of each of these types directly, with the exception of type variables. Constructor types tn and tn(τ) include the basic types, as required by the special constants; value constructor types; reference constructor types; and exception constructor types. Type-schemes σ can represent polymorphic types. For example, the polymorphic identity function is represented by the type scheme ∀ α . α → α, where α is a type variable.

A program in the language contains a set of datatype declarations, a set of exception declarations, and an expression. A datatype declaration consists of a unique type name and a list of typed constructors. Each exception declaration consists of a unique exception name and an exception type. The expressions divide into those for constructing and de-constructing values, defining and manipulating variables, and controlling the order of evaluation. A small example is shown in Figure 4 to illustrate the differences between Standard ML and MΛ.

Standard ML:

      exception Factorial
      fun fac n = if (n < 0) then raise Factorial
                  else if (n = 0) then 1
                  else n * fac(n - 1)
      fac 10;

MΛ Translation:

(∅, exception (e factorial, t unit), fix (fac, t int → t int) = fn (n, t int → t int) =

switch (prim (LT_{i}, (var n, scon 0)))

case ({c true ↦ raise (con e factorial, t int),

c false ↦ switch (prim (EQ_{i}, (var n, scon 0))) case ({c true ↦ scon 1,

c false ↦

prim (MUL_{i}, (var n,

app (var fac, prim (SUB_{i}, (var n, scon 1)))))}, raise (con e match, t int))},

raise (con e match, t int)) in app (varfac, scon 10))

Figure 4: Factorial Example.

3 Sequential Memory Management

In order to formalise the sequential garbage collection operation, it is necessary to define the dynamic semantics of the sequential sub-language (i.e. excluding the communication and concurrency operations). The dynamic semantics of MΛ are formalised by a transition relation between states of an abstract machine. The machine describes the memory management behaviour of an implementation of the language, except that it abstracts from the allocation of environments. The allocation of environments simply adds extra baggage to the rules, for a treatment of this topic see [9]. The organisation of the MΛ abstract machine has some features in common with the λgc^{→∀} abstract machine [4] which is used in the formal description of the behaviour of the TIL/ML compiler. However, the transitions differ considerably as MΛ does not adopt the named-form representation of expressions and types.

The syntax of the abstract machine is given in Figure 5. The state of the machine is defined by a 4-tuple (H, E, ES, RS) of a heap, an environment, an exception stack, and a result stack. The heap is used to store all the run-time data of the program, while the environment provides a view of the heap relevant to the fragment of the program being evaluated, e.g. a mapping between the bound variables currently in scope, and their values on the heap. The exception stack stores pointers to exception handling functions (closures). The result stack holds pointers to temporary results during evaluation. Thus, the memory of the machine is effectively modelled by the heap, as the stacks simply contain pointers into the heap.

Machine State  M  ::=  (H, E, ES, RS)
Heap  H  ::=  (TH , VH )
Type Heap  TH  ::=  p ↦^{map} ty
Heap Types  ty  ::=  tn | tn(p) |
\overline{p}^{k} | p_{1} → p_{2} |
tv | ∀ \overline{p_{1}} ^{k} . p_{2}
Value Heap  VH  ::=  l ↦^{map} val
Heap Values  val  ::=  scon | con | con(l) |
\overline{l}^{k} | ⟨⟨E, \overline{lv}^{k}, Λ⟩⟩ | Ω
Environment  E  ::=  (TE, CE, VE)
Type Env.  TE  ::=  \overline{\overline{tn}}
Constructor Env.  CE  ::=  con ↦^{map} p
Variable Env.  VE  ::=  lv ↦^{map} (l, p)
Exception Stack  ES  ::=  () | (l, p)·ES
Result Stack  RS  ::=  () | p·RS | (l, p)·RS | E·RS

Figure 5: MΛ Abstract Machine Syntax.

The heap consists of a type-heap mapping pointers to allocated types, and a value-heap mapping locations to allocated values. The heap types correspond directly to types in the MΛ language, and the heap values correspond to the heap types. Nullary constructors scon and con have type tn. Unary constructors con(l) have type tn(p). Tuples \overline{l}^{k} have type \overline{p}^{k} and function closures ⟨⟨E, \overline{lv}^{k}, Λ⟩⟩ have type p_{1} → p_{2}. The type heap and value heap are represented by finite-maps, as heap-locations and type-pointers may be bound only once.

The shape of the data at a particular heap-location is determined by its corresponding type. Without this type information, a heap value is simply a collection of binary information. The type information makes clear the internal representations of the value, e.g. pointers for garbage collection. Thus, each heap-location must be paired with a type-pointer: (l, p).

It is important to note that there is no explicit notion of a memory address. For example, it is not possible to perform pointer arithmetic, e.g. p_{1} + p_{2}. The only operations permitted on type-pointers and heap-locations are the comparison for equality, e.g. p_{1} = p_{2}, and the retrieval of the corresponding value from the heap, e.g. H(p) = tn.

The following syntactic conventions are used for performing heap allocations: H[l_{1} ↦ val_{1}, …, l_{k} ↦ val_{k}] allocates values val_{1}, …, val_{k} on the value heap, binding them to fresh locations l_{1}, …, l_{k}. H[p_{1} ↦ τ_{1}, …, p_{k} ↦ τ_{k}] allocates types τ_{1}, …, τ_{k} on the type heap, binding them to fresh type-pointers p_{1}, …, p_{k}. There are no corresponding operations for removing values or types from the heap as this is achieved through garbage collection. However, the assignment of references and the fixed-point operator require a heap-update operation. Assignment uses the update operation H[l_{1} ↦^{upd} c ref(l_{2})] to update the reference at l_{1} to c ref(l_{2}). This is clearly a trivial operation as it only requires the update of a single heap-location. The fixed-point case is slightly more complex: H[l ↦ Ω] allocates a dummy closure on the value heap bound to a fresh heap-location l. This location can subsequently be updated with a mapping to a closure H[l ↦^{upd} ⟨⟨E, \overline{lv}^{k}, Λ⟩⟩]. In this case, a suitably-sized area of the heap must be reserved to hold the closure.

M = (H, E, (), (), P)
H  = (TH , ∅)
TH = {p_{1} ↦ t unit → t bool,

p_{2} ↦ tv^{1}, p_{3} ↦ ∀ (p_{2}) . t unit → t list(p_{2}),

p_{4} ↦ tv^{2}, p_{5} ↦ ∀ (p_{4}) . (p_{4}, t list(p_{4})) → t list(p_{4}), p_{6} ↦ tv^{3}, p_{7} ↦ ∀ (p_{6}) . p_{6} → t ref(p_{6}), p_{8} ↦ t unit → t exn}

E  = (TE, CE, ∅)
TE = {t unit, t int, t word, t real, t char, t string, t bool,

t list, t ref, t exn}

CE = {c true ↦ p_{1}, c false ↦ p_{1},

c nil ↦ p_{3}, c cons ↦ p_{5}, c ref ↦ p_{7},

e match ↦ p_{8}, e bind ↦ p_{8}}

Figure 6: Initial Machine State.

The environment records the allocation of MΛ values, mapping them to pairs of heap locations and type-pointers. As identifiers and variables are unique, their corresponding environments are represented by finite-maps, with the exception of the type environment where it is sufficient just to use a set for type names. The following notational conventions are used for extending the environment: E[tn] adds tn to the type environment, E[con ↦ p] binds the constructor con to the heap pointer p in the constructor environment. Similarly, E[lv ↦ (l, p)] denotes the binding of a lambda variable to a type-pointers and heap-location in the environment. There are no operations for removing bindings from the environment. However, unlike the heap, a copy of the current environment may be made at any time, for example by creating a closure. Thus, bindings can effectively be removed from the environment by reverting to an old copy of the environment.

Execution of the abstract machine is defined by a transition system between machine states. The individual transitions are listed in Appendix A. The toplevel transition has the form (H_{1}, E_{1}, ES_{1}, RS_{1}, P) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2}), where P is an MΛ program, (H_{1}, E_{1}, ES_{1}, RS_{1}) is the initial machine state (as illustrated in Figure 6), and (H_{2}, E_{2}, ES_{2}, RS_{2}) is the final machine state.

The majority of the rules in Appendix A concern the evaluation of expressions: (H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l, p)·RS_{2}). Evaluating an expression always generates a new machine state and leaves a single pair on the result stack. A new machine state is generated at each step as garbage collection may occur in the middle of an evaluation (this will be discussed in the next section). The transitions for the prim expression do not appear as they are largely trivial. The primitive operations, as defined in the Standard ML Initial Basis, are listed in Figure 7.

There are three possible outcomes which result from an evaluation: termination, exceptional termination and non-termination. Firstly, the sequence of transitions may terminate normally yielding a single pair (l, p) in the result stack which references the result. Secondly, the sequence may terminate prematurely, through an uncaught exception, yielding a pair (l, p) at the top of the result stack which references the exception. Finally, the machine may encounter an infinite sequence of transitions and fail to terminate.

Absolute Value (abs)  ABS_{i}, ABS_{r}
Negate (~)  NEG_{i}, NEG_{r}
Divide (/)  DIV_{r}
Integer Divide (div)  DIV_{i}, DIV_{w}
Modulo (mod)  MOD_{i}, MOD_{w}
Multiply (*)  MUL_{i}, MUL_{w}, MUL_{r}
Add (+)  ADD_{i}, ADD_{w}, ADD_{r}
Subtract (-)  SUB_{i}, SUB_{w}, SUB_{r}
Less (<)  LT_{i}, LT_{w}, LT_{r}, LT_{c}, LT_{s}
Greater (>)  GT_{i}, GT_{w}, GT_{r}, GT_{c}, GT_{s}
Equal (=)  EQ_{i}, EQ_{w}, EQ_{r}, EQ_{c}, EQ_{s}

i = integer, w = word, r = real, c = char, s = string

Figure 7: Primitive Operations (op).

A number of the evaluation rules in Appendix A (e.g. Rule 85) make use of the instance(p_{σ}, p_{τ}) operation which performs the instantiation of the typescheme referenced by p_{σ} with the types referenced by p_{τ} (i.e. the type variables in p_{σ} are substituted with types from p_{τ}). The rules associated with this operation appear in Figure 8. These rules Rule 1 creates a substitution environment S from the type variables of p_{σ} to the types of p_{τ}. The subst(S, p) operation (Rules 2 to 7) are then invoked to perform the substitution. There is a separate case for each of the types in the language. Substitution is performed recursively until all if the types have been examined. Rule 7 performs the actual substitution of a type variable with a type from S.

H_{1}(p_{σ}) = ∀ \overline{p_{1}} ^{k} . p_{2} H_{1}(p_{τ}) = \overline{p_{3}} ^{k} S = {p_{1}^{1} ↦ p_{3}^{1}, …, p_{1}^{k} ↦ p_{3}^{k}} (H_{1}, E, ES, RS_{1}, subst(S, p_{2})) ⇒ (H_{2}, E, ES, RS_{2}) (H_{1}, E, ES, RS_{1}, instance(p_{σ}, p_{τ})) ⇒ (H_{2}, E, ES, RS_{2})

(1)

\frac{H(p) = tn}{(H, E, ES, RS, subst(S, p)) ⇒ (H, E, ES, p·RS)}  (2)

H_{1}(p_{1}) = tn(p_{2}) (H_{1}, E, ES, RS, subst(S, p_{2})) ⇒ (H_{2}, E, ES, p_{3}·RS) (H_{1}, E, ES, RS, subst(S, p_{1})) ⇒ (H_{2}[p_{4} ↦ tn(p_{3})], E, ES, p_{4}·RS)

(3)

H_{1}(p_{1}) = \overline{p_{2}} ^{k} (H_{1}, E, ES, RS, subst(S, p_{2}^{1})) ⇒ (H_{2}, E, ES, p_{3}^{1}·RS) ⋯

(H_{k}, E, ES, RS, subst(S, p_{2}^{k})) ⇒ (H_{k+1}, E, ES, p_{3}^{k}·RS) (H_{1}, E, ES, RS, subst(S, p_{1})) ⇒ (H_{k+1}[p_{4} ↦ \overline{p_{3}} ^{k}], E, ES, p_{4}·RS)

(4)

H_{1}(p_{1}) = p_{2} → p_{3} (H_{1}, E, ES, RS, subst(S, p_{2})) ⇒ (H_{2}, E, ES, p_{4}·RS) (H_{2}, E, ES, RS, subst(S, p_{3})) ⇒ (H_{3}, E, ES, p_{5}·RS) (H_{1}, E, ES, RS, subst(S, p_{1})) ⇒ (H_{3}[p_{6} ↦ p_{4} → p_{5}], E, ES, p_{6}·RS)

(5)

\frac{H(p) = tv  p ∉ Dom S}{(H, E, ES, RS, subst(S, p)) ⇒ (H, E, ES, p·RS)}  (6)

\frac{H(p) = tv  p ∈ Dom S}{(H, E, ES, RS, subst(S, p)) ⇒ (H, E, ES, S(p)·RS)}  (7)

Figure 8: Polymorphic Type Instantiation.

3.1 Sequential Garbage Collection

The following semantic account of sequential memory management consists of a formalisation of two-space copying garbage collection. Before proceeding, it is necessary to obtain an understanding of the basic algorithm. The address space of the heap is divided into two contiguous semi-spaces. During normal program execution, only one of these semi-spaces is used. Memory is allocated in a linear fashion until garbage collection appears to be profitable. At this point, the copying collector is called to reclaim space. The current semi-space (from space) is recursively scanned from the root objects, and all reachable objects are copied into the other semi-space (to space). When all of the objects that are reachable from the roots have been copied, the collection is finished, and the old semi-space (from space) can be discarded (see Figure 9). Subsequent memory allocations are performed in the new space (to space). The role of the semi-spaces is then reversed for the next garbage collection.

roots from space (before collection)  (after collection) to space free space ⋯ garbage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 9: Two-Space Copying Garbage Collection

The MΛ garbage collection algorithm uses the type-based, tag-free style of [8]. The key idea is to preserve all heap values and types that are reachable either directly or indirectly from the current environment and stacks. The type information is used to determine the shape of the heap values. This allows the extraction of further locations and their types from the heap values without resorting to extra tags on the values themselves.

The garbage collector uses several data structures illustrated in Figure 10. The state of the garbage collector is the 4-tuple (Hf , Ht, PF , LF ). The from space (heap) is denoted Hf , and the to space (heap) is denoted Ht. When a type or a value is copied from Hf into Ht, an entry is created in either PF or LF respectively. An entry p_{1} ↦ p_{2} in PF represents a copied type where p_{1} is the old type-pointer in Hf , and p_{2} is the new type-pointer in Ht. Similarly, an entry l_{1} ↦ l_{2} in LF represents a copied value. These forwarding tables are used during garbage collection to ensure that a type or value is copied only once between spaces.

Garbage Collection State  GC  ::=  (Hf , Ht, PF , LF )
From Semi-space  Hf  ::=  H
To Semi-space  Ht  ::=  H
Forwarding Type Pointer  PF  ::=  p_{1} ↦ p_{2}
Forwarding Value Pointer  LF  ::=  l_{1} ↦ l_{2}

Figure 10: Garbage Collection Structures.

The garbage collection operation is defined by a transition system between garbage collection states. The roots of the garbage collection are the current environment E, the exception stack ES, and the result stack RS. Garbage collection is incorporated into the dynamic semantics of MΛ through the rule in Figure 11. Garbage collection can occur when an expression Λ is to be evaluated. At this point, the machine is interrupted, the garbage collector is initialised, and collection proceeds from each of the roots in turn. Once collection has completed, the evaluation of Λ resumes with the new abstract machine state.

The complex issue of when to initiate a collection will not be dealt with in detail here. However, a discussion can be found in [10] where the authors arrive at the following rule:

• For some constant R > 1, when current memory usage is more than R times the amount of reachable data preserved by the previous garbage collection, start a new garbage collection.

The MΛ abstract machine transitions in Appendix A have been designed with garbage collection in mind. As stated earlier in Section 3, a new machine state is generated by the evaluation of each expression to reflect the fact that garbage collection may have occurred. A number of the other rules also involve extra garbage collection considerations. For example, in the let expression (Rule 98) a copy of the environment is placed on the result stack while the body of the let expression is evaluated. This environment is later restored from the result stack to remove any bindings created during the evaluation of the body. The numbering of these environments reflects the fact that collections may have occured during the evaluation, and the stored environment on the result stack may have been updated.

(Hf , ∅, ∅, ∅, E_{1}) ⇒_{gc} (Hf , Ht_{1}, PF_{1}, LF_{1}, E_{2}) (Hf , Ht_{1}, PF_{1}, LF_{1}, ES_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, ES_{2}) (Hf , Ht_{2}, PF_{2}, LF_{2}, RS_{1}) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF_{3}, RS_{2}) (Ht_{3}, E_{2}, ES_{2}, RS_{2}, Λ) ⇒ (Ht_{4}, E_{3}, ES_{3}, RS_{3}) (Hf , E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (Ht_{4}, E_{3}, ES_{3}, RS_{3})

(8)

Figure 11: Garbage Collection Introduction.

The garbage collection rules are defined in Figures 12 through 15. These in turn deal with the garbage collection of types, values, environments, and stacks. The garbage collection of types is defined by a series of rules of the form (Hf , Ht_{1}, PF_{1}, LF , p_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF , p_{2}). These rules perform a recursive copy of the type referenced by p_{1} (in Hf ) into Ht. The final state contains the copied type in Ht_{2}, a new pointer to the type p_{2}, and entries in PF_{2} for the copied type. There are separate rules for each of the MΛ types. Rule 9 ensures that types are only copied once.

\frac{p_{1} ∈ Dom PF}{(Hf , Ht, PF , LF , p_{1}) ⇒_{gc} (Hf , Ht, PF , LF , PF (p_{1}))}  (9)

\frac{p_{1} ∉ Dom PF  Hf (p_{1}) = tn}{(Hf , Ht, PF , LF , p_{1}) ⇒_{gc} (Hf , Ht[p_{2} ↦ tn], PF [p_{1} ↦ p_{2}], LF, p_{2})}  (10)

p_{1} ∉ Dom PF_{1} Hf (p_{1}) = tn(p_{2}) (Hf , Ht_{1}, PF_{1}, LF , p_{2}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF , p_{3}) (Hf , Ht_{1}, PF_{1}, LF , p_{1}) ⇒_{gc}

(Hf , Ht_{2}[p_{4} ↦ tn(p_{3})], PF_{2}[p_{1} ↦ p_{4}], LF , p_{4})

(11)

p_{1} ∉ Dom PF_{1} Hf (p_{1}) = \overline{p_{2}} ^{k} (Hf , Ht_{1}, PF_{1}, LF , p_{2}^{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF , p_{3}^{1}) ⋯

(Hf , Ht_{k}, PF_{k}, LF , p_{2}^{k}) ⇒_{gc} (Hf , Ht_{k+1}, PF_{k+1}, LF , p_{3}^{k}) (Hf , Ht_{1}, PF_{1}, LF , p_{1}) ⇒_{gc}

(Hf , Ht_{k+1}[p_{4} ↦ (p_{3}^{1}, …, p_{3}^{k})], PF_{k+1}[p_{1} ↦ p_{4}], LF , p_{4})

(12)

p_{1} ∉ Dom PF_{1} Hf (p_{1}) = p_{2} → p_{3} (Hf , Ht_{1}, PF_{1}, LF , p_{2}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF , p_{4}) (Hf , Ht_{2}, PF_{2}, LF , p_{3}) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF , p_{5}) (Hf , Ht_{1}, PF_{1}, LF , p_{1}) ⇒_{gc}

(Hf , Ht_{3}[p_{6} ↦ p_{4} → p_{5}], PF_{3}[p_{1} ↦ p_{6}], LF , p_{6})

(13)

\frac{p_{1} ∉ Dom PF  Hf (p_{1}) = tv}{(Hf , Ht, PF , LF , p_{1}) ⇒_{gc} (Hf , Ht[p_{2} ↦ tv], PF [p_{1} ↦ p_{2}], LF, p_{2})}  (14)

p_{1} ∉ Dom PF_{1} Hf (p_{1}) = ∀ \overline{p_{2}} ^{k}. p_{3} (Hf , Ht_{1}, PF_{1}, LF , p_{2}^{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF , p_{4}^{1}) ⋯

(Hf , Ht_{k}, PF_{k}, LF , p_{2}^{k}) ⇒_{gc} (Hf , Ht_{k+1}, PF_{k+1}, LF , p_{4}^{k}) (Hf , Ht_{k+1}, PF_{k+1}, LF , p_{3}) ⇒_{gc} (Hf , Ht_{k+2}, PF_{k+2}, LF , p_{5}) (Hf , Ht_{1}, PF_{1}, LF , p_{1}) ⇒_{gc}

(Hf , Ht_{k+2}[p_{6} ↦ ∀ \overline{p_{4}} ^{k}. p_{5}], PF_{k+2}[p_{1} ↦ p_{6}], LF , p_{6})

(15)

Figure 12: Type Heap Rules.

\frac{l_{1} ∈ Dom LF}{(Hf , Ht, PF , LF , (l_{1}, p_{1})) ⇒_{gc} (Hf , Ht, PF , LF , (LF (l_{1}), p_{1}))}  (16)

l_{1} ∉ Dom LF Hf (p_{1}) = tn (Hf , Ht, PF , LF , (l_{1}, p_{1})) ⇒_{gc}

(Hf , Ht[l_{2} ↦ Hf (l_{1})], PF , LF [l_{1} ↦ l_{2}], (l_{2}, p_{1}))

(17)

l_{1} ∉ Dom LF_{1}  Hf (p_{1}) = tn(p_{2})  Hf (l_{1}) = con(l_{2})

(Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{2}, p_{2})) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, (l_{3}, p_{2})) (Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{1}, p_{1})) ⇒_{gc}

(Hf , Ht_{2}[l_{4} ↦ con(l_{3})], PF_{2}, LF_{2}[l_{1} ↦ l_{4}], (l_{4}, p_{1}))

(18)

l_{1} ∉ Dom LF_{1}  Hf (p_{1}) = \overline{p_{2}} ^{k}  Hf (l_{1}) = \overline{l_{2}} ^{k}

(Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{2}^{1}, p_{2}^{1})) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, (l_{3}^{1}, p_{2}^{1})) ⋯

(Hf , Ht_{k}, PF_{k}, LF_{k}, (l_{2}^{k}, p_{2}^{k})) ⇒_{gc}

(Hf , Ht_{k+1}, PF_{k+1}, LF_{k+1}, (l_{3}^{k}, p_{2}^{k})) (Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{1}, p_{1})) ⇒_{gc}

(Hf , Ht_{k+1}[l_{4} ↦ (l_{3}^{1}, …, l_{3}^{k})], PF_{k+1}, LF_{k+1}[l_{1} ↦ l_{4}], (l_{4}, p_{1}))

(19)

l_{1} ∉ Dom LF_{1}  Hf (p_{1}) = p_{2} → p_{3}  Hf (l_{1}) = ⟨⟨E_{1}, \overline{lv}^{k}, Λ⟩⟩

(Hf , Ht_{1}, PF_{1}, LF_{1}, E_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, E_{2}) (Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{1}, p_{1})) ⇒_{gc}

(Hf , Ht_{2}[l_{2} ↦ ⟨⟨E_{2}, \overline{lv}^{k}, Λ⟩⟩], PF_{2}, LF_{2}[l_{1} ↦ l_{2}], (l_{2}, p_{1}))

(20)

l_{1} ∉ Dom LF_{1}  Hf (p_{1}) = p_{2} → p_{3}  Hf (l_{1}) = Ω

(Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{1}, p_{1})) ⇒_{gc} (Hf , Ht_{2}[l_{2} ↦ Ω], PF_{2}, LF_{2}[l_{1} ↦ l_{2}], (l_{2}, p_{1}))

(21)

Figure 13: Value Heap Rules.

The garbage collection of values is defined in Figure 13 by rules of the form (Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{1}, p_{1})) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, (l_{2}, p_{2})). These rules perform a recursive copy of the value referenced by l_{1} into Ht_{1}. This uses the type referenced by p_{1} to determine the shape. The result is a new location l_{2} which references the copied value in Ht_{2}. There is a separate rule for each of the MΛ values. In the case where the value is a closure (Rule 20), the rules in Figure 14 are used to copy the closure environment.

The collection rules for environments are given in Figure 14. These rules have the form (Hf , Ht_{1}, PF_{1}, LF_{1}, E_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, E_{2}). The environment E_{1} is decomposed into a constructor environment CE_{1}, and a value environment V E_{1}. A new constructor environment CE_{2} is built by copying all of the types referenced in CE_{1}. Similarly, a new value environment V E_{2} is built by copying all of the values and types referenced in V E_{1}. Finally, a new environment E_{2} is built from CE_{2}, and V E_{2}.

E_{1} = (TE, CE_{1}, VE_{1}) CE_{1} = {con^{1} ↦ p_{1}^{1}, …, con^{k} ↦ p_{1}^{k}} (Hf , Ht_{1}, PF_{1}, LF_{1}, p_{1}^{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{1}, p_{2}^{1}) ⋯

(Hf , Ht_{k}, PF_{k}, LF_{1}, p_{1}^{k}) ⇒_{gc} (Hf , Ht_{k+1}, PF_{k+1}, LF_{1}, p_{2}^{k}) CE_{2} = {con^{1} ↦ p_{2}^{1}, …, con^{k} ↦ p_{2}^{k}} V E_{1} = {lv^{1} ↦ (l_{1}^{1}, p_{1}^{1}), …, lv^{l} ↦ (l_{1}^{l}, p_{1}^{l})} (Hf , Ht_{k+1}, PF_{k+1}, LF_{1}, p_{1}^{1}) ⇒_{gc} (Hf , Ht_{k+2}, PF_{k+2}, LF_{1}, p_{2}^{1}) ⋯

(Hf , Ht_{k+l}, PF_{k+l}, LF_{1}, p_{1}^{l}) ⇒_{gc} (Hf , Ht_{k+l+1}, PF_{k+l+1}, LF_{1}, p_{2}^{l}) (Hf , Ht_{k+l+1}, PF_{k+l+1}, LF_{1}, (l_{1}^{1}, p_{1}^{1})) ⇒_{gc}

(Hf , Ht_{k+l+2}, PF_{k+l+2}, LF_{2}, (l_{2}^{1}, p_{1}^{1})) ⋯

(Hf , Ht_{k+2l}, PF_{k+2l}, LF_{l}, (l_{1}^{l}, p_{1}^{l})) ⇒_{gc}

(Hf , Ht_{k+2l+1}, PF_{k+2l+1}, LF_{l+1}, (l_{2}^{l}, p_{1}^{l}))

V E_{2} = {lv^{1} ↦ (l_{2}^{1}, p_{2}^{1}), …, lv^{l} ↦ (l_{2}^{l}, p_{2}^{l})} E_{2} = (TE, CE_{2}, VE_{2}) (Hf , Ht_{1}, PF_{1}, LF_{1}, E_{1}) ⇒_{gc} (Hf , Ht_{k+2l+1}, PF_{k+2l+1}, LF_{l+1}, E_{2})

(22)

Figure 14: Environment Rule.

The garbage collection rules in Figure 15 are used to copy a stack recursively. The item at the top of the stack is either a type, a value, or an environment. This will cause the invocation of the corresponding rule from one of the previous three figures. The four rules for collecting stacks all have the form (Hf , Ht_{1}, PF_{1}, LF_{1}, S_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, S_{2}).

(Hf , Ht, PF , LF , ()) ⇒_{gc} (Hf , Ht, PF , LF , ())

(23)

(Hf , Ht_{1}, PF_{1}, LF_{1}, p_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{1}, p_{2}) (Hf , Ht_{2}, PF_{2}, LF_{1}, S_{1}) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF_{2}, S_{2}) (Hf , Ht_{1}, PF_{1}, LF_{1}, p_{1}·S_{1}) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF_{2}, p_{2}·S_{2})

(24)

(Hf , Ht_{1}, PF_{1}, LF_{1}, p_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{1}, p_{2}) (Hf , Ht_{2}, PF_{2}, LF_{1}, (l_{1}, p_{1})) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF_{2}, (l_{2}, p_{1})) (Hf , Ht_{3}, PF_{3}, LF_{2}, S_{1}) ⇒_{gc} (Hf , Ht_{4}, PF_{4}, LF_{3}, S_{2}) (Hf , Ht_{1}, PF_{1}, LF_{1}, (l_{1}, p_{1})·S_{1}) ⇒_{gc} (Hf , Ht_{4}, PF_{4}, LF_{3}, (l_{2}, p_{2})·S_{2})

(25)

(Hf , Ht_{1}, PF_{1}, LF_{1}, E_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF_{2}, E_{2}) (Hf , Ht_{2}, PF_{2}, LF_{2}, S_{1}) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF_{3}, S_{2}) (Hf , Ht_{1}, PF_{1}, LF_{1}, E_{1}·S_{1}) ⇒_{gc} (Hf , Ht_{3}, PF_{3}, LF_{3}, E_{2}·S_{2})

(26)

Figure 15: Stack Rules.

4 Distributed Memory Management

The LEMMA memory interface [2] identifies two main services that are required for distributed memory management: sharing of distributed data, and distributed garbage collection. As far as possible, the LEMMA interface has been designed to be independent of the details of the language implemented on it, and also as independent as possible of the memory and communication system on which it is implemented. The interface definition is simply a function-level specification, the actual implementation is left open. Different implementations of the interface have been created for parallel computers [11] and local-area networks of workstations [12]. A wide-area network implementation is also in progress. In each case, the assumptions regarding the speed and reliability of the underlying network require a different solution. Here the focus is on providing an abstract machine definition suitable for the LEMMA interface on a reliable local-area network. However, the resulting definition can easily be extended to cover a range of possibilities.

The LEMMA interface is based on the Distributed Shared Memory (DSM) model [13]. In this model, the memory of the distributed system is treated as a single globally-addressable object. LEMMA statically partitions the global address space into contiguous semi-spaces, where each semi-space is managed by a different machine. Each machine is responsible for allocation and garbagecollection within its own semi-space.

Space Managed By Machine3 Space Managed By Machine2 Space Managed By Machine1 Data Copied From Machine2 Virtual Address Spaces Machine1  Machine3 Machine2

Figure 16: Distributed Memory Access.

In a parallel implementation, where communication costs are low, data accesses are simply performed in-place in the global address space. However, in a workstation implementation, the overheads associated with distributed memory access necessitate a form of caching mechanism. The solution adopted by the workstation implementation of LEMMA uses the fact that a typical workstation has a very large virtual address space, but only uses a fraction of it for its real memory. Thus, the virtual address space on each machine is used to represent the entire distributed address space. When a machine wishes to access some external data, it simply addresses its own virtual address space at the required location. The page-faulting mechanism of the operating system is extended to fetch the data from the remote machine, as illustrated in Figure 16. Further accesses to the data will simply use the local copy. This operation can be implemented very efficiently on a typical UNIX workstation.

It is clear that some form of coherency protocol is also required. The original data may be updated, invalidating any copies on other machines. A number of schemes for ensuring coherency are detailed in [14]. One significant property of typical Standard ML programs is that most of the data values are immutable. The only values on which updates are permitted are references. Thus, LEMMA distinguishes between mutables and immutables and only performs coherency checks on the mutables. For brevity, only the caching of immutables is formalised in this report. Mutables are simply accessed in-place remotely. A formalisation of the caching and coherency mechanism for the mutables is left as further work.

The provision of efficient algorithms for distributed garbage collection continues to be a very active area of garbage collection research. Techniques vary from simple schemes (e.g. where one process garbage collections while another executes), up to complex multi-generational schemes. A survey of distributed garbage collection techniques is presented in [15]. The technique presented here is not the most efficient, but extends naturally from the sequential case described in the previous section. A number of techniques for improving the efficiency of the algorithm are outlined in [12].

Each semi-space of the global address space managed by each machine is further divided in two to constitute the from and to spaces. The collective from and to spaces are the concatenation of these local spaces. Garbage collection begins with a global synchronisation. All of the machines perform garbage collection in parallel, but asynchronously. The task of each machine is to ensure that all of the objects in the collective from space that are reachable from its own roots have been copied into the collective to space. Once all of the machines have finished, the global garbage collection is complete and each machine resumes executing in its local to space.

The garbage collection algorithm executed by each machine is the same as the sequential variant with the following addition:

• When machine A encounters a pointer to an object managed by machine B, it sends a message containing the pointer to machine B.

• If the object has already been copied, machine B returns the updated pointer, so machine A can update the object that it was scanning.

• If the object has not been copied, machine B proceeds with the copy and returns the updated pointer to machine A. During the copy, machine B may encounter further remote pointers, in which case the above steps are repeated.

The protocol has the property that an object is always copied by the machine that first created it, even if that machine no longer has a reference to it. It must also be noted that the garbage collection invalidates all of the cached copies of objects on other machines. Optimisations which permit object migration, and provide cache contents preservation are described in [12] although they will not be formalised here.

4.1 Distributed Abstract Machine

The provision of an abstract machine definition for the complete MΛ language introduces a number of interesting problems. The language includes primitives for providing communication and concurrency. However, it is far from obvious how these should be expressed in the abstract machine semantics. An examination of the literature on concurrency in structured operational semantics reveals that a ‘single-step’ (atomic action) approach is typically used to express the computation. Concurrency is then introduced by interleaving the atomic actions of the processes. Unfortunately, this approach is directly in contrast with the abstract machine style, where the intermediate steps are hidden and only the final state of the computation is of interest.

At first glance, it appears that the semantics must be rewritten in the singlestep style before the concurrent extensions can be expressed. This is undesirable for a number of reasons. The abstract machine model provides an ideal setting for expressing memory management behaviour in a manner that approximates an actual implementation. Furthermore, the single-step approach requires a large number of rules for even the simplest of operations. A further problem can occur when some of the intermediate states do not correspond directly to programs in the language. In such cases, the language may need to be extended with additional constructs before the semantics can be defined. Techniques exist for automatically performing this transformation in a number of cases [16]. However, the transformed semantics is rather messy in comparison to the original, and this makes reasoning about the extended language more tedious.

Fortunately, there is an alternative technique inspired by the relational-style semantics of concurrency presented in [17] and [18]. Consider a transition of the form: (H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2}). This transition expresses the evaluation an expression Λ with machine state (H_{1}, E_{1}, ES_{1}, RS_{1}) resulting in the final machine state (H_{2}, E_{2}, ES_{2}, RS_{2}). In the full language, this treatment is no longer acceptable as the evaluation of Λ may require some external interaction before it can yield the result. This leads to a definition of the form (H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒^{t} (H_{2}, E_{2}, ES_{2}, RS_{2}), where t is a trace which records the external interactions required to produce the final result.

Trace t ::= ϵ | t_{1} ; t_{2} | t_{1} ∥ t_{2} | cn ! m | cn ? m

Figure 17: Computation and Communication Traces.

For the MΛ language, the definition of traces in Figure 17 is sufficient. A trace may be empty ϵ if no external interactions occur. The sequential evaluation of two expressions leads to a trace of the form t_{1} ; t_{2}. Similarly, two expressions evaluated in parallel produce a trace of the form t_{1} ∥ t_{2}. A message m sent over a channel cn yields a trace of the form cn ! m, and a message received on the channel gives the trace cn ? m. Figure 18 contains the reduction rules for traces. It should always be the case that the traces reduce to ϵ for a complete program, or an error will have occurred.

ϵ ; t = t (27)

ϵ ∥ t = t (28)

t_{1} ∥ t_{2} = t_{2} ∥ t_{1} (29)

cn ! m ∥ cn ? m = ϵ (30)

cn ! m ; t_{1} ∥ cn ? m ; t_{2} = t_{1} ∥ t_{2} (31)

Figure 18: Trace Reduction Rules.

The syntax of the distributed abstract machine, hereafter referred to as the DMΛ abstract machine, is given in Figure 20. In order to remain consistent with the LEMMA interface definition, the machine contains two levels of abstraction: processes and threads. The sequential abstract machine defined in Section 3 effectively corresponds to a single thread executing on a machine containing a single process.

There are a fixed number k of concurrently executing processes Π each containing a local heap H, a cache C , and a multi-set of threads \overline{\overline{T}} . It is assumed that these processes are physically distributed, for example, across a network of k machines. The memory of the machine is modelled using distributed shared memory. This means that any process can directly access the data contained on the heap of any other process, e.g. H^{i}(p) = ty, where 0 < i ≤ k.

The set of threads associated with each process also execute concurrently. However, unlike processes, the multi-set of threads may dynamically grow or shrink. The multi-set may also be empty. Each thread contains a local environment E, an exception stack ES, and a result stack RS. The threads share the heap of the parent process.

The execution of processes and threads is defined in Figure 19. All of the processes execute concurrently as defined in Rule 32. Note the parallel composition of the traces generated by each process. Concurrent execution of threads is defined inductively in Rule 33. The base case, an empty multi-set of threads, is defined by Rule 34.

\frac{Π_{1}^{1} ⟹^{t_{1}} Π_{2}^{1} ⋯ Π_{1}^{k} ⟹^{t_{k}} Π_{2}^{k}}{(Π_{1}^{1}, …, Π_{1}^{k}) ⟹^{t_{1}∥···∥t_{k}} (Π_{2}^{1}, …, Π_{2}^{k})}  (32)

\frac{T_{1} ⟹^{t_{1}} T_{3}  \overline{\overline{T_{2}}} ⟹^{t_{2}} \overline{\overline{T_{4}}}}{T_{1} ⊎ \overline{\overline{T_{2}}} ⟹^{t_{1}∥t_{2}} T_{3} ⊎ \overline{\overline{T_{4}}}}  (33)

\overline{∅ ⟹^{ϵ} ∅}  (34)

Figure 19: Concurrent Execution of Processes and Threads.

Machine State  M  ::=  \overline{Π}^{k}
Process  Π  ::=  (H, C , \overline{\overline{T}} )
Thread  T  ::=  (E, ES, RS)
Trace  t  ::=  ϵ | t_{1} ; t_{2} | t_{1} ∥ t_{2} | cn ! m | cn ? m
Message  m  ::=  (p) | (l, p) | (E)
Heap  H  ::=  (TH , VH )
Cache  C  ::=  (TC , VC )
Type Heap  TH  ::=  p ↦^{map} ty
Type Cache  TC  ::=  p ↦^{map} ty
Heap Types  ty  ::=  tn | tn(p) |
\overline{p}^{k} | p_{1} → p_{2} |
tv | ∀ \overline{p_{1}} ^{k} . p_{2}
Value Heap  VH  ::=  l ↦^{map} val
Value Cache  VC  ::=  l ↦^{map} val
Heap Values  val  ::=  scon | cn | con | con(l) |

\overline{l}^{k} | ⟨⟨E, \overline{lv}^{k}, Λ⟩⟩ | Ω

Environment  E  ::=  (TE, NE, CE, VE)
Type Env.  TE  ::=  \overline{\overline{tn}}
Channel Env.  NE  ::=  \overline{\overline{cn}}
Constructor Env.  CE  ::=  con ↦^{map} p
Variable Env.  VE  ::=  lv ↦^{map} (l, p)
Exception Stack  ES  ::=  () | (l, p)·ES
Result Stack  RS  ::=  () | p·RS | (l, p)·RS | E·RS

Figure 20: DMΛ Abstract Machine Syntax.

The memory of each process is represented by the heap H and the cache C. With reference to Figure 16, the area of the virtual address space which corresponds to the area managed by the process is represented by the heap. The remainder of the virtual address space is represented by the cache. The allocation of heap values and types is performed in two stages in the DMΛ machine. H ↑ l returns the next available heap location in H, and H[l ↦ val] allocates val on the heap and binds it to the location l. Similarly, H ↑ p returns the next available type-pointer, and H[p ↦ ty] allocates ty on the heap bound to the pointer p. Thus, heap locations and type-pointers may effectively be reserved before being used. Data is allocated on the cache in a single step, e.g. C[l ↦ val] allocates val in the cache at location l. Cache locations and pointers do not need to be reserved as they correspond directly to locations and pointers in the heaps (it is assumed that heap locations and pointers belonging to different heaps are distinct).

4.2 Data Caching

The caching mechanisms of the LEMMA interface are formalised by the rules in Figures 21 and 22. In order for these mechanisms to be effective, all memory accesses in the DMΛ machine are done via a fetch function. The arguments to this function are either a type-pointer p or a pair (l, p).

The rules are defined via transitions between machine states of the form (Π^{1}, …, Π^{k}). Each of the rules is defined for a single fetch operation within a single thread n on a process Π^{i}, where 0 < i ≤ k. The rules utilise the functions num(p) and num(l) which return the number of the process whose heap contains the type-pointer p or heap-location l respectively. The mutable(p) predicate determines if a pointer p references a mutable type. In an implementation, the heap is typically divided into mutable and immutable areas. Thus, this predicate may be implemented by simply examining the address of the pointer.

The fetch(p) function returns the type referenced by the type-pointer p. This function is defined in Figure 21 by four rules corresponding to the following cases. The type may be local, i.e. contained within the heap of the parent process, in which case it is accessed directly (Rule 35). The type may be nonlocal and mutable in which case, it is accessed remotely in-place (Rule 36). The type may be remote, but a local copy may exist in the cache, in which case the cached version is accessed (Rule 37). Finally, if the type is remote and immutable, and a copy is not present in the cache, then a local copy is made (Rule 38).

num(p) = i

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T^{i}}}), …, Π^{k}) ⟹^{ϵ}

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, H^{i}(p)·RS^{n}) ⊎ \overline{\overline{T^{i}}}), …, Π^{k})

(35)

num(p) = j  j ≠ i  mutable(p)

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T^{i}}}), …

(H^{j}, C^{j}, \overline{\overline{T^{j}}}), …, Π^{k}) ⟹^{ϵ}

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, H^{j}(p)·RS^{n}) ⊎ \overline{\overline{T^{i}}}), …

(H^{j}, C^{j}, \overline{\overline{T^{j}}}), …, Π^{k})

(36)

num(p) = j  j ≠ i  ¬mutable(p)  p ∈ Dom C^{i}

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T^{i}}}), …, Π^{k}) ⟹^{ϵ}

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, C^{i}(p)·RS^{n}) ⊎ \overline{\overline{T^{i}}}), …, Π^{k})

(37)

num(p) = j  j ≠ i  ¬mutable(p)  p ∉ Dom C^{i}  H^{j}(p) = ty

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T^{i}}}), …

(H^{j}, C^{j}, \overline{\overline{T^{j}}}), …, Π^{k}) ⟹^{ϵ}

(Π^{1}, …, (H^{i}, C^{i}[p ↦ ty], (E^{n}, ES^{n}, ty·RS^{n}) ⊎ \overline{\overline{T^{i}}}), …

(H^{j}, C^{j}, \overline{\overline{T^{j}}}), …, Π^{k})

(38)

Figure 21: Type Heap Caching.

The fetch(l, p) function is described in Figure 22. The function returns a pair (val, ty) containing the value and the type corresponding to the location and pointer of the arguments. Once again, this operation is defined by four rules, corresponding to the four cases described previously: local, mutable, cached, and remote. The rules are slightly more complex as the type must first be obtained via a call to fetch(p) before the value is retrieved.

num(l) = i

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, ty·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(l, p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, (H_{2}^{i}(l), ty)·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(39)

num(l) = j  j ≠ i  mutable(p)

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, ty·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …

(H_{1}^{j}, C_{1}^{j}, \overline{\overline{T_{1}^{j}}}), …, Π_{2}^{k}) H_{1}^{j}(l) = val

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(l, p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, (val, ty)·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …

(H_{1}^{j}, C_{1}^{j}, \overline{\overline{T_{1}^{j}}}), …, Π_{2}^{k})

(40)

num(l) = j  j ≠ i  ¬mutable(p)  l ∈ Dom C_{1}^{i}

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, ty·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k}) C_{2}^{i}(l) = val

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(l, p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, (val, ty)·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(41)

num(l) = j  j ≠ i  ¬mutable(p)  l ∉ Dom C_{1}^{i}

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E^{n}, ES^{n}, ty·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …

(H_{1}^{j}, C_{1}^{j}, \overline{\overline{T_{1}^{j}}}), …, Π_{2}^{k}) H_{1}^{j}(l) = val

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ES^{n}, RS^{n}, fetch(l, p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}[l ↦ val], (E^{n}, ES^{n}, (val, ty)·RS^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …

(H_{1}^{j}, C_{1}^{j}, \overline{\overline{T_{1}^{j}}}), …, Π_{2}^{k})

(42)

Figure 22: Value Heap Caching.

4.3 Concurrency and Communication

The dynamic semantics of the complete MΛ language are formalised by transitions between states of the distributed abstract machine. As with the caching rules, the transitions are defined for a single thread n executing on a process Π^{i}, where 0 < i ≤ k.

The initial state of the DMΛ abstract machine is illustrated in Figure 23. Evaluation begins with a single process Π^{1}, containing the initial heap H^{1}, and a single thread (E^{1}, (), (), P), containing the initial environment E^{1} and the program program P. The remaining processes Π^{2} ⋯ Π^{k} remain idle, with an empty heap and multi-set of threads, until an rfork is performed by the program.

M = (Π^{1}, (∅, ∅, ∅)^{2}, …, (∅, ∅, ∅)^{k})
Π^{1} = (H^{1}, ∅, {(E^{1}, (), (), P)})
H^{1} = (TH , ∅)
TH = {p_{1} ↦ t unit → t bool,

p_{2} ↦ tv^{1}, p_{3} ↦ ∀ (p_{2}) . t unit → t list(p_{2}),

p_{4} ↦ tv^{2}, p_{5} ↦ ∀ (p_{4}) . (p_{4}, t list(p_{4})) → t list(p_{4}), p_{6} ↦ tv^{3}, p_{7} ↦ ∀ (p_{6}) . p_{6} → t ref(p_{6}), p_{8} ↦ t unit → t exn}

E^{1} = (TE, ∅, CE, ∅)
TE = {t unit, t int, t word, t real, t char, t string, t bool,

t list, t ref, t exn, t chan}

CE = {c true ↦ p_{1}, c false ↦ p_{1},

c nil ↦ p_{3}, c cons ↦ p_{5}, c ref ↦ p_{7},

e match ↦ p_{8}, e bind ↦ p_{8}}

Figure 23: Initial Machine State.

There is a relatively straightforward conversion from the transitions of the MΛ machine to the DMΛ machine. This conversion is performed via the templates illustrated in Figure 24.

The first template (43) is used to convert an MΛ program into a DMΛ program. A MΛ heap H becomes a DMΛ heap H^{i}. Similarly, am MΛ environment E becomes a DMΛ environment E^{n}, etc. The templates for datatypes and exceptions are essentially identical and are not given here. The template for expressions (44) is also very similar.

Owing to the shared-memory model of the DMΛ machine, MΛ memory accesses must be converted into calls to the fetch function. This is achieved simply using the templates (45) and (46). There is one slight complication in that a garbage collection can now occur during a fetch operation. Therefore, some additional saving and restoring on the result stack is required to ensure that all pointers will be collected. This is illustrated in the example below.

With a little work, these templates can be used to convert all of the MΛ rules in Appendix A into their DMΛ counterparts. For brevity, this is left as an exercise for the reader. The conversion simply involves renumbering the heaps, stacks, etc. and ensuring that type-pointers and value-locations are saved and restored on the result stack around instances of the fetch operation.

MΛ : (H_{1}, E_{1}, ES_{1}, RS_{1}, P) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2})
DMΛ : (Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, P) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}
(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(43)

MΛ : (H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l, p)·RS_{2})
DMΛ : (Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, Λ) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}
(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (l, p)·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(44)

MΛ : H_{1}(p) = ty
DMΛ : (Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, fetch(p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t}
(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (ty)·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(45)

MΛ : H_{1}(p) = ty  H_{1}(l) = val
DMΛ : (Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, fetch(l, p)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k})

⟹^{t} (Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (val, ty)·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(46)

Figure 24: Conversion Templates from MΛ to DMΛ.

As an example, the MΛ app expression (Rule 101) is converted into the DMΛ abstract machine according to Figure 25. Note the sequential composition of the evaluation traces for the subexpressions: t_{1} ; t_{2} ; t_{3} ; t_{4}. This must be performed for all of the rules in the sequential sub-language.

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, Λ_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t_{1}}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}, Λ_{2}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k}) ⟹^{t_{2}}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, (l_{2}, p_{2})·(l_{1}, p_{1})·RS_{3}^{n}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k}) (Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, (l_{2}, p_{2})·RS_{3}^{n}, fetch(l_{1}, p_{1})) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k})

⟹^{t_{3}} (Π_{4}^{1}, …, (H_{4}^{i}, C_{4}^{i}, (E_{4}^{n}, ES_{4}^{n},

(⟨⟨E_{c}, lv, Λ_{c}⟩⟩, ty)·(l_{3}, p_{3})·RS_{4}^{n}) ⊎ \overline{\overline{T_{4}^{i}}}), …, Π_{4}^{k}) (Π_{4}^{1}, …, (H_{4}^{i}, C_{4}^{i}, (E_{c}[lv ↦ (l_{3}, p_{3})], ES_{4}^{n}, E_{4}^{n}·RS_{4}^{n}, Λ_{c}) ⊎ \overline{\overline{T_{4}^{i}}}), …, Π_{4}^{k})

⟹^{t_{4}} (Π_{5}^{1}, …, (H_{5}^{i}, C_{5}^{i}, (E_{5}^{n}, ES_{5}^{n}, (l_{4}, p_{4})·E_{6}·RS_{4}^{n}) ⊎ \overline{\overline{T_{5}^{i}}}), …, Π_{5}^{k})

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, app (Λ_{1}, Λ_{2})) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k})

⟹^{t_{1} ; t_{2} ; t_{3} ; t_{4}} (Π_{5}^{1}, …, (H_{5}^{i}, C_{5}^{i}, (E_{6}, ES_{5}^{n}, (l_{4}, p_{4})·RS_{5}^{n}) ⊎ \overline{\overline{T_{5}^{i}}}), …, Π_{5}^{k})

(47)

Figure 25: Function Application in DMΛ.

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, Λ) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t_{1}}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (l_{1}, p_{1})·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}, fetch(l_{1}, p_{1})) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k}) ⟹^{t_{2}}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, (⟨⟨E_{c}, lv, Λ_{c}⟩⟩, ty)·RS_{3}^{n}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k})

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, fork(Λ)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t_{1} ; t_{2}}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, (l_{unit}, p_{unit})·RS_{3}^{n}) ⊎ (E_{c}, ∅, ∅, Λ_{c}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k})

(48)

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, Λ_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t_{1}}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (l_{1}, p_{1})·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}, fetch(l_{1}, p_{1})) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k}) ⟹^{t_{2}}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, RS_{3}^{n}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k})

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, RS_{3}^{n}, Λ_{2}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k}) ⟹^{t_{3}}

(Π_{4}^{1}, …, (H_{4}^{i}, C_{4}^{i}, (E_{4}^{n}, ES_{4}^{n}, (l_{2}, p_{2})·(j, ty_{1})·RS_{4}^{n}) ⊎ \overline{\overline{T_{4}^{i}}}), …, Π_{4}^{k})

(Π_{4}^{1}, …, (H_{4}^{i}, C_{4}^{i}, (E_{4}^{n}, ES_{4}^{n}, RS_{4}^{n}, fetch(l_{2}, p_{2})) ⊎ \overline{\overline{T_{4}^{i}}}), …, Π_{4}^{k}) ⟹^{t_{4}}

(Π_{5}^{1}, …, (H_{5}^{i}, C_{5}^{i}, (E_{5}^{n}, ES_{5}^{n}, (⟨⟨E_{c}, lv, Λ_{c}⟩⟩, ty_{2})·RS_{5}^{n}) ⊎ \overline{\overline{T_{5}^{i}}}), … (H^{j}, C^{j}, \overline{\overline{T^{j}}}), …, Π_{5}^{k})

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, rfork(Λ_{1}, Λ_{2})) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k})

⟹^{t1 ; t_{2} ; t_{3} ; t_{4}}

(Π_{5}^{1}, …, (H_{5}^{i}, C_{5}^{i}, (E_{5}^{n}, ES_{5}^{n}, (l_{unit}, p_{unit})·RS_{5}^{n}) ⊎ \overline{\overline{T_{5}^{i}}}), … (H^{j}, C^{j}, (E_{c}, ∅, ∅, Λ_{c}) ⊎ \overline{\overline{T^{j}}}), …, Π_{5}^{k})

(49)

\begin{matrix}(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E^{n}, ∅, ∅, (l_{unit}, p_{unit})) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{ϵ} \\ (Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) \end{matrix}  (50)

Figure 26: Concurrency.

It therefore remains to provide a definition for the communication and concurrency primitives which do not appear in the sequential sub-language. Concurrency is introduced into the language by the rules in Figure 26. The fork(Λ) expression creates a new thread on the local process Π^{i}. The Λ expression is evaluated to obtain a closure ⟨⟨E_{c}, lv, Λ_{c}⟩⟩. This closure is simply converted into a new thread (E_{c}, ∅, ∅, Λ_{c}) and appended to the local multi-set of threads. The rfork(Λ_{1}, Λ_{2}) expression creates a new thread on a remote process Π^{j}. The expression Λ_{1} is first evaluated to determine the remote process number j. Λ_{2} is then evaluated to provide a closure, which is again converted to a thread, and appended to the multi-set of threads on process Π^{j}. When a thread has finished execution, it has the form: (E^{n}, ∅, ∅, (l_{unit}, p_{unit})). Such threads are identified by Rule 50 and removed from the multi-set of threads.

cn fresh

(Π^{1}, …, (H^{i}, C^{i}, (E^{n}, ES^{n}, RS^{n}, channel()) ⊎ \overline{\overline{T^{i}}}), …, Π^{k}) ⟹^{ϵ}

(Π^{1}, …, (H^{i}[l ↦ cn][p ↦ t chan], C^{i}, (E^{n}[cn ↦ (l, p)], ES^{n}, (l, p)·RS^{n}) ⊎ \overline{\overline{T^{i}}}), …, Π^{k})

(51)

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, Λ_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t_{1}}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (l_{1}, p_{1})·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}, fetch(l_{1}, p_{1})) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k}) ⟹^{t_{2}}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, RS_{3}^{n}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k})

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, RS_{3}^{n}, Λ_{2}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k}) ⟹^{t_{3}}

(Π_{4}^{1}, …, (H_{4}^{i}, C_{4}^{i}, (E_{4}^{n}, ES_{4}^{n}, (l_{2}, p_{2})·(cn, ty)·RS_{4}^{n}) ⊎ \overline{\overline{T_{4}^{i}}}), …, Π_{4}^{k}) cn ! (l_{2}, p_{2})

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, send(Λ_{1}, Λ_{2})) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k})

⟹^{t_{1} ; t_{2} ; t_{3} ; cn ! (l_{2}, p_{2})}

(Π_{4}^{1}, …, (H_{4}^{i}, C_{4}^{i}, (E_{4}^{n}, ES_{4}^{n}, (l_{unit}, p_{unit})·RS_{4}^{n}) ⊎ \overline{\overline{T_{4}^{i}}}), …, Π_{4}^{k})

(52)

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, Λ) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k}) ⟹^{t_{1}}

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, (l_{1}, p_{1})·RS_{2}^{n}) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k})

(Π_{2}^{1}, …, (H_{2}^{i}, C_{2}^{i}, (E_{2}^{n}, ES_{2}^{n}, RS_{2}^{n}, fetch(l_{1}, p_{1})) ⊎ \overline{\overline{T_{2}^{i}}}), …, Π_{2}^{k}) ⟹^{t_{2}}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, (cn, ty)·RS_{3}^{n}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k}) cn ? (l_{2}, p_{2})

(Π_{1}^{1}, …, (H_{1}^{i}, C_{1}^{i}, (E_{1}^{n}, ES_{1}^{n}, RS_{1}^{n}, receive(Λ)) ⊎ \overline{\overline{T_{1}^{i}}}), …, Π_{1}^{k})

⟹^{t_{1} ; t_{2} ; cn ? (l_{2}, p_{2})}

(Π_{3}^{1}, …, (H_{3}^{i}, C_{3}^{i}, (E_{3}^{n}, ES_{3}^{n}, (l_{2}, p_{2})·RS_{3}^{n}) ⊎ \overline{\overline{T_{3}^{i}}}), …, Π_{3}^{k})

(53)

Figure 27: Communication.

Communication between threads is performed across bi-directional channels. New channels are created by the channel() expression (Rule 51). With reference to Figure 20, the channel environment NE tracks the allocation of channel names. A channel is represented in the heap as a value cn of type t chan.

Channels communicate pairs of value-locations and type-pointers (l, p). These pairs are sent along channels by the send(Λ_{1}, Λ_{2}) expression (Rule 52) and received by the receive(Λ) expression (Rule 53). The channel along which communication takes place is provided by evaluating Λ_{1} in the case of a send, or Λ in the case of receive. The second argument Λ_{2} of a send is evaluated to provide the pair (l, p). The communication operations are blocking. Both the sending and receiving threads are blocked until the pair (l, p) is passed, which happens atomically. The notation for sending and receiving across channels is the same as the communication traces. For example, sending the pair (l, p) across channel cn is written cn ! (l, p).

Concurrent ML:

let val c = channel()
    val   = rfork(2, fn () => send(c, receive(c) + 3))
    val   = send(c, 7)
in
    receive(c)
end

DMΛ Translation:

(∅, ∅,

let (c, t unit) = channel ()  (i)

in

let ( , t unit) = rfork (scon 2,

fn ( , t unit → t unit) =

send (var c, prim (ADD_{i}, (receive (var c), scon 3))))  (ii)

in

let ( , t unit) = send (var c, scon 7)  (iii)

in

receive(var c))  (iv)

Simplified Evaluation Trace:

(i)  ϵ
(ii)  ϵ ∥ (c ? (l_{1}, p_{1}) ; c ! (l_{2}, p_{2}))
(iii)  (ϵ ; c ! (l_{1}, p_{1})) ∥ (c ? (l_{1}, p_{1}) ; c ! (l_{2}, p_{2}))
(iv)  (ϵ ; c ! (l_{1}, p_{1}) ; c ? (l_{2}, p_{2})) ∥ (c ? (l_{1}, p_{1}) ; c ! (l_{2}, p_{2}))

Trace Reduction:

(ϵ ; c ! (l_{1}, p_{1}) ; c ? (l_{2}, p_{2})) ∥ (c ? (l_{1}, p_{1}) ; c ! (l_{2}, p_{2}))
= (c ! (l_{1}, p_{1}) ; c ? (l_{2}, p_{2})) ∥ (c ? (l_{1}, p_{1}) ; c ! (l_{2}, p_{2}))  by Rule 27
= c ? (l_{2}, p_{2}) ∥ c ! (l_{2}, p_{2})  by Rule 31
= c ! (l_{2}, p_{2}) ∥ c ? (l_{2}, p_{2})  by Rule 29
= ϵ  by Rule 30

Figure 28: Trace Reduction Example.

Earlier in this section (4.1) it was stated that the traces for a correct program should always reduce to ϵ. Having now provided the transitions for the communication and concurrency primitives, Figure 28 shows that this is the case for the example given in the introduction. For clarity, the traces have been simplified by removing all the ϵ traces resulting from the intermediate steps in the evaluation. The first pair that is transmitted across the channel c, corresponding to the special constant 7, is denoted (l_{1}, p_{1}). The second pair, corresponding to the special constant 10 (7+3), is denoted (l_{2}, p_{2}).

4.4 Distributed Garbage Collection

In this section an abstract machine is presented which describes the distributed garbage collection algorithm. The syntax of this abstract machine, called the DGC machine, is given in Figure 29.

Machine State GC ::= \overline{π}^{k}
GC Process  π  ::= (Hf , Ht, PF , LF , \overline{\overline{T}})
GC Thread  T  ::= E | S | cn_{l} | cn_{p} | (p_{1}, p_{2}) | (l_{1}, p_{1}, l_{2})
Trace  t  ::= ϵ | t_{1} ; t_{2} | t_{1} ∥ t_{2} | cn ! m | cn ? m
Message  m ::= (p) | (l, p) | (E)

Figure 29: DGC Abstract Machine Syntax.

The organisation of DGC machine is very similar to the DMΛ machine. There are a fixed number k of concurrently executing processes π each executing a multi-set of threads T. This similarity is intended. There is a one-to-one correspondence between DGC processes and DMΛ processes. In an actual implementation the two machines would be combined. The combined machine would alternate between the execution of DMΛ and DGC processes and threads during cycles of program execution and garbage collection. Figure 30 defines the parallel execution of garbage collection processes and threads.

\frac{π_{1}^{1} ⟹^{t_{1}}_{gc} π_{2}^{1} ⋯ π_{1}^{k} ⟹^{t_{k}}_{gc} π_{2}^{k}}{(π_{1}^{1}, …, π_{1}^{k}) ⟹^{t_{1}∥···∥t_{k}}_{gc} (π_{2}^{1}, …, π_{2}^{k})}  (54)

\frac{T_{1} ⟹^{t_{1}}_{gc} T_{3}  \overline{\overline{T_{2}}} ⟹^{t_{2}}_{gc} \overline{\overline{T_{4}}}}{T_{1} ⊎ \overline{\overline{T_{2}}} ⟹^{t_{1}∥t_{2}}_{gc} T_{3} ⊎ \overline{\overline{T_{4}}}}  (55)

Figure 30: Execution of DGC Processes and Threads.

Each DGC process is effectively a separate copy of the uniprocessor algorithm. Therefore, each process contains a copy of the GC state as defined in Figure 10. There are separate threads for garbage collecting environments, stacks, values, and types. Environments are garbage collected using E threads and stacks are garbage collected using S threads. The garbage collection of types and values is more complex. Recall from the description of the distributed garbage collection algorithm, at the beginning of this section, that each process is responsible for garbage collecting data that is contained within its own heap. Thus, in the DGC machine a mechanism is required for communicating pointers to the appropriate processes for collection. This is achieved through the use of server threads. Each DGC process has two server threads: one for types and one for values. Each of these server threads has an associated channel along which messages are sent and received. Hence, the server threads are named cn_{l}^{i} and cn_{p}^{i}, where 0 < i ≤ k. When an external pointer is encountered during garbage collection, it is simply sent along a channel to the appropriate server thread which returns an updated pointer along the same channel.

The server thread is determined using the num operation defined in Section 4.2. For example, a type referenced by the pointer p_{1} is garbage collected by sending it to a server, where i = num(p_{1}): cn_{p}^{i} ! (p_{1}). The updated pointer p_{2} is subsequently retrieved from the same server: cn_{p}^{i} ? (p_{2}). For convenience, these operations are combined in the garbage collection rules e.g. cn_{p}^{i} ! (p_{1}) ? (p_{2}), which is shorthand for cn_{p}^{i} ! (p_{1}) ; cn_{p}^{i} ? (p_{2}). In order to simplify the garbage collection rules, a distinction is not made between local and remote data. All type-pointers and value-locations are sent in this manner to the servers, even if the server is on the same process. It would be straightforward to optimise the local case, but the number of rules would double.

It may be the case that two (or more) threads attempt to communicate with a single server thread at the same time. In this case, the server makes a non-deterministic choice between the threads. Only one thread is permitted to communicate with the server. The remaining threads are blocked until the server becomes available. Communication with the server is always done by performing a send operation followed by a receive. This ordering ensures that the correct thread receives the reply from the server.

The server threads do not actually perform garbage collection. A copying operation may require the co-operation of a number of other servers. This could easily lead to a deadlock owing to the blocking nature of the communication channel, e.g. two servers may become blocked waiting for each other to finish. One solution would be to fork a new server thread every time the server becomes busy. However, each of these server threads would require a separate communication channel which would considerably complicate the collection algorithm.

The solution adopted here involves the use of worker threads to perform the copying operation. Recall from Section 4.1 that a pointer may be reserved on the heap. Thus, the server thread simply reserves and returns a pointer while a separate worker thread is forked to copy the data. A worker thread for copying a value is denoted (l_{1}, p_{1}, l_{2}). The value referenced by l_{1} is copied recursively into the location referenced by l_{2} using the type reference by p_{1}. Similarly, a worker thread for copying a type is denoted (p_{1}, p_{2}). The type referenced by p_{1} is copied recursively into the heap referenced by p_{2}.

The rule in Figure 32 illustrates how distributed garbage collection is combined with the rules of the DMΛ abstract machine. This rule generates a single DGC process from a single DMΛ process. Distributed garbage collection requires this operation to be performed on every process in the DMΛ machine. The set of garbage collection threads (roots) for a single DGC process is generated from the union of all the environments and stacks contained within the threads of a DMΛ process. The set of threads also includes the value and type servers for processing external references.

Garbage collection proceeds until all of the roots have been processed. The set of DMΛ threads is then rebuilt with the new environments and stacks and normal evaluation is resumed. Note that the contents of the cache is cleared by garbage collection.

An example distributed garbage collection with two processes is illustrated in Figure 31. In the example, an integer list type is garbage collected. Initially, the list type t list is referenced by the type-pointer p_{1} and is contained within the from heap of process π^{1}. The list type contains a pointer p_{2} to the integer type t int contained within the from heap of process π^{2}.

Garbage collection is initiated by sending the pointer p_{1} to the server thread cn_{p}^{1} on process π^{1}. The server thread reserves a pointer p_{3} on the to heap of process π^{1} and returns this pointer. A worker thread (p_{1}, p_{3}) is created to perform the copy of the list type. During the copy operation, the worker thread encounters the pointer p_{2} to the integer type. This pointer is sent to the server thread cn_{p}^{2} on process π^{2}. The server thread subsequently reserves a pointer p_{4} on the to heap of process π^{2} and returns this to the worker thread. Now a new worker thread (p_{2}, p_{4}) is created on process π^{2} to perform the copy of the integer type. Meanwhile, the worker thread on process π^{1} completes the copy of the list type with the updated pointer p_{4}. Once the worker thread on process π^{2} has completed the copy of the integer type, the garbage collection is complete. The type-pointer p_{3} references the garbage collected type in the to heap of process π^{1}.

p1 ^{t list(p2)}^{t int}^{p2}  ^{p4}^{p3}^{p3} cn cn^{p}^{1}^{p}^{2}^{from heap}^{from heap}  ^{(p1, p3)}  ^{t list(p4)}^{t int}^{p4}  ^{to heap}^{to heap}^{(p2, p4)}^{p2}^{p1} π^{2} π^{1}

Figure 31: Distributed Garbage Collection Example.

\overline{\overline{T_{1}^{i}}} = \{(E_{1}^{1}, ES_{1}^{1}, RS_{1}^{1}), …, (E_{1}^{j}, ES_{1}^{j}, RS_{1}^{j})\} (π_{1}^{1}, …, (H_{1}^{i}, ∅, ∅, ∅, E_{1}^{1} ⊎ ES_{1}^{1} ⊎ RS_{1}^{1} ⊎ ⋯

⋯ ⊎ E_{1}^{j} ⊎ ES_{1}^{j} ⊎ RS_{1}^{j} ⊎ cn_{l} ⊎ cn_{p}), …, π_{1}^{k}) ⟹^{t}_{gc}

(π_{2}^{1}, …, (H_{1}^{i}, H_{2}^{i}, PF^{i}, LF^{i}, E_{2}^{1} ⊎ ES_{2}^{1} ⊎ RS_{2}^{1} ⊎ ⋯

⋯ ⊎ E_{2}^{j} ⊎ ES_{2}^{j} ⊎ RS_{2}^{j} ⊎ cn_{l} ⊎ cn_{p}), …, π_{2}^{k})

\overline{\overline{T_{2}^{i}}} = \{(E_{2}^{1}, ES_{2}^{1}, RS_{2}^{1}), …, (E_{2}^{j}, ES_{2}^{j}, RS_{2}^{j})\}

(Π^{1}, …, (H_{1}^{i}, C_{1}^{i}, \overline{\overline{T_{1}^{i}}}), …, Π^{k}) ⟹^{t} (Π^{1}, …, (H_{2}^{i}, ∅, \overline{\overline{T_{2}^{i}}}), …, Π^{k})

(56)

Figure 32: Distributed Garbage Collection Introduction.

Figures 33 through 37 define the behaviour of the garbage collection threads. It is worth noting that these rules are very similar to their sequential equivalents in Figures 12 through 15. Where the sequential algorithm collects a pointer (Hf , Ht_{1}, PF_{1}, LF , p_{1}) ⇒_{gc} (Hf , Ht_{2}, PF_{2}, LF , p_{2}), the distributed algorithm communicates with a server cn_{p}^{num(p_{1})} ! (p_{1}) ? (p_{2}). A sequential collection effectively corresponds to a single garbage collection process collecting a single DMΛ process in the DGC machine.

The server thread for types cn_{p} is defined in Figure 33. In Rule 57, the type referenced by p_{1} has already been collected. The entry in the forwarding table PF (p_{1}) is therefore returned. In Rule 58 the type has not been collected. A pointer p_{2} is reserved in Ht, to hold the collected type, and returned. A worker thread (p_{1}, p_{2}) is created to copy the type, and a mapping p_{1} ↦ p_{2} is added to the forwarding table. Note that the server is still present in the set of threads at the end of the rule. This has the effect of restarting the server. The server thread for values cn_{l} is defined in Figure 35.

The worker thread for types (p_{1}, p_{2}) is defined in Figure 34. There are separate rules for each of the types in the language. Any type pointers that are encountered are collected by sending them to the appropriate type server. The heap is accessed directly, instead of going via the fetch operation, as the types will always be contained within the local heap. The worker thread for values (l_{1}, p_{1}, l_{2}) is defined in Figure 35. There are separate rules for each of the values in the language. The type information referenced by p_{1} is used to guide the collection, but the type itself is not collected by these rules. Any value locations that are encountered are sent to the appropriate value server.

The thread for collecting environments is given in Figure 37. The environment E_{1} is decomposed into a constructor environment CE_{1}, and a value environment V E_{1}. A new constructor environment CE_{2} is built by collecting all of the types referenced in CE_{1}. This is achieved by sending all of the type references to the type servers. Similarly, a new value environment V E_{2} is built by collecting all of the values and types referenced in V E_{1}. This is achieved by sending all of the references to the type and value servers. A new environment E_{2} is built from CE_{2}, and V E_{2}.

The final Figure 38 contains the rules for garbage collecting the stacks ES and RS. There are separate rules depending on wether the item at the top of the stack is a type (Rule 74), a value (Rule 75), or an environment (Rule 76). The base case, an empty stack, is handled by Rule 73.

t_{1} = cn_{p}^{i} ? (p_{1})  p_{1} ∈ Dom PF^{i}  p_{2} = PF^{i}(p_{1})  t_{2} = cn_{p}^{i} ! (p_{2})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (cn_{p}^{i}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (cn_{p}^{i}) ⊎ \overline{\overline{T^{i}}}), …, π^{k})

(57)

t_{1} = cn_{p}^{i} ? (p_{1}) p_{1} ∉ Dom PF^{i} Ht^{i} ↑ p_{2} t_{2} = cn_{p}^{i} ! (p_{2})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (cn_{p}^{i}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}[p_{1} ↦ p_{2}], LF^{i}, (cn_{p}^{i}) ⊎ (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k})

(58)

Figure 33: Type Server Thread.

Hf^{i}(p_{1}) = tn

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⇒^{ϵ}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[p_{2} ↦ tn], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(59)

Hf^{i}(p_{1}) = tn(p_{3}) t = cn_{p}^{num(p_{3})} ! (p_{3}) ? (p_{4})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[p_{2} ↦ tn(p_{4})], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(60)

Hf^{i}(p_{1}) = \overline{p_{3}} ^{n} t = cn_{p}^{num(p_{3}^{1})} ! (p_{3}^{1}) ? (p_{4}^{1}) ; ⋯; cn_{p}^{num(p_{3}^{n})} ! (p_{3}^{n}) ? (p_{4}^{n})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[p_{2} ↦ \overline{p_{4}} ^{n}], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(61)

Hf^{i}(p_{1}) = p_{3} → p_{4} t = cn_{p}^{num(p_{3})} ! (p_{3}) ? (p_{5}) ; cn_{p}^{num(p_{4})} ! (p_{4}) ? (p_{6})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[p_{2} ↦ p_{5} → p_{6}], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(62)

Hf^{i}(p_{1}) = tv

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⇒^{ϵ}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[p_{2} ↦ tv], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(63)

Hf^{i}(p_{1}) = ∀ \overline{p_{3}} ^{n}. p_{4} t_{1} = cn_{p}^{num(p_{3}^{1})} ! (p_{3}^{1}) ? (p_{5}^{1}) ; ⋯; cn_{p}^{num(p_{3}^{n})} ! (p_{3}^{n}) ? (p_{5}^{n}) t_{2} = cn_{p}^{num(p_{3})} ! (p_{4}) ? (p_{6})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (p_{1}, p_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[p_{1} ↦ ∀ \overline{p_{5}} ^{n}. p_{6}], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(64)

Figure 34: Type Worker Thread.

t_{1} = cn_{l}^{i} ? (l_{1}, p_{1})  l_{1} ∈ Dom LF^{i}  l_{2} = LF^{i}(l_{1})  t_{2} = cn_{l}^{i} ! (l_{2}, p_{1})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (cn_{l}^{i}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}[p_{1} ↦ p_{2}], LF^{i}, (cn_{l}^{i}) ⊎ \overline{\overline{T^{i}}}), …, π^{k})

(65)

t_{1} = cn_{l}^{i} ? (l_{1}, p_{1}) l_{1} ∉ Dom LF^{1} Ht^{i} ↑ l_{2} t_{2} = cn_{l}^{i} ! (l_{2}, p_{1})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (cn_{l}^{i}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}[l_{1} ↦ l_{2}], (cn_{l}^{i}) ⊎ (l_{1}, p_{1}, l_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k})

(66)

Figure 35: Value Server Thread.

Hf^{i}(p_{1}) = tn

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (l_{1}, p_{1}, l_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{ϵ}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[l_{2} ↦ Hf^{i}(l_{1})], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(67)

Hf^{i}(p_{1}) = tn(p_{2}) Hf^{i}(l_{1}) = con(l_{3}) t = cn_{l}^{num(l_{3})} ! (l_{3}, p_{2}) ? (l_{4}, p_{2})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (l_{1}, p_{1}, l_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[l_{2} ↦ con(l_{4})], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(68)

Hf^{i}(p_{1}) = \overline{p_{2}} ^{n} Hf^{i}(l_{1}) = \overline{l_{3}} ^{n} t = cn_{l}^{num(l_{3}^{1})} ! (l_{3}^{1}, p_{2}^{1}) ? (l_{4}^{1}, p_{2}^{1}) ; ⋯; cn_{p}^{num(l_{3}^{n})} ! (l_{3}^{n}, p_{2}^{n}) ? (l_{4}^{n}, p_{2}^{n})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (l_{1}, p_{1}, l_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[l_{2} ↦ (l_{4}^{1}, …, l_{4}^{n})], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(69)

Hf^{i}(p_{1}) = p_{2} → p_{3} Hf^{i}(l_{1}) = ⟨⟨E_{1}, \overline{lv}^{l}, Λ⟩⟩

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, E_{1} ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, E_{2} ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, (l_{1}, p_{1}, l_{2}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}[l_{2} ↦ ⟨⟨E_{2}, \overline{lv}^{l}, Λ⟩⟩], PF _{2}^{i}, LF _{2}^{i}, \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(70)

Hf^{i}(p_{1}) = p_{2} → p_{3} Hf^{i}(l_{1}) = Ω

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (l_{1}, p_{1}, l_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{ϵ}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}[l_{2} ↦ Ω], PF^{i}, LF^{i}, \overline{\overline{T^{i}}}), …, π^{k})

(71)

Figure 36: Value Worker Thread.

E_{1} = (TE, NE, CE_{1}, VE_{1}) CE_{1} = {con^{1} ↦ p_{1}^{1}, …, con^{k} ↦ p_{1}^{k}} t_{1} = cn_{p}^{num(p_{1}^{1})} ! (p_{1}^{1}) ? (p_{2}^{1}) ; ⋯; cn_{p}^{num(p_{1}^{k})} ! (p_{1}^{k}) ? (p_{2}^{k}) CE_{2} = {con^{1} ↦ p_{2}^{1}, …, con^{k} ↦ p_{2}^{k}} VE_{1} = {lv^{1} ↦ (l_{1}^{1}, p_{3}^{1}), …, lv^{l} ↦ (l_{1}^{l}, p_{5}^{l})} t_{2} = cn_{p}^{num(p_{3}^{1})} ! (p_{3}^{1}) ? (p_{4}^{1}) ; ⋯; cn_{p}^{num(p_{3}^{l})} ! (p_{3}^{l}) ? (p_{4}^{l}) t_{3} = cn_{l}^{num(l_{1}^{1})} ! (l_{1}^{1}, p_{4}^{1}) ? (l_{2}^{1}, p_{4}^{1}) ; ⋯; cn_{l}^{num(l_{1}^{l})} ! (l_{1}^{l}, p_{4}^{l}) ? (l_{2}^{l}, p_{4}^{l}) VE_{2} = {lv^{1} ↦ (l_{2}^{1}, p_{4}^{1}), …, lv^{l} ↦ (l_{2}^{l}, p_{4}^{l})} E_{2} = (TE, NE, CE_{2}, VE_{2})

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (E_{1}) ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{t_{1} ; t_{2} ; t_{3}}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, (E_{2}) ⊎ \overline{\overline{T^{i}}}), …, π^{k})

(72)

Figure 37: Environment Thread.

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, () ⊎ \overline{\overline{T^{i}}}), …, π^{k}) ⟹^{ϵ}_{gc}

(π^{1}, …, (Hf^{i}, Ht^{i}, PF^{i}, LF^{i}, () ⊎ \overline{\overline{T^{i}}}), …, π^{k})

(73)

t_{1} = cn_{p}^{num(p_{1})} ! (p_{1}) ? (p_{2})

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, (S_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t_{2}}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, (S_{2}) ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, (p_{1}·S_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, (p_{2}·S_{2}) ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(74)

t_{1} = cn_{p}^{num(p_{1})} ! (p_{1}) ? (p_{2}) t_{2} = cn_{l}^{num(l_{1})} ! (l_{1}, p_{1}) ? (l_{2}, p_{1})

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, (S_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t_{3}}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, (S_{2}) ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, ((l_{1}, p_{1})·S_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t_{1} ; t_{2} ; t_{3}}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, ((l_{2}, p_{2})·S_{2}) ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(75)

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, (E_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t_{1}}_{gc}

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, (E_{2}) ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k})

(π_{2}^{1}, …, (Hf _{2}^{i}, Ht_{2}^{i}, PF _{2}^{i}, LF _{2}^{i}, (S_{1}) ⊎ \overline{\overline{T_{2}^{i}}}), …, π_{2}^{k}) ⟹^{t_{2}}_{gc}

(π_{3}^{1}, …, (Hf _{3}^{i}, Ht_{3}^{i}, PF _{3}^{i}, LF _{3}^{i}, (S_{2}) ⊎ \overline{\overline{T_{3}^{i}}}), …, π_{3}^{k})

(π_{1}^{1}, …, (Hf _{1}^{i}, Ht_{1}^{i}, PF _{1}^{i}, LF _{1}^{i}, (E_{1}·S_{1}) ⊎ \overline{\overline{T_{1}^{i}}}), …, π_{1}^{k}) ⟹^{t_{1} ; t_{2}}_{gc}

(π_{3}^{1}, …, (Hf _{3}^{i}, Ht_{3}^{i}, PF _{3}^{i}, LF _{3}^{i}, (E_{2}·S_{2}) ⊎ \overline{\overline{T_{3}^{i}}}), …, π_{3}^{k})

(76)

Figure 38: Stack Thread.

5 Further Work and Concluding Remarks

Modern compilers for higher-order typed programming languages use typed intermediate languages to structure the compilation process. The use of such languages in this report has allowed the construction of efficient tag-free algorithms for both the sequential and distributed cases. In addition, the use of abstract machine notation has enabled a formal presentation of memory management separately from other aspects such as syntax and type-correctness. Unlike traditional models, the abstract machine exposes many important details such as the heap, stacks, and environments and provides an implementor with an unambiguous and precise description of memory management.

The use of type information also enables a number of extensions to the garbage collection algorithm. The model presented here only deals with heap garbage collection. However, space leaks in the heap may also result from stack and environment garbage. Stack garbage results from recursive tail-calls, and environment garbage results from unused bindings. As an example, Figure 39 illustrates the removal of unused bindings from closure environments. CON returns the set of constructors which appear in Λ, and VAR returns the set of variables which appear in Λ. Rule 77 is for the sequential case, and Rule 78 is for the distributed case. These rules could easily be combined with Rule 20 (sequential) and Rule 70 (distributed) to improve the efficiency of the garbage collection algorithms. The collection of stack garbage is a more complex problem and is currently under investigation.

CON (Λ) ⊆ Dom CE^{1} VAR(Λ) ⊆ Dom VE^{1} ⟨⟨(TE, CE^{1} ⊎ CE^{2}, VE^{1} ⊎ VE^{2}), \overline{lv}^{k}, Λ⟩⟩ ⇒_{gc}

⟨⟨(TE, CE^{1}, VE^{1}), \overline{lv}^{k}, Λ⟩⟩

(77)

CON (Λ) ⊆ Dom CE^{1} VAR(Λ) ⊆ Dom VE^{1} ⟨⟨(TE, NE, CE^{1} ⊎ CE^{2}, VE^{1} ⊎ VE^{2}), \overline{lv}^{k}, Λ⟩⟩ ⇒_{gc}

⟨⟨(TE, NE, CE^{1}, VE^{1}), \overline{lv}^{k}, Λ⟩⟩

(78)

Figure 39: Closure Garbage Collection.

The abstract machine model has also provided a definition for the mechanisms of the LEMMA memory interface. In order to clearly present the memory management operations, a number of simplifications have been made in the distributed case, e.g. mutable data is not cached. An obvious extension would be an inclusion of the optimisation techniques described in [12] and [14]. Beyond these optimisations, it would also be interesting to adapt the model to cope with wide-area distribution. In this setting, the intention would clearly be to minimise the amount of communication. Also, the model of distributed shared memory may be unrealistic and require a change to a purely messagepassing paradigm. It would also be necessary to cope with the presence of computation and communication failures. This may require some changes to the Concurrent ML primitives. For example, the addition of time-outs to the communication operations.

A Sequential Abstract Machine Definition

A.1 Programs

P = ({D^{1}, …, D^{k}}, {X^{1}, …, X^{l}}, Λ) (H_{1}, E_{1}, ES_{1}, RS_{1}, D^{1}) ⇒ (H_{2}, E_{2}, ES_{1}, RS_{1}) ⋯

(H_{k}, E_{k}, ES_{1}, RS_{1}, D^{k}) ⇒ (H_{k+1}, E_{k+1}, ES_{1}, RS_{1}) (H_{k+1}, E_{k+1}, ES_{1}, RS_{1}, X^{1}) ⇒ (H_{k+2}, E_{k+2}, ES_{1}, RS_{1}) ⋯

(H_{k+l}, E_{k+l}, ES_{1}, RS_{1}, X^{l}) ⇒ (H_{k+l+1}, E_{k+l+1}, ES_{1}, RS_{1}) (H_{k+l+1}, E_{k+l+1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{k+l+2}, E_{k+l+2}, ES_{2}, RS_{2}) (H_{1}, E_{1}, ES_{1}, RS_{1}, P) ⇒ (H_{k+l+2}, E_{k+l+2}, ES_{2}, RS_{2})

(79)

Comment: (Rule 79) The Program P is decomposed into datatypes D, exceptions X, and an expression Λ. These components are then evaluated in turn by sequences of transitions.

A.2 Datatype and Exception Declarations

(H, E, ES, RS, datatype tn of \overline{(con, τ)}^{k}) ⇒ (H[p_{1} ↦ τ^{1} → tn, …, p_{k} ↦ τ^{k} → tn], E[tn][con^{1} ↦ p_{1}, …, con^{k} ↦ p_{k}], ES, RS)

(80)

Comment: (Rule 80) Datatype constructors are represented as functions from the constructor argument type to the datatype name τ → tn. The type of a nullary constructor is t unit → tn. These function types are allocated on the type heap H[p ↦ τ → tn], and entered into the environment E[tn][con ↦ p].

(H, E, ES, RS, datatype (\overline{tv}^{k}, tn) of \overline{(con, τ)}^{l}) ⇒ (H[p_{1} ↦ ∀ \overline{tv}^{k}. τ^{1} → tn, …, p_{l} ↦ ∀ \overline{tv}^{k}. τ^{l} → tn], E[tn][con^{1} ↦ p_{1}, …, con^{l} ↦ p_{l}], ES, RS)

(81)

Comment: (Rule 81) Polymorphic datatype constructors are represented by functions ∀ \overline{tv}^{k}. τ → tn.

(H, E, ES, RS, exception (con, τ)) ⇒ (H[p ↦ τ → t exn], E[con ↦ p], ES, RS)

(82)

Comment: (Rule 82) The effect of an exception declaration is analogous to that of adding a constructor to a pre-defined datatype named t exn.

A.3 Values

(H, E, ES, RS, scon scon) ⇒ (H[l ↦ scon][p ↦ τ_{scon}], E, ES, (l, p)·RS)

(83)

Comment: (Rule 83) τ_{scon} is the type of the special constant scon (e.g. t int).

\frac{E(lv) = (l, p)}{(H, E, ES, RS, var lv) ⇒ (H, E, ES, (l, p)·RS)}  (84)

E(lv) = (l_{1}, p_{1}) (H_{1}[p_{2} ↦ \overline{τ}^{k}], E, ES, RS, instance(p_{1}, p_{2})) ⇒ (H_{2}, E, ES, p_{3}·RS) (H_{1}, E, ES, RS, var (\overline{τ}^{k}, lv)) ⇒ (H_{2}, E, ES, (l_{1}, p_{3})·RS)

(85)

(H, E, ES, RS, fn (lv, τ_{1} → τ_{2}) = Λ) ⇒ (H[l ↦ ⟨⟨E, lv, Λ⟩⟩][p ↦ τ_{1} → τ_{2}], E, ES, (l, p)·RS)

(86)

(H, E, ES, RS, fn (\overline{lv}^{k}, \overline{τ_{1}} ^{k} → τ_{2}) = Λ) ⇒ (H[l ↦ ⟨⟨E, \overline{lv}^{k}, Λ⟩⟩][p ↦ \overline{τ_{1}} ^{k} → τ_{2}], E, ES, (l, p)·RS)

(87)

Comment: (Rules 86 and 87) These rules allocate a new closure on the value heap. The second rule is for functions which take multiple arguments. The closure consists of a copy of the environment, a variables (or list of variables) to be bound to the function parameters, and an expression for the body of the function.

A.4 Constructors

\frac{E(con) = p_{1}  H(p_{1}) = p_{2} → p_{3}}{(H, E, ES, RS, con con) ⇒ (H[l_{1} ↦ con], E, ES, (l_{1}, p_{3})·RS)}  (88)

E(con) = p_{1} (H_{1}[p_{2} ↦ \overline{τ}^{k}], E, ES, RS, instance(p_{1}, p_{2})) ⇒ (H_{2}, E, ES, p_{3}·RS) H_{2}(p_{3}) = p_{4} → p_{5} (H_{1}, E, ES, RS, con (con, \overline{τ}^{k})) ⇒ (H_{2}[l_{1} ↦ con], E, ES, (l_{1}, p_{5})·RS)

(89)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) E_{2}(con) = p_{2} H_{2}(p_{2}) = p_{3} → p_{4} (H_{1}, E_{1}, ES_{1}, RS_{1}, con (con, Λ)) ⇒

(H_{2}[l_{2} ↦ con(l_{1})], E_{2}, ES_{2}, (l_{2}, p_{4})·RS_{2})

(90)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) E_{2}(con) = p_{2} (H_{2}[p_{3} ↦ \overline{τ}^{k}], E_{2}, ES_{2}, RS_{2}, instance(p_{2}, p_{3})) ⇒ (H_{3}, E_{2}, ES_{2}, p_{4}·RS_{2}) H_{3}(p_{4}) = p_{5} → p_{6} (H_{1}, E_{1}, ES_{1}, RS_{1}, con (con, \overline{τ}^{k}, Λ)) ⇒

(H_{3}[l_{2} ↦ con(l_{1})], E_{2}, ES_{2}, (l_{2}, p_{6})·RS_{2})

(91)

Comment: (Rules 88 to 91) Constructing a datatype value is analogous to applying the constructor function τ → tn (or an instance of ∀ \overline{tv}^{k}. τ → tn for polymorphic constructors). Unary constructors require an argument Λ of type τ. A new constructor value is allocated on the value heap with associated type tn in the type heap.

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) E_{2}(con) = p_{2} H_{2}(p_{2}) = p_{3} → p_{4} H_{2}(l_{1}) = con(l_{2}) (H_{1}, E_{1}, ES_{1}, RS_{1}, decon (con, Λ)) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{2}, p_{3})·RS_{2})

(92)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) E_{2}(con) = p_{2} (H_{2}[p_{3} ↦ \overline{τ}^{k}], E_{2}, ES_{2}, RS_{2}, instance(p_{2}, p_{3})) ⇒ (H_{3}, E_{2}, ES_{2}, p_{4}·RS_{2}) H_{3}(p_{4}) = p_{5} → p_{6} H_{3}(l_{1}) = con(l_{2}) (H_{1}, E_{1}, ES_{1}, RS_{1}, decon (con, \overline{τ}^{k}, Λ)) ⇒ (H_{3}, E_{2}, ES_{2}, (l_{2}, p_{5})·RS_{2})

(93)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{1}) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2}) (H_{2}, E_{2}, ES_{2}, RS_{2}, Λ_{2}) ⇒ (H_{3}, E_{3}, ES_{3}, (l_{2}, p_{2})·(l_{1}, p_{1})·RS_{3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, assign (Λ_{1}, Λ_{2})) ⇒

(H_{3}[l_{1} ↦^{upd} c ref(l_{2})], E_{3}, ES_{3}, (l_{unit}, p_{unit})·RS_{3})

(94)

Comment: (Rule 94) Assignment uses the update operation l_{1} ↦^{upd} c ref(l_{2}) to update the reference at l_{1} to c ref(l_{2})

A.5 Structured Expressions

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{1}) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) cmap = {c^{1} ↦ Λ_{2}^{1}, …, c^{k} ↦ Λ_{2}^{k}} H_{2}(l_{1}) = val Λ_{4} = if val ∈ Dom cmap then cmap(val) else Λ_{3} (H_{2}, E_{2}, ES_{2}, RS_{2}, Λ_{4}) ⇒ (H_{3}, E_{3}, ES_{3}, RS_{3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, switch Λ_{1} case (cmap, Λ_{3})) ⇒ (H_{3}, E_{3}, ES_{3}, RS_{3})

(95)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ^{1}) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2}) ⋯

(H_{k}, E_{k}, ES_{k}, RS_{k}, Λ^{k}) ⇒

(H_{k+1}, E_{k+1}, ES_{k+1}, (l_{k}, p_{k}) ⋯ (l_{1}, p_{1})·RS_{k+1}) (H_{1}, E_{1}, ES_{1}, RS_{1}, tuple \overline{Λ}^{k}) ⇒

(H_{k+1}[l_{k+1} ↦ (l_{1}, …, l_{k})][p_{k+1} ↦ (p_{1}, …, p_{k})], E_{k+1}, ES_{k+1}, (l_{k+1}, p_{k+1})·RS_{k+1})

(96)

Comment: (Rule 96) A tuple is constructed by evaluating its members \overline{Λ}^{k} in left-to-right order. The resulting (l, p) pairs are kept on the result stack RS until the last one is evaluated. A tuple \overline{l}^{k} is then allocated on the value heap (with a corresponding type on the type heap) to hold the results.

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) H_{2}(l_{1}) = \overline{l_{2}} ^{k} H_{2}(p_{1}) = \overline{p_{2}} ^{k} (H_{1}, E_{1}, ES_{1}, RS_{1}, select (i, Λ)) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{2}^{i}, p_{2}^{i})·RS_{2})

(97)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{1}) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) (H_{2}[p_{2} ↦ σ], E_{2}[lv ↦ (l_{1}, p_{2})], ES_{2}, E_{2}·RS_{2}, Λ_{2}) ⇒

(H_{3}, E_{3}, ES_{3}, (l_{3}, p_{3})·E_{4}·RS_{3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, let (lv, σ) = Λ_{1} in Λ_{2}) ⇒ (H_{3}, E_{4}, ES_{3}, (l_{3}, p_{3})·RS_{3})

(98)

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{1}) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) H_{2}(l_{1}) = \overline{l_{2}} ^{k} (H_{2}[p_{2}^{1} ↦ σ^{1}, …, p_{2}^{k} ↦ σ^{k}], E_{2}[lv^{1} ↦ (l_{2}^{1}, p_{2}^{1}), …, lv^{k} ↦ (l_{2}^{k}, p_{2}^{k})],

ES_{2}, E_{2}·RS_{2}, Λ_{2}) ⇒ (H_{3}, E_{3}, ES_{3}, (l_{3}, p_{3})·E_{4}·RS_{3}) (H_{1}, E_{1}, ES_{1}, RS, let \overline{(lv, σ)}^{k} = Λ_{1} in Λ_{2}) ⇒ (H_{3}, E_{4}, ES_{3}, (l_{3}, p_{3})·RS_{3})

(99)

A.6 Function Expressions

(H_{1}[l_{1}^{1} ↦ Ω, …, l_{1}^{k} ↦ Ω][p_{1}^{1} ↦ σ^{1}, …, p_{1}^{k} ↦ σ^{k}],

E_{1}[v^{1} ↦ (l_{1}^{1}, p_{1}^{1}), …, v^{k} ↦ (l_{1}^{k}, p_{1}^{k})], ES_{1}, RS_{1}, Λ_{1}^{1}) ⇒

(H_{2}, E_{2}, ES_{2}, (l_{2}, p_{2})·RS_{2})

(H_{2}[l_{1}^{1} ↦^{upd} H_{2}(l_{2})], E_{2}, ES_{2}, RS_{2}, Λ_{1}^{2}) ⇒ (H_{3}, E_{3}, ES_{3}, (l_{3}, p_{3})·RS_{3}) ⋯

(H_{k}[l_{1}^{k−1} ↦^{upd} H_{k}(l_{k})], E_{k}, ES_{k}, RS_{k}, Λ_{1}^{k}) ⇒

(H_{k+1}, E_{k+1}, ES_{k+1}, (l_{k+1}, p_{k+1})·RS_{k+1})

(H_{k+1}[l_{1}^{k} ↦^{upd} H_{k+1}(l_{k+1})], E_{k+1}, ES_{k+1}, RS_{k+1}, Λ_{2}) ⇒

(H_{k+2}, E_{k+2}, ES_{k+2}, RS_{k+2}) (H_{1}, E_{1}, ES_{1}, RS_{1}, fix \overline{(lv, σ) = Λ_{1}} ^{k} in Λ_{2}) ⇒

(H_{k+2}, E_{k+2}, ES_{k+2}, RS_{k+2})

(100)

Comment: (Rule 100) This rule achieves a simultaneous binding of a sequence of function closures (obtained from evaluating \overline{Λ}^{k}) to the variables \overline{v}^{k}. Initially, a dummy closure is allocated on the heap for each variable. The closure expressions are then evaluated in turn, and the dummy closures are updated to real closures. Thus, when the body expression Λ_{2} is evaluated, all of the dummy closures will have been updated, and any closure which references another will do so correctly when evaluated.

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{1}) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2}) (H_{2}, E_{2}, ES_{2}, RS_{2}, Λ_{2}) ⇒ (H_{3}, E_{3}, ES_{3}, (l_{2}, p_{2})·(l_{1}, p_{1})·RS_{3}) H_{3}(l_{1}) = ⟨⟨E_{c}, lv, Λ_{c}⟩⟩ (H_{3}, E_{c}[lv ↦ (l_{2}, p_{2})], ES_{3}, E_{3}·RS_{3}, Λ_{c}) ⇒

(H_{4}, E_{4}, ES_{4}, (l_{3}, p_{3})·E_{5}·RS_{4}) (H_{1}, E_{1}, ES_{1}, RS_{1}, app (Λ_{1}, Λ_{2})) ⇒ (H_{4}, E_{5}, ES_{4}, (l_{3}, p_{3})·RS_{4})

(101)

Comment: (Rule 101) The function application rule applies the function expression Λ_{1} (which evaluates to a closure) to the argument expression Λ_{2}. Firstly, both expressions are evaluated. The closure is then obtained from the result of Λ_{1}, and the result of Λ_{2} is bound to the variable v in the closure environment E_{1}. The body of the closure Λ_{3} is then evaluated in this environment. The previous environment E is then restored. The result of the function application remains on the result stack.

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{1}) ⇒ (H_{2}, E_{2}, ES_{2}, RS_{2}) (H_{2}, E_{2}, ES_{2}, RS_{2}, Λ_{2}^{1}) ⇒ (H_{3}, E_{3}, ES_{3}, RS_{3}) ⋯

(H_{k+1}, E_{k+1}, ES_{k+1}, RS_{k+1}, Λ_{2}^{k}) ⇒

(H_{k+2}, E_{k+2}, ES_{k+2}, (l_{2}^{k}, p_{2}^{k})·(l_{2}^{1}, p_{2}^{1})·(l_{1}, p_{1})·RS_{k+2}) H_{k+2}(l_{1}) = ⟨⟨E_{c}, \overline{lv}^{k}, Λ_{c}⟩⟩ (H_{k+2}, E_{c}[lv^{1} ↦ (l_{2}^{1}, p_{2}^{1}), …, lv^{k} ↦ (l_{2}^{k}, p_{2}^{k})],

ES_{k+2}, E_{k+2}·RS_{k+2}, Λ_{c}) ⇒ (H_{k+3}, E_{k+3}, ES_{k+3}, (l_{3}, p_{3})·E_{k+4}·RS_{k+3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, app (Λ_{1}, \overline{Λ_{2}} ^{k})) ⇒ (H_{k+3}, E_{k+4}, ES_{k+3}, RS_{k+3})

(102)

A.7 Exceptions

\frac{(H_{1}, E_{1}, (), RS_{1}, Λ) ⇒ (H_{2}, E_{2}, (), RS_{2})}{(H_{1}, E_{1}, (), RS_{1}, raise Λ) ⇒ halt (H_{2}, E_{2}, (), RS_{2})}  (103)

Comment: (Rule 103) If there are no closures on the exception stack then a raised exception will not be handled. The effect of an un-handled exception is to halt the evaluation of the abstract machine.

(H_{1}, E_{1}, ES_{1}, RS_{1}, Λ) ⇒ (H_{2}, E_{2}, (l_{1}, p_{1})·ES_{2}, (l_{2}, p_{2})·RS_{2}) H_{2}(l_{1}) = ⟨⟨E_{c}, lv, Λ_{c}⟩⟩ (H_{2}, E_{c}[lv ↦ (l_{2}, p_{2})], ES_{2}, E_{2}·RS_{2}, Λ_{c}) ⇒

(H_{3}, E_{3}, ES_{3}, (l_{3}, p_{3})·E_{4}·RS_{3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, raise Λ) ⇒ (H_{3}, E_{4}, ES_{3}, (l_{3}, p_{3})·RS_{3})

(104)

Comment: (Rule 104) If an exception is raised, and the exception stack is nonempty, the closure at the top of the exception stack is evaluated (see Rule 101).

Λ_{2} = (fn (lv, τ_{1} → τ_{2}) = Λ_{3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, Λ_{2}) ⇒ (H_{2}, E_{2}, ES_{2}, (l_{1}, p_{1})·RS_{2}) (H_{2}, E_{2}, (l_{1}, p_{1})·ES_{2}, RS_{2}, Λ_{1}) ⇒ (H_{3}, E_{3}, (l_{2}, p_{2})·ES_{3}, RS_{3}) (H_{1}, E_{1}, ES_{1}, RS_{1}, handle Λ_{1} with Λ_{2}) ⇒ (H_{3}, E_{3}, ES_{3}, RS_{3})

(105)

Comment: (Rule 105) This rule ensures that an exception raised in Λ_{1} is handled by Λ_{2} (which is syntactically a closure, as ensured by the equation Λ_{2} = (fn (lv, τ_{1} → τ_{2}) = Λ_{3})). This amounts to simply applying Rule 86 to Λ_{2} and placing it on the exception stack while Λ_{1} is evaluated. The raise rule performs the actual evaluation of the exception handler.

References

[1] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML: Revised 1997. The MIT Press, 1997.

[2] David C.J. Matthews and Thierry Le Sergent. LEMMA Interface Definition. Technical Report ECS-LFCS-95-316, LFCS, Division of Informatics, University of Edinburgh, January 1995.

[3] David C.J. Matthew. A Distributed Concurrent Implementation of Standard ML. In Proceedings of EurOpen Autumn 1991 Conference, September 1991. Also published as LFCS Technical Report ECS-LFCS-91-17.

[4] Greg Morrisett and Robert Harper. Semantics of Memory Management for Polymorphic Languages. Technical Report CMU-CS-96-176, School of Computer Science, Carnegie Mellon University, September 1996. Also published as Fox Memorandum CMU-CS-FOX-96-04.

[5] Chris Walton, Dilsun Kırlı, and Stephen Gilmore. An Abstract Machine for Module Replacement. In Stephan Diehl and Peter Sestoft, editors, Proceedings of the Workshop on Principles of Abstract Machines, pages 73–87, September 1998. Also published as Technical Report A 02/98 Universität Des Saarlandes.

[6] Paul R. Wilson. Uniprocessor Garbage Collection Techniques. In Yves Bekkers and Jacques Cohen, editors, International Workshop on Memory Management, number 637 in Lecture Notes in Computer Science, pages 1–42. Springer-Verlag, September 1992.

[7] M. Tofte and J. Talpin. Region-Based Memory Management. Information and Computation, 132(2):109–176, 1997.

[8] Andrew Tolmach. Tag-free Garbage Collection using Explicit Type Parameters. In Proceedings of the 1994 ACM Conference on LISP and Functional Programming, pages 1–11. ACM Press, June 1994.

[9] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed Closure Conversion. In Proceedings of the Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271–283. ACM Press, January 1996.

[10] Andrew W. Appel. Compiling with Continuations, chapter 12. Cambridge University Press, 1992.

[11] Christopher D. Walton and Bruce J. McAdam. The C-LEMMA Memory Interface on the Cray T3D. Technical Report ECS-LFCS-97-362, LFCS, Division of Informatics, University of Edinburgh, July 1997.

[12] David C.J. Matthews and Thierry Le Sergent. LEMMA: A Distributed Shared Memory with Global and Local Garbage Collection. Technical Report ECS-LFCS-95-325, LFCS, Division of Informatics, University of Edinburgh, June 1995.

[13] Bill Nitzberg and Virginia Lo. Distributed Shared Memory: A Survey of Issues and Algorithms. IEEE Computer, pages 52–60, August 1991.

[14] Thierry Le Sergent and David C J Matthews. Adaptive selection of protocols for strict coherency in distributed shared memory. Technical Report ECS-LFCS-94-306, LFCS, Division of Informatics, University of Edinburgh, September 1994.

[15] Saleh E. Abdullahi and Graem A. Ringwood. Garbage Collecting the Internet: A Survey of Distributed Garbage Collection. ACM Computing Surveys, 30(3):330–373, September 1998.

[16] Dave Berry. Generating Program Animators from Programming Language Semantics. PhD thesis, LFCS, Division of Informatics, University of Edinburgh, June 1991. Thesis No. CST-79-91.

[17] Xavier Leroy. Polymorphic Typing of an Algorithmic Language. PhD thesis, INRIA, 1992. Thesis No. 1778.

[18] Kevin Mitchell. Concurrency in a Natural Semantics. Technical Report ECS-LFCS-94-311, LFCS, Division of Informatics, University of Edinburgh, December 1994.