Glen Mével
email: glen.mevel@inria.fr

Jacques-Henri Jourdan
email: jacques-henri.jourdan@universite-paris-saclay.fr.

Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model

Keywords: CCS Concepts:, Theory of computation → Separation logic, Program verification, Program specifications separation logic, program verification, concurrency, weak memory, concurrent queue

We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.

INTRODUCTION

Advances in multicore hardware during the last two decades have created a need for powerful tools for writing efficient and trustworthy multicore software. These tools include well-designed programming languages and their compilers, efficient thread-safe libraries, and expressive program logics for proving the correctness of these and of the applications that exploit them. While some such verification tools already exist, researchers are only beginning to explore whether and how these tools can be exploited to modularly specify and verify realistic libraries that support fine-grained shared-memory concurrency.

Most of the programming languages that support multicore programming present shared memory as the primitive means of communication between threads. Although this design choice offers the greatest flexibility for writing efficient programs, it comes at an important cost: in order to achieve maximal efficiency, shared-memory concurrency cannot follow an intuitive sequentially consistent semantics [START_REF] Lamport | How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs[END_REF], where all threads have the same view of memory at every time. Instead, these programming languages usually come with a subtle weak memory model, which defines precisely how the memory accesses performed by different threads may interact and does not offer a wide variety of concurrent data structures yet, its ecosystem may benefit from this new library. We take inspiration from a well-established algorithm [START_REF] Rigtorp | MPMCQueue[END_REF]] that has been used in production in several applications.

• The specification of the concurrent queue should indicate that it behaves as if all of its operations acted atomically on a common shared state, even though in reality they access distinct parts of the memory and require many machine instructions. To address this challenge, we use the recently-developed concept of logical atomicity [START_REF] Jung | Iris: monoids and invariants as an orthogonal basis for concurrent reasoning[END_REF][START_REF] Jung | Logical Atomicity in Iris: the Good, the Bad, and the Ugly[END_REF][START_REF] Da | TaDA: A logic for time and data abstraction[END_REF]], which we transport to the setting of Cosmo. • To the best of our knowledge, this is the first use of logical atomicity in a weak-memory setting. This raises new questions: for instance, even though our implementation realizes a total order on the operations on a queue, it offers strictly weaker guarantees than would be offered by a coarse-grained implementation. Indeed, in the context of a weak memory model, the specification of a concurrent data structure must describe not only the result of its operations, but also the manner in which these are synchronized, that is, the happens-before relationships that exist between these. This additional information allows reasoning about accesses to areas of memory outside of the data structure itself. This is crucial, for example, if a queue is used to transfer the ownership of a piece of memory from a producer to a consumer: there must exist a happens-before relationship between the enqueue operation and the corresponding dequeue operation, so as to ensure that the consumer acquires the producer's view of this piece of memory. Our specification faithfully captures a subtle behavior of the implementation: even though operations are totally ordered by logical atomicity, not all operations are ordered by happens-before-but some are. • We use the Coq proof assistant [The Coq development team 2020] to formally verify our proofs. Our development is available from our repository [START_REF] Mével | Coq proofs for Cosmo and examples[END_REF]].

We believe our approach, whose key ingredients are Cosmo and logical atomicity, scales to other memory models and other data structures. Indeed, first, the core of Cosmo (beyond basic Separation Logic) is a logic for reasoning with views, an operational description of the memory model; other memory models than that of Multicore OCaml can also be termed in this fashion, as iGPS [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris[END_REF]] and iRC11 [START_REF] Dang | RustBelt meets relaxed memory[END_REF]] have demonstrated for C11. Second, logical atomicity has already successfully been used for various data structures in the Iris community [Iris developers and contributors 2021;[START_REF] Frumin | ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity[END_REF].

The paper begins with a detailed explanation of the specification of a concurrent queue ( §2). Then, we present an implementation of the queue in Multicore OCaml ( §3), and explain our proof of its correctness ( §4). Next, we demonstrate that our specification is indeed usable, by exploiting it in the context of a simple piece of client code, where the concurrent queue is used to establish a pipeline between a set of producers and a set of consumers ( §5). The paper ends with a review of the related work ( §6).

SPECIFICATION OF A MPMC QUEUE IN A CONCURRENT SEPARATION LOGIC

A queue is a first-in first-out container data structure. At any time, it holds an ordered list of items. It supports two main operations: enqueue inserts an item at one extremity of the queue (the head); dequeue extracts an item-if there is one-from the other extremity (the tail).

In a concurrent setting, a legitimate question is whether several threads can operate the queue safely. The answer depends on the implementation. Possible restrictions include allowing only one thread to enqueue (single producer), or allowing only one thread to dequeue (single consumer), or both. In this paper we study an implementation of a multiple-producer, multiple-consumer (MPMC) queue, that is, a queue in which any number of threads are allowed to enqueue and dequeue.

{ True } make ()

{ 𝜆𝑞. IsQueue 𝑞 [] }
{ IsQueue 𝑞 [𝑣 0 , ..., 𝑣 𝑛-1 ] } enqueue 𝑞 𝑣 { 𝜆(). IsQueue 𝑞 [𝑣 0 , ..., 𝑣 𝑛-1 , 𝑣] } { IsQueue 𝑞 [𝑣 0 , ..., 𝑣 𝑛-1 ] } dequeue 𝑞 { 𝜆𝑣. 1 ≤ 𝑛 * 𝑣 = 𝑣 0 * IsQueue 𝑞 [𝑣 1 , ..., 𝑣 𝑛-1 ] } Fig. 1. A specification of the "queue" data structure in a sequential setting

In addition, this queue is bounded, that is, it occupies no more than a fixed memory size. A motivation for that trait is that items may be enqueued more frequently than they are dequeued; in this situation, a bounded queue has no risk of exhausting system memory; instead, if the maximum size is reached, enqueuing either blocks or fails.

Specification in a Sequential Setting

Let us start by assuming a sequential setting. We can then use standard Separation Logic [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF]] to reason about programs and the resources they manipulate. In Separation Logic, a queue 𝑞 holding 𝑛 items [𝑣 0 , ..., 𝑣 𝑛-1 ], where the left extremity of the list is the tail and the right extremity is the head, can be represented with an assertion:

IsQueue 𝑞 [𝑣 0 , ..., 𝑣 𝑛-1 ]

As is usual in Separation Logic, this representation predicate asserts the unique ownership of the entire data structure. When holding it, we can safely manipulate the queue without risk of invalidating other assertions about resources that may alias parts of our queue. In particular, the representation predicate cannot be duplicated; we say that it is exclusive.

The operations of the queue admit a simple sequential specification which is presented in Figure 1. We use the standard Hoare triple notation, with a partial correctness meaning. The asterisk ( * ) is the separating conjunction.

• The function make has no prerequisite and gives us the ownership of a new empty queue.

• If we own a queue 𝑞, then we can enqueue some item 𝑣 into 𝑞; if this operation ever returns, then it must return the unit value () and give us back the ownership of 𝑞, where 𝑣 has been appended at the head. • Conversely, if we own a queue 𝑞, then we can dequeue from 𝑞; if this operation ever returns, then it must return the first item 𝑣 0 found at the tail of 𝑞, and it gives us back the ownership of 𝑞, where that first item has been removed. This specification implies that dequeue cannot possibly return when the queue is empty (𝑛 = 0); in this case, it must loop forever. This is pointless in a sequential setting, but becomes meaningful in the presence of concurrency, where it makes sense for dequeue to wait until an item is enqueued. This specification also applies to bounded queues, where (somewhat analogously) enqueue loops when the capacity is reached (𝑛 = 𝐶), waiting until room becomes available.

Specification under Sequential Consistency

We now consider a situation where several threads can access the queue concurrently. Let us assume for now that the memory model is sequentially consistent [START_REF] Lamport | How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs[END_REF]]. In a seminal

{ 𝜆𝑞. ∃𝛾 . QueueInv 𝑞 𝛾 * IsQueue 𝛾 [] } QueueInv 𝑞 𝛾 ⟨ 𝑛, 𝑣 0 , ..., 𝑣 𝑛-1 . IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 ] ⟩ enqueue 𝑞 𝑣 ⟨ 𝜆(). IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 , 𝑣] ⟩ QueueInv 𝑞 𝛾 ⟨ 𝑛, 𝑣 0 , ..., 𝑣 𝑛-1 . IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 ] ⟩ dequeue 𝑞 ⟨ 𝜆𝑣. 1 ≤ 𝑛 * 𝑣 = 𝑣 0 * IsQueue 𝛾 [𝑣 1 , ..., 𝑣 𝑛-1 ] ⟩ Fig. 2.
A specification of the "queue" data structure in a sequentially consistent memory model work, [START_REF] Stephen | A Semantics for Concurrent Separation Logic[END_REF][START_REF] O'hearn | Resources, Concurrency and Local Reasoning[END_REF] devised Concurrent Separation Logic, an extension of Separation Logic which enables to reason about programs where several threads can access a same piece of memory. Though the original logic achieves sharing through hard-wired "conditional critical regions", it has spawned a variety of descendants lifting this limitation and pushing further the applicability of such separation logics. In this work, we use Iris [START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF]], a modular framework for building separation logics.

In a derivative of Concurrent Separation Logic, we may retain the exact same specification as is presented in Figure 1, recalling that IsQueue 𝑞 [𝑣 0 , ..., 𝑣 𝑛-1 ] is an exclusive assertion: a thread that has this assertion can safely assume to be the only one allowed to operate on the queue. A client application can transfer this assertion between threads via some means of synchronization: for instance, it may use a lock to guard all operations on the shared queue, following the approach of Concurrent Separation Logic. However this coarse grain concurrency has a run-time penalty, and it also creates some contention on the use of the queue. These costs are often unnecessary, as many data structures are designed specifically to support concurrent accesses. In this paper, as stated, we wish to prove the correctness of a MPMC queue implementation, which should thus ensure, by itself, thread safety. Hence we can achieve finer-grain concurrency, where operating on a queue does not require its exclusive ownership.

