A Concurrent Language with a Uniform Treatment
of Regions and Locks
Prodromos Gerakios

Nikolaos Papaspyrou

Konstantinos Sagonas

School of Electrical and Computer Engineering, National Technical University of Athens, Greece
{ pgerakios, nickie, kostis } @softlab.ntua.gr

A challenge for programming language research is to design and implement multi-threaded low-level
languages providing static guarantees for memory safety and freedom from data races. Towards
this goal, we present a concurrent language employing safe region-based memory management and
hierarchical locking of regions. Both regions and locks are treated uniformly, and the language
supports ownership transfer, early deallocation of regions and early release of locks in a safe manner.

1

Introduction

Writing safe and robust code is a hard task; writing safe and robust multi-threaded low-level code is even
harder. In this paper we present a minimal, low-level concurrent language with advanced region-based
memory management and hierarchical lock-based synchronization primitives.
Region-based memory management achieves efficiency by bulk allocation and deallocation of objects in segments of memory called regions. Similar to other approaches, our regions are organized in
a hierarchical manner such that each region is physically allocated within a single parent region and
may contain multiple child regions. This hierarchical structure imposes an ownership relation as well as
lifetime constraints over regions. Unlike other languages employing hierarchical regions, our language
allows early subtree deallocation in the presence of region sharing between threads. In addition, each
thread is obliged to release each region it owns by the end of its scope.
Multi-threaded programs that interact through shared memory generate random execution interleavings. A data race occurs in a multi-threaded program when there exists an interleaving such that some
thread accesses a memory location while some other thread attempts to write to it. So far, type systems
and analyses that guarantee race freedom [6] have mainly focused on lexically-scoped constructs. The
key idea in those systems is to statically track or infer the lockset held at each program point. In the
language presented in this paper, implicit reentrant locks are used to protect regions from data races. Our
locking primitives are non-lexically scoped. Locks also follow the hierarchical structure of regions so
that each region is protected by its own lock as well as the locks of all its ancestors.
Furthermore, our language allows regions and locks to be safely aliased, escape the lexical scope
when passed to a new thread, or become logically separated from the remaining hierarchy. These features
are invaluable for expressing numerous idioms of multi-threaded programming such as sharing, region
ownership or lock ownership transfers, thread-local regions and region migration.

2

Language Design

We briefly outline the main design goals for our language, as well as some of the main design decisions
that we made to serve these goals.
Alastair R. Beresford and Simon Gay (Eds.): Programming Language
Approaches to Concurrency and Communication-cEntric Software
EPTCS 17, 2010, pp. 79–93, doi:10.4204/EPTCS.17.7

c P. Gerakios, N. Papaspyrou, and K. Sagonas
This work is licensed under the
Creative Commons Attribution License.

80

A Concurrent Language with a Uniform Treatment of Regions and Locks

Low-level and concurrent. Our language must efficiently support systems programming. As such, it
should cater for memory management and concurrency. It also needs to be low-level: it is not intended
to be used by programmers but as a target language of higher-level systems programming languages.
Static safety guarantees. We define safety in terms of memory safety and absence of data races. A
static type system should guarantee that well-typed programs are safe, with minimal run-time overhead.
Safe region-based memory management. Similarly to other languages for safe systems programming (e.g. Cyclone) our language employs region-based memory management, which achieves efficiency by bulk allocation and deallocation of objects in segments of memory (regions). Statically typed
regions [13, 14] guarantee the absence of dangling pointer dereferences, multiple release operations of
the same memory area, and memory leaks. Traditional stack-based regions [13] are limiting as they
cannot be deallocated early. Furthermore, the stack-based discipline fails to model region lifetimes in
concurrent languages, where the lifetime of a shared region depends on the lifetime of the longest-lived
thread accessing that region. In contrast, we want regions that can be deallocated early and that can
safely be shared between concurrent threads.
We opt for a hierarchical region [8] organization: each region is physically allocated within a single parent region and may contain multiple child regions. Early region deallocation in our multi-level
hierarchy automatically deallocates the immediate subtree of a region without having to deallocate each
region of the subtree recursively. The hierarchical region structure imposes the constraint that a child
region is live only when its ancestors are live. In order to allow a function to access a region without
having to pass all its ancestors explicitly, we allow ancestors to be abstracted (i.e., our language supports
hierarchy abstraction) for the duration of the function call. To maintain the liveness invariant we require
that the abstracted parents are live before and after the call. Regions whose parent information has been
abstracted cannot be passed to a new thread as this may be unsound.
Race freedom. To prevent data races we use lock-based mutual exclusion. Instead of having a separate
mechanism for locks, we opt for a uniform treatment of locks and regions: locks are placed in the same
hierarchy as regions and enjoy similar properties. Each region is protected by its own private lock and
by the locks of its ancestors. The semantics of region locking is that the entire subtree of a region
is atomically locked once the lock for that region has been acquired. Hierarchical locking can model
complex synchronization strategies and lifts the burden of having to deal with explicit acquisition of
multiple locks. Although deadlocks are possible, they can be avoided by acquiring a single lock for
a group of regions rather than acquiring multiple locks for each region separately. Additionally, our
language provides explicit locking primitives, which in turn allow a higher degree of concurrency than
lexically-scoped locking, as some locks can be released early.
Region polymorphism and aliasing. Our language supports region polymorphism: it is possible to
pass regions as parameters to functions or concurrent threads. This enables region aliasing: one actual
region could be passed in the place of two distinct formal region parameters. In the presence of mutual
exclusion and early region deallocation, aliasing is dangerous. Our language allows safe region aliasing
with minimal restrictions. The mechanism that we employ for this purpose also allows us to encode
numerous useful idioms of concurrent programming, such as region migration, lock ownership transfers,
region sharing, and thread-local regions.

P. Gerakios, N. Papaspyrou, and K. Sagonas

3

81

Language Features through Examples

