figure 11institutetext: Drexel University
11email<EMAIL_ADDRESS>
# Safe Deferred Memory Reclamation with Types

Ismail Kuru  0000-0002-5796-2150 Colin S. Gordon  0000-0002-9012-4490

###### Abstract

Memory management in lock-free data structures remains a major challenge in
concurrent programming. Design techniques including read-copy-update (RCU) and
hazard pointers provide workable solutions, and are widely used to great
effect. These techniques rely on the concept of a grace period: nodes that
should be freed are not deallocated immediately, and all threads obey a
protocol to ensure that the deallocating thread can detect when all possible
readers have completed their use of the object. This provides an approach to
safe deallocation, but only when these subtle protocols are implemented
correctly.

We present a static type system to ensure correct use of RCU memory
management: that nodes removed from a data structure are always scheduled for
subsequent deallocation, and that nodes are scheduled for deallocation at most
once. As part of our soundness proof, we give an abstract semantics for RCU
memory management primitives which captures the fundamental properties of RCU.
Our type system allows us to give the first proofs of memory safety for RCU
linked list and binary search tree implementations without requiring full
verification.

##  1 Introduction

For many workloads, lock-based synchronization – even fine-grained locking –
has unsatisfactory performance. Often lock-free algorithms yield better
performance, at the cost of more complex implementation and additional
difficulty reasoning about the code. Much of this complexity is due to memory
management: developers must reason about not only other threads violating
local assumptions, but whether other threads are _finished accessing_ nodes to
deallocate. At the time a node is unlinked from a data structure, an unknown
number of additional threads may have already been using the node, having read
a pointer to it before it was unlinked in the heap.

A key insight for manageable solutions to this challenge is to recognize that
just as in traditional garbage collection, the unlinked nodes need not be
reclaimed immediately, but can instead be reclaimed later after some protocol
finishes running. Hazard pointers [31] are the classic example: all threads
actively collaborate on bookkeeping data structures to track who is using a
certain reference. For structures with read-biased workloads, Read-Copy-Update
(RCU) [25] provides an appealing alternative. The programming style resembles
a combination of reader-writer locks and lock-free programming. Multiple
concurrent readers perform minimal bookkeeping – often nothing they wouldn’t
already do. A single writer at a time runs in parallel with readers,
performing additional work to track which readers may have observed a node
they wish to deallocate. There are now RCU implementations of many common tree
data structures [9, 36, 6, 26, 3, 21], and RCU plays a key role in Linux
kernel memory management [29].

However, RCU primitives remain non-trivial to use correctly: developers must
ensure they release each node exactly once, from exactly one thread, _after_
ensuring other threads are finished with the node in question. Model checking
can be used to validate correctness of implementations for a mock client [23,
8, 19, 1], but this does not guarantee correctness of arbitrary client code.
Sophisticated verification logics can prove correctness of the RCU primitives
and clients [17, 13, 35, 24]. But these techniques require significant
verification expertise to apply, and are specialized to individual data
structures or implementations. One important reason for the sophistication in
these logics stems from the complexity of the underlying memory reclamation
model. However, Meyer and Wolff [30] show that a suitable abstraction enables
separating verifying correctness of concurrent data structures from its
underlying reclamation model under the assumption of memory safety, and study
proofs of correctness assuming memory safety.

We propose a type system to ensure that RCU client code uses the RCU
primitives safely, ensuring memory safety for concurrent data structures using
RCU memory management. We do this in a general way, not assuming the client
implements any specific data structure, only one satisfying some basic
properties common to RCU data structures (such as having a tree memory
footprint). In order to do this, we must also give a formal operational model
of the RCU primitives that abstracts many implementations, without assuming a
particular implementation of the RCU primitives. We describe our RCU semantics
and type system, prove our type system sound against the model (which ensures
memory is reclaimed correctly), and show the type system in action on two
important RCU data structures.

Our contributions include:

  * •

A general (abstract) operational model for RCU-based memory management

  * •

A type system that ensures code uses RCU memory management correctly, which is
signifiantly simpler than full-blown verification logics

  * •

Demonstration of the type system on two examples: a linked-list based bag and
a binary search tree

  * •

A proof that the type system guarantees memory safety when using RCU
primitives.

##  2 Background & Motivation

In this section, we recall the general concepts of read-copy-update
concurrency. We use the RCU linked-list-based bag [27] from Figure 2 as a
running example. It includes annotations for our type system, which will be
explained in Section 4.2.

⬇ 1struct BagNode{ 2 int data; 3 BagNode<rcuItr> Next; 4} 5BagNode<rcuRoot> head; 6void add(int toAdd){ 7WriteBegin; 8BagNode nw = new; 9$\\{nw\mathsf{:rcuFresh}\\{\\}\\}$ 10nw.data = toAdd; 11$\\{head\mathsf{:rcuRoot},par\mathsf{:undef},cur\mathsf{:undef}\\}$ 12BagNode<rcuItr> par,cur = head; 13$\\{head\mathsf{:rcuRoot},par\mathsf{:rcuItr}\epsilon\\{\\}\\}$ 14$\\{cur\mathsf{:rcuItr}\epsilon\\{\\}\\}$ 15cur = par.Next; 16$\\{cur\mathsf{:rcuItr}Next\\{\\}\\}$ 17$\\{par\mathsf{:rcuItr}\epsilon\\{Next\mapsto cur\\}\\}$ 18while(cur.Next != null){ 19 $\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{\\}\\}$ 20 $\\{par\mathsf{:rcuItr}(Next)^{k}\\{Next\mapsto cur\\}\\}$ 21 par = cur; 22 cur = par.Next; 23 $\\{cur\mathsf{:rcuItr}(Next)^{k}.Next.Next\\{\\}\\}$ 24 $\\{par\mathsf{:rcuItr}(Next)^{k}.Next\\{Next\mapsto cur\\}\\}$ 25} 26$\\{nw\mathsf{:rcuFresh}\\{\\}\\}$ 27$\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{Next\mapsto null\\}\\}$ 28$\\{par\mathsf{:rcuItr}(Next)^{k}\\{Next\mapsto cur\\}\\}$ 29nw.Next= null; 30$\\{nw\mathsf{:rcuFresh}\\{Next\mapsto null\\}\\}$ 31$\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{Next\mapsto null\\}\\}$ 32cur.Next=nw; 33$\\{nw\mathsf{:rcuItr}(Next)^{k}.Next.Next\\{Next\mapsto null\\}\\}$ 34$\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{Next\mapsto nw\\}\\}$ 35WriteEnd; 36} |  ⬇ 1void remove(int toDel){ 2WriteBegin; 3$\\{head\mathsf{:rcuRoot},par:\mathsf{undef},cur\mathsf{:undef}\\}$ 4BagNode<rcuItr> par,cur = head; 5$\\{head\mathsf{:rcuRoot},par\mathsf{:rcuItr}\epsilon\\{\\},cur\mathsf{:rcuItr}\epsilon\\{\\}\\}$ 6cur = par.Next; 7$\\{cur\mathsf{:rcuItr}Next\\{\\}\\}$ 8$\\{par\mathsf{:rcuItr}\epsilon\\{Next\mapsto cur\\}\\}$ 9while(cur.Next != null&&cur.data != toDel) 10{ 11 $\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{\\}\\}$ 12 $\\{par\mathsf{:rcuItr}(Next)^{k}\\{Next\mapsto cur\\}\\}$ 13 par = cur; 14 cur = par.Next; 15 $\\{cur\mathsf{:rcuItr}(Next)^{k}.Next.Next\\{\\}\\}$ 16 $\\{par\mathsf{:rcuItr}(Next)^{k}.Next\\{Next\mapsto cur\\}\\}$ 17} 18$\\{nw\mathsf{:rcuFresh}\\{\\}\\}$ 19$\\{par\mathsf{:rcuItr}(Next)^{k}\\{Next\mapsto cur\\}\\}$ 20$\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{\\}\\}$ 21BagNode<rcuItr> curl = cur.Next; 22$\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{Next\mapsto curl\\}\\}$ 23$\\{curl\mathsf{:rcuItr}(Next)^{k}.Next.Next\\{\\}\\}$ 24par.Next = curl; 25$\\{par\mathsf{:rcuItr}(Next)^{k}\\{Next\mapsto curl\\}\\}$ 26$\\{cur\mathsf{:unlinked}\\}$ 27$\\{cur\mathsf{:rcuItr}(Next)^{k}.Next\\{\\}\\}$ 28SyncStart; 29SyncStop; 30$\\{cur\mathsf{:freeable}\\}$ 31Free(cur); 32$\\{cur\mathsf{:undef}\\}$ 33WriteEnd; 34}
---|---

Figure 1: RCU client: singly linked list based bag implementation.

As with concrete RCU implementations, we assume threads operating on a
structure are either performing read-only traversals of the structure —
_reader threads_ — or are performing an update — _writer threads_ — similar to
the use of many-reader single-writer reader-writer locks.111RCU
implementations supporting multiple concurrent writers exist [3], but are the
minority. It differs, however, in that readers may execute concurrently with
the (single) writer.

This distinction, and some runtime bookkeeping associated with the read- and
write-side critical sections, allow this model to determine at modest cost
when a node unlinked by the writer can safely be reclaimed.

Figure 2 gives the code for adding and removing nodes from a bag. Type
checking for all code, including membership queries for bag, can be found in
our technical report [22]. Algorithmically, this code is nearly the same as
any sequential implementation. There are only two differences. First, the
read-side critical section in member is indicated by the use of ReadBegin and
ReadEnd; the write-side critical section is between WriteBegin and WriteEnd.
Second, rather than immediately reclaiming the memory for the unlinked node,
remove calls SyncStart to begin a _grace period_ — a wait for reader threads
that may still hold references to unlinked nodes to finish their critical
sections. SyncStop blocks execution of the writer thread until these readers
exit their read critical section (via ReadEnd). These are the essential
primitives for the implementation of an RCU data structure.

These six primitives together track a critical piece of information: which
reader threads’ critical sections overlapped the writer’s. Implementing them
efficiently is challenging [9], but possible. The Linux kernel for example
finds ways to reuse existing task switch mechanisms for this tracking, so
readers incur no additional overhead. The reader primitives are semantically
straightforward – they atomically record the start, or completion, of a read-
side critical section.

The more interesting primitives are the write-side primitives and memory
reclamation. WriteBegin performs a (semantically) standard mutual exclusion
with regard to other writers, so only one writer thread may modify the
structure _or the writer structures used for grace periods_.

SyncStart and SyncStop implement _grace periods_ [33]: a mechanism to wait for
readers to finish with any nodes the writer may have unlinked. A grace period
begins when a writer requests one, and finishes when all reader threads active
_at the start of the grace period_ have finished their current critical
section. Any nodes a writer unlinks before a grace period are physically
unlinked, but not logically unlinked until after one grace period.

An attentive reader might already realize that our usage of logical/physical
unlinking is different than the one used in data-structures literature where
typically a logical deletion (e.g., marking) is followed by a physical
deletion (unlinking). Because all threads are forbidden from holding an
interior reference into the data structure after leaving their critical
sections, waiting for active readers to finish their critical sections ensures
they are no longer using any nodes the writer unlinked prior to the grace
period. This makes actually freeing an unlinked node after a grace period
safe.

SyncStart conceptually takes a snapshot of all readers active when it is run.
SyncStop then blocks until all those threads in the snapshot have finished at
least one critical section. SyncStop does not wait for _all_ readers to
finish, and does not wait for all overlapping readers to simultaneously be out
of critical sections.

To date, every description of RCU semantics, most centered around the notion
of a grace period, has been given algorithmically, as a specific (efficient)
implementation. While the implementation aspects are essential to real use,
the lack of an abstract characterization makes judging the correctness of
these implementations – or clients – difficult in general. In Section 3 we
give formal _abstract_ , _operational_ semantics for RCU implementations –
inefficient if implemented directly, but correct from a memory-safety and
programming model perspective, and not tied to specific low-level RCU
implementation details. To use these semantics or a concrete implementation
correctly, client code must ensure:

  * •

Reader threads never modify the structure

  * •

No thread holds an interior pointer into the RCU structure across critical
sections

  * •

Unlinked nodes are always freed by the unlinking thread _after_ the unlinking,
_after_ a grace period, and _inside_ the critical section

  * •

Nodes are freed at most once

In practice, RCU data structures typically ensure additional invariants to
simplify the above, e.g.:

  * •

The data structure is always a tree

  * •

A writer thread unlinks or replaces only one node at a time.

and our type system in Section 4 guarantees these invariants.

##  3 Semantics

In this section, we outline the details of an abstract semantics for RCU
implementations. It captures the core client-visible semantics of most RCU
primitives, but not the implementation details required for efficiency [29].
In our semantics, shown in Figure 2, an abstract machine state, MState,
contains:

  * •

A stack $s$, of type
$\textsf{Var}\times\textsf{TID}\rightharpoonup\textsf{Loc}$

  * •

A heap, $h$, of type
$\textsf{Loc}\times\textsf{FName}\rightharpoonup\textsf{Val}$

  * •

A lock, $l$, of type $\textsf{TID}\uplus\\{\textsf{unlocked}\\}$

  * •

A root location $rt$ of type Loc

  * •

A read set, $R$, of type $\mathcal{P}(\textsf{TID})$ and

  * •

A bounding set, $B$, of type $\mathcal{P}(\textsf{TID})$

The lock $l$ enforces mutual exclusion between write-side critical sections.
The root location $rt$ is the root of an RCU data structure. We model only a
single global RCU data structure; the generalization to multiple structures is
straightforward but complicates formal development later in the paper. The
reader set $R$ tracks the thread IDs (TIDs) of all threads currently executing
a read block. The bounding set $B$ tracks which threads the writer is
_actively_ waiting for during a grace period — it is empty if the writer is
not waiting.

$\begin{array}[]{rclcl}\alpha&::=&\mathsf{skip}\mid\mathsf{x.f=y}\mid\mathsf{y=x}\mid\mathsf{y=x.f}\mid\mathsf{y=new}\mid\mathsf{Free}\mathsf{(\textsf{x})}\mid\mathsf{Sync}\end{array}\quad\textsf{Sync}\overset{\Delta}{=}\texttt{{SyncStart};{SyncStop}}$

$\begin{array}[]{c@{\;}rl@{\Downarrow_{\mathit{tid}}}ll}(\textsc{RCU-
WBegin})&\llbracket\texttt{WriteBegin}\rrbracket&(s,h,\mathsf{unlocked},rt,R,B)&(s,h,l,rt,R,B)&\\\
(\textsc{RCU-
WEnd})&\llbracket\texttt{WriteEnd}\rrbracket&(s,h,l,rt,R,B)&(s,h,\mathsf{unlocked},rt,R,B)&\\\
(\textsc{RCU-
RBegin})&\llbracket\texttt{ReadBegin}\rrbracket&(s,h,tid,rt,R,B)&(s,h,tid,rt,R\uplus\\{tid\\},B)\qquad\mathit{tid}\neq
l&\\\ (\textsc{RCU-
REnd})&\llbracket\texttt{ReadEnd}\rrbracket&(s,h,tid,rt,R\uplus\\{tid\\},B)&(s,h,l,rt,R,B\setminus\\{tid\\})\qquad\mathit{tid}\neq
l&\\\ (\textsc{RCU-
SStart})&\llbracket\texttt{SyncStart}\rrbracket&(s,h,l,rt,R,\emptyset)&(s,h,l,rt,R,R)&\\\
(\textsc{RCU-
SStop})&\llbracket\texttt{SyncStop}\rrbracket&(s,h,l,rt,R,\emptyset)&(s,h,l,rt,R,\emptyset)&\\\
(\textsc{Free})&{\llbracket\texttt{Free}(x)\rrbracket}&(s,h,l,rt,R,\emptyset)&(s,h^{\prime},l,rt,R,\emptyset)&\end{array}$