In this context, another option is for the client to share this ownership among several threads, logically. In an Iris-like logic, one would typically place the exclusive ownership in an invariant. An invariant is an assertion which is agreed upon by all threads, and is owned by anyone; it remains true forever. As the public state of the queue-the list [𝑣 0 , ..., 𝑣 𝑛-1 ] of currently stored items-would only be known from that invariant, the client would also express in there the properties about this state that their particular application needs. Then, when one of the threads needs to access the shared resource, it can open the invariant, get the assertions it contains, perform the desired operation on the shared state, reestablish the invariant, and finally close it. However, to ensure soundness in the face of concurrency, the use of invariants in Iris obeys a strict constraint: they can remain open during at most one step of execution. Unfortunately, enqueue and dequeue are complex operations which, a priori, take several steps. Hence a client would be unable to open their invariant around the triples shown in Figure 1. Yet these operations are "atomic" in some empirical sense.

The concept of logical atomicity [START_REF] Jacobs | Expressive modular fine-grained concurrency specification[END_REF][START_REF] Jung | Logical Atomicity in Iris: the Good, the Bad, and the Ugly[END_REF]Jung et al. 2015, §7] aims at addressing that difficulty. To use it, we substitute ordinary Hoare triples with logically atomic triples. Two important reasoning rules for logically atomic triples are given in Figure 3.1 A logically atomic triple is denoted with angle brackets ⟨. . .⟩. Just like an ordinary triple, it specifies a program fragment with a precondition and a postcondition. In fact, as witnessed by rule LAHoare, one can deduce an ordinary Hoare triple from a logically atomic triple. The core difference is that, thanks to rule LAInv, invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic. The definition of logically atomic triples is further discussed in §4.6 and given with detail in previous work [START_REF] Jung | Logical Atomicity in Iris: the Good, the Bad, and the Ugly[END_REF]Jung et al. 2015, §7]. We now try to give an intuition of that concept: a logically atomic triple ⟨𝑃⟩ 𝑒 ⟨𝑄⟩ states, roughly, that the expression 𝑒 contains an atomic instruction, called the commit point, which has 𝑃 as a precondition and 𝑄 as a postcondition. Because it is atomic, invariants can be opened around that commit point.

Using logically atomic triples, the specification can be written as shown in Figure 2. It closely resembles that of the sequential setting (Figure 1). The first noticeable difference is the use of angle brackets ⟨. . .⟩ denoting logically atomic triples instead of curly brackets {. . .} for ordinary Hoare triples.

Another difference is the presence, in the syntax of logically atomic triples, of an explicit binder for some variables (𝑛, 𝑣 0 , ..., 𝑣 𝑛-1 ). This binder addresses a subtlety of logical atomicity: a client calling enqueue or dequeue does not know in advance the state of the queue at the commit point, which is when the precondition and postcondition are to be interpreted. Hence, both formulas have to be parameterized by said shared state. Said otherwise, a logically atomic triple provides a family of pre/postcondition pairs covering every possible shared state at the commit point.

The last departure from the sequential specification is that the representation predicate is split into two parts: a persistent2 assertion QueueInv 𝑞 𝛾 and an exclusive assertion IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 ], connected by a ghost name3 𝛾. That splitting is an artifact of our correctness proof technique, which we detail in §4. Note that this does not complicate the use of the queue by the client: both assertions are produced when creating the queue, and while the exclusive component can be put in an invariant as before, the persistent component can be directly duplicated and distributed to all threads. 4The use of such a specification in a concrete example will be detailed in §5.3. For now, we illustrate how a weaker specification can be easily deduced from this one.

A persistent specification. If it were not for logical atomicity, and we still wanted to share the ownership of the queue, we would have little choice left than renouncing to an exclusive representation predicate. Only a persistent assertion would be provided, because the description of the public state has to be stable in the face of interference by other threads. The resulting specification would be much weaker. For example, we may merely specify that all of the elements stored in the queue satisfy some predicate Φ. In doing so, we lose most structural properties of a queue: the same specification could also describe a stack or a bag.

persistent(QueuePersistent 𝑞 Φ) QueuePersistent 𝑞 Φ {Φ 𝑣 } enqueue 𝑞 𝑣 {𝜆(). True} QueuePersistent 𝑞 Φ {True} dequeue 𝑞 {𝜆𝑣. Φ 𝑣 }
To derive these Hoare triples from the ones of Figure 2, one simply defines the persistent assertion as follows, where the boxed assertion is an Iris invariant:

QueuePersistent 𝑞 Φ ≜ ∃𝛾 . * QueueInv 𝑞 𝛾 ∃𝑛, 𝑣 0 , ..., 𝑣 𝑛-1 . IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 ] * Φ 𝑣 0 * • • • * Φ 𝑣 𝑛-1
This assertion is trivial to produce at the creation of the queue, when make hands us the assertions QueueInv 𝑞 𝛾 and IsQueue 𝛾 []. Then, for proving the weaker specification of enqueue and dequeue, one opens the invariant around the associated logically atomic triples.

Specification under Weak Memory

Up to now, we have ignored the weakly consistent behavior of the semantics of Multicore OCaml. In this section, we take this aspect into account and propose a refined specification.

We use the separation logic Cosmo [START_REF] Mével | Cosmo: A Concurrent Separation Logic for Multicore OCaml[END_REF], which provides a proof framework for the weak memory model of Multicore OCaml. This memory model has been described by [START_REF] Stephen Dolan | Bounding data races in space and time[END_REF] under the form of a small-step operational semantics. Following previous authors, such as [START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris[END_REF], the semantics features a notion of view5 which captures the essence of weak memory, namely, the fact that each thread has different knowledge of the state of the shared memory. A view represents this subjective knowledge. Cosmo builds on this operational semantics, and brings views to the level of the program logic. All assertions of the logic depend on an ambient view, which corresponds to the current view of the subject thread. Thus, Cosmo assertions are in general subjective, that is, implicitly dependent on an ambient view.

Because Cosmo is based on Iris, logically atomic triples can also be defined in Cosmo. In fact, the specification shown in Figure 2 still applies.

Yet, as such, it is of little value in a weakly consistent context. Indeed, as explained in §2.2, it is designed so that IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 ] can be shared among threads by means of an invariant. But, in Cosmo, invariants are restricted to a special class of assertions called objective assertionsthose assertions that do not actually depend on the ambient view. Hence, our first addition to the specification is to stipulate that the representation predicate is objective. This reflects the fact that there exists a total order on the updates to the logical state, on which all threads objectively agree.

Even with this addition, the specification given in §2.2 is not precise enough to verify interesting clients such as the one described in §5. Indeed, in a weakly consistent setting, one typically expects a concurrent data structure to establish synchronization between some of its concurrent accesses. For example, imagine that thread 𝐴 enqueues a pointer to a complex data structure (say, a hash table). Then, when thread 𝐵 dequeues this pointer, 𝐵 should obtain the unique ownership of the hash table and be able to access it accordingly. In a weakly consistent memory model, 𝐵 expects to see all of the changes that 𝐴 has made to the data structure. This is guaranteed only if there is a happens-before relationship from the enqueuing event to the dequeuing event.

66:8

Glen Mével and Jacques-Henri Jourdan One possibility would be to guarantee that our concurrent queue implementation behaves like its coarse-grained alternative, that is, a sequential implementation guarded by a lock. This would correspond to an intuitive definition of linearizability, even though this notion is difficult to define precisely outside of the world of sequential consistency [START_REF] Smith | Linearizability on hardware weak memory models[END_REF]]. However, our concurrent queue library is weaker than that: it does guarantee some happens-before relationships, but not between all pairs of accesses. Namely, it guarantees a happens-before relationship:

Seen-Zero ⊢ ↑ ⊥ Seen-Two ↑ V 1 * ↑ V 2 ⊣⊢ ↑(V 1 ⊔ V 2 ) Split-Subjective-Objective 𝑃 ⊣⊢ ∃V. (↑ V * 𝑃 @ V) Fig. 4. Selected Cosmo rules persistent(QueueInv𝑞𝛾) objective(IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )]) { ↑V 0 } make () { 𝜆𝑞. ∃𝛾 . QueueInv𝑞𝛾 * IsQueue𝛾 V 0 V 0 [] } QueueInv𝑞𝛾 ⟨ T ,H,𝑛,(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 ). IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * ↑V ⟩ enqueue 𝑞 𝑣 ⟨ 𝜆(). IsQueue𝛾 T (H ⊔V) [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 ),(𝑣,V)] * ↑H ⟩ QueueInv𝑞𝛾 ⟨ T ,H,𝑛,(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 ). IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * ↑V ⟩ dequeue 𝑞 ⟨ 𝜆𝑣 . IsQueue𝛾 (T ⊔V) H [(𝑣 1 ,V 1 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * ↑T * ↑V 0 * 1 ≤ 𝑛 * 𝑣 =𝑣 0⟩ QueueInv𝑞𝛾 ⟨ T ,H,𝑛,(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 ). IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * ↑V ⟩ try_enqueue 𝑞 𝑣 ⟨ 𝜆𝑏. ∨ IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * 𝑏 = false IsQueue𝛾 T (H ⊔V) [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 ),(𝑣,V)] * ↑H * 𝑏 = true ⟩ QueueInv𝑞𝛾 ⟨ T ,H,𝑛,(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 ). IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * ↑V ⟩ try_dequeue 𝑞 ⟨ 𝜆𝑣 ? . ∨ IsQueue𝛾 T H [(𝑣 0 ,V 0 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * 𝑣 ? = None IsQueue𝛾 (T ⊔V) H [(𝑣 1 ,V 1 ),...,(𝑣 𝑛-1 ,V 𝑛-1 )] * ↑T * ↑V 0 * 1 ≤ 𝑛 * 𝑣 ? = Some𝑣 0 ⟩ Fig. 5. A
(1) from an enqueuer to the dequeuer that obtains the corresponding item;

(2) from an enqueuer to the following enqueuers;

(3) from a dequeuer to the following dequeuers. The first one permits resource transfer through the queue as described in the example above.

In Cosmo, happens-before relationships can be expressed as transfers of views. To the user of this logic, views (denoted in this paper by calligraphic capital letters, such as T , H, V, S) are abstract values equipped with lattice structure: the least view ⊥ is the empty view, and larger views correspond to more recent knowledge. Cosmo features two kinds of assertions to deal with views. First, if V is a view, then the persistent assertion ↑ V indicates that the current thread has the knowledge contained in V. Second, if V is a view and 𝑃 is a (subjective) assertion, then 𝑃 @ V denotes the assertion 𝑃 where V has been substituted for the ambient view; as it does not depend on the ambient view anymore, 𝑃 @ V is objective. 6 Cosmo provides reasoning rules about these assertions, shown in Figure 4. We comment on rule Split-Subjective-Objective in the next paragraph.

In Cosmo, the usual way of specifying a happens-before relationship between two program points is by giving the client the ability to transfer any assertion of the form ↑ V between these two points: this corresponds to saying that the destination program point has all the knowledge the source program point had about the shared memory. As seen later with the example of the pipeline ( §5.3), this is sufficient for transferring any subjective resource from a sender to a receiver. Indeed, rule Split-Subjective-Objective says that we can split any subjective assertion 𝑃 into two assertions ↑ V and 𝑃 @ V for some view V and, conversely, we can reconstruct 𝑃 from two such assertions. The second part being objective, it can be shared in an invariant. Hence, to transfer 𝑃, it is enough to transfer its subjective part ↑ V.

In the specification of the queue, to express the happens-before relationships mentioned earlier, the representation predicate now takes more parameters:

IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )]
(1) For each item 𝑣 𝑘 in the queue, we now have a corresponding view V 𝑘 . This view materializes the flow of memory knowledge from the thread which enqueued the item, to the one which will dequeue it.

(2) The head view H materializes memory knowledge accumulated by successive enqueuers.

(3) The tail view T materializes memory knowledge accumulated by successive dequeuers. The queue that we study, however, does not guarantee any happens-before relationship from a dequeuer to an enqueuer. 7 Hence, it provides fewer guarantees than a sequential queue guarded by a lock.

Interestingly, Cosmo is able to express this subtle difference between the behavior of our library and that of a lock-based implementation: the full specification under weak memory is shown

𝑥 ∈ Var -variables ℓ ∈ Loc -memory locations 𝑏 ∈ {false, true} -Boolean values 𝑛 ∈ Z -integer values 𝑣 ::= 𝜇 𝑓 . 𝜆 𝑥 . 𝑒 | ℓ | () | 𝑏 | 𝑛 -values | None | Some 𝑣 | (𝑣, . . . , 𝑣) ⊙ ∈ {∧, ∨, +, ×, mod, . . . } -operators 𝑒 ::= -expressions: 𝑥 | 𝜇 𝑓 . 𝜆 𝑥 . 𝑒 | 𝑒 𝑒 | 𝑒 ⊙ 𝑒 -𝜆-calculus with recursive functions | ℓ | () | 𝑏 | 𝑛 | None | Some 𝑒 | (𝑒, . . . , 𝑒)
-primitive values and constructors

| if 𝑒 then 𝑒 else 𝑒 -conditional | match 𝑒 with Some 𝑥 → 𝑒 | None → 𝑒 -pattern matching | let (𝑥, . . . , 𝑥) = 𝑒 in 𝑒 -tuples | fork 𝑒 -spawning a new thread | array na [𝑒] 𝑒 | 𝑒 [𝑒] na | 𝑒 [𝑒] na ← 𝑒 -non-atomic cells | array at [𝑒] 𝑒 | 𝑒 [𝑒] at | 𝑒 [𝑒] at ← 𝑒 -atomic cells | CAS 𝑒 [𝑒] 𝑒 𝑒
-atomic compare-and-set 𝑒 ::= . . .

-syntactic sugar: (1) When a thread with a local view V (in other words, with ↑ V as a precondition) enqueues an item 𝑣, it pairs it with the view V. Afterwards, when another thread dequeues that same item 𝑣 0 , it merges the view V 0 that was paired with it into its own local view (in other words, it obtains ↑ V 0 as a postcondition).

| let rec 𝑥 𝑥 . . . 𝑥 = 𝑒 in 𝑒 -definitions of recursive functions | let 𝑥 . . . 𝑥 = 𝑒 in 𝑒 | 𝑒 ; 𝑒 -definitions, sequencing | for 𝑥 from 𝑒 to 𝑒 do 𝑒 done -loops | ref na 𝑒 | ! na 𝑒 | 𝑒 na 𝑒 -non-atomic references | ref at 𝑒 | ! at 𝑒 | 𝑒 at 𝑒 | CAS 𝑒 𝑒 𝑒 -atomic references
(2) When a thread enqueues an item, it also obtains the head view H left by the previous enqueuer (in other words, it obtains ↑ H as a postcondition), and it adds its own view V to the head view (which becomes H ⊔ V).

(3) When a thread dequeues an item, it also obtains the tail view T left by the previous dequeuer (in other words, it obtains ↑ T as a postcondition), and it adds its own view V to the tail view (which becomes T ⊔ V).

IMPLEMENTATION OF A BOUNDED MPMC QUEUE USING A RING BUFFER

We now present an implementation of a bounded MPMC queue, that satisfies the specification devised in §2. For the purpose of the formalization, it is written in an idealized version of the Multicore OCaml language which we introduce in §3.1, before showing the code ( §3.2, §3.3) and giving intuitions about its mode of operation ( §3.4, §3.5).

{

ℓ [𝑘] na 𝑣 } ℓ [𝑘] na { 𝜆𝑣 ′ . 𝑣 ′ = 𝑣 * ℓ [𝑘] na 𝑣 } { ℓ [𝑘] na _ } ℓ [𝑘] na ← 𝑣 { 𝜆(). ℓ [𝑘] na 𝑣 } { ℓ [𝑘] at ⟨𝑣, V⟩ } ℓ [𝑘] at { 𝜆𝑣 ′ . 𝑣 ′ = 𝑣 * ℓ [𝑘] at ⟨𝑣, V⟩ * ↑ V } { ℓ [𝑘] at ⟨_, V⟩ * ↑ V ′ } ℓ [𝑘] at ← 𝑣 { 𝜆(). ℓ [𝑘] at ⟨𝑣, V ⊔ V ′ ⟩ } { 𝑣 0 ≠ 𝑣 1 * ℓ [𝑘] at ⟨𝑣 0 , V⟩ } CAS ℓ [𝑘] 𝑣 1 𝑣 2 { 𝜆𝑣 ′ . *        𝑣 ′ = false ℓ [𝑘] at ⟨𝑣 0 , V⟩ ↑ V } { ℓ [𝑘] at ⟨𝑣 1 , V⟩ * ↑ V ′ } CAS ℓ [𝑘] 𝑣 1 𝑣 2 { 𝜆𝑣 ′ . *        𝑣 ′ = true ℓ [𝑘] at ⟨𝑣 2 , V ⊔ V ′ ⟩ ↑ V } Fig. 7
. Simplified Cosmo triples for the memory operations of Multicore OCaml

Multicore OCaml

The syntax of our idealized version of Multicore OCaml is presented in Figure 6. It is untyped (contrary to the actual Multicore OCaml language) and equipped with a standard call-by-value, left-to-right evaluation. The parts of interest are the memory operations. Their semantics have been described by [START_REF] Mével | Cosmo: A Concurrent Separation Logic for Multicore OCaml[END_REF]; however, in the present paper, each location stores an array of values, whose cells act as independent memory cells with respect to the memory model. Cells are rigidly ascribed an access mode 𝛼, which is either "atomic" (𝛼 = at) or "non-atomic" (𝛼 = na). When 0 ≤ 𝑛, the expression array 𝛼 [𝑛] 𝑣 allocates a block of 𝑛 cells whose access mode is 𝛼 and whose initial value is 𝑣. Reading from a cell with access mode 𝛼 at offset 𝑘 of location ℓ is written ℓ [𝑘] 𝛼 . Writing a value 𝑣 to a cell with access mode 𝛼 at offset 𝑘 of location ℓ is written ℓ [𝑘] 𝛼 ← 𝑣.

In addition, atomic cells support the usual compare-and-set operation: CAS ℓ [𝑘] 𝑣 1 𝑣 2 reads the atomic cell at offset 𝑘 of location ℓ, tests whether its value is equal to 𝑣 1 , overwrites it with 𝑣 2 if that is the case, and returns the Boolean result of the test; importantly, the read and the write operations happen atomically. There is syntactic sugar for single-cell locations, or "references": ref 𝛼 𝑣 allocates a location of length one, ! 𝛼 ℓ reads at offset zero, ℓ 𝛼 𝑣 writes at offset zero and CAS ℓ 𝑣 1 𝑣 2 performs compare-and-set at offset zero. Lastly, fork 𝑒 creates a new thread which executes 𝑒. The expression fork 𝑒 returns the unit value () without waiting for the completion of the new thread.

The memory model of Multicore OCaml describes how the memory operations interact with the shared memory. [START_REF] Stephen Dolan | Bounding data races in space and time[END_REF] give an operational account, which is out of the scope of the current paper. However, to give some intuition, we show in Figure 7 what this semantics translates to in the Cosmo program logic. In the following paragraphs, we give an overview of these triples which are explained more thoroughly by [START_REF] Mével | Cosmo: A Concurrent Separation Logic for Multicore OCaml[END_REF].

There are different points-to assertions for atomic cells and for non-atomic cells. As is standard, these predicates assert unique ownership of the cells.

Operations on non-atomic cells obey the usual-looking Hoare triples, but an important departure from sequential consistency is that their associated points-to assertion ℓ [𝑘] na 𝑣 is subjective: the knowledge of the latest value 𝑣 of a non-atomic cell ℓ [𝑘] is relative to the ambient view. 8On the other hand, the points-to assertion ℓ [𝑘] at ⟨𝑣, V⟩ that represents an atomic cell is objective: this implies that an atomic cell ℓ [𝑘] stores a single value 𝑣 on which all threads agree. In addition, an atomic cell also stores a view V. As can be seen in the triples of atomic operations, this view accumulates the knowledge of all writers and transmits this knowledge to readers. This means that there is a happens-before relationship from a write operation to a read operation which reads from it (in a release-acquire fashion). In fact, atomic accesses are the prime means of inter-thread synchronization in Multicore OCaml.

The last two triples say that a failed CAS operation behaves as an atomic read (returning false), while a successful CAS operation behaves as the combination of an atomic read and an atomic write (returning true).

Overview of the Data Structure

The code of the concurrent queue library we consider appears in Figure 8. It uses a ring buffer of fixed capacity 𝐶 ≥ 1. The buffer is represented by two arrays of length 𝐶, statuses and items; in each slot (whose offset ranges from 0 included to 𝐶 excluded), the buffer thus stores a status in an atomic field and an item in a non-atomic field. The data structure also has two integers stored in atomic references, head and tail.

Items are identified by their rank (starting at zero) of insertion in the queue since its creation. The item of rank 𝑘 is stored in slot "𝑘 mod 𝐶", which from now on we denote as 𝑘. The reference head stores the number of items that have been enqueued since the creation of the queue, including those that have since been dequeued. In other words, it is the rank of the next item to be enqueued. Similarly, tail stores the number of items that have been dequeued since the creation of the queue. In other words, it is the rank of the next item to be dequeued.

Each slot is in one of two states: either it is occupied, meaning that it stores some item of the queue; or it is available, meaning that the value it stores is irrelevant. In addition, for the concurrent queue operations to work properly, we must remember for which rank each slot was last used. 9The status encodes this information in a single integer, as follows:

• an even status 2𝑘 indicates that slot 𝑘 is available for storing a future item of rank 𝑘;

• an odd status 2𝑘 + 1 indicates that slot 𝑘 is currently occupied by the item of rank 𝑘.

Let ℎ and 𝑡 be the value of references head and tail, respectively. At any time, the ranks of items that are stored in the queue-or in the process of being stored-range from 𝑡 included to ℎ excluded, and there cannot be more than 𝐶 such items. Thus, an invariant property of the queue is:

0 ≤ 𝑡 ≤ ℎ ≤ 𝑡 + 𝐶

Explanation of the Code

The function enqueue repeatedly calls try_enqueue until it succeeds; the latter can fail either because the buffer is full or because of a competing enqueuer. 10When calling try_enqueue, we start by reading the current value ℎ of the reference head. To check that slot ℎ is available for rank ℎ, we read its status. If it differs from 2ℎ, we fail: a status less than 2ℎ indicates that the buffer is full11 , a status greater than 2ℎ indicates interference from another competing enqueuing thread, which has been attributed rank ℎ before we have.

If the status is 2ℎ, then we try to increment head from ℎ to ℎ + 1. If the CAS fails, we fail: again, another competing enqueuer has been attributed rank ℎ.

If the CAS succeeds, then we are attributed rank ℎ and can proceed to inserting an item into slot ℎ. As we will explain later, this implies that its status has not changed since we read it: the slot is still available. We write the new item, and then we update the status accordingly. This update must come last, as it serves as a signal that the slot is now occupied with an item and ready for dequeuers.

Similarly, dequeue repeatedly calls try_dequeue until it succeeds; the latter works analogously to try_enqueue,12 and can fail either because the buffer is empty or because of a competing dequeuer. 10

Monotonicity of the Internal State of the Queue

Once the queue has been created, the reference head is only accessed from function try_enqueue. The only place where it is modified is the compare-and-set operation in this function, which attempts to increment it by one, using a compare-and-set operation. Hence this counter is strictly monotonic, and we can regard a successful increment from ℎ to ℎ + 1 as uniquely attributing rank ℎ to the candidate enqueuer. Only then it is allowed to write into slot ℎ.

Similarly, tail is only accessed from function try_dequeue, is strictly monotonic, and a successful increment from 𝑡 to 𝑡 + 1 uniquely attributes rank 𝑡 to the candidate dequeuer. Only then it is allowed to write into slot 𝑡.

The status of a given slot is strictly monotonic too. Indeed, there are two places where it is updated. As an enqueuer, when we write 2ℎ + 1, no other enqueuer updated the status since we read it to be 2ℎ, because only we have been attributed rank ℎ. In particular, it remained even, so no dequeuer tried to obtain rank ℎ and update the status of slot ℎ. Hence, the status is still 2ℎ when we overwrite it with 2ℎ + 1. Symmetrically, the status is still 2𝑡 + 1 when a dequeuer overwrites it with 2(𝑡 + 𝐶).

Notes on Contention in the Queue

A noteworthy feature of this implementation is that it tries to limit competition between enqueuers and dequeuers. Indeed, enqueuers and dequeuers generally operate on separate references: enqueuers never access tail and dequeuers never access head. Hence in favorable situations-when the buffer is neither empty nor full-there are no enqueuer-dequeuer competitions beyond ones between an enqueuer and a dequeuer of the same rank.

A weakness of this implementation, however, is that it does not enjoy any non-blocking property [Fraser 2004, Chapter 2]: if an enqueuer or a dequeuer halts after it has been attributed a rank but before it updates the corresponding slot, then after some time, any other thread trying to enqueue or dequeue fails. »

PROOF OF THE SPECIFICATION FOR THE RING BUFFER

We now turn to proving the following. In the Iris methodology, which Cosmo is based on, concurrent protocols are established thanks to ghost state and invariants. Ghost state in Iris is a flexible tool for defining custom resources. It takes values from algebraic structures called CMRAs; for the purpose of this paper, it is enough to think of a CMRA as a set equipped with a binary composition operation (•) that is partial, associative and commutative. Ghost state values are assigned to ghost variables. The separation logic assertion 𝑎 𝛾 , where 𝑎 is an element of some CMRA, intuitively means that we own a fragment of the ghost variable 𝛾 and that this fragment has value 𝑎. Unlike what happens with a traditional points-to assertion, the ownership and value of a ghost variable can be split into fragments according to the composition operation of the CMRA: 𝑎 • 𝑏 𝛾 ⊣⊢ 𝑎 𝛾 * 𝑏 𝛾 . In Cosmo, ghost state is objective, as it is independent from the physical state of the memory.

Ghost state can be coupled with invariants such as the ones presented in §2.2 to describe protocols that threads must follow to access shared resources. In Figure 9, one can see how this methodology is used for describing the internal protocol of the queue: the persistent predicate QueueInv 𝑞 𝛾 is in fact an invariant; the exclusive representation predicate IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )] is defined using ghost state, as are several internal resources. We detail these definitions in the following sections.

