Hoang-Hai Dang
email: haidang@mpi-sws.org

Jacques-Henri Jourdan
email: jacques-henri.jourdan@lri.fr

Jacques-Henri Jourdan

Jan-Oliver Kaiser

Derek Dreyer Rustbelt

Jacques- Henri Jourdan

Oliver Kaiser

Derek Dreyer
email: dreyer@mpi-sws.org.

RustBelt Meets Relaxed Memory

Keywords: CCS Concepts:, Theory of computation → Separation logic, Operational semantics, Programming logic Rust, semantic soundness, relaxed memory models, Iris

The Rust programming language supports safe systems programming by means of a strong ownership-tracking type system. In their prior work on RustBelt, Jung et al. began the task of setting Rust's safety claims on a more rigorous formal foundation. Specifically, they used Iris, a Coq-based separation logic framework, to build a machine-checked proof of semantic soundness for a λ-calculus model of Rust, as well as for a number of widely-used Rust libraries that internally employ unsafe language features. However, they also made the significant simplifying assumption that the language is sequentially consistent. In this paper, we adapt RustBelt to account for the relaxed-memory operations that concurrent Rust libraries actually use, in the process uncovering a data race in the Arc library. We focus on the most interesting technical problem: how to reason about resource reclamation under relaxed memory, using a logical construction we call synchronized ghost state.

INTRODUCTION

Rust [START_REF] Klabnik | The Rust Programming Language[END_REF] is a young and evolving programming language-sponsored by Mozilla and developed actively over the past decade by a diverse community of contributors-that aims to bring safety to the world of systems programming. Specifically, Rust provides low-level control over data layout and resource management à la modern C++, while at the same time offering strong high-level guarantees (such as type and memory safety) that are traditionally associated with safe languages like Java. In fact, Rust takes a step further, statically preventing more insidious forms of anomalous behavior, such as data races and iterator invalidation, that safe languages typically fail to rule out. Rust strikes its delicate balance between safety and control using a substructural type system, in which types not only classify data but also represent ownership of resources, such as the right to read, write, or reclaim a piece of memory. By tracking ownership in the types, Rust is able to prohibit dangerous combinations of mutation and aliasing, a well-known source of programming pitfalls and security vulnerabilities in C/C++ and Java.

Only recently has Rust begun to receive attention from the programming languages research community. Notably, the RustBelt project [START_REF] Dreyer | RustBelt project webpage[END_REF]] has sought to set the safety claims of Rust on a more rigorous formal foundation. The initial work on RustBelt by Jung et al. [2018a] made two main contributions. First, Jung et al. proposed a formal definition of a core typed calculus called λ Rust , which encapsulates the central features of the Rust language. Second, they used the Coq proof assistant to verify formally that Rust's aforementioned safety guarantees do in fact hold, both for the core λ Rust calculus and for a number of widely-used Rust libraries.

However, the initial work on RustBelt also made a significant simplifying assumption: it assumed a sequentially consistent (SC) model for concurrent memory accesses. On the one hand, sequential consistency [START_REF] Lamport | How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs[END_REF]]-i.e., an interleaving semantics in which threads take turns accessing the global state, and all threads share the same view of that state-has long been the standard memory model assumed by research on concurrency verification. On the other hand, this assumption does not match the reality of modern multicore programming languages, Rust included.

In reality, following C/C++11 (hereafter, C11), Rust provides a relaxed memory model (hereafter, RMM), supporting a variety of different consistency levels for shared-memory accesses [START_REF] Batty | Mathematizing C++ Concurrency[END_REF]. For programmers who demand strong synchronization, SC accesses are available, but this strength comes at the cost of disabling standard compiler optimizations and inserting expensive memory fences into the compiled code. The weaker consistency levels of release/acquire and relaxed allow one to trade off synchronization strength in return for more efficient compiled code. Rust employs a variety of these different consistency levels in several of its widely-used concurrency libraries, such as Arc, Mutex, and RwLock. But in the initial RustBelt verification effort, all atomic (i.e., potentially racy) memory accesses were treated as having the strongest consistency level, SC.

In this paper, we present RustBelt Relaxed (or RB rlx , for short), the first formal validation of the soundness of Rust under relaxed memory. Although based closely on the original RustBelt, RB rlx takes a significant step forward by accounting for the safety of the more weakly consistent memory operations that real concurrent Rust libraries actually use. For the most part, we were able to verify Rust's uses of relaxed-memory operations as is. Only in the implementation of one Rust library (Arc) did we need to strengthen the consistency level of two memory reads (from relaxed to acquire) in order to make our verification go through. And in one of these cases, our attempt to verify the original (more relaxed) access led us to expose it as the source of a previously undetected data race in the library. Our fix for this race has since been merged into the Rust codebase [START_REF] Jourdan | Insufficient synchronization in Arc::get_mut[END_REF]].

Relaxing RustBelt: Overview and Key Challenge

The overarching challenge in developing RB rlx is that the logical foundation on which the original RustBelt is built is unsound for relaxed memory. To understand why, let us first review a bit about Rust and the structure of the RustBelt verification.

Background on Rust and RustBelt. At the heart of Rust is an ownership-based type system, which rules out bad combinations of mutation and aliasing, yet is expressive enough to typecheck many common systems programming idioms. Nonetheless, certain kinds of functionality (e.g., some pointer-based data structures, synchronization abstractions, garbage collection mechanisms) cannot be implemented within the strictures of Rust's type system. Rust provides these abstractions instead via libraries whose implementations internally utilize unsafe features (e.g., unchecked type casts, array accesses without bounds checks, or accesses of "raw" pointers whose aliasing is untracked by the type system). These libraries are claimed to be safe extensions to Rust because they encapsulate their uses of unsafe features in "safe APIs". However, given that the set of such extensions is far from fixed-new and surprising "safe APIs" are being developed all the time-there is a pressing need to understand what property an internally-unsafe library ought to satisfy to be deemed a safe extension to Rust.

To formalize Rust's "extensible" notion of safety, RustBelt follows prior work on Foundational Proof-Carrying Code [START_REF] Ahmed | Semantic foundations for typed assembly languages[END_REF]] by employing a semantic soundness proof. First, it defines a semantic model of Rust types: a mapping from types T to logical predicates on terms Φ(e), which asserts what it means for the term e to behave safely at type T (even if internally e uses unsafe features). Then, the RustBelt proof breaks into two main parts:

(1) Safety of libraries that use unsafe features: For any library that makes use of unsafe features, the implementation of the library is proven to satisfy the semantic model of its API, thus establishing that it is safe for clients to make use of the library. RustBelt proved safety for a number of widely-used Rust libraries, including Arc, Rc, Cell, RefCell, Mutex, and RwLock.

(2) Safety of the λ Rust type system: The syntactic typing rules of λ Rust are proven to respect the semantic model, thus establishing that code written in the "safe" fragment of Rust is in fact observably safe-i.e., its behavior is well-defined. Put together, these imply that if a program P is well-typed, and its only uses of unsafe features appear within the libraries that have been verified safe (in part 1), then P is observably safe.

In carrying out their semantic soundness proof for RustBelt, Jung et al. relied on separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]]. Separation logic is a good fit for modeling Rust because it is designed around the same notion of ownership as Rust's type system, and thus provides built-in support for ownershipbased reasoning. More specifically, RustBelt was formalized in a higher-order concurrent separation logic framework called Iris [Jung et al. 2018b]. One benefit of using Iris is that it was designed to support the derivation of new separation logics with domain-specific reasoning principles. Jung et al. exploited this facility to derive a new logic called the lifetime logic, which they used extensively in their proofs in order to reason about Rust's "lifetimes" and "borrowing" mechanisms at a higher level of abstraction [Klabnik and Nichols 2018, §4.2, §10.3]. A second benefit of using Iris is that it comes with tactical support for developing machine-checked proofs interactively in Coq [START_REF] Krebbers | Interactive Proofs in Higher-Order Concurrent Separation Logic[END_REF]; this support made it possible for RustBelt to be fully mechanized in Coq.

Separation logic for relaxed memory. So why do we say that the logical foundation of RustBelt is unsound for relaxed memory? The reason is as follows. The Iris framework (on which RustBelt is built) is parameterized by an operational semantics for the language under consideration, and depending on how this parameter is instantiated, Iris can be used to derive proof rules of varying strength. In the case of RustBelt, Iris was instantiated with a sequentially consistent (SC) semantics for λ Rust . This SC instantiation of Iris (call it "Iris-SC") provides a variety of proof rules that are valid only under SC semantics and not under relaxed-memory semantics. In particular, Iris-SC enables one to establish general invariants governing arbitrary regions of shared memory. Unfortunately, under relaxed memory, different threads can observe writes to different locations in different orders, so one cannot in general maintain an invariant on multiple locations simultaneously.

To adapt RustBelt to relaxed memory, we must therefore rebuild it using a logic that is suitably restricted so as to be sound under relaxed memory, yet still supports machine-checked proofs as Iris does. A promising path forward was charted by [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF], who showed how Iris could be used to derive a relaxed-memory separation logic called iGPS, targeting RA+NA (the fragment of C11 comprising release/acquire and non-atomic accesses). Following prior work on relaxed-memory separation logics [START_REF] Vafeaidis | Relaxed Separation Logic: A Program Logic for C11 Concurrency[END_REF][START_REF] Turon | GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation[END_REF], iGPS accounts for weak memory consistency by weakening the power of invariants: the user of iGPS may only establish single-location invariants (i.e., invariants that govern a single shared memory location), the soundness of which is guaranteed by the coherence (or "SC per location") property of C11.

In this paper, drawing inspiration from FSL [Doko andVafeiadis 2016, 2017], we will extend iGPS further to account for the additional features of the C11 memory model that Rust libraries make use of-specifically, relaxed accesses and release/acquire fences. We call this extended logic iRC11.

To a first approximation, we would therefore like to "port" RustBelt so that it is built on top of iRC11 rather than Iris-SC. Following the structure of RustBelt, this porting effort breaks down into two major tasks:

SC-CInv-Acc {I * P } e {v. I * Q } atomic(e) τ I ⊢ { [τ ] q * P } e { v. [τ ] q * Q } SC-CInv-Tok [τ ] q+q ′ ⇔ [τ ] q * [τ ] q ′ SC-CInv-Cancel τ I ⊢ [τ ] 1 I
Fig. 1. Key rules for cancellable invariants in Iris-SC.

Task 1: Re-prove the safety of the Rust libraries considered by RustBelt, this time verifying their real, relaxed-memory implementations in iRC11. Task 2: Re-prove the safety of the λ Rust type system, this time relying only on proof rules that are sound in iRC11.

Key challenge. As it turns out, both of these tasks require us to overcome a technical challenge that is relevant not just to Rust but to relaxed-memory verification in general: namely, that existing work on separation logic does not provide an adequate foundation for reasoning about resource reclamation under relaxed memory. We will first explain this challenge in the context of Task 1, before briefly describing how it also informs Task 2.

Task 1: Re-prove the safety of Rust libraries under relaxed memory. One of the main motivations for using a "systems programming" language like Rust or C/C++ (as opposed to a garbage-collected language like Java) is to have more precise control over limited resources such as memory. In particular, the Rust programmer can be assured that when an object goes out of scope, the destructor (drop method) associated with its type will be invoked and any resources it owns will be reclaimed. Yet the safety of destructors is often quite subtle because objects can contain references to resources that are shared with other objects. For example, objects of type Arc<T> are simply aliases to a shared struct containing an object of type T along with a reference counter, which keeps track of the current number of active aliases to the object. Consequently, the destructor for Arc<T> cannot simply reclaim the shared struct that it points to: rather, it decrements the shared reference counter, and only if it observes that it was the last remaining alias can it safely reclaim the memory for the reference counter and invoke the destructor for the object of type T.