Our regions are lexically-scoped first-class citizens; they are manipulated via explicit handles. For instance, a region handle can be used for releasing a region early, for allocating references and regions
within it, or for locking it. Our language uses a type and effect system to guarantee that regions and their
contents are properly used. The details will be made clear in Sections 4 and 6. Here, we present the
main features of our language through examples. We try to avoid technical issues as much as possible;
however, some characteristics of the type and effect system are revealed in this section and their presence is justified. Furthermore, to simplify the presentation in this section, we use abbreviations for a few
language constructs that we expect the readers will find more intuitive.
Example 1 (Simple Region Usage) This example shows a typical region use. New regions are allocated
via the newrgn construct. This construct requires a handle to an existing region (heap in this case), in
which the new region will be allocated, and introduces a type-level name (ρ ) and a fresh handle (h) for
the new region. The handle h is then used to allocate a new integer in region ρ ; a reference to this integer
(z) is created. Finally, the region is deallocated before the end of its lexical scope.
newrgn ρ , h at heap in
// {ρ 1,1 ⊲ ρH }
let z = new 10 at h in
...
z := deref z + 5 ;
...
free h ;
// { }
— empty effect, ρ is no longer alive
...
The comments on the right-hand side of the example’s code show the current effect. An effect is roughly
a set of capabilities that are held at a given program point. Right after creation of region ρ , the entry
ρ 1,1 ⊲ ρH is added to the effect; this means that a capability (“1, 1” — we will later explain what this
means) is held for region ρ , which resides in the heap region (ρH ). Regions start their life as local to
a thread and their contents can be directly accessed. For instance, a reference z can be created in ρ ,
dereferenced and assigned a new value, as long as the type system can verify that a proper capability for
ρ is present in the current effect. Deallocation of ρ removes the capability from the effect; once that is
done, the region’s contents become inaccessible.
Example 2 (Hierarchical Regions) In the previous example a trivial hierarchy was created by allocating region ρ within the heap region. It is possible to construct richer region hierarchies. As in the
previous example, the code below allocates a new region ρ1 within the heap. Other regions can be then
allocated within ρ1 , e.g. ρ2 ; this can done by passing the handle of ρ1 to the region creation construct.
Similarly, regions ρ3 and ρ4 can be allocated within region ρ2 .
newrgn ρ1 , h at heap in
...
newrgn ρ2 , h2 at h1 in
...
newrgn ρ3 , h3 at h2 in
newrgn ρ4 , h4 at h2 in
...

// {ρ11,1 ⊲ ρH }

ρH1,0

// {ρ11,1 ⊲ ρH , ρ21,1 ⊲ ρ1 }

ρ11,1

// {ρ11,1 ⊲ ρH , ρ21,1 ⊲ ρ1 , ρ31,1 ⊲ ρ2 }
// {ρ11,1 ⊲ ρH , ρ21,1 ⊲ ρ1 , ρ31,1 ⊲ ρ2 , ρ41,1 ⊲ ρ2 }

...

...

ρ21,1
ρ31,1

ρ41,1

Our language allows regions to be allocated at any level of the hierarchy. For instance, it is possible to
allocate more regions within region ρ1 , in the lexical scope of region ρ4 .

82

A Concurrent Language with a Uniform Treatment of Regions and Locks

Example 3 (Bulk Region Deallocation) In the first example a single region was deallocated. That region was a leaf node in the hierarchy; it contained no sub-regions. In the general case, when a region is
deallocated, the entire subtree below that region is also deallocated. This is what happens if, in the code
of the previous example, we deallocate region ρ2 within the innermost scope; regions ρ3 and ρ4 are also
deallocated. They are all removed from the current effect and thus are no longer accessible.
newrgn ρ1 , h at heap in
...
newrgn ρ2 , h2 at h1 in
...
newrgn ρ3 , h3 at h2 in
newrgn ρ4 , h4 at h2 in
...
free h2 ;
...

// {ρ11,1 ⊲ ρH }

ρH1,0

// {ρ11,1 ⊲ ρH , ρ21,1 ⊲ ρ1 }
//
//

{ρ11,1 ⊲ ρH , ρ21,1 ⊲ ρ1 , ρ31,1 ⊲ ρ2 }
{ρ11,1 ⊲ ρH , ρ21,1 ⊲ ρ1 , ρ31,1 ⊲ ρ2 , ρ41,1 ⊲ ρ2 }

// {ρ11,1 ⊲ ρH }
// ρ2 , ρ3 and ρ4 are no longer alive

ρ11,1
...

...

ρ21,1
ρ31,1

ρ41,1

Example 4 (Region Migration) A common multi-threaded programming idiom is to use thread-local
data. At any time, only one thread will have access to such data and therefore no locking is required.
A thread can transfer thread-local data to another thread but, doing so, it loses access to the data. This
idiom is known as migration. Our language encodes thread-local data and data migration. As we have
seen, newly created regions are considered thread-local; a capability for them is added to the current
effect. We support data migration by allowing such capabilities to be transferred to other threads.
The following example illustrates region migration. A server thread is defined, which executes an
infinite loop. In every iteration, a new region is created and is initialized with client data. The contents
of the region are then processed and finally transferred to a newly created (spawned) thread.
def server = ΛρH . λ heap.
while (true) do
newrgn ρ , h at heap in
let z = wait data[ρ ](h) in
process(z);
spawn output[ρ ](h, z);
...

// {ρ 1,1 ⊲ ρH }
// region ρ is thread-local
// { }
— empty effect, ρ migrates to output
// ρ cannot be accessed here

The server thread accepts the heap region and its handle. Within the infinite loop, it allocates a new
region ρ in the heap. Its handle h is passed to function wait data, which is supposed to fill the region
ρ with client data (z). Function process is then called and works on the data. Until this point, region ρ
is thread-local and accessible to the server thread, so no explicit locking is required. Now, let us assume
that we want the processed data to be output by a different thread, e.g. to avoid an unnecessary delay on
the server thread. A new thread output is spawned and receives the region handle h and the reference z
to the client data. The capability ρ 1,1 ⊲ ρH is removed from the effect of server and is added to the input
effect of thread output. Therefore, region ρ has now become thread-local to thread output, which can
access it directly, while it is no longer accessible to the server thread.
Example 5 (Region Sharing) In the previous examples, capabilities for all regions were “1, 1” which,
as we roughly explained, corresponds to thread-local. In general, a capability for a region consists of two
natural numbers; the first denotes the region count, whereas the second denotes the lock count. When the
region count is positive, the region is definitely alive. Similarly, when the lock count is positive, memory

P. Gerakios, N. Papaspyrou, and K. Sagonas

83

accesses to this region’s contents are guaranteed to be race free. Capabilities with counts other than 1
can be used for sharing regions between threads.
Multithreaded programs often share data for communication purposes. In this example, a server
thread almost identical to that of the previous example is defined. The programmer’s intention here,
however, is to process the data and display it in parallel. Therefore, the output thread is spawned first
and then the server thread starts processing the data.
def server = ΛρH . λ heap.
while (true) do
newrgn ρ , h at heap in
let z = wait data[ρ ](h) in
share h; unlock h;
spawn output[ρ ](h, z);
while (! finished) do
lock h;
process(z);
unlock h