$\textrm{provided}~{}\forall_{f,o^{\prime}}\ldotp rt\neq s(x,tid)\textrm{ and
}o^{\prime}\neq s(x,tid)\implies
h(o^{\prime},f)=h^{\prime}(o^{\prime},f)\textrm{ and }\forall_{f}\ldotp
h^{\prime}(o,f)=\textsf{undef}$

$\begin{array}[]{c@{\;}rl@{\Downarrow_{\mathit{tid}}}ll}(\textsc{HUpdt})&\llbracket\texttt{x.f=y}\rrbracket&(s,h,l,rt,R,B)&(s,h[s(x,tid),f\mapsto
s(y,tid)],l,rt,R,B)&\\\
(\textsc{HRead})&\llbracket\texttt{y=x.f}\rrbracket&(s,h,l,rt,R,B)&(s[(y,tid)\mapsto
h(s(x,tid),f)],h,l,rt,R,B)&\\\
(\textsc{SUpdt})&\llbracket\texttt{y=x}\rrbracket&(s,h,l,rt,R,B)&(s[(y,tid)\mapsto(x,tid)],h,l,rt,R,B)&\\\
(\textsc{HAlloc})&\llbracket\texttt{y=new}\rrbracket&(s,h,l,rt,R,B)&(s,h[\ell\mapsto\mathsf{nullmap}],l,rt,R,B)&\end{array}$

$\textrm{provided}~{}rt\neq s(y,tid)\textrm{ and
}s[(y,tid)\mapsto\ell],\textrm{ and }$
$h[\ell\mapsto\mathsf{nullmap}]\overset{\mathrm{def}}{=}\lambda(o^{\prime},f).\textrm{
if }o=o^{\prime}\textrm{ then }skip\textrm{ else }h(o^{\prime},f)$

Figure 2: Operational semantics for RCU.

Figure 2 gives operational semantics for _atomic_ actions; conditionals,
loops, and sequencing all have standard semantics, and parallel composition
uses sequentially-consistent interleaving semantics.

The first few atomic actions, for writing and reading fields, assigning among
local variables, and allocating new objects, are typical of formal semantics
for heaps and mutable local variables. Free is similarly standard. A writer
thread’s critical section is bounded by WriteBegin and WriteEnd, which acquire
and release the lock that enforces mutual exclusion between writers.
WriteBegin only reduces (acquires) if the lock is unlocked.

Standard RCU APIs include a primitive synchronize_rcu() to wait for a grace
period for the current readers. We decompose this here into two actions,
SyncStart and SyncStop. SyncStart initializes the blocking set to the current
set of readers — the threads that may have already observed any nodes the
writer has unlinked. SyncStop blocks until the blocking set is emptied by
completing reader threads. However, it does not wait for _all_ readers to
finish, and does not wait for all overlapping readers to simultaneously be out
of critical sections. If two reader threads $A$ and $B$ overlap some
SyncStart-SyncStop’s critical section, it is possible that $A$ may exit and
re-enter a read-side critical section before $B$ exits, and vice versa.
Implementations must distinguish subsequent read-side critical sections from
earlier ones that overlapped the writer’s initial request to wait: since
SyncStart is used _after_ a node is physically removed from the data structure
and readers may not retain RCU references across critical sections, $A$ re-
entering a fresh read-side critical section will not permit it to re-observe
the node to be freed.

Reader thread critical sections are bounded by ReadBegin and ReadEnd.
ReadBegin simply records the current thread’s presence as an active reader.
ReadEnd removes the current thread from the set of active readers, and also
removes it (if present) from the blocking set — if a writer was waiting for a
certain reader to finish its critical section, this ensures the writer no
longer waits once that reader has finished its current read-side critical
section.

Grace periods are implemented by the combination of ReadBegin, ReadEnd,
SyncStart, and SyncStop. ReadBegin ensures the set of active readers is known.
When a grace period is required, SyncStart;SyncStop; will store (in $B$) the
active readers (which may have observed nodes before they were unlinked), and
wait for reader threads to record when they have completed their critical
section (and implicitly, dropped any references to nodes the writer wants to
free) via ReadEnd.

These semantics do permit a reader in the blocking set to finish its read-side
critical section and enter a _new_ read-side critical section before the
writer wakes. In this case, _the writer waits only for the first critical
section of that reader to complete_ , since entering the new critical section
adds the thread’s ID back to $R$, but not $B$.

##  4 Type System & Programming Language

In this section, we present a simple imperative programming language with two
block constructs for modeling RCU, and a type system that ensures proper
(memory-safe) use of the language. The type system ensures memory safety by
enforcing these sufficient conditions:

  * •

A heap node can only be freed if it is no longer accessible from an RCU data
structure or from local variables of other threads. To achieve this we ensure
the reachability and access which can be suitably restricted. We explain how
our types support a delayed ownership transfer for the deallocation.

  * •

Local variables may not point inside an RCU data structure unless they are
inside an RCU read or write block.

  * •

Heap mutations are local: each unlinks or replaces exactly one node.

  * •

The RCU data structure remains a tree. While not a fundamental constraint of
RCU, it is a common constraint across known RCU data structures because it
simplifies reasoning (by developers or a type system) about when a node has
become unreachable in the heap.

We also demonstrate that the type system is not only sound, but useful: we
show how it types Figure 2’s list-based bag implementation [27]. We also give
type checked fragments of a binary search tree to motivate advanced features
of the type system; the full typing derivation can be found in our technical
report [22] Appendix B. The BST requires type narrowing operations that refine
a type based on dynamic checks (e.g., determining which of several fields
links to a node). In our system, we presume all objects contain all fields,
but the number of fields is finite (and in our examples, small). This avoids
additional overhead from tracking well-established aspects of the type system
— class and field types and presence, for example — and focus on checking
correct use of RCU primitives. Essentially, we assume the code our type system
applies to is already type-correct for a system like C or Java’s type system.

###  4.1 RCU Type System for Write Critical Section

Section 4.1 introduces RCU types and the need for subtyping. Section 4.2,
shows how types describe program states, through code for Figure 2’s list-
based bag example. Section 4.3 introduces the type system itself.

####

RCU Types There are six types used in Write critical sections

$\tau::=\textsf{rcuItr}\;\rho\;\mathcal{N}\mid\textsf{rcuFresh}\;\mathcal{N}\mid\textsf{unlinked}\mid\textsf{undef}\mid\textsf{freeable}\mid\textsf{rcuRoot}$

#### rcuItr

is the type given to references pointing into a shared RCU data structure. A
rcuItr type can be used in either a write region or a read region (without the
additional components). It indicates both that the reference points into the
shared RCU data structure and that the heap location referenced by rcuItr
reference is reachable by following the path $\rho$ from the root. A component
$\mathcal{N}$ is a set of field mappings taking the field name to local
variable names. Field maps are extended when the referent’s fields are read.
The field map and path components track reachability from the root, and local
reachability between nodes. These are used to ensure the structure remains
acyclic, and for the type system to recognize exactly when unlinking can
occur.

Read-side critical sections use rcuItr without path or field map components.
These components are both unnecessary for readers (who perform no updates) and
would be invalidated by writer threads anyways. Under the assumption that
reader threads do not hold references across critical sections, the read-side
rules essentially only ensure the reader performs no writes, so we omit the
reader critical section type rules. They can be found in our technical report
[22] Appendix E.

#### unlinked

is the type given to references to unlinked heap locations — objects
previously part of the structure, but now unreachable via the heap. A heap
location referenced by an unlinked reference may still be accessed by reader
threads, which may have acquired their own references before the node became
unreachable. Newly-arrived readers, however, will be unable to gain access to
these referents.

#### freeable

is the type given to references to an unlinked heap location that is safe to
reclaim because it is known that no concurrent readers hold references to it.
Unlinked references become freeable after a writer has waited for a full grace
period.

#### undef

is the type given to references where the content of the referenced location
is inaccessible. A local variable of type freeable becomes undef after
reclaiming that variable’s referent.

#### rcuFresh

is the type given to references to freshly allocated heap locations. Similar
to rcuItr type, it has field mappings set $\mathcal{N}$. We set the field
mappings in the set of an existing rcuFresh reference to be the same as field
mappings in the set of rcuItr reference when we replace the heap referenced by
rcuItr with the heap referenced by rcuFresh for memory safe replacement.

#### rcuRoot

is the type given to the fixed reference to the root of the RCU data
structure. It may not be overwritten.

####

Subtyping It is sometimes necessary to use imprecise types — mostly for
control flow joins. Our type system performs these abstractions via subtyping
on individual types and full contexts, as in Figure 3.

$\displaystyle\mathcal{N}=\\{f_{0}|\ldots|f_{n}\rightharpoonup\\{y\\}\mid
f_{i}\in\textsf{FName}\land\;0\leq i\leq n\land\;(y\in\textsf{Var}\lor
y\in\\{null\\})\\}\quad\mathcal{N}_{f,\emptyset}=\mathcal{N}\setminus\\{f\rightharpoonup\\_\\}\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathcal{N}_{\emptyset}=\\{\\}\quad\mathcal{N}(\cup_{f\rightharpoonup
y})=\mathcal{N}\cup\\{f\rightharpoonup
y\\}\quad\mathcal{N}(\setminus_{f\rightharpoonup
y})=\mathcal{N}-\\{f\rightharpoonup y\\}\penalty-10000\hskip 20.00003pt plus
0.5fil minus 5.0pt\mathcal{N}([f\rightharpoonup y])=\mathcal{N}\text{ where
}f\rightharpoonup y\in\mathcal{N}\quad\mathcal{N}(f\rightharpoonup x\setminus
y)=\mathcal{N}\setminus\\{f\rightharpoonup x\\}\cup\\{f\rightharpoonup
y\\}\penalty-10000\hskip 20.00003pt plus 0.5fil minus
5.0pt\framebox{$\vdash\,\mathcal{N}\prec:\mathcal{N}^{\prime}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-NSub3)}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
30.24016pt\vbox{\vbox{}\hbox{\hskip-30.24016pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\,\mathcal{N}_{f,\emptyset}\prec:\mathcal{N}([f\rightharpoonup
y])$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-NSub4)}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
14.5911pt\vbox{\vbox{}\hbox{\hskip-14.5911pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\,\mathcal{N}_{\emptyset}\prec:\mathcal{N}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-NSub5)}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
13.6111pt\vbox{\vbox{}\hbox{\hskip-13.6111pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\,\mathcal{N}\prec:\mathcal{N}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
9.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-NSub2)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
47.50505pt\vbox{\vbox{}\hbox{\hskip-47.50504pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\,\mathcal{N}([f_{2}\rightharpoonup
y])\prec:\mathcal{N}([f_{1}|f_{2}\rightharpoonup
y])$}}}}}}$}}\hbox{}$}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\raise
9.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-NSub1)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
47.50505pt\vbox{\vbox{}\hbox{\hskip-47.50504pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\,\mathcal{N}([f_{1}\rightharpoonup
y])\prec:\mathcal{N}([f_{1}|f_{2}\rightharpoonup
y])$}}}}}}$}}\hbox{}$}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\framebox{$\vdash\,\rho\prec:\rho^{\prime}$}\;\;\raise
9.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-PSub1)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
26.44102pt\vbox{\vbox{}\hbox{\hskip-26.44101pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\rho.f_{1}\prec:\rho.f_{1}|f_{2}$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
9.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-PSub2)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
26.44102pt\vbox{\vbox{}\hbox{\hskip-26.44101pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\rho.f_{2}\prec:\rho.f_{1}|f_{2}$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
9.1111pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-PSub3)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
13.3413pt\vbox{\vbox{}\hbox{\hskip-13.3413pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\rho\prec:\rho$}}}}}}$}}\hbox{}$}\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt\framebox{$\vdash\,T\prec:T^{\prime}$}\penalty 50\hskip 20.00003pt plus
0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-TSub2)}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
24.53891pt\vbox{\vbox{}\hbox{\hskip-24.53891pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\textsf{rcuItr}\prec:\textsf{rcuItr}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-TSub)}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
28.85281pt\vbox{\vbox{}\hbox{\hskip-28.8528pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\textsf{rcuItr}\;\\_\prec:\textsf{undef}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-TSub1)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
33.47485pt\vbox{\hbox{\hskip-33.47485pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\rho\prec:\rho^{\prime}\qquad\vdash\mathcal{N}\prec:\mathcal{N}^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
36.8193pt\vbox{\vbox{}\hbox{\hskip-36.8193pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\textsf{rcuItr}\,\rho\,\mathcal{N}\prec:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\framebox{$\vdash\,\Gamma\prec:\Gamma^{\prime}$}\;\;\raise
9.61665pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-CSub1)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
29.41396pt\vbox{\hbox{\hskip-29.41396pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma\prec:\Gamma^{\prime}\;\;\vdash\text{T}\prec:\text{T'}$}}}\vbox{}}}\over\hbox{\hskip
31.85907pt\vbox{\vbox{}\hbox{\hskip-31.85907pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma\,,x:\text{T}\prec:\Gamma^{\prime}\,,x:\text{T'}$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
8.56738pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-CSub)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
14.0972pt\vbox{\vbox{}\hbox{\hskip-14.0972pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma\prec:\Gamma$}}}}}}$}}\hbox{}$}$

Figure 3: Subtyping rules.

Figure 3 includes four judgments for subtyping. The first two —
$\vdash\mathcal{N}\prec:\mathcal{N}^{\prime}$ and
$\vdash\rho\prec:\rho^{\prime}$ — describe relaxations of field maps and paths
respectively. $\vdash\mathcal{N}\prec:\mathcal{N}^{\prime}$ is read as “the
field map $\mathcal{N}$ is more precise than $\mathcal{N}^{\prime}$” and
similarly for paths. The third judgment $\vdash T\prec:T^{\prime}$ uses path
and field map subtyping to give subtyping among rcuItr types — one rcuItr is a
subtype of another if its paths and field maps are similarly more precise —
and to allow rcuItr references to be “forgotten” — this is occasionally needed
to satisfy non-interference checks in the type rules. The final judgment
$\vdash\Gamma\prec:\Gamma^{\prime}$ extends subtyping to all assumptions in a
type context.

$\displaystyle\framebox{$\Gamma\vdash_{M,R}C\dashv\Gamma^{\prime}$}\;\;\;\;\;\;{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-ReIndex)}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
36.59634pt\vbox{\vbox{}\hbox{\hskip-36.59634pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
C_{k}\dashv\Gamma[\rho.f^{k}/\rho.f^{k}.f]$}}}}}}$}}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\raise
11.0pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Loop1)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
39.50917pt\vbox{\hbox{\hskip-39.50916pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma(x)=\textsf{bool}\qquad\Gamma\vdash
C\dashv\Gamma$}}}\vbox{}}}\over\hbox{\hskip
31.0439pt\vbox{\vbox{}\hbox{\hskip-31.0439pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{while}(x)\\{C\\}\dashv\Gamma$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
9.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Branch1)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
108.64722pt\vbox{\hbox{\hskip-108.64722pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f_{1}\rightharpoonup
z])\vdash
C_{1}\dashv\Gamma_{4}\qquad\Gamma\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f_{2}\rightharpoonup
z])\vdash C_{2}\dashv\Gamma_{4}$}}}\vbox{}}}\over\hbox{\hskip
94.73355pt\vbox{\vbox{}\hbox{\hskip-94.73355pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f_{1}\mid
f_{2}\rightharpoonup z])\vdash\textsf{if}(x.f_{1}==z)\textsf{ then
}C_{1}\textsf{ else }C_{2}\dashv\Gamma_{4}$}}}}}}$}}\hbox{}$}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\raise
9.81111pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Branch3)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
116.3279pt\vbox{\hbox{\hskip-116.3279pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
y\setminus\textsf{null}])\vdash
C_{1}\dashv\Gamma^{\prime}\qquad\Gamma,\,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
y])\vdash C_{2}\dashv\Gamma^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
92.30452pt\vbox{\vbox{}\hbox{\hskip-92.30452pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
y])\vdash\textsf{if}(x.f==\textsf{null})\textsf{ then }C_{1}\textsf{ else
}C_{2}\dashv\Gamma^{\prime}$}}}}}}$}}\hbox{}$}\penalty 50\hskip 20.00003pt
plus 0.5fil minus 5.0pt\raise
11.0pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Loop2)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
87.08838pt\vbox{\hbox{\hskip-87.08836pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f\rightharpoonup\\_])\vdash
C\dashv\Gamma,x:\textsf{rcuItr}\;\rho^{\prime}\;\mathcal{N}([f\rightharpoonup\\_])$}}}\vbox{}}}\over\hbox{\hskip
118.77628pt\vbox{\vbox{}\hbox{\hskip-118.77626pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f\rightharpoonup\\_])\vdash\textsf{while}(x.f\neq\textsf{null})\\{C\\}\dashv
x:\textsf{rcuItr}\;\rho^{\prime}\;\mathcal{N}([f\rightharpoonup\textsf{null}]),\,\Gamma$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
9.81111pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Branch2)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
62.79903pt\vbox{\hbox{\hskip-62.79901pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma(x)=\textsf{bool}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
C_{1}\dashv\Gamma^{\prime}\qquad\Gamma\vdash
C_{2}\dashv\Gamma^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
42.30031pt\vbox{\vbox{}\hbox{\hskip-42.3003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{if}(x)\textsf{
then }C_{1}\textsf{ else }C_{2}\dashv\Gamma^{\prime}$}}}}}}$}}\hbox{}$}$