Public State

The assertion IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )], defined in Figure 9a, exposes to the user the public state of the queue. This public state, as motivated in §2.3, is composed of the tail view, the head view, and the list of current items with their views. It is tied to the internal state of the queue via the use of an authoritative ghost state, stored in a ghost variable 𝛾. More precisely, the public state is kept in sync with the values which appear in an authoritative assertion • (T , H, [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )]) 𝛾 , the latter being owned by the internal invariant. The two assertions satisfy the properties shown in Figure 10a. Rule IsQueue-Agree asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise). Rule IsQueue-Update asserts that, whenever we own both the representation predicate and its authoritative counterpart, we can update the public state to any other value by taking a ghost update step. Such a ghost update is allowed by the Iris modality denoted | ⇛.

We achieve these properties by using an adequate CMRA for the values of the ghost variable 𝛾. This CMRA is built by composing several classical Iris constructs: the exclusive CMRA Ex(𝑆), and the authoritative CMRA Auth(𝑀). We do not explain the construction in more detail; we refer the interested reader to the documentation of Iris [START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF].

It is worth remarking that this construction makes the representation predicate exclusive: it is absurd to own simultaneously two assertions of the form IsQueue 𝛾 ---.

Internal Invariant

Along with the exclusive representation predicate IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )], we provide the user with a persistent assertion QueueInv 𝑞 𝛾 defined in Figure 9e. It contains the internal invariant governing the queue 𝑞, whose public state is exposed via the ghost variable 𝛾. In addition to the public state, there are two more ghost variables, named 𝛾 mono and 𝛾 tokens , which are hidden to the user of the queue but needed internally. Thus they are existentially quantified in this persistent assertion. We will explain the purpose and meaning of these ghost variables in a moment. For now, we look at the internal invariant, QueueInvInner 𝑞 𝛾 𝛾 mono 𝛾 tokens .

This invariant owns most of the physical locations of the queue: tail, head, statuses, and some parts of the array items. Recall that points-to assertions for atomic cells are objective and can be placed inside an invariant. The array-points-to assertion statuses * at [(𝑠 0 , S 0 ), ..., (𝑠 𝐶-1 , S 𝐶-1 )] is a shorthand for the following iterated conjunction: * 0≤𝑖<𝐶 statuses[𝑖] at ⟨𝑠 𝑖 , S 𝑖 ⟩ Also, since we encode references as arrays of length one, we write tail at ⟨𝑡, T ⟩ as a shorthand for tail[0] at ⟨𝑡, T ⟩.

Apart from this physical state, the invariant also stores ghost state. It owns the authority on all three ghost variables, 𝛾, 𝛾 mono and 𝛾 tokens . The authority of 𝛾 is simple: it ties internal values to the public state of the queue, as explained earlier. We now explain the other two pieces of ghost state.

IsQueue-Agree Witness-Order