// {ρ 1,1 ⊲ ρH }
// {ρ 2,0 ⊲ ρH }
// {ρ 1,0 ⊲ ρH }

— output consumes ρ 1,0 ⊲ ρH

// {ρ 1,1 ⊲ ρH }
// {ρ 1,0 ⊲ ρH }

Operator share increases the region count and operator unlock decreases the lock count. As a consequence, starting with capability ρ 1,1 ⊲ ρH , we end up with ρ 2,0 ⊲ ρH . When output is spawned, it
consumes “half” of this capability (ρ 1,0 ⊲ ρH ); the remaining “half” (ρ 1,0 ⊲ ρH ) is still held by the server
thread. Region ρ is now shared between the two threads; however, none of them can access its data
directly, as this may lead to a data race. The lock and unlock operators have to be used for explicitly
locking and unlocking the region, before safely accessing its contents. Processing is now performed
iteratively; the server thread avoids locking the region for long periods of time, thus allowing the output
thread to execute a similar loop and gain access to the region when needed.
Example 6 (Hierarchical Locking) In the previous example, locking and unlocking was performed on
a leaf region. In general, locking a region in the hierarchy has the effect of atomically locking its subregions as well. A region is accessible when it has been locked by the current thread or when at least one
of its ancestors has been locked.
Hierarchical locking can be useful when a set of locks needs to be acquired atomically. In this
example, we assume that two hash tables (tbl1 and tbl2 ) are used. An object with a given key must be
removed from tbl1 , which resides in region ρ1 , and must be inserted in tbl2 , which resides in region ρ2 .
We can atomically acquire access to both regions ρ1 and ρ2 , by locking a common ancestor of theirs.
lock h;
let ob j = hash remove[ρ1 ](tbl1 , key) in
hash insert[ρ2 ](tbl2 , key, ob j);
unlock h

// the handle of a common ancestor of ρ1 and ρ2

Example 7 (Region Aliasing) An expressive language with regions will have to support region polymorphism, which invariably leads to region aliasing. This must be handled with caution, as a naı̈ve
approach may cause unsoundness. In the examples that follow, we discuss how region aliasing is used in
our language as well as the restrictions that we impose to guarantee safety.
Function swap accepts two integer references, residing in regions ρ1 and ρ2 , and swaps their contents.
It assumes that both regions are already locked and remain locked when the function returns.
def swap = Λρ1 . Λρ2 . λ (x : ref(ρ1 , int), y : ref(ρ2 , int)).// ρ1 and ρ2 must be both locked
let z = deref x in
// OK: ρ1 is locked

A Concurrent Language with a Uniform Treatment of Regions and Locks

84
x := deref y;
y := z

// OK: ρ1 and ρ2 are locked
// OK: ρ2 is locked

In order to instantiate ρ1 and ρ2 with the same region ρ , we can create two lock capabilities by using
the lock operator twice on ρ ’s handle h. Of course, the second use of lock will succeed immediately,
as the region has already been locked by the same thread.
...
lock h; lock h;
swap[ρ ][ρ ](a, b);
unlock h; unlock h

//
//
//
//

{ρ 2,0 ⊲ ρH }
{ρ 2,2 ⊲ ρH }
each ρ parameter requires ρ 1,1 ⊲ ρH
{ρ 2,0 ⊲ ρH }

Example 8 (Reentrant locks) Region aliasing introduces the need for reentrant locks. To see this, let
us change the swapping function of the previous example, so that it receives two references in unlocked
regions. For swapping their contents, it will have to acquire locks for the two regions (and release them,
when they are no longer needed).
def swap = Λρ1 . Λρ2 . λ (h1 : rgn(ρ1 ), h2 : rgn(ρ2 ).
x : ref(ρ1 , int), y : ref(ρ2 , int)).//
lock h1 ;
let z = deref x in
//
lock h2 ;
x := deref y;
//
unlock h1 ;
y := z;
//
unlock h2
//

ρ1 and ρ2 are unlocked
OK: ρ1 is locked
OK: ρ1 and ρ2 are locked
OK: ρ2 is locked
all locks can be released

Suppose again that we are to instantiate ρ1 and ρ2 with the same region ρ .
...
swap[ρ ][ρ ](h, h, a, b);

// {ρ 2,0 ⊲ ρH }
// each ρ parameter requires ρ 1,0 ⊲ ρH

We can easily see, however, that the run-time system cannot use binary locks; in that case, swap[ρ ][ρ ]
would either come to a deadlock, waiting to obtain once more the lock that it has already acquired, or
— worse — it might release the lock early (at unlock h1 ) and allow a data race to occur. To avoid
unsoundness, we use reentrant locks: lock counts are important both for static typing and for the runtime system. A lock with a positive run-time count can immediately be acquired again, if it was held by
the same thread. Moreover, a lock is released only when its run-time count becomes zero.
Example 9 (Pure and Impure Capabilities) Unrestricted region aliasing leads to unsoundness. Consider function bad, which accepts two integer references (x and y) in regions ρ1 and ρ2 , which are both
locked. It lets ρ1 migrate to a new thread and passes x as a parameter. It then assigns a value to y.
def bad = Λρ1 . Λρ2 . λ (x : ref(ρ1 , int), y : ref(ρ2 , int)). // ρ1 and ρ2 must be both locked
spawn f[ρ1 ](x);
// ρ1 migrates to f while locked
y := 7
// OK: ρ2 is still locked — WRONG!
A data race may occur if we call bad as follows; both threads have access to a, each holding a lock for
ρ.
swap[ρ ][ρ ](a, a);

// each ρ parameter requires ρ 1,1 ⊲ ρH

P. Gerakios, N. Papaspyrou, and K. Sagonas
Value

v

Function

f

Expression e

::=

f | c | rgnı | locl
γ →γ

::= λ x. e as τ −→ τ | Λρ . f
ξ

::= x | c | f | (e e) | e [r] | new e at eε | e := e | locl
| deref e | newrgn ρ , x at e in e | capη e | rgnı
γ →γ

Type

τ

::= b | τ −→ τ | ∀ρ . τ | ref(τ , r) | rgn(r)

Effect

γ

::= 0/ | γ , rκ ⊲ π

85
Calling mode

ξ

::= seq | par(γ )

Capability op

η

::= ψ + | ψ −

Capability kind

ψ

::= rg | lk

Capability

κ

::= n, n | n, n

Region parent

π

::= r | ⊥ | ?

Region

r

::= ρ | ı