Figure 4: Type rules for control-flow.

It is often necessary to abstract the contents of field maps or paths, without
simply forgetting the contents entirely. In a binary search tree, for example,
it may be the case that one node is a child of another, but _which_ parent
field points to the child depends on which branch was followed in an earlier
conditional (consider the lookup in a BST, which alternates between following
left and right children). In Figure 5, we see that cur aliases different
fields of par – either $Left$ or $Right$ – in different branches of the
conditional. The types after the conditional must overapproximate this, here
as $Left|Right\mapsto cur$ in par’s field map, and a similar path disjunction
in cur’s path. This is reflected in Figure 3’s T-NSub1-5 and T-PSub1-2 –
within each branch, each type is coerced to a supertype to validate the
control flow join.

Another type of control flow join is handling loop invariants – where paths
entering the loop meet the back-edge from the end of a loop back to the start
for repetition. Because our types include paths describing how they are
reachable from the root, some abstraction is required to give loop invariants
that work for any number of iterations – in a loop traversing a linked list,
the iterator pointer would naïvely have different paths from the root on each
iteration, so the exact path is not loop invariant. However, the paths
explored by a loop are regular, so we can abstract the paths by permitting
(implicitly) existentially quantified indexes on path fragments, which express
the existence of _some_ path, without saying _which_ path. The use of an
explicit abstract repetition allows the type system to preserve the fact that
different references have common path prefixes, even after a loop.

Assertions for the add function in lines 19 and 20 of Figure 2 show the loop’s
effects on paths of iterator references used inside the loop, cur and par. On
line 20, par’s path contains has $(Next)^{k}$. The $k$ in the $(Next)^{k}$
abstracts the number of loop iterations run, implicitly assumed to be non-
negative. The trailing $Next$ in cur’s path on line 19 – $(Next)^{k}.Next$ –
expresses the relationship between cur and par: par is reachable from the root
by following $Next$ $k$ times, and cur is reachable via one additional $Next$.
The types of 19 and 20, however, are not the same as lines 23 and 24, so an
additional adjustment is needed for the types to become loop-invariant.
_Reindexing_ (T-ReIndex in Figure 4) effectively increments an abstract loop
counter, contracting $(Next)^{k}.Next$ to $Next^{k}$ everywhere in a type
environment. This expresses the same relationship between par and cur as
before the loop, but the choice of $k$ to make these paths accurate after each
iteration would be one larger than the choice before. Reindexing the type
environment of lines 23–24 yields the type environment of lines 19–20, making
the types loop invariant. The reindexing essentially chooses a new value for
the abstract $k$. This is sound, because the uses of framing in the heap
mutation related rules of the type system ensure uses of any indexing variable
are never separated – either all are reindexed, or none are.

⬇

1$\\{cur:\mathsf{rcuItr}\;Left|Right\;\\{\\},\;\;par:\mathsf{rcuItr}\;\epsilon\;\\{Left|Right\mapsto
cur\\}\\}$

2if(par.Left == cur){

3
$\\{cur:\mathsf{rcuItr}\;Left\;\\{\\},\;\;par:\mathsf{rcuItr}\;\epsilon\;\\{Left\mapsto
cur\\}\\}$

4 par = cur;

5 cur = par.Left;

6
$\\{cur:\mathsf{rcuItr}\;Left.Left\;\\{\\},\;\;par:\mathsf{rcuItr}\;Left\;\\{Left\mapsto
cur\\}\\}$

7}else{

8
$\\{cur:\mathsf{rcuItr}\;Right\;\\{\\},\;\;par:\mathsf{rcuItr}\;\epsilon\;\\{Right\mapsto
cur\\}\\}$

9 par = cur;

10 cur = par.Right;

11
$\\{cur:\mathsf{rcuItr}\;Right.Right\;\\{\\},\;\;par:\mathsf{rcuItr}\;Right\;\\{Right\mapsto
cur\\}\\}$

12}

13$\\{cur:\mathsf{rcuItr}\;Left|Right.Left|Right\;\\{\\},\;\;par:\mathsf{rcuItr}\;Left|Right\;\\{Left|Right\mapsto
cur\\}\\}$

Figure 5: Choosing fields to read.

While abstraction is required to deal with control flow joins, reasoning about
whether and which nodes are unlinked or replaced, and whether cycles are
created, requires precision. Thus the type system also includes means (Figure
4) to refine imprecise paths and field maps. In Figure 5, we see a conditional
with the condition $par.Left==cur$. The type system matches this condition to
the imprecise types in line 1’s typing assertion, and refines the initial type
assumptions in each branch accordingly (lines 2 and 7) based on whether
execution reflects the truth or falsity of that check. Similarly, it is
sometimes required to check – and later remember – whether a field is null,
and the type system supports this.

###  4.2 Types in Action

The system has three forms of typing judgement: $\Gamma\vdash C$ for standard
typing outside RCU critical sections; $\Gamma\vdash_{R}C\dashv\Gamma^{\prime}$
for reader critical sections, and $\Gamma\vdash_{M}C\dashv\Gamma^{\prime}$ for
writer critical sections. The first two are straightforward, essentially
preventing mutation of the data structure, and preventing nesting of a writer
critical section inside a reader critical section. The last, for writer
critical sections, is flow sensitive: the types of variables may differ before
and after program statements. This is required in order to reason about local
assumptions at different points in the program, such as recognizing that a
certain action may unlink a node. Our presentation here focuses exclusively on
the judgment for the write-side critical sections.

Below, we explain our types through the list-based bag implementation [27]
from Figure 2, highlighting how the type rules handle different parts of the
code. Figure 2 is annotated with “assertions” – local type environments – in
the style of a Hoare logic proof outline. As with Hoare proof outlines, these
annotations can be used to construct a proper typing derivation.

Reading a Global RCU Root All RCU data structures have fixed roots, which we
characterize with the rcuRoot type. Each operation in Figure 2 begins by
reading the root into a new rcuItr reference used to begin traversing the
structure. After each initial read (line 12 of add and line 4 of remove), the
path of cur reference is the empty path ($\epsilon$) and the field map is
empty ($\\{\\}$), because it is an alias to the root, and none of its field
contents are known yet.

Reading an Object Field and a Variable As expected, we explore the heap of the
data structure via reading the objects’ fields. Consider line 6 of remove and
its corresponding pre- and post- type environments. Initially par’s field map
is empty. After the field read, its field map is updated to reflect that its
$Next$ field is aliased in the local variable cur. Likewise, afer the update,
cur’s path is $Next$ ($=\epsilon\cdot Next$), extending the par node’s path by
the field read. This introduces field aliasing information that can
subsequently be used to reason about unlinking.

Unlinking Nodes Line 24 of remove in Figure 2 unlinks a node. The type
annotations show that before that line cur is in the structure (rcuItr), while
afterwards its type is unlinked. The type system checks that this unlink
disconnects only one node: note how the types of par, cur, and curl just
before line 24 completely describe a section of the list.

Grace and Reclamation After the referent of cur is unlinked, concurrent
readers traversing the list may still hold references. So it is not safe to
actually reclaim the memory until after a grace period. Lines 28–29 of remove
initiate a grace period and wait for its completion. At the type level, this
is reflected by the change of cur’s type from unlinked to freeable, reflecting
the fact that the grace period extends until any reader critical sections that
might have observed the node in the structure have completed. This matches the
precondition required by our rules for calling Free, which further changes the
type of cur to undef reflecting that cur is no longer a valid reference. The
type system also ensures no local (writer) aliases exist to the freed node and
understanding this enforcement is twofold. First, the type system requires
that only unlinked heap nodes can be freed. Second, framing relations in rules
related to the heap mutation ensure no local aliases still consider the node
linked.

Fresh Nodes Some code must also allocate new nodes, and the type system must
reason about how they are incorporated into the shared data structure. Line 8
of the add method allocates a new node nw, and lines 10 and 29 initialize its
fields. The type system gives it a fresh type while tracking its field
contents, until line 32 inserts it into the data structure. The type system
checks that nodes previously reachable from cur remain reachable: note the
field maps of cur and nw in lines 30–31 are equal (trivially, though in
general the field need not be null).

###  4.3 Type Rules

$\displaystyle\framebox{$\Gamma\vdash_{M}\alpha\dashv\Gamma^{\prime}$}\;\;\raise
9.27443pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Root)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
17.59157pt\vbox{\hbox{\hskip-17.59155pt\hbox{\hbox{$\displaystyle\displaystyle
y\not\in\textsf{FV}(\Gamma)$}}}\vbox{}}}\over\hbox{\hskip
83.67361pt\vbox{\vbox{}\hbox{\hskip-83.67361pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,r\textsf{:rcuRoot},y\textsf{:undef}\vdash
y=r\dashv
y\textsf{:rcuItr}\epsilon\mathcal{N}_{\emptyset},r\textsf{:rcuRoot},\Gamma$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
10.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-ReadS)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
17.53162pt\vbox{\hbox{\hskip-17.5316pt\hbox{\hbox{$\displaystyle\displaystyle
z\not\in\textsf{FV}(\Gamma)$}}}\vbox{}}}\over\hbox{\hskip
95.54099pt\vbox{\vbox{}\hbox{\hskip-95.54099pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,z:\\_,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\vdash
z=x\dashv
x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N},z:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N},\Gamma$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\raise
9.27443pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Alloc)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
56.16577pt\vbox{\vbox{}\hbox{\hskip-56.16577pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x\textsf{:undef}\vdash
x=\texttt{new}\dashv
x\textsf{:rcuFresh}\mathcal{N}_{\emptyset},\Gamma$}}}}}}$}}\hbox{}$}\;\;\raise
9.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Free)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
43.59691pt\vbox{\vbox{}\hbox{\hskip-43.59691pt\hbox{\hbox{$\displaystyle\displaystyle
x\textsf{:freeable}\vdash\textsf{Free}(x)\dashv
x\textsf{:undef}$}}}}}}$}}\hbox{}$}\penalty 50\hskip 20.00003pt plus 0.5fil
minus 5.0pt\raise
10.5pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-ReadH)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
37.00221pt\vbox{\hbox{\hskip-37.0022pt\hbox{\hbox{$\displaystyle\displaystyle\rho.f=\rho^{\prime}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle
z\not\in\textsf{FV}(\Gamma)$}}}}\vbox{}}}\over\hbox{\hskip
101.07782pt\vbox{\vbox{}\hbox{\hskip-101.0778pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,z:\\_,x\textsf{:rcuItr}\rho\mathcal{N}\vdash
z=x.f\dashv x\textsf{:rcuItr}\rho\mathcal{N}([f\rightharpoonup
z]),z\textsf{:rcuItr}\rho^{\prime}\mathcal{N}_{\emptyset},\Gamma$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-WriteFH)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
61.82109pt\vbox{\hbox{\hskip-61.82109pt\hbox{\hbox{$\displaystyle\displaystyle
z:\textsf{rcuItr}\rho.f\\_\quad\mathcal{N}(f)=z\quad f\notin
dom(\mathcal{N}^{\prime})$}}}\vbox{}}}\over\hbox{\hskip
128.93918pt\vbox{\vbox{}\hbox{\hskip-128.93918pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,p\textsf{:rcuFresh}\mathcal{N}^{\prime},x\textsf{:rcuItr}\rho\mathcal{N}\vdash_{M}p.f=z\dashv
p\textsf{:rcuFresh}\mathcal{N}^{\prime}([f\rightharpoonup
z]),x\textsf{:rcuItr}\rho\mathcal{N}([f\rightharpoonup
z]),\Gamma$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\raise
9.71388pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(T-Sync)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
45.3848pt\vbox{\vbox{}\hbox{\hskip-45.38478pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{SyncStart};\textsf{SyncStop}\dashv\Gamma[\overline{x\textsf{:freeable}/x\textsf{:unlinked}}]$}}}}}}$}}\hbox{}$}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-UnlinkH)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
200.69812pt\vbox{\hbox{\hskip-167.90443pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}(f_{1})=z$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\rho.f_{1}=\rho_{1}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\rho_{1}.f_{2}=\rho_{2}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}^{\prime}=\mathcal{N}([f_{1}\rightharpoonup
z\setminus r])$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall_{f\in
dom(\mathcal{N}_{1})}\ldotp f\neq
f_{2}\implies(\mathcal{N}_{1}(f)=\textsf{null})$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}(f_{1})=z$}}}}}}}}\vbox{\hbox{\hskip-200.6981pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}_{1}(f_{2})=r$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\begin{array}[]{l}\forall_{n\in\Gamma,m,\mathcal{N}_{3},p_{3},f}\ldotp
n\textsf{:rcuItr}\,\rho_{3}\,\mathcal{N}_{3}([f\rightharpoonup
m])\implies\left\\{\begin{array}[]{l}((\neg\mathsf{MayAlias}(\rho_{3},\\{\rho,\rho_{1},\rho_{2}\\}))\land(m\not\in\\{z,r\\}))\@arraycr\land(\forall_{\rho_{4}\neq\epsilon}\ldotp\neg\mathsf{MayAlias}(\rho_{3},\rho_{2}.\rho_{4}))\end{array}\right.\end{array}$}}}}\vbox{}}}}\over\hbox{\hskip
135.2134pt\vbox{\vbox{}\hbox{\hskip-135.2134pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x\textsf{:rcuItr}\rho\mathcal{N},z\textsf{:rcuItr}\rho_{1}\mathcal{N}_{1},r\textsf{:rcuItr}\rho_{2}\mathcal{N}_{2}\vdash
x.f_{1}=r\dashv
z\textsf{:unlinked},x\textsf{:rcuItr}\rho\mathcal{N}^{\prime},r\textsf{:rcuItr}\rho_{1}\mathcal{N}_{2},\Gamma$}}}}}}$}}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-Replace)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
184.70705pt\vbox{\hbox{\hskip-49.58844pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}(f)=o$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}^{\prime}=\mathcal{N}([f\rightharpoonup
o\setminus
n])$}}}}\vbox{\hbox{\hskip-184.70705pt\hbox{\hbox{$\displaystyle\displaystyle\rho.f=\rho_{1}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}_{1}=\mathcal{N}_{2}\qquad\textsf{FV}(\Gamma)\cap\\{p,o,n\\}=\emptyset$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall_{x\in\Gamma,\mathcal{N}_{3},\rho_{2},f_{1},y}\ldotp(x\textsf{:rcuItr}\,\rho_{2}\,\mathcal{N}_{3}([f_{1}\rightharpoonup
y]))\implies(\neg\mathsf{MayAlias}(\rho_{2},\\{\rho,\rho_{1}\\})\land(y\neq
o))$}}}}}\vbox{}}}}\over\hbox{\hskip
137.04997pt\vbox{\vbox{}\hbox{\hskip-137.04996pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,p\textsf{:rcuItr}\rho\mathcal{N},o\textsf{:rcuItr}\rho_{1}\mathcal{N}_{1},n\textsf{:rcuFresh}\mathcal{N}_{2}\vdash
p.f=n\dashv
p\textsf{:rcuItr}\rho\mathcal{N}^{\prime},n\textsf{:rcuItr}\rho_{1}\mathcal{N}_{2},o\textsf{:unlinked},\Gamma$}}}}}}$}}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{{\vbox{\hbox{\hbox{\small\small{\scriptsize(T-Insert)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
189.9849pt\vbox{\hbox{\hskip-97.12819pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}^{\prime}=\mathcal{N}([f\rightharpoonup
o\setminus n])$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\rho.f=\rho_{1}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\rho_{1}.f_{4}=\rho_{2}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}(f)=\mathcal{N}_{1}(f_{4})$}}}}}}\vbox{\hbox{\hskip-189.98488pt\hbox{\hbox{$\displaystyle\displaystyle\forall_{f_{2}\in
dom(\mathcal{N}_{1})}\ldotp f_{4}\neq
f_{2}\implies\mathcal{N}_{1}(f_{2})=\textsf{null}$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{FV}(\Gamma)\cap\\{p,o,n\\}=\emptyset$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall_{x\in\Gamma,\mathcal{N}_{3},\rho_{3},f_{1},y}\ldotp(x:\textsf{rcuItr}\,\rho_{3}\,\mathcal{N}_{3}([f_{1}\rightharpoonup
y]))\implies(\forall_{\rho_{4}\neq\epsilon}\ldotp\neg\mathsf{MayAlias}(\rho_{3},\rho.\rho_{4}))$}}}}}\vbox{}}}}\over\hbox{\hskip
139.28337pt\vbox{\vbox{}\hbox{\hskip-139.28337pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,p\textsf{:rcuItr}\rho\mathcal{N},o\textsf{:rcuItr}\rho_{1}\mathcal{N}_{2},n\textsf{:rcuFresh}\mathcal{N}_{1}\vdash
p.f=n\dashv
p\textsf{:rcuItr}\rho\mathcal{N}^{\prime},n\textsf{:rcuItr}\rho_{1}\mathcal{N}_{1},o\textsf{:rcuItr}\rho_{2}\mathcal{N}_{2},\Gamma$}}}}}}$}}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\framebox{$\Gamma\vdash_{M}C\dashv\Gamma^{\prime}$}\;\;\raise
11.0pt\hbox{$\hbox{$\hbox{\small\small{\scriptsize(ToRCUWrite)}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
151.02028pt\vbox{\hbox{\hskip-151.02026pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{NoFresh}(\Gamma^{\prime})\qquad\textsf{NoUnlinked}(\Gamma^{\prime})\qquad\textsf{NoFreeable}(\Gamma^{\prime})$}\hskip
14.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,y\textsf{:rcuItr}\\_\vdash_{M}C\dashv\Gamma^{\prime}\qquad\textsf{FType}(f)=\textsf{RCU}$}}}}\vbox{}}}\over\hbox{\hskip
48.03267pt\vbox{\vbox{}\hbox{\hskip-48.03267pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{RCUWrite}\,x.f\textsf{
as }y\textsf{ in }\\{C\\}$}}}}}}$}}\hbox{}$}$

