Linear Types and Program Resource Management
Resources and life cycles
Linear types and values
a = b;
Resource categories
-
Can the value be copied and destroyed trivially?
If yes: value belongs to category 1; this category includes all values which are merely bit patterns of fixed size: integral and floating-point numbers, booleans, characters, enumeration values, bit masks.
-
If no (it requires cleanup): are the point(s) of cleanup in the
program statically known?
If yes: (category 2) the value is used linearly, and can be (explicitly) disposed of at the appropriate place(s).
-
If no (the points of cleanup are not statically known): is the value immutable?
If yes: (category 3) the value can be either copied in its entirety, and the copies disposed of individually (3a); or the value can be managed through reference counting (3b), in which case a "copy" action consists of incrementing its reference count, and a "destroy" action consists of decrementing its reference count and optionally (if the count reaches zero) disposing of the value.
-
If no (the value is shared and mutable): is the value used from a
single thread only (or, more generally, is it only used in scope of
a specific other value which is used linearly)?
If yes: (category 4) the value can be put in a heap which is linearly owned (i.e., only accessible from one thread at a time).
-
If no (the value is mutable and shared between threads):
(category 5) the value can be protected by a lock; the lock is
reference counted and its disposal causes the value to be disposed.
-
Atoms and small integers are contained in a single machine word and
are simply copied (category 1).
-
Process contexts are linear (category 2), and is disposed of at
specific program points.
-
Message between processes are copied (category 3a).
-
Large binary values are managed through reference counting (category 3b).
-
Other Erlang terms (tuples, lists, bignums, small binaries, etc.) live
in a heap which belongs to a process which is a linear value (category 4).
-
Finally, certain data structures: the process registry, non-private tables,
etc., which are mutable and shared among processes, are managed
through the use of locks (category 5).
Intermezzo: Type notation
-
A ⊗ B is a linear product type — which is like a traditional
product type (aka record, struct, or tuple type, depending on language) type
except that each of its fields must be used (consumed) exactly once.
-
A ⊕ B is a linear sum type — which is like a normal sum type (aka tagged
union, algebraic datatype, etc.) except that the value it contains
(whichever of the variants it is) must be consumed exactly once.
-
∀T.A(T) is universal quantification — aka. parametric polymorphism
or generics, which is used for e.g. generic container types.
-
∃T.A(T) is existential quantification — such as can be used for
subtype polymorphism or typeclasses, but in what follows will be
used in a more general manner.
Resource management in a linear virtual machine
Category 1: bit patterns
copy : T → T ⊗ T dispose : T → ()
Category 2: linear values
Category 3a: resource copying
copy : T → T ⊗ T dispose : T → ()
Category 3b: reference counting
copy : T → T ⊗ T dispose : T → ()
Category 4: (defered)
Category 5: lock-protection
copy and dispose works as for a reference counted value. acquire and release work the lock.
copy : LockedT → LockedT ⊗ LockedT copy : T → T ⊗ LockedT dispose : LockedT → () acquire : LockedT → T acquire : LockedT ⊗ Timeout → T ⊕ LockedT release : T → LockedT
Category 4: heap allocation in linearly owned heap
-
At allocation time, the garbage collector must know all of the root
objects in the heap, in order to preserve all reachable values;
-
At allocation time, the location of all live pointers into the heap
must be known to the garbage collector, so that it can adjust them
appropriately when it moves objects.
Heap[h,a]
HeapPtr[T,a]
access_field : ∀h.∀a. Heap[h,a] ⊗ HeapPtr[T,a] → Heap[h,a] ⊗ F
dispose : ∀T.∀a. HeapPtr[T,a] → ()
allocate : ∀h.∀a. Heap[h,a] ⊗ _A_ ⊗ _B_ → ∃b.Heap[h,b]
RootPtr[T,h]
register_root : ∀h.∀a.∀T. Heap[h,a] ⊗ HeapPtr[T,a] → Heap[h,a] ⊗ RootPtr[T,h] read_root : ∀h.∀a.∀T. Heap[h,a] ⊗ RootPtr[T,h] → Heap[h,a] ⊗ HeapPtr[T,a] dispose_root : ∀h.∀T. RootPtr[T,h] → ()
create_heap : () → ∃h.∃a. Heap[h,a] dispose : ∀h.∀a. Heap[h,a] → ()