Figure 1: Syntax.
The cause of the unsoundness is that, in this last call to swap[ρ ][ρ ], we allowed a single capability
ρ 2,2 ⊲ ρH to be divided in two distinct capabilities ρ 1,1 ⊲ ρH . More specifically, we divided the lock count
in two and created two distinct lock capabilities, one of which escaped to a different thread through
region migration. To resolve the unsoundness, we introduce the notion of pure (i.e., full) and impure (i.e.,
divided) capabilities. For instance, ρ 2,2 ⊲ ρH is a pure capability; when we divide it we obtain two impure
halves, which we denote as ρ 1,1 ⊲ ρH . Impure capabilities cannot be given to newly spawned threads
when their lock count is positive. In contrast with pure capabilities, they represent inexact knowledge of
a region’s counts.

4

Language Description

The syntax of the language is illustrated in Figure 1. The language core comprises of variables (x),
constants (c), functions, and function application. Functions can be region polymorphic (Λρ . f ) and
region application is explicit (e[ρ ]). Monomorphic functions (λ x. e) must be annotated with their type.
The application of monomorphic functions is annotated with a calling mode (ξ ), which is seq for normal
(sequential) application and par(γ ) for spawning a new thread.1 Parallel application is annotated with
the input effect of the new thread (γ ); this annotation can be automatically inferred by the type checker.
The constructs for manipulating references are standard. A newly allocated memory cell is returned by
new e1 at e2 , where e1 is the value that will be placed in the cell and e2 is a handle of the region in which
the new cell will be allocated. Standard assignment and dereference operators complete the picture.
The construct newrgn ρ , x at e1 in e2 allocates a new region ρ and binds x to the region handle.
The new region resides in a parent region, whose handle is given in e1 . The scope of ρ and x is e2 ,
which must consume the new region by the end of its execution. A region can be consumed either by
deallocation or by transferring its ownership to another thread. At any given program point, each region
is associated with a capability (κ ). Capabilities consist of two natural numbers, the capability counts:
the region count and lock count, which denote whether a region is live and locked respectively. When
first allocated, a region starts with capability (1, 1), meaning that it is live and locked, so that it can
be exclusively accessed by the thread that allocated it. As we have seen, this is our equivalent of a
thread-local region.
By using the construct capη e, a thread can increment or decrement the capability counts of the
region whose handle is specified in e. The capability operator η can be, e.g., rg+ (meaning that the
region count is to be incremented) or lk− (meaning that the lock count is to be decremented).2 When a
region count reaches zero, the region may be physically deallocated and no subsequent operations can
1 In

the examples of Section 3, we used more intuitive notation: we omitted seq and used the keyword spawn instead of par.
region manipulation operators used in Section 3 are simple abbreviations: share ≡ caprg+ , unlock ≡ caplk− , etc.

2 The

A Concurrent Language with a Uniform Treatment of Regions and Locks

86
Configuration

C

::= S; T

Threads

T

::= 0/ | T, n : e

Store

S

::= 0/ | S, ı : (θ , H, S)

Thread map

θ

::= 0/ | θ , n1 7→ n2 , n3

Memory heap

H

::= 0/ | H, ℓ 7→ v

E

::=
|
|
|

 | (E e)ξ | (v E)ξ | E [r]
newrgn ρ , x at E in e | capη E
new E at eε | new v at E ε
deref E | E := e | v := E

Figure 2: Configurations, store, threads and evaluation contexts.
be performed on it. When a lock count reaches zero, the region is unlocked. As we explained, capability
counts determine the validity of operations on regions and references. All memory-related operations
require that the involved regions are live, i.e., the region count is greater than zero. Assignment and
dereference can be performed only when the corresponding region is live and locked.
A capability of the form (n1 , n2 ) is called a pure capability, whereas a capability of the form (n1 , n2 )
is called an impure capability. In both cases, it is implied that the current thread can decrement the
region count n1 times and the lock count n2 times. Impure capabilities are obtained by splitting pure or
other impure capabilities into several pieces, e.g., (3, 2) = (2, 1) + (1, 1), in the same spirit as fractional
capabilities [4]. As we explained in Example 9 of Section 3, these pieces are useful for region aliasing,
when the same region is to be passed to a function in the place of two distinct region parameters. An
impure capability implies that our knowledge of the region and lock count is inexact. The use of such
capabilities must be restricted; e.g., an impure capability with a non-zero lock count cannot be passed to
another thread, as it is unsound to allow two threads to simultaneously hold the same lock. Capability
splitting takes place automatically with function application.

5

Operational Semantics

We define a small-step operational semantics for our language, using two evaluation relations, at the level
of threads and expressions (Figures 3 and 4 on the next page). The thread evaluation relation transforms
configurations. A configuration C (see Figure 2) consists of an abstract store S and a list of threads T .3
Each thread in T is of the form n : e, where n is a thread identifier and e is an expression. The store is a
list of regions of the form ı : (θ , H, S), where ı is a region identifier, θ is a thread map, H is a memory
heap and S is the list of subregions in the region hierarchy. The thread map associates thread identifiers
with capability counts for region ı, whereas the memory heap represents the region’s contents, mapping
locations to values.
A thread evaluation context E (Figure 2) is defined as an expression with a hole, represented as .
The hole indicates the position where the next reduction step can take place. Our notion of evaluation
context imposes a call-by-value evaluation strategy to our language. Subexpressions are evaluated in a
left-to-right order.
We assume that concurrent reduction events can be totally ordered. At each step, a random thread
(n) is chosen from the thread list for evaluation (Figure 3). It should be noted that the thread evaluation
rules are the only non-deterministic rules in the operational semantics of our language; in the presence of
more than one active threads, our semantics does not specify which one will be selected for evaluation.
Threads that have completed their evaluation and have been reduced to unit values, represented as (),
are removed from the active thread list (rule E-T ). Rule E-S reduces some thread n via the expression
3 The order of elements in comma-separated lists, e.g. in a store S or in a list of threads T , is not important; we consider all
list permutations as equivalent.

P. Gerakios, N. Papaspyrou, and K. Sagonas

87

e′ ≡ ((λ x. e as τ ) v)par(γ1 )
e′′ ≡ ((λ x. e as τ ) v)seq
fresh n′
S′ = transfer(S, n, n′ , γ1 )
S; T, n : E[e′ ]
S′ ; T, n : E[()], n′ : e′′
S; e →n S′ ; e′
S; T, n : E[e]
S′ ; T, n : E[e′ ]

(E-S)

S; T, n : ()

S; T

(E-A)

(S′ , k) = newrgn(S, n, j)
S; newrgn ρ , x at rgnj in e →n S′ ; e[k/ρ ][rgnk /x]
(S′ , ℓ) = alloc(j, S, v)
S; new v at rgnj ε →n S′ ; locℓ