Figure 6: Type rules for write side critical section.

Figure 6 gives the primary type rules used in checking write-side critical
section code as in Figure 2.

T-Root reads a root pointer into an rcuItr reference, and T-ReadS copies a
local variable into another. In both cases, the free variable condition
ensures that updating the modified variable does not invalidate field maps of
other variables in $\Gamma$. These free variable conditions recur throughout
the type system, and we will not comment on them further. T-Alloc and T-Free
allocate and reclaim objects. These rules are relatively straightforward.
T-ReadH reads a field into a local variable. As suggested earlier, this rule
updates the post-environment to reflect that the overwritten variable $z$
holds the same value as $x.f$. T-WriteFH updates a field of a _fresh_ (thread-
local) object, similarly tracking the update in the fresh object’s field map
at the type level. The remaining rules are a bit more involved, and form the
heart of the type system.

Grace Periods T-Sync gives pre- and post-environments to the compound
statement SyncStart;SyncStop implementing grace periods. As mentioned earlier,
this updates the environment afterwards to reflect that any nodes unlinked
before the wait become freeable afterwards.

Unlinking T-UnlinkH type checks heap updates that remove a node from the data
structure. The rule assumes three objects $x$, $z$, and $r$, whose identities
we will conflate with the local variable names in the type rule. The rule
checks the case where $x.f_{1}==z$ and $z.f_{2}==r$ initially (reflected in
the path and field map components, and a write $x.f_{1}=r$ removes $z$ from
the data structure (we assume, and ensure, the structure is a tree).

The rule must also avoid unlinking multiple nodes: this is the purpose of the
first (smaller) implication: it ensures that beyond the reference from $z$ to
$r$, all fields of $z$ are null.

Finally, the rule must ensure that no types in $\Gamma$ are invalidated. This
could happen one of two ways: either a field map in $\Gamma$ for an alias of
$x$ duplicates the assumption that $x.f_{1}==z$ (which is changed by this
write), or $\Gamma$ contains a descendant of $r$, whose path from the root
will change when its ancestor is modified. The final assumption of T-UnlinkH
(the implication) checks that for every rcuItr reference $n$ in $\Gamma$, it
is not a path alias of $x$, $z$, or $r$; no entry of its field map ($m$)
refers to $r$ or $z$ (which would imply $n$ aliased $x$ or $z$ initially); and
its path is not an extension of $r$ (i.e., it is not a descendant). MayAlias
is a predicate on two paths (or a path and set of paths) which is true if it
is possible that any concrete paths the arguments may abstract (e.g., via
adding non-determinism through $|$ or abstracting iteration with indexing)
_could_ be the same. The negation of a MayAlias use is true only when the
paths are guaranteed to refer to different locations in the heap.

$R$$H_{0}$$H_{1}$$H_{f}$$H_{2}$$H_{4}$$pr$$cr$$cf$$crl$$lm$$a_{0}$$a_{1}$$l$$l$$r$$l$$r$$l$
(a) Freshly allocated heap node referenced by $cf$

$R$$H_{0}$$H_{1}$$H_{f}$$H_{2}$$H_{4}$$pr$$cr$$cf$$crl$$lm$$a_{0}$$a_{1}$$l$$r$$l$$r$$l$$l$
(b) Safe replacement of the heap node referenced by $cr$ with the fresh heap
node referenced by $cf$.

Figure 7: Replacing existing heap nodes with fresh ones. Type rule T-Replace.

Replacing with a Fresh Node Replacing with a rcuFresh reference faces the same
aliasing complications as direct unlinking. We illustrate these challenges in
Figures 7(a) and 7(b). Our technical report [22] also includes Figures 32a and
32b in Appendix D to illustrate complexities in unlinking. The square $R$
nodes are root nodes, and $H$ nodes are general heap nodes. All resources in
thick straight lines and dotted lines form the memory foot print of a node
replacement. The hollow thick circular nodes – $pr$ and $cr$ – point to the
nodes involved in replacing $H_{1}$ (referenced by cr) wih $H_{f}$ (referenced
by $cf$) in the structure. We may have $a_{0}$ and $a_{1}$ which are aliases
with $pr$ and $cr$ respectively. They are path-aliases as they share the same
path from root to the node that they reference. Edge labels $l$ and $r$ are
abbreviations for the $Left$ and $Right$ fields of a binary search tree. The
thick dotted $H_{f}$ denotes the freshly allocated heap node referenced by
thick dotted $cf$. The thick dotted field $l$ is set to point to the referent
of $cl$ and the thick dotted field $r$ is set to point to the referent of the
heap node referenced by $lm$.

$H_{f}$ initially (Figure 7(a)) is not part of the shared structure. If it
was, it would violate the tree shape requirement imposed by the type system.
This is why we highlight it separately in thick dotts — its static type would
be rcuFresh. Note that we cannot duplicate a rcuFresh variable, nor read a
field of an object it points to. This restriction localizes our reasoning
about the effects of replacing with a fresh node to just one fresh reference
and the object it points to. Otherwise another mechanism would be required to
ensure that once a fresh reference was linked into the heap, there were no
aliases still typed as fresh — since that would have risked linking the same
reference into the heap in two locations.

The transition from the Figure 7(a) to 7(b) illustrates the effects of the
heap mutation (replacing with a fresh node). The reasoning in the type system
for replacing with a fresh node is nearly the same as for unlinking an
existing node, with one exception. In replacing with a fresh node, there is no
need to consider the paths of nodes deeper in the tree than the point of
mutation. In the unlinking case, those nodes’ static paths would become
invalid. In the case of replacing with a fresh node, those descendants’ paths
are preserved. Our type rule for ensuring safe replacement (T-Replace)
prevents path aliasing (representing the nonexistence of $a_{0}$ and $a_{1}$
via dashed lines and circles) by negating a MayAlias query and prevents field
mapping aliasing (nonexistence of any object field from any other context
pointing to $cr$) via asserting $(y\neq o)$. It is important to note that
objects($H_{4},H_{2}$) in the field mappings of the $cr$ whose referent is to
be unlinked captured by the heap node’s field mappings referenced by $cf$ in
rcuFresh. This is part of enforcing locality on the heap mutation and captured
by assertion $\mathcal{N}=\mathcal{N}^{\prime}$ in the type rule(T-Replace).

Inserting a Fresh Node T-Insert type checks heap updates that link a fresh
node into a linked data structure. Inserting a rcuFresh reference also faces
some of the aliasing complications that we have already discussed for direct
unlinking and replacing a node. Unlike the replacement case, the path to the
last heap node (the referent of $o$) from the root is _extended_ by $f$, which
risks falsifying the paths for aliases and descendants of $o$. The final
assumption(the implication) of T-Insert checks for this inconsistency.

There is also another rule, T-LinkF-Null, not shown in Figure 6, which handles
the case where the fields of the fresh node are not object references, but
instead all contain null (e.g., for appending to the end of a linked list or
inserting a leaf node in a tree).

Critical Sections (Referencing inside RCU Blocks) We introduce the syntactic
sugaring $\textsf{RCUWrite }x.f\textsf{ as }y\textsf{ in }\\{C\\}$ for write-
side critical sections where the analogous syntactic sugaring can be found for
read-side critical sections in Appendix E of the technical report [22].

The type system ensures unlinked and freeable references are handled linearly,
as they cannot be dropped – coerced to undef. The top-level rule ToRCUWrite in
Figure 6 ensures unlinked references have been freed by forbidding them in the
critical section’s post-type environment. Our technical report [22] also
includes the analogous rule ToRCURead for the read critical section in Figure
33 of Appendix E.

Preventing the reuse of rcuItr references across critical sections is subtler:
the non-critical section system is not flow-sensitive, and does not include
rcuItr. Therefore, the initial environment lacks rcuItr references, and
trailing rcuItr references may not escape.

##  5 Evaluation

$R$$T_{0}$$T$$H_{1}$$T_{2}$$H_{2}$$T_{4}$$T$$H_{s}$$T$$T_{6}$$pr$$cr$$lp$ (a)
The writer traverses subtree $T_{0}$ to find the heap node $H_{1}$ with local
references $pr$ and $cr$. Black-filled node representing the null node.

$R$$T_{0}$$T$$H_{1}$$H_{s}$$T_{2}$$H_{2}$$T_{4}$$T$$H_{s}$$T$$pr$$cr$$cf$$lp$$sc$$T_{6}$
(b) Traverse subtree $T_{4}$ starting from $H_{2}$ with references $lp$ and
$sc$ to find successor $H_{s}$ of $H_{1}$. Duplicating $H_{s}$ as a fresh heap
node before replacing $H_{1}$ with the fresh one.

$R$$T_{0}$$T$$H_{1}$$H_{s}$$T_{2}$$H_{2}$$T_{4}$$T$$H_{s}$$T$$T_{6}$$pr$$cr$$cf$$lp$$sc$
(c) Replace $H_{1}$ with fresh successor and synchronize with the readers.

$R$$T_{0}$$T$$H_{s}$$T_{2}$$H_{2}$$T_{4}$$T$$H_{s}$$T$$pr$$cf$$lp$$sc$$T_{6}$
(d) Unlinks old successor referenced by $sc$.

$R$$T_{0}$$T$$H_{s}$$T_{2}$$H_{2}$$T_{4}$$T$$H_{s}$$T$$pr$$cf$$lp$$sc$$T_{6}$
(e) Safe unlinking of the old successor whose left subtree is null.

$R$$T_{0}$$T$$H_{s}$$T_{2}$$H_{2}$$T_{4}$$T$$T$$T_{6}$$pr$$lp$$cf$ Figure 8:
Reclamation of the old successor.

Figure 9: Delete of a heap node with two children in BST [3].

We have used our type system to check correct use of RCU primitives in two RCU
data structures representative of the broader space.

Figure 2 gives the type-annotated code for add and remove operations on a
linked list implementation of a bag data structure, following McKenney’s
example [27]. Our technical report [22] contains code for membership checking.

We have also type checked the most challenging part of an RCU binary search
tree, the deletion (which also contains the code for a lookup). Our
implementation is a slightly simplified version of the Citrus BST [3]: their
code supports fine-grained locking for multiple writers, while ours supports
only one writer by virtue of using our single-writer primitives. For lack of
space the annotated code is only in Appendix B of the technical report [22],
but here we emphasise the important aspects our type system via showing its
capabilities of typing BST delete method, which also includes looking up for
the node to be deleted.

In Figure 9, we show the steps for deleting the heap node $H_{1}$. To locate
the node $H_{1}$, as shown in Figure 8(a), we first traverse the subtree
$T_{0}$ with references $pr$ and $cr$, where $pr$ is the parent of $cr$ during
traversal:

$pr:rcuItr(l|r)^{k}\\{l|r\rightarrow cr\\},\,cr:rcuItr(l|r)^{k}.(l|r)\\{\\}$

Traversal of $T_{0}$ is summarized as $(l|k)^{k}$. The most subtle aspect of
the deletion is the final step in the case the node $H_{1}$ to remove has both
children; as shown in Figure 8(b), the code must traverse the subtree $T_{4}$
to locate the next element in collection order: the node $H_{s}$, the left-
most node of $H_{1}$’s right child ($sc$) and its parent ($lp$):

$lp:(l|r)^{k}.(l|r).r.(l|r)^{m}\\{l|r\rightarrow
sc\\},\,sc:(l|r)^{k}.(l|r).r.l.(l)^{m}.l\\{\\}$

where the traversal of $T_{4}$ is summarized as $(l|m)^{m}$.

Then $H_{s}$ is copied into a new freshly-allocated node as shown in Figure
8(b), which is then used to _replace_ node $H_{1}$ as shown in Figure 8(c):
the replacement’s fields exactly match $H_{1}$’s except for the data
(T-Replace via $\mathcal{N}_{1}=\mathcal{N}_{2}$) as shown in Figure 8(b), and
the parent is updated to reference the replacement, unlinking $H_{1}$.

At this point, as shown in Figures 8(c) and 8(d), there are two nodes with the
same value in the tree (the weak BST property of the Citrus BST [3]): the
replacement node, and what was the left-most node under $H_{1}$’s right child.
This latter (original) node $H_{s}$ must be unlinked as shown in Figure 8(e),
which is simpler because by being left-most the left child is null, avoiding
another round of replacement (T-UnlinkH via $\forall_{f\in
dom(\mathcal{N}_{1})}\ldotp f\neq
f_{2}\implies(\mathcal{N}_{1}(f)=\textsf{null}$).

Traversing $T_{4}$ to find successor complicates the reasoning in an
interesting way. After the successor node $H_{s}$ is found in 8(b), there are
_two_ local unlinking operations as shown in Figures 8(c) and 8(e), at
different depths of the tree. This is why the type system must keep separate
abstract iteration counts, e.g., $k$ of $(l|r)^{k}$ or $m$ of $(l|r)^{m}$, for
traversals in loops — these indices act like multiple cursors into the data
structure, and allow the types to carry enough information to keep those
changes separate and ensure neither introduces a cycle.

To the best of our knowledge, we are the first to check such code for memory-
safe use of RCU primitives modularly, without appeal to the specific
implementation of RCU primitives.

##  6 Soundness

This section outlines the proof of type soundness – our full proof appears the
accompanying technical report [22]. We prove type soundness by embedding the
type system into an abstract concurrent separation logic called the Views
Framework [10], which when given certain information about proofs for a
specific language (primitives and primitive typing) gives back a full program
logic including choice and iteration. As with other work taking this approach
[16, 15], this consists of several key steps explained in the following
subsections, but a high-level informal soundness argument is twofold. First,
because the parameters given to the Views framework ensure the Views logic’s
Hoare triples $\\{-\\}C\\{-\\}$ are sound, this proves soundness of the type
rules with respect to type denotations. Second, as our denotation of types
encodes the property that the post-environment of any type rule accurately
characterizes which memory is linked vs. unlinked, etc., and the global
invariants ensure all allocated heap memory is reachable from the root or from
some thread’s stack, this entails that our type system prevents memory leaks.

###  6.1 Proof

This section provides more details on how the Views Framework [10] is used to
prove soundness, giving the major parameters to the framework and outlining
global invariants and key lemmas.

Logical State Section 3 defined what Views calls _atomic actions_ (the
primitive operations) and their semantics on runtime _machine states_. The
Views Framework uses a separate notion of instrumented (logical) state over
which the logic is built, related by a concretization function
$\lfloor-\rfloor$ taking an instrumented state to the machine states of
Section 3. Most often — including in our proof — the logical state adds useful
auxiliary state to the machine state, and the concretization is simply
projection. Thus we define our logical states LState as:

  * •

A machine state, $\sigma=(s,h,l,rt,R,B)$

  * •

An observation map, O, of type $\textsf{Loc}\to\mathcal{P}(\textsf{obs})$

  * •

Undefined variable map, $U$, of type
$\mathcal{P}(\textsf{Var}\times\textsf{TID})$

  * •

Set of threads, $T$, of type $\mathcal{P}(\textsf{TIDS})$

  * •

A to-free map (or free list), $F$, of type
$\textsf{Loc}\rightharpoonup\mathcal{P}(\textsf{TID})$

The thread ID set $T$ includes the thread ID of all running threads. The free
map $F$ tracks which reader threads may hold references to each location. It
is not required for execution of code, and for validating an implementation
could be ignored, but we use it later with our type system to help prove that
memory deallocation is safe. The (per-thread) variables in the undefined
variable map $U$ are those that should not be accessed (e.g., dangling
pointers).

The remaining component, the observation map $O$, requires some further
explanation. Each memory allocation / object can be _observed_ in one of the
following states by a variety of threads, depending on how it was used.

$\textsf{obs}:=\texttt{iterator}\;\mathrm{tid}\mid\texttt{unlinked}\mid\texttt{fresh}\mid\texttt{freeable}\mid\texttt{root}$

An object can be observed as part of the structure (iterator), removed but
possibly accessible to other threads, freshly allocated, safe to deallocate,
or the root of the structure.

Invariants of RCU Views and Denotations of Types Next, we aim to convey the
intuition behind the predicate WellFormed which enforces global invariants on
logical states, and how it interacts with the denotations of types (Figure 10)
in key ways.

WellFormed is the conjunction of a number of more specific invariants, which
we outline here. For full details, see Appendix A.2 of the technical report
[22].

#### The Invariant for Read Traversal

Reader threads access valid heap locations even during the grace period. The
validity of their heap accesses ensured by the observations they make over the
heap locations — which can only be iterator as they can only use local rcuItr
references. To this end, a Readers-Iterators-Only invariant asserts that
reader threads can only observe a heap location as iterator.

#### Invariants on Grace-Period

Our logical state includes a “free list” auxiliary state tracking which
readers are still accessing _each_ unlinked node during grace periods. This
must be consistent with the bounding thread set $B$ in the machine state, and
this consistency is asserted by the Readers-In-Free-List invariant. This is
essentially tracking which readers are being “shown grace” for each location.
The Iterators-Free-List invariant complements this by asserting all readers
with such observations on unlinked nodes are in the bounding thread set.

The writer thread can refer to a heap location in the free list with a local
reference either in type freeable or unlinked. Once the writer unlinks a heap
node, it first observes the heap node as unlinked then freeable. The
denotation of freeable is only valid following a grace period: it asserts no
readers hold aliases of the freeable reference. The denotation of unlinked
permits the either the same (perhaps no readers overlapped) or that it is in
the to-free list.

#### Invariants on Safe Traversal against Unlinking

The write-side critical section must guarantee that no updates to the heap
cause invalid memory accesses. The Writer-Unlink invariant asserts that a heap
location observed as iterator by the writer thread cannot be observed
differently by other threads. The denotation of the writer thread’s rcuItr
reference, $\llbracket\mathsf{rcuItr}\,\rho\,\mathcal{N}\rrbracket_{tid}$,
asserts that following a path from the root compatible with $\rho$ reaches the
referent, and all are observed as iterator.

The denotation of a reader thread’s rcuItr reference,
$\llbracket\mathsf{rcuItr}\rrbracket_{tid}$ and the invariants Readers-
Iterator-Only, Iterators-Free-List and Readers-In-Free-List all together
assert that a reader thread(which can also be a bounding thread) can view an
unlinked heap location(which can be in the free list) only as iterator. At the
same time, it is essential that reader threads arriving after a node is
unlinked cannot access it. The invariants Unlinked-Reachability and Free-List-
Reachability ensure that any unlinked nodes are reachable only from other
unlinked nodes, and never from the root.

#### Invariants on Safe Traversal against Inserting/Replacing

A writer replacing an existing node with a fresh one or inserting a single
fresh node assumes the fresh (before insertion) node is unreachable to readers
before it is published/linked. The Fresh-Writes invariant asserts that a fresh
heap location can only be allocated and referenced by the writer thread. The
relation between a freshly allocated heap and the rest of the heap is
established by the Fresh-Reachable invariant, which requires that there exists
no heap node pointing to the freshly allocated one. This invariant supports
the preservation of the tree structure. The Fresh-Not-Reader invariant
supports the safe traversal of the reader threads via asserting that they
cannot observe a heap location as fresh. Moreover, the denotation of the
rcuFresh type, $\llbracket\mathsf{rcuFresh}\,\mathcal{N}\rrbracket_{tid}$,
enforces that fields in $\mathcal{N}$ point to valid heap locations (observed
as iterator by the writer thread).

#### Invariants on Tree Structure

Our invariants enforce the tree structure heap layouts for data structures.
The Unique-Reachable invariant asserts that every heap location reachable from
root can only be reached with following an unique path. To preserve the tree
structure, Unique-Root enforces unreachability of the root from any heap
location that is reachable from root itself.

$\begin{array}[]{l@{\;\;=\;\;}l}\llbracket\,x:\textsf{rcuItr}\,\rho\,\mathcal{N}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{iterator}\,tid\in
O(s(x,tid)))\land(x\notin U)\\\ &\land(\forall_{f_{i}\in
dom(\mathcal{N})x_{i}\in
codom(\mathcal{N})}\ldotp\left\\{\begin{array}[]{l}s(x_{i},tid)=h(s(x,tid),f_{i})\\\
\land\textsf{iterator}\in O(s(x_{i},tid)))\end{array}\right.\\\
&\land(\forall_{\rho^{\prime},\rho^{\prime\prime}}\ldotp\rho^{\prime}.\rho^{\prime\prime}=\rho\implies\textsf{iterator}\,tid\in
O(h^{*}(rt,\rho^{\prime})))\\\ &\land h^{*}(rt,\rho)=s(x,tid)\land(l=tid\land
s(x,\\_)\notin dom(F)))\end{array}\right\\}\\\
\llbracket\,x:\textsf{rcuItr}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{iterator}\,tid\in
O(s(x,tid)))\land(x\notin U)\land\\\ &(tid\in
B)\implies\left\\{\begin{array}[]{l}(\exists_{T^{\prime}\subseteq
B}\ldotp\\{s(x,tid)\mapsto T^{\prime}\\}\cap F\neq\emptyset)\land\\\
\land(tid\in T^{\prime})\end{array}\right.\end{array}\right\\}\\\
\llbracket\,x:\textsf{unlinked}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{unlinked}\in
O(.s(x,tid))\land l=tid\land x\notin U)\land\\\ &(\exists_{T^{\prime}\subseteq
T}\ldotp s(x,tid)\mapsto T^{\prime}\in F\implies T^{\prime}\subseteq B\land
tid\notin T^{\prime})\end{array}\right\\}\\\
\llbracket\,x:\textsf{freeable}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&\begin{array}[]{l}\textsf{freeable}\in
O(s(x,tid))\land l=tid\land x\notin U\land\\\
s(x,tid)\mapsto\\{\emptyset\\}\in F\end{array}\end{array}\right\\}\\\
\llbracket\,x:\textsf{rcuFresh}\,\mathcal{N}\,\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{fresh}\in
O(s(x,tid))\land x\notin U\land s(x,tid)\notin dom(F))\\\ &(\forall_{f_{i}\in
dom(\mathcal{N}),x_{i}\in codom(\mathcal{N})}\ldotp
s(x_{i},tid)=h(s(x,tid),f_{i})\\\ &\land\textsf{iterator}\,tid\in
O(s(x_{i},tid))\land s(x_{i},tid)\notin dom(F))\end{array}\right\\}\\\
\llbracket
x:\textsf{undef}\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(x,tid)\in
U\land s(x,tid)\notin dom(F)\end{array}\right\\}\\\
\llbracket\,x:\textsf{rcuRoot}\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&\begin{array}[]{l}((rt\notin
U\land s(x,tid)=rt\land rt\in dom(h)\land\\\ O(rt)\in\textsf{root}\land
s(x,tid)\notin dom(F))\end{array}\end{array}\right\\}\end{array}$