RustBelt showed how to put this subtle kind of resource reclamation on a sound formal footing using Iris-SC's mechanism of cancellable invariants (Fig. 1), a generalization of [START_REF] Gotsman | Local Reasoning for Storable Locks and Threads[END_REF] and [START_REF] Hobor | Oracle Semantics for Concurrent Separation Logic[END_REF]'s storable locks. A cancellable invariant τ I is an invariant governing a shared resource (described by proposition I ) which is only "active" for a certain period of time, after which point it is "cancelled". To access the shared resource during an atomic step of computation (SC-CInv-Acc), a thread must prove that the invariant is still active by exhibiting ownership of an invariant token [τ ] q , where q is a fraction in (0,1]. This is an instance of the well-known concept of fractional permissions [START_REF] Boyland | Checking interference with fractional permissions[END_REF]], and correspondingly, ownership of invariant tokens can be split or combined through fractional arithmetic (SC-CInv-Tok). If a thread π can assert ownership of [τ ] 1 (i.e., the "full" τ token), it knows that no other thread can assert that the invariant is active; thus it is safe for π to cancel the invariant and reclaim full ownership of I (SC-CInv-Cancel), after which it can free the memory governed by I if it wants to. In RustBelt, cancellable invariants played a crucial role in verifying the safety of destructors such as Arc's.

However, adapting cancellable invariants to the relaxed-memory setting turns out to be quite tricky-tricky enough that no existing relaxed-memory separation logic supports them. 1 Even if, following iGPS and its predecessors, we restrict invariants to govern a single location, a problem arises in how to model the cancellable invariant tokens. Under SC, one can simply model invariant tokens as a form of ghost state, i.e., purely logical state that is manipulated by the proof but does not appear in the physical program. But in existing relaxed-memory separation logics, ghost state is unsynchronized, meaning that ownership of it can be transferred between threads without the need for any physical synchronization. On the one hand (see §3.3), unsynchronized ghost state is indispensable for representing globally consistent state, such as (in the case of Arc) the number of Arc aliases currently in existence. On the other hand (see §4.1), if invariant tokens are modeled naively as unsynchronized ghost state, the logic of cancellable invariants becomes unsound! Our solution is to instead model invariant tokens using a novel notion of synchronized ghost state: ghost state that implicitly tracks the subjective view of the thread that owns it, and that therefore can only be transferred between threads using physical synchronization. Using synchronized ghost state, iRC11 offers the first general account of resource reclamation in relaxed-memory separation logic. We demonstrate its effectiveness on a number of real Rust libraries.

Task 2: Re-prove the safety of the λ Rust type system under relaxed memory. In contrast to RustBelt's proofs of safety for libraries, its proof of safety for the λ Rust type system did not rely directly on cancellable invariants or any other SC-specific features of Iris-SC. Rather, as mentioned above, the safety proof for the type system made essential use of a Rust-oriented logic called the lifetime logic, which was a domain-specific logic derived within Iris-SC. Thus, if we are able to show that the lifetime logic remains sound under relaxed memory-by instead deriving its soundness in iRC11then RB rlx can inherit RustBelt's safety proof for the λ Rust type system without modification! Synchronized ghost state is the key to making this modular porting strategy possible. Specifically, the lifetime logic is centered around a mechanism called borrow propositions, describing resources that are borrowed for the duration of a Rust "lifetime" and that can be reclaimed once the lifetime is over. Borrow propositions are similar in many ways to cancellable invariants, but also more flexible and more complex in terms of the protocols they support for sharing and reclamation of resources. Just as synchronized ghost state enables us to adapt cancellable invariants to relaxed memory, it plays an analogously central role in adapting borrow propositions to relaxed memory as well.

Contributions

In this paper, we present RB rlx , an adaptation of RustBelt to a relaxed memory model (or RMM), which (like its predecessor) is mechanized in Coq. The adaptation involves many components whose full technical explanation is beyond the scope of this paper. Instead, we focus on the key points of difference between RustBelt and RB rlx , and on the key technical innovations that make the adaptation feasible, most importantly our development of synchronized ghost state.

In summary, our contributions are as follows:

• We define ORC11, a new operational-semantics-based characterization of a large fragment of C11, including release/acquire/relaxed/non-atomic accesses and release/acquire fences.2 Developing such an operational semantics for C11 is a necessary prerequisite for instantiating the Iris framework. Since the C11 model is known to be flawed [START_REF] Boehm | Outlawing ghosts: Avoiding out-of-thin-air results[END_REF], we instead design ORC11 to match the semantics of RC11 (Repaired C11) [START_REF] Lahav | Repairing sequential consistency in C/C++11[END_REF], and in the appendix [START_REF] Dang | Appendix and Coq development accompanying this paper[END_REF] we sketch a proof of correspondence between them. • We develop iRC11, a logic for ORC11 derived within Iris, which combines elements of iGPS and FSL, and moreover supports resource reclamation via cancellable invariants in a manner that is sound for relaxed memory. The soundness of iRC11 relies crucially on our novel construction of synchronized ghost state. • We use iRC11 to port RustBelt from SC to relaxed memory. In particular, the major components that required re-verification were the library proofs (since we are now verifying implementations with relaxed-memory operations in them) and the proof of soundness of RustBelt's lifetime logic. The proof of safety of λ Rust 's type system, by virtue of being built atop the lifetime logic, did not need to be changed at all.

The rest of the paper is structured as follows. In §2, we briefly review the basics of relaxed-memory programming under the C11 memory model, as well as the basic idea (drawn from previous work) of how one can characterize such a memory model operationally. In §3, we present a representative fragment of iRC11, focusing on how it supports resource reclamation via cancellable invariants. In §4, we discuss how to prove soundness of iRC11: we motivate the need for synchronized ghost state in building a model for iRC11, and describe in some detail how the model works. In §5, we give further details about ORC11 ( §5.1) and iRC11 ( §5.2), about verifying and finding a bug in the Arc library ( §5.3), and about porting the lifetime logic ( §5.4). In §6, we conclude with a discussion of related work.

BACKGROUND: RELAXED-MEMORY OPERATIONAL SEMANTICS

We briefly review the C11 memory model in §2.1 and ORC11-the operational version of C11 that we use as the memory model for RB rlx -in §2.2.

C11, Intuitively

The C11 memory model offers several different modes of memory accesses, including non-atomic (na), relaxed (rlx), release (rel), acquire (acq), and sequentially consistent (sc). Non-atomic accesses are "normal" data accesses, meaning that it is the programmer's responsibility to ensure that they are properly synchronized through other means. (If they are not properly synchronized-i.e., there is a data race involving non-atomics-then C11 says the whole program has undefined behavior.)

The remaining modes, collectively called atomic accesses, are allowed to be racy and are indeed used to establish synchronization among non-atomic accesses.

To explain what synchronization actually means, we explore the examples in Fig. 2. In Example 2a, we initialize two locations X and Y to 0, then spawn two threads π (on the left) and ρ (on the right). Thread π intends to pass a "message" to ρ. The message, 42, is stored in X . Thread π then sets the boolean flag Y to 1, to signal to ρ that the message is ready to be received. Once ρ sees the flag set, it attempts to read the message from X . However, both the intended value of 42 as well as the initial value of 0 could be read. That is, even though ρ has read 1 from Y , it is not guaranteed to read 42 from X . This is because the relaxed accesses of Y are not enough to establish synchronization.

In the C11 memory model, threads are not synchronized by default: they each have their own perspective on the values in shared memory, and thus may observe memory events in different order. However, certain ways of performing accesses, as defined in C11, allow all threads to agree that one event happens-before another, and to "establish synchronization" is to somehow guarantee that two memory events of interest will be in the happens-before relation. Relaxed accesses are the weakest atomic accesses in C11 and do not guarantee happens-before. Thus, in Example 2a, the relaxed accesses on Y do not establish synchronization between the accesses on X .

In order to synchronize, we complement relaxed accesses with fences. 3 In Example 2b, thread π performs a release fence after the write to X , and then writes to Y . Meanwhile, ρ performs an acquire fence once it reads 1 from Y . Now, when ρ reads from X the result will be 42.

π successfully passes the message to ρ because C11 guarantees happens-before through chains of the form "release fence → relaxed write → relaxed read → acquire fence". That is, synchronization is guaranteed between the events before the release fence and the events after the acquire fence if the two fences are connected by the relaxed write and read. As a result, we know that π 's write of 42 to X happens before ρ's read of X -or in other words, that ρ's read of X is synchronized with π 's write to it. Since the write of 42 is the most recent write to X , we know that thread ρ must read 42.

Data races. Note that for Example 2a, where we do not have sufficient synchronization between the accesses to X , the worst thing can happen is that ρ would read unwanted values. However, if we were to replace the rlx accesses of X with non-atomic accesses (na), it would constitute a data race and the program would exhibit undefined behavior.

High-Level Overview of ORC11 (Operational RC11)

ORC11 is the operational version of C11 that we use for RB rlx . Its expression language, closely following that of λ Rust [Jung et al. 2018a], is a standard lambda calculus with recursive functions, fork-based concurrency, and references extended with relaxed consistency access modes: The syntax includes standard types of memory accesses, including reads, writes, compare-andset (CAS), and fetch-and-add (FAA), which atomically increments the contents of a location by a given integer. All memory accesses and fences are annotated with access modes o. As a shorthand notation, we use * ℓ and ℓ := v for na reads and writes (omitting the o).

alloc(e) allocates a fresh block of memory with size determined by e. free(e 1 , e 2 ) deallocates a block of memory starting at e 1 with size e 2 (we will often elide the size argument for simplicity). C11 only specifies that the lifetime of an object is from its allocation to deallocation, but does not specify a synchronization condition or possible races between allocation/deallocation and normal accesses. To fill this gap, we employ the following conditions that are widely thought to be reasonable.

The allocation of a block must happen-before all accesses to it.

(Alloc-Safe)

The deallocation of a block must happen-after all accesses to it.

(Free-Safe)

We consider violations of these conditions data races and, thus, undefined behavior. To implement them, we treat the semantics of allocations and deallocations as that of non-atomic writes with special values. We follow the reduction semantics of λ Rust except where interaction with memory is concerned, where we base the reduction rules on C11. As mentioned in the introduction, we cannot directly use C11 because (1) its semantics is flawed in several ways, and (2) it is formalized in an axiomatic (eventgraph) style, whereas for the purpose of instantiating Iris, we require an operational semantics that relates the programs state before and after an execution step. To address (1), we instead target RC11 [START_REF] Lahav | Repairing sequential consistency in C/C++11[END_REF]], which fixes the major flaws in C11. To address (2), we take inspiration from the approaches of [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF] and [START_REF] Kang | A Promising Semantics for Relaxedmemory Concurrency[END_REF], developing ORC11, an operational version of RC11. We give some more details about ORC11 in §5.1. In this section, we focus on the high-level aspects of ORC11 that are relevant for understanding the main body of this paper.

The key concept of the ORC11 semantics is that of views. A thread's view records the memory events (reads and writes) that the thread has observed so far-i.e., the events that happen-before the current step in the thread's execution. To account for C11's notion of synchronization, we define a partial view inclusion order on views: V 1 ⊑ V 2 holds if and only if all events in V 1 are also present in V 2 , in which case we sometimes say that V 2 has "seen" all the events in V 1 . Correspondingly, views also come with a join operator ⊔ that performs the role of synchronizing with another view:

V 1 ⊔ V 2 corresponds to the union of events in V 1 and V 2 . When a thread updates its view from V 1 to V 1 ⊔ V 2 ,
we will say that the thread is synchronizing with V 2 .

Every thread π actually maintains three views, which together form the thread-local view V:

(1) the current view V.cur contains all the events that π has observed, (2) the release view V.rel contains events that π had observed at its last release fence, and

(3) the acquire view V.acq contains events that π will have observed by its next acquire fence. Since a thread's views only grow over time, it is always the case that V.rel ⊑ V.cur ⊑ V.acq.