(E-NR)

(E-T)

C ′.

Figure 3: Thread evaluation relation C
S; ((λ x. e as τ ) v)seq →n S; e[v/x]

(E-SN)

S; (Λρ . f )[r] →n S; f [r/ρ ]

(E-NG)

S′ = update(S, ℓ, v, n)
S; locℓ := v →n S′ ; ()

(E-RP)

S′ = updcap(S, η , j, n)
S; capη rgnj →n S′ ; ()

(E-AS)

(E-C)

v = lookup(S, ℓ, n)
S; deref locℓ →n S; v

(E-D)

Figure 4: Expression evaluation relation S; e →n S′ ; e′ .
evaluation relation. When a parallel function application redex is detected within the evaluation context
of a thread, a new thread is created (rule E-SN ). The redex is replaced with a unit value in the currently executed thread and a new thread is added to the thread list, with a fresh thread identifier. The
partial function transfer(S, n, n′ , γ1 ) updates the thread maps of all regions specified in γ1 , transferring
capabilities between threads n and n′ . It is undefined when this transfer is not possible.
The expression evaluation relation is defined in Figure 4. The rules for reducing function application
(E-A ) and region application (E-RP ) are standard. The remaining rules make use of five partial functions
that manipulate the store. These functions are undefined when their constraints are not met. All of them
require that some region is live. A region is live when the sum of all region counts in the thread map
associated with that region is positive and all ancestors of the region are live as well. In addition to
liveness, some of these functions require that some region is accessible to the currently executed thread.
Region r is accessible to some thread n (and inaccessible to all other threads) when r is live and the
thread map associated with r, or with some ancestor of r, maps n to a positive lock count.
• alloc(j, S, v) is used in rule E-NR for creating a new reference. It allocates a new object in S. The
object is placed in region j and is set to value v. Region j must be live. Upon success, the function
returns a pair (S′ , ℓ) containing the new store and a fresh location for the new object.
• lookup(S, ℓ, n) is used in rule E-D to look up the value of location ℓ in S. The region in which ℓ
resides must be accessible to the currently executed thread n. Upon success, the function returns
the value v stored at ℓ.
• update(S, ℓ, v, n) is used in rule E-AS to assign the value v to location ℓ in S. The region in which
ℓ resides must be accessible to the currently executed thread n. Upon success, the function returns
the new store S′ .
• newrgn(S, n, j) is used in rule E-NG to create a new region in S. The new region is allocated
within j, which must be live. Its thread map is set to n 7→ 1, 1. Upon success, the function returns
a pair (S′ , k) containing the new store and a fresh region name for the new region.
• updcap(S, η , j, n) is used in rule E-C . This operation updates S by modifying the region or lock
count of thread n for region j. Upon success, the function returns the new store S′ . When a lock

A Concurrent Language with a Uniform Treatment of Regions and Locks

88
γ1 →γ2

R; ∆ ⊢ τ
τ ≡ τ1 −→ τ2
R; M; ∆; Γ, x : τ1 ⊢ e : τ2 & (γ1 ;γ2 )
R; M; ∆; Γ ⊢ λ x. e as τ : τ & (γ ;γ )
R; M; ∆; Γ ⊢ e : ref(τ , r) & (γ ;γ ′ )
is accessible (γ ′ , r)
R; M; ∆; Γ ⊢ deref e : τ & (γ ;γ ′ )

γ1 →γ2

(T-F)

(T-D)

R; M; ∆; Γ ⊢ e1 : τ1 −→ τ2 & (γ ;γ ′ ) ξ 6= seq ⇒ τ2 = hi
ξ ⊢ γ ′′′ = γ2 ⊕ (γ ′′ ⊖ γ1 )
R; M; ∆; Γ ⊢ e2 : τ1 & (γ ′ ;γ ′′ )
R; M; ∆; Γ ⊢ (e1 e2 )ξ : τ2 & (γ ;γ ′′′ )

(T-AP)

r ∈ dom (γ ′ )
R; ∆ ⊢ τ
R; M; ∆; Γ ⊢ e1 : rgn(r) & (γ ;γ ′ )
′
R; M; ∆, ρ ; Γ, x : rgn(ρ ) ⊢ e2 : τ & (γ , ρ 1,1 ⊲ r;γ ′′ ) ρ 6∈ dom (γ ′′ )
R; M; ∆; Γ ⊢ newrgn ρ , x at e1 in e2 : τ & (γ ;γ ′′ )

R; M; ∆; Γ ⊢ e1 : τ & (γ ;γ ′ )
R; M; ∆; Γ ⊢ e2 : rgn(r) & (γ ′ ;γ ′′ ) r ∈ dom (γ ′′ )
R; M; ∆; Γ ⊢ new e1 at e2 ε : ref(τ , ρ ) & (γ ;γ ′′ )

(T-NR)

R; M; ∆; Γ ⊢ e1 : rgn(r) & (γ ;γ ′ , rκ ⊲ π )
′
κ ′ = [[η ]] (κ )
γ ′′ = live (γ ′ , rκ ⊲ π )
R; M; ∆; Γ ⊢ capη e1 : hi & (γ ;γ ′′ )

(T-NG)

(T-CP)

Figure 5: Selected typing rules.
update is requested and the lock is held by another thread, the result is undefined. In this case, rule
E-C cannot be applied and the operation will block, until the lock is available.
The operational semantics may get stuck when a deadlock occurs. Our semantics will also get stuck
when a thread attempts to access a memory location without having acquired an appropriate lock for this
location. In this case, update(S, ℓ, v, n) and lookup(S, ℓ, n) are undefined and it is impossible to perform a
single step via rules E-AS or E-D . The same is true in several other situations (e.g. when referring to a
non-existent region or location). Threads that may cause a data race will definitely get stuck.
We follow a different approach from related work, e.g. the work of Grossman [10], where a special
kind of value junkv is often used as an intermediate step when assigning a value v to a location, before
the real assignment takes place, and type safety guarantees that no junk values are ever used. As described above, we use a more direct approach by incorporating the locking mechanism in the operational
semantics. Our progress lemma in Section 7 guarantees that, at any time, all threads can make progress
and, therefore, a possible implementation does not need to check liveness or accessibility at run-time.

6

Static Semantics