• (T , H, [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )]) 𝛾 * IsQueue 𝛾 T ′ H ′ 𝑣 ′ 0 , V ′ 0 , ..., 𝑣 ′ 𝑛-1 , V ′ 𝑛-1 T = T ′ ∧ H = H ′ ∧∀𝑖. 𝑣 = 𝑣 ′ 𝑖 ∧ V 𝑖 = V ′ 𝑖 IsQueue-Update • (T , H, [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )]) 𝛾 * IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )] | ⇛ • T ′ , H ′ , 𝑣 ′ 0 , V ′ 0 , ..., 𝑣 ′ 𝑛-1 , V ′ 𝑛-1 𝛾 * IsQueue 𝛾 T ′ H ′ 𝑣 ′ 0 , V ′ 0 , ..., 𝑣 ′ 𝑛-1 , V ′ 𝑛-1 (
{𝑖 ↦ → • (𝑠, S)} 𝛾 mono * Witness 𝛾 mono 𝑖 (𝑠 ′ , S ′ ) (𝑠 ′ , S ′ ) ⊑ (𝑠, S) Witness-Update {𝑖 ↦ → • (𝑠, S)} 𝛾 mono * (𝑠, S) ⊑ (𝑠 ′ , S ′ ) | ⇛ {𝑖 ↦ → • (𝑠 ′ , S ′ )} 𝛾 mono * Witness 𝛾 mono 𝑖 (𝑠 ′ , S ′ ) (b) Properties of witnesses Token-Exclusive-RR TokenR 𝛾 tokens 𝑘 * TokenR 𝛾 tokens 𝑘 ′ 𝑘 ≠ 𝑘 ′ Token-Exclusive-RW TokenR 𝛾 tokens 𝑘 * TokenW 𝛾 tokens 𝑘 ′ (𝑣 ′ , V ′ ) 𝑘 ≠ 𝑘 ′ Token-Exclusive-WW TokenW 𝛾 tokens 𝑘 (𝑣, V) * TokenW 𝛾 tokens 𝑘 ′ (𝑣 ′ , V ′ ) 𝑘 ≠ 𝑘 ′ TokenR-Agree • 𝑚 𝛾 tokens * TokenR 𝛾 tokens 𝑘 𝑚(𝑘) = () TokenW-Agree • 𝑚 𝛾 tokens * TokenW 𝛾 tokens 𝑘 (𝑣, V) 𝑚(𝑘) = (𝑣, V) Token-Update-RW • 𝑚 𝛾 tokens * TokenR 𝛾 tokens (𝑘 -𝐶) | ⇛ • 𝑚[𝑘 -𝐶 ↦ → ⊥] [𝑘 ↦ → (𝑣, V)] 𝛾 tokens * TokenW 𝛾 tokens 𝑘 (𝑣, V) Token-Update-WR • 𝑚 𝛾 tokens * TokenW 𝛾 tokens 𝑘 (𝑣, V) | ⇛ • 𝑚[𝑘 ↦ → ()] 𝛾 tokens * TokenR 𝛾 tokens 𝑘 (

Monotonicity of Statuses

The purpose of the ghost variable 𝛾 mono is to reflect the fact that statuses are monotonic. More precisely, they are strictly monotonic: every write to a status cell necessarily increases its value. As a consequence, as long as the value of a status cell has not increased, we know that no write happened to it and, in particular, that the view that it stores has not increased either. In other words, we have the monotonicity of the value-view pair stored in a status cell, for the lexicographic order where the order on views is reversed:

(𝑠 1 , S 1 ) ⊑ (𝑠 2 , S 2 ) ⇐⇒ 𝑠 1 < 𝑠 2 ∨ (𝑠 1 = 𝑠 2 ∧ S 1 ⊒ S 2 )
This stronger monotonicity property will be used in proofs, and specifying it is thus an additional requirement of working with a weak memory model. ,S) means that the value-view pair stored in the status cell is at least (𝑠, S). Importantly, a witness assertion is persistent: once it has been established, it remains true forever and can be duplicated at will.

We thus have the properties summarized in Figure 10b. Rule Witness-Persistent is the persistence just mentioned. Rule Witness-Order asserts that a witness gives a lower bound on what the status cell currently stores. Rule Witness-Update asserts that we can update a status cell to any larger (or equal) content, and obtain a witness for that content.

We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable 𝛾 mono . Again, we will not explain standard Iris constructs here, except for one point. The construction involves building a CMRA whose carrier set is Z × View, the set of status-view pairs, and whose inclusion order 13 coincides with the desired order ⊑. A general recipe for deriving a CMRA structure with a given inclusion order, if that order admits binary joins, consists in taking the join operation as the composition of the CMRA [START_REF] Timany | Reasoning about Monotonicity in Separation Logic[END_REF]. In this case, we equip the product set Z × View with the join-semilattice structure whose definition appears in Figure 9b.

Available and Occupied Slots

In Figure 9e, the last two lines of the invariant describe the state of each slot. For clarity, we introduce two abbreviations: the assertion Available 𝑘 (𝑠, S) represents slot 𝑘 being available for a future item of rank 𝑘 + 𝐶; the assertion Occupied 𝑘 (𝑠, S) (𝑣, V) represents slot 𝑘 being occupied by the item of rank 𝑘, whose value is 𝑣 with the associated view V. In these two abbreviations, the status field of the slot has value 𝑠 and stores view S. These abbreviations are also where we keep the ownership of the non-atomic cell items[ 𝑘], via a points-to assertion.

Recall that, in Cosmo, unlike an atomic points-to assertion, a non-atomic points-to assertion is subjective: its truth depends on the view of the subject thread. As a consequence, it cannot be placed in an invariant as is. In order to share this assertion, we must explicitly indicate at which view it holds. This is the purpose of the @ connective.

At which view can we own a non-atomic memory cell? At a view which contains the latest write event to that cell. Fortunately, in our case, any thread-enqueuer or dequeuer-which writes to the non-atomic cell items[ 𝑘] then writes to the atomic cell statuses [ 𝑘]. Thus it adds its knowledge, including its own write to the item field, to the view S stored by the status field. 13 For two elements 𝑎 and 𝑏 of a CMRA 𝑀, we say that 𝑏 is included in 𝑎 if there exists some 𝑐 such that 𝑎 = 𝑏 • 𝑐. With all this said, a first attempt at representing the buffer might look as follows:

QueueInvInner 𝑞 𝛾 𝛾 mono 𝛾 tokens ? = *                      . . . * ℎ-𝐶 ≤𝑘<𝑡 Available 𝑘 (𝑠 𝑘 , S 𝑘 ) * 𝑡 ≤𝑘<ℎ Occupied 𝑘 (𝑠 𝑘 , S 𝑘 ) (𝑣 𝑘 , V 𝑘 )
Available 𝑘 (𝑠, S)

? = 𝑠 = 2(𝑘 + 𝐶) * (items[ 𝑘] na -) @ S
Occupied 𝑘 (𝑠, S) (𝑣, V)

? = 𝑠 = 2𝑘 + 1 * (items[ 𝑘] na 𝑣) @ S * V ⊑ S
That is, we describe the 𝐶 slots by ranging from ℎ -𝐶 to ℎ. The indices from ℎ -𝐶 to 𝑡 correspond to available slots, while indices from 𝑡 to ℎ correspond to slots occupied by the items of the queue. In both cases, we own the item field at the view S which is stored in the corresponding status field. The item field of an available slot stores an arbitrary value, while for an occupied slot it stores the item 𝑣.

An occupied slot should also carry the view V which the queue is supposed to transfer from the enqueuer to the dequeuer alongside item 𝑣. This again relies on the view S: the enqueuer adds V to S when updating the status, and the dequeuer adds S into its own view when reading the status; so, to retrieve V, it is enough to state the inclusion V ⊑ S.

The tentative invariant stated above, however, is not correct: while an invariant has to hold at any point of the execution, the assertion above is temporarily invalidated when a thread enqueues or dequeues. Specifically, the thread breaks the assertion when it increments head or tail, thus committing to enqueuing or dequeuing, until it updates the status of the corresponding slot. It is thus necessary to represent slots which are in a temporary state. In the actual invariant shown in Figure 9e, slots from ℎ -𝐶 to 𝑡 are either available or in a temporary state where they appear as occupied (𝑠 𝑘 = 2𝑘 + 1), until a dequeuer finishes emptying them; slots from 𝑡 to ℎ are either occupied or in a temporary state where they appear as available (𝑠 𝑘 = 2𝑘), until an enqueuer finishes filling them.

When an enqueuer or dequeuer moves a slot into a temporary state, it takes ownership of its item field, so that it can write to it. Hence the invariant does not have the corresponding points-to assertion. The thread must give it back when updating the status.

Slot Tokens

This time frame-when a slot is in a temporary state-is also when the last piece of ghost state, stored in the ghost variable 𝛾 tokens , intervenes. Other threads can make the queue progress between the moment when an enqueuer is attributed rank 𝑘, and the moment when it returns the updated slot to the invariant. An enqueuer needs the assurance that the queue has not gotten too far and attributed the slot on which it was working to a dequeuer, or to another enqueuer in a subsequent cycle.

To this effect, we start by stating how advances of the head and tail are limited with respect to one another; indeed, we prove these inequalities as part of the invariant:

0 ≤ 𝑡 ≤ ℎ ≤ 𝑡 + 𝐶
We also maintain in existence one token for each rank from ℎ -𝐶 to ℎ. These tokens are exclusive assertions, and there cannot exist two tokens whose ranks are congruent modulo 𝐶. Hence the token of rank 𝑘 is enough to grant unique write access to slot 𝑘. We use it as follows.

(1) When an enqueuer is attributed rank 𝑘, it borrows a newly created token of the same rank.

(2) When returning the updated slot to the invariant, the enqueuer also returns the token; from that moment the token is thus kept in the assertion Occupied 𝑘 (𝑠, S) (𝑣, V).

(3) When a dequeuer is attributed rank 𝑘, it claims that assertion and borrows the token. (4) When returning the updated slot to the invariant, the dequeuer also returns the token; from that moment the token is thus kept in the assertion Available 𝑘 (𝑠, S).

In step 1, the token is created while destructing the token of rank 𝑘 -𝐶 taken from the assertion Available (𝑘 -𝐶) -, which represents the available cell that the thread claims for enqueuing.

To be able to distinguish between the two temporary states (enqueuing and dequeuing), we give the token a flavor: from steps 1 to 2 it is a write token; from steps 3 to 4 it is a read token. At any moment, there are read tokens from rank ℎ -𝐶 to 𝑡, and write tokens from 𝑡 to ℎ.

We have a last requirement: when an enqueuer is attributed rank 𝑘, the new item is added to the public state immediately-the CAS operation on head is the commit point of enqueuing-even though the enqueuer has not actually written the item yet. When it finally returns the updated slot, the enqueuer has lost track of the public state, which may have continued to progress in the meantime. At that moment, it thus needs a reminder that the item it just wrote is indeed the one it was expected to write. We implement this by adding the value 𝑣-and view V-of the item as a payload to the write token.

The read token of rank 𝑘 is denoted by TokenR 𝛾 tokens 𝑘, while the write token of rank 𝑘 with payload 𝑣 and V is denoted by TokenW 𝛾 tokens 𝑘 (𝑣, V). Their authoritative counterpart, owned by the invariant, is an assertion of the form • 𝑚 𝛾 tokens where 𝑚 is a finite map. Its domain is the range [ℎ -𝐶, ℎ) of ranks which have a token, and its images are the payload (considering that read tokens bear a payload of ()). In the invariant, the value of the map is connected to that of the public state.

The assertions are defined in Figure 9d and satisfy the properties in Figure 10c. The first three properties say that tokens are exclusive. The next two say that tokens agree with the authoritative counterpart, hence with the public state. Rule Token-Update-RW corresponds to step 1 in the list above, where we create a write token of rank 𝑘 by destructing a read token of rank 𝑘 -𝐶. Likewise, rule Token-Update-WR corresponds to step 3, where we turn a write token into a read token of the same rank.

In addition to these rules, the finite map described in the internal invariant is such that, whenever we own a read token (respectively a write token), the rank of this token necessarily lies in the range [ℎ -𝐶, 𝑡) (respectively [𝑡, ℎ)), where 𝑡 and ℎ are the values of tail and head which are existentially quantified in the invariant. Thanks to that property, at step 4 (respectively 2), when a dequeuer (respectively an enqueuer) returns the token, it knows that the rank it has been operating on is still in the right range-in other words, that the queue has not advanced too far while the thread was working.

There are more properties that are invariants of the queue, and thus could be stated and verified. However, they are not needed to prove that the code satisfies its specification. For example, the fact that tail and head are strictly monotonic, and the fact that statuses are non-negative, are not explicitly used.

Logical Atomicity

The specification that we wish to prove is a logically atomic Hoare triple. The definition of such triples for Iris is given by Jung et al. [2015, §7] and further refined by [START_REF] Jung | Logical Atomicity in Iris: the Good, the Bad, and the Ugly[END_REF]. It turns out that this definition can be ported as is using the connectives of Cosmo. As we will see in §4.7 and §5.3, the logically atomic triples so defined can be proved and are sufficient for interesting clients. We do not attempt to replicate in this paper the full definition. An approximate definition that suffices to capture the essence of logical atomicity, and to understand our proof, is:

⟨𝑥 . 𝑃⟩ 𝑒 ⟨Φ⟩ ≜ ∀Ψ, | ⇛ ⊤ ∅ ∃𝑥 . 𝑃 * ∀𝑣. Φ 𝑣 - * | ⇛ ∅ ⊤ Ψ 𝑣 - * wp 𝑒 {Ψ}
In this formula, the variable 𝑃 is a Cosmo assertion (of type vProp); the variables Φ and Ψ are predicates on values (of type Val → vProp); 𝑃 and Φ may refer to the name 𝑥. The assertion wp 𝑒 {Ψ} is the weakest precondition for program 𝑒 and postcondition Ψ (in Iris, Hoare triples are syntactic sugar for weakest preconditions).

The purpose of a logically atomic triple is to give a specification to a non-atomic program 𝑒 as if it were atomic. In practice, we require that the proof of 𝑒 accesses the precondition and turns it into the postcondition in one atomic step only, which we call the commit point of this logically atomic program. That is, if 𝑒 satisfies the triple ⟨𝑥 . 𝑃⟩ 𝑒 ⟨Φ⟩, then it can perform several steps of computation but, as soon as it accesses the resource 𝑃, it must return the resource Φ in the same step of computation. 14 Once it has done so, 𝑒 can perform further computation steps but 𝑃 is not available anymore. As explained in §2.2, thanks to this constraint, the client of this specification can open invariants around 𝑒 as if 𝑒 were atomic.

To capture this atomicity requirement, we ask the proof of the logically atomic triple for 𝑒 to be valid for any postcondition Ψ chosen by the client. Given that Ψ is arbitrary, the only means of establishing this postcondition is to use the premise

| ⇛ ⊤ ∅ ∃𝑥 . 𝑃 * (∀𝑣 . Φ 𝑣 - * | ⇛ ∅ ⊤ Ψ 𝑣), which is
known as an atomic update. When desired, this atomic update gives access to the precondition 𝑃 for some value of 𝑥, and, in exchange for the postcondition Φ of the logically atomic triple, it returns the resource Ψ, which can then be used to finish the proof. Crucially, the masks ∅ and ⊤ annotating the fancy updates | ⇛ ⊤ ∅ and | ⇛ ∅ ⊤ require that the atomic update be used during one atomic step only, as required.

Using the invariant rules of Iris [START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF], it is easy to show that atomic updates can be used to open and close invariants. Rule LAInv follows as a corollary, rule LAHoare is immediate.

Proof of try_enqueue

We now outline the proof that try_enqueue satisfies its specification from Figure 5. The proof for try_dequeue is similar; those for enqueue and dequeue are deduced from the previous two by an obvious induction; and the proof of make is simply a matter of initializing the ghost state. The interested reader may find these proofs, conducted in the Coq proof assistant, in our repository [START_REF] Mével | Coq proofs for Cosmo and examples[END_REF].

Recalling here the specification in Figure 5, and unfolding the definition of QueueInv 𝑞 𝛾, we ought to prove the following assertion:

QueueInvInner 𝑞 𝛾 𝛾 mono 𝛾 tokens ⟨ T , H, 𝑛, (𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 ). IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )] * ↑ V ⟩ try_enqueue 𝑞 𝑣 ⟨ 𝜆𝑏. ∨ IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )] * 𝑏 = false IsQueue 𝛾 T (H ⊔ V) [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 ), (𝑣, V)] * ↑ H * 𝑏 = true ⟩
This is also when the strict monotonicity of the status comes into play: because 𝑠 𝑘 = 𝑠 1 , it gives us S 𝑘 ⊑ S 1 . But we have ↑ S 1 in our proof context, so we obtain the points-to assertion as a subjective assertion: items[ 𝑘] na -.