$\textrm{provided}~{}h^{*}:(\textsf{Loc}\times\textsf{Path})\rightharpoonup\textsf{Val}$

Figure 10: Type Environments

Type Environments Assertions in the Views logic are (almost) sets of the
logical states that satisfy a validity predicate WellFormed, outlined above:

$\mathcal{M}\stackrel{{\scriptstyle def}}{{=}}\\{m\in(\textsf{MState}\times
O\times U\times T\times F)\mid\textsf{WellFormed}(m)\\}$

Every type environment represents a set of possible views (WellFormed logical
states) consistent with the types in the environment. We make this precise
with a denotation function

$\llbracket-\rrbracket\\_:\mathsf{TypeEnv}\rightarrow\mathsf{TID}\rightarrow\mathcal{P}(\mathcal{M})$

that yields the set of states corresponding to a given type environment. This
is defined as the intersection of individual variables’ types as in Figure 10.

Individual variables’ denotations are extended to context denotations slightly
differently depending on whether the environment is a reader or writer thread
context: writer threads own the global lock, while readers do not:

  * •

For read-side as $\llbracket x_{1}:T_{1},\ldots
x_{n}:T_{n}\rrbracket_{tid,\textsf{R}}=\llbracket
x_{1}:T_{1}\rrbracket_{tid}\cap\ldots\cap\llbracket
x_{n}:T_{n}\rrbracket_{tid}\cap\llbracket\textsf{R}\rrbracket_{tid}$ where
$\llbracket\textsf{R}\rrbracket_{tid}=\\{(s,h,l,rt,R,B),O,U,T,F\mid tid\in
R\\}$

  * •

For write-side as $\llbracket x_{1}:T_{1},\ldots
x_{n}:T_{n}\rrbracket_{tid,\textsf{M}}=\llbracket
x_{1}:T_{1}\rrbracket_{tid}\cap\ldots\cap\llbracket
x_{n}:T_{n}\rrbracket_{tid}\cap\llbracket\textsf{M}\rrbracket_{tid}$ where
$\llbracket\textsf{M}\rrbracket_{tid}=\\{(s,h,l,rt,R,B),O,U,T,F\mid tid=l\\}$

Composition and Interference To support framing (weakening), the Views
Framework requires that views form a partial commutative monoid under an
operation
$\bullet:\mathcal{M}\longrightarrow\mathcal{M}\longrightarrow\mathcal{M}$,
provided as a parameter to the framework. The framework also requires an
interference relation $\mathcal{R}\subseteq\mathcal{M}\times\mathcal{M}$
between views to reason about local updates to one view preserving validity of
adjacent views (akin to the small-footprint property of separation logic).
Figure 11 defines our composition operator and the core interference relation
$\mathcal{R}_{0}$ — the actual inferference between views (between threads, or
between a local action and framed-away state) is the reflexive transitive
closure of $\mathcal{R}_{0}$. Composition is mostly straightforward point-wise
union (threads’ views may overlap) of each component. Interference bounds the
interference writers and readers may inflict on each other. Notably, if a view
contains the writer thread, other threads may not modify the shared portion of
the heap, or release the writer lock. Other aspects of interference are
natural restrictions like that threads may not modify each others’ local
variables. WellFormed states are closed under both composition (with another
WellFormed state) and interference ($\mathcal{R}$ relates WellFormed states
only to other WellFormed states).

$\displaystyle\bullet\overset{\mathrm{def}}{=}(\bullet_{\sigma},\bullet_{O},\cup,\cup)\;\;(F_{1}\bullet_{F}F_{2})\overset{\mathrm{def}}{=}F_{1}\cup
F_{2}\texttt{ when }dom(F_{1})\cap dom(F_{2})=\emptyset$ $\displaystyle
O_{1}\bullet_{O}O_{2}(loc)\overset{\mathrm{def}}{=}O_{1}(loc)\cup
O_{2}(loc)\;\;(s_{1}\bullet_{s}s_{2})\overset{\mathrm{def}}{=}s_{1}\cup
s_{2}\texttt{ when }dom(s_{1})\cap dom(s_{2})=\emptyset$

$(h_{1}\bullet_{h}h_{2})(o,f)\overset{\mathrm{def}}{=}\left\\{\begin{array}[]{ll}\mathrm{undef}&\textrm{if}~{}h_{1}(o,f)=v\land
h_{2}(o,f)=v^{\prime}\land v^{\prime}\neq v\\\
v&\textrm{if}~{}h_{1}(o,f)=v\land h_{2}(o,f)=v\\\
v&\textrm{if}~{}h_{1}(o,f)=\mathrm{undef}\land h_{2}(o,f)=v\\\
v&\textrm{if}~{}h_{1}(o,f)=v\land h_{2}(o,f)=\mathrm{undef}\\\
\mathrm{undef}&\textrm{if}~{}h_{1}(o,f)=\mathrm{undef}\land
h_{2}(o,f)=\mathrm{undef}\end{array}\right.$

$\begin{array}[]{l}((s,h,l,rt,R,B),O,U,T,F)\mathcal{R}_{0}((s^{\prime},h^{\prime},l^{\prime},rt^{\prime},R^{\prime},B^{\prime}),O^{\prime},U^{\prime},T^{\prime},F^{\prime})\overset{\mathrm{def}}{=}\\\
\bigwedge\left\\{\begin{array}[]{l}l\in T\rightarrow(h=h^{\prime}\land
l=l^{\prime})\\\ l\in T\rightarrow F=F^{\prime}\\\ \forall
tid,o\ldotp\textsf{iterator}\,tid\in O(o)\rightarrow o\in dom(h)\\\ \forall
tid,o\ldotp\textsf{iterator}\,tid\in O(o)\rightarrow o\in dom(h^{\prime})\\\
\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in dom(h)\\\
\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h^{\prime})\\\ O=O^{\prime}\land U=U^{\prime}\land T=T^{\prime}\land
R=R^{\prime}\land rt=rt^{\prime}\\\ \forall x,t\in T\ldotp
s(x,t)=s^{\prime}(x,t)\end{array}\right\\}\end{array}$