In this section we discuss the most interesting parts of our type system. As we sketched in Section 3, to
enforce our safety invariants, we use a type and effect system. Effects are used to statically track region
capabilities. An effect (γ ) is a list of elements of the form rκ ⊲ π , denoting that region r is associated with
capability κ and has parent π , which can be another region, ⊥, or ?. Regions whose parents are ⊥ or ?
are considered as roots in our region hierarchy. We assume that there is an initial (physical) root region
corresponding to the entire heap, whose handle is available to the main program. The parent of the heap
region is ⊥. More (logical) root regions can be created using hierarchy abstraction. The abstract parent
of a region that is passed to a function is denoted by ?.
The syntax of types in Figure 1 (on page 85) is more or less standard. A collection of base types b is
assumed; the syntax of values belonging to these types and operations upon such values are omitted from
this paper. We assume the existence of a unit base type, which we denote by hi. Region handle types
rgn(r) and reference types ref(τ , r) are associated with a type-level region r. Monomorphic function
types carry an input and an output effect. A well-typed expression e has a type τ under an input effect γ
and results in an output effect γ ′ . The typing relation (see Figure 5) is denoted by R; M; ∆; Γ ⊢ e : τ & (γ ;γ ′ )
and uses four typing contexts: a set of region literals (R), a mapping of locations to types (M), a set of
region variables (∆), and a mapping of term variables to types (Γ). The effects that appear in our typing

P. Gerakios, N. Papaspyrou, and K. Sagonas

89

ξ ⊢ γ = γ1 ⊕ γr
ξ ⊢ γ ′ = γ2 ⊕ γr
γ ′′ = live (γ ′ )
consistent (γ ; γ ′′ )
′′
′′′
ξ = seq ⇒ abs par (γ ; γ1 ) ⊆ dom (γ ) ξ = par(γ ) ⇒ γ1 = γ ′′′ ∧ γ2 = 0/
ξ ⊢ γ ′′ = γ2 ⊕ (γ ⊖ γ1 )
ξ ⊢ γ = 0/ ⊕ γ

π ′ ∈ {π , ? }

(ES-N)

ξ = par(γ ′ ) ⇒ π ′ 6= ?
ξ ⊢ κ = κ1 + κ2
κ
κ
1
ξ ⊢ γ , r ⊲ π = γ 1 , r ⊲ π ′ ⊕ γ 2 , r κ2 ⊲ π

(ESJ)
ξ ⊢ γ = γ1 ⊕ γ2

lk (κ ) = lk (κ1 ) + lk (κ2 )
rg (κ1 ) > 0
rg (κ ) = rg (κ1 ) + rg (κ2 )
is pure (κ1 ) ⇔ is pure (κ2 ) is pure (κ1 ) ⇒ κ = κ1
ξ 6= seq ∧ ¬is pure (κ1 ) ⇒ lk (κ2 ) = 0
ξ ⊢ κ = κ1 + κ2

(ES-C)

(CS)

Figure 6: Effect and capability splitting.
(rκ ⊲ π ) ∈ γ

rg (κ ) > 0
is live (γ , r)

(rκ ⊲ r′ ) ∈ γ

π ∈ {⊥, ? }

(rκ ⊲ π ) ∈ γ
lk (κ ) > 0
is accessible (γ , r)

rg (κ ) > 0
is live (γ , r)

is live (γ , r′ )

(rκ ⊲ r′ ) ∈ γ
is accessible (γ , r′ )
is accessible (γ , r)

Figure 7: Auxiliary predicates: region liveness and accessibility.
rg (κ )
lk (κ )
dom (γ )
live (γ )
is pure (κ )
consistent (γ1 ; γ2 )

=
=
=
=
=
=

abs par (γ1 ; γ2 )

=

n1 if κ = n1 , n2 ∨ κ = n1 , n2
n2 if κ = n1 , n2 ∨ κ = n1 , n2
{ r | (rκ ⊲ π ) ∈ γ }
{ rκ ⊲ π | (rκ ⊲ π ) ∈ γ ∧ is live (γ , r) }
∃n1 . ∃n2 . κ = n1 , n2
′
(∀(rκ ⊲ π ) ∈ γ1 . ∀(rκ ⊲ π ′ ) ∈ γ2 . π = π ′ ∧ (is pure (κ ) ⇔ is pure (κ ′ )))
n ∧ dom (γ2 ) ⊆ dom (γ1 ) ∧ live (γ1o) = γ1 ∧ live (γ2 ) = γ2
r | (rκ ⊲ r′ ) ∈ γ1 ∧ (rκ ⊲ ? ) ∈ γ2
′

Figure 8: Auxiliary functions and predicates.
relation must satisfy a liveness invariant: all regions that appear in the effect are live, i.e., their region
counts and those of all their ancestors are positive. Thus, in order to check if a region r is live in the
effect γ , we only need to check that r ∈ dom (γ ).
The typing rule for lambda abstraction (T-F ) requires that the body e is well-typed with respect to the
effects ascribed on its type. The typing rule for function application (T-AP ) splits the output effect of e2
(γ ′′ ) by subtracting the function’s input effect (γ1 ). It then joins the remaining effect with the function’s
output effect (γ2 ). In the case of parallel application, rule T-AP also requires that the return type is
unit. The splitting and joining of effects is controlled by the judgement ξ ⊢ γ ′′ = γ2 ⊕ (γ ⊖ γ1 ), which is
defined in Figure 6 (the auxiliary functions and predicates are defined in Figures 7 and 8). It enforces the
following properties:
• the liveness invariant for γ ′′ ;
• the consistency of γ and γ ′′ , i.e., regions cannot change parent and capabilities cannot switch from
pure to impure or vice versa; the domain of γ ′′ is a subset of the domain of γ ;
• for sequential application, all parent regions that become abstracted for the duration of the function
call must be live after the function returns;
• for parallel application, the thread output effect must be empty, the thread input effect must not
contain impure capabilities with positive lock counts and hierarchy abstraction is disallowed.
The typing rules for references are standard. In Figure 5 we only show the rules for dereference

A Concurrent Language with a Uniform Treatment of Regions and Locks

90

(T-D ) and reference allocation (T-NR ). The former checks that region r is accessible. The latter only
checks that the region r is live. The rule for creating new regions (T-NG ) checks that e1 is a handle for
some live region r′ . Expression e2 is type checked in an extended typing context (i.e., ρ and x : rgn(ρ )
are appended to ∆ and Γ respectively) and an extended input effect (i.e., a new effect is appended to the
input effect such that the new region is live and accessible to this thread). The rule also checks that the
type and the output effect of e2 do not contain any occurrence of region variable ρ . This implies that ρ
must be consumed by the end of the scope of e2 . The capability manipulation rule (T-CP ) checks that e
is a handle of a live region r. It then modifies the capability count of r as dictated by function [[η ]], which
increases or decreases the region or the lock count of its argument, according to the value of η . The
dynamic semantics ensures that an operational step is performed when the actual counts are consistent
with the desired output effect. For instance, if the lock of region r is held by some other executing
thread, the evaluation of caplk+ must be suspended until the lock can be obtained. On the other hand,
the evaluation of caprg− does not need to suspend but may not be able to physically deallocate a region,
as it may be used by other threads.