We commit the atomic update now. Indeed the successful CAS is the commit point of try_enqueue. We know that the program will return true, so we must provide the corresponding postcondition of the logically atomic triple, where our item (𝑣, V) has been appended to the public state of the queue. Thus we take a ghost step to update this public state. By committing, we finally obtain the assertion Ψ true that will serve at the end of the proof, since true is the return value of the operation. Along the way, we also collect the persistent assertion ↑ V from the precondition of the logically atomic triple.

Finally, we keep on our side the write token, the non-atomic points-to assertion items[ 𝑘] na -, we reconstruct the invariant, updated for the new value of head, and we close it.

The next step of the program writes the value 𝑣 to the non-atomic item field, which is easy since we have the points-to assertion at hand. This assertion then becomes items[ 𝑘] na 𝑣. We turn it back to an objective assertion, which gives us a view W and two assertions ↑ W and (items[ 𝑘] na 𝑣) @ W.

The last step of the program is to update the (atomic) status of the slot. Once more we open the invariant. If we again note ℎ and 𝑡 the current values of head and tail (potentially different from the last time we opened the invariant), then owning a write token for rank 𝑘 teaches us that 𝑡 ≤ 𝑘 < ℎ. The invariant then gives us for slot 𝑘:

Occupied 𝑘 (𝑠 𝑘 , S 𝑘 ) (𝑣 𝑘 , V 𝑘 ) ∨ 𝑠 𝑘 = 2𝑘
The left disjunct would own our write token, but we already have it and it is exclusive; hence we are in the right disjunct, 𝑠 𝑘 = 2𝑘 = 𝑠 1 . We perform the atomic write with value 𝑠 2 ≜ 2𝑘 + 1 (strict monotonicity is respected), and since we have both ↑ V and ↑ W in context, we can push the view S 2 = V ⊔ W to this atomic location while writing. We then switch to the left disjunct, by constituting the assertion:

Occupied 𝑘 𝑠 2 , S 2 (𝑣, V) ⊣⊢ *            𝑠 2 = 2𝑘 + 1 (items[ 𝑘] na 𝑣) @ S 2 TokenW 𝛾 tokens 𝑘 (𝑣, V) V ⊑ S 2
Hence we return the non-atomic points-to assertion and the write token to the invariant before closing it.

A SIMPLE PIPELINE

We now demonstrate the use of our specification of a concurrent queue by a simple client application, that chains two treatments on a sequence of data, where each treatment is applied in a separate thread. Thus the sequence of intermediate values is transferred from a producer to a consumer using a concurrent queue.

Implementation of the Pipeline

The code of the application is presented in Figure 11. It provides a single function, pipeline, which takes as arguments two functions 𝑔 and 𝑓 , a sequence xs, and returns a sequence obtained by applying 𝑔 • 𝑓 to each item of the input sequence. The functions 𝑔 and 𝑓 need not be pure: they can have side effects and rely on some state. For simplicity, input and output sequences are encoded as (non-atomic) arrays, whose length can be obtained via a primitive operation length -. However the implementation can be modified to consume and produce lists of unknown length, or even infinite streams, provided an encoding of such data structures; we would then use a sentinel value in the queue to signal the end of stream.

