Reference Capabilities for Flexible Memory Management: Extended Version]Reference Capabilities for Flexible Memory Management: Extended Version

This extended version of the paper contains an appendix with the
full formal development and proofs. Citations should use the
original version of the paper <cit.>.

E. Arvidsson]Ellen Arvidsson

Information Technology
Uppsala University

E. Castegren]Elias Castegren

Information Technology
Uppsala University

S. Clebsch]Sylvan Clebsch

Azure Research

S. Drossopoulou]Sophia Drossopoulou

Department of Computing
Imperial College London

J. Noble]James Noble

Creative Research & Programming
New Zeeland

M. Parkinson]Matthew J. Parkinson

Azure Research

T. Wrigstad]Tobias Wrigstad

Information Technology
Uppsala University

is a concurrent object-oriented programming language
that organises

all the objects in a program into a forest of isolated regions.
Memory is managed

locally for each
region, so programmers can control a program's memory use
by adjusting objects' partition into regions, and by
setting each region's memory management strategy.

A thread can only mutate (allocate, deallocate) objects
within one active region — its “window of mutability”.
Memory management costs are localised to the active
region, ensuring overheads can be predicted and controlled.
Moving the mutability window between regions
is explicit, so code can be executed wherever it
is required,  yet programs remain in control of memory use.

An ownership type system based
on reference capabilities enforces region isolation,
controlling aliasing within and between regions,
yet supporting objects moving between regions and threads.
Data accesses
never need expensive atomic operations, and

are always thread-safe.

<concept_desc>Software and its engineering General programming languages</concept_desc>
<concept_desc>Social and professional topics History of programming languages</concept_desc>

[500]Software and its engineering General programming languages
[300]Social and professional topics History of programming languages

§ INTRODUCTION

Memory management has always been challenging, and programmers and
programming language designers have developed a wide range of
techniques and patterns to deal with it <cit.>. Most early
languages like FORTRAN and COBOL supported only fixed memory
allocation, where memory was allocated before a program began
to execute. Algol-60 popularised stack allocation, enabling
recursive procedures to be expressed clearly, and then languages like
C and Pascal popularised heap allocation, where programmers
could manually request memory from the runtime system, and
manually return that memory when it was no longer required.
LISP introduced the first automatic memory management
system—a garbage collector—which relieved programmers from the
need to explicitly free memory, rather memory will be automatically
reclaimed once it is no longer needed <cit.>.  As
well as reducing the amount of bookkeeping code programmers have to
write, garbage collection typically provides “memory safety” which
prevents a number of characteristic errors common to manual memory
management, such as failing to free objects that are no longer needed, or
accidentally freeing objects that are still in use.

While there is now a 60+ year history of research in garbage
collection algorithms and implementations, many programmers seem
resistant to using garbage collection, despite the
pitfalls of manual memory management. According to the TIOBE index
of programming languages <cit.>, about half out of the top
twenty programming languages eschew garbage collection, and rely
on various forms of manual memory management.
The 1st and 3rd of the top 25 Common Weaknesses in
CWE 2020–2022 are writing and reading outside of allocated memory and
using memory after freeing it is 7th. Memory leaks come in at 32nd and race
conditions 33rd <cit.>.