The global state consists of two parts (M, V Race ). First, M is the message pool that tracks all write events for all locations. It is modeled as a finite partial function from locations and timestamps to messages. Timestamps are used to encode a location's modification order ("mo")-a C11 relation that totally orders all writes to a single location. (The details of timestamps are largely inherited from [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF] and [START_REF] Kang | A Promising Semantics for Relaxedmemory Concurrency[END_REF]-for most of the paper, we will keep the discussion at the more abstract level of views and view inclusion.) Messages are records that contain (1) the value m.(val) written, and (2) a view m.(view) called the message view. The message view is used to communicate the observations from one thread's write to another thread's read, establishing synchronization (see below). The second component of the global state, V Race , is called the race detector view, because (unsurprisingly) it gets used by ORC11's race detector, as we describe in §5.1.

ORC11 is defined with a standard threadpool step relation, lifted from a per-thread step relation

(M, V Race ) | (e, V) - → (M ′ , V ′ Race ) | (e ′ , V ′ )
, where the scheduled thread π is executing its expression e with its thread-local view V and the shared global state (M, V Race ).

We refer the reader to our appendix and Coq development [START_REF] Dang | Appendix and Coq development accompanying this paper[END_REF] for the full semantics. Below, we give a high-level description for the semantics of the atomic operations used in Example 2b.

Step-Rlx-Write A relaxed write adds a message m, whose message view is the thread's release view V.rel extended by the write itself, to the message pool M. Only the current view V.cur and acquire view V.acq, but not V.rel, are updated to include the relaxed write event itself.

Step-Rel-Fence A release fence joins the thread's current view V.cur into its release view V.rel.

Step-Rlx-Read A relaxed read that reads the write encoded by m will join the message view m.(view) into the thread's acquire view V.acq.

Step-Acq-Fence An acquire fence joins the acquire view V.acq into the current view V.cur.

In Example 2b, in line π 1, the relaxed write of 42 to X is recorded in π 's current view, but not its release view. In line π 2, the release fence synchronizes π 's release view with its current view. In line π 3, the relaxed write to Y creates a message m with π 's release view-including the write of 42 to X . In line ρ1, if reading 1, the relaxed read joins m.(view) into ρ's acquire view. In line ρ2, the acquire fence joins ρ's acquire view into its current view, which now includes the write of 42 to X . In line ρ3, the relaxed read selects a message to read from that is no older than ρ's most recent observed write to X . With ρ having observed π 's write of 42 to X , it must then read 42. In this way, the ORC11 view semantics implements the release/acquire synchronization chain described above.

RESOURCE RECLAMATION UNDER RELAXED MEMORY WITH IRC11

iRC11 is a relaxed-memory separation logic for ORC11. Following iGPS [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF]], ORC11 is an instantiation of the Iris framework [Jung et al. 2018b]. Its soundness is derived within Iris, and it inherits its features both from the general Iris framework and from previous RMM logics. We begin in §3.1 by reviewing a small but representative set of features of iRC11 that come from previous RMM logics. In §3.2, we present the most notable novelty of iRC11: cancellable single-location invariants. In §3.3, we review the verification of the core of the Arc data type to demonstrate a crucially powerful property of the primitive ghost state assertions in RMM logics, namely that they are unsynchronized. (As explained in §1.1, we will need to develop a new form of synchronized ghost state when we model cancellation in §4.)

iRC11: The Old

Here, we review several core features of iRC11 that are inherited from prior RMM logics, including single-location invariants, fence modalities, and user-defined ghost state. A selection of rules concerning these features is displayed in Fig. 3. For now, please ignore all shaded parts, as these are new iRC11 additions pertaining to cancellable invariants, and we will discuss them in §3.2. More specifically, please ignore any parts concerning τ , as well as the two rules iRC11-CInv-Tok and iRC11-CInv-Cancel. 4Hoare triples and fancy updates. In these rules, we write {P } e @ π {v. Q } for Hoare triples with pre-condition P, expression e, thread id π (sometimes omitted), and post-condition Q where Q may mention v, i.e., the result of evaluating e. The thread id π is needed for fence modality assertions, as we explain below. A number of proof rules also make use of Iris's fancy updates, written P Q. Fancy updates are essentially a more flexible form of logical implication that also includes the ability to update ghost state-e.g., see Count-Ghost-Update in §3.3-among other things.

Assertions as view predicates. First of all, assertions in RMM logics, iRC11 included, need to represent not just ownership of some resources, but ownership of some resources with respect to the local perspective of the thread owning those resources. Assertions thus become predicates not only on resources but also on views. The reason for this may be illustrated by the points-to assertion of separation logic. If a thread owns ℓ → v, it should be guaranteed (among other things) that a read from ℓ will return v. In RMM, ownership of ℓ → v must therefore say something about the current local view V of the thread asserting it: V should contain the latest write to ℓ, and it should have value v. Otherwise, reading from ℓ could yield an older value and thus render at least one guarantee of the points-to assertion invalid.

The assertions in Fig. 3 are thus to be interpreted at some view. In the case of Hoare triples and assertions owned by a thread, the view used to interpret them is, by default, the thread's current

NA-Write {ℓ → -} ℓ := na v {ℓ → v} NA-Read {ℓ → v} * na ℓ {v. ℓ → v} Dealloc {ℓ → -} free(ℓ) {True} Rel-fence {P } fence rel @ π {∆ π P } Acq-fence {∇ π P } fence acq @ π {P } Ghost-Mod a γ ⇔ ∆ π a γ ⇔ ∇ π a γ iRC11-CInv-New ℓ → v * I(v) ∃τ . [τ ] 1 * τ ℓ I iRC11-CInv-FAA-Rlx ∀v. P * I(v) I(v + n) * Q(v) τ ℓ I ⊢ { [τ ] q * ∆ π P } FAA rlx (ℓ, n) @ π { v. [τ ] q * ∇ π Q(v) } iRC11-CInv-Tok [τ ] q+q ′ ⇔ [τ ] q * [τ ] q ′ iRC11-CInv-Cancel τ ℓ I ⊢ [τ ] 1 ∃v. ℓ → v * I(v)
Fig. 3. Selected iRC11 rules (new additions for cancellable invariants are shaded ). Note that fractions are always assumed to be well-formed, i.e., q ∈ (0, 1].

view. The view picked to interpret assertions, however, is not always necessarily some thread's current view. To allow transferring resources through writes, we also want to attach resources to write messages. In that case, the resources attached to a message m will be interpreted at the message view m.(view). Furthermore, as explained in §2.2, we have the fine-grained notion of a thread's local view V with its current view V.cur, release view V.rel, and acquire view V.acq. This leads to more choices (and more obligations) in picking which view to use when interpreting an assertion. As we will see below, the release and acquire views come into play when interpreting assertions concerning relaxed accesses and fences.

Points-to assertions. A familiar feature in separation logics is the points-to assertion. In iRC11, the points-to assertion ℓ → v represents the full ownership of the location ℓ as well as the knowledge that ℓ has the current value v. The assertion ℓ →simply ignores this knowledge about the value: ℓ → -::= ∃v. ℓ → v. With full ownership, one can perform any operation on ℓ, including nonatomic operations (NA-Write, NA-Read), atomic operations, and deallocation (Dealloc). Following prior RMM logics, iRC11 also supports fractional points-to assertions (not shown here) so that the permission to non-atomically read a location can be split up between concurrent threads.

Consider a variant of the Message-Passing example in Fig. 4a. Here, after allocation, we can initialize two locations X and Y to 0 with NA-Write because we own their points-to assertions. After spawning two threads, since we give thread π 1 (on the left) the points-to X → 0, it can write non-atomically to X again with NA-Write. In thread π 2 (on the right), if somehow after the acquire fence we receive the "message" X →from thread π 1 , then we can use Dealloc to free X . To complete the proof of this example, we need single-location invariants for Y .

Single-location invariants. All RMM logics have a notion of single-location invariants. This feature comes from the observation that, although general invariants are unsound in RMM because threads may have different views on a region of multiple locations, invariants that only govern a single location are sound because threads do agree on the order of writes to any single location. Prior RMM logics support a range of somewhat different single-location invariant mechanisms, including some that let the user establish "protocols" on how a location's value can evolve over time. iRC11 inherits such a protocol mechanism from iGPS, but for the purpose of this paper we focus on a , Vol. 1, No. 1, Article . Publication date: November .

{X → - * Y → -}X := 0; Y := 0; simplified version that ignores the extra functionality of protocols, as that is orthogonal to the issue of resource reclamation.

{X → 0 * Y → 0} X → 0 * Y I Y X → 0 * Y I Y X := 42; {X → 42} fence rel ; @ π 1 ∆ π 1 X → 42 FAA rlx (Y, 1); {True} Y I Y if FAA rlx (Y, 2) == 1 ∇ π 2 X → 42 fence acq ; @ π 2 {X → -} free(X ); {True} (a) With basic invariants. {X → - * Y → -}X := 0; Y := 0; {X → 0 * Y → 0} [τ ] 1 * τ X ⊤ * Y I Y [τ ] 1/2 * τ X ⊤ * Y I Y FAA rlx (X, 42); [τ ] 1/2 fence rel ; @ π 1 ∆ π 1 [τ ] 1/2 FAA rlx (Y, 1); {True} [τ ] 1/2 * τ X ⊤ * Y I Y if FAA rlx (Y, 2) == 1 [τ ] 1/2 * ∇ π 2 [τ ] 1/2 fence acq ; @ π 2 {[τ ] 1 } {X → -} free(X ); {True} (b) With cancellable invariants.
The invariant assertion ℓ I asserts the knowledge that an invariant I governs ℓ. As an invariant represents knowledge, not exclusive ownership, it is a duplicable assertion that can be passed on to multiple concurrent threads. With iRC11-CInv-New we can initialize an invariant for ℓ if we have the full ownership ℓ → v and the resource I(v). The predicate I, also called the interpretation, is a user-defined predicate on values: I(v) describes the invariant over shared resources that must hold in order for ℓ to have the value v. I(v) is a requirement that every write of value v to ℓ must provide. Intuitively, the resource I(v) is attached to the message m created by the write of v to ℓ. When a read of value v from ℓ finds the message m, it can use I(v) for its reasoning. As such, the interpretation encodes resources to be transferred from writes to reads. This is demonstrated in the premise of the fetch-and-add (FAA) access rule iRC11-CInv-FAA-Rlx for an invariant ℓ I . A FAA is a read-modify-write (RMW) operation that has the atomic effect of both a read and a write. (Note that we are focusing on FAA here, rather than plain relaxed writes and reads, merely because the proof rules for FAA are a bit simpler and they suffice for the purpose of our story in this paper. In iRC11, we of course also support rules for reads, writes, and CAS.) As the FAA is a write, we must establish the interpretation I(v + n) for the value v + n that the FAA is going to write. But we can also use the interpretation I(v) for the value v that the FAA read and our local resource P to establish I(v + n). If there is any remaining resource Q(v), we can take it out as our local resource afterwards. This is the standard way in RMM logics to model the ownership transfer that is achievable with RMW operations like FAA.

In Fig. 4a, we want to transfer X →through the communication from thread 1's FAA to thread π 2 s FAA on Y . To do so, we set up an invariant I Y for Y :

I Y (v) ::= v ≥ 0 ∧ if v = 1 then X → -else True
That is, the invariant owns X →if the value of Y is currently 1. With Y → 0, we can initialize the invariant for Y with iRC11-CInv-New where I Y (0) is trivial. We then pass knowledge of the invariant Y I Y to both threads. When thread π 1 writes 1 (FAA from 0 to 1) to Y , it uses iRC11-CInv-FAA-Rlx with P ::= X →to transfer the ownership of X into I(1) (and with Q ::= True to take nothing out). When thread π 2 reads 1 (FAA from 1 to 3) from thread π 1 's write, it also uses iRC11-CInv-FAA-Rlx with Q ::= X →to take the ownership out of I Y (1) (and with P ::= True because it does not need anything to establish the trivial I Y (3)). The transfer, however, is not completed yet, because there are caveats in using the rlx access mode, which we explain next. Fence modalities. To model the effects of relaxed accesses and fences, iRC11 inherits two modalities from FSL [Doko andVafeiadis 2016, 2017]-the release modality ∆ and the acquire modality ∇-which allow us to talk about ownership of resources at a thread's release or acquire views. The assertion ∆ π P represents ownership of P at thread π 's release view, while the assertion ∇ π P represents ownership of P at thread π 's acquire view.