The code is straightforward: we create a concurrent queue ys, then we fork a thread. The queue is shared between the main thread and the forked thread, while xs is transmitted to the forked thread. The forked thread reads items from xs in turn, applies 𝑓 to them and enqueues the results. The main thread creates a new (non-atomic) array zs to store the output; then, it dequeues 𝑛 items, where 𝑛 is the number of items in the input sequence, applies 𝑔 to them, and adds the results to zs. Finally, it returns zs.

Specification of the Pipeline

A possible specification for this pipeline is shown in Figure 12. It is higher-order, and expressed using the weakest-precondition predicate.

In postcondition we obtain one assertion 𝑅 𝑘 𝑧 𝑘 for each item of the stream, related to its position 𝑘 (in particular, 𝑅 may relate the output value 𝑧 𝑘 to the input value 𝑥 𝑘 ).

In the precondition, essentially, we want to state that for some predicates 𝑃 and 𝑄, we have the assertions 𝑃 𝑘 𝑥 𝑘 for all items of the input stream, and functions 𝑓 and 𝑔 satisfy Hoare triples of the form:

{𝑃 𝑘 𝑥 } 𝑓 𝑥 {𝜆𝑦. 𝑄 𝑘 𝑦} {𝑄 𝑘 𝑦} 𝑔 𝑦 {𝜆𝑧. 𝑅 𝑘 𝑧} so that, by the chaining rule, the composition satisfies: {𝑃 𝑘 𝑥 } 𝑔 (𝑓 𝑥) {𝜆𝑧. 𝑅 𝑘 𝑧} By using weakest preconditions instead of Hoare triples, we avoid mentioning the predicate 𝑃; by taking advantage of the higher-order nature of Iris, we can nest the triples so as to conceal the intermediate predicate 𝑄.

• Indices in the range [0, 𝑛 g ) have been processed by both 𝑓 and 𝑔. Hence, we have consumed their intermediate weakest-precondition assertions, and have obtained postconditions 𝑅 𝑘 𝑧 𝑘 as a result. These are owned by the thread computing 𝑔, along with the array zs which contains the output items.

The key point is that the assertion wp 𝑔 𝑦 𝑘 {-} has been given by the thread computing 𝑓 to the invariant when enqueuing the corresponding item, and will be taken by the thread computing 𝑔 when dequeuing that item. This assertion is thus exchanged between two threads with differing views of the shared memory, and transits via a neutral ground: an objective invariant. We make the assertion objective by specifying at which view it holds: namely, the view V 𝑘 which the enqueuer had and which the dequeuer will acquire. Therefore, we rely crucially on the enqueuer-to-dequeuer synchronization guaranteed by the queue.

With these invariant assertions correctly stated, the proof is rather straightforward. When creating the pipeline, we have 0 = 𝑛 g = 𝑛 f and assertions PipeInvInner and PipeG hold trivially (the queue is empty and there are no output items computed yet); the assertion PipeF is constituted exactly from the preconditions of the pipeline (Figure 12), and is given by the main thread to the child thread that will compute 𝑓 . When the pipeline has completed its work, we have 𝑛 g = 𝑛 f = 𝑛 and the assertion PipeG provides exactly the postcondition of the pipeline.

Thanks to the logically atomic triples in the specification of the queue, when enqueuing (respectively, dequeuing), we can open the invariant of the pipeline and move assertions to it (respectively, from it) as already explained.

RELATED WORK

The verification of fine-grained concurrent data structures is a well-studied problem with a particularly rich literature. Several approaches were tried, targeting various verification frameworks, various data structures in different contexts.

The notion of linearizability is central for specifying such libraries. [START_REF] Dongol | Verifying linearisability: A comparative survey[END_REF] gave a survey of the different techniques used for linearizability of concurrent libraries at that time. Of particular interest in the context of separation logic is the technique of logical atomicity, which has been recently proved to be equivalent to linearizability [START_REF] Birkedal | Theorems for Free from Separation Logic Specifications[END_REF] in the context of a sequentially consistent model. This concept has been developed through several iterations over the last decade [START_REF] Da | TaDA: A logic for time and data abstraction[END_REF][START_REF] Jung | Iris: monoids and invariants as an orthogonal basis for concurrent reasoning[END_REF][START_REF] Jacobs | Expressive modular fine-grained concurrency specification[END_REF][START_REF] Kasper Svendsen | Modular Reasoning about Separation of Concurrent Data Structures[END_REF][START_REF] Jung | The Future is Ours: Prophecy Variables in Separation Logic[END_REF]]. In the present work, we adapt an unpublished, modern version of Iris's logically atomic triples [START_REF] Jung | Logical Atomicity in Iris: the Good, the Bad, and the Ugly[END_REF]], to the setting of Cosmo. This is, to the best of our knowledge, the first use of logical atomicity in a weakly consistent setting.

Another popular approach for proving the correctness of concurrent libraries is the use of refinement with respect to a simpler implementation. This is the track chosen by ReLoC [START_REF] Frumin | ReLoC: A mechanised relational logic for fine-grained concurrency[END_REF]], which has recently been combined with logical atomicity [START_REF] Frumin | ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity[END_REF]]. Interestingly, ReloC has been recently used for proving the correctness of several concurrent queue implementations [START_REF] Vindum | Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook's Folly Library[END_REF][START_REF] Vindum | Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook's Folly Library[END_REF], one of which is very close to ours. However, these proofs do not handle relaxed memory behaviors, so that they do not provide a solution to the problem of specifying the lack of happens-before relationship between some data structure accesses, which we discussed in §2.3. Because it lacks some happens-before relationships, our queue implementation is not a refinement of a naive implementation which would use a lock to protect a sequential implementation, so a refinement-based approach would not be useful for proving our library correct. The refinement approach has also been used to prove correct some data structures used in a concurrent garbage collector [START_REF] Zakowski | Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement[END_REF]].

LAHoare

  Fig. 3. Selected rules for logically atomic triples

Fig. 6 .

 6 Fig. 6. The syntax of a fragment of Multicore OCaml

Theorem 4. 1 .

 1 There exist predicates IsQueue and QueueInv such that the implementation shown in Figure 8 ( §3) satisfies the functional specification appearing in Figure 5 ( §2.3).

  a) Properties of the representation predicate Witness-Persistent persistent(Witness 𝛾 mono 𝑖 (𝑠, S))

  Fig. 10. Axiomatic description of the ghost state of the queue

  Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021. Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model 66:19

Fig. 11 .

 11 Fig. 11. Implementation of a pipeline

  let make () = let tail = ref at 0 in let head = ref at 0 in let items = array na [𝐶] () in let statuses = array at [𝐶] 0 in for 𝑖 from 0 to 𝐶 -1 do statuses[𝑖] na ← 2𝑖 done; (tail, head, statuses, items) let try_enqueue 𝑞 𝑣 = let (tail, head, statuses, items) = 𝑞 in let ℎ = ! at head in let 𝑠 = statuses[ℎ mod 𝐶] at in if 𝑠 = 2ℎ ∧ CAS head ℎ (ℎ + 1) then items[ℎ mod 𝐶] na ← 𝑣; statuses[ℎ mod 𝐶] at ← 2ℎ + 1; 𝑞 in let 𝑡 = ! at tail in let 𝑠 = statuses[𝑡 mod 𝐶] at in if 𝑠 = 2𝑡 + 1 ∧ CAS tail 𝑡 (𝑡 + 1) then let 𝑣 = items[𝑡 mod 𝐶] na in items[𝑡 mod 𝐶]

	let try_dequeue 𝑞 =
	let (tail, head,
	statuses, items) =
	true
	else
	false
	let rec enqueue 𝑞 𝑣 =
	if try_enqueue 𝑞 𝑣
	then ()
	else enqueue 𝑞 𝑣

na ← (); statuses[𝑡 mod 𝐶] at ← 2(𝑡 + 𝐶); Some 𝑣 else None let rec dequeue 𝑞 = match try_dequeue 𝑞 with | Some 𝑣 → 𝑣 | None → dequeue 𝑞 Fig. 8. Implementation of the bounded queue

  To reflect monotonicity of the status of offset 𝑖, we use two assertions, {𝑖 ↦ → • (𝑠, S)} 𝛾 mono and Witness 𝛾 mono 𝑖 (𝑠, S), connected via a ghost variable 𝛾 mono . Relevant definitions appear in Figure9c. The first assertion, owned by the invariant of the queue is connected by the invariant to the value-view pair stored in the status cell. It is exclusive: for any offset 𝑖, two assertions of the form {𝑖 ↦ → • -}

	𝛾

mono cannot hold simultaneously. The second assertion Witness 𝛾 mono 𝑖 (𝑠

  let pipeline 𝑔 𝑓 xs = let 𝑛 = length xs in let ys = make () in fork (pipef 𝑛 xs ys 𝑓 ); let zs = array na [𝑛] () in pipeg 𝑛 ys zs 𝑔; zs let pipef 𝑛 xs ys 𝑓 = for 𝑘 from 0 to 𝑛 -1 do let 𝑥 = xs[𝑘] na in let 𝑦 = 𝑓 𝑥 in enqueue ys 𝑦 done let pipeg 𝑛 ys zs 𝑔 = for 𝑘 from 0 to 𝑛 -1 do let 𝑦 = dequeue ys in let 𝑧 = 𝑔 𝑦 in zs[𝑖] na ← 𝑧 done

Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021.

Following Iris notations, 𝐼 is an invariant whose content is the assertion 𝐼 , and ⊲ is a step-indexing modality, a technicality of Iris that we can ignore in this paper.

In Iris terms, persistent qualifies an assertion that is duplicable. Once established, such an assertion holds forever.

Ghost names in Iris are identifiers for pieces of ghost state. We say more on this in §4.

An Iris expert may want to conceal the queue invariant, QueueInv 𝑞 𝛾 , inside IsQueue 𝛾 [𝑣 0 , ..., 𝑣 𝑛-1 ]. However, we need to access this invariant at various places other than the commit point. This is feasible with a more elaborate definition of logically atomic triples than the one given in this paper, so that they support aborting[START_REF] Jung | Logical Atomicity in Iris: the Good, the Bad, and the Ugly[END_REF]]. Another drawback is that we would lose the timelessness of the representation predicate.Proc. ACM Program. Lang., Vol.