Figure 11: Composition($\bullet$) and Thread Interference
Relation($\mathcal{R}_{0}$)

Stable Environment and Views Shift The framing/weakening type rule will be
translated to a use of the frame rule in the Views Framework’s logic. There
separating conjunction is simply the existence of two composable instrumented
states:

$m\in P\ast Q\stackrel{{\scriptstyle def}}{{=}}\exists m^{\prime}\ldotp\exists
m^{\prime\prime}\ldotp m^{\prime}\in P\land m^{\prime\prime}\in Q\land m\in
m^{\prime}\bullet m^{\prime\prime}$

In order to validate the frame rule in the Views Framework’s logic, the
assertions in its logic — sets of well-formed instrumented states — must be
restricted to sets of logical states that are _stable_ with respect to
expected interference from other threads or contexts, and interference must be
compatible in some way with separating conjunction. Thus a View — the actual
base assertions in the Views logic — are then:

$\textsf{View}_{\mathcal{M}}\stackrel{{\scriptstyle
def}}{{=}}\\{M\in\mathcal{P}(\mathcal{M})|\mathcal{R}(M)\subseteq M\\}$

Additionally, interference must distribute over composition:

$\forall m_{1},m_{2},m\ldotp(m_{1}\bullet
m_{2})\mathcal{R}m\Longrightarrow\begin{array}[]{ll}\exists
m^{\prime}_{1}m^{\prime}_{2}\ldotp m_{1}\mathcal{R}m^{\prime}_{1}\land
m_{2}\mathcal{R}m^{\prime}_{2}\land m\in m^{\prime}_{1}\bullet
m^{\prime}_{2}\end{array}$

Because we use this induced Views logic to prove soundness of our type system
by translation, we must ensure any type environment denotes a valid view:

######  Lemma 1 (Stable Environment Denotation-M)

For any _closed_ environment $\Gamma$ (i.e., $\forall
x\in\mathsf{dom}(\Gamma)\ldotp,\mathsf{FV}(\Gamma(x))\subseteq\mathsf{dom}(\Gamma)$):
$\mathcal{R}(\llbracket\Gamma\rrbracket_{\mathsf{M},tid})\subseteq\llbracket\Gamma\rrbracket_{\mathsf{M},tid}$.
Alternatively, we say that environment denotation is _stable_ (closed under
$\mathcal{R}$).

###### Proof

In Appendix A.1 Lemma 7 of the technical report [22].

We elide the statement of the analogous result for the read-side critical
section, available in Appendix A.1 of the technical report.

With this setup done, we we can state the connection between the Views
Framework logic induced by earlier parameters, and the type system from
Section 4. The induced Views logic has a familiar notion of Hoare triple —
$\\{p\\}C\\{q\\}$ where $p$ and $q$ are elements of
$\mathsf{View}_{\mathcal{M}}$ — with the usual rules for non-deterministic
choice, non-deterministic iteration, sequential composition, and parallel
composition, sound given the proof obligations just described above. It is
parameterized by a rule for atomic commands that requires a specification of
the triples for primitive operations, and their soundness (an obligation we
must prove). This can then be used to prove that every typing derivation
embeds to a valid derivation in the Views Logic, roughly
$\forall\Gamma,C,\Gamma^{\prime},\mathit{tid}\ldotp\Gamma\vdash
C\dashv\Gamma^{\prime}\Rightarrow\\{\llbracket\Gamma\rrbracket_{\mathit{tid}}\\}\llbracket
C\rrbracket_{\mathit{tid}}\\{\llbracket\Gamma^{\prime}\rrbracket_{\mathit{tid}}\\}$
once for the writer type system, once for the readers.

$\begin{array}[]{l}\downarrow{\mathsf{if}\;(x.f==y)\;C_{1}\;C_{2}}\downarrow\mathit{tid}\overset{\mathrm{def}}{=}z=x.f;((\mathsf{assume}(z=y);C_{1})+(\mathsf{assume}(z\neq
y);C_{2}))\end{array}$
$\llbracket\texttt{assume}(\mathcal{S})\rrbracket(s)\overset{\mathrm{def}}{=}\left\\{\begin{array}[]{ll}\\{s\\}&\textrm{if}~{}s\in\mathcal{S}\\\
\emptyset&\textrm{Otherwise}\end{array}\right.$
$\downarrow{\mathsf{while}\;(e)\;C}\downarrow\overset{\mathrm{def}}{=}\left(\mathsf{assume}(e);C\right)^{*};(\mathsf{assume}(\lnot
e));$ $\displaystyle\displaystyle{\hbox{\hskip
31.94461pt\vbox{\hbox{\hskip-31.9446pt\hbox{\hbox{$\displaystyle\displaystyle\\{P\\}\cap\\{\lceil\mathcal{S}\rceil\\}\sqsubseteq\\{Q\\}$}}}\vbox{}}}\over\hbox{\hskip
31.0946pt\vbox{\vbox{}\hbox{\hskip-31.09459pt\hbox{\hbox{$\displaystyle\displaystyle\\{P\\}\texttt{assume}\left(\mathcal{S}\right)\\{Q\\}$}}}}}}$
where  $\lceil\mathcal{S}\rceil=\\{m|\lfloor
m\rfloor\cap\mathcal{S}\neq\emptyset\\}$

Figure 12: Encoding branch conditions with assume(b)

There are two remaining subtleties to address. First, commands $C$ also
require translation: the Views Framework has only non-deterministic branches
and loops, so the standard versions from our core language must be encoded.
The approach to this is based on a standard idea in verification, which we
show here for conditionals as shown in Figure 12. $\textsf{assume}(b)$ is a
standard idea in verification semantics [4, 32], which “does nothing”
(freezes) if the condition $b$ is false, so its postcondition in the Views
logic can reflect the truth of $b$. assume in Figure 12 adapts this for the
Views Framework as in other Views-based proofs [16, 15], specifying sets of
machine states as a predicate. We write boolean expressions as shorthand for
the set of machine states making that expression true. With this setup done,
the top-level soundness claim then requires proving – once for the reader type
system, once for the writer type system – that every valid source typing
derivation corresponds to a valid derivation in the Views logic:
$\forall\Gamma,C,\Gamma^{\prime},\Gamma\vdash_{M}C\dashv\Gamma^{\prime}\Rightarrow\\{\llbracket\Gamma\rrbracket\\}\downarrow
C\downarrow\\{\llbracket\Gamma^{\prime}\rrbracket\\}$.

Second, we have not addressed a way to encode subtyping. One might hope this
corresponds to a kind of implication, and therefore subtyping corresponds to
consequence. Indeed, this is how we (and prior work [16, 15]) address
subtyping in a Views-based proof. Views defines the notion of _view shift_
222This is the same notion present in later program logics like Iris [20],
though more recent variants are more powerful. ($\sqsubseteq$) as a way to
reinterpret a set of instrumented states as a new (compatible) set of
instrumented states, offering a kind of logical consequence, used in a rule of
consequence in the Views logic:

$p\sqsubseteq q\stackrel{{\scriptstyle def}}{{=}}\forall
m\in\mathcal{M}\ldotp\lfloor p*\\{m\\}\rfloor\subseteq\lfloor
q*\mathcal{R}(\\{m\\})\rfloor$

We are now finally ready to prove the key lemmas of the soundness proof,
relating subtying to view shifts, proving soundness of the primitive actions,
and finally for the full type system. These proofs occur once for the writer
type system, and once for the reader; we show here only the (more complex)
writer obligations:

######  Lemma 2 (Axiom of Soundness for Atomic Commands)

For each axiom, $\Gamma_{1}\vdash_{\textsf{M}}\alpha\dashv\Gamma_{2}$, we show
$\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{tid}*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

By case analysis on $\alpha$. Details in Appendix A.1 of the techical report
[22].

######  Lemma 3 (Context-SubTyping-M)

$\Gamma\prec:\Gamma^{\prime}\implies\llbracket\Gamma\rrbracket_{M,tid}\sqsubseteq\llbracket\Gamma^{\prime}\rrbracket_{M,tid}$

###### Proof

Induction on the subtyping derivation, then inducting on the single-type
subtype relation for the first variable in the non-empty context case.

######  Lemma 4 (Views Embedding for Write-Side)

$\qquad\forall\Gamma,C,\Gamma^{\prime},\mathit{t}\ldotp\Gamma\vdash_{M}C\dashv\Gamma^{\prime}\Rightarrow\llbracket\Gamma\rrbracket_{\mathit{t}}\cap\llbracket{M}\rrbracket_{t}\vdash\llbracket
C\rrbracket_{\mathit{t}}\dashv\llbracket\Gamma^{\prime}\rrbracket_{\mathit{t}}\cap\llbracket{M}\rrbracket_{t}$

###### Proof

By induction on the typing derivation, appealing to Lemma 2 for primitives,
Lemma 3 and consequence for subtyping, and otherwise appealing to structural
rules of the Views logic and inductive hypotheses. Full details in Appendix
A.1 of the technical report [22].

The corresponding obligations and proofs for the read-side critical section
type system are similar in statement and proof approach, just for the read-
side type judgments and environment denotations.

##  7 Related Work

Our type system builds on a great deal of related work on RCU implementations
and models; and general concurrent program verification (via program logics,
model checking, and type systems).

Modeling RCU and Memory Models Alglave et al. [2] propose a memory model to be
assumed by the platform-independent parts of the Linux kernel, regardless of
the underlying hardware’s memory model. As part of this, they give the first
formalization of what it means for an RCU implementation to be correct
(previously this was difficult to state, as the guarantees in principle could
vary by underlying CPU architecture). Essentially, that reader critical
sections do not span grace periods. They prove by hand that the Linux kernel
RCU implementation [1] satisfies this property. According to the fundamental
requirements of RCU [28], our model in Section 3 can be considered as a valid
RCU implementation satisfying all requirements for an RCU
implementation(assuming sequential consistency) aside from one performance
optimization, Read-to-Write Upgrade, which is important in practice but not
memory-safety centric – see the technical report [22] for detailed discussion
on satisfying RCU requirements.

  * •

Grace-Period and Memory-Barrier Guarantee: To reclaim a heap location, a
mutator thread must synchronize with all of the reader threads with
overlapping read-side critical sections to guarantee that none of the updates
to the memory cause invalid memory accesses. The operational semantics enforce
a protocol on the mutator thread’s actions. First it unlinks a node from the
data structure; the local type for that reference becomes unlinked. Then it
waits for current reader threads to exit, after which the local type is
freeable. Finally, it may safely reclaim the memory, after which the local
type is undef. The semantics prevent the writer from reclaiming too soon by
adding the heap location to the free list of the state, which is checked
dynamically by the actual free operation. We discuss the grace period and
unlinking invariants in our system in Section 6.1.

  * •

Publish-Subscribe Guarantee: Fresh heap nodes cannot be observed by the reader
threads until they are published. As we see in the operational semantics, once
a new heap location is allocated it can only be referenced by a local variable
of type fresh. Once published, the local type for that reference becomes
rcuItr, indicating it is now safe for the reader thread to access it with
local references in rcuItr type. We discuss the related type assertions for
inserting/replacing(Figures 7(a)-7(b)) a fresh node in Section 4.3 and the
related invariants in Section 6.1.

  * •

RCU Primitives Guaranteed to Execute Unconditionally: Unconditional execution
of RCU Primitives are provided by the definitions in our operational semantics
for our RCU primitives(e.g. ReadBegin, ReadEnd, WriteBegin and WriteEnd) as
their executions do not consider failure/retry.

  * •

Guaranteed Read-to-Write Upgrade: This is a performance optimization which
allows the reader threads to upgrade the read-side critical section to the
write-critical section by acquiring the lock after a traversal for a data
element and ensures that the upgrading-reader thread exit the read-critical
section before calling RCU synchronization. This optimization also allows
sharing the traversal code between the critical sections. Read-to-Write is an
important optimization in practice but largely orthogonal to memory-safety.
Current version of our system provides a strict separation of traverse-and-
update and traverse-only intentions through the type system(e.g. different
iterator types and rules for the RCU Write/Read critical sections) and the
programming primitives. As a future work, we want to extend our system to
support this performance optimization.

To the best of our knowledge, ours is the first abstract _operational_ model
for a Linux kernel-style RCU implementation – others are implementation-
specific [24] or axiomatic like Alglave et al.’s.

Tassarotti et al. model a well-known way of implementing RCU synchronization
without hurting readers’ performance, Quiescent State Based Reclamation(QSBR)
[9] where synchronization between the writer thread and reader threads
provided via per-thread counters. Tassarotti et al. [35] uses a protocol based
program logic based on separation and ghost variables called GPS [37] to
verify a user-level implementation of RCU with a singly linked list client
under _release-acquire_ semantics, which is a weaker memory model than
sequential-consistency. They require release-writes and acquire-reads to the
QSRB counters for proper synchronization in between the mutator and the reader
threads. This protocol is exactly what we enforce over the logical
observations of the mutator thread: from unlinked to freeable. Tassarotti et
al.’s synchronization for linking/publishing new nodes occurs in a similar way
to ours, so we anticipate it would be possible to extend our type system in
the future for similar weak memory models.

Program Logics Fu et al. [14] extend Rely-Guarantee and Separation-Logic [38,
12, 11] with the past-tense temporal operator to eliminate the need for using
a history variable and lift the standard separation conjunction to assert over
on execution histories. Gotsman et al. [17] take assertions from temporal
logic to separation logic [38] to capture the essence of epoch-based memory
reclamation algorithms and have a simpler proof than what Fu et al. have [14]
for Michael’s non-blocking stack [31] implementation under a sequentially
consistent memory model.

Tassarotti et al. [35] use abstract-predicates – e.g. WriterSafe – that are
specialized to the singly-linked structure in their evaluation. This means
reusing their ideas for another structure, such as a binary search tree, would
require revising many of their invariants. By contrast, our types carry
similar information (our denotations are similar to their definitions), but
are reusable across at least singly-linked and tree data structures (Section
5). Their proofs of a linked list also require managing assertions about RCU
implementation resources, while these are effectively hidden in the type
denotations in our system. On the other hand, their proofs ensure full
functional correctness. Meyer and Wolff [30] make a compelling argument that
separating memory safety from correctness if profitable, and we provide such a
decoupled memory safety argument.

Realizing our RCU Model A direct implementation of our semantics would yield
unacceptable performance, since both entering (ReadBegin) and exiting
(ReadEnd) modify shared data structures for the bounding-threads and readers
sets. A slight variation on our semantics would use a bounding set that
tracked such a snapshot of counts, and a vector of per-thread counts in place
of the reader set. Blocking grace period completion until the snapshot was
strictly older than all current reader counts would be more clearly equivalent
to these implementations. Our current semantics are simpler than this
alternative, while also equivalent.

Model Checking Kokologiannakis et al. [19] use model-checking to test the core
of Tree RCU in Linux kernel. Liang et al. [23] use model-checking to verify
the _grace period_ guarantee of Tree RCU. Both focus on validating a
particular RCU implementation, whereas we focus on verifying memory safety of
clients independent of implementation. Desnoyers et al. [9] use the SPIN model
checker to verify a user-mode implementation of RCU and this requires manual
translation from C to SPIN modeling language. In addition to being
implementation-specific, they require test harness code, validating its
behavior rather than real client code.

Type Systems Howard et al. [18, 7] present a Haskell library called _Monadic
RP_ which provides types and relativistic programming constructs for
write/read critical sections which enforce correct usage of relativistic
programming pattern. They also have only checked a linked list. They claim
handling trees (look-up followed by update) as a future work [18]. Thus our
work is the first type system for ensuring correct use of RCU primitives that
is known to handle more complex structures than linked lists.

##  8 Conclusions

We presented the first type system that ensures code uses RCU memory
management safely, and which is significantly simpler than full-blown
verification logics. To this end, we gave the first general operational model
for RCU-based memory management. Based on our suitable abstractions for RCU in
the operational semantics we are the first showing that decoupling the memory-
safety proofs of RCU clients from the underlying reclamation model is
possible. Meyer et al. [30] took similar approach for decoupling the
correctness verification of the data structures from the underlying
reclamation model under the assumption of the memory-safety for the data
structures. We demonstrated the applicability/reusability of our types on two
examples: a linked-list based bag [27] and a binary search tree [3]. To our
best knowledge, we are the first presenting the memory-safety proof for a tree
client of RCU. We managed to prove type soundness by embedding the type system
into an abstract concurrent separation logic called the Views Framework [10]
and encode many RCU properties as either type-denotations or global invariants
over abstract RCU state. By doing this, we managed to discharge these
invariants once as a part of soundness proof and did not need to prove them
for each different client.

####

Acknowledgements. We are grateful to Matthew Parkinson for guidance and
productive discussions on the early phase of this project. We also thank to
Nik Sultana and Klaus V. Gleissenthall for their helpful comments and
suggestions for improving the paper.

## References

  * [1] Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013\. Proceedings. pp. 141–157 (2013). https://doi.org/10.1007/978-3-642-39799-8_9, http://dx.doi.org/10.1007/978-3-642-39799-8_9
  * [2] Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.: Frightening small children and disconcerting grown-ups: Concurrency in the linux kernel. In: Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems. pp. 405–418. ASPLOS ’18, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3173162.3177156, http://doi.acm.org/10.1145/3173162.3177156
  * [3] Arbel, M., Attiya, H.: Concurrent updates with rcu: Search tree as an example. In: Proceedings of the 2014 ACM Symposium on Principles of Distributed Computing. pp. 196–205. PODC ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2611462.2611471, http://doi.acm.org/10.1145/2611462.2611471
  * [4] Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects. pp. 364–387. FMCO’05, Springer-Verlag, Berlin, Heidelberg (2006). https://doi.org/10.1007/11804192_17, http://dx.doi.org/10.1007/11804192_17
  * [5] Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proceedings of the 22Nd Annual IEEE Symposium on Logic in Computer Science. pp. 366–378. LICS ’07, IEEE Computer Society, Washington, DC, USA (2007). https://doi.org/10.1109/LICS.2007.30, https://doi.org/10.1109/LICS.2007.30
  * [6] Clements, A.T., Kaashoek, M.F., Zeldovich, N.: Scalable address spaces using RCU balanced trees. In: Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012, London, UK, March 3-7, 2012. pp. 199–210 (2012). https://doi.org/10.1145/2150976.2150998, http://doi.acm.org/10.1145/2150976.2150998
  * [7] Cooper, T., Walpole, J.: Relativistic programming in haskell using types to enforce a critical section discipline (2015), http://web.cecs.pdx.edu/~walpole/papers/haskell2015.pdf
  * [8] Desnoyers, M., McKenney, P.E., Dagenais, M.R.: Multi-core systems modeling for formal verification of parallel algorithms. SIGOPS Oper. Syst. Rev. 47(2), 51–65 (Jul 2013). https://doi.org/10.1145/2506164.2506174, http://doi.acm.org/10.1145/2506164.2506174
  * [9] Desnoyers, M., McKenney, P.E., Stern, A., Walpole, J.: User-level implementations of read-copy update. IEEE Transactions on Parallel and Distributed Systems (2009), /static/publications/desnoyers-ieee-urcu-submitted.pdf
  * [10] Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013. pp. 287–300 (2013). https://doi.org/10.1145/2429069.2429104, http://doi.acm.org/10.1145/2429069.2429104
  * [11] Feng, X.: Local rely-guarantee reasoning. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 315–327. POPL ’09, ACM, New York, NY, USA (2009). https://doi.org/10.1145/1480881.1480922, http://doi.acm.org/10.1145/1480881.1480922
  * [12] Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: Proceedings of the 16th European Symposium on Programming. pp. 173–188. ESOP’07, Springer-Verlag, Berlin, Heidelberg (2007), http://dl.acm.org/citation.cfm?id=1762174.1762193
  * [13] Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y.: Reasoning about optimistic concurrency using a program logic for history. In: CONCUR. pp. 388–402. Springer (2010)
  * [14] Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y.: Reasoning about optimistic concurrency using a program logic for history. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory. pp. 388–402. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [15] Gordon, C.S., Ernst, M.D., Grossman, D., Parkinson, M.J.: Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement Types. ACM Transactions on Programming Languages and Systems (TOPLAS) 39(3) (May 2017). https://doi.org/10.1145/3064850, http://doi.acm.org/10.1145/3064850
  * [16] Gordon, C.S., Parkinson, M.J., Parsons, J., Bromfield, A., Duffy, J.: Uniqueness and Reference Immutability for Safe Parallelism. In: Proceedings of the 2012 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA’12). Tucson, AZ, USA (October 2012). https://doi.org/10.1145/2384616.2384619, http://dl.acm.org/citation.cfm?id=2384619
  * [17] Gotsman, A., Rinetzky, N., Yang, H.: Verifying concurrent memory reclamation algorithms with grace. In: Proceedings of the 22Nd European Conference on Programming Languages and Systems. pp. 249–269. ESOP’13, Springer-Verlag, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_15, http://dx.doi.org/10.1007/978-3-642-37036-6_15
  * [18] Howard, P.W., Walpole, J.: A relativistic enhancement to software transactional memory. In: Proceedings of the 3rd USENIX Conference on Hot Topic in Parallelism. pp. 15–15. HotPar’11, USENIX Association, Berkeley, CA, USA (2011), http://dl.acm.org/citation.cfm?id=2001252.2001267
  * [19] Kokologiannakis, M., Sagonas, K.: Stateless model checking of the linux kernel’s hierarchical read-copy-update (tree rcu). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. pp. 172–181. SPIN 2017, ACM, New York, NY, USA (2017). https://doi.org/10.1145/3092282.3092287, http://doi.acm.org/10.1145/3092282.3092287
  * [20] Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: European Symposium on Programming. pp. 696–723. Springer (2017)
  * [21] Kung, H.T., Lehman, P.L.: Concurrent manipulation of binary search trees. ACM Trans. Database Syst. 5(3), 354–382 (Sep 1980). https://doi.org/10.1145/320613.320619, http://doi.acm.org/10.1145/320613.320619
  * [22] Kuru, I., Gordon, C.S.: Safe deferred memory reclamation with types. CoRR abs/1811.11853 (2018), http://arxiv.org/abs/1811.11853
  * [23] Liang, L., McKenney, P.E., Kroening, D., Melham, T.: Verification of the tree-based hierarchical read-copy update in the linux kernel. CoRR abs/1610.03052 (2016), http://arxiv.org/abs/1610.03052
  * [24] Mandrykin, M.U., Khoroshilov, A.V.: Towards deductive verification of c programs with shared data. Program. Comput. Softw. 42(5), 324–332 (Sep 2016). https://doi.org/10.1134/S0361768816050054, http://dx.doi.org/10.1134/S0361768816050054
  * [25] Mckenney, P.E.: Exploiting Deferred Destruction: An Analysis of Read-copy-update Techniques in Operating System Kernels. Ph.D. thesis, Oregon Health & Science University (2004), aAI3139819
  * [26] McKenney, P.E.: N4037: Non-transactional implementation of atomic tree move (May 2014), http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4037.pdf
  * [27] McKenney, P.E.: Some examples of kernel-hacker informal correctness reasoning. Technical Report paulmck.2015.06.17a (2015), http://www2.rdrop.com/users/paulmck/techreports/IntroRCU.2015.06.17a.pdf
  * [28] Mckenney, P.E.: A tour through rcu’s requirements (2017), https://www.kernel.org/doc/Documentation/RCU/Design/Requirements/Requirements.html
  * [29] Mckenney, P.E., Appavoo, J., Kleen, A., Krieger, O., Krieger, O., Russell, R., Sarma, D., Soni, M.: Read-copy update. In: In Ottawa Linux Symposium. pp. 338–367 (2001)
  * [30] Meyer, R., Wolff, S.: Decoupling lock-free data structures from memory reclamation for static analysis. PACMPL 3(POPL), 58:1–58:31 (2019), https://dl.acm.org/citation.cfm?id=3290371
  * [31] Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst. 15(6), 491–504 (Jun 2004). https://doi.org/10.1109/TPDS.2004.8, http://dx.doi.org/10.1109/TPDS.2004.8
  * [32] Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583. pp. 41–62. VMCAI 2016, Springer-Verlag New York, Inc., New York, NY, USA (2016). https://doi.org/10.1007/978-3-662-49122-5_2, http://dx.doi.org/10.1007/978-3-662-49122-5_2
  * [33] Paul E. McKenney, Mathieu Desnoyers, L.J., Triplett, J.: The rcu-barrier menagerie (Nov 2016), https://lwn.net/Articles/573497/
  * [34] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55–74. LICS ’02, IEEE Computer Society, Washington, DC, USA (2002), http://dl.acm.org/citation.cfm?id=645683.664578
  * [35] Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 110–120. PLDI ’15, ACM, New York, NY, USA (2015). https://doi.org/10.1145/2737924.2737992, http://doi.acm.org/10.1145/2737924.2737992
  * [36] Triplett, J., McKenney, P.E., Walpole, J.: Resizable, scalable, concurrent hash tables via relativistic programming. In: Proceedings of the 2011 USENIX Conference on USENIX Annual Technical Conference. pp. 11–11. USENIXATC’11, USENIX Association, Berkeley, CA, USA (2011), http://dl.acm.org/citation.cfm?id=2002181.2002192
  * [37] Turon, A., Vafeiadis, V., Dreyer, D.: Gps: Navigating weak memory with ghosts, protocols, and separation. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications. pp. 691–707. OOPSLA ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2660193.2660243, http://doi.acm.org/10.1145/2660193.2660243
  * [38] Vafeiadis, V., Parkinson, M.: A Marriage of Rely/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V. (eds.) CONCUR 2007 – Concurrency Theory, Lecture Notes in Computer Science, vol. 4703, pp. 256–271. Springer Berlin / Heidelberg (2007), http://dx.doi.org/10.1007/978-3-540-74407-8_18, 10.1007/978-3-540-74407-8_18