The motivation for these modalities as follows. We have some resource described by the proposition P that we want to transfer from one thread to another through a pair of a relaxed write and a relaxed read (or in our example, a pair of relaxed FAA's), communicating through a single-location invariant (in our example, I Y ). However, when the "producer" thread π 1 performs its relaxed write, the message view of that write is drawn from π 1 's release view, not its current view. Hence, we need a way of insisting (in the precondition of the relaxed write) that the P that π 1 is sending holds under its release view-that is what is denoted by ∆ π 1 P. Dually, when the "consumer" thread π 2 performs its relaxed read, the message view it reads will only be joined into its acquire view, not its current view. Hence, we need a way of insisting (in the postcondition of the relaxed read) that π 2 only receives ownership of P under its acquire view-that is what is denoted by ∇ π 2 P. Since FAA combines a read and a write, the FAA rule (iRC11-CInv-FAA-Rlx) combines both of these reasoning principles into one.

Of course, we now need a way of actually introducing ∆ π 1 P and eliminating ∇ π 2 P. These steps are achieved by rules Rel-fence and Acq-fence, which allow one to transfer any proposition into the release modality at the point of a rel fence, or out of the acquire modality at the point of an acq fence, because those are the points where the current and release/acquire views get synchronized.

In Fig. 4a, because we are using relaxed FAA's, we have to provide ∆ π 1 X →in thread π 1 , and we receive ∇ π 2 X →in thread π 2 . In thread π 1 , with a release fence, we use Rel-fence to put X →under the release modality and then perform the FAA. In thread π 2 , with an acquire fence, we use Acq-fence to regain X → -. Then the transfer is completed and thread π 2 can safely deallocate X .

iRC11: The New -Cancellable Invariants

The problem with standard single-location invariants from previous logics is that they cannot be reclaimed. Consider the example in Fig. 4b, which is identical to Fig. 4a except that X is used atomically instead of non-atomically. To use X atomically, we need to govern it with invariants. But in prior logics, any invariant placed on X would govern it forever, making it non-reclaimable.

One key novelty of iRC11 is the ability to cancel its single-location invariants, so that atomic locations can be reclaimed fully. To make single-location invariants cancellable, iRC11 takes a page from Iris-SC cancellable invariants (Fig. 1) where the invariant is guarded by a token τ (see the shaded part in Fig. 3). As seen in iRC11-CInv-FAA-Rlx, only those who own a fraction [τ ] q of τ can access the invariant. Similar to SC cancellable invariants, the ownership [τ ] q guarantees that the invariant τ ℓ I has not been cancelled and is still accessible.

After initializing the invariant with iRC11-CInv-New, we obtain the full token [τ ] 1 which can be split and rejoined with iRC11-CInv-Tok so that multiple threads can access the invariant concurrently. Once all threads are done using the location through the invariant, the thread π owning the full token [τ ] 1 can cancel the invariant with the rule iRC11-CInv-Cancel. The thread π then reclaims the points-to ℓ → v for some value v, which guarantees that π has synchronized with all other accesses to ℓ, and thus π can safely deallocate ℓ or use ℓ non-atomically. The thread also reclaims I(v), the interpretation at the last write before the cancellation. I(v) can be useful, for example, when ℓ is a lock and v is the "unlocked" state. In that case, the lock-protected content is still in I(v) and we can reclaim it. This feature is thus important in verifying locks, of which Rust's Mutex<T> library is an example.

, Vol. 1, No. 1, Article . Publication date: November .

To verify Fig. 4b, we create a cancellable invariant for X , guarded by τ , with a trivial interpretation I X ::= True (written ⊤ in the proof outline) because we only want to access X concurrently, not to transfer any resource through it. We still use a non-cancellable invariant for Y since we do not care about reclaiming Y here. But we do use a slightly different interpretation for Y :

I Y (v) ::= v ≥ 0 ∧ if v = 1 then [τ ] 1/2 else True.
Here, instead of transferring X → -(which allows non-atomic accesses to X ) through the invariant of Y , we transfer [τ ] 1/2 (which allows atomic accesses to X ). We use the invariant I Y only to transfer half of the token ([τ ] 1/2 ) from thread π 1 to thread π 2 , because we also want to give the other half to thread π 2 (when spawning π 2 ) so that it can access X concurrently with thread π 1 (not shown in the example). After the acquire fence, thread π 2 will then regain the full token [τ ] 1 (instead of X → -); then it can use iRC11-CInv-Cancel to cancel the invariant and reclaim X → -, after which it can safely free X .

User-Defined Ghost State in Relaxed Memory

We turn our attention now to an essential feature of the more recent RMM logics-user-defined ghost state-which iRC11 inherits directly from Iris. Ghost state is logical state that is used to track additional information in the verification, but is not part of physical state. In Iris, the user of the framework is free to define the particular structure of ghost state-in the form of a partial commutative monoid (PCM)-that is appropriate for their proof. More specifically, the user can define their own PCM M and Iris will give them a new class of ghost assertions of the form a γ , which asserts the ownership of some ghost element a (a member of M) stored at a ghost location γ .

Iris also provides a few basic proof rules for reasoning about these ghost assertions, with which the user can derive a "ghost theory" (a logical API) applicable to their PCM [Jung et al. 2018b].

User-defined ghost state is useful in deriving domain-specific logics. For example, the points-to assertions, single-location invariants, and fence modalities are all derived by iRC11 in Iris, each with the help of a specialized PCM. Furthermore, iRC11 also exposes this facility to its users, so that they can employ it for their own verifications of RMM algorithms. And, indeed, ghost state has proven indispensable for verifying intricate concurrent data structures in both traditional SC and RMM separation logics. In the setting of RMM, however, ghost state enjoys an additional property that is encoded in the Ghost-Mod rule (Fig. 3).

Ghost-Mod states that the ghost assertion a γ can move freely in and out of the fence modalities. This is because ghost state belongs to the class of unsynchronized assertions, in the sense that their ownership is not tied to the physical, subjective view of the thread asserting them. Recall that ∆ π P and ∇ π P assert that P holds at π 's release view and acquire view, respectively. Since a γ is unsynchronized and thus does not care at which view it is interpreted, it is equivalent to ∆ π a γ or ∇ π a γ . As a result, a γ can be transferred from one thread to another without the need for physical synchronization-in particular, without the need for release/acquire fences. (For more details, please see the model of fence modalities and unsynchronized ghost state in §5.2.) To help the reader appreciate the importance of Ghost-Mod, we now quickly review the verification of Core Arc, a simplified version of Rust's Arc library. (See §5.3 for more details about our verification of the full Arc.) Core Arc has been verified previously in FSL++ [START_REF] Doko | Tackling Real-Life Relaxed Concurrency with FSL++[END_REF], but their proof did not account for the reclamation of Arc's reference count field. In RB rlx , we improve on their proof by fully verifying Arc's destructor using iRC11 cancellable invariants.

3.3.1 Core Arc Library. Arc<T>, short for Atomically Reference Counted, is used to share atomically an object of type T, whose mutation is disabled by default. To mutate T, one needs T to support thread-safe mutability, for example with T being an atomic type, or with T wrapped inside a lock (e.g., Mutex<T>). The following Rust example instantiates Arc with an atomic integer AtomicUsize and demonstrates how Arc is typically used: In line 1 in the main thread, a new Arc pointer arc1 is created to govern an atomic integer allocated in shared memory, and arc1's internal counter field for the number of references to the content is set to 1. An Arc pointer acts almost like its underlying content, so in line 6 we can call fetch_add on arc1 as if on the atomic integer itself. To share the content with the child thread, we create another arc2 by clone-ing arc1 (line 2), which has the effect of incrementing the counter field to 2: there are now 2 Arc objects sharing the atomic integer. Unsurprisingly, to allow concurrent clone-ing, the counter field is itself implemented with an atomic integer, too.

When the Arc pointers go out of scope (after lines 4 and 6), their destructor-the drop method-is called, and the counter field is decremented accordingly. The last call of drop will deallocate both the data and counter fields.

The implementation of Core Arc is given in Fig. 5. The new method allocates a region of two locations for the counter and data fields, then initializes them. The deref method provides access to the data field, effectively allowing an Arc<T> to behave like its content T. The clone method does a rlx FAA by 1 to increment counter and then returns a copy of a.

Finally, the drop method does a rel FAA by -1 to decrement counter. If the value of counter was 1 before the decrement-i.e., this is the last drop-drop additionally does an acquire (acq) fence before deallocating both the counter and data fields. With that acquire fence, the deallocation of the region a in the last drop is guaranteed to be synchronized with all previous calls to drop. This, in turn, guarantees that the deallocation is synchronized with all concurrent accesses by other pointers to the region a-i.e., there is no data race between the deallocation and the accesses.

Core

Arc's Invariant. Core Arc has the following simple specification:

{True} new(v) {a. ∃ τ , γ . ARC γ (a, v, τ , I)} (ARC-New) {ARC γ (a, v, τ , I)} clone(a) {ARC γ (a, v, τ , I) * ARC γ (a, v, τ , I)} (ARC-Clone) {ARC γ (a, v, τ , I)} deref(a) {x. x = v * ARC γ (a, v, τ , I)} (ARC-Deref) {ARC γ (a, v, τ , I)} drop(a) {True} (ARC-Drop)
Here, ARC is an abstract predicate that represents the logical ownership of an Arc object and gives one permission to invoke methods on the Arc object a, and I is a single-location invariant governing the shared location a.counter, which enables threads to access a.counter atomically. The two main challenges of the verification are (1) cloning the ARC permission (in ARC-Clone) even though clone only uses a relaxed FAA and (2) safely deallocating the region at the last invocation of drop (ARC-Drop).

, Vol. 1, No. 1, Article . Publication date: November .

The definitions of ARC and I are given as follows. We explain them piecemeal below, beginning with the unshaded parts, which are essentially the same as in the proof of [START_REF] Doko | Tackling Real-Life Relaxed Concurrency with FSL++[END_REF].

ARC γ (a, v, τ , I) ::= ∃q. a.data q -→ v * [τ ] q * τ a.counter I γ ,v * Count(q)
γ (ARC-Own)

I γ ,v (n) ::=                  False n < 0 TotalCount(0, 0) γ n = 0 ∃q in , q out ∈ (0, 1). a.data q in --→ v * [τ ] q in * q in + q out = 1 * TotalCount(n, q out ) γ n > 0 (ARC-Inv)
Each ARC permission has several components. First, it has a fractional points-to assertion for a.data. This fractional assertion is essential for verifying ARC-Deref, since the deref method relies on the ARC permission to justify a non-atomic read of a.data. In the verification of ARC-Clone, this fractional permission is split into two half permissions (a.data q/2 --→ v), which are then used to satisfy the two ARC predicates in the postcondition. Second, ARC stipulates the knowledge that a.counter is governed by the single-location invariant I. This invariant, in turn, owns the remainder of a.data: the fraction of a.data-namely, q in -that is not owned by any ARC. Third, ARC owns a ghost element Count(q)

γ . We now explain in detail what purpose this ghost element serves, and how it interacts with the invariant I.

Unsynchronized Ghost

State for Core Arc. The invariant I needs to maintain that the total number of ARC permissions currently in existence is equal to the current physical value n of a.counter. It does so using a "ghost theory" of counting permissions [START_REF] Bornat | Permission accounting in separation logic[END_REF]]. This ghost theory involves two ghost assertions:

• the single count assertion, Count(q) γ , which represents the contribution of a single ARC predicate to the total number of ARC permissions currently in existence, as well as the fact that that ARC predicate owns a q fraction of a.data, and • the total count assertion, TotalCount(n, q out ) γ , which stipulates that currently there are n ARC permissions in existence, and that the sum of all their fractions of a.data equals q out . The invariant I then enforces that the n in TotalCount(n, q out ) γ matches the current physical value of a.counter, and that the remainder fraction (q in ) of a.data owned by I is precisely 1q out . Formally, these ghost assertions are built from Iris's Auth PCM [Jung et al. 2018b]: Count(q) γ ::=

• (1, q) γ and TotalCount(n, q) γ ::= • (n, q) γ . The details of this construction are not important for the present discussion; the important point is that it establishes the soundness of various rules for manipulating these assertions, such as the following ghost update rule:

TotalCount(n, q out ) γ * Count(q) γ TotalCount(n + 1, q out ) γ * (Count-Ghost-Update) Count(q/2) γ * Count(q/2) γ
This rule allows us to split a single count into two by increasing the total count by 1, without changing the total fraction q out . It is needed in the proof of clone: there, we need to produce two single counts Count(q/2) γ , for the two new ARC permissions, from the one single count Count(q) γ of the original ARC permission, and this requires accessing the TotalCount predicate in I and applying Count-Ghost-Update. However, there is a problem. Since clone uses a relaxed FAA, we will be using rule iRC11-CInv-FAA-Rlx to access the invariant I, but if we instantiate that rule with P ::= Count(q) γ and

Q ::= Count(q/2) γ * Count(q/2)
γ , what we obtain is:

{∆ π ( Count(q) γ )} FAA rlx (a.counter, 1) @ π {∇ π ( Count(q/2) γ * Count(q/2) γ )}

But what we really need is:

{ Count(q) γ } FAA rlx (a.counter, 1) @ π { Count(q/2) γ * Count(q/2) γ } This is where Ghost-Mod saves the day! We can immediately derive the latter Hoare triple from the former from the fact that both the pre and post are unsynchronized ghost state assertions.

In general, unsynchronized ghost state is useful for encoding objective, view-agnostic information about globally consistent properties of a data structure, such as (in the case of Arc) the total number of Arc permissions currently in existence. Fully relaxed (rlx) accesses suffice to update such viewagnostic state consistently, and the Ghost-Mod rule lets us exploit that. We hasten to add that this is not a novel observation-as [START_REF] Doko | Tackling Real-Life Relaxed Concurrency with FSL++[END_REF] have already noted: "The most important feature of ghost state from the perspective of the verification of Arc is [the] ability to transfer ownership of ghosts without the need for synchronization. This is achieved by having the ghost state be agnostic with respect to the ∆ and ∇ modalities. " 3.3.4 Core Arc Fully Reclaimed. The FSL++ verification of Core Arc can only reclaim the data field, but not the counter field. In the proof of the last drop, [START_REF] Doko | Tackling Real-Life Relaxed Concurrency with FSL++[END_REF] can only reclaim a.data → -, because a.counter is governed by a permanent invariant. Using iRC11 cancellable invariants, however, we can verify what Rust's Arc really does, which is to reclaim both fields.

Specifically, we create a cancellable invariant for a.counter, guarded by τ , and then treat [τ ] q analogously to a.data q -→ v: wherever we use a.data q -→ v to represent shared ownership of a.data, we mirror that with the use of [τ ] q for the exact same q to represent shared ownership of a.counter. This proof extension is shaded in the definition of ARC (ARC-Own) and I (ARC-Inv). Therefore, when the last drop regains the full ownership of a.data → -, it also regains the full token [τ ] 1 , enough to invoke iRC11-CInv-Cancel and reclaim ownership of a.counter → -. The whole region can then be safely deallocated. This example demonstrates that the changes needed for adapting uses of ordinary invariants to uses of cancellable invariants are modular and manageable.

MODELING CANCELLABLE INVARIANTS WITH SYNCHRONIZED GHOST STATE

In the previous section, we saw how iRC11's support for both cancellable invariants and userdefined ghost state played a crucial role in verifying data structures like Rust's Arc. As it turns out, ghost state also plays an important role in building a model for cancellable invariants-in particular, in defining the semantics of invariant tokens. However, in the relaxed-memory setting, it is unsound to model invariant tokens using the unsynchronized ghost state we have seen so far. In this section, we show how to soundly model iRC11 cancellable invariants instead using a novel construction of synchronized ghost state.

Deriving Unsoundness in a Naive Model with Unsynchronized Ghost State

Let us begin by showing why a naive model of iRC11's cancellable invariant tokens using unsynchronized ghost state cannot possibly work.

Suppose that it did-that is, suppose that invariant tokens were modeled purely as some form of unsynchronized ghost state assertion. If that were possible, it would mean that, according to Ghost-Mod, token assertions would be agnostic to the fence modalities:

[τ ] q ⇔ ∆ π [τ ] q ⇔ ∇ π [τ ] q .
We will show that this in turn would enable us to spuriously verify the example given in Fig. 6. This example is exactly the same as Fig. 4b, except that there are no fences, and thus there is no

{X → - * Y → -}X := 0; Y := 0; {X → 0 * Y → 0} [τ ] 1 * τ X True * Y I Y [τ ] 1/2 * τ X True * Y I Y FAA rlx (X, 42); [τ ] 1/2 ∆ π 1 [τ ] 1/2 Unsound! FAA rlx (Y , 1); {True} [τ ] 1/2 * τ X True * Y I Y if FAA rlx (Y, 2) == 1 [τ ] 1/2 * ∇ π 2 [τ ] 1/2 {[τ ] 1 }Unsound! {X → -}free(X ); {True}
Fig. 6. Buggy example verified where [τ ] q is modeled with unsynchronized ghost state.

Raw-CInv-New I ∃τ . [τ ] 1 * τ I Raw-CInv-Tok [τ ] q+q ′ ⇔ [τ ] q * [τ ] q ′ Raw-CInv-Acc ∀V i . { ⌊I ⌋ ⊔V i * P } e @ π { v. ⌊I ⌋ ⊔V i * Q } atomic(e) τ I ⊢ { [τ ] q * P } e @ π { v. [τ ] q * Q } Raw-CInv-Cancel τ I ⊢ [τ ] 1 I Fig. 7
. Selected rules for RMM-sound raw cancellable invariants.

synchronization between thread 2's deallocation of X and the FAA on X performed by thread 1. As a violation of Free-Safe (see §2.2), this constitutes a data race and thus undefined behavior. To spuriously verify this example, we use the exact same proof as Fig. 4b, except that instead of using the fence rules, we simply use Ghost-Mod to move the token [τ ] q across the fence modalities. Note that this proof step is only possible because we assume the tokens are modeled with unsynchronized ghost state. Then, when thread 2 regains the full token [τ ] 1 , it uses iRC11-CInv-Cancel to obtain X → -. This, in turn, licenses the subsequent racy deallocation of X .

As we can see from this scenario, any model for cancellable invariant tokens based purely on unsynchronized ghost state violates a key safety guarantee: An invariant's cancellation must happen-after all accesses to it.

(Cancel-Safe)

Raw Cancellable Invariants

It is obvious that the invariant tokens need to be made view-dependent, so that Ghost-Mod does not apply to them and the example in Fig. 6 is not verifiable. It is less obvious, though, what a sound model of invariant tokens (guaranteeing Cancel-Safe) should look like.

Before we can answer that question, it is helpful to first simplify the problem. In this subsection, we present an important intermediate mechanism we call raw cancellable invariants. Raw cancellable invariants are sound for RMM but support a much simpler set of proof rules than iRC11 cancellable invariants do. In §4.3, we will then show how to construct a model of raw invariant tokens using synchronized ghost state. Finally, in §4.4, we will use raw cancellable invariants as the key stepping stone for building a model for the single-location cancellable invariants of iRC11.

Selected rules of raw cancellable invariants are given in Fig. 7. Like the previous forms of cancellable invariants we have seen, a raw cancellable invariant τ I describes an invariant protected by an invariant token τ . However, the rules for raw cancellable invariants are much closer to those for Iris-SC's cancellable invariants than iRC11's. In particular, raw cancellable invariants are general invariants that are not restricted to a single location: they can contain arbitrary resources, and yet they are still sound in RMM. The invariant can be created with Raw-CInv-New if we can provide the initial invariant content I , and can be cancelled with Raw-CInv-Cancel if we have the full token [τ ] 1 , after which we reclaim ownership of the content I . These rules are exactly the same as those of SC-sound cancellable invariants (Fig. 1).

The only rule that differs from Iris-SC's cancellable invariants is the access rule Raw-CInv-Acc. Recall that the access rule allows any thread to access and update the invariant content I during a single, atomic physical step (thus the side-condition atomic(e)). 5 The rule for accessing raw invariants is, however, significantly weakened from its SC counterpart (SC-CInv-Acc)-this is in order to keep raw invariants sound in RMM. Recall that in iRC11, assertions are to be thought of as view predicates. If the SC access rule SC-CInv-Acc were sound for raw cancellable invariants, it would mean that at any instant a thread π could assume that the shared resource backing up the invariant satisfied I at π 's local view V π , and it could also update the resource to one satisfying I at V π . But clearly, since in RMM different threads have different views of memory, such reasoning is unsound. (It is only sound under SC because under SC all threads share the same view of memory.)

Since the content view V i -i.e., the view at which I is justified-can be constantly changed by different threads accessing the invariant, there is in general no relationship between threads' current local views and the content view V i . Therefore, the access rule Raw-CInv-Acc cannot equate the view at which the content is provided with the current local view of the thread. The rule can only provide I protected by a new modality we call the view-join modality. To explain this modality, we must first review some basics of how assertions are modeled in iRC11.

Basics of modeling iRC11 assertions. To understand the model • of iRC11 assertions in Iris, recall that • is of type vProp → View → iProp, where vProp is the type of iRC11 assertions and iProp is the type of Iris assertions. The model • interprets iRC11 assertions as view predicates in Iris, i.e., for P ∈ vProp, P ∈ View → iProp.

Furthermore, it is crucial that these predicates be view-monotone, i.e., that iRC11 assertions remain valid when the thread witnesses additional memory events. Formally, monotonicity means that if V 1 ⊑ V 2 , then P (V 1 ) implies P (V 2 ). This requirement stems from separation logic's "frame rule". Intuitively, a thread owning (X → v) * P must be able to frame P around accesses to X -i.e., retaining ownership of P throughout-even though such accesses will grow the thread's local view. For this, the validity of P must be monotone in the thread's local view and, in general, be monotone with respect to any view.

In the following, we use blue font-face to distinguish Iris assertions against iRC11 assertions, which are in black font-face.

View-join modality. If P ∈ vProp and V b ∈ View, then the semantics of the view-join modality ⌊P⌋ ⊔V b is defined by ⌊P⌋ ⊔V b (V ) ::= P (V ⊔ V b ), which means that P holds at the join of the thread's current view V and V b .

The rule Raw-CInv-Acc uses this view-join modality to restore soundness of the access rule under RMM. Notice that the appearances of the invariant content I in the premise occur under the view-join modality ⌊I ⌋ ⊔V i . This means that, when we use Raw-CInv-Acc to open a raw cancellable invariant τ I , we only gain access to I at an arbitrarily larger view V ⊔ V i , where V i represents the view at which the invariant content is currently justified. During the access to I , the instruction e can update π 's current view to a larger view V ′ , so long as it returns the invariant content at the view V ′ ⊔ V i . To explain why this weakened access rule is sound, we now delve into the details of synchronized ghost state and the model of raw invariants.

The Model of Raw Cancellable Invariants

The model of invariant tokens and raw cancellable invariants is as follows.

[τ ] q (V )

::= ∃V tok . PartialV(q, V tok ) τ * V tok ⊑ V (Raw-CInv-Model-Tok) τ I (V ) ::= ∃V i . PartialV(1, V i ) τ ∨ ( I (V i ) * FullV(V i ) τ ) (Raw-CInv-Model)
Invariant tokens. First of all, invariant tokens [τ ] q are view-dependent assertions: even though owning a token [τ ] q means owning only the ghost element PartialV(q, V tok )