In short, manual memory management ( C/C++) is unsafe and
prone to errors but allows programmers to leverage domain
knowledge to optimise memory management. Some compile-time memory
management ( Rust) and automatic GC ( Java/C#)
avoids the memory unsafety, but instead leads programmers to write
unsafe code for a variety of reasons.
In Rust, programmers must use unsafe code to construct well-known
data structures, and object topologies without clear domination.
In Java, programmers use unsafe code <cit.> to leverage domain knowledge
to optimise memory management and to make GC performance more
predictable. In general, reasoning about the performance of
automatic GC is made difficult by the systemic effects of GC on
program performance and the heuristics which control when and how
GC is run.

§.§.§ Contributions

This paper introduces 's region system——and its
accompanying type system.  gives
programmers control over memory management costs by dividing a
program's heap into a flexible forest of independent regions.
Programmers can pick a suitable strategy for how memory in each
region is managed, irrespective of what other regions do. Within
each thread, the programmer explicitly moves a single “window of
mutability” through the region forest. The single window of
mutability makes clear which region each part of a program is
working within, and how the program affects that region, in
particular with respect to object liveness, and
also permits a flexible aliasing. As a region can only be made accessible through a single pointer,
programs become free of data-races by design, and cheap ownership transfer to
support reconfiguring the region topology is easy.
Memory management overheads ( tracing, and reference count
manipulations) are likewise localised to just the mutable region.

§ BACKGROUND

The continuing appeal of manual memory management

highlights the research problem we aim to solve:
how can languages give programmers the level of
control offered by manual memory management, while maintaining
memory safety? Two broad research streams tackle
this problem, one based on regions and one based on

§.§.§ Regions

<cit.> introduced explicit
regions for managing memory in C-like languages: objects are
allocated in regions; and entire regions of objects are deleted in
one operation, rather than deleting objects individually. A later
version of this scheme added annotations to indicate that a
pointer refers to an object in the same region, in an enclosing
region, or is not allocated via the region
system <cit.>. <cit.> had previously shown
how regions could help local reasoning, based on
the “collections” or “local stores” used to differentiate
pointers in Euclid <cit.>.

Rather than using explicit, programmer-visible regions, Tofte and
Talpin  demonstrated how Milner-style
inference <cit.> could be extended to implicitly
allocate objects to regions, and allocate and deallocate those
regions, without either explicit first-class regions, or
additional annotations on programs or types. Their
MLKit <cit.> runs ML programs using stack allocation,
as the regions are allocated last-in, first-out. Because these
inferred regions are implicit, the region structure does not
capture a programmer's intent about how and where memory should be
allocated and freed. MLKit remains under continuous
development, in particular showing how regions can be supported in
a straightforward monadic style <cit.>, and
integrating generational-style GC within
regions <cit.>.

Safe region allocation was then tested at scale in
Cyclone <cit.> an extension of C
with an explicit region construct, rather than using
inference. Like the MLKit, Cyclone regions were originally stack
based; later versions also adopted support for unique pointers and
reference counted objects to permit deallocation of individual
objects inside a region, at the cost or introducing memory leaks
due to cycles or failure to deallocate a dropped unique
pointer <cit.>. Both MLKit style implicit /
inferred regions, and Cyclone explicit / annotated regions can be
modelled by a common core calculus based on linear references to
explicit, first-class
regions <cit.>.

§.§.§ Ownership

Work on object ownership effectively begins with Hogg's
Islands  and a general
recognition of the need to control topologies of programs <cit.> in
languages where object identity ( dynamic allocation, mutable
state), encapsulation, and even “automatic storage management”
are taken as essential design principles, rather than accidental
optimisations <cit.>.

Based on “Flexible Alias Protection”
<cit.>, ownership
types <cit.>
compile-time enforcement of pointer encapsulation, including the
property that, considering paths through the object graph, an
“owner” object should dominate all other objects that programmers
intend to encapsulate “inside” it <cit.>.

Leveraging “owners-as-dominators”, extensions to ownership types
have been applied to encapsulate object
invariants <cit.>, record conformance to
software architecture <cit.>, localise
program effects <cit.>, scope object
cloning <cit.>, ensure actor
isolation <cit.>,
prevent data races <cit.>, support safe
parallelisation <cit.> or ensure data is only accessed
under a mediating lock <cit.>—the first
fifteen years of these efforts are surveyed
in <cit.>. Owners-as-dominators leads
directly to applications in memory management, as deleting a
dominating node from a graph, by definition, must also delete
every node it dominates. This was first demonstrated in
SafeJava <cit.> using ownership types to compile
straightforwardly annotated programs to the Real-Time
Specification for Java <cit.>, which supports fine-grained
control over memory via explicit dynamically-scoped regions.

Distinguishing between the inside and outside of an encapsulated
object lets languages generalise traditional pointer-based
uniqueness to external uniqueness
<cit.>, where an object may have only one
pointer from the outside, but any number of pointers from its
inside. As with regions for unique objects, an externally unique
object can be represented as the sole object in a region; however
for external uniqueness, the object's region can also contain one
or more enclosed subregions in turn containing the object's
insides. External uniqueness is almost as strong as regular
uniqueness <cit.>, and in particular
makes it easier to change objects' ownership, or dually, to
transfer objects between actors or independent threads

§.§.§ Rust

Regions and ownership have been brought together recently in the
design of Rust, combining control of memory use, safe concurrency,
and excellent compiler error messages <cit.>. Rust essentially inherits
Cyclone's and MLKit's regions, but strongly integrated with
uniqueness. In particular, only values which are uniquely
referenced or passed by copy are mutable. Nested uniqueness brings
nested ownership: a unique value is owned by its storage
location, ensuring that when an owner is deallocated, all the
memory owned by that owner can also be deallocated.

To make programming in Rust practical, Rust allows unique values
to be borrowed without nullifying their source: a unique mutable
reference can be passed up the stack without losing
uniqueness <cit.> or traded for multiple
read-only borrowed references <cit.>. To
ensure absence of dangling pointers, Rust tracks lifetimes of
borrowed references and ensure that a “longer-lived” (or
enclosing) object can never point to a “shorter-lived” (or
encapsulated) object. This borrowing semantics is reminiscent of
fractional permissions <cit.>. Through
uniqueness, Rust imposes a multiple-reader/single-writer
concurrency model <cit.>.

The strict rules surrounding ownership and borrowing, and
compilers' inability to accept safe programs that they “cannot
understand”, make Rust hard to learn and to use
correctly <cit.>—to the point where the difficulty of implementing
first-year data structures (such as doubly-linked lists) has now
become an Internet trope <cit.>. When faced with these problems in practice, Rust
programmers either escape into unsafe Rust or revert to the
birthplace of aliasing, using integer array indices, FORTRAN
style <cit.>.

§  REGIONS

In this section we describe
the central concepts of the  region system:
the region topology,
operations on regions,
the single window of mutability,
and the properties of the region system.
But first, let us overview the goals of this work.

§.§ Motivation

The design decisions in this paper are motivated by our primary goal:

* Controllable and Predictable Memory Management

It should be possible for a programmer to reason about and
control the impact of memory management on performance.

Our approach is to divide a program's heap into isolated regions and
make each region an isolated unit of memory management. Concretely, we
set the following five sub-goals:

* Mix-and-Match Memory Management.

A region is free to manage its own memory however it likes, irrespective of any other regions in the program.

Thus, a programmer is free to pick a memory management strategy suited to the needs of particular operations.

* Incremental Memory Management.

Performance of memory management in one region should not be affected by activities in another region.

Thus, fine-grained partitioning gives finer cost-control.

* Zero-Copy Ownership Transfer.

Ownership transfer between regions must be possible without copying objects.

Thus, fine-grained partitioning does not have a hidden expensive cost, and heap topology can be modified cheaply.

* Concurrent Memory Management.

Timing of memory management in one region should not be contingent by activities in another region.

Thus, a programmer can initiate an operation—memory management or not—without having to wait, or forcing a wait upon any other part of the program.

* Safe Concurrency.

A thread that has access to a datum may access it freely without any need for synchronisation, and with a guarantee of data-race freedom.

Because this paper does not deal explicitly with concurrency, we
will refrain from discussing the last two goals until

§.§ High-Level Overview

We distinguish between mutable and immutable objects. In this
paper, we are mostly concerned with the former. Immutable objects
do not live in regions, and can be accessed freely in a program.
In contrast, every mutable object belongs to a particular region.
In certain circumstances, mutable objects may be made
temporarily immutable. To avoid confusion, we will
sometimes use the phrase permanently immutable to denote
objects whose mutability is irretrievably lost.

§.§.§ Regions and Region Topology

A region is a set of objects whose memory is managed together. At
any moment, one of these objects is designated as the
bridge object. A region can be opened or
closed. Closed regions are isolated from the rest of the
program which means that with the exception of the bridge object,
objects in a closed region are only referenced from within the
region. Bridge objects are externally
unique <cit.> so they may have an additional,
single external incoming reference.

The only outgoing references from objects in a region are either
to immutable objects or to bridge objects of other (nested) regions.
Thus, a program's region topology forms a forest,
and moving the external reference to the bridge object changes the
topology. The topology of references within regions
is unrestricted: any object can point to any other within the
same region.

Region isolation of two closed regions.

<ref> illustrates the isolation of the region $R$
(bean-shaped boundary). Object $a$ is the current bridge object of
the region, denoted by drawing it on the boundary. Also $c$ and
$e$ could serve as the bridge object. References en and me are not
permitted as they break isolation. The reference from ai is permitted as $i$ is
immutable. The reference ma is permitted because $a$ is the current
bridge object. Immutable objects do not live in regions and may
only refer to other immutable objects. Therefore, the reference
oa is not allowed. Last, bridge objects may only have one
incoming reference from outside the region, so no more references
to $a$ are allowed from outside of $R$, regardless of their

§.§.§ Regions and Memory Management

Every region manages the memory of its objects in isolation, and
according to a strategy picked by the programmer specifically for
that region at the time of its creation. Code inside of a region
is agnostic to how memory is managed, meaning that a library can
leave such decisions to its users.

When an external reference to a bridge object is dropped, the
entire corresponding region can be free'd along with any nested
regions. In <ref>, dropping ma makes all
objects in region $R$ unreachable as external references to its
objects ( me) are not permitted. Thus, they can be
collected immediately.

§.§.§ Single Window of Mutability

A region must be explicitly opened to be accessed, and must be
closed before it can be opened again. The open regions form a LIFO
stack. The top region is active and the remaining regions
on the stack are suspended. An active region permits
allocation, deallocation and mutation of its objects. When a
region is suspended, neither allocation, deallocation nor mutation
is permitted in it.

Making a region active temporarily weakens its outgoing
encapsulation: its objects are permitted to reference objects in
the suspended regions further down the stack. Suspending a region
conversely weakens its incoming encapsulation: its objects
can be referenced by the regions further up the stack.
<Ref> overviews the allowed actions depending on a
whether a region is active, suspended or closed. When the active
region is closed, it is popped from the stack, and the new top
region goes from suspended to active. Because closed regions are
not permitted outgoing refereces, any references to objects in
open regions must be invalidated.

To the active region, the suspended regions appear as a single
temporarily immutable region whose objects can be
referenced as long as the active region remains on the stack. Programmers
can thus trade mutability for access, and any object can
be temporarily accessed from anywhere, provided the containing
regions are opened on the stack in a permitting order.

Allowed actions depending on a region's state. Incoming
and outgoing denote references to mutable objects from and to other regions respectively.
Bridge means only to bridge objects; any$^*$ means to any object
of a previously (outgoing) or subsequently (incoming) opened
region. Free object denotes ability to free individual objects
inside of a region. Free region denotes the ability to free an
entire region.

2cEncapsulation     2cEffects     3cMemory Management     Nested

State     Incoming                           Outgoing                     Mutate                                 Read     Alloc object     Free object     Free region     Regions

active	      bridge                                 any$^*$                              yes                                        yes          yes               yes              no               yes

suspended	    any$^*$                                    any$^*$                              no                                         yes          no                no               no               yes

closed	      bridge                                  bridge                           no                                         no           no                no               yes              yes

In <ref>, to open $R$ we must first
open $R'$ to access the reference ma. Opening $R$
through this reference suspends $R'$, making $m$ and $n$
temporarily immutable, $a$, $c$, and $e$ mutable, and permitting
en. With the topology of <ref>, we cannot
open $R$ and $R'$ in a way that permits the creation of me
as $m$ is immutable when $R'$ is suspended, and $e$ is not
accessible when $R$ is closed. To do so, we must change the
topology by moving ma out of $R'$,  to a stack
variable or other region.

In combination, the design decision to only permit mutation in one
region at a time, the LIFO order of the region stack and the
inaccessibility of closed regions facilitates reasoning about
side-effects. The main motivation, however, is to control the
costs of memory management. As we shall see, direct overheads
related to memory management such as maintaining reference counts
or tracing object structures are only applicable to active

§.§.§ Navigating Through the Region Forest

Left: $R'$ is active and $R$ is closed.
Right: we opened $R$ making it active and suspending $R'$.

Due to the single window of mutability, programs require explicit
navigation through the region forest. The left subfigure of
<Ref> shows
<ref>, denoting regions' states by colour when $R'$
is active and $R$ is closed. The white box denotes the stack frame
of $R'$ with its local variable(s).

If we proceed by opening $R$ we
arrive at the right subfigure of <Ref>: a
new top frame is created inside $R$ containing its own local
variables, with y̧ holding a reference to $a$; $R'$
is suspended and $R$ active, and the window of mutability is moved
from $R'$ to $R$. The reference zm shows the weakened
isolation allowing outgoing references from $R$ and incoming
references to $R'$.

To continue, we may close $R$ or open any reachable region $R''$. The former
will invalidate any references from $R$ to $R'$ since these would violate
isolation. The latter gives mutable access to $R''$ and suspends $R$, and
permits references from $R''$ to both $R$ and $R'$.

Examples of bridge swapping. Time moves left; we use different shades of blue for clarity. Subfigures 1–3 construct the cyclic
linked list $[a,b,c]$, using the most recently added link as the bridge object.
Subfigures 4–6 construct an iterator, for the list, and make it the bridge object. We
subsequently use the iterator to iterate to the $b$ link and unlink it, before dropping the
iterator and making $a$ the bridge object (and with a garbage iterator whose
removal is determined by the region's memory management strategy).

§.§.§ Swapping the Bridge Object

Any object in a region can serve as the bridge object. While a
region is open, any object can be designated as the new bridge
object, and we make this choice visible when the region closes.
Thus, it is possible to  create a region with a stack where
the bridge object is always the top link. If we wish to create an
external iterator to the stack, we can create an iterator inside
the region, and make the iterator the bridge object for the
duration of the iteration, and then switch back again.
<ref> shows the situation pictorially.

§.§.§ Merging and Freezing Regions

A closed region's contents may be merged into another region by dropping
the uniqueness of the bridge object. For clarity, we use an
explicit merge operation.

<Ref> shows merging $R'$ into $R$, which moves the objects in $R'$
into $R$ and creating the (now legal) ab reference from the variable
x̧, after which $R'$ ceases to exist. Merging a region (source) into
another (sink) moves all regions directly nested in the source to the sink, but
does not merge those regions into the sink (see $R''$ in <Ref>).

Permanently immutable structures are created by constructing a mutable region
and then turning its entire contents immutable through
an explicit freeze operation that operates on closed regions.

In contrast to merging, freezing a region also freezes its nested
regions (see <ref>). This preserves the property that immutable objects may
only reference other immutable objects. Freezing dissolves region
boundaries, making the frozen objects freely accessible to objects
in all regions.

Left: Three nested regions $R$, $R'\!$, and $R''$. Centre: Merging region $R'$ into $R$. Right: Freezing $R'$.

§ REFERENCE CAPABILITIES FOR STATICALLY ENFORCING REGION ISOLATION

We now introduce a type system that statically enforces region
isolation according to the encapsulation and effects
columns of <ref>. A region is opened through an
ȩņţȩŗ operation that takes a reference to bridge object and a
lambda, executes the lambda inside the region passing it the
bridge object as argument, and then closes the region. Its
companion operation ȩx̧p̧ļo̧ŗȩ opens a region in a suspended state
(while still suspending the former active region).

Our type system uses reference
capabilities which decorate all types $\tau$ in a program:

*  $\tau$ denotes an intra-regional reference to an object of type $\tau$ (ŗ, ç, ȩ,
and m̧ in <ref>);

*  $\tau$ is like  $\tau$, but the lifetime of
the object is bound to the ȩņţȩŗ/ȩx̧p̧ļo̧ŗȩ scope;

*  $\tau$ denotes a reference to a permanently immutable
object of type $\tau$ (i̧ and o̧);

*  $\tau$ denotes an externally unique reference
to a bridge object of type $\tau$ of a closed
region (a̧);

*  $\tau$ denotes a reference to an immutable
object in a suspended region (z̧ in

On assignment, the lhs capability and the rhs
capability must be the same. m̧ȩŗģȩ has the signature
$\to$ and f̧ŗȩȩz̧ȩ has the signature $\to$.
To ȩņţȩŗ or ȩx̧p̧ļo̧ŗȩ, an  is needed.

All expressions are typed from the point of view of the currently
active region. A field f̧ declared with a  capability
will only appear as such when the object $o$ containing f̧ is
in the active region. If $o$'s containing region is suspended,
f̧ will also appear as suspended; if $o$'s containing region is
closed, f̧ is not even visible to the program. This is handled
by viewpoint adaptation ( <ref>).

An invariant in our system is that aliases to an object that are
accessible simultaneously have the same capability. This
design is motivated in-part by region isolation and in-part by a desire
to keep complexity down in this presentation. For example: If a
and  could alias, the immutability of the latter
would be weakened to read-only. If  and  could
alias, it would violate the temporary vs. permanent nature of
their immutability. (This restriction could be relaxed to permit
some aliasing across the mutable capabilities and aliasing across
immutable capabilities.)

[style=tinyverona,numbers=right,caption=Code creating the region $R$ from $R'$ as depicted in <ref>.,label=lst:isolation]
// Freeze creates immutable objects, c.f. (*@<ref>@*)
let i = freeze new iso Cell(42) (*@@*)
let o = freeze new iso Cell(i) (*@@*)
let a = new iso Link // creates R (*@@*)
//  r $\textcolor{blue}{\Rightarrow}$ ...  is a lambda with argument r
enter a  r (*@$\Rightarrow$@*) let c = new mut Link (*@@*)
let e = new mut Link (*@@*)
r.elem := i
r.next := c
c.next := e
e.next := r  (*@@*)
let m = new mut Cell(a) // buries a (*@@*)

Constructing <ref>

<ref> shows code that
creates the regions, objects, and (permitted) references of
<ref>. Line <ref> creates the $R$ region.

On Line <ref>,
the immutable object $i$ is constructed by creating a region and
freezing it. The object $o$ is created similarly. Its reference to
$i$ does not break region isolation as $i$ is immutable. We could
get rid of the f̧ŗȩȩz̧ȩ on Line <ref> since
Line <ref> moves $i$ into $o$'s region and then
freezes the entire structure.

When a region is created, it is closed and empty, except for its
bridge object. To populate $R$ as in <ref>, it must
first be made active. The ȩņţȩŗ keyword is used to open a
region and making it active. It takes a unique reference to a
bridge object as its argument. Lines <ref>–<ref>
of <ref> show the use of an ȩņţȩŗ block to open
the $R$ region to allocate and mutate its objects. (The code executes with region $R$ active and region $R'$

Entering a region moves control inside it and places a
reference to its bridge object in a variable on the stack (ŗ)
that can be used to call methods, or obtain and store references to other
objects in the region. Exiting the ȩņţȩŗ block (after
Line <ref>) closes the region, and moves control back to
the previous region. While a region is open, the external
reference to its bridge object is
buried <cit.>, meaning it is not accessible to
the program.

Upon exiting the ȩņţȩŗ block, all variables referencing
objects in the now-closed region (ç, ȩ, and ŗ) are
invalidated, save for the reference to the bridge object in a̧.
Any temporarily permitted references to objects in suspended regions,
such as en in <ref>, will be invalidated as well. (We will show how
this is enforced statically in <ref>.)

§.§ Controlling Effects through Viewpoint Adaptation

Viewpoint adaptation.

If the capabilities of x̧ and f̧ are $\alpha$ and $\beta$,
then the capability of x̧.̧f̧ is $\VPA{\alpha}{\beta} = \gamma$,
which we read as “$\alpha$ sees $\beta$ as $\gamma$.”

For $\dag$,  <ref>.
The meaning of $\bot$ is inaccessible;
For $\bot$/ see text.

Capabil-     5cCapability on f̧

ity on x̧

$\dag$          $\bot$/     $\dag$

We rely on viewpoint adaptation <cit.> to
capture how a reference's type changes depending on its enclosing
region's relation to the active region. Viewpoint adaptation
means that the type of an object may appear differently depending on
from where it is accessed. For example, when accessed through a
variable of type , a field declared with type  appears
as . (This particular case  ensures
that turning a unique reference to a bridge object immutable will
propagate the immutability to the entire region and nested

Viewpoint adaptation also changes the types of variables captured
by an ȩņţȩŗ or ȩx̧p̧ļo̧ŗȩ block to propagate suspension.
Captured s retain their -ness rather than become
. <ref> shows the viewpoint adaptation rules.

The meaning of $\bot/\Iso{}$ is that an  location is
inaccessible through a ,  or ,
unless it is swapped, buried or borrowed
( <ref>).

To illustrate viewpoint adaptation,
consider $̧\̧Şço̧p̧ȩA̧\̧ ̧$̧ ̧ȩņţȩŗ ̧x̧ ̧{̧ ̧y̧ ̧$̧\̧ ̧\̧Ŗi̧ģḩţa̧ŗŗo̧w̧ ̧$̧ ̧ ̧ ̧ ̧$̧\̧ ̧\̧Şço̧p̧ȩB̧\̧ ̧$̧ ̧ ̧ ̧}̧.
In scope , let the
variables x̧ and v̧ have the types $\Iso{}~\tau_1$ and
$k~\tau_2$ respectively.

In scope , x̧ is undefined and y̧ is introduced
with type $\Mut{}~\tau_1$. This reflects the region pointed to by
x̧ going from closed (denoted by x̧ being ) to active (denoted by y̧ being ).

Moving control from  to  suspends the region active in
(denoted there by  and ). Thus, in scope , the type of v̧ is
$(\VPA{\Paused{}}{k})~\tau_2$. Through a  reference,
objects in the same region are .
and  references stay  and  respectively
(permanently immutable is stronger than temporarily immutable).
references stay . This
permits opening nested regions of a suspended region.

If $k$ = , then v̧.̧f̧ is not typeable in neither
nor  as $\VPA{\Iso}{k'}=\bot$, regardless of what $k'$
(the capability of f̧) is. This is as expected, as 's
cannot be dereferenced (they must be ȩņţȩŗ'd).

§.§ Region Isolation and Bridge Object External Uniqueness

Regions which are closed or active only have a single incoming
reference, which goes to the bridge object. Thus, when a region is
closed, it can be moved in and out of other regions by moving its
single incoming reference. When a region is opened, its containing
region is suspended, which means that the object containing field
holding the reference to the bridge object is  so the
field cannot be reassigned. Thus, regions cannot move while open.
Finally, when a region is suspended, incoming references are
permitted from the stack and heap of subsequently opened regions
( <ref>). As regions are opened using a lexically
scoped construct (ȩņţȩŗ or ȩx̧p̧ļo̧ŗȩ), regions are opened
and closed in LIFO order. This means that when a suspended region
becomes active again, the permitted incoming aliases that could be
declared in the block have gone out of scope, and the region's
bridge object is again the only incoming alias.

As shown in <ref> uniqueness of bridge object references
is maintained by a combination of swapping, burying, and borrowing.

Maintaining uniqueness of bridge object references.

Swap<cit.>     Reading a mutable variable containing an  requires that its contents is replaced. For example, y̧ ̧=̧ ̧x̧ is not permitted when x̧ is . However, y̧ ̧=̧ ̧x̧ ̧=̧  $v$ is, which replaces the value of x̧ by the value $v$ and moves the previous value of x̧ into y̧.

Bury<cit.>     Reading a let-bound variable with an  invalidates the variable. For example, f̧o̧o̧(̧x̧,̧ ̧x̧)̧ is not permitted when x̧ is  as the second use of x̧ cannot be typed.

Borrow<cit.>     Dereferencing an  requires opening its region, where aliasing of the bridge object is unrestricted, and region isolation protects aliases to the bridge object from escaping.

Entering a region borrows and/or buries the variable or field
referencing the bridge object. In the case of a stack variable,
the variable is buried to prevent the region from being multiply
opened. In the case of a field, we instead resort to a dynamic
check of the region's state. If the region is closed, it may be
opened. If the region is already open, an exception is thrown.

§.§ Temporary Objects Allow References to Suspended Regions on the Heap

As exemplified already, we permit local variables to store references to
objects in a suspended region ( z̧ in
<ref>). This is sound as objects in
suspended regions are immutable, and because local variables in
the active region are guaranteed to go out of scope before a
region opened by an enclosing ȩņţȩŗ or ȩx̧p̧ļo̧ŗȩ becomes
active (and thus mutable), as explained above.

Because objects with  capability are created in, and bounded
by, a lexical scope, they have the same lifetimes as local
variables declared therein. Therefore, we can grant the same
permissions to store references to suspended regions to
objects. We permit accessing  and  fields through a
, but not through a  (as shown in <ref>).
Permitting a  object to store a suspended reference could
lead to a breach of region isolation (see
<ref> for an example). Thus from
$\VPA{k_1}{k_2}=\Tmp{}$ it follows that $k_1=\Tmp{}$.

In terms of <ref>, making $e$ a temporary object
allows its fields to store references with  capability. This
permits the reference en when $R$ is active and $R'$ is
suspended. However, ce would no longer be permitted unless
$c$ is also , etc.

§.§ Storage Locations, Strong Updates and Bridge Object Swapping

We unify the treatment of mutable variables (denoted v̧a̧ŗ as
opposed to ļȩţ) and fields through a storage location
abstraction (similar to a pointer to a variable or field in C).

Storage locations are typed $k$  where
$k$ is the capability of the frame or object containing the
location and $k'$ is the capability of the value stored at the

We add a new capability that we call  for use in mutable
local variables.  differs from  in that it supports
strong updates. Its viewpoint adaptation rule is
$\VPA{\Var}{k}=k$ (“ sees $k$ as $k$”).

As shown in <ref>, a mutable local variable x̧
holding a $\tau$-typed value has the type v̧a̧ŗ
Şţo̧ŗȩ[̧$̧\̧ţa̧u̧$̧]̧. Storage locations are subject to the normal
rules for viewpoint adaptation, so opening another region when
x̧ is already in scope will change the type of x̧ to
p̧a̧u̧şȩḑ Şţo̧ŗȩ[̧$̧\̧ţa̧u̧$̧]̧. We introduce a dereference operator
*̧ and an update operator :̧=̧ to access the contents of a
storage location.

A storage location must be , , or  to be

We apply viewpoint adaptation to type the result of dereferencing.
On Line <ref>, *̧x̧ has type
($\VPA{\Paused}{\Mut}$) Çȩļļ,  p̧a̧u̧şȩḑ ̧Çȩļļ.

[numbers=right,firstnumber=1,caption=Storage locations example.,label=lst:store]
var u = new iso Cell(42) // (*@var Store[iso Cell]@*)
var x = new Cell(4711) // (*@var Store[mut Cell]@*)
enter u  y $\Rightarrow$
// y has type (*@var$\,$Store[mut Cell]@*)
// x has type (*@paused$\,$Store[mut Cell]@*)
y := new Foo(*y) // changes bridge object('s type) (*@@*)
y := *x // (*@rejected:@*) *x is (*@paused$\,$Cell@*), not (*@mut$\,$Cell@*) (*@@*)
x := ... // (*@rejected:@*) the x storage location is (*@paused@*)
// change to u becomes visible

We support changing the bridge object of a region—including
changing it for an object of a different type—by presenting the
borrowed bridge object reference internally in the ȩņţȩŗ block
as a  storage location. (Note that it is not possible to
update the bridge object in an ȩx̧p̧ļo̧ŗȩ as it opens the region as

Line <ref> shows that changing the bridge
object to an object of another type is possible by simply
assigning to y̧. Strong updates of fields are not possible,
and this is handled by using ţm̧p̧ Şţo̧ŗȩ[̧$̧\̧ļḑo̧ţş$̧]̧ instead of
v̧a̧ŗ Şţo̧ŗȩ[̧$̧\̧ļḑo̧ţş$̧]̧ to type a bridge object reference
borrowed from a field as opposed to a stack variable.

§.§ Types Enforce Region Isolation and the Single Window of Mutability

Region isolation means no references into active
or closed regions from other regions (modulo unique
references to bridge objects) or from immutable
objects, and no outgoing references from closed
regions to open regions. Let's see how our types enforce this, by
looking at $R$ in <ref>.

The newly created region $R$ (Line <ref>) is isolated as
constructors only accept 's and 's as arguments.

Right after creation, $R$ is closed, and its only
external reference is . Since 's cannot be the
receivers of method calls or field accesses, we cannot read or
write internal objects in $R$, so we cannot create the illegal
references me or en.

When $R$ is active (Line
<ref>–<ref>), all previously suspended regions
stay suspended (none in <ref>), and are joined by
the current region ($R'$). This is captured by viewpoint
adaptation which changes all variables which are , ,
or  in the enclosing region to . This prevents
these variables from being updated, and reading them yields
references. Field updates via  or
references are not allowed, and method calls on
such references require that the method's self type matches the
external view, meaning any callable method cannot perform a field
update on şȩļf̧ (or call such a method). Thus, we cannot create
me or oa.

As permitted by our definition of region isolation, we may store
references in the fields of  objects in $R$ while
$R$ is active ( en if $e$ is created as  on
Line <ref>). These references will be invalidated when
$R$ closes as  references can only be stored in variables
local to the ȩņţȩŗ block (since mutable variables in the
enclosing scope have been suspended), or in other  objects
( $a \to c \to e$ is an impossible path if $e$ is , as
the $a$ object is  by definition).

If we did not invalidate references into suspended regions such as
en, we could circumvent region encapsulation. For example,
imagine closing $R$ (without invalidating en), then
closing $R'$ while moving $R$ out of $R'$. Then reopen $R$ without
first opening $R'$. Now en would constitute a reference into
the internals of a closed region, thereby breaking region

Inside an ȩņţȩŗ or ȩx̧p̧ļo̧ŗȩ block the enclosing scope is
immutable. Together with region isolation this gives that only one
region at a time is mutable,  a “single window of

Last, region isolation means that reassigning the pointer to the
externally unique bridge object effectively changes the region
topology of the heap <ref>.

§ THE USE OF REGIONS FOR MANAGING LIVENESS

We have sketched how our type system enforces region isolation and the single window of mutability.
In this section, we will show how this translates to costs for managing liveness when considering
memory management in isolated regions.

<ref> shows a heap consisting of regions
$R_1$ to $R_6$.

Presently, the program has entered $R_1$, $R_2$, $R_3$ and $R_4$
in that order. Ignoring method call
indirections, we can imagine a corresponding program shape starting in $R_1$:
$̧\̧Şço̧p̧ȩŖ{̧1̧}̧\̧ ̧$̧ ̧ȩņţȩŗ ̧x̧ ̧{̧ ̧ḑ ̧$̧\̧ ̧\̧Ŗi̧ģḩţa̧ŗŗo̧w̧\̧ ̧\̧Şço̧p̧ȩŖ{̧2̧}̧\̧ ̧$̧ ̧ȩņţȩŗ ̧ȩ.̧f̧ ̧{̧ ̧f̧ ̧$̧\̧ ̧\̧Ŗi̧ģḩţa̧ŗŗo̧w̧\̧ ̧\̧Şço̧p̧ȩŖ{̧3̧}̧\̧ ̧$̧ ̧ȩņţȩŗ ̧ȩ.̧ģ ̧{̧ ̧ģ ̧$̧\̧ ̧\̧Ŗi̧ģḩţa̧ŗŗo̧w̧\̧ ̧$̧ ̧ ̧ ̧ ̧$̧\̧ ̧\̧Şço̧p̧ȩŖ{̧4̧}̧\̧ ̧$̧ ̧ ̧ ̧}̧ ̧ ̧}̧ ̧ ̧}̧.

Program with 4 open and 2 closed regions.

The region stack is thus [$R_4$, $R_3$, $R_2$, $R_1$] where
$R_4$ is active. Region isolation prevents references from objects in region $i$ to objects
in region $j$ if $i < j$ with the exception of the bridge object
references: d, ef, and eg. The
first of these is made inaccessible right after the first ȩņţȩŗ
by making x̧ undefined in 2 and nested scopes. While
$R_4$ is open, $R_2$ and $R_3$ are suspended, meaning the fields
holding ef and eg cannot be reassigned (static
check). Furthermore, they cannot be dereferenced ( opened)
since the regions are already open (dynamic check). Thus, while
$R_4$ is open, the incoming references to the bridge objects will
remain the same,  the path that holds the region alive is
stable.[Since an enter block can change the
bridge object on exit, the incoming reference does not affect
liveness. We can think of the incoming bridge object reference
as being invisibly nullified during the enter, and
reinstated at the exit.]

Because of this, as long as $R_4$ remains active, liveness of objects in regions $R_1$–$R_3$
and $R_5$ is invariant as no activity in $R_4$ can cause
objects in these regions to become garbage.[Every
reference in $R_4$ to an object in $R_1$–$R_3$ is a copy of a
reference inside one of those (immutable) regions that still
exists.] This does not hold for $R_6$, as $R_4$ could drop
hi to make the entire region $R_6$ garbage. It does
hold for bc however, since $b$ is in a suspended region ($b$ is
temporarily immutable).

Furthermore, because of the absence of references from $R_1$–$R_3$
into $R_4$—with the exceptions of the stable bridge object
references that are either buried or cannot be re-opened, objects in $R_1$–$R_3$ cannot affect the
liveness of objects in $R_4$ (this is also true for $R_5$ and
$R_6$ as they are closed). Thus, we can safely ignore references
to objects in suspended regions when managing liveness. For
example, if objects in $R_1$, $R_2$ or $R_3$ are managed by
reference counting, we do not need to increment or decrement
reference counts when manipulating  references
in $R_4$. Similarly, if objects in $R_1$, $R_2$ or $R_3$ are
managed by a tracing GC, tracing in $R_4$ does not need to follow
references. Thus, when managing memory in the
active region, we can safely ignore any outgoing references, and
so it is possible for $R_1$–$R_3$ to use different strategies,
unbeknownst to $R_4$ and irrespective of how $R_4$ manages its
memory <ref>. The only references to objects in
$R_5$ and $R_6$ that are possible (given that the regions are
closed) are to the bridge objects $c$ and $i$. Aliases of $c$ are
not possible in $R_4$ as  references are unique, and we
cannot transfer references out of an immutable $b$. However, we do
need to track liveness of the reference to $i$, which is possible
to do statically  as in Rust.

From the reasoning above it follows that liveness of objects in $R_4$
can be determined by looking at objects in $R_4$ alone, meaning
that the costs of memory management are determined by the contents
of and activity in $R_4$ <ref>. This makes it possible
to collect garbage in just $R_4$ <ref>.

§ PROGRAMMING WITH  REGIONS

As an example of how regions enable predictable memory
management performance, consider the server application “Po” with
the following key characteristics (see <ref> for skeleton code):

* The server serves incoming requests. Tasks that process
requests are short-lived and their side-effects are typically in
the form of data stored in a database.

* Responses to requests are served from data in an in-memory
key–value store implemented as a skip list. This storage will
shrink and grow continuously during execution.

* Values in the store can have a complicated graph-like
structure ( they may contain cycles).

We now explain how we can express this, and compare with
Cyclone, MLKit, Pony, and Rust.

§.§.§ Processing Requests

To manage allocations necessary to process a request, each request
is wrapped in a region (Line 16, Line 49). These regions use
arena allocation: allocations in the region persist until
the region itself is deallocated. This gives cheap bump-pointer
allocation and fast deallocation of the entire region once the
response has been computed. If a request must be processed by
different threads, this can be done cheaply due to the
transferability of 's. If some requests turn out to require
considerable processing time, their corresponding regions might
switch away from arena allocation at the small cost of changing one
annotation at the creation site of the region(s).

Cyclone's LIFO regions are perfect for this purpose (as are
MLKit's, provided that the inference engine infers according to
intentions, or better). While Cyclone does not support switching
from arena allocation, it does permit manually managed reference
counts or unique objects that can be manually deallocated during
the arena's lifetime. Pony only supports memory management on a
per-actor level, (using tracing GC). We could make each request an
actor, but it would have to communicate asynchronously with all
surrounding state. Rust does not support regions, but could
build a unique object holding unique values and thread this object
through computation. While more complicated, Rust's values would
have individual lifetimes.

§.§.§ Key–Value Store

The key–value store is implemented as a single region containing
a skip list (Line 5, could as well be a hash table, B-tree, etc.).
As it is a large long-living data structure of objects with
different lifetimes, arena allocation is not a suitable strategy.
Furthermore, if the resources (values) stored in the skip list are
costly, reference counting is a good choice as it allows
the resources in the list to be recycled immediately when they
become garbage. Alternatively (the path we chose) is to make each
element a region of its own, with independently managed memory (Line 1).

If the store is large enough to warrant parallel
accesses, it can be divided into several smaller regions with one
list each. For a compile-time guarantee that no reference count
manipulations in the skip list are needed during lookups, lookups
can be implemented using ȩx̧p̧ļo̧ŗȩ rather than ȩņţȩŗ as the
former opens the skip list region directly as  (Line 23,
and its dynamic extent f̧o̧o̧(̧)̧). Note that since the elements in
the skip list are regions of their own, these can be entered
separately and thus mutated, even if the list structure
is immutable (Line 35).

Cyclone's dynamic regions are a good fit for the key–value store.
The objects that make up the skip list would require manual
reference counting, which can be laborious. Failure to properly
manage reference counts in Cyclone will also lead to “memory
leaks” which will not be reclaimed until the region holding the
store is (manually) destroyed. Pony can wrap the skip list inside
an actor with an asynchronous interface, and manage its memory
using tracing of the entire list leading to more time spent
tracing memory and more floating garbage. Skip lists (hash tables,
B-trees, etc.) cannot be constructed in Rust without judicious use
of u̧ņşa̧f̧ȩ. Safe Rust's reference counting does not relax its
ownership rules, so mutation of aliased values is not permitted.

[style=tinyverona,numbers=left,caption=Skeleton code for Po. To save space, we permit constructor arguments to iso objects to take mut arguments (Lines 38, 45, 52, and 54). This is safe and can desugar to an extra enter. These lines all create an object that escapes the active region and is merged into the enclosing region, making them mut in r (append expects a mut argument). The ServerSocket is created elsewhere. It likely does not use arena allocation since it allocates on each turn of the loop (Line 13). If it did, those allocations would only be free'd on Line 31. The default annotation on new iso is <Arena> ( <ref>). Notice how code is agnostic to how memory is managed.,label=lst:skeleton]
type_alias KV = Skiplist[imm Id, iso Value] // To shorten code horisontally for this presentation
type_alias Response = UpdateOK | InsertOK | DeleteOK | Failure

def start_po(fn : imm String, server_socket : iso ServerSocket) : Unit
let kv : iso KV = new iso<RC> KV // create empty key-value store; (*@<RC>@*)=reference counting, see (*@<ref>@*)
enter kv  list => // Populate key-value store from persistent storage
let data : tmp File = open(fn, "r")
... list.insert(...) ... // read contents from data and add to list
// data goes out of scope, so get's free'd and closed

enter server_socket  ss =>
while (ss.is_open())
let socket : mut Socket = ss.accept() // new connection
let raw_request : imm String = socket.read_request() // get incoming request

let r : iso Response = enter new iso<Arena> Unit  _ => // arena-managed region for tmp allocations
let work : mut List[mut Tasks] = RequestParser::parse(raw_request) // parse request
let response = new mut List[mut Response] // holds all responses to tasks in request

while (!work.empty())
response.append(merge match work.pop()  // merges iso result from match into r since append expects mut
case mut StopTask => return // stop service, no response to client
case mut UpdateTask(id) =>          explore kv  kv' => update(kv', id)
case mut InsertTask(id, payload) => enter kv  kv' => insert(kv', id, payload)
case mut DeleteTask(id) =>          enter kv  kv' => delete(kv', id)

response.accumulate(new iso Message) // chained through accumuator, moves out of arena
// arena effectively goes out of scope, allocs on line 17, 18 + any tmp objects are freed
socket.respond(r); // render response object

def update(kv : paused KV, id : imm Id) : iso Response // process UpdateTasks, inside suspended kv
let value : paused Store[iso Value] = kv.get(id) // reference to a link's reference to a Value
enter *value  v => // Requires a dynamic check - because of aliasing cannot rule out v is already open
v.add_log_entry() // adds surviving object to v's region
v.remove_some_token() // makes object in v's region garbage
return new iso UpdateOK(v) // moves out of *value and kv regions and merged into r on line 21

def insert(kv : mut KV, id : imm Id, payload : imm Payload) : iso Response // process InsertTasks, inside kv
let new_value = Factory::create(id, payload) // decides memory management for new_value dynamically
enter new_value  v => v.tokens = new mut List; v.log = new mut List
kv.insert(id, new_value) // buries new_value
return new iso InsertOK() // moves out of kv region and merged into r on line 21

def delete(kv : mut KV, id : imm Id) : iso Response // process DeleteTasks, inside kv
enter new iso<Arena> Unit  _ => // create new tmp region, the one created on Line 16 is not accessible here
let q : mut SQL_Query = Factory::make_can_delete_query(id) // q cannot refer to kv because it is mut
let r : tmp SQL_Result = Backend::execute_query(q) // because it is tmp, r could refer to kv if it needed to
if (!r.OK) return new iso Failure(...) // moves out of tmp and kv regions and merged into r on line 21
// arena goes out of scope, allocs on lines 50, 51 are free'd
return enter kv.remove(id)  v => new iso DeleteOK(v)  // Creates garbage in kv, drops a Value region

§.§.§ Values in the Store

Finally, the elements in the store are suitable for either
reference counting or tracing GC because of their graph-like
structure (Line 42 delegates this decision to a factory method).
GC is especially favoured in the (possible) presence of cycles
which are expensive to detect with reference
counting <cit.>.

Later versions of Cyclone and MLKit support a global arena where
memory is managed using tracing GC. Thus, all elements in the
store contribute to pressure on the same GC, and GC requires
tracing through all elements to free garbage objects in one
element. MLKit's region propagation requires all elements to be
put in a single region. Pony can handle this pattern by making
each element an actor, which makes each element aliasable, and use
an asynchronous interface. Finally, Rust will not be able to
express and manage lifetimes of these structures automatically. A
combination of u̧ņşa̧f̧ȩ and manual memory management is needed.

§.§.§ Navigating Regions

<Ref> shows a zip computation involving three unrelated regions.

[numbers=right,firstnumber=1,caption=Opening two non-nested regions, computing a result in an active region.  is type parameters.,label=lst:zip]
let staff : iso List[imm Employee] = ...
let reviews : iso List[imm Review] = ...
var zip = new iso List[imm (String, (*@Int@*))]

explore staff  s => // open as immutable
explore reviews  r => // open as immutable
enter zip  z => // open as mutable
let si = s.iterator() // si is tmp (*@@*)
let ri = r.iterator() // ri is tmp (*@@*)
while (si.has_more()        ri.has_more())
z.append(new imm Pair(si.next().name(), (*@@*)
ri.next().calculate_salary())) (*@@*)

Using ȩx̧p̧ļo̧ŗȩ, we open the staff and reviews regions to make
them temporarily immutable and their contents accessible. Finally,
we open the zip region using . This makes the region
active which allows allocation of the two iterators on
Lines <ref> and <ref> and any allocation needed by the call
to append on Line <ref> to extend the list. It also allows
the mutation in the ņȩx̧ţ(̧)̧ calls to advance the iterators, and
the mutation necessary to add the new pair to the zip list.
Allocating the iterators inside the same region as their
corresponding list is not useful as it would make the
iterators immutable on Lines <ref> and <ref>. This
would cause the program to not typecheck—as the ņȩx̧ţ(̧)̧ method
needs to update the iterator, it needs to be called on a  or
receiver. Since the iterators need to store  references,
they must be  ( <ref>). This can be handled in
i̧ţȩŗa̧ţo̧ŗ(̧)̧ by overloading on the self type, letting the
implementation with  self-type return a  reference.
Elements are immutable so  ņȩx̧ţ(̧)̧ returns .

§.§.§ Design Thoughts on Explore vs. Enter—And Invariants

The ȩx̧p̧ļo̧ŗȩ construct is essentially syntactic sugar for two
nested ȩņţȩŗ blocks, the outermost entering the region to be
explored and the innermost entering a fresh region:

ȩx̧p̧ļo̧ŗȩ ̧x̧ ̧{̧ ̧y̧ ̧=̧>̧ ̧$̧\̧ ̧\̧ļḑo̧ţş\̧ ̧$̧ ̧}̧
desugars to  ȩņţȩŗ ̧x̧ ̧{̧ ̧y̧ ̧=̧>̧ ̧{̧ ̧ȩņţȩŗ ̧(̧ņȩw̧ ̧i̧şo̧ ̧U̧ņi̧ţ)̧ ̧{̧ ̧_̧ ̧=̧>̧ ̧$̧\̧ ̧\̧ļḑo̧ţş\̧ ̧$̧ ̧}̧ ̧}̧

The first ȩņţȩŗ activates the region, and the second suspends
it. The new region (ņȩw̧ ̧i̧şo̧ ̧U̧ņi̧ţ) is independent from the rest
of the program. As it is active, it serves all allocations that
appear inside the ȩx̧p̧ļo̧ŗȩ block (as suspended regions do not
permit allocation or deallocation, <ref>). What
ȩx̧p̧ļo̧ŗȩ guarantees that unprincipled nesting of ȩņţȩŗs
does not, is that the explored region was not mutated before
suspended. Conceptually, this is a big difference as we will
explain next.

Similar to object invariants, we expect invariants of a closed
region to hold at the time of opening. While active, invariants
may temporarily be broken and then restablished before the region
is closed. As a nested ȩņţȩŗ can reference any
enclosing region, it will be able to observe any invariants broken
by mutation following the opening of the enclosing regions. By opening
regions directly in a suspended state, ȩx̧p̧ļo̧ŗȩ ensures that
region invariants continue to hold. We are considering using a
separate capability to capture this statically.

We are also considering an
“eager” explore construct that opens a region along
with all its subregions as suspended in one fell swoop. This
would avoid the need for explicit opening of subregions thus
further simplifying working with immutable objects. The
cost is more complexity in the type system. Time will tell
whether this complexity is warranted or not.

With respect to memory management, ȩx̧p̧ļo̧ŗȩ allows opening a
region for reading, and navigating through it, without any memory
management overhead as the region's object structure is invariant
and there are neither allocations nor deallocations in the region.

§.§.§ 's Borrowing Capabilities

var x = new iso Cell // x : var Store[iso Cell]
enter y  => _ // now x : paused Store[iso Cell]
enter *x  => z
... // Can still mutate z!

Traditional borrowing as originally introduced
by <cit.>, explored deeply by
<cit.> and
<cit.>, and popularised by Rust relaxes
uniqueness of a value in a well-defined lexical scope. We can
express a similar form of borrowing through the type p̧a̧u̧şȩḑ
̧ ̧ ̧Şţo̧ŗȩ[̧i̧şo̧ ̧Ţ]̧,  a reference to a storage location in a
suspended region storing a reference to a closed region. Such a
reference ( x̧) can be shared freely inside a single
thread, allowing it to flow to a place where it can be opened
(ȩņţȩŗ ̧*̧x̧) with mutation rights, including swapping the
bridge object (as long as the new bridge object is a subtype of Ţ).

§ FORMALISING

We formalise  through two interacting languages:
region and command, and their respective semantics. The former
controls all accesses to memory (loads and stores), allocation of objects in
regions, creating, merging, freezing—and importantly entering and
exiting—regions. The most important properties of the region language is
expressed as a topology invariant ( <ref>).

The command language is essentially “what the programmer wrote”.
This separation makes it possible to specify  under what
conditions a store is valid, irrespective of what caused the

During execution, the command language emits effects which the region language
performs. The static semantics of the command language ensures,
modulo one dynamic check, that the topology invariant is preserved.

We present most of the rules of the region language and key type system rules.
Additional details are available in the appendix.

§.§ Dynamic Semantics of the Region Language

\RCfg & ::= & \langle \RS; H; H; H\rangle        \\
\RS   & ::= & \RF \mathop{::} \RS
~|~ \epsilon                             \\
\RF   & ::= & (r, S, F)                          \\
H     & ::= & R ~|~ H * H ~|~ \epsilon
\end{array}$

Configuration in region language (1/2)

A configuration in the region language has four components: a LIFO region stack
$\RS$ and the sub-heaps of open regions , closed regions ,
and frozen regions . The latter is an unimportant simplification
(conceptually, only mutable objects live in regions).
A heap $H$ is a collection of disjoint regions $R$. Opening a
closed region moves it from  to  and pushes a new stack
frame on top of $\RS$. Closing the top-most region in $\RS$ returns it back to
. Freezing a region moves it, and all regions reachable from it,
permanently to .

As an example, consider the region topology depicted in
<ref>. We can write down the corresponding configuration as $\langle \RS,
\OpenRegs, \ClosedRegs, \FrozenRegs \rangle$ where

\[
\begin{array}{lcl}
\RS &=& \RF_4 \mathop{::} \RF_3 \mathop{::} \RF_2 \mathop{::} \RF_1
\mathop{::} \epsilon \\
\OpenRegs &=& R_1 * R_2 * R_3 * R_4 \\
\ClosedRegs &=& R_5 * R_6 \\
\FrozenRegs &=& \epsilon
\end{array}
\]

For the region sub-heap $R_i$, if $R_i$ is open ( part of $\OpenRegs$),
$\RF_i$ is its region frame (depicted in <ref> as a white box) that holds the stack variables created in the scope of the corresponding ȩņţȩŗ block. Opening the closed region
$R_6$ would push a new frame $\RF_6$ above $\RF_4$ in $\RS$, and move $R_6$ from
$\ClosedRegs$ to $\OpenRegs$. Similarly we could freeze (merge) $R_6$, which
would move it from $\ClosedRegs$ to $\FrozenRegs$ (remove it from $\ClosedRegs$
and merge it into $R_4$).

S     & ::= & \iota \mapsto o, S ~|~ \epsilon    \\
F     & ::= & f\mapsto v?, F  ~|~ \epsilon       \\
v?    & ::= & v ~|~ \mathbf{undef}               \\
v     & ::= & (k, \iota)                         \\
R     & ::= & (r, S)                             \\
o     & ::= & (\#CL, F)                          \\
\end{array}$

Configuration in region language (2/2)

In this model, an inter-region reference into an open region is permissible iff
it points downwards in the region stack (from left to right according to
$\RS$), or it is the unique () reference through which the region was
opened. The LIFO region stack constitutes a “path” through the region forest
that corresponds to the opening order of ȩņţȩŗ blocks ( the region LIFO
order in <ref>). Thus, in <ref>, any reference
from $R_4$ to $R_3$ is permissible (as long as we do not close $R_4$), while a
reference from $R_2$ to $R_3$ must necessarily be the reference from object $e$
to object $f$. We model ȩx̧p̧ļo̧ŗȩ as nested ȩņţȩŗs.

A region stack frame  contains a region identifier $r$, a temporary store
$S$ for objects whose lifetimes are bounded by the scope of the region's ȩņţȩŗ
block (values with capability ), and a map $F$ from variable names $f$ to
values $v$, representing the local variables in that ȩņţȩŗ block (we model
destructive reads of a variable $x$ by remapping it to $\mathbf{undef}$, at
which point reading $x$ again will lead to the program getting stuck).

A region $R$ is a tuple of a (unique) region identifier $r$ and a store $S$
containing the objects in that region.

Objects are identified by $\iota$.

Values $v$ are object identifiers $\iota$ tagged with a capability $k$.

Stores $S$ map object ids $\iota$ to objects $o$ which store their
class tag $\#CL$ and fields (for simplicity we reuse the same $F$
as for local variables, although a field will never contain $\mathbf{undef}$).

The command language communicates with the region language via
effects. The relation
$\RCfg \yrightarrow{\Eff}[-1pt] \RCfg'$ should
be understood as performing the effect $\Eff$ in $\RCfg$,
resulting in $\RCfg'$.

Effects include entering and exiting a region, loading a value from an object
store, writing (swapping) a value for another in an object store, merging or
freezing a region, etc.

We now describe a selection of rules for these effects.

In every effect, the first parameter should be understood as the name of the
variable where the results should be stored. For example, the effect
$\mathit{load}(x, y.f)$ is handled in rule region-load by binding the value
of field $y.f$ to variable $x$.

First, the value of $y$ is looked up in the top stack frame as
$(k, \iota)$. The object id $\iota$ is used to find the
corresponding object $o$ in the configuration—it may be stored
in the subheap of an open or frozen region, or in one of the
temporary stores on the region stack. The capability $k$ is used
for viewpoint adaptation of the (capability of the) value $v$ of
field $f$ in $o$ before it is inserted into the top frame.

%   \Use ::= x ~|~ \kw{drop}~x\\\\
\mathbf{get}(F[x \mapsto v], \text{\c{drop}}\ x) =\\
\quad (v, F[x \mapsto \mathbf{undef}])\\
\mathbf{get}(F[x \mapsto (k, \iota)], x) =\\
\quad ((k, \iota), F[x \mapsto (k, \iota)])\\
\quad \text{ if } k \not\eq \Var \land k \not\eq \Iso
\end{array}$

(Non-)destructive reads

Field assignments are caused by the effect $\mathit{swap}(x, y.f, \Use)$, which
writes the value of $\Use$ to $y.f$ and binds the
old value of $y.f$ to $x$. A $\Use$ is a potentially destructive variable
access ($z$ or $\kw{drop}~z$, see <ref>). Rules region-swap-temp and
region-swap-heap handle the cases where the object being assigned to is in
the temporary store or on the heap. In both cases, we perform the $\Use$ (which
may make a variable invalid) with the helper function $\mathbf{get}$ (see
<ref>). We then proceed just as when loading a field, but finish
by updating the object being assigned to and update its containing store $S$.

Note that assigning and loading mutable variables are special
cases of the $\mathit{swap}$ and $\mathit{load}$ effects since we model mutable
variables as single-field objects.

Allocation on the heap is caused by the effect
$\mathit{halloc}(x, k, C, \Use_1 ... \Use_n)$, which instructs the
region language to heap allocate a new
$C$ object with fields initialized according to $\Use_1 ... \Use_n$ and bind it
to the name $x$. The capability $k$ denotes whether to allocate in the current
region region-alloc-heap-mut or in a new region

Since each $\Use$ is a possibly destructive variable access the ordering
matters. We begin by performing these one by one with the local variables $F_1$.
Each value $v_i$ is paired up with the corresponding field $f_i$ of the class
and put into an object $o$.

We then add $o$ at location $\iota$ to the subheap of the
currently active region, or add a new region $r'$ in the closed
regions containing only the object $o$ at location $\iota$.

Finally we bind the object to $x$ in the top frame with capability
or .

We omit the rule region-alloc-temp which allocates objects
with capabilities  or  in the temporary store $S$ of
the currently active region frame.

The key rules of the region language govern entering and exiting
a region.

region-enter-ok shows successfully entering a region $r'$
through its bridge object $\iota'$ stored in the field $f$ of the
variable $y$.

(This operation can fail if $R'$ is already opened. This will not change the
state in the region language, as seen in region-enter-fail, and it is up
to the command language to choose how to handle this: by exception,
having a construct like i̧f̧-̧ȩņţȩŗ-̧ȩļşȩ, etc. For simplicity, the command
language steps to a failure state.)

The $\mathit{enter}$ effect supplies four things: the name $w$ and capability
$k$ of the parameter of the ȩņţȩŗ block, the field $y.f$
through which we are entering, and a list of bindings
$\overline{z = \Use}$ denoting the block's captured variables.
Going back to <ref>, the enter block captures i̧, so the
corresponding effect would include $z = \text{\c{i}}$. Note that $z$ is chosen by the
command language and due to variable renaming is not necessarily i̧.

Considering the rule again, we first use the $\mathbf{get}$ helper function to
perform the $\Use$s.

For each resulting value $(k_i, \iota_i)$, we apply the
viewpoint adaptation when $k_i$ is not  and create a new
mapping $F$ of the captured variables.

We then get the value $\iota$ of $y$, load its corresponding
object $o$ and extract the value $\iota'$ of field $f$ (our bridge

On the last line of the premises we check that $\iota'$ is an
object in a closed region $r'$; this region will be moved into
the collection of open regions. We extend $F$ with a mapping from
$w$ to a fresh location $\iota''$, and finally install this
extended $F$ into a region frame $\RF$ where $\iota''$ is the
identifier of a ref cell object pointing to our bridge object
$\iota'$. We push this region frame onto the region stack.

region-exit-heap and region-exit-temp describe exiting the region
$r'$, popping its region frame from the top of the region frame stack. After
exiting, the region frame corresponding to $r$ will be on the top of the stack
and thus active. The $\mathit{exit}$ effect provides $\Use$ and $x$ which
correspond to the return value and the variable to which this will be bound (in
the stack frame of $r$). $z.f'$ specifies a location in $r'$ where a reference
to the new bridge object can be found. Finally, $y.f$ specifies a location where
this reference will be written.

The only difference between region-exit-heap and region-exit-temp is
where the object pointed to by $y$ is located. In the former it is on the heap
of some open region, while for the latter it is in a temporary store in
the region stack.

For simplicity, we do not implicitly reinstate  variables
captured from the previous region even if they are still valid
upon exit from a region (this would be sound,  <ref>
where variables ŗȩv̧i̧ȩw̧ş and z̧i̧p̧ are reinstated in the
top-level scope after line <ref>). This is without loss
of generality as we can return them in an object together with the result $v$
and reinstate them manually.

The rules for merging region-merge and freezing
region-freeze are similar. Both perform a $\Use$ to get an
object identifier $\iota$ and find its containing region $R$ among
the closed regions.

For merges, the subheap of $R$ is merged with the subheap of the
currently active region, and $\iota$ is bound to $x$ as .

For freezes, all the reachable regions of $R$ are moved from the
closed to the frozen regions together with $R$, and $\iota$ is
bound to $x$ as .

In addition to allocation in the temporary store, we have omitted
the rules for type casts and rebinding of variables.

§.§ Static Semantics of the Command Language

e & ::= & \Use ~|~ \text{\c{let}}~x = b~\text{\c{in}}~e\\
& ~|~ & \text{\c{if}~\c{typetest}}(\Use, t) \SB y => e \FB \SB y => e \FB\\
\Use & ::= & x ~|~ \text{\c{drop}}~x\\
b & ::= & \c{*}\lval
~|~ \lval~\c{:=}~\Use
~|~ \fnc(\many{use})
~|~ \text{\c{var}}~\Use\\
& ~|~ & \text{\c{new}}~k~C(\many{use})
~|~ \text{\c{freeze}}~\Use
~|~ \text{\c{merge}}~\Use \\
& ~|~ & \text{\c{enter}}~\lval~[\many{y=\Use}] \SB z~\c{=>}~e \FB
~|~ e\\
\lval & ::= & x ~|~ x.f\\
t & ::= & k~CL ~|~\, t\,\c{|}\,t
\end{array}$

Syntax of the command language

The command language is an imperative language in A-normal form.
The syntax is shown in <ref>.

We encode mutable variables of type $t$ as ref cells. For
uniformity we model these as objects of
type Çȩļļ[̧$t$]̧ with a single field v̧a̧ļ.

The i̧f̧ ̧ţy̧p̧ȩţȩşţ expression is a dynamic type test similar to
Java 16 style pattern matching, ḑŗo̧p̧ $x$ denotes a
destructive read, $\texttt{*}\lval$ dereferences a field or ref
cell, and v̧a̧ŗ allocates a new ref cell with the capability
and initializes its value from $\Use$. For simplicity we provide ȩņţȩŗ
blocks with an explicit capture list, but this could also be inferred from
variable use.

Types $t$ are unions $t_1\,\texttt{|}\,t_2$ or $k~CL$, where $k$ is a
capability and $CL$ is Çȩļļ or a class name $C$.

The static semantics is a flow-sensitive type system producing judgements of the form

$\Gamma_1 \vdash r : t \dashv \Gamma_2$ ($r \in e \cup b \cup \Use$). Thus it
statically tracks destructive reads and strong updates of unique variables.

We discuss a few of the rules below.

Reading a variable $x$ that is not a  or  is
straightforward and introduces an alias cmd-ty-use-keep.

When $x$ is  or , cmd-ty-use-drop allows reading
the variable but undefines it in the environment as a side-effect
to ensure its single use.

When accessing a field $x.f$ cmd-ty-deref-field, its type is
subject to viewpoint adaptation $\VPA{k}{t}$ where $k$ is the
capability of $x$ and $t$ the type of $f$. Note that viewpoint
adaptation disallows reading an  field unless $k$ is , expressing
the fact that freezing a region is deep (all nested regions will be frozen as

A field $x.f$ can be updated through assignment cmd-ty-assign
when the capability of $x$ is  or ,
internal references in the currently active region (note that assignment
returns the old value of the field). Viewpoint adaptation
is not needed as we are moving values rather than copying them, allowing
swapping of  references.

Local variables allow strong updates cmd-ty-assign-var. As we model them
as ref cells we update the type parameter for $x$ after assignment.

The predicate $\Hcap{k, t}$ asserts that the type $t$ has capability $k$;
the predicate $\Hopen{k}$ is true if the capability denotes an
open region,  $k$ is , ,  or .
Finally, $\Hmakemut{t}$ and $\Hmakeiso{t}$ return a $t$ whose
capabilities have been replaced by  and vice versa.

Opening a region through a field $x.f$ cmd-ty-enter requires that
$x$'s capability is $\mathsf{open}$, and $f$'s capability is

We create a new environment $\Gamma'$ with the captured variables
$y_1,...,y_n$, using viewpoint adaptation to suspend the types of
all non- variables, as well as a  ref cell holding
the bridge object.

We use $\Hmakemut{t}$ to change the type of the bridge
from  to  as control is moving inside the
opened region. Finally, the ȩņţȩŗ block may only return
's and 's.

(Note that entering a region through a field incurs a dynamic
check to see if the region is already open. )

Opening a region through a  ref cell cmd-ty-enter-var
is similar to a field cmd-ty-enter, but allows strong updates of
the ref cell holding the bridge object by retaining its
capability. This allows changing the bridge object's type from
within the ȩņţȩŗ block.

The rules for merging and freezing a region (cmd-ty-merge and
cmd-ty-freeze) are straightforward. Both demand that the
value that we operate on is an  reference ( bridge object to a closed
region), and produce either a  or  depending on the operation.

§.§ Dynamic Semantics of the Command Language

A configuration $\SB de \FB$ in the command language is a dynamic
expression $de$, which is an extension of $e$ by “entered blocks” that propagates syntactically the nesting structure of enters and exits,
and thus dynamically tracks the nesting of open regions, and
$\mathbf{Failure}$, used to report failed dynamic checks when
entering an already open region.

The dynamic semantics steps a configuration and produces an effect
of the same kind consumed by the region language.

For example, the expression ļȩţ $x = \texttt{*}y.f~$i̧ņ$~e$
produces the effect $\textit{load}(x, y.f)$, which tells the
region language to load the field $f$ from the object stored in
$y$ and store it in $x$.

§.§ Interaction Between the Region and Command Languages

A complete configuration is a product of the configurations of
the region and command languages. It steps if there is an effect
that steps both of them in tandem:

A dynamic expression is typed under a stack of typing contexts
$\many{\Gamma}$, corresponding to the nesting of
entered blocks. We lift the static semantics of the
command language to define well-formed effects:

the relation $\many{\Gamma} \vdash \Eff \dashv \many{\Gamma}'$
statically describes the effect $\Eff§$ and how it
changes the typing context.

For example, the static description of the effect
$\mathit{load}(x, y.f)$ states that the type of $y$ in the
top-most entered block is $k~CL$, that $CL$ has a field
$f$ of type $t$, and that the viewpoint adapted type $\VPA{k}{t}$
is well-formed ( cmd-ty-deref-field).

In order to reason about soundness, we define well-formedness of a
configuration in the region language as the relation
$\many{\Gamma} \vdash \langle \RS; \OpenRegs; \ClosedRegs;
\FrozenRegs\rangle$. A well-formed configuration ensures four

First, the stack of environments $\many{\Gamma}$ mirrors the
region stack $\RS$ so that each environment describes the local
variables of a region frame in $\RS$.

Second, each field of every object in the configuration contains a
value that corresponds to its static type.

Third, we have invariants about the reference
capabilities:  references are unique, objects in frozen
regions only refer to other references in frozen regions,
references point within the same region and to the heap,
and  point within the same region and to the
temporary store,  references point downwards in the
region stack, etc.

Finally, we have the invariant that the object graph and its
regions have the expected topology. We describe this invariant in
detail in the following section.

§.§ The Topology Invariant

The most important properties of the object (and region) graph
are captured in a single invariant that we call the
topology invariant (<ref>).

We express this as a property that holds for any pair of
references $\REF{1}$ and $\REF{2}$ in a well-formed configuration.
The helper functions  and  denote the storage location
and referee of a reference respectively;  denotes the region
of an object (or variable);  projects the region
identifiers out of a set of regions $H$.

For all references $\REF{1}$ and $\REF{2}$, either:

they are the same reference,  both are stored in the same $\iota.f$ or variable $x$ (1);

both refer to objects in different regions (2); or at least one of them

is an intra-region reference (3);

refers to a permanently immutable object (4); or

is a reference outwards in the nesting hierarchy, downwards in the region stack (5).

The relation $\RS\vdash \dst{\REF{}}\preceq\src{\REF{}}$
holds if $\dst{\REF{}}$ is higher up in $\RS$ than $\src{\REF{}}$
and $\REF{}$ originates from the temporary store. In other words, we
allow temporary references into suspended regions from open

\forall \REF{1}, \REF{2} \in \references{\langle \RS; \OpenRegs; \ClosedRegs; \FrozenRegs\rangle}.\\[1ex]
\quad\bigvee\left\{\begin{array}{l@{\quad}l}
\REF{1} = \REF{2} & (1) \\[1ex]
\reg{\dst{\REF{1}}} \neq \reg{\dst{\REF{2}}} & (2) \\[1ex]
\reg{\src{\REF{1}}} = \reg{\dst{\REF{1}}}\ \lor \\ \qquad \reg{\src{\REF{2}}} = \reg{\dst{\REF{2}}}  & (3) \\[1ex]
\reg{\dst{\REF{1}}} \in \regions{\FrozenRegs}\ \lor \\ \qquad \reg{\dst{\REF{2}}} \in \regions{\FrozenRegs} & (4) \\[1ex]
\RS\vdash\dst{\REF{1}} \preceq \src{\REF{1}}\ \lor \\ \quad \RS\vdash\dst{\REF{2}} \preceq\src{\REF{2}} & (5) \\
\end{array}\right.
\end{array}$

The topology invariant

The topology invariant has several important implications:

The object graph inside a region is unconstrained (3). The object graph
of the permanently immutable objects is unconstrained (4). Temporary objects in
an open region $R$ are allowed to refer to objects in an open region $R'$ as
long as $R'$ was opened before $R$ (5).

Finally, considering the whole invariant, if we have two external references
((3) does not hold) pointing into the same non-frozen region ((2) and (4)
do not hold), and neither of them points downwards in the region stack ((5)
does not hold), then they must be the same reference ((1) holds).

In particular, this means that there is at most one external reference into any
closed region, implying that the region graph of closed regions forms a forest.

§.§.§ The Topology Invariant and <ref>

Applying the topology invariant to all pairs of references in
<ref>, assuming $R$ was opened after $R'$, the
reference en is allowed to co-exist with any other alias
of $n$ since $\RS \vdash n \preceq e$ (5).

The reference me is not allowed to co-exist with
ma since there would be two external references into the
same region (1–5). However, ea can co-exist with ma
since the former stays within its region (3).

The references ai and oi are allowed to co-exist
because i is in a frozen region (4).

Finally, oa is illegal both because it cannot co-exist
with ma, and since references in frozen regions cannot
point to non-frozen regions.

§.§  is Sound

We prove soundness of our system by proving variants of progress
and preservation for the respective language. (The full proofs
are available in the appendix.)

Command Language Progress A well-formed command
configuration is done, has failed or can step:

$\many{\Gamma} \vdash \SB de \FB \implies de = \Use \lor de =
\mathbf{Failed} \lor \exists \Eff, de'.~ \SB de \FB
\yrightarrow{\Eff}[-1pt] \SB de' \FB$.

Command Language Preservation The command language
preserves well-formedness and produces well-formed effects:

$\many{\Gamma} \vdash \SB de \FB ~\land~ \SB de \FB \yrightarrow{\Eff}[-1pt] \SB de' \FB \implies
\exists \many{\Gamma}'.~ \many{\Gamma}'\vdash \SB de' \FB ~\land~
\many{\Gamma} \vdash \Eff \dashv \many{\Gamma}'$.

The command language is more permissive than the region
language, since it has no way of inspecting the state of the
global configuration. For example, an enter can always both
fail and succeed in the command language, whereas the region
language always permits exactly one of the behaviours. This
affects the formulation of progress:

Region Language Progress In a well-formed
configuration where the command configuration can step, there is
some effect which steps both configurations:

$\vdash \langle\SB de \FB~\RCfg\rangle \land \SB de \FB \yrightarrow{\Eff}[-1pt] \SB de' \FB \implies
\exists \Eff', de'', \RCfg'. \SB de \FB \yrightarrow{\Eff'}[-1pt] \SB de'' \FB ~\land~ \RCfg \yrightarrow{\Eff'}[-1pt] \RCfg'$.

Region Language Preservation The region language
preserves well-formedness for well-formed effects:

$\many{\Gamma} \vdash \RCfg ~\land~ \RCfg \yrightarrow{\Eff}[-1pt] \RCfg'
~\land~ \many{\Gamma} \vdash \Eff \dashv \many{\Gamma}' \implies \many{\Gamma}'
\vdash \RCfg'$.

Note that Lemma <ref> includes
preservation of the topology invariant.

Together, these lemmas prove the final soundness theorem:

Soundness A program never gets stuck and
it preserves well-formedness:

$\vdash \langle\SB de \FB~\RCfg\rangle \implies de = \Use \lor
de = \mathbf{Failed} \lor \exists de', \RCfg'. \langle\SB de \FB~\RCfg\rangle
\rightarrow \langle\SB de' \FB~\RCfg'\rangle \land \\ \vdash
\langle\SB de' \FB~\RCfg'\rangle$.

§  IN

While  regions are a stand-alone language design
component, they were developed specifically for the
programming language, from where the overarching
goal <ref> stems. In this section, we describe
-specific aspects and revisit concurrency-related goals
<ref> and <ref>.

§.§ Safe Concurrency

While regions and isolation can form the backbone of a “safe
concurrency” story for a language, concurrency is an orthogonal
aspect to our region design.  regions can be integrated
with different concurrency models. The necessary feature missing
from this paper is a way to share regions across threads of

uses a concurrency model based on behaviours
(tasks that do not join or have a return value) that operate on
cowns, short for concurrent owners. A cown is a wrapper
around an  that permits regions to be indirectly shared
across multiple threads of control, but importantly does not
permit direct access to its contents.

Cowns and 's are similar in that an explicit operation is
needed to access their contents. In the case of 's, access
is immediate and synchronous as exclusivity is already
established. In the case of cowns, access is asynchronous and will
only commence after exclusive access has been established
dynamically. This check requires region isolation for
soundness <cit.> and as a result, any mutable reference
accessible to a thread of control is safe to access
synchronously <ref>.

For a complete introduction to 's concurrency model, see
work by <cit.>.

§.§ Concurrent Memory Management

As memory management must only consider objects inside the active
region <ref> when determining liveness (
<ref>), and regions are always exclusive to one
thread, reference count manipulations do not need atomic
instructions, tracing GC does not need barriers, and there is no
need to momentarily stop all threads as in concurrent
GC's <cit.>.

By extension, a thread in  is free to mediate between
program work or memory management work without informing or
synchronising with other threads. Thus, we achieve concurrent
memory management <ref>.

§.§ Support for Different Memory Management Strategies

currently supports three different memory management
strategies for regions:
arena allocation,
reference counting, and
tracing GC.

How a region manages its memory is decided at use-site at
creation time using a qualifier on the ņȩw̧ keyword: ņȩw̧
̧ ̧ ̧i̧şo̧<̧A̧ŗȩņa̧>̧, ņȩw̧ ̧i̧şo̧<̧ŖÇ>̧ and ņȩw̧ ̧i̧şo̧<̧ĢÇ>̧. As liveness is
a local property, different regions' memory management does not
interact, so we do not need to  propagate this information
further in the program.

Selecting memory management at use-site is desirable since it lets
a programmer implement a data structure or library without having
to commit to decisions that could limit its future use. Such a
design also allows straightforward support for libraries that
consist of multiple nested regions whose memory management can be
controlled when the library is instantiated by programmatic means,
through a strategy pattern or equivalent.

§.§ Memory Management of Immutable Objects

Note that the memory management offered by regions does not extend
to immutable objects, at least not conceptually. One option for
implementation is going the way of Erlang and let a region have
a copy of each immutable object it references. This may facilitate
fast reclamation, but increases memory pressure. Furthermore, it
introduces a $O(n)$ copying overhead for transferring immutable
objects across region boundaries, in sharp contrast
with <ref>.

In the  run-time, we permit immutable objects to be
shared between regions. Thus, when a region is collected, we must
detect its implications for liveness of immutable objects.
Immutable objects must also consider roots across multiple
threads. On the other hand, tracing immutable objects is easy and
efficient as the structures are guaranteed not to change
underfoot <cit.>. How  manages
immutable objects is out of scope of this paper.

§.§ Propagating Capabilities Through Self Typing

is a class-based programming language. As an instance's
capability is determined at use-site, methods declare an
explicit self-capability,    to
propagate the external view of the instance into the instance. A
class may provide several different implementations of a method
overloaded on the self-capability.

[numbers=right,firstnumber=1,caption=Self typing in Çȩļļ.,label=lst:self-typing]
class Cell
var value : I64 // (*@mut Store[mut I64]@*)
def set_value(self:mut, v:I64)
// value : (*@($\VPA{\Mut}{\Mut}$) Store[mut I64]@*)
value := v

def set_value(self:paused, v:I64)
// value : (*@($\VPA{\Paused}{\Mut}$) Store[mut I64]@*)
value := v // (*@does not typecheck!@*)

def get_value(self:mut) = value
def get_value(self:paused) = value

A method can only be called on a receiver if its self-capability
matches the receiver's static type, which means that the object's
treatment of itself internally will match the external view, both
in terms of restrictions and abilities. For example, a method
whose self-capability is  can only be called when the
receiver's region is .
Notably, it is
not permitted to call a  method on a  receiver because
this would lead to aliasing between  and  (which
would weaken  from temporarily immutable to read-only).

Methods that are polymorphic in their self capability can be used
to avoid multiple near-identical versions of a single method like
in <ref>. For brevity, we refrain from discussing
this further.

§ RELATED WORK

We started out by describing related work leading up to Rust. We
now extend this picture by going beyond Rust and also relating
our work to garbage collection work before revisiting novelty.

§.§.§ Beyond Rust

In addition to what we have already covered, there is continuing
research into Rust to alleviate its restrictions, including
incorporating a garbage collector <cit.>, careful library
design <cit.>, phantom types <cit.>, or proving
unsafe Rust code correct <cit.>.

Recent research has focused on techniques for “post-Rust
languages”, building on Rust's use of ownership types, but supporting
more flexible program topologies (and hopefully more efficient
execution), typically by increasing the complexity of the type
system. This remains an active research area: the tradeoffs between
regions, ownership, types, capabilities, effects, topologies,
restrictions etc are complex and multifaceted

Pony <cit.> employs
implicit regions, external uniqueness and ownership to offer high
performance for actor programs by concurrent execution on multicore
CPUs, while maintaining data-race and memory safety.  Building on
capabilities used to describe what programs can do with particular
references <cit.> Pony offers at least six
“reference capabilities”: unique, thread-local, read-only,
write-only, and identity-only, (globally) immutable, plus type
modifiers for ephemeral (Hogg's “free”) and aliased references.
Reading or writing a field depends on the capabilities of both the
reference to the object, and of the field within the object: there
are 43 valid cases from 72 possible combinations of capabilities.

<cit.> design Dala
as a simplified alternative to Pony, based on three
different kinds of objects—immutable, unique (aka isolated), and
thread-local—rather than six different kinds of references. Dala
programs are also data-race free, however this guarantee may be
provided by a race detector at runtime, or by an optional/gradual
type system.

Milano et al.'s  Gallifrey aims to be more flexible than
Rust, by relying at least as much on MLKit style region inference as
on ownership annotations.  Rather than an explicit global ownership
model, Gallifrey programmers have to annotate unique (aka isolated)
object fields, and identify parameters that will be consumed by a
method invocation or that should be in the same region as other
parameters or the method result. A dynamic “if disconnected”
predicate searches the program's heap at runtime to determine of two
references are mutually disjoint.

Cogent <cit.> is a derivative of Haskell for systems
programming. It adopts a Rust-like discipline, permitting either
multiple read-only references to objects, or a single read-write
reference. Cogent uses annotations to support both a formally
defined operational semantics, generation of executable C source
code, and a proof certificate proving that the generated code
accurately implements the semantics.

§.§.§ Garbage Collection

Of the GC design goals, <ref> and
<ref> can be met to some extent without
region isolation. Here, 's contribution is trading
additional work to manage regions (at development time) for
reduced overheads of managing memory (at run-time) due to avoiding
GC techniques like remembered sets, barrier synchronisation, and
stop-the-world pauses. Region isolation guarantees that a
region's remembered set will always be empty. Thus, there is no
cost associated with additional region partitioning due to
tracking of inter-region references.

With respect to <ref>, generational GC's (
G1 <cit.>) and thread-local GC's ( <cit.>)
support collecting only a portion of the heap ( just the
young generation or one particular thread), but the shape and size
of this heap is beyond programmer control ( all young or
thread-local objects will take part of GC, not just particular
data structures). Furthermore, in the absence of (something like)
region isolation, inter-region aliases must be tracked dynamically
to be able to correctly compute liveness. Actor GC's that rely on
actor isolation using types (
Pony <cit.>) or copying
( Erlang <cit.>) are close as they
allow individual actor-local heaps to be collected. This is
similar to 's regions, but  supports additional
partitioning of the heap without an imposed asynchronous

With respect to <ref>, while it may be
possible to run different GC's in different generations (or
threads, actors, etc.), GC's typically use the same algorithm for
the entire heap, with minor tweaks ( to account for different
object characteristics due to age) as do actor GC's.
HRTGC is a real-time GC for mixed-criticality
work-loads <cit.> that hierarchically decomposes the heap
into regions that each run a different tracing GC, tuned
differently and with different collection frequency. HRTGC permits
inter-region references and tracks them dynamically. In the actor
world, Isolde <cit.> permits actors
implemented using type-enforced actor
isolation <cit.>
to manage their memory concurrent with their execution, using a
reference-counting based scheme.

With respect to <ref>, garbage collectors like
C4 <cit.>,
Shenandoah <cit.> and
ZGC <cit.> provide concurrent collection with brief
stop-the-world pauses to coordinate phase changes, with pause times invariant
of heap sizes. Their heaps have unrestricted references, and
instead rely on dynamic checks in read and write barriers. The
aforementioned actor GC's <cit.> support “fully
concurrent” collection: an actor can choose to collect its local
garbage without synchronising with any other concurrent activity.
's regions additionally allow us to statically detect
when an entire region is invalidated, without the need for a
specific actor collector to eventually detect the floating garbage
( <cit.>). Explicitly killing an actor to
instantly free its heap is a common programming pattern in Erlang
where it is made possible by copying objects on transfer,
giving up <ref>.

§ DISCUSSION

First, we place 's design concepts

into the context of all related work. Almost any ownership
system paired with external uniqueness will support region isolation and
dynamic reconfiguration. 's key
contribution here is a negative contribution, but important
nonetheless. Almost all other systems provide one or more top,
global, or shared heap region, and in various ways permit
references from inner/encapsulated/shorter-lived regions back to
outer/enclosing/longer-lived regions. (Generational garbage
collection works on a very similar principle
<cit.>).  does not, and this enhanced
decoupling of regions is critical to achieving many of our goals,
especially about concurrency, and independent GC.

's dynamic mutability and relaxed isolation is
novel and differs from other ownership and region systems.
Inasmuch as region systems like the MLKit are based on inference, and
are sound for all legal programs, questions of mutability and
isolation don't apply—if the program is type-correct, the
inference system can always place objects into regions such that no
region errors will arise at runtime.  Programming with more explicit
regions, or with ownership and capability annotations, either lack
polymorphism ( Dala) or require complex resolution or viewpoint
adaptation rules, or asynchronous indirections ( Pony).

In a way, 's region system trades precision for
simplicity. It cannot construct data structures that consist of
several morally overlapping regions, as is possible in  C++
or Rust. We believe all programs written in  C++ or Rust pay
the price for that precision—even though most programs do not
need it.

's “single window of mutability” is
probably its most novel concept. In pretty much every language, from
FORTRAN to LISP to ML to Haskell to C$++$ to Pony to Gallifrey, if
some code can finagle a mutable reference to an object, the program
can always update the object through that reference.  In Rust for
example, programs can collect up “mutable borrows” () of
any number of objects, pass them around as method arguments to
anywhere in the program, and then mutate all the borrowed
objects. Rust's “interior mutability” (aka C$++$'s const-cast) just
increases the scope for potential mutation.  This kind of
indiscriminate mutation is exactly what the “single window of
mutability” in  prevents.  Once a program departs—even
temporarily—from the scope of an opened region, ( by opening
some other closed region) the program can no longer modify
anything in that first opened region, no matter what kind of objects
are in the region, nor what kind of capability or reference the
program has to those objects.  Perhaps a single window of mutability
will prove too restrictive in practice, which may be why no other
system has yet adopted it.   demonstrates that it is possible
to build a system with a single mutability window as a core design
concept; exploring that concept further must necessarily be further work.

The single window of mutability is key to simplicity, both with
respect to the type system that enforces region isolation and our
invariants for memory management. We need only distinguish objects
in the active region, from objects in suspended regions and
objects in closed regions. As suspended regions are immutable and
closed regions inaccessible, we do not need to distinguish objects
belonging to different regions as nothing can be done to them that
affects or is affected by their region membership. By having only
a single mutable region at a time, non-local operations cannot
effect object liveness in the active region, or the liveness of an
entire active region. This permits optimisations at the
implementation level and simplifies the task of the programmer
wishing to reason about—and control—memory management

In contrast to other works which use types to enforce (or impose)
a structure on the heap, we let the path of the program through
the heap dictate the permissible pointer structure—not the other
way around. For example,  allows a single point in the
program to access the contents of two mutually isolated regions
$A$ and $B$, simply by virtue of opening them in a nested fashion.
The key insight is the decoupling of accessing from mutating,
implemented through the movable window of mutability. Rather than
alternating between accessing $A$ and $B$, we can gain access to
first $A$ and then $B$ without giving up access to $A$, just the
rights to mutate it. Opening $B$ after $A$ allows references to
objects in $A$ from $B$ to be created freely, but these references
may only persist as long as $B$ remains open. When $B$ is closed,
the references to $A$ are invalidated. This retains the
flexibility of navigating heap structures in any order,  we
could close $B$ then $A$ and open them immediately in the opposite
order, allowing pointers from $A$ to $B$. It also ensures that an
object is either mutable or immutable at any moment in time.

§ CONCLUSION

We have presented , a region system enforced by reference capabilities
that partitions a program's heap into a forest
of isolated regions. Memory in different regions
can be managed differently <ref>,
incrementally <ref> and
concurrently <ref>. The single external reference
to each region plus their full encapsulation enable cheap
ownership transfer <ref> and guarantees
freedom from data races <ref>. The ability to temporarily
trade mutability for access on the region stack allows any region
to (temporarily) reference any other region, and
also allows “external code” to operate inside a region, which is
crucial for libraries and reuse—not all uses of a region can be
predicted and supplied in its interface. In combination with the
region isolation and the single window of
mutability this allows the formulation of
topological invariants which are useful for a programmer to
control and reason about object liveness and implications of
memory management <ref> and can be leveraged for
efficient implementation of memory management. Memory management
costs are only incurred by the active region (one per thread), and
data accesses within that region—whether reading, writing,
tracing, or reference counting—never need atomic operations to
coordinate with other threads.

This work was partially supported by a grant from the
VRSwedish Research Councilhttps://www.vr.se/
(VR2020-05346), and partially by the Royal Society of
New Zealand Te Apārangi  Marsden Fund Te Pūtea Rangahau a
Marsden grants CRP1801 and CRP2101, and Agoric.
We thank the anonymous reviewers at OOPSLA'23 for their input that
greatly improved the presentation of this paper.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abtahi and DietzAbtahi and Dietz2020]
authorpersonParastoo Abtahi and
personGriffin Dietz. year2020.
Learning Rust: How Experienced Programmers
Leverage Resources to Learn a New Programming Language. In
booktitleCHI Extended Abstracts. pages1–8.

[Aldrich and ChambersAldrich and
authorpersonJonathan Aldrich and
personCraig Chambers. year2004.
Ownership domains: Separating aliasing policy
from mechanism. In booktitleECOOP,
Vol. volume4. publisherSpringer,

authorpersonJ. Armstrong.
A History of Erlang. In
booktitleHOPL III.

[Arvidsson, Castegren, Clebsch, Drossopoulou,
Noble, Parkinson, and WrigstadArvidsson et al2023]
authorpersonEllen Arvidsson, personElias
Castegren, personSylvan Clebsch, personSophia
Drossopoulou, personJames Noble, personMatthew J.
Parkinson, and personTobias Wrigstad.
Reference Capabilities for Flexible Memory
journalProceedings of the ACM on Programming
Languages volume7, numberOOPSLA2
(date10 year2023).

authorpersonHenry G. Baker.
Unify and Conquer (Garbage, Updating,
Aliasing,…) in Functional Languages. In
booktitleLISP and Functional Programming.

authorpersonAria Beingessner.
titleYou can't spell Trust without Rust.
thesistypeMaster's thesis. schoolComputer
Science, Carleton University.

authorpersonAria Beingessner.
titleLearn Rust With Entirely Too Many Linked Lists.
Accessed 2023-04-14.

authorpersonEli Bendersky.
titleRust data structures with circular references.

authorpersonDavid Blaser.
titleSimple Explanation of Complex Lifetime Errors in
Rust.  (year2019).
Bachelor Thesis, ETH Zürich.

authorpersonRobert Bocchino.
Deterministic Parallel Java.
In booktitleEncyclopedia of Parallel
Computing. pages566–573.

[Bollella, Canham, Carson, Champlin, Dvorak,
Giovannoni, Indictor, Meyer, Murray, and ReinholtzBollella
et al2003]
authorpersonGregory Bollella, personTim
Canham, personVanessa Carson, personVirgil Champlin,
personDaniel L. Dvorak, personBrian Giovannoni,
personMark B. Indictor, personKenny Meyer,
personAlex Murray, and personKirk Reinholtz.
Programming with non-heap memory in the real time
specification for Java. In booktitleOOPSLA Companion.

[Boyapati and RinardBoyapati and
authorpersonChandrasekhar Boyapati and
personMartin Rinard. year2001.
A Parameterized Type System for Race-Free
Java Programs. In booktitleProceedings of the 16th
ACM SIGPLAN Conference on Object-Oriented Programming, Systems,
Languages, and Applications (seriesOOPSLA '01).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages56–69.

[Boyapati, Salcianu, Beebee, and
RinardBoyapati et al2003]
authorpersonChandrasekhar Boyapati,
personAlexandru Salcianu, personWilliam Beebee, and
personMartin Rinard. year2003.
Ownership Types for Safe Region-Based Memory
Management in Real-Time Java. In booktitleProceedings of
the ACM SIGPLAN 2003 Conference on Programming Language Design and
Implementation (San Diego, California, USA) (seriesPLDI
'03). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages324–337.

authorpersonJohn Boyland.
Alias burying: Unique variables without
destructive reads.
journalSoftware: Practice and Experience
volume31, number6 (year2001),

Publisher: Wiley.

authorpersonJohn Boyland.
Fractional Permissions.
In booktitleAliasing in Object-Oriented
Programming, editorpersonDave Clarke,
personJames Noble, and personTobias Wrigstad
(Eds.). publisherSpringer-Verlag, addressBerlin,
Heidelberg, pages270–288.

[Boyland, Noble, and RetertBoyland
et al2001]
authorpersonJohn Boyland, personJames
Noble, and personWilliam Retert.
Capabilities for Sharing.
In booktitleProceedings of the 15th European
Conference on Object-Oriented Programming ECOOP, Budapest,
Hungary, June 18-22, 2001. publisherSpringer Berlin
Heidelberg, pages2–27.

[Brachthäuser, Schuster, Lee, and
Boruch-GruszeckiBrachthäuser et al2022]
authorpersonJonathan Immanuel Brachthäuser,
personPhilipp Schuster, personEdward Lee, and
personAleksander Boruch-Gruszecki.
Effects, Capabilities, and Boxes: From Scope-Based
Reasoning to Type-Based Reasoning and Back.
journalProc. ACM Program. Lang., Article
articleno76 (dateapr year2022),
numpages30 pages.

authorpersonNicholas Cameron.
titleWhat’s the “best” way to implement a
doubly-linked list in Rust?
Accessed 2023-04-14.

[Castegren and Tobias
WrigstadCastegren and Tobias Wrigstad2016]
authorpersonElias Castegren and
personTobias Wrigstad. year2016.
Reference Capabilities for Concurrency Control. In
booktitle30th European Conference on Object-Oriented
Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy.

[Castegren and WrigstadCastegren and
authorpersonElias Castegren and
personTobias Wrigstad. year2017.
Relaxed Linear References for Lock-free
Data Structures. In booktitleProceedings of the 31st
European Conference on Object-Oriented Programming ECOOP
(seriesLeibniz International Proceedings in
Informatics (LIPIcs), Vol. volume74).
publisherSchloss Dagstuhl–Leibniz-Zentrum fuer Informatik,

ISSN: 1868-8969.

[Cheeseman, Parkinson, Clebsch, Kogias,
Drossopoulou, Chisnall, Wrigstad, and LiétarCheeseman
et al2023]
authorpersonLuke Cheeseman, personMatthew J.
Parkinson, personSylvan Clebsch, personMarios
Kogias, personSophia Drossopoulou, personDavid
Chisnall, personTobias Wrigstad, and personPaul
Liétar. year2023.
When Concurrency Matters.
journalProceedings of the ACM on Programming
Languages volume7, numberOOPSLA2
(date10 year2023).

authorpersonDavid Clarke.
titleObject Ownership and Containment.
thesistypePh.D. Dissertation. schoolUniversity
of New South Wales.

[Clarke and DrossopoulouClarke and
authorpersonDave Clarke and personSophia
Drossopoulou. year2002.
Ownership, Encapsulation and the Disjointness of
Type and Effect. In booktitleProceedings of the 17th ACM
SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and
Applications (Seattle, Washington, USA) (seriesOOPSLA
'02). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages292–310.

[Clarke and WrigstadClarke and
authorpersonDave Clarke and personTobias
Wrigstad. year2003.
External Uniqueness Is Unique Enough. In
booktitleECOOP 2003 – Object-Oriented Programming,
editorpersonLuca Cardelli (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages176–200.

[Clarke, Wrigstad, and NobleClarke
et al2013]
authorpersonDavid Clarke, personTobias
Wrigstad, and personJames Noble.
booktitleAliasing in Object-oriented
Programming: Types, Analysis and Verification.
Vol. volume7850.

[Clarke, Wrigstad, Östlund, and
JohnsenClarke et al2008]
authorpersonDave Clarke, personTobias
Wrigstad, personJohan Östlund, and
personEinar Broch Johnsen. year2008.
Minimal Ownership for Active Objects. In
booktitleProgramming Languages and Systems,
editorpersonG. Ramalingam (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages139–154.

[Clarke, Potter, and NobleClarke
et al1998]
authorpersonDavid G. Clarke, personJohn M.
Potter, and personJames Noble.
Ownership Types for Flexible Alias
Protection. In booktitleProceedings of the 13th ACM
SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and
Applications (Vancouver, British Columbia, Canada)
(seriesOOPSLA '98). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Clebsch and DrossopoulouClebsch and
authorpersonSylvan Clebsch and
personSophia Drossopoulou. year2013.
Fully Concurrent Garbage Collection of
Actors on Many-core Machines. In booktitleProceedings
of the 2013 ACM SIGPLAN International Conference on Object
Oriented Programming Systems Languages & Applications, OOPSLA
2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31,
2013. pages553–570.

[Clebsch, Franco, Drossopoulou, Yang, Wrigstad,
and VitekClebsch et al2017]
authorpersonSylvan Clebsch, personJuliana
Franco, personSophia Drossopoulou,
personAlbert Mingkun Yang, personTobias Wrigstad,
and personJan Vitek. year2017.
Orca: GC and Type System Co-design for
Actor Languages.
journalPACMPL volume1,
numberOOPSLA (year2017),

[Click, Tene, and WolfClick
et al2005]
authorpersonCliff Click, personGil Tene,
and personMichael Wolf. year2005.
The Pauseless GC Algorithm. In
booktitleProceedings of the 1st ACM/USENIX
International Conference on Virtual Execution Environments
(seriesVEE '05). publisherACM,
addressNew York, NY, USA, pages46–56.

event-place: Chicago, IL, USA.

[Coblenz, Mazurek, and HicksCoblenz
et al2022]
authorpersonMichael Coblenz,
personMichelle L. Mazurek, and personMichael
Hicks. year2022.
Garbage Collection Makes Rust Easier to Use: A
Randomized Controlled Trial of the Bronze Garbage Collector. In
booktitleProceedings of the 44th International Conference on
Software Engineering (Pittsburgh, Pennsylvania)
(seriesICSE '22). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonRussell Cohen.
titleWhy Writing a Linked List in (safe) Rust is So
Damned Hard.
Accessed 2023-04-14.

CWE year2022.
title2021 CWE Top 25 Most Dangerous Software Weaknesses.

[Detlefs, Flood, Heller, and PrintezisDetlefs
et al2004]
authorpersonDavid Detlefs, personChristine
Flood, personSteve Heller, and personTony
Printezis. year2004.
Garbage-First Garbage Collection. In
booktitleProceedings of the 4th International Symposium on
Memory Management (Vancouver, BC, Canada) (seriesISMM
'04). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages37–48.

[Dietl, Drossopoulou, and MüllerDietl
et al2007]
authorpersonWerner Dietl, personSophia
Drossopoulou, and personPeter Müller.
Generic Universe Types. In
booktitleECOOP 2007 - Object-Oriented Programming,
21st European Conference, Berlin, Germany, July 30 - August 3,
2007, Proceedings. pages28–53.

[Domani, Goldshtein, Kolodner, Lewis, Petrank,
and SheinwaldDomani et al2002]
authorpersonTamar Domani, personGal
Goldshtein, personElliot K. Kolodner, personEthan
Lewis, personErez Petrank, and personDafna
Sheinwald. year2002.
Thread-Local Heaps for Java. In
booktitleProceedings of the 3rd International Symposium on
Memory Management (Berlin, Germany) (seriesISMM '02).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages76–87.

[Elsman and HallenbergElsman and
authorpersonMartin Elsman and personNiels
Hallenberg. year2021.
Integrating region memory management and tag-free
generational garbage collection.
journalJ. Funct. Program.  volume31
(year2021), pagese4.

[Fernandez-Reyes, Gariano, Noble,
Greenwood-Thessman, Homer, and WrigstadFernandez-Reyes
et al2021]
authorpersonKiko Fernandez-Reyes,
personIsaac Oscar Gariano, personJames Noble,
personErin Greenwood-Thessman, personMichael Homer,
and personTobias Wrigstad. year2021.
Dala: A Simple Capability-Based Dynamic
Language Design For Data Race-Freedom. In
booktitleProceedings of the 2021 ACM SIGPLAN International
Symposium on New Ideas, New Paradigms, and Reflections on Programming and
Software (Chicago, IL, USA) (seriesOnward! 2021).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages1–17.

[Flanagan and FreundFlanagan and
authorpersonCormac Flanagan and
personStephen N. Freund. year2000.
Type-Based Race Detection for Java. In
booktitleProceedings of the ACM SIGPLAN 2000 Conference on
Programming Language Design and Implementation (Vancouver, British
Columbia, Canada) (seriesPLDI '00).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages219–232.

[Flood, Kennke, Dinn, Haley, and
WestrelinFlood et al2016]
authorpersonChristine H. Flood, personRoman
Kennke, personAndrew Dinn, personAndrew Haley, and
personRoland Westrelin. year2016.
Shenandoah: An open-source concurrent compacting
garbage collector for OpenJDK. In booktitleProceedings of
the 13th International Conference on Principles and Practices of
Programming on the Java Platform: Virtual Machines, Languages,
and Tools, Lugano, Switzerland, August 29 - September 2, 2016.

[Fluet and MorrisettFluet and
authorpersonMatthew Fluet and personGreg
Morrisett. year2006.
Monadic regions.
journalJ. Funct. Program. volume16,
number4-5 (year2006), pages485–545.

[Fluet, Morrisett, and AhmedFluet
et al2006]
authorpersonMatthew Fluet, personGreg
Morrisett, and personAmal J. Ahmed.
Linear Regions Are All You Need. In
booktitleESOP, Vol. volume3924.

[Francis-Landau, Xue, Eisner, and
SarkarFrancis-Landau et al2016]
authorpersonMatthew Francis-Landau,
personBing Xue, personJason Eisner, and
personVivek Sarkar. year2016.
Fine-grained parallelism in probabilistic parsing
with Habanero Java. In booktitleIA3 '16:
Proceedings of the Sixth Workshop on Irregular Applications:
Architectures and Algorithms. publisherIEEE Press,
addressPiscataway, NJ, USA, pages78–81.
event-place: Salt Lake City, Utah.

[Franco, Clebsch, Drossopoulou, Vitek, and
WrigstadFranco et al2018]
authorpersonJuliana Franco, personSylvan
Clebsch, personSophia Drossopoulou, personJan Vitek,
and personTobias Wrigstad. year2018.
Correctness of a fully concurrent Garbage
Collector for Actor Languages. In booktitleEuropean
Symposium on Programming (ESOP), Vol. volume10801.

[Gay and AikenGay and Aiken1998]
authorpersonDavid Gay and personAlex
Aiken. year1998.
Memory Management with Explicit Regions.
journalSIGPLAN Not. volume33,
number5 (datemay year1998),

[Gay and AikenGay and Aiken2001]
authorpersonDavid Gay and personAlex
Aiken. year2001.
Language Support for Regions.
journalSIGPLAN Not. volume36,
number5 (datemay year2001),

[Gonnord, Henrio, Morel, and RadanneGonnord
et al2023]
authorpersonLaure Gonnord, personLudovic
Henrio, personLionel Morel, and personGabriel
Radanne. year2023.
A Survey on Parallelism and Determinism.
journalACM Comput. Surv. volume55,
number10, Article articleno210 (datefeb
year2023), numpages28 pages.

authorpersonColin S. Gordon.
Designing with Static Capabilities and Effects:
Use, Mention, and Invariants (Pearl). In
editorpersonRobert Hirschfeld and
personTobias Pape (Eds.). pages10:1–10:25.

[Gordon, Parkinson, Parsons, Bromfield, and
DuffyGordon et al2012]
authorpersonColin S. Gordon,
personMatthew J. Parkinson, personJared Parsons,
personAleks Bromfield, and personJoe Duffy.
Uniqueness and reference immutability for safe
parallelism. In booktitleProceedings of the 27th Annual
ACM SIGPLAN Conference on Object-Oriented Programming, Systems,
Languages, and Applications, OOPSLA 2012, part of SPLASH 2012,
Tucson, AZ, USA, October 21-25, 2012. pages21–40.

[Grossman, Morrisett, Jim, Hicks, Wang, and
CheneyGrossman et al2002]
authorpersonDan Grossman, personGreg
Morrisett, personTrevor Jim, personMichael Hicks,
personYanling Wang, and personJames Cheney.
Region-based memory management in Cyclone.
journalACM Sigplan Notices volume37,
number5 (year2002), pages282–293.
Publisher: ACM.

[Gruber and BoyerGruber and Boyer2013]
authorpersonOlivier Gruber and
personFabienne Boyer. year2013.
Ownership-Based Isolation for Concurrent
Actors on Multi-core Machines. In booktitleECOOP
2013 – Object-Oriented Programming,
editorpersonGiuseppe Castagna (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages281–301.

[Haller and LoikoHaller and Loiko2016]
authorpersonPhilipp Haller and
personAlexander Loiko. year2016.
LaCasa: lightweight affinity and object
capabilities in Scala. In booktitleProceedings of the
2016 ACM SIGPLAN International Conference on Object-Oriented
Programming, Systems, Languages, and Applications, OOPSLA 2016,
part of SPLASH 2016, Amsterdam, The Netherlands, October 30 -
November 4, 2016. pages272–291.

[Haller and OderskyHaller and
authorpersonPhilipp Haller and
personMartin Odersky. year2010.
Capabilities for Uniqueness and Borrowing.
In booktitleProceedings of 24th European
Conference on Object-Oriented Programming, ECOOP, Maribor,
Slovenia, June 21-25.

[Harms and WeideHarms and Weide1991]
authorpersonDouglas E. Harms and
personBruce W. Weide. year1991.
Copying and Swapping: Influences on the
Design of Reusable Software Components.
journalIEEE Trans. Softw. Eng.
volume17, number5 (dateMay
year1991), pages424–435.

Publisher: IEEE Press.

[Hicks, Morrisett, Grossman, and JimHicks
et al2004]
authorpersonMichael W. Hicks,
personJ. Gregory Morrisett, personDan Grossman, and
personTrevor Jim. year2004.
Experience with safe manual memory-management in
Cyclone. In booktitleISMM. pages73–84.

authorpersonJohn Hogg.
Islands: Aliasing Protection in
Object-Oriented Languages. In booktitleConference
proceedings on Object-oriented programming systems, languages, and
applications - OOPSLA '91. publisherACM Press,

[Hogg, Lea, Wills, de Champeaux, and HoltHogg
et al1992]
authorpersonJ. Hogg, personD. Lea,
personA. Wills, personD. de Champeaux, and
personR. Holt. year1992.
The Geneva Convention on the Treatment of Object
journalOOPS Messenger volume3,
number2 (dateApril year1992).

authorpersonVivian Hu.
titleRust Breaks into TIOBE Top 20 Most Popular
Programming Languages.  (dateJune year2020).

authorpersonDaniel H. Ingalls.
Design Principles Behind Smalltalk.
journalBYTE volume6,
number8 (dateAugust year1981),

[Jones, Hosking, and MossJones
et al2016]
authorpersonRichard Jones, personAntony
Hosking, and personEliot Moss.
booktitleThe garbage collection handbook: the art of
automatic memory management.
publisherCRC Press.

[Jung, Dang, Kang, and DreyerJung
et al2019]
authorpersonRalf Jung, personHoang-Hai
Dang, personJeehoon Kang, and personDerek Dreyer.
Stacked Borrows: An Aliasing Model for Rust.
journalProc. ACM Program. Lang.
volume4, numberPOPL, Article articleno41,
numpages32 pages.

[Jung, Jourdan, Krebbers, and DreyerJung
et al2017]
authorpersonRalf Jung, personJacques-Henri
Jourdan, personRobbert Krebbers, and personDerek
Dreyer. year2017.
RustBelt: Securing the Foundations of the Rust
Programming Language.
journalPACMPL volume2,
numberPOPL, Article articleno66 (dateJan.
year2017), numpages66:1–66:34 pages.

[Jung, Jourdan, Krebbers, and DreyerJung
et al2020]
authorpersonRalf Jung, personJacques-Henri
Jourdan, personRobbert Krebbers, and personDerek
Dreyer. year2020.
Safe Systems Programming in Rust: The Promise and
the Challenge.
journalCommunications of the ACM

[Klabnik and NicholsKlabnik and
authorpersonSteve Klabnik and personCarol
Nichols. year2019.
booktitleThe Rust Programming Language (Covers Rust
publisherNo Starch Press.

authorpersonPaul Krill.
titleMicrosoft forms Rust language team.
(dateFeb. year2021).

[Lampson, Horning, London, Mitchell, and
PopekLampson et al1977]
authorpersonButler Lampson, personJim
Horning, personRalph London, personJim Mitchell,
and personGerry Popek. year1977.
Report on the Programming Language Euclid.
journalACM Sigplan Notices volume12,
number3 (dateMarch year1977),

authorpersonDoug Lea. year1998.
booktitleConcurrent Programming in Java
(edition2nd ed.).

[Lehrmann Madsen, Møller-Pedersen, and
NygaardLehrmann Madsen et al1993]
authorpersonOle Lehrmann Madsen,
personBirger Møller-Pedersen, and personKristen
Nygaard. year1993.
booktitleObject-Oriented Programming in the
BETA Programming Language.

[Li, Cameron, and NobleLi
et al2012]
authorpersonPaley Li, personNicholas
Cameron, and personJames Noble.
Sheep Cloning with Ownership Types. In
booktitleFoundations of Object-Oriented Programming
Languages (FOOL). publisherACM.

[Lidén and KarlssonLidén and
authorpersonPer Lidén and personStefan
Karlsson. year2018.
titleThe Z Garbage Collector—Low Latency GC
for OpenJDK.

<http://cr.openjdk.java.net/ pliden/slides/ZGC-Jfokus-2018.pdf>

[Lieberherr and HollandLieberherr and
authorpersonKarl J. Lieberherr and
personIan Holland. year1989.
Assuring Good Style for Object-Oriented Programs.
journalIEEE Software numberSeptember
(year1989), pages38–48.

[Mastrangelo, Ponzanelli, Mocci, Lanza,
Hauswirth, and NystromMastrangelo et al2015]
authorpersonLuis Mastrangelo, personLuca
Ponzanelli, personAndrea Mocci, personMichele Lanza,
personMatthias Hauswirth, and personNathaniel
Nystrom. year2015.
Use at Your Own Risk: The Java Unsafe API in the
Wild. In booktitleProceedings of the 2015 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems, Languages,
and Applications (Pittsburgh, PA, USA) (seriesOOPSLA
2015). publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages695–710.

[Milano, Turcotti, and MyersMilano
et al2022]
authorpersonMae Milano, personJoshua
Turcotti, and personAndrew C. Myers.
A flexible type system for fearless concurrency.
In booktitlePLDI '22: 43rd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, San Diego, CA,
USA, June 13 - 17, 2022, editorpersonRanjit Jhala
and personIsil Dillig (Eds.). publisherACM,

[Müller and Poetzsch-HeffterMüller and
authorpersonPeter Müller and personArnd
Poetzsch-Heffter. year1999.
Universes: A type system for controlling
representation exposure. In booktitleProgramming
Languages and Fundamentals of Programming,
Vol. volume263. publisherTechnical Report 263,
Fernuniversität Hagen. http://www. informatik. fernuni-hagen.
de/pi5/publications. html.

authorpersonndrewxie. year2019.
titleWhat’s the “best” way to implement a
doubly-linked list in Rust?
Accessed 2023-04-14.

[Noble, Mackay, and WrigstadNoble
et al2022]
authorpersonJames Noble, personJulian
Mackay, and personTobias Wrigstad.
Rusty Links in Local Chains. In

[Noble, Vitek, and PotterNoble
et al1998]
authorpersonJames Noble, personJan Vitek,
and personJohn Potter. year1998.
Flexible Alias Protection. In
booktitleECOOP'98 — Object-Oriented Programming,
editorpersonEric Jul (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages158–185.

[Noble and WeirNoble and Weir2000]
authorpersonJames Noble and personCharles
Weir. year2000.
booktitleSmall Memory Software: Patterns for Systems
with Limited Memory.

[O’Connor, Chen, Rizkallah, Jackson, Amani,
Klein, Murray, Sewell, and KellerO’Connor et al2021]
authorpersonLiam O’Connor, personZilin
Chen, personChristine Rizkallah, personVincent
Jackson, personSidney Amani, personGerwin Klein,
personToby Murray, personThomas Sewell, and
personGabriele Keller. year2021.
Cogent: uniqueness types and certifying
journalJournal of Functional Programming
volume31 (year2021), pagese25.

[Pizlo, Hosking, and VitekPizlo
et al2007]
authorpersonFilip Pizlo, personAntony L.
Hosking, and personJan Vitek.
Hierarchical Real-Time Garbage Collection. In
booktitleProceedings of the 2007 ACM SIGPLAN/SIGBED
Conference on Languages, Compilers, and Tools for Embedded Systems (San
Diego, California, USA) (seriesLCTES '07).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages123–133.

[Potter, Noble, and ClarkePotter
et al1998]
authorpersonJ. Potter, personJ. Noble,
and personD. Clarke. year1998.
The Ins and Outs of Objects. In

[Qin, Chen, Yu, Song, and ZhangQin
et al2020]
authorpersonBoqin Qin, personYilun Chen,
personZeming Yu, personLinhai Song, and
personYiying Zhang. year2020.
Understanding memory and thread safety practices
and issues in real-world Rust programs. In
booktitlePLDI. pages763–779.

authorpersonRyan James Spencer.
titleFour Ways To Avoid The Wrath Of The Borrow Checker.

[Srinivasan and MycroftSrinivasan and
authorpersonS. Srinivasan and personA.
Mycroft. year2008.
Kilim: Isolation-Typed Actors for Java. In

[Tene, Iyengar, and WolfTene
et al2011]
authorpersonGil Tene, personBalaji Iyengar,
and personMichael Wolf. year2011.
C4: The Continuously Concurrent Compacting
Collector. In booktitleProceedings of the International
Symposium on Memory Management (seriesISMM '11).
publisherACM, addressNew York, NY, USA,

event-place: San Jose, California, USA.

Tiobe year2022.
titleTIOBE Index for June 2022.

[Tofte, Birkedal, Elsman, and HallenbergTofte
et al2004]
authorpersonMads Tofte, personLars
Birkedal, personMartin Elsman, and personNiels
Hallenberg. year2004.
A Retrospective on Region-Based Memory Management.
journalHigher Order Symbolic Computing
volume17, number3 (year2004),

[Tofte, Birkedal, Elsman, Hallenberg, Olesen,
and SestoftTofte et al2021]
authorpersonMads Tofte, personLars
Birkedal, personMartin Elsman, personNiels
Hallenberg, personTommy Højfeld Olesen, and
personPeter Sestoft. year2021.
booktitleProgramming with Regions in the MLKit
(Revised for Version 4.6.0).
typeTechnical Report.
institutionDepartment of Computer Science, University of
Copenhagen, Denmark.

[Tofte and TalpinTofte and Talpin1997]
authorpersonMads Tofte and
personJean-Pierre Talpin. year1997.
Region-based Memory Management.
journalInf. Comput. volume132,
number2 (year1997), pages109–176.

authorpersonAaron Turon.
titleFearless Concurrency with Rust.

authorpersonMark Utting.
Reasoning about aliasing. In
booktitleFourth Australasian Refinement Workshop.

authorpersonPhilip Wadler.
Linear types can change the world. In
booktitleIFIP TC, Vol. volume2.
publisherCiteseer, pages347–359.

authorpersonTobias Wrigstad.
titleOwnership-Based Alias Management.
thesistypePh.D. Dissertation. schoolRoyal
Institute of Technology, Stockholm.

[Yang and WrigstadYang and Wrigstad2017]
authorpersonAlbert Mingkun Yang and
personTobias Wrigstad. year2017.
Type-Assisted Automatic Garbage Collection for
Lock-Free Data Structures. In booktitleProceedings of the
2017 ACM SIGPLAN International Symposium on Memory Management (Barcelona,
Spain) (seriesISMM 2017). publisherAssociation
for Computing Machinery, addressNew York, NY, USA,

[Yanovski, Dang, Jung, and DreyerYanovski
et al2021]
authorpersonJoshua Yanovski,
personHoang-Hai Dang, personRalf Jung, and
personDerek Dreyer. year2021.
GhostCell: separating permissions from data in
Rust. In booktitleICFP.

§ INTRODUCTION TO APPENDIX

This appendix contains the static and dynamic semantic of
, and the full proof of soundness. The dynamic semantics
is defined as two systems executing in tandem: the region
semantics and the command semantics.

The region semantics is the most important dynamic semantics in
terms of understanding the system. It is responsible for entering
and exiting regions, handling allocations and variable bindings.
(We do not model deallocation.)

The command semantics drives execution by emitting effects which
are then performed by the region semantics.

Any differences between the main paper and the appendix is purely
for presentational reasons.

§ TANDEM SEMANTICS

\[
\begin{array}{rcll}
\Cfg & ::= & \langle \SB de \FB~\RCfg\rangle & \text{Tandem configuration}
\end{array}
\]

A  configuration is a tuple of a command configuration
and a region configuration. It steps if the two configurations can
both step with the same effect, and is well-formed if both
configurations are well-formed with the same $\Gammas$.

$\Cfg \rightarrow \Cfg'$Tandem Semantics

$\vdash \Cfg$Tandem Semantics

§ REGION SEMANTICS

\[
\begin{array}{ll}
r \in \Reg                                       & \text{Region ids}                                     \\
\iota \in \Oid                                   & \text{Object ids}                                     \\
x,y,z,w,f,g \in \X                               & \text{Field and variable names}\\
C \in \Cls                                       & \text{Class names}                                    \\
\end{array}
\]

\[
\begin{array}{rcll}
\CL &  ::= & C ~|~ \Cell[t] & \text{Static types} \\
\CLTag & ::= & \#C ~|~ \#\Cell    & \text{Dynamic type tags} \\
k & ::= & \Iso ~|~ \Var ~|~ \Mut ~|~ \Tmp ~|~ \Paused ~|~ \Imm & \text{Capabilities}                        \\
t & ::= & k~\CL ~|~ t | t & \text{Types} \\
v & ::= & (k, \iota)                                & \text{Values (references tagged with capabilities)}   \\
o & ::= & (\CLTag, F)                                  & \text{Objects (class tag and field)}                 \\
F & ::= & x \mapsto v, F ~|~ x \mapsto \Undef, F ~|~ \varepsilon & \text{Field and variable bindings}                    \\
R & ::= & (r, S)                                    & \text{Region (region id and sub-heap)}                \\
S & ::= & \iota \mapsto o, S ~|~ \varepsilon        & \text{Store}                                          \\
H & ::= & H * H ~|~ R ~|~ \varepsilon               & \text{Heap (collection of Regions)}                   \\
\RF & ::= & (r, S, F)                               & \text{Region frame}                                   \\
\RS & ::= & \RF \mathop{::} \RS
~|~ \varepsilon                           & \text{Region stack}                                  \\
\RCfg & ::= & \langle \RS; H; H; H \rangle & \text{Configuration}

\end{array}
\]

The heap $H$ is a collection of disjoint regions $R$, each
containing a region identifiers $r$ and a store $S$ mapping object
identifiers $\iota$ to objects $o$. An object consists of the
object's class tag (without the type parameter of ) and a
mapping $F$ from field names $f$ to values $v$ (consisting of a
capability $k$ and an object identifier $\iota$).

The region configuration  is a region stack  and three
heaps $H$, for the open, closed and frozen regions respectively.

The region stack is a stack of frames  holding a region
identifier, a (local) store $S$ and a mapping $F$ from variables
to values. Note that for simplicity we reuse $F$ for storing field
mappings and variable mappings, meaning fields and variables are
in the same syntactic category $\X$.

We assume the existence of a table of classes and their fields
such that $\mathbf{ftypes}(CL) = f_1 : t_1, ..., f_n : t_n$ and
$\mathbf{ftype}(CL, f_i) = t_i$, meaning that the class $CL$ has a
field $f_i$ with type $t_i$. We also assume that no field has
capability $\Var{}$. We use $\mathbf{fields}(CL)$ to get just the
names of the fields.

We further assume that we can always create fresh