5, No. ICFP, Article 66. Publication date: August 2021.

[START_REF] Stephen Dolan | Bounding data races in space and time[END_REF] call these views frontiers.Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article

Publication date: August 2021.

An equivalent definition is the following: asserting 𝑃 @ V is asserting that, even without other knowledge, if we have the knowledge contained in V, then 𝑃 holds. In other words, 𝑃 @ V is objective and entails ↑ V - * 𝑃 .

This is not entirely true: the implementation shown in §3 does create a happens-before relationship from the dequeuer of rank 𝑘 to the enqueuer of rank 𝑘 + 𝐶 (hence also to all enqueuers of subsequent ranks). We choose to not reveal this in the specification, since the constant 𝐶 is an implementation detail.Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021.

This single-value points-to assertion effectively forbids reasoning about races on non-atomic cells. The operational semantics of[START_REF] Stephen Dolan | Bounding data races in space and time[END_REF] is more general, as it gives a well-defined (albeit nondeterministic) semantics to racy uses of non-atomic cells.

Actually, we need not remember the full rank 𝑘: only the cycle, 𝑘 ÷ 𝐶, is needed.

The code does not distinguish between these two causes, but this is feasible with only one more test.Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021.

Technically, the public state of the queue may contain less than 𝐶 elements in this case, so that we may consider it is not full. Here, by "full" we mean that the next buffer slot is either not reclaimed by anyone or still in the process of being emptied by another thread. Even though the buffer is "full", it may have available slots if dequeuing has completed more rapidly in these other slots.Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021.

Overwriting the extracted value with a unit value () is unnecessary for functional correctness but it prevents memory leaks.Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021.

The full definition of logically atomic triples allows to access the precondition atomically before the commit point, hence without turning it into the postcondition. This is called aborting; it is not needed in our proof, and out of the scope of this paper.Proc. ACM Program. Lang., Vol. 5, No. ICFP, Article 66. Publication date: August 2021.

𝛾 : Auth(Ex(View×View×List(Val×View))) IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )] ≜ • (T , H, [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )]) 𝛾 (a) Ghost state describing the public state After unfolding the logically atomic triple, we must prove wp (try_enqueue 𝑞 𝑣) {Ψ} for any Ψ, when in the proof context we have the internal invariant of the queue (with ghost variables 𝛾, 𝛾 mono , 𝛾 tokens ) as well as the atomic update whose precondition and postcondition are that of the triple above. We then step through the program using usual weakest-precondition calculus.

The first interesting step is the atomic read of head. The ownership of that reference is shared in the invariant of the queue. Hence, to access it, we must open the invariant; then we get the points-to assertion, we can step through the read operation, return the points-to assertion and close the invariant again. After we have done so, and thus forgotten all the quantities which are existentially quantified inside that invariant, we learn little about the value that has just been read, excepted that it is a non-negative integer, say 𝑘.

The second interesting step is the atomic read at index 𝑘 of the array statuses. Again the invariant owns this cell, so we open it around the read instruction. This read yields some value 𝑠 1 and, since it is atomic, it also augments our current (thread) view with the view S 1 which, at this moment, is stored in this cell. In other words, we gain the (persistent) assertion ↑ S 1 . We can remember more information before closing the invariant: indeed, from the authority of 𝛾 mono found in the invariant, we derive a witness for the strict monotonicity of the status that we just read:

Next, the program tests whether 𝑠 1 = 2𝑘. If the test fails, then the program returns false. In this case, we have to provide as postcondition of the logically atomic triple the untouched representation predicate that is in its precondition (IsQueue 𝛾 T H [(𝑣 0 , V 0 ) , ..., (𝑣 𝑛-1 , V 𝑛-1 )]). We do this by committing the atomic update in a trivial way, then conclude the proof.

If 𝑠 1 = 2𝑘, the program proceeds to performing CAS head 𝑘 (𝑘 + 1). To access head, we open the invariant again. If that operation fails, the program also returns false and, after closing the invariant without having updated ghost state, we conclude as before.

If the CAS succeeds, then a number of things happen logically. First, if ℎ and 𝑡 are the values of head and tail at the moment of the CAS, then ℎ = 𝑘. Second, we deduce that the buffer is not full, i.e. ℎ < 𝑡 + 𝐶. Indeed, the invariant directly gives us ℎ ≤ 𝑡 + 𝐶; if we had ℎ = 𝑡 + 𝐶, then in particular, 𝑡 ≤ 𝑘 -𝐶 < ℎ, so the invariant would own the following for slot 𝑘 -𝐶:

Because 𝑘 -𝐶 = 𝑘, this implies:

In either case, we get 𝑠 𝑘 < 2𝑘 = 𝑠 1 , which contradicts the monotonicity of the status of that slot. We derive the contradiction by combining the assertion Witness 𝛾 mono 𝑘 𝑠 1 , S 1 that we had since we read the status, and the authority • (𝑠 𝑘 , S 𝑘 )

𝛾 mono that is found in the invariant. Third, we thus know that ℎ -𝐶 ≤ 𝑘 -𝐶 < 𝑡, so that the invariant gives us:

Again the second disjunct is absurd because the status is monotonic. Hence the slot we are claiming is available indeed. From this we get 𝑠 𝑘 = 2𝑘 = 𝑠 1 , the points-to assertion (items[ 𝑘] na -) @ S 𝑘 and the read token of rank 𝑘 -𝐶. The sets of read tokens and write tokens depend on the value of tail and head, and we have just incremented the latter, to 𝑘 + 1, so we destruct the read token of rank 𝑘 -𝐶 and create a write token of rank 𝑘 instead, giving it as payload the item (𝑣, V) that we are trying to enqueue. We use the primitive Cosmo assertion |xs| = 𝑛 to stipulate that the length of a given array is 𝑛 (recall that the array-points-to assertion is shorthand for a separating conjunction of points-to assertions for cells of the array in some range of indices, but it does not state that there are no cells beyond those mentioned).

Proof of the Specification for the Pipeline

We know prove the following result.

Theorem 5.1. The code shown in Figure 11 satisfies the specification appearing in Figure 12.

The proof relies on the assertions presented in Figure 13. The persistent assertion PipeInv 𝑔 𝑓 𝑅 join together the internal invariant of the queue with that of the pipeline. The two assertions PipeF 𝑔 𝑓 𝑅 𝛾 𝛾 f 𝑛 f xs [𝑥 0 , ..., 𝑥 𝑛-1 ] and PipeG 𝑔 𝑓 𝑅 𝛾 𝛾 g 𝑛 g zs [𝑧 0 , ..., 𝑧 𝑛-1 ] are owned by the threads which compute 𝑓 and 𝑔, respectively, and describe their loop invariants.

We again associate the queue to a ghost variable 𝛾. In addition, we use two ghost variables 𝛾 f and 𝛾 g whose values are the current positions 𝑛 f and 𝑛 g of the loops computing 𝑓 and 𝑔, respectively. This ghost state allows both threads, while in their respecting loops, to agree with the shared invariant on these values. At any time, we have 0 ≤ 𝑛 g ≤ 𝑛 f ≤ 𝑛.

• Indices in the range [𝑛 f , 𝑛) have not been processed by 𝑓 yet. Hence, for these indices, we still have the weakest-precondition assertions wp 𝑓 𝑥 𝑘 {-} initially provided to the pipeline. These assertions can be regarded as a permission to run 𝑓 once on the corresponding items.

The thread computing 𝑓 owns these assertions, and it also owns the array xs containing the input items. • Indices in the range [𝑛 g , 𝑛 f ) have been processed by 𝑓 but are yet to be processed by 𝑔.

Hence, we have consumed their initial weakest-precondition assertions, and have obtained weakest-precondition assertions wp 𝑔 𝑦 𝑘 {-} as a result. These assertions are stored in the shared invariant. The invariant also owns the queue ys, whose contents are the intermediate items for exactly this range of indices.

In a weakly consistent setting, new problems arise. As discussed in §2.3, even the definition of linearizability needs special care. [START_REF] Smith | Linearizability on hardware weak memory models[END_REF] propose new definitions of linearizability for the case of weak memory models. In contrast, other authors have developed new kinds of specifications which allow for weak behaviors of the library itself [START_REF] Krishna | Verifying Visibility-Based Weak Consistency[END_REF][START_REF] Emmi | Weak-consistency specification via visibility relaxation[END_REF][START_REF] Raad | On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models[END_REF]]. We found that our method of combining logically atomic triples with views is expressive and allows for concise specifications at the same time. Previous works include the generalization of various methods to weak consistency: Lê et al. [2013b,a] used manual methods directly tied to the axiomatic memory model to prove the correctness of a queue and of a work-stealing algorithm, while [START_REF] Lahav | Owicki-Gries reasoning for weak memory models[END_REF] adapted the Owicki-Gries methodology to the release-acquire fragment of the C11 memory model and applied it to verify a read-copy-update library. The idea of a separation logic for programs with a relaxed memory semantics has been first developed in the RSL logic [START_REF] Vafeiadis | Relaxed separation logic: a program logic for C11 concurrency[END_REF], and further developed in subsequent work [START_REF] Turon | GPS: navigating weak memory with ghosts, protocols, and separation[END_REF][START_REF] Doko | A Program Logic for C11 Memory Fences[END_REF][START_REF] Kaiser | Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris[END_REF][START_REF] Dang | RustBelt meets relaxed memory[END_REF][START_REF] Mével | Cosmo: A Concurrent Separation Logic for Multicore OCaml[END_REF]. None of these papers addressed the problem of the full functional correctness of a data structure. In particular, the specification proposed for a circular buffer in GPS [START_REF] Turon | GPS: navigating weak memory with ghosts, protocols, and separation[END_REF]] is a weak specification in the style of the persistent specification given at the end of §2.2: in contrast to ours, it does not specify in which order the elements leave the queue.