τ , this ghost ownership is tied to the view V at which the assertion is interpreted through the token view V tok . In particular, the ghost element PartialV(q, V tok ) τ records both the fraction q, which represents how much of the invariant this token owns, and the token view V tok , which represents what this particular fractional token has observed, i.e., what invariant accesses this fractional token has participated in. The model requires that V -the view at which the token is interpreted-has also at least observed what [τ ] q has observed: V tok ⊑ V . Being view-dependent, [τ ] q therefore no longer enjoys Ghost-Mod, so the spurious verification in §4.1 is excluded.

Invariant assertions. The model of invariant assertions τ I simply encodes the two possible states of the invariant: "active" or "cancelled". Thus it is an Iris invariant of a disjunction (see Raw-CInv-Model). The right-hand side of the disjunction encodes the active state, where the content I is still available in the invariant at some content view V i . In the active state the Iris invariant also owns a ghost element FullV(V i )

τ that records the view V i in the ghost state. The left-hand side of the disjunction encodes the cancelled state, which asserts ownership of the full fractional element PartialV(1, V i ) τ . Note that the invariant assertion τ I itself is view-agnostic: it ignores the view V at which it is asserted. The relation between the content view V i and the token views V tok 's is managed entirely by the ghost elements FullV(V i ) τ and PartialV(q, V tok ) τ .

Synchronized ghost state. These view-dependent ghost elements are members of a "synchronized ghost state" instance that we build to model raw invariants. This ghost construction has two kinds of elements: (1) a unique element FullV(V f )

τ that is used to record the full view V f , and (2) fractional elements PartialV(q, V p ) τ that are used to associate some partial view V p with some fraction q.

The ghost construction is built to maintain the following property:

The join of all partial views (the V p 's from all PartialV(q, V p )

τ 's) is always equal to the full view V f in FullV(V f ) τ . (Sync-Ghost)
This property guarantees that the partial view V p of the full fractional element

PartialV(1, V p ) τ is actually equal to the full view V f of FullV(V f ) τ : V p = V f . The Sync-Ghost
property is what we require for view-dependent ghost state to be synchronized ghost state. By synchronized ghost state we mean any ghost construction that is built on the notion of fractional observations. That is, the ghost state has fractional elements that track the subjective observations of the threads the elements are tied to, and, most importantly, the full fractional element is guaranteed to have tracked all observations. In the case of raw cancellable invariants, the observations are the views around which threads access and update the invariant content I . Intuitively, we record the view V i of the invariant content I as the full view in FullV(V i )

τ . The token view V tok in the ghost ownership PartialV(q, V tok ) τ of some token [τ ] q tracks the changes to I made by each access that [τ ] q participated in. By Sync-Ghost, the full token view V tok_full of the full token [τ ] 1 will thus be equal to the content view V i . Consequently a thread owning [τ ] 1 must have observed all changes to the invariant content I .

Raw-CInv-Model-Sync

FullV(V i ) τ * PartialV(q, V tok ) τ ⇒ V tok ⊑ V i ∧ (q = 1 ⇒ V tok = V i ) Raw-CInv-Model-Update FullV(V i ) τ * PartialV(q, V tok ) τ FullV(V ′ ⊔ V i ) τ * PartialV(q, V ′ ⊔ V tok ) τ Raw-CInv-Model-Join PartialV(q, V ) τ * PartialV(q ′ , V ′ ) τ ⇒ PartialV(q + q ′ , V ⊔ V ′ ) τ * q + q ′ ≤ 1 Fig. 8.
Selected properties (at Iris level) of the ghost construction for raw cancellable invariants.

To maintain Sync-Ghost, the ghost construction for PartialV(q, V tok ) τ and FullV(V i ) τ admits the rules in Fig. 8. (We omit the details of how they are encoded, but for Iris enthusiasts the resource algebra from which they are drawn is Auth (Option (Frac × View ⊔ )).) Raw-CInv-Model-Sync says that any token view V tok is included in the content view V i , and the full token view V tok_full of [τ ] 1 is exactly V i . Raw-CInv-Model-Join requires that the fractions consistently cannot sum up to more than 1, and also allows us to join together partial token views of the fractions when we are recollecting them. Raw-CInv-Model-Update formalizes a restriction on how the ghost state can grow: We can update a token view V tok by extending it with some V ′ only if we simultaneously update the content view V i in the same way. This makes sure that every change in the full view V i is accounted for by some token view V tok , and thus Sync-Ghost is maintained.

Proving cancellation. To understand how the model works, we briefly present the proof of the cancellation rule Raw-CInv-Cancel. To prove a rule sound in the model, we first interpret the rule at the current view V of the thread π that applies the rule and then prove it in Iris. For Raw-CInv-Cancel, we need to prove the following in Iris:

τ I (V ) * [τ ] 1 (V ) I (V )
The user of this rule provides us-the prover of the rule-with the full token [τ ] 1 at V , and we need to give the user back I at the same V . Looking at the interpretation of tokens, we effectively have the full fractional PartialV(1, V tok_full ) τ with a token view V tok_full ⊑ V . We then open the Iris invariant and find a content view V i and the two possibilities for the invariant state (see Raw-CInv-Model). If the invariant were in the cancelled state, we would have two full fractional PartialV(1, -) τ and

Raw-CInv-Model-Join would give us contradiction from 1 + 1 ≤ 1. Thus the Iris invariant must be in the active state. By owning the full fraction, with Raw-CInv-Model-Sync we know that the thread's current view V must have observed all changes to the invariant content:

V ⊒ V tok_full = V i .
With that, we now can take the content I (V i ) out of the invariant and upgrade it to I (V ) for the user, because I is view-monotone. To finish the proof, we use PartialV(1, V tok_full ) τ to switch the Iris invariant to the cancelled state and re-establish it. □

Proving access. The proof outline of the access rule Raw-CInv-Acc is shown in Figure 9. The proof is an application of standard Iris proof rules. As in cancellation, we first open the invariant and deduce that it must be in the active state. Then, we apply the rule of consequence which leaves us with two side goals that we discuss below. Finally, we use framing to arrive at our premise.

As indicated in the outline, we have two goals to prove for the application of the rule of consequence: (1) prove that from the pre-condition of the conclusion we can obtain the pre-condition of the premise and (2) from the post-condition of the premise, we can obtain the post-condition of the conclusion. In task (1), our goal is follows from view monotonicity. In task (2), our goal is

I (V ) ⌊I ⌋ ⊔V i (V ), i.e., I (V ) I (V ⊔ V i ), which , Vol. 1, No. 1, Article . Publication date: November . 1 ⃝ { ⌊I ⌋ ⊔V i (V ) * P (V ) } e @ π { v , V ′ ⊒ V . ⌊I ⌋ ⊔V i (V ′ ) * Q (V ′ ) } Assumption { ⌊I ⌋ ⊔V i (V ) * FullV(V i ) τ * PartialV(q, V tok ) τ * V tok ⊑ V * P (V ) } e @ π { v , V ′ ⊒ V . ⌊I ⌋ ⊔V i (V ′ ) * FullV(V i ) τ * PartialV(q, V tok ) τ * V tok ⊑ V * Q (V ′ ) } Frame { I (V i ) * FullV(V i ) τ * PartialV(q, V tok ) τ * V tok ⊑ V * P (V ) } e @ π { v , V ′ ⊒ V . I (V ′ ⊔ V i ) * FullV(V ′ ⊔ V i ) τ * PartialV(q, V ′ ) τ * Q (V ′ ) } 2 ⃝ τ I ⊢ { [τ ] q (V ) * P (V ) } e @ π { v , V ′ ⊒ V . [τ ] q (V ′ ) * Q (V ′ ) } Inv
FullV(V i ) τ * PartialV(q, V tok ) τ * V tok ⊑ V FullV(V ′ ⊔ V i ) τ * PartialV(q, V ′ ) τ
This proof step amounts to an application of Raw-CInv-Model-Update where we make use of the fact that

V ′ ⊔ V tok = V ′ . This follows from V tok ⊑ V ⊑ V ′ . □

The Model of iRC11 Single-Location Cancellable Invariants

The access rule for raw cancellable invariants, Raw-CInv-Acc, may seem overly restrictive: due to the use of the view-join modality in the premise, the invariant content is only made accessible at an arbitrarily large view V ⊔ V i , where V is the thread's local view and V i is unknown. How, the reader may wonder, can that be useful? To illustrate how this apparent limitation is not really a problem at all, we now give a high-level explanation of how raw cancellable invariants can be used to model iRC11 single-location cancellable invariants. (For purposes of presentation, we abstract away here from certain gory details of the construction-largely inherited from [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF]-that are orthogonal to the goal of supporting safe cancellation.) (iRC11-CInv-Model) The iRC11 cancellable invariant assertion τ ℓ I is nothing more than a raw cancellable invariant (guarded by τ ) whose invariant content is ATOM(ℓ, I), an Iris view-predicate with three parts:

ATOM
(1) The first component of ATOM-History(ℓ, h)-asserts ownership of the entire history h of writes to ℓ. This makes it the owner of location ℓ and enforces that all accesses to ℓ will need to go through the raw cancellable invariant.

(2) The second component of ATOM is the knowledge that the view V i at which the invariant is interpreted contains all message views in ℓ's history. (This means in particular that V i is synchronized with all writes to ℓ.) (3) The third component of ATOM is the invariant content I(m.val) (m.view) for every message m in Frontier(h), i.e., every message corresponding to a write to ℓ that has not been read from by an RMW operation (like FAA). (For messages not in the frontier, ownership of the invariant content may have been transferred away from ATOM by an RMW operation.)

Crucially, the ATOM predicate uses the view V i (at which it is interpreted) exclusively as an upper bound on the message views for the writes to ℓ, a property that is crucial for safe cancellation. The remaining parts of ATOM are either view-agnostic (in the case of History) or they hold at views that end up synchronizing with some component of the thread's local view when a physical memory operation is performed. This allows us to all but ignore V i when accessing the invariant, thus avoiding the apparent problem of how to reason about the view-join modality in Raw-CInv-Acc.

Proving cancellation. Let us now see how to prove iRC11-CInv-Cancel. Suppose we invoke the rule for thread π whose current view is V π . Since we own [τ ] 1 , we can immediately use Raw-CInv-Cancel to cancel the underlying raw invariant, thus reclaiming ownership of ATOM(ℓ, I) (V π ). By the definition of ATOM, we now own the history of writes to ℓ, and we know that V π has seen all writes to ℓ-including the most recent write of value v with message m-so we can assert ℓ → v at thread π 's current view V π . Furthermore, we now also own the invariant interpretation I(v) (m.view), because certainly m is in the frontier of ℓ's history. Since we know that m.view is contained in the thread view V π , we can assert I(v) holds at V π as well. □

Proving access. We now turn to the proof of iRC11-CInv-FAA-Rlx, the iRC11 rule for relaxed FAA operations. Consider an execution of FAA(ℓ, n) in thread π with local views V before and V ′ after the instruction, reading message m r (with value v) and writing message m w (with value v + n). In the proof of iRC11-CInv-FAA-Rlx, we access the raw invariant τ ATOM(ℓ, I) using Raw-CInv-Acc. This gives us ⌊ATOM(ℓ, I)⌋ ⊔V i (V.cur)-i.e., ATOM(ℓ, I) (V.cur ⊔ V i ), for some unknown V i .

As suggested above, the fact that V i is unknown is not actually a problem: as we now explain, the proof of the ownership transfer at the heart of iRC11-CInv-FAA-Rlx does not care about V i at all-it only cares about specific messages and their interpretations.

We start out with P (V.rel) from our precondition and I(v) (m r .view) from ATOM (since m r is in the frontier-it must be so because we are reading from it, which means it could not have been read from by an RMW before). By view monotonicity, we therefore have P * I(v) (V.rel⊔m r .view). Applying the premise of iRC11-CInv-FAA-Rlx to this, we obtain

I(v + n) * Q(v) (V.rel ⊔ m r .view).
From that we need to establish (1) I(v +n) (m w .view) to close the invariant and (2) Q(v) (V ′ .acq) for the postcondition. To justify these steps, it suffices to observe that (i) m w 's message view is precisely V.rel ⊔ m r .view extended to include the new write to ℓ, and (ii) after executing the FAA operation, π 's updated acquire view (V ′ .acq) includes both its original release view (V.rel) and the view of the read message (m r .view). We thus obtain (1) and (2) immediately by view monotonicity.

Notice how the unknown V i did not come up even once in the last paragraph! Indeed, V i is only relevant to the final step where we have to re-establish ATOM at V ′ .cur ⊔ V i which we call V ′ i . The crucial part here lies in showing V ′ i ⊒ m w .view, i.e., making sure that V ′ i is synchronized with the view of the new write message. It is easy to check that V ′ i contains m r .view (through m r .view ⊑ V i ) and V.rel (through V.rel ⊑ V.cur ⊑ V ′ .cur). This leaves the write itself. As an RMW operation, FAA records the new write in the updated view, V ′ .cur. Hence, V ′ i ⊒ m w .view and we can re-establish ATOM at V ′ i . □

OTHER CONTRIBUTIONS

In this paper, we have focused on our central technical contribution of synchronized ghost state. However, RB rlx encompasses a number of other contributions, a few of which we highlight in this section: ORC11's race detector ( §5.1), a model of fence modalities ( §5.2), the verification of Arc and the bug we found in its implementation ( §5.3), and, finally, the adaptation of RustBelt's lifetime logic to RMM ( §5.4).

Data Race Detection in ORC11

ORC11 is the first operational semantics that incorporates a race detector for non-atomic accesses into a language with release-acquire accesses, relaxed accesses, and fences. ORC11's race detector extends the race detector [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF] of relaxed accesses. To explain the necessity of this extension, we first discuss why the approach of [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF] does not scale to relaxed accesses. The iGPS race detector, introduced by [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF] for the release-acquire/non-atomic fragment of C11, is somewhat unusual in that it does not in fact detect all races in every execution. (Recall that, by C11, two accesses to the same location are racy if one of them is non-atomic, one is a write, and there is no happens-before relation between them.) Instead, although iGPS forbids write-before-read races-that is, races where a write is interleaved before a racing read-it allows read-before-write races-where a read is interleaved before a racing write. To illustrate this asymmetry, consider the following example code: X := 0; * X || X := 37

In this program there are two possible interleavings, both of which are considered racy by C11. The iGPS race detector detects a race in the interleaving where the read from X is executed after the write to X , but it does not detect a race in the interleaving where X is read first.

The upside of iGPS's approach is that reads do not need to be tracked by the race detector, which reduces the amount of state in the operational semantics. The downside, of course, is that some races are not detected-a seemingly rather severe problem for a race detector! The reason this is not a problem in iGPS is that Hoare triples imply absence of races for all executions of a program. In order to be able to claim that the iGPS logic ensures absence of data races according to C11, it thus suffices for the race detector in the operational semantics to detect a race on some execution of every program that is racy according to C11. And indeed it does: for programs with only release-acquire and non-atomic accesses (the domain of iGPS), for any execution with a read-before-write race, there is always a differently interleaved execution with a write-before-read race, which iGPS's race detector will detect.

In the presence of relaxed accesses, however, the iGPS race detector is no longer sufficient, because the property mentioned above is no longer true. That is, it is possible to construct programs that have executions in which the read-before-write races happen, but there is no interleaving where the write will be executed before the read. For example, consider the following program: X := 0; Y := 0; * X ; Y := rlx 1 || while ( * rlx Y == 0); X := 37 Here, the non-atomic read in the left thread is guaranteed to be executed before the non-atomic write to X in the right thread, and there is no interleaving where the reverse can happen. The iGPS race detector would not declare this program racy, but the two accesses to X are not related by happens-before and are thus considered a race by C11.

To account for such programs, we extend iGPS's race detector, which already tracked nonatomic writes, to track all access events, including atomic writes, and atomic and non-atomic reads in threads' local views. These events will then be sent across threads when they perform synchronization. The race detector view V Race of the global state ( §2.2) then records, for every location, the latest non-atomic write, a global set of atomic writes, a global set of atomic reads, and a global set of non-atomic reads. When a thread π is performing an access a, depending on the kind of access a, the ORC11 race detector will then require that the thread π must have observed certain events in the global race detector view V Race .

In the example above, the non-atomic read of X by the left thread, when executed, will add a fresh read event ε na into V Race 's set of non-atomic reads for X . The non-atomic write of X by the right thread is guaranteed to be executed after the read by the left thread. However, when the write is executed, the race detector requires that the right thread must have observed in its local view all read events, including ε na , in order to be deemed non-racy. Since the right thread did not synchronize with the left thread to obtain ε na in its local view, its write to X will be declared racy by the ORC11 race detector.

To show a formal correspondence between ORC11 and RC11 [START_REF] Lahav | Repairing sequential consistency in C/C++11[END_REF], we exploit the fact that ORC11 is very close to the "promise-free" fragment of [START_REF] Kang | A Promising Semantics for Relaxedmemory Concurrency[END_REF] extended with non-atomics and a race detector. [START_REF] Kang | A Promising Semantics for Relaxedmemory Concurrency[END_REF] already proved a formal correspondence between their promise-free fragment and C11. Building on their result, we show (on paper) that any racy execution in RC11 can be replayed as a racy execution in ORC11 [START_REF] Dang | Appendix and Coq development accompanying this paper[END_REF]]. The proof is relatively straightforward since ORC11 explicitly tracks read and write events.