##  Appendix 0.A Complete Soundness Proof of Atoms and Structural Program
Statements

###  0.A.1 Complete Constructions for Views

To prove soundness we use the Views Framework [10]. The Views Framework takes
a set of parameters satisfying some properties, and produces a soundness proof
for a static reasoning system for a larger programming language. Among other
parameters, the most notable are the choice of machine state, semantics for
_atomic_ actions (e.g., field writes, or WriteBegin), and proofs that the
reasoning (in our case, type rules) for the atomic actions are sound (in a way
chosen by the framework). The other critical pieces are a choice for a partial
_view_ of machine states — usually an extended machine state with meta-
information — and a relation constraining how other parts of the program can
interfere with a view (e.g., modifying a value in the heap, but not changing
its type). Our type system will be related to the views by giving a denotation
of type environments in terms of views, and then proving that for each atomic
action shown in 2 in Section 3 and type rule in Figures 6 Section 4.2 and 34
Appendix 0.E, given a view in the denotation of the initial type environment
of the rule, running the semantics for that action yields a local view in the
denotation of the output type environment of the rule. The following works
through this in more detail. We define logical states, LState to be

  * •

A machine state, $\sigma=(s,h,l,rt,R,B)$;

  * •

An observation map, O, of type $\textsf{Loc}\to\mathcal{P}(\textsf{obs})$

  * •

Undefined variable map, $U$, of type
$\mathcal{P}(\textsf{Var}\times\textsf{TID})$

  * •

Set of threads, $T$, of type $\mathcal{P}(\textsf{TIDS})$

  * •

A to-free map(or free list), $F$, of type
$\textsf{Loc}\rightharpoonup\mathcal{P}(\textsf{TID})$

The free map $F$ tracks which reader threads may hold references to each
location. It is not required for execution of code, and for validating an
implementation could be ignored, but we use it later with our type system to
help prove that memory deallocation is safe.

Each memory region can be observed in one of the following type states within
a snapshot taken at any time

$\textsf{obs}:=\texttt{iterator}\;\mathrm{tid}\mid\texttt{unlinked}\mid\texttt{fresh}\mid\texttt{freeable}\mid\texttt{root}$

We are interested in RCU typed of heap domain which we define as:

$\textsf{RCU}=\\{o\mid\textsf{ftype}(f)=\textsf{RCU}\land\exists
o^{\prime}\ldotp h(o^{\prime},f)=o\\}$

A thread’s (or scope’s) _view_ of memory is a subset of the
instrumented(logical states), which satisfy certain well-formedness criteria
relating the physical state and the additional meta-data ($O$, $U$, $T$ and
$F$)

$\mathcal{M}\stackrel{{\scriptstyle def}}{{=}}\\{m\in(\textsf{MState}\times
O\times U\times T\times F)\mid\textsf{WellFormed}(m)\\}$

We do our reasoning for soundness over instrumented states and define an
erasure relation

$\lfloor-\rfloor:\mathsf{MState}\implies\textsf{LState}$

that projects instrumented states to the common components with MState.