7

Type Safety

In this section we discuss the fundamental theorems that prove type safety of our language.4 The type
safety formulation is based on proving the preservation and progress lemmata. Informally, a program
written in our language is safe when for each thread of execution an evaluation step can be performed or
that thread is waiting for a lock (blocked). As discussed in Section 5, a thread may become stuck when it
accesses a region that is not live or accessible (these are obviously the interesting cases in our concurrent
setting; of course a thread may become stuck when it performs a non well-typed operation). Deadlocked
threads are not considered to be stuck.
Definition 1 (Thread Typing) Let T be a collection of threads. Let R; M; δ be a global typing context,
in which δ is a mapping from thread identifiers to effects, used only for metatheoretic purposes. For each
thread n : e in T , we take δ (n) to be the input effect that corresponds to the evaluation of expression e.
The following rules define well-typed threads.
R; M; δ ⊢T T
R; M; 0/ ⊢T 0/

R; M; 0;
/ 0/ ⊢ e : hi & (γ ;0)
/
R; M; δ , n 7→ γ ⊢T T, n : e

n∈
/ dom (δ )

Definition 2 (Store Consistency) A store S is consistent with respect to an effect mapping δ when the
following conditions are met:
• Region consistency: the set of region names occurring in the co-domain of δ is a subset of the set
of region names in S.
• Static-dynamic count consistency: for each region, the dynamic region and lock counts of some
thread must be greater than or equal to the corresponding static counts of the same thread.
• Mutual exclusion: only one thread may have a positive lock count in δ for a particular region j.
Additionally, only this thread is allowed to access or lock sub-regions of j.
Definition 3 (Store Typing) A store S is well-typed with respect to R; M; δ (we denote this by
R; M; δ ⊢str S) when the following conditions are met:
4 Full

proofs and a full formalization of our language are given in the companion technical report [9].

P. Gerakios, N. Papaspyrou, and K. Sagonas

91

