Safe Deferred Memory Reclamation with Types

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

RCU Types. There are six types used in Write critical sectionsrcuItr 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 [20] Appendix E.

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.

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 Fig. 3.

Figure 3 includes four judgments for subtyping. The first two—\(\vdash \mathcal {N}\prec :\mathcal {N}'\) and \(\vdash \rho \prec :\rho '\)—describe relaxations of field maps and paths respectively. \(\vdash \mathcal {N}\prec :\mathcal {N}'\) is read as “the field map \(\mathcal {N}\) is more precise than \(\mathcal {N}'\)” and similarly for paths. The third judgment \(\vdash T\prec :T'\) 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 \varGamma \prec :\varGamma '\) extends subtyping to all assumptions in a type context.

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 Fig. 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 Fig. 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 Fig. 1 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 Fig. 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.

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 (Fig. 4) to refine imprecise paths and field maps. In Fig. 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.

The system has three forms of typing judgement: \(\varGamma \vdash C\) for standard typing outside RCU critical sections; \(\varGamma \vdash _R C \dashv \varGamma '\) for reader critical sections, and \(\varGamma \vdash _M C \dashv \varGamma '\) 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 [25] from Fig. 1, highlighting how the type rules handle different parts of the code. Figure 1 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 Fig. 1 begins by reading the root into a new rcuItr reference used to begin traversing the structure. After each initial read (line 12 of and line 4 of ), 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 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, after 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 in Fig. 1 unlinks a node. The type annotations show that before that line 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 , and 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 initiate a grace period and wait for its completion. At the type level, this is reflected by the change of 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 , which further changes the type of to undef reflecting that 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 remain reachable: note the field maps of and nw in lines 30–31 are equal (trivially, though in general the field need not be null).

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

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 \(\varGamma \). 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 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 \(\varGamma \) are invalidated. This could happen one of two ways: either a field map in \(\varGamma \) for an alias of x duplicates the assumption that \(x.f_1==z\) (which is changed by this write), or \(\varGamma \) 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 \(\varGamma \), 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.

Replacing with a Fresh Node. Replacing with a rcuFresh reference faces the same aliasing complications as direct unlinking. We illustrate these challenges in Figs. 7a and b. Our technical report [20] 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) with \(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 (Fig. 7a) 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 dots—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 Fig. 7a to 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\ne 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}'\) 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 Fig. 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 [20].

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 Fig. 6 ensures unlinked references have been freed by forbidding them in the critical section’s post-type environment. Our technical report [20] 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.

This section provides more details on how the Views Framework [9] 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 Sect. 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:

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.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 (Fig. 9) 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 [20].

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, , 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, 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, , 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.

Type Environments. Assertions in the Views logic are (almost) sets of the logical states that satisfy a validity predicate WellFormed, outlined above: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 functionthat yields the set of states corresponding to a given type environment. This is defined as the intersection of individual variables’ types as in Fig. 9.

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: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 10 defines our composition operator and the core interference relation \(\mathcal {R}_0\)—the actual interference 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).

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: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:Additionally, interference must distribute over composition:

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:

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 can state the connection between the Views Framework logic induced by earlier parameters, and the type system from Sect. 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 once for the writer type system, once for the readers.

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 Fig. 11. \(\textsf {assume}(b)\) is a standard idea in verification semantics [4, 30], 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 Fig. 11 adapts this for the Views Framework as in other Views-based proofs [13, 14], 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: .

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 [13, 14]) address subtyping in a Views-based proof. Views defines the notion of view shift² (\(\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: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:

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.