The Model of Fence Modalities

In §3.3, we argue that the Ghost-Mod rule is sound without actually giving the model of unsynchronized ghost state nor the fence modalities. While the model of unsynchronized ghost state can be easily given as

a γ (V ) ::= a γ (USGS-Model)
it is rather technically tricky to get a simple and clean model of the fence modalities. In this section we briefly discuss how the model of fence modalities works.

In iGPS, a thread's subjective view is a simple view of type View, and consequently an iGPS assertion is interpreted as a function of type View → iProp. In iRC11, even though a thread's subjective view is a triple of three views, we still managed keep the interpretation • of an iRC11 assertion as simply a function of type View → iProp. That may seem rather suspicious, for as we mentioned in §3.1, the release and acquire views of a thread π are needed to model the release ∆ π and acquire ∇ π modalities, respectively. If • is only a function of type View → iProp, then, assuming that by default the view V supplied to • (V ) is the thread's current view, how can • get access to the release or acquire view that it needs in order to interpret the fence modalities?

To model the fence modalities, we exploit extra ghost state that enables the interpretation • to gain indirect access to the thread π 's physical release view and acquire view:

∆ π P (V ) ::= ∃V rel . RelV(V rel ) π * P (V rel ) (RelMod-Model) ∇ π P (V ) ::= ∃V acq . AcqV(V acq ) π * P (V acq ) (AcqMod-Model)
Here, RelV(V rel ) π and AcqV(V acq ) π are elements of a view-dependent ghost state instance for the thread π . These are governed by a global invariant, which enforces that they always record snapshots of π 's release and acquire views, i.e., V rel ⊑ V.rel and V acq ⊑ V.acq, where V is π 's local view. (For Iris enthusiasts, these are the snapshot elements in the Master-Snapshot monoid.) Thus, ∆ π P (V ) (respectively, ∇ π P (V )), ignoring the view V at which it is being interpreted, states that P holds at some V rel ⊑ V.rel (V acq ⊑ V.acq). By view-monotonicity this means also that P holds at V.rel-the release view of π (respectively, V.acq-the acquire view of π ).

Soundness of Ghost-Mod. With these definitions, it is now clear how Ghost-Mod is sound. For example, the direction "∆ π a γ ⇒ a γ " is trivial after unfolding the model of the release modality.

The direction " a γ ⇒ ∆ π a γ " is also essentially trivial because it is always possible to create a snapshot RelV(V.rel) π of the thread's release view V.rel. □

Verification of Relaxed-Memory Libraries

Adapting RustBelt to ORC11 required us to re-verify all the internally unsafe libraries considered by RustBelt, i.e., to show that these libraries still properly encapsulate their unsafe behaviors within safe interfaces when we consider their real relaxed-memory implementations. RB rlx has ported all verifications done in RustBelt, including the following concurrency libraries: thread::spawn, Arc<T> and Weak<T>. Arc<T> has a sibling library Weak<T> which is also an atomic reference counter. The Weak type, being very similar to Arc, counts how many Weak pointers are in existence, and also comes with its own clone and drop functions. However, while owning an Arc guarantees access to the underlying object of type T, owning a Weak does not prevent the underlying object from being reclaimed. In order to access the object with a Weak pointer, one first calls Weak::upgrade to upgrade the Weak pointer to an Arc pointer. Weak::upgrade can fail when the object has already been reclaimed, that is, when there is no Arc pointer left. A Weak pointer is typically created by calling Arc::downgrade on a shared reference of Arc.

The challenge in verifying Arc and Weak in RMM is that they are implemented together by two tightly coupled atomic locations-one for each counter, and reasoning about the relation between multiple locations in RMM is known to be complicated [START_REF] Turon | GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation[END_REF]]. The interplay of the two counters is further complicated by the library's support for temporarily reclaiming full ownership of the underlying content when the thread knows it owns the last unique Arc and Weak pointers. The functions Arc::get_mut (see Figure 10) and Arc::make_mut provide these capabilities: they return a mutable reference &mut T to the underlying content. The reclamation is temporary because when the reference goes out of scope (when the lifetime of the mutable reference ends), the content is returned and the original Arc pointer can be used again.

In RB rlx , we need to use two separate iRC11 cancellable invariants for each counter. At the same time, we employ both unsynchronized and synchronized ghost state to maintain the intricate relation between the two counters (see the appendix [START_REF] Dang | Appendix and Coq development accompanying this paper[END_REF]] for more details).

Insufficient Synchronization in Arc<T>::get_mut. Unfortunately, our proof setup was not strong enough to verify Arc and Weak without change (although at least partly for good reason!). The read of the Arc counter a.strong in is_unique (used by get_mut, Fig. 10), as well as another read implemented in make_mut for the similar role, were rlx in the original code and we had to strengthen them both to acq in order to make the verification go through. The reason is that, while we managed to temporarily get the full resources out by a read, the rlx reads do not give us those resources at the thread's current view (they are under a ∇ modality). We conjecture that the rlx read in make_mut is in fact sufficient, but the rlx read in get_mut turned out to be insufficient. The bug has been reported and fixed in the Rust codebase [START_REF] Jourdan | Insufficient synchronization in Arc::get_mut[END_REF]].

Fig. 11 shows an example where a data race (according to C11) can arise when using get_mut in otherwise safe code. Here, there are two na operations: the read of the underlying integer in line 3 (child thread) and the write to the same integer in line 6 (parent thread). The read should be safe because the child thread owns arc2 and the underlying integer is shared and immutable. The write should be safe because a successful get_mut gives the parent (who owns arc1) temporary full non-atomic access to the integer. This can only happen after the child thread finishes and arc2 has been drop-ed. However, the two na operations constitute a data race according to C11 because neither one happens-before the other. More specifically, in the child thread, when arc2 goes out of scope it will be destructed by Arc::drop (line 3), which uses a release (rel) FAA (see the code in Fig. 5). This release FAA will be read by get_mut (in the second check of is_unique, Fig. 10) in the parent thread (line 4). If this read had been acq, then there would have been a release-acquire synchronization between drop and get_mut, and the na read of the child thread would have been guaranteed to happen-before the na write of the parent thread. However, the read was rlx, and thus no synchronization can be established between the two na operations.

Adapting the Lifetime Logic to Relaxed Memory