• S is consistent with respect to δ ,
• the set of region names in S is equal to R,
• the set of locations in M is equal to the set of locations in S, and
• for each location ℓ, the stored value S(ℓ) is closed and has type M(ℓ) with empty effects, i.e.,
R; M; 0;
/ 0/ ⊢ S(ℓ) : M(ℓ) & (0;
/ 0).
/
Definition 4 (Configuration Typing) A configuration S; T is well-typed with respect to R; M; δ (we
denote this by R; M; δ ⊢C S; T ) when the collection of threads T is well-typed with respect to R; M; δ and
the store S is well-typed with respect to R; M; δ .
Definition 5 (Not stuck) A configuration S; T is not stuck when each thread in T can take one of the
evaluation steps in Figure 3 (E-S , E-T or E-SN ) or it is waiting for a lock held by some other thread.
Given these definitions, we can now present the main results of this paper. The progress and preservation lemmata are first formalized at the program level, i.e., for all concurrently executed threads.
Lemma 1 (Progress — Program) Let S; T be a closed well-typed configuration with R; M; δ ⊢C S; T .
Then S; T is not stuck.
Lemma 2 (Preservation — Program) Let S; T be a well-typed configuration with R; M; δ ⊢C S; T . If
the operational semantics takes a step S; T
S′ ; T ′ , then there exist R′ ⊇ R, M ′ ⊇ M and δ ′ such that the
resulting configuration is well-typed with R′ ; M ′ ; δ ′ ⊢C S′ ; T ′ .
An expression-level version for each of these two lemmata is required, in order to prove the above.
At the expression level, progress and preservation are defined as follows.
Lemma 3 (Progress — Expression) Let S be a well-typed store with R; M; δ , n 7→ γ ⊢str S and let e be
a closed well-typed redex with R; M; 0;
/ 0/ ⊢ e : τ & (γ ;γ ′ ). Then exactly one of the following is true:
• e is of the form caplk+ rgnj and j is a live but inaccessible region to thread n, or
• e is of the form (λ x. e1 as τ v)par(γ ) or
• there exist S′ and e′ such that S; e →n S′ ; e′ .
Lemma 4 (Preservation — Expression) Let e be a well-typed expression with R; M; 0;
/ 0/ ⊢ e : τ & (γ ;γ ′′ )
and let S be a well-typed store with R; M; δ , n 7→ γ ⊢str S. If the operational semantics takes a step
S; e →n S′ ; e′ , then there exist R′ ⊇ R, M ′ ⊇ M and γ ′ such that the resulting expression and the resulting
store are well-typed with R′ ; M ′ ; 0;
/ 0/ ⊢ e′ : τ & (γ ′ ;γ ′′ ) and R′ ; M ′ ; δ [n 7→ γ ′ ] ⊢str S′ .
The type safety theorem is a direct consequence of Lemmata 1 and 2. Let function main be the
initial program, let ιH be global heap region and let the initial typing contexts R0 and δ0 and the initial
program configuration S0 ; T0 be defined by the following singleton lists: R0 = {ιH }, δ0 = {1 7→ ιH1,0 ⊲ ⊥},
/ 0)},
/
and T0 = {1 : (main[ιH ] rgnιH )seq }.
θ0 = {1 7→ 1, 0}, S0 = {ιH : (θ0 , 0,
Theorem 1 (Type Safety) If the initial configuration S0 ; T0 is well-typed with R0 ; 0;
/ δ0 ⊢C S0 ; T0 and the
operational semantics takes any number of steps S0 ; T0 n Sn ; Tn , then the resulting configuration Sn ; Tn
is not stuck.
The empty (except for R0 that contains only ιH ) contexts that are used when typechecking the initial
configuration S0 ; T0 guarantee that all functions in the program are closed and that no explicit region
values (rgnı ) or location values (locℓ ) are used in the source of the original program.

A Concurrent Language with a Uniform Treatment of Regions and Locks

92

8

Related Work

The first statically checked stack-based region system was developed by Tofte and Talpin [13]. Since
then, several memory-safe systems that enabled early region deallocation for a sequential language were
proposed [1, 12, 15, 7]. Cyclone [11] and RC [8] were the first imperative languages to allow safe
region-based management with explicit constructs. Both allowed early region deallocation and RC also
introduced the notion of multi-level region hierarchies. RC programs may throw region-related exceptions, whereas our approach is purely static. Both Cyclone and RC make no claims of memory safety
or race freedom for concurrent programs. Grossman proposed a type system for safe multi-threading
in Cyclone [10]. Race freedom is guaranteed by statically tracking locksets within lexically-scoped
synchronization constructs. Grossman’s proposal allows for fine-grained locking, but only deals with
stack-based regions and does not enable early release of regions and locks. In contrast, we support
hierarchical locking, as opposed to just primitive locking, and bulk region deallocation.
Statically checked region systems have also been proposed [3, 17, 16] for real-time Java to rule
out dynamic checks imposed by the language specification. Boyapati et al. [3] introduce hierarchical
regions in ownership types but the approach suffers from the same disadvantages as Grossman’s work.
Additionally, their type system only allows sub-regions for shared regions, whereas we do not have this
limitation. Boyapati also proposed an ownership-based type system that prevents deadlocks and data
races [2]; in contrast to his system, we support locking of arbitrary nodes in the region hierarchy. Static
region hierarchies (depth-wise) have been used by Zhao [17]. Their main advantage is that programs
require fewer annotations compared to programs with explicit region constructs. In the same track,
Zhao et al. [16] proposed implicit ownership annotations for regions. Thus, classes that have no explicit
owner can be allocated in any static region. This is a form of existential ownership. In contrast, we
allow a region to completely abstract its owner/ancestor information by using the hierarchy abstraction
mechanism. None of the above approaches allow full ownership abstraction for region subtrees.
Cunningham et al. [5] proposed a universe type system to guarantee race freedom in a calculus of objects. Similarly to our system, object hierachies can be atomically locked at any level. Unlike our system,
they do not support early lock releases and lock ownership transfers between threads. Consequently, their
system cannot encode two important aspects of multi-threaded programming: thread-locality and data
migration. Finally, our system provides explicit memory management and supports separate compilation.
The main limitation of our work is that we require explicit annotations regarding ownership and
region capabilities. Moreover, our locking system offers coarser-grained locking than most other related
works. The use of hierarchical locking avoids some, though not all, deadlocks.

9

Concluding Remarks

In this paper, we have presented a concurrent language emloying region-based memory management
and locking primitives. Regions and locks are organized in a common hierarchy and treated uniformly.
Our language allows atomic deallocation and locking of entire subtrees at any level of the hierarchy;
it also allows region and lock capabilities to be transferred between threads, encoding useful idioms of
concurrent programming such as thread-local data and data migration. The type system guarantees the
absence of memory access violations and data races in the presence of region aliasing.
We are currently integrating our system in Cyclone. In the future, we are planning to extend our type
system to achieve an exact correspondence between static and dynamic capability counts, and provide
deadlock freedom guarantees.

P. Gerakios, N. Papaspyrou, and K. Sagonas

93

References
[1] Alexander Aiken, Manuel Fähndrich & Raph Levien (1995): Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages. In: Proc. of the ACM SIGPLAN Conference on
Programming Language Design and Implementation. pp. 174–185.
[2] Chandrasekhar Boyapati, Robert Lee & Martin Rinard (2002): Ownership Types for Safe Programming:
Preventing Data Races and Deadlocks. In: Proc. of the ACM SIGPLAN Conference on Object-Oriented
Programming, Systems, Languages, and Applications. pp. 211–230.
[3] Chandrasekhar Boyapati, Alexandru Salcianu, William S. Beebee & Martin Rinard (2003): Ownership Types
for Safe Region-based Memory Management in Real-Time Java. In: Proc. of the ACM SIGPLAN Conference
on Programming Language Design and Implementation. pp. 324–337.
[4] John Boyland (2003): Checking Interference with Fractional Permissions. In: Proc. of the 10th International
Symposium on Static Analysis, LNCS 2694. Springer, pp. 55–72.
[5] David Cunningham, Sophia Drossopoulou & Susan Eisenbach (2007): Universe Types for Race Safety. In:
Proc. of the 1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs.
pp. 20–51.
[6] Cormac Flanagan & Martı́n Abadi (1999): Object Types Against Races. In: Proc. of the 10th International
Conference on Concurrency Theory, LNCS 1664. Springer, pp. 288–303.
[7] Matthew Fluet, Gregory Morrisett & Amal Ahmed (2006): Linear Regions Are All You Need. In: Proc. of the
European Symposium on Programming, LNCS 3924. Springer, pp. 7–21.
[8] David Gay & Alexander Aiken (2001): Language Support for Regions. In: Proc. of the ACM SIGPLAN
Conference on Programming Language Design and Implementation. pp. 70–80.
[9] Prodromos Gerakios, Nikolaos Papaspyrou & Konstantinos Sagonas (2009): A Concurrent Language With
a Uniform Treatment of Regions and Locks. Technical Report CSD-SW-TR-7-09, Software Engineering Laboratory, National Technical University of Athens. Available at http://www.softlab.ntua.gr/
~pgerakios/papers/reglock_techrep09.pdf.
[10] Dan Grossman (2003): Type-safe Multithreading in Cyclone. In: Proc. of the ACM SIGPLAN International
Workshop on Types in Languages Design and Implementation. pp. 13–25.
[11] Dan Grossman, Gregory Morrisett, Trevor Jim, Michael Hicks, Yanling Wang & James Cheney (2002):
Region-based Memory Management in Cyclone. In: Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 282–293.
[12] Fritz Henglein, Henning Makholm & Henning Niss (2001): A direct approach to control-flow sensitive
region-based memory management. In: Proc. of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. pp. 175–186.
[13] Mads Tofte & Jean-Pierre Talpin (1994): Implementation of the Typed Call-by-value λ -calculus using a Stack
of Regions. In: Proc. of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
pp. 188–201.
[14] David Walker, Karl Crary & Gregory Morrisett (2000): Typed Memory Management via Static Capabilities.
ACM Transactions on Programming Languages and Systems 22(4), pp. 701–771.
[15] David Walker & Kevin Watkins (2001): On Regions and Linear Types. In: Proc. of the ACM SIGPLAN
International Conference on Functional Programming. pp. 181–192.
[16] Tian Zhao, Jason Baker, James Hunt, James Noble & Jan Vitek (2008): Implicit ownership types for memory
management. Science of Computer Programming 71(3), pp. 213–241.
[17] Tian Zhao, James Noble & Jan Vitek (2004): Scoped Types for Real-Time Java. In: Proc. of the 25th IEEE
International Real-Time Systems Symposium. pp. 241–251.