$\begin{array}[]{l@{\;\;=\;\;}l}\llbracket\,x:\textsf{rcuItr}\,\rho\,\mathcal{N}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{iterator}\,tid\in
O(s(x,tid)))\land(x\notin U)\\\ &\land(\forall_{f_{i}\in
dom(\mathcal{N})x_{i}\in
codom(\mathcal{N})}\ldotp\left\\{\begin{array}[]{l}s(x_{i},tid)=h(s(x,tid),f_{i})\\\
\land\textsf{iterator}\in O(s(x_{i},tid)))\end{array}\right.\\\
&\land(\forall_{\rho^{\prime},\rho^{\prime\prime}}\ldotp\rho^{\prime}.\rho^{\prime\prime}=\rho\implies\textsf{iterator}\,tid\in
O(h^{*}(rt,\rho^{\prime})))\\\ &\land h^{*}(rt,\rho)=s(x,tid)\land(l=tid\land
s(x,\\_)\notin dom(F)))\end{array}\right\\}\\\
\llbracket\,x:\textsf{rcuItr}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{iterator}\,tid\in
O(s(x,tid)))\land(x\notin U)\land\\\ &(tid\in
B)\implies\left\\{\begin{array}[]{l}(\exists_{T^{\prime}\subseteq
B}\ldotp\\{s(x,tid)\mapsto T^{\prime}\\}\cap F\neq\emptyset)\land\\\
\land(tid\in T^{\prime})\end{array}\right.\end{array}\right\\}\\\
\llbracket\,x:\textsf{unlinked}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{unlinked}\in
O(.s(x,tid))\land l=tid\land x\notin U)\land\\\ &(\exists_{T^{\prime}\subseteq
T}\ldotp s(x,tid)\mapsto T^{\prime}\in F\implies T^{\prime}\subseteq B\land
tid\notin T^{\prime})\end{array}\right\\}\\\
\llbracket\,x:\textsf{freeable}\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&\begin{array}[]{l}\textsf{freeable}\in
O(s(x,tid))\land l=tid\land x\notin U\land\\\
s(x,tid)\mapsto\\{\emptyset\\}\in F\end{array}\end{array}\right\\}\\\
\llbracket\,x:\textsf{rcuFresh}\,\mathcal{N}\,\,\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(\textsf{fresh}\in
O(s(x,tid))\land x\notin U\land s(x,tid)\notin dom(F))\\\ &(\forall_{f_{i}\in
dom(\mathcal{N}),x_{i}\in codom(\mathcal{N})}\ldotp
s(x_{i},tid)=h(s(x,tid),f_{i})\\\ &\land\textsf{iterator}\,tid\in
O(s(x_{i},tid))\land s(x_{i},tid)\notin dom(F))\end{array}\right\\}\\\
\llbracket
x:\textsf{undef}\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&(x,tid)\in
U\land s(x,tid)\notin dom(F)\end{array}\right\\}\\\
\llbracket\,x:\textsf{rcuRoot}\rrbracket_{tid}&\left\\{\begin{array}[]{l|l}m\in\mathcal{M}&\begin{array}[]{l}((rt\notin
U\land s(x,tid)=rt\land rt\in dom(h)\land\\\ O(rt)\in\textsf{root}\land
s(x,tid)\notin dom(F))\end{array}\end{array}\right\\}\end{array}$

$\textrm{provided}~{}h^{*}:(\textsf{Loc}\times\textsf{Path})\rightharpoonup\textsf{Val}$

Figure 13: Type Environments

Every type environment represents a set of possible views (well-formed logical
states) consistent with the types in the environment. We make this precise
with a denotation function

$\llbracket-\rrbracket\\_:\mathsf{TypeEnv}\rightarrow\mathsf{TID}\rightarrow\mathcal{P}(\mathcal{M})$

that yields the set of states corresponding to a given type environment. This
is defined in terms of denotation of individual variable assertions

$\llbracket-:-\rrbracket_{-}:\mathsf{Var}\rightarrow\mathsf{Type}\rightarrow\mathsf{TID}\rightarrow\mathcal{P}(\mathcal{M})$

The latter is given in Figure 13. To define the former, we first need to state
what it means to combine logical machine states.

Composition of instrumented states is an operation

$\bullet:\mathcal{M}\longrightarrow\mathcal{M}\longrightarrow\mathcal{M}$

that is commutative and associative, and defined component-wise in terms of
composing physical states, observation maps, undefined sets, and thread sets
as shown in Figure 2

$\bullet=(\bullet_{\sigma},\bullet_{O},\cup,\cup)$
$O_{1}\bullet_{O}O_{2}(loc)\overset{\mathrm{def}}{=}O_{1}(loc)\cup O_{2}(loc)$
$(s_{1}\bullet_{s}s_{2})\overset{\mathrm{def}}{=}s_{1}\cup s_{2}\texttt{ when
}dom(s_{1})\cap dom(s_{2})=\emptyset$

$(F_{1}\bullet_{F}F_{2})\overset{\mathrm{def}}{=}F_{1}\cup F_{2}\texttt{ when
}dom(F_{1})\cap dom(F_{2})=\emptyset$
$(h_{1}\bullet_{h}h_{2})(o,f)\overset{\mathrm{def}}{=}\left\\{\begin{array}[]{ll}\mathrm{undef}&\textrm{if}~{}h_{1}(o,f)=v\land
h_{2}(o,f)=v^{\prime}\land v^{\prime}\neq v\\\
v&\textrm{if}~{}h_{1}(o,f)=v\land h_{2}(o,f)=v\\\
v&\textrm{if}~{}h_{1}(o,f)=\mathrm{undef}\land h_{2}(o,f)=v\\\
v&\textrm{if}~{}h_{1}(o,f)=v\land h_{2}(o,f)=\mathrm{undef}\\\
\mathrm{undef}&\textrm{if}~{}h_{1}(o,f)=\mathrm{undef}\land
h_{2}(o,f)=\mathrm{undef}\end{array}\right.$
$\begin{array}[]{l}((s,h,l,rt,R,B),O,U,T,F)\mathcal{R}_{0}((s^{\prime},h^{\prime},l^{\prime},rt^{\prime},R^{\prime},B^{\prime}),O^{\prime},U^{\prime},T^{\prime},F^{\prime})\overset{\mathrm{def}}{=}\\\
\bigwedge\left\\{\begin{array}[]{l}l\in T\rightarrow(h=h^{\prime}\land
l=l^{\prime})\\\ l\in T\rightarrow F=F^{\prime}\\\ \forall
tid,o\ldotp\textsf{iterator}\,tid\in O(o)\rightarrow o\in dom(h)\\\ \forall
tid,o\ldotp\textsf{iterator}\,tid\in O(o)\rightarrow o\in dom(h^{\prime})\\\
\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in dom(h)\\\
\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h^{\prime})\\\ O=O^{\prime}\land U=U^{\prime}\land T=T^{\prime}\land
R=R^{\prime}\land rt=rt^{\prime}\\\ \forall x,t\in T\ldotp
s(x,t)=s^{\prime}(x,t)\end{array}\right\\}\end{array}$ An important property
of composition is that it preserves validity of logical states:

######  Lemma 5 (Well Formed Composition)

Any successful composition of two well-formed logical states is well-formed:

$\forall_{x,y,z}\ldotp\mathsf{WellFormed}(x)\implies\mathsf{WellFormed}(y)\implies
x\bullet y=z\implies\mathsf{WellFormed(z)}$

###### Proof

By assumption, we know that Wellformed(x) and Wellformed(y) hold. We need to
show that composition of two well-formed states preserves well-formedness
which is to show that for all $z$ such that $x\bullet y=z$, Wellformed(z)
holds. Both $x$ and $y$ have components
$((s_{x},h_{x},l_{x},rt_{x},R_{x},B_{x}),O_{x},U_{x},T_{x},F_{x})$ and
$((s_{y},h_{y},l_{y},rt_{y},R_{y},B_{y}),O_{y},U_{y},T_{y},F_{y})$,
respectively. $\bullet_{s}$ operator over stacks $s_{x}$ and $s_{y}$ enforces
$dom(s_{x})\cap dom(s_{y})=\emptyset$ which enables to make sure that
wellformed mappings in $s_{x}$ does not violate wellformed mappings in $s_{y}$
when we union these mappings for $s_{z}$. Same argument applies for
$\bullet_{F}$ operator over $F_{x}$ and $F_{y}$. Disjoint unions of wellformed
$R_{x}$ with wellformed $R_{y}$ and wellformed $B_{x}$ with wellformed $B_{y}$
preserves wellformedness in composition as it is disjoint union of different
wellformed elements of sets. Wellformed unions of $O_{x}$ with $O_{y}$,
$U_{x}$ with $U_{y}$ and $T_{x}$ with $T_{y}$ preserve wellformedness. When we
compose $h_{x}(s(x,tid),f)$ and $h_{y}(s(x,l),f)$, it is easy to show that we
preserve wellformedness if both threads agree on the heap location. Otherwise,
if the heap location is undefined for one thread but a value for the other
thread then composition considers the value. If a heap location is undefined
for both threads then this heap location is also undefined for the location.
All the cases for heap composition still preserves the wellformedness from the
assumption that $x$ and $y$ are wellformed.

We define separation on elements of type contexts

  * •

For read-side as $\llbracket x_{1}:T_{1},\ldots
x_{n}:T_{n}\rrbracket_{tid,\textsf{R}}=\llbracket
x_{1}:T_{1}\rrbracket_{tid}\cap\ldots\cap\llbracket
x_{n}:T_{n}\rrbracket_{tid}\cap\llbracket\textsf{R}\rrbracket_{tid}$ where
$\llbracket\textsf{R}\rrbracket_{tid}=\\{(s,h,l,rt,R,B),O,U,T,F\mid tid\in
R\\}$

  * •

For write-side as $\llbracket x_{1}:T_{1},\ldots
x_{n}:T_{n}\rrbracket_{tid,\textsf{M}}=\llbracket
x_{1}:T_{1}\rrbracket_{tid}\cap\ldots\cap\llbracket
x_{n}:T_{n}\rrbracket_{tid}\cap\llbracket\textsf{M}\rrbracket_{tid}$ where
$\llbracket\textsf{M}\rrbracket_{tid}=\\{(s,h,l,rt,R,B),O,U,T,F\mid tid=l\\}$

  * •

$\llbracket x_{1}:T_{1},\ldots
x_{n}:T_{n}\rrbracket_{tid,\textsf{O}}=\llbracket
x_{1}:T_{1}\rrbracket_{tid}\cap\ldots\cap\llbracket
x_{n}:T_{n}\rrbracket_{tid}\cap\llbracket\textsf{O}\rrbracket_{tid}$ where
$\llbracket\textsf{O}\rrbracket_{tid}=\\{(s,h,l,rt,R,B),O,U,T,F\mid tid\neq
l\land tid\notin R\\}$.

Partial separating conjunction then simply requires the existence of two
states that compose:

$m\in P\ast Q\stackrel{{\scriptstyle def}}{{=}}\exists m^{\prime}\ldotp\exists
m^{\prime\prime}\ldotp m^{\prime}\in P\land m^{\prime\prime}\in Q\land m\in
m^{\prime}\bullet m^{\prime\prime}$

Different threads’ views of the state may overlap (e.g., on shared heap
locations, or the reader thread set), but one thread may modify that shared
state. The Views Framework restricts its reasoning to subsets of the logical
views that are _stable_ with respect to expected interference from other
threads or contexts. We define the interference as (the transitive reflexive
closure of) a binary relation $\mathcal{R}$ on $\mathcal{M}$, and a View in
the formal framework is then:

$\textsf{View}_{\mathcal{M}}\stackrel{{\scriptstyle
def}}{{=}}\\{M\in\mathcal{P}(\mathcal{M})|\mathcal{R}(M)\subseteq M\\}$

Thread interference relation

$\mathcal{R}\subseteq\mathcal{M}\times\mathcal{M}$

defines permissible interference on an instrumented state. The relation must
distribute over composition:

$\forall m_{1},m_{2},m\ldotp(m_{1}\bullet
m_{2})\mathcal{R}m\Longrightarrow\begin{array}[]{ll}\exists
m^{\prime}_{1}m^{\prime}_{2}\ldotp m_{1}\mathcal{R}m^{\prime}_{1}\land
m_{2}\mathcal{R}m^{\prime}_{2}\land m\in m^{\prime}_{1}\bullet
m^{\prime}_{2}\end{array}$

where $\mathcal{R}$ is transitive-reflexive closure of $\mathcal{R}_{0}$ shown
at Figure 2. $\mathcal{R}_{0}$ (and therefore $\mathcal{R}$) also “preserves”
validity:

######  Lemma 6 (Valid $\mathcal{R}_{0}$ Interference)

For any $m$ and $m^{\prime}$, if $\mathsf{WellFormed}(m)$ and
$m\mathcal{R}_{0}m^{\prime}$, then $\mathsf{WellFormed}(m^{\prime})$.

###### Proof

By assumption, we know that $m=(s,h,l,rt,R,B),O,U,T,F)$ is wellformed. We also
know that
$m^{\prime}=(s^{\prime},h^{\prime},l^{\prime},rt^{\prime},R^{\prime},B^{\prime}),O^{\prime},U^{\prime},T^{\prime},F^{\prime})$
is related to $m$ via $R_{0}$. By assumptions in $R_{0}$ and semantics, we
know that $O$,$R$,$T$ and $U$ which means that these components do not have
any effect on wellformedness of the $m$. In addition, change on stack, $s$,
does not affect the wellformedness as

$\forall x,t\in T\ldotp s(x,t)=s^{\prime}(x,t)$

Moreover, from semantics we know that $l$ and $h$ can only be changed by
writer thread and from $R_{0}$

$l\in T\rightarrow(h=h^{\prime}\land l=l^{\prime})$ $l\in T\rightarrow
F=F^{\prime}$

and by assumptions from the lemma($\mathsf{WellFormed}(m)$.RINFL) we can
conclude that $F$,$l$ and $h$ do not have effect on wellformedness of the $m$.

######  Lemma 7 (Stable Environment Denotation-M)

For any _closed_ environment $\Gamma$ (i.e., $\forall
x\in\mathsf{dom}(\Gamma)\ldotp,\mathsf{FV}(\Gamma(x))\subseteq\mathsf{dom}(\Gamma)$):

$\mathcal{R}(\llbracket\Gamma\rrbracket_{\mathsf{M},tid})\subseteq\llbracket\Gamma\rrbracket_{\mathsf{M},tid}$

Alternatively, we say that environment denotation is _stable_ (closed under
$\mathcal{R}$).

###### Proof

By induction on the structure of $\Gamma$. The empty case holds trivially. In
the other case where $\Gamma=\Gamma^{\prime},x:T$, we have by the inductive
hypothesis that

$\llbracket\Gamma^{\prime}\rrbracket_{\mathsf{M},tid}$

is stable, and must show that

$\llbracket\Gamma^{\prime}\rrbracket_{\mathsf{M},tid}\cap\llbracket{x:\tau}\rrbracket_{tid}$

is as well. This latter case proceeds by case analysis on $T$.

We know that $O$, $U$, $T$, $R$, $s$ and $rt$ are preserved by $R_{0}$. By
unfolding the type environment in the assumption we know that $tid=l$. So we
can derive conclusion for preservation of $F$ and $h$ and $l$ by

$l\in T\rightarrow(h=h^{\prime}\land l=l^{\prime})$ $l\in T\rightarrow
F=F^{\prime}$

Cases in which denotations, $\llbracket x:T\rrbracket$, touching these _R 0
preserved_ maps are trivial to show.

###### Case 1

\- unlinked, undef, $\textsf{rcuFresh}\,\mathcal{N}$ and freeable trivial.

###### Case 2

\- $\textsf{rcuItr}\,\rho\,\mathcal{N}$: All the facts we know so far from
$R_{0}$, $tid=l$ and additional fact we know from $R_{0}$:

$\forall tid,o\ldotp\textsf{iterator}\,tid\in O(o)\rightarrow o\in dom(h)$
$\forall tid,o\ldotp\textsf{iterator}\,tid\in O(o)\rightarrow o\in
dom(h^{\prime})$

prove this case.

###### Case 3

\- root: All the facts we know so far from $R_{0}$, $tid=l$ and additional
fact we know from $R_{0}$:

$\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in dom(h)$
$\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h^{\prime})$

prove this case.

######  Lemma 8 (Stable Environment Denotation-R)

For any _closed_ environment $\Gamma$ (i.e., $\forall
x\in\mathsf{dom}(\Gamma)\ldotp,\mathsf{FV}(\Gamma(x))\subseteq\mathsf{dom}(\Gamma)$):

$\mathcal{R}(\llbracket\Gamma\rrbracket_{\mathsf{R},tid})\subseteq\llbracket\Gamma\rrbracket_{\mathsf{R},tid}$

Alternatively, we say that environment denotation is _stable_ (closed under
$\mathcal{R}$).

###### Proof

Proof is similar to one for Lemma 7 where there is only one simple case,
$\llbracket x:\textsf{rcuItr}\rrbracket$.

The Views Framework defines a program logic (Hoare logic) with judgments of
the form $\\{p\\}C\\{q\\}$ for views p and q and commands $C$. Commands
include atomic actions, and soundness of such judgments for atomic actions is
a parameter to the framework. The framework itself provides for soundness of
rules for sequencing, fork-join parallelism, and other general rules. To prove
type soundness for our system, we define a denotation of _type judgments_ in
terms of the Views logic, and show that every valid typing derivation
translates to a valid derivation in the Views logic:

$\forall\Gamma,C,\Gamma^{\prime},\mathit{tid}\ldotp\Gamma\vdash_{M,R}C\dashv\Gamma^{\prime}\Rightarrow\\{\llbracket\Gamma\rrbracket_{\mathit{tid}}\\}\llbracket
C\rrbracket_{\mathit{tid}}\\{\llbracket\Gamma^{\prime}\rrbracket_{\mathit{tid}}\\}$

The antecedent of the implication is a type judgment(shown in Figure 6 Section
4.3, Figure 4 Section 4.1 and Figure 34 Appendix 0.E) and the conclusion is a
judgment in the Views logic. The environments are translated to views
($\mathsf{View}_{\mathcal{M}}$) as previously described. Commands $C$ also
require translation, because the Views logic is defined for a language with
non-deterministic branches and loops, so the standard versions from our core
language must be encoded. The approach to this is based on a standard idea in
verification, which we show here for conditionals as shown in Figure 15.
$\textsf{assume}(b)$ is a standard construct in verification semantics [4]
[32], which “does nothing” (freezes) if the condition $b$ is false, so its
postcondition in the Views logic can reflect the truth of $b$. This is also
the approach used in previous applications of the Views Framework [16, 15].

$\begin{array}[]{l}\llbracket{\mathsf{if}\;(x.f==y)\;C_{1}\;C_{2}}\rrbracket_{\mathit{tid}}\overset{\mathrm{def}}{=}z=x.f;((\mathsf{assume}(z=y);C_{1})+(\mathsf{assume}(z\neq
y);C_{2}))\end{array}$