RustBelt's semantic soundness proof for the Rust type system depends on the lifetime logic. The lifetime logic provides so-called borrow propositions, a family of mechanisms similar to raw cancellable invariants (see §4.2) that are instrumental in handling various features required by Rust's type system and by the verification of Rust libraries. Borrow propositions improve on raw cancellable invariants in multiple ways, the most important being that they decouple the assertions used to access the underlying resource from the assertions used to reclaim it. This is achieved by offering three kinds of assertions: borrow propositions (of which there are several different kinds), lifetime tokens (similar to invariant tokens), and an inheritance assertion. Borrow propositions and (fractions of) lifetime tokens are used together to gain temporary access to the underlying resource. Separately, the inheritance assertion can be used together with the full lifetime token to reclaim the contents of the borrow.

These assertions can be owned by different threads and if we were to model them using unsynchronized ghost state we would run into the same problems as in §4.1. (A full counterexample is presented in Section 4 of [START_REF] Dang | Appendix and Coq development accompanying this paper[END_REF].) Thus, we make essential use of synchronized ghost state in the model of lifetime tokens, just as we did for cancellable invariant tokens.

Fortunately, despite this change to the model of the logic, the lifetime logic's proof rules are almost entirely sound in ORC11. The only feature that required changes is atomic borrows (see below). However, atomic borrows are only used in the verification of concurrent libraries and not in the soundness proof of the type system because Rust's type system does not know anything about concurrency. The proof of safety of the λ Rust type system thus did not need to be changed.

Atomic borrows. The lifetime logic offers several kinds of borrow propositions, which represent different ways of managing ownership of resources. Only one of them, atomic borrows, allows shared atomic access to the underlying resource.

SC-LftL-at-Acc {P * Q 1 } e {v. P * Q 2 } atomic(e) & κ at P ⊢ { [κ]

q * Q 1 } e { v. [κ] q * Q 2 } Rlx-LftL-at-Acc ∀V b . { ⌊P⌋ ⊔V b * Q 1 } e { v. ⌊P⌋ ⊔V b * Q 2 } atomic(e) & κ at P ⊢ { [κ] q * Q 1 } e { v.
[κ] q * Q 2 } , Vol. 1, No. 1, Article . Publication date: November .

Under SC, accesses to atomic borrows were automatically synchronized. This is no longer true in RMM. Consequently, we apply the same technique used for raw cancellable invariants to weaken the access rule, providing access to the underlying resource P only under the view-join modality.

Other borrows. The proof rules for other kinds of borrows did not need changing because these borrows always ensure proper synchronization between accesses. As an example, consider full borrows. Full borrows can only ever be owned by one thread and whichever thread owns the full borrow assertion is the only one that can access the underlying resource.

Owing to this exclusiveness, full borrows enjoy a particularly strong access rule shown below. Concretely, LftL-full-acc states that the full borrow assertion & κ full P can be exchanged for the underlying resource P at the thread's view together with a return predicate Ret(κ, P, q), which can then be used to return P in exchange for & κ full P. Note that access to P is not restricted to an atomic step of execution. Instead, P can be returned at any later point by applying LftL-full-ret.

LftL-full-acc & κ full P * [κ] q P * Ret(κ, P, q)

LftL-full-ret P * Ret(κ, P, q) & κ full P * [κ] q To establish the soundness of these proof rules, we require an additional instance of synchronized ghost state on top of the synchronized ghost state used for lifetime tokens. The purpose of this extra ghost state is to maintain that that all accesses to the borrowed content P are fully synchronized. In particular, under the hood, P is held in an invariant at a content view V i together with a piece of ghost state that records V i . The borrow assertion & κ full P carries its own synchronized ghost state as well, satisfying the invariant that the view V of the thread that owns & κ full P must include the view V i of the borrowed content. This allows us to deduce that it is safe for the thread that owns & κ full P to gain access to P at its own local view, as required to prove soundness of LftL-full-acc.

RELATED AND FUTURE WORK

Program logics and verifications. [START_REF] He | GPS+: Reasoning About Fences and Relaxed Atomics[END_REF] present GPS+, a extension to GPS that supports relaxed accesses and release/acquire fences. However, their logic lacks support for relaxed CAS/FAA operations which Arc uses. Additionally, their logic is based on the axiomatic semantics of C11 which cannot be used together with Iris and thus would not allow us to extend the existing RustBelt development. GPS+ also does not support mechanized verification of programs.

iGPS [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF]] supports a mechanism called fractional protocols, which is closely related to cancellable invariants. However, iGPS's fractional protocols are not as powerful as iRC11's cancellable invariants in that they cannot reclaim the resources governed by the protocol at the thread's local view. This is because the protocol tokens they use are modeled with unsynchronized ghost state. By using synchronized ghost state, we can support full reclamation of all resources governed by either iRC11 cancellable invariants or borrow propositions. [START_REF] Tassarotti | Verifying read-copy-update in a logic for weak memory[END_REF]] use GPS to verify an implementation of the Read-Copy-Update (RCU) technique. With GPS, they are able verify the reclamation of clients' non-atomic locations, but not RCU's internal atomic locations because they are governed by GPS's non-cancellable protocols. [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris[END_REF] fixed this problem by re-verifying RCU in iGPS with their fractional protocols. However, as mentioned above, fractional procotols are not a general solution. [START_REF] Gotsman | Local Reasoning for Storable Locks and Threads[END_REF] provide an SC-based logic where ownership of a location can be turned into a lock with fractional permissions for shared accesses, and later when the full permission of the lock is collected, the ownership of the location can be reclaimed. [START_REF] Hobor | Oracle Semantics for Concurrent Separation Logic[END_REF] provide a similar mechanism that additionally allows attaching "invariant resources" to locks. Our cancellable invariants are more general than these mechanisms in that our cancellable invariants are not specifically tied to locks and are proven sound with respect to a much weaker memory model. [START_REF] Doko | Tackling Real-Life Relaxed Concurrency with FSL++[END_REF] verify a subset of the Arc library with FSL++. We improve on their results by (1) enlarging the scope of the verification to include important parts of the API such as the make_mut and get_mut functions (the latter of which we found to contain a data race) as well as the Weak reference type, (2) allowing full resource reclamation of both the contents and the reference-count fields of the Arc data structure, and (3) embedding our verification effort in the RustBelt framework, so that we can establish the soundness of Arc when linked with unknown well-typed λ Rust code.

Operational semantics for relaxed memory. [START_REF] Podkopaev | Operational Aspects of C/C++ Concurrency[END_REF] develop an operational account of a subset of C11 that includes relaxed accesses and non-atomics. However, it lacks support for fences and thus could not be used as is (to build a logic) to verify Arc. Their semantics also does not forbid the data race in Section 5.1. [START_REF] Doherty | Verifying C11 Programs Operationally[END_REF] develop an operational semantics based on event graphs for the release/acquire/relaxed fragment of RC11. They also develop an invariant-based logic geared towards automated verification for programs in that fragment. As their operational semantics supports neither non-atomics nor fences, it is not expressive enough to handle the Rust libraries targeted by RB rlx .

Kang et al. 's promising semantics [START_REF] Kang | A Promising Semantics for Relaxedmemory Concurrency[END_REF]] is a proposal for fixing C11's out-of-thin-air problem without prohibiting load-store reordering on relaxed accesses (as RC11 and ORC11 do). [START_REF] Kasper Svendsen | A Separation Logic for a Promising Semantics[END_REF] introduce the first program logic for the promising semantics. Their logic is based on RSL [START_REF] Vafeaidis | Relaxed Separation Logic: A Program Logic for C11 Concurrency[END_REF] and supports relaxed accesses but not fences. Moreover, unlike FSL, it disallows the transfer of ownership through relaxed accesses, among other reasoning principles that have proven useful in RB rlx . Extending RB rlx to account for promises is a very interesting avenue for future work.

Finally, it is worth re-iterating that ORC11 and iRC11 currently do not support SC accesses and SC fences. In fact, we are not aware of any existing RMM separation logic that does. 6 Adding support for SC would enable us to verify some interesting and challenging fine-grained concurrent algorithms, such as the work-stealing queue by [START_REF] Chase | Dynamic circular work-stealing deque[END_REF], as well as epoch-based resource reclamation schemes such as that implemented by Rust's crossbeam library [START_REF] Turon | Crossbeam: Support for concurrent and parallel programming[END_REF]].

,

  Vol. 1, No. 1, Article . Publication date: November .

  Fig. 2. Message-Passing example in RMM.

AccessMode

  ∋ o ::= na | rlx | acq | rel Expression ∋ e ::= . . . | rec f (x) := e | fork { e } | alloc(e) | free(e 1 , e 2 ) | . . . | * o e | e 1 := o e 2 | CAS o f ,o r ,o w (e 0 , e 1 , e 2 ) | FAA o r ,o w (e 1 , e 2 ) | fence o | . . .

Fig. 4 .

 4 Fig. 4. iRC11 demonstrated with Message-Passing example verifications.

,

  Vol. 1, No. 1, Article . Publication date: November .

Fig. 5 .

 5 Fig. 5. Implementation of Core Arc.

Fig. 9 .

 9 Fig. 9. Proof outline of Raw-CInv-Acc (at Iris level).

  (ℓ, I) (V i ) ::= ∃h. History(ℓ, h) * (∀m ∈ h. m.view ⊑ V i ) * * m ∈Frontier(h) I(m.val) (m.view) * . . . τ ℓ I ::= τ ATOM(ℓ, I)

  Fig. 10. The implementation of Arc::get_mut.

,

  Fig. 11. Example demonstrating the bug we found in Arc.

  developed for iGPS, in order to address the extra effects

, Vol. 1, No. 1, Article . Publication date: November .

, Vol. 1, No. 1, Article . Publication date: November .

iGPS supports a related notion of "fractional protocol", but as we explain in §6, it is not nearly as powerful as cancellable invariants and is thus not general enough to account for resource reclamation in Rust., Vol. 1, No. 1, Article . Publication date: November .

Caveat: ORC11 omits SC accesses and fences because (1) they are not used by any of the libraries verified in RustBelt, and (2) it is still an open question how to develop a separation logic for reasoning about SC accesses in a relaxed-memory setting. See §6 for further details. , Vol. 1, No. 1, Article . Publication date: November .

We could instead use a pair of release write and acquire read accesses. We use fences for the sake of exposition., Vol. 1, No. 1, Article . Publication date: November .

Note: Throughout this paper, to simplify the presentation, we elide certain "administrative" details of proof rules concerning invariant namespaces and the "later" (▷) modality. Invariant namespaces are present to ensure that we do not attempt to access invariants twice in a nested fashion. The ▷ modality is necessary to ensure soundness in the presence of impredicative invariants. We elide these details because they are completely standard in Iris developments, and do not interact interestingly with the RMM features. We refer the reader toJung et al. [2018b] for details. , Vol. 1, No. 1, Article . Publication date: November .

In Iris parlance, atomic instructions are expressions that evaluate in just one step. This is not to be confused with the notion of relaxed-memory atomic accesses, even though atomic accesses are indeed atomic instructions., Vol. 1, No. 1, Article . Publication date: November .

The abstract of the RSL paper[START_REF] Vafeaidis | Relaxed Separation Logic: A Program Logic for C11 Concurrency[END_REF] claims that it supports reasoning about SC accesses, but according to Vafeiadis [personal communication], this is a mistake, and indeed the body of the paper does not., Vol. 1, No. 1, Article . Publication date: November .

ACKNOWLEDGMENTS

We would like to thank Jeehoon Kang, Ori Lahav, and Viktor Vafeiadis for their suggestions on building the race detector of ORC11. We would also like to thank Ralf Jung and Robbert Krebbers for various discussions on the original RustBelt development, as well as for their maintanance effort on both Iris and RB rlx . Finally, we would like to thank the anonymous reviewers from both PLDI 2019 and POPL 2020 for their constructive suggestions concerning presentation.

This research was supported in part by a European Research Council (ERC) Consolidator Grant for the project "RustBelt", funded under the European Union's Horizon 2020 Framework Programme (grant agreement no. 683289).