Paul-André Melliès

Léo Stefanesco

AN ASYNCHRONOUS SOUNDNESS THEOREM FOR CONCURRENT SEPARATION LOGIC

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems C S and C L which describe the operational behavior of the Code when confronted to its Environment or Frame -both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ {P }C{Q} defines a winning and asynchronous strategy π Sep with respect to both asynchronous semantics C S and C L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map L : C S → C L from the stateful semantics C S to the stateless semantics C L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

Introduction

A simple way to understand an imperative (possibly nondeterministic) program C is to interpret it as a binary relation [C] ⊆ S × S between machine states s, s ∈ S. In that approach, the statement s[C]s indicates that one execution trace (at least) of the program C has initial state s ∈ S and final state s ∈ S. One practical advantage of this description is that the binary relation [C] abstracts away from the execution traces of the program C, and only retains their initial and final states. However crude, this abstraction is generally sufficient to analyze the properties of sequential imperative programs, and to establish the soundness of Hoare logic. Unfortunately, the abstraction becomes too coarse when one decides to shift to concurrent imperative programs with shared memory and locks, and to establish the soundness of a specification logic like Concurrent Separation Logic (CSL). To that purpose, it has long been recognized that one needs a proper account of the execution traces of the program C, see Brookes [START_REF] Brookes | A semantics for concurrent separation logic[END_REF]. In this paper, we go one step further, and advocate that the soundness theorem of CSL, and more specifically the absence of data races, is intrinsically related to the asynchronous structure of the execution paths of C. Inspired by asynchronous game semantics, we interpret every concurrent imperative program C as a pair of asynchronous graphs C S and C L related by an asynchronous graph homomorphism

L C : C S C L (1.1)
We thus start by recalling the notion of asynchronous graph [START_REF] Melliès | Asynchronous Games: Innocence Without Alternation[END_REF][START_REF] Melliès | Une étude micrologique de la négation[END_REF] before discussing the relationship between time and space separation.

Asynchronous graphs. A graph G = (V, E, ∂ -, ∂ + ) consists of a set V of vertices or nodes, a set of E of edges or transitions, and a source and a target function ∂ -, ∂ + : E → V . An asynchronous graph (G, ) is a graph G equipped with a binary relation between paths f, g : P Q of length 2, with the same source and target vertices. A pair (f, g) such that f g is called a permutation tile and is depicted as a 2-dimensional tile between the paths f = u • v and g = v • u as follows:

v u u v ´(1.2)
The intuition conveyed by such a permutation tile u • v v • u is that the two transitions u and v are independent. For that reason, the two paths u • v and v • u may be seen as equivalent up to scheduling. The binary relation is required to satisfy the following two axioms axiomatic properties below. Axiom 1. The permutation relation is symmetric, in the sense that u • v v • u implies v • u u • v for all transitions u, v, u , v . Axiom 2. In the situation below where u

• w 1 v 1 • u 1 and u • w 2 v 2 • u 2 , one has that v 1 = v 2 if and only if w 1 = w 2 . v  u w  v  u w 
Two paths f, g : M N of an asynchronous graph are equivalent modulo one permutation tile h 1 h 2 when f and g factor as f = d • h 1 • e and g = d • h 2 • e for two paths d : M P and e : Q N . We write f ∼ g when the path f : M N is equivalent to the path g : M N modulo a number of such permutation tiles. Note that the relation ∼ is symmetric, reflexive and transitive, and thus defines an equivalence relation, closed under composition.

Separation in space and time. The 2-dimensional permutation tiles f g provide a topological means to reflect the temporal nature of independence in concurrency theory. Every permutation tile (1.2) indicates that the two transitions u and v are independent in time: they may be equivalently executed in the sequential order u • v or in the sequential order v • u . Although all the asynchronous graphs considered in this paper are discrete, it is enlightening to take the topological intuition of "homotopy" seriously, and to imagine that the path u • v could be transformed "continuously" into the path v • u by a sequence of local deformations of the form v u u v ás it would be possible if one embedded our asynchronous graphs (G, ) in the topological framework of directed homotopy, see [START_REF] Fajstrup | Directed Algebraic Topology and Concurrency[END_REF]. In the same spirit, we could replace our 2dimensional graphs by higher-dimensional automata admitting n-dimensional cubes [START_REF] Pratt | Modeling Concurrency with Geometry[END_REF].

Interestingly, in practical situations, the temporal independence of two transitions u and v is not primitive: it is a consequence of their spatial separation. In that respect, the idea of temporal independence may be seen as a layer of abstraction above the more concrete and machine-dependent idea of spatial separation. We illustrate this basic but important point by constructing an asynchronous graph (G, G ) based on a very simple machine model, consisting of

• a countable set Var of variables, written x, y, . . . ,

• a countable set Val of values, written v, w, . . . ,

• a countable set Loc ⊆ Val of memory locations, written . A memory state µ = (s, h) of the machine is defined as a pair consisting of two partial functions s : Var fin Val h : Loc fin Val (1.3) with finite domains, called the stack s and the heap h of the memory state µ. The instructions m of our machine are of three kinds:

x := v x := [ ] [ ] := x (1.4)
where (1) the instruction x := v assigns a value v to the variable x, (2) the instruction x := [ ] loads the value h( ) at location and assigns it to the variable x, and (3) the instruction [ ] := x stores at location the current value s(x) of the variable x. The asynchronous graph (G, G ) is defined in the following way. Its nodes are the memory states (1.3) of the machine, and its transitions are of the form (s, h) (s , h)

x:=v when s = s{x → v}, (s, h) (s , h)

x:=[ ] when h( ) is defined and s = s{x → h( )}, (s, h) (s, h )

[ ]:=x when s(x) is defined and h = h{ → s(x)}.

Here, we use the following convenient notation: given a partial function f : X fin Y with finite domain between two sets X and Y , and an element y ∈ Y , we write f {x → y} : X fin Y for the partial function with finite domain defined as

f {x → y} : x → f (x) when x = x, y when x = x.
In order to define the permutation tiles of the asynchronous graph (G, G ), one observes that every transition u : (s, h) (s , h ) m performed by an instruction m reads and writes on a specific area rd(u) ⊆ Var + Loc wr(u) ⊆ Var + Loc of the memory of the machine, which we shall call its footprint. This footprint may be computed from the instruction m performing the transition u = (µ, m, µ ) in the following way:

rd(x := v) = ∅ wr(x := v) = {x} rd(x := [ ]) = { } rd([ ] := x) = {x} wr(x := [ ]) = {x} wr([ ] := x) = { }
Now, suppose given two transitions u : µ → µ 1 and v : µ → µ 2 starting from the same memory state µ in the graph G. The two transitions u and v are declared independent when

(rd(u) ∪ wr(u)) ∩ wr(v) = ∅ and wr(u) ∩ (rd(v) ∪ wr(v)) = ∅.
Note that the independence of the transitions u and v is a consequence of their spatial separation. It is not difficult to see that for every pair of such independent transitions

u : µ 1 µ 2 m 1 v : µ 2 µ 3 m 2
there exists a unique memory state µ 2 such that

u : µ 2 µ 3 m 1 v : µ 1 µ 2 m 2
are transitions of the graph G. In that case, we say that u is the residual of u after v and, symmetrically, that v is the residual of v after u. This basic confluence property leads us to the following definition. A permutation tile of the form (1.2)

u • v G v • u
in the asynchronous graph (G, G ) is defined as a pair of independent transitions u and v where the transition u is defined as the residual of u after v, and the transition v is defined as the residual of v after u. It is not difficult to see that the graph G = (V, E) of memory states and transitions between them, together with the notion of permutation tile u•v G v •u just defined, satisfy the axioms required of an asynchronous graph (G, G ).

Stateful

L : (G, G ) -→ (H, H ) (1.5)
which maps every memory state µ to the node * , and every instruction to itself. We recall the definition of such a homomorphism: Definition 1.1 (homomorphism). An asynchronous graph homomorphism

F : (G, G ) -→ (H, H ) (1.6)
is a graph homomorphism F : G → H between the underlying graphs, such that

u • v G v • u ⇒ F(u) • F(v ) H F(v) • F(u )
for all transitions u, u , v, v of the asynchronous graph G.

Note that, in that situation, one has

f ∼ g ⇒ L(f) ≈ L(g)
for all paths f, g : M N in G, where ≈ denotes the permutation equivalence in the asynchronous graph (H, H ).

Data races as topological obstructions.

The reason for the liberal definition of H is that nothing should forbid two instructions m 1 and m 2 to commute at the stateless level of abstraction. By way of illustration, there exists a permutation tile in H (depicted below in light yellow) which permutes the two instructions x := 2 and x := 3 in the following way:

x := 2 x := 3 x := 3 x := 2 (1.7)
This permutation tile (1.7) should be understood as a basic example of data race in the machine, where the two instructions x := 2 and x := 3 compete for the same variable x. As a matter of fact, one key observation and guiding idea of the paper is that such a data race may be detected by the fact that it defines a permutation tile in the stateless semantics (H, H ) which does not lift along L to a permutation tile in the stateful semantics (G, G ). This line of thought leads us to the following definitions of 1-fibration and 2-fibration.

Definition 1.2 (1-fibration

). An asynchronous graph homomorphism F : (G, G ) → (H, H ) is called a 1-fibration when for every node x of G and transitions v : F(x) → z, there exists a transition u : x → y such that F(u) = v.

Definition 1.3 (2-fibration). An asynchronous graph homomorphism

F : (G, G ) → (H, H )
is called a 2-fibration when for every pair of transitions u and v defining a path u • v of length 2 in G and for every permutation tile

F(u) • F(v ) H b • a in H, there exists a pair of transitions v and u in G such that u • v G v • u and F(v) = b and F(u ) = a .
Coming back to our construction, our point is that the asynchronous graph homomorphism L defined in (1.5) is not a 2-fibration because of the presence of data races such as (1.7) in the stateless semantics. Typically, any sequence of transitions in (G, G )

µ 1 µ 2 µ 3 x:=2 x:=3
(1.8) mapped by L to the upward border * * *

x:=2 x:=3

of the permutation tile (1.7) in the asynchronous graph (H, H ) satisfies µ 2 (x) = 2 and µ 3 (x) = 3. For that reason, there exists no way to lift the permutation tile (1.7) along L and to permute the sequence of instructions (1.8) accordingly in (G, G ) as follows:

µ 1 µ 2 µ 3 x:=3 x:=2
(1.9) because this would mean that µ 3 (x) = 2, and this would contradict the fact that µ 3 (x) = 3. More generally, every data race in the machine may be detected as a topological obstruction to the fact that the stateful-to-stateless homomorphism L is a 2-fibration. Note that, in the same way but for different reasons, the data race between the two instructions x := 1 described by the permutation tile in H below

x := 1

x := 1

x := 1

x := 1

(1.10)

does not lift along L to a permutation tile in G. Indeed, the instruction x := 1 : µ → µ starting from any memory state µ has the nontrivial footprint wr(x := 1) = {x}, and is thus not independent of itself in the asynchronous graph (G, G ).

An asynchronous semantics of code. The machine just considered is a very elementary toy model, which can be easily extended with locks and with memory allocation and deallocation. Also, more than in the machine itself, we are interested in the asynchronous description of the code C we want to analyse. We thus need to explain how we shift from the machine to the code. Interestingly, the story remains essentially the same. The asynchronous soundness theorem. As in the case of the machine model, the data races produced by the program C will be detected as obstructions to the fact that L C is a 2-fibration. Typically, the program C defined as x := 2 ; x := 3 is data-race-free because the permutation tile (1.7) does not appear in the stateless semantics C L , while the program C defined as x := 2 x := 3 produces a data race reflected by the fact that the permutation tile (1.7) appears in the stateless interpretation C L and cannot be lifted along L to the stateful interpretation C S .

In the present paper, we carry on our game-theoretic investigation of Concurrent Separation Logic (CSL) initiated in [START_REF] Melliès | A Game Semantics for Concurrent Separation Logic[END_REF] and establish that well-specified programs are data-race-free. We achieve this by interpreting every derivation tree . . . π Γ {P }C{Q} (1.12) of CSL as an asynchronous strategy π Sep playing on the asynchronous game of separated states. Our asynchronous version of the Soundness Theorem is then formulated in the following fibrational way. Suppose that a code C comes equipped with a proof of the Hoare triple Γ {P }C{Q} in CSL, and consider the asynchronous subgraph {P }C τ S obtained by restricting C S to the nodes reachable from an initial node satisfying the precondition P . In that situation, we establish (see Thm. 8.3 in §8 for details) that Asynchronous Soundness Theorem. The stateful-to-stateless homomorphism L C : C S → C L is a 2-fibration when restricted to the asynchronous subgraph {P }C τ S . The 2-fibrational property is conceptually new and provides the first structural explanation for the absence of data races in concurrent programs specified by CSL.

Related works.

Stephen Brookes established the first proof of soundness of CSL in [START_REF] Brookes | A semantics for concurrent separation logic[END_REF], using a stateless trace semantics similar to C L for the concurrent imperative programs. More recently, Viktor Vafeiadis [START_REF] Vafeiadis | Concurrent Separation Logic and Operational Semantics[END_REF] gave a new proof of soundness, based this time on a stateful operational semantics, similar to C S . Our approach can be seen as unifying the two schools of semantics, by revealing the asynchronous graph morphism (1.11) between them. Also, one main benefit of our asynchronous approach is that we can directly describe and analyze the concurrent execution of two instructions.

In the same way as we do here, Jonathan Hayman and Glynn Winskel [hayman-Winskel] establish the soundness of CSL in a "truly concurrent" setting. They interpret programs as Petri nets, where the interference of the environment is modeled by adding events to the Petri net. In contrast to our work, precision of the invariants is necessary for their semantics to work whereas [START_REF] Gotsman | Precision and the Conjunction Rule in Concurrent Separation Logic[END_REF] has shown that precision is only needed in order to interpret properly the conjunction rule of CSL. Another difference is that they consider a language somewhat different from Brookes' original language [START_REF] Brookes | A semantics for concurrent separation logic[END_REF], without local variables, but with dynamic binding of resources.

We give in [START_REF] Melliès | A Game Semantics for Concurrent Separation Logic[END_REF] a game-theoretic interpretation of CSL, where every Hoare triple is interpreted as a game between Adam and Eve, and every derivation tree π as a winning strategy for Eve in that game. Every program is interpreted there as a set of purely sequential traces. For that reason, it is not possible to establish in this framework the absence of data races, at least in a nice and conceptual way. One main achievement of the paper is thus to define a properly asynchronous game semantics of CSL, and to derive for the first time the absence of data races from purely semantic considerations on the model. Synopsis of the paper. After the machine states and instructions are described in §2, we construct in §3 the two asynchronous graphs S and L defining our stateful and stateless machine models. We then explain in §4 how to interpret every code C as a pair C S and C L of asynchronous transition systems (ATS) with respective machine models S and L . Once the notions of logical state and of separated state are recalled in §5 and in §6, we explain in §7 how to interpret every proof π of CSL as an asynchronous strategy π Sep playing on the machine model Sep of separated states. From this, we establish our asynchronous soundness theorem in §8, and conclude in §9.

Machine states and machine instructions

We introduce below the notions of machine state and of machine instruction which will be used throughout the paper. We suppose given countable sets

MState = State × ℘ (LockName) + { }
A machine step is defined as a labeled transition between machine states. There are two kinds of transitions:

(µ, L) (µ , L ) m (µ, L) m (2.1)
depending on whether the instruction m ∈ Instr has been executed successfully (on the left) or has produced a runtime error (on the right). In particular, has no successor. The machine instructions m ∈ Instr which label the machine steps are of the following form:

m ::= x := E | x := [E] | [E] := E | nop | x := alloc(E, ) | dispose(E) | P (r) | V (r)
where x ∈ Var is a variable, r ∈ LockName is a resource name, is a location, and E, E are arithmetic expressions, possibly with "free" variables in Var. For example, the instruction x := E executed in a machine state s = (µ, L) assigns to the variable x the value E(µ) ∈ Val when the value of the expression E can be evaluated in the memory state µ, and produces the runtime error otherwise. The instruction P (r) acquires the resource variable r when it is available, while the instruction V (r) releases it when r is locked, as described below:

E(µ) = v (µ, L) (µ[x → v], L) x:=E E(µ) not defined (µ, L) x:=E r / ∈ L (µ, L) (µ, L {r}) P (r) r / ∈ L (µ, L {r}) (µ, L) V (r)
The inclusion Loc ⊆ Val means that an expression E may also denote a location. In that case, [E] refers to the value stored at location E in the heap. The instruction x := alloc(E, ) allocates some memory space on the heap at address ∈ Loc, initializes it with the value of the expression E, and assigns the address to the variable x ∈ Var if location was free, otherwise there is no transition. dispose(E) deallocates the location denoted by E when it is allocated, and returns otherwise. Finally, the instruction nop (for no-operation) does not alter the state.

Asynchronous Machine Models

As explained in the introduction, machine models are described using asynchronous graphs. Since we consider stateful as well as stateless descriptions of the machine and of the code, we will consider two kinds of machine models, organized into a pair of asynchronous graphs: the stateful model S based on machine states, and the stateless model L based on locks. Their tiles will be defined using the notion of footprint, which summarizes which area of the state (memory, locks) an instruction relies on, and how it uses it. In both cases, we write footprint s (m) for the footprint of an instruction m in state s, omitting the subscript when it is clear from the context. Our machine models S and L are parameterized over the finite set Locks ⊆ LockName of locks, or resources, which are considered well-defined. We sometimes write S (Locks) or L (Locks) to make it explicit.

The stateful model. A machine state footprint

ρ ∈ ℘ (Var + Loc) × ℘ (Var + Loc) × ℘ (Locks) × ℘ (Loc)
is, made of: (i) rd(ρ), the part of the memory that is read, (ii) wr(ρ), the part of the memory that is written, (iii) lock(ρ), the locks that are touched, and (iv) mem(ρ) the addresses that are allocated or deallocated. Two footprints ρ and ρ are declared independent when:

( rd(ρ ) ∪ wr(ρ ) ) ∩ wr(ρ ) = ∅ ( rd(ρ ) ∪ wr(ρ ) ) ∩ wr(ρ ) = ∅ lock(ρ) ∩ lock(ρ ) = ∅ mem(ρ) ∩ mem(ρ ) = ∅
The stateful model S is the following asynchronous graph: its nodes are the machine states in MState, its transitions are of the form

(µ, L) m ---→ (µ , L ) or (µ, L) m ---→
corresponding to the machine steps, defined in §2. The asynchronous tiles of S are the squares of the form

s m ---→ s 1 m ----→ s ∼ s m ----→ s 2 m ---→ s
where their footprints are independent in the sense above.

The stateless model. A lock footprint

ρ ∈ ℘ (Locks) × ℘ (Loc)
is made of a set of locks lock(ρ) and a set of locations mem(ρ). Two such footprints are independent when their sets are componentwise disjoint. The stateless model L is defined in the following way: its nodes are the subsets of Locks, and its transitions are all the edges of the form (note the non-determinism)

L P (r) ----→ L {r} L alloc( ) ------→ L L τ --→ L L {r} V (r) ----→ L L dispose( ) -------→ L L m ---→
where m is a lock instruction of the form:

P (r) | V (r) | alloc( ) | dispose( ) | τ
for ∈ Loc and r ∈ Locks. The purpose of these transitions is to extract from each instruction of the machine its synchronization behavior. An important special case, the transition τ represents the absence of any synchronization mechanism in an instruction like

x := E, x := [E] or [E] := E .
The asynchronous tiles of L are the squares of the form

L x ---→ L 1 y ---→ L ∼ L y ---→ L 2 x ---→ L
when the lock footprints of x and y are independent. It is worth noting that L may be equal to in such an asynchronous tile. Note that the asynchronous graph L is more liberal than S about which footprints commute, because it only takes into account the locks as well as the allocated and deallocated locations. As explained in the introduction, this mismatch enables us to detect data races in the machine as well as in the code.

Remark. The last component mem(ρ) in the machine state footprint as well as in the lock footprint enables us to forbid a deallocation followed by an allocation to happen at the same address without some kind of synchronization, both at the stateful and stateless level. This is consistent with practice, since the malloc implementation would typically synchronize its accesses to the free-list(s) of the different threads.

Asynchronous Semantics of Code

In this section, we associate to every program C a pair of asynchronous transition systems C S and C L over the machine models S and L introduced in the previous section. The first interpretation C S is stateful and describes how each instruction of the program C acts on the memory states and on the locks. The second interpretation C L is stateless and only remembers the action of the instructions on the locks.

Asynchronous transition systems (ATSs).

Asynchronous transition systems (ATSs) are specific asynchronous graphs where every transition is either executed by Code or by Frame. We thus start by introducing the following notion:

Definition 4.1 (Asynchronous graph with polarities). An asynchronous graph with polarities is an asynchronous graph (G, G ) where every transition is assigned a polarity Code or Frame. One requires that in every permutation tile u • v G v • u , the two transitions u and u (symmetrically v and v ) have the same polarity.

A path in an asynchronous graph G with polarities is called Code-proper when it contains (at least) one Code transition. A node x is called initial in G when there are no Code-proper incoming paths into x, and final when there are no Code-proper outgoing paths from x. The sets of initial and final nodes in G are denoted ∂ 0 G and ∂ 1 G, respectively. The graph G is called Code-acyclic when there are no Code-proper cycles, that is, every cycle of the graph G contains only Frame transitions. A set S of nodes of a graph is forward-closed when x ∈ S and x → y implies that y ∈ S.

λ G : (G, G ) ---→ ( , )
One requires moreover that 1. the map λ G defines a bijection between the set ∂ 0 G of initial nodes and the set of nodes of , and an injection from the set |G| of returning nodes into the set of nodes of .

2. the map λ G is a Frame 1-fibration, in the sense that for every transition v : λ G (x) → z in the machine model , there exists a unique Frame transition u :

x → y in G such that λ G (u) = v : λ G (x) → λ G (y),
3. the map λ G is a Code-Frame and Frame-Frame 2-fibration, in the sense that for every sequence of transitions

x y z u v
in G where v : y → z is a Frame transition, and for every permutation tile in of the form:

u λ ( ) G λ ( ) G v b a (4.1)
there exists a sequence of transitions

x y z v u and a permutation tile u • v G v • u in G transported by λ G to the permutation tile (4.1) in the sense that λ G (x) • λ G (z) λ G (v) λ G (u ) = λ G (x) • λ G (z) b a
Notation. We often find convenient to label the transitions u : x → y in G with the instruction or lock instruction m which labels the transition λ G (u) in the underlying asynchronous graph S or L . We also write m : C or m : F to mean that the transition u : x → y has the polarity Code or Frame in G, respectively.

Basic constructions on ATSs.

The asynchronous interpretations C S and C L of the program C are performed by structural induction, using a number of primitive operations on ATSs defined below. Note that whenever a construction makes some nodes unreachable from the initial nodes, they are implicitly removed.

Sum. The sum of two ATSs G 1 and G 2 with same machine model , written

G 1 ⊕ G 2 ,
is the disjoint union of the two asynchronous graphs G 1 and G 2 , where we identify their respective initial and returning states together, when they have the same image under λ G 1 and λ G 2 . This means that for the case of the returning states, there are three cases. Parallel product. The parallel product G 1 G 2 of two ATSs G 1 and G 2 over the same machine model is defined as follows. The nodes of G 1 G 2 are the pairs of nodes

x 1 | x 2 ∈ G 1 × G 2 such that λ G 1 (x 1 ) = λ G 2 (x 2 ) and λ G 1 G 2 (x 1 , x 2
) is defined to be that common value. The transitions of G 1 G 2 are of three kinds:

1. the Code transitions x 1 |x 2 m : C -----→ x 1 |x 2 where x 1 m : C -----→ x 1 in G 1 and x 2 m : F -----→ x 2 in G 2 . 2. the Code transitions x 1 |x 2 m : C -----→ x 1 |x 2 where x 1 m : F -----→ x 1 in G 1 and x 2 m : C -----→ x 2 in G 2 . 3. the Frame transitions x 1 |x 2 m : F -----→ x 1 |x 2 where x 1 m : F -----→ x 1 in G 1 and x 2 m : F -----→ x 2 in G 2 .
Note that every transition u :

x 1 |x 2 → y 1 |y 2 in the graph G 1 G 2 is a pair u = (u 1 , u 2 ) also written u = u 1 |u 2 of a transition u 1 : x 1 → y 1 in G 1 and u 2 : x 2 → y 2 in G 2 . A permutation tile in G 1 |G 2 v x  x y   y z   z y   y ´  v u   u ´ú   u ´v   v
is then defined as a square whose projections

v x y  z  y   u  ú v v x y  z  y   u  ú v define permutation tiles in (G 1 , 1
) and (G 2 , 2 ), respectively. Finally, the returning nodes

x 1 |x 2 ∈ |G 1 ||G 2 | are defined as the pairs x 1 |x 2 of returning nodes x 1 ∈ |G 1 | and x 2 ∈ |G 2 |.
The parallel product of G 1 and G 2 is asynchronous in the sense that every Code transition in G 1 G 2 is a Code transition performed by G 1 and seen as a Frame transition by G 2 , or symmetrically, a Code transition performed by G 2 and seen as a Frame transition by G 1 . In particular, by definition, the two components G 1 and G 2 never execute (or "fire") a Code transition simultaneously in G 1 G 2 . At the level of permutation tiles, a Resource hiding. In order to interpret the resource introduction construct resource r do C, we introduce a hiding operator hide[r] on ATSs which hides the new resource r, similarly to the operator ν in the π-calculus. Formally, if G is an ATS over (Locks {r}), then hide[r](G) is the ATS over (Locks) where: (1) the resource r has been removed from the sets of locked resources of all states, (2) the Code transitions P (r) and V (r) are replaced with nops, (3) the Frame transitions P (r) and V (r) are removed from the graph G, and (4) the remaining permutation tiles are preserved. Moreover, we only keep as initial and returning states the initial and returning states x of G such that the resource r is not held in λ G (x).

Critical sections. Dually, inside critical sections, we need to "lift" ATSs over some set Locks of locks to ATSs over Locks {r}. This can be done naturally in this case because we know that, during the critical section, the resource r is held by the Code. Formally, when[r](G) has the same underlying asynchronous graph as G, where λ := λ when[r](G) is defined by:

λ (x) := L {r} if λ G (x) = L λ (x) := (µ, L {r}) if λ G (x) = (µ, L).
This does not define an ATS yet, for conditionň3 is not satisfied: there are not enough Environment transitions. This is why we must freely add Frame transitions and new nodes to make it an ATS. The returning nodes are defined to be the same as G.

Other constructions on ATSs. Given an ATS G and a Boolean formula B, we define whentrue[B](G) as the graph G where, among the Code transitions out of initial nodes, we only keep those where B holds on λ G (x). Then, we remove the nodes made unreachable by this edge removal. Similarly, we define whenfalse[B] for when B does not hold. Finally, whenabort[B] is the graph with transitions from the initial states where B errors out, because it tries to read undefined variables, to . Note that in the case of the C L semantics, since the nodes do not contain information on the state, the first two constructions above are the identity. This means that we sometimes consider impossible branches.

4.3. Asynchronous semantics of the code. We explain how to give a semantics to any code C as an ATS C , by induction on its structure. This lets us build C S and C L in the same way. First, we give the syntax of our imperative concurrent language, which we borrow from [START_REF] Brookes | A semantics for concurrent separation logic[END_REF][START_REF] Vafeiadis | Concurrent Separation Logic and Operational Semantics[END_REF].

B ::= true | false | B ∧ B | B ∨ B | E = E E ::= 0 | 1 | . . . | x | E + E | E * E C ::= x := E | x := [E] | [E] := E | C; C | C 1 C 2 | skip | while B do C | resource r do C | with r when B do C | if B then C 1 else C 2 | x := malloc(E) | dispose(E)
Semantics of instructions. To every instruction m ∈ Instr, we associate the ATS m with machine model defined as two copies 0 + 1 (called source and target) of the asynchronous graph . Every transition in 0 + 1 is assigned the Frame polarity. To this, one adds a Code transition x 0 → y 1 for every transition of the form (2.1) labeled by m in the small step semantics. Here, x 0 and y 1 are the nodes x and y of taken in the source and target components 0 and 1 of m , respectively. The transition x 0 → y 1 is mapped by λ m to the transition associated to the small step transition (2.1) in = S or = L . Finally, one adds a Code-Frame permutation tile in m for each Code-Frame permutation tile in , in such a way that λ m : m → defines a Code-Frame 2-fibration.

Leaf codes. For leaf codes that correspond to instructions (all, except for malloc), their semantics is the same as that of the instruction. For malloc(E), we take the non-deterministic union of all the alloc(E, ):

malloc(E) := ∈Loc alloc(E, )
Conditionals. Conditional branching is interpreted as

if B then C else C 1 = whentrue[B]( nop ) ; C 1 ⊕ whenfalse[B]( nop ) ; C 2 ⊕ whenabort[B]
The nops are needed because the environment can interfere between the evaluation of B and the beginning of the execution of C i .

Sequential and parallel compositions. We use the sequential and parallel product of ATSs with machine models defined in §4.2, in the following way:

C 1 C 2 = C 1 C 2 C 1 ; C 2 = C 1 ; C 2 .
Resource introduction. The interpretation of resource r do C is defined as

resource r do C = hide[r] C
Critical sections. The semantics with r when B do C is defined using the sequential composition above and whentrue:

whentrue[B] P (r) ; when[r] C ; V (r) ⊕ whenabort[B].
Loops. For loops, the interpretation of C = while B do C is defined as the (possibly infinite) least fixpoint of the function F :

F (G) = whentrue[B] nop ; C ; G ⊕ whenfalse[B] nop ⊕ whenabort[B].
Remark. The map λ G is a 2-fibration for Code-Frame and Frame-Frame permutations, but not for Code-Code permutations in general. Consider for instance the interpretation of the program C = resource r do (P (r); V (r)) (P (r); V (r)) where r ∈ LockName is a resource name. Since the resource introduction performed by resource r do C is interpreted by hiding the resource r, the two instructions P (r) and V (r) are both transformed in nops instructions. However the two nops do not form a tile! Another example is, of course, the sequential composition C 1 ; C 2 of two codes C 1 and C 2 . 4.4. Comparing the stateful and the stateless semantics. We construct a category of ATSs with machine models, in the following way. A morphism between ATSs with machine models

λ G 1 : G 1 -→ 1 λ G 2 : G 2 -→ 2
is a pair of asynchronous graph morphisms

F : 1 → 2 and G : G 1 → G 2 such that the diagram below commutes: G 1 G 2 1 2 G λ G 1 λ G 2 F
One requires moreover that G send initial (resp. returning) nodes of G 1 to initial (resp. returning) nodes of G 2 . This defines a category noted ATS. Let F : S → L denote the asynchronous graph morphism which transports every machine state s = (µ, L) to the underlying subset L ⊆ Locks of locks held in s. Every instruction m ∈ Instr comes equipped with an ATS morphism

L m = (F, G m ) : m S ---→ m L
where the asynchronous graph morphism G m is defined as

(µ, L) m -→ (µ , L ) ---→ L m -→ L
Because the stateful and stateless interpretations -S and -L are defined using the same functorial operations over F, we can associate to every code C a morphism of ATS L C = (F, G C ) :

C S ---→ C L
starting from the family of morphisms L m associated to instructions. Note that this morphism L C = (F, G C ) living in the category ATS plays a fundamental role in the present work, since our asynchronous refinement of the original Soundness Theorem for CSL relies on it, see §8 for details.

Logical States

As discussed in [START_REF] Melliès | A Game Semantics for Concurrent Separation Logic[END_REF], reasoning about concurrent programs in separation logic requires to introduce an appropriate notion of logical state, including information about permissions. The version of concurrent separation logic we consider is almost the same as its original formulation by O'Hearn and Brookes [START_REF] O'hearn | Resources, Concurrency, and Local Reasoning[END_REF][START_REF] Brookes | A semantics for concurrent separation logic[END_REF]. One difference is that we benefit from the work of Bornat, Calcagno, O'Hearn, Parkinson and Yang in [Bor+05; BCY06; PBC06] and use permissions p and the predicate Own p (x) in order to handle the heap as well as variables in the stack. We suppose given an arbitrary partial cancellative commutative monoid Perm which we call the permission monoid, following [START_REF] Bornat | Permission Accounting in Separation Logic[END_REF]. The element will be used as the permission required for a program to write somewhere in memory. We thus require that does not admit any multiples, ie. ∀x ∈ Perm, • x is not defined. The intuition (which we will need to turn into a theorem) is that we prevent in this way concurrent mutation and observation of the same location, that is, data races. The set LState of logical states is defined in much the same way as the set State of memory states, with the addition of permissions:

LState = (Var fin (Val × Perm)) × (Loc fin (Val × Perm))
The main benefit of permissions is that they enable us to define a separation product σ * σ between two logical states σ and σ , which generalizes the disjoint union. When it is defined, the logical state σ * σ is defined as a partial function with domain

dom(σ * σ) = dom(σ) ∪ dom(σ )
in the following way: for a ∈ Var Loc,

σ * σ (a) =      σ(a) if a ∈ dom(σ) \ dom(σ ) σ (a) if a ∈ dom(σ ) \ dom(σ) (v, p • p ) if σ(a) = (v, p) and σ (a) = (v, p )
The separation product σ * σ of the two logical states σ and σ is not defined otherwise.

In particular, the memory states underlying σ and σ agree on the values of the shared variables and heap locations when the separation product is well defined. The syntax and the semantics of the formulas of Concurrent Separation Logic is the same as in Separation Logic. The grammar of formulas is:

P, Q, R, J ::= emp | true | false | P ∨ Q | P ∧ Q | ¬P | ∀v.P | ∃v.P | P * Q | v p → w | Own p (x) | E 1 = E 2
where x ∈ Var, p ∈ Perm, v, w ∈ Val. Given a logical state σ = (s, h) consisting of a logical stack s and of a logical heap h, the semantics of the formulas, expressed as the predicate σ P , is standard:

σ v p → w ⇐⇒ v ∈ Loc ∧ s = ∅ ∧ h = [v → (w, p)] σ Own p (x) ⇐⇒ ∃v ∈ Val, s = [x → (v, p)] ∧ h = ∅ σ E 1 = E 2 ⇐⇒ E 1 = E 2 ∧ fv(E 1 = E 2 ) ⊆ vdom(s) σ P ∧ Q ⇐⇒ σ P and σ Q σ P * Q ⇐⇒ ∃σ 1 σ 2 , σ = σ 1 * σ 2
and σ 1 P and σ 2 Q.

The proof system underlying concurrent separation logic is a sequent calculus, whose sequents are Hoare triples of the form Γ {P }C{Q} where C ∈ Code, P , Q are predicates, and Γ is a context, defined as a partial function with finite domain from the set LockName of resource variables to predicates. Intuitively, the context Γ = r 1 : J 1 , . . . , r k : J k describes the invariant J i satisfied by the resource variable r i . The purpose of these resources is to describe the fragments of memory shared between the various threads during the execution.

The inference rules of CSL are given in Figure 1. The inference rule Res associated to resource r do C moves a piece of logical state which is owned by the Code into the shared context Γ, which means that it can be accessed concurrently inside the code C. However, the access to that piece of state is mediated by the with construct, which grants temporary access under the condition that one must give it back (rule With). Note that the rule With has the side condition P ⇒ def(B). This means that if P is true in some logical state, then it implies, for each free variable x of B, that there exists some permission p such that Own p (x) holds.

Aff Γ {(Own (x) * P ) ∧ E = v}x := E{(Own (x) * P ) ∧ x = v} Store Γ {E → -}[E] := E {E → E } x / ∈ fv(E) Load Γ {E → p v * Own (x)}x := [E]{E → p v * Own (x) * x = v} Γ {P }C 1 {Q} Γ {Q}C 2 {R} Seq Γ {P }C 1 ; C 2 {R} P ⇒ def(B) Γ {P ∧ B}C 1 {Q} Γ {P ∧ ¬B}C 2 {Q} If Γ {P }if B then C 1 else C 2 {Q} Γ is precise Γ {P 1 }C{Q 1 } Γ {P 2 }C{Q 2 } Conj Γ {P 1 ∧ P 2 }C{Q 1 ∧ Q 2 } Γ {P 1 }C{Q 1 } Γ {P 2 }C{Q 2 } Disj Γ {P 1 ∨ P 2 }C{Q 1 ∨ Q 2 } Γ, r : J {P }C{Q} Res Γ {P * J}resource r do C{Q * J} P ⇒ def(B) Γ {(P * J) ∧ B}C{Q * J} With Γ, r : J {P }with r when B do C{Q} Γ {P 1 }C 1 {Q 1 } Γ {P 2 }C 2 {Q 2 } Par Γ {P 1 * P 2 }C 1 C 2 {Q 1 * Q 2 } Γ {P }C{Q} Frame Γ {P * R}C{Q * R}
Notice that the context Γ = r 1 : J 1 , . . . , r k : J k is required to be precise in the rule Conj. This means that each of the predicates J i is precise in the following sense: Definition 5.1 (Precise predicate). A predicate P is precise when, for every logical state σ ∈ LState, there exists at most one logical state σ ∈ LState such that σ P and ∃σ ∈ LState, σ = σ * σ .

The machine model of separated states

We recall the notion of separated state formulated in [START_REF] Melliès | A Game Semantics for Concurrent Separation Logic[END_REF] whose purpose is to separate the logical memory state into one region controlled by the Code, one region controlled by the Frame, and one independent region for each unlocked resource. In order to define the notion, we suppose given a finite set Locks ⊆ LockName of resource variables, or locks. Definition 6.1. A separated state is a triple

(σ C , σ, σ F ) ∈ LState × (Locks → LState + {C, F }) × LState
such that the logical state below is defined:

σ C * r∈dom(σ) σ(r) * σ F ∈ LState (6.1)
where

dom(σ) = { r ∈ Locks | σ(r) ∈ LState }, dom C (σ) = { r ∈ Locks | σ(r) = C }, dom F (σ) = { r ∈ Locks | σ(r) = F }.
We say that a separated state (σ C , σ, σ F ) combines into a machine state s = (µ, L) precisely when L = dom C (σ) dom F (σ) and when the function U : LState → State which forgets the permissions transports the logical state (6.1) into the memory state µ ∈ State. Note that, by definition, every separated state (σ C , σ, σ F ) combines into a unique machine state, which we write for concision

(µ, L) = (σ C , σ, σ F ). (6.2)
Interestingly, the notion of separated state comes with the same notion of footprint as the machine states, defined as elements of

ρ ∈ ℘ (Var + Loc) × ℘ (Var + Loc) × ℘ (Locks) × ℘ (Loc).
which describes the footprint of a transition by Eve or Adam.

Definition 6.2. The machine model of separated states Sep is the asynchronous graph whose nodes are the separated states and whose edges are either Adam or Eve transitions:

• Eve transitions are of the form

(σ C , σ, σ F ) m : C ------→ (σ C , σ , σ F )
where m ∈ Instr is an instruction such that

(σ C , σ, σ F ) (σ C , σ , σ F ) m
and such that the following conditions are satisfied:

∀ / ∈wr(m), σ C ( ) = σ C ( ) wr(m) ∪ rd(m) ⊆ dom(σ C ) lock(m) ⊆ dom(σ) ∪ dom C (σ) ∀r / ∈ lock(m), σ(r) = σ (r).
• Adam moves of the form

(σ C , σ, σ F ) m : F ----→ (σ C , σ , σ F )
where m ∈ Instr is an instruction, such that

(σ C , σ, σ F ) (σ C , σ , σ F ) m
and such that the following conditions are satisfied:

∀ / ∈wr(m), σ F ( ) = σ F ( ) wr(m) ∪ rd(m) ⊆ dom(σ F ) lock(m) ⊆ dom(σ) ∪ dom F (σ) ∀r / ∈ lock(m), σ(r) = σ (r).
Like the two other machine models S and L , the tiles of Sep are the squares where the footprints of m and m at state x are independent. More concretely, an Eve-Eve tile is of the following form (where we only write the first component of each separated state):

σ1 * σ2 * σ σ 1 * σ 2 * σ σ 1 * σ2 * σ σ1 * σ 2 * σ m m m m
For example, the first state σ C is split into σ 1 * σ 2 * σ, where the domain of σ 1 is wr(m), that of σ 2 is wr(m ) and σ is the rest of σ C . The resulting definition of the machine model Sep of separated states ensures that the operation (6.2) defines a morphism : Sep → S of asynchronous graphs from Sep to the stateful model S .

An asynchronous semantics of proofs

In this section, we interpret derivation trees (or proofs) of CSL in our asynchronous semantics.

In the same way as we did for the Code in §4, we interpret every proof π of a Hoare triple Γ {P }C{Q} as an asynchronous transition system (ATS, Definition 4.2). The underlying asynchronous machine model is Sep , the graph of separated states. As in the previous case, our ATSs have the 1-fibration property, and moreover the initial states are all the states that satisfy P , and all the final states satisfy Q. The interpretation π Sep also satisfies that the second component σ of all its nodes of π Sep satisfies the invariants of Γ pointwise. In order to define the interpretation of a proof π by induction on its structure, we start by defining a small number of new constructions on ATSs.

The parallel product with separated states. In order to define the parallel product G 1 G 2 of two ATSs on the model Sep of separated states, we need to adapt the compatibility condition given by the equality λ G (x 1 ) = λ G (x 2 ) in the case of the stateful and stateless models S and L . In the case of Sep , two nodes of G 1 and G 2 should be declared compatible when they describe the two "subjective" (and dual) views of the same situation, provided in this case by a separated state of G 1 G 2 . This leads us to the notion of three-party separated state, defined as a tuple (σ 1 , σ 2 , σ * , σ F ) where σ 1 , σ 2 , σ F ∈ LState are logical states, where σ * : Locks → LState + {C 1 , C 2 , F }, and where the product (σ 1 , σ 2 , σ * , σ F ) immediately adapted from (6.1) is well-defined. We define three functions on these new separated states: the "objective" projection, which corresponds to the view of the whole program C 1 C 2 , is defined by:

(σ 1 , σ 2 , σ * , σ C ) → (σ 1 * σ 2 , σ * [C i → C], σ C )
the left and right "subjective" projections

λ 1 : (σ 1 , σ 2 , σ * , σ C ) → (σ 1 , σ * [C 1 → C, C 2 → F ], σ C * σ 2 ) λ 2 : (σ 1 , σ 2 , σ * , σ C ) → (σ 2 , σ * [C 1 → F, C 2 → C], σ C * σ 1 )
which give the state of the program from the point of view of one of the programs in parallel. This leads us to the following definition: Definition 7.1. Two separated states x 1 , x 2 ∈ SState are compatible when there exists a three-party separated state y such that λ 1 (y) = x 1 and λ 2 (y) = x 2 . Note that the three-party separated state y is unique in that case.

Framing. To handle framing (Frame rule), we need to be able to move a piece of (logical) heap from the Frame side to the Code side. First, we define the framing of a logical state σ R . Given an ATS G over Sep , we define frame[σ R ](G) pointwise with:

λ (x) = (σ C * σ R , σ, σ F ) if λ(x) = (σ C , σ, σ F * σ R ) undefined otherwise
Given such a graph G and a predicate R, we define frame[R](G) as the following union of ATSs (defined in §??):

frame[R](G) = σ R R frame[σ R ](G)
Resource introduction. To give a semantics to the resource introduction rule, we need to extend the hiding operator to separated states. More precisely, the action of hide[r], in addition to replacing P (r) and V (r) with nop, is:

(σ C , σ [r → σ], σ F ) → (σ C * σ, σ, σ F ) (σ C , σ [r → C or F ], σ F ) → (σ C , σ, σ F )
Critical sections. Similarly, we extend the definition of when[r](G) to separated states: to the same underlying graph we associate the asynchronous morphism λ defined as

λ (x) = (σ C , σ [r → C], σ F ) if λ G (x) = (σ C , σ, σ F )
We also need to take and release locks in the semantics of the proofs: the ATS acquire[r] is defined by its Eve moves:

(σ C , σ [r → σ], σ F ) P (r) : C -----→ (σ C * σ, σ [r → C], σ F )
and release[r] by (for all σ ∈ LState satisfying r's invariant in Γ):

(σ C * σ, σ [r → C], σ F ) V (r) : C -----→ (σ C , σ [r → σ], σ F ).
Union. It is sometimes necessary to combine in a single asynchronous strategy two asynchronous strategies G 1 and G 2 whose purpose is to justify the transitions performed by the very same Code C. This is precisely the purpose of the disjoint union

G 1 ∪ G 2 . The disjoint union G 1 ∪ G 2 of two
S π 1 ∪π 2 : π 1 Sep ∪ π 2 Sep -→ C S
whereas the homomorphism associated to the sum is of the form:

S π 1 ⊕π 2 : π 1 Sep ⊕ π 2 Sep -→ C S ⊕ C S
The disjoint union S π 1 ∪π 2 may be thus obtained by postcomposing S π 1 ⊕π 2 with the codiagonal of C S :

π 1 Sep ⊕ π 2 Sep C S Sπ 1 ∪π 2 = π 1 Sep ⊕ π 2 Sep C S ⊕ C S C S S π 1 ⊕π 2 codiagonal
Intersection. In order to interpret the introduction rule of the conjunction, we need to define the intersection of two ATSs G 1 and G 2 over the same machine model . The definition of G 1 ∩ G 2 is very similar to the definition of the parallel product. The only difference lies in the fact that the two ATSs G 1 and G 2 must behave synchronously. The nodes of G 1 ∩ G 2 are defined in the same way as the nodes of G 1 G 2 , that is, as the pairs

x 1 & x 2 consisting of a node x 1 of G 1 and of a node x 2 of G 2 , such that λ G 1 (x 1 ) = λ G 2 (x 2 )
There are two types of transitions. The Code transitions which are pairs of Code transitions:

x 1 & x 2 m : C -----→ y 1 & y 2 when x 1 m : C -----→ y 1 ∈ G 1 and x 2 m : C
-----→ y 2 ∈ G 2 and similarly for Frame transitions. A square is a tile in G 1 ∩ G 2 precisely when it is the superposition of two tiles of G 1 and of G 2 .

Machine instructions. The rules that correspond to machine instructions m ∈ Instr (such as Load) are interpreted in the obvious way, always preserving the permission associated to affected locations.

Semantics of proofs.

. . . π 1

Γ {P }C 1 {Q} . . . π 2 Γ {Q}C 2 {R} Γ {P }C 1 ; C 2 {R} Sep = π 1 Sep ; π 2 Sep
For the parallel product rule Par, we use the parallel product of ATSs using the above notion of compatibility: . . .

π 1 Γ {P 1 }C 1 {Q 1 } . . . π 2 Γ {P 2 }C 2 {Q 2 } Γ {P 1 * P 2 }C 1 C 2 {Q 1 * Q 2 } Sep = π 1 Sep π 2 Sep . . . π Γ {P }C{Q} Γ {P * R}C{Q * R} Sep = frame[R] π . . . π Γ, r : J {P }C{Q} Γ {P * J}resource r do C{Q * J} Sep = hide[r] π . . . π Γ, r : J {(P * J) ∧ B}C{Q * J} Γ, r : J {P }with r when B do C{Q} Sep = whentrue[B] acquire[r] ; when[r] π Sep ; release[r] . . . π 1 Γ {P 1 }C{Q 1 } . . . π 2 Γ {P 2 }C{Q 2 } Γ {P 1 ∨ P 2 }C{Q 1 ∨ Q 2 } Sep = π 1 Sep ∪ π 2 Sep
The interpretation of the conjunction rule relies on the intersection of ATSs just defined: . . .

π 1 Γ {P 1 }C{Q 1 } . . . π 2 Γ {P 2 }C{Q 2 } Γ {P 1 ∧ P 2 }C{Q 1 ∧ Q 2 } Sep = π 1 Sep ∩ π 2 Sep
Note that we do not rely on the preciseness of the context Γ to define the interpretation of the Conj proof rule, though precision is needed in order to establish the soundness of the rule.

An asynchronous soundness theorem

At this stage, we are ready to state our soundness theorem for Concurrent Separation Logic. We start by observing that every proof π in CSL of a Hoare triple of the form Γ {P }C{Q} comes equipped with a morphism of asynchronous graphs S π :

π Sep ---→ C S which makes the diagram below commute π Sep C S Sep S Sπ λπ λ C
The morphism S π thus defines a morphism of ATS which relates the interpretation of the proof π with the stateful interpretation of C. For every such proof π of a Hoare triple Γ {P }C{Q}, we write

L π : π Sep ---→ C L for the composite L π = L C • S π below: π Sep C S C L Sπ L C
Our soundness theorem follows from two properties of the asynchronous strategy π Sep associated to a CSL proof tree π. The first property (1-soundness) implies that a wellspecified program does not crash during a valid execution, that is, an execution which starts from a state satisfying the precondition P and where the Frame performs only legal transitions. The second property (2-soundness) implies that such a program does not encounter any data race.

Theorem 8.1 (1-soundness). S π is a Code 1-fibration.

A Code 1-fibration is a 1-fibration (Def. 1.2) where we only ask that Code transitions can be lifted, similarly to axiom 3 of Def. 4.3. This lifting property reflects the fact that the strategy π Sep interpreting the proof π is winning, in the sense that every transition performed by the Code on machine states can be lifted (and thus logically justified) by the strategy into a transition between separated states, see [START_REF] Melliès | A Game Semantics for Concurrent Separation Logic[END_REF] for a discussion. This implies in particular that well specified programs do not go wrong, because the error state cannot be lifted to a separated state. The next statement is of a different nature: it says that the strategy π Sep adapts at the separated level to the possible reorderings of scheduling performed at the stateless level:

Theorem 8.2 (2-soundness). L π is a 2-fibration.
This property implies (in particular) that valid executions of C never produce data races. More deeply, it says that two executions which are equivalent modulo ≈ at the stateless level, in the sense that they behave in the same way with respect to the locks (each thread acquires and releases each lock in the same order), are also equivalent modulo ∼ at the stateful level. To make this statement formal, consider a well-specified program ∅ {P }C{Q} and define {P }C τ S as the subgraph of C S obtained by removing every Frame transition, and keeping only the states which can be reached from an initial node satisfying the precondition P . We are interested in the morphism

L P C : {P }C τ S -→ C L
obtained by restricting L C to the asynchronous subgraph {P }C τ S of C S . This enables us to establish the soundness theorem announced in the introduction:

Theorem 8.3 (Soundness). L P C is a 2-fibration.

Conclusion and future works

For the first time, we devise and establish a properly asynchronous version of the Soundness Theorem for Concurrent Separation Logic (CSL). In our formulation, the absence of data races follows from a more fundamental lifting property of scheduling along the stateful-tostateless translation C S → C L . The proof of the theorem itself is original in design, and relies on the construction of an asynchronous game semantics of CSL, building on the foundations set in [START_REF] Melliès | A Game Semantics for Concurrent Separation Logic[END_REF]. In future work, we wish to adapt this asynchronous semantics of CSL to weak memory models boudol,brookes,Vafeiadis-separation-for-promising,promisingsemantics,Dreyer-weak-memory-iris and to distributed algorithms [START_REF] Gotsman | Cause I'm strong enough: reasoning about consistency choices in distributed systems[END_REF]. In another direction of investigation, we want to extend our version of the soundness theorem to a higherorder and axiomatic setting like Iris [START_REF] Jung | Iris: Monoids and Invariants As an Orthogonal Basis for Concurrent Reasoning[END_REF]. Also, now that the asynchronous soundness theorem has been established by semantic means, a nice and instructive challenge will be to prove it again using purely syntactic techniques, in the line adopted for Mezzo [START_REF] Balabonski | Type Soundness and Race Freedom for Mezzo[END_REF].

S i : π i Sep → C i S
is a 1-fibration on Code transitions, for i = 1, 2. In that case, the asynchronous graph morphism

S : π Sep → C 1 C 2 S is also a Code 1-fibration.
A Code transition in C 1 C 2 S is (without loss of generality) a pair of compatible transitions: one Code transition from C 1 S and one Frame transition from C 2 S . We need to lift this transition into a move in π Sep = π 1 Sep π 2 Sep . Using the induction hypothesis, we can show that Eve can lift the former into π 1 Sep , and we can lift the latter because λ π 2 is a Frame 1-fibration. Therefore, we can lift the Code transition from

C 1 C 2 S into π 1 π 2 Sep .
Proof. Consider a node x in π Sep whose label is (σ C , σ, σ F ), and let s = (σ C , σ, σ F ). Consider a Code transition in C 1 C 2 S of the form (writing the images of the nodes underλ)

s m : C -----→ s (A.1)
whose starting node is S(x). By definition of the parallel product there exists a three-party separated state

(σ 1 , σ 2 , σ, σ F ) whose projection through proj is (σ C , σ, σ F ). By definition of C 1 C 2 S , the transi- tion (A.1) is of the form a 1 |a 2 m : C -----→ b 1 |b 2 with λ 1 (a 1 ) = λ 2 (a 2 ) = s and λ 1 (b 1 ) = λ 2 (b 2 ) = s . Our goal is to find two moves, one in π 1 Sep of the form (σ 1 , σ, σ F * σ 2 ) m : C -----→ (σ 1 , σ , σ F * σ 2 )
that is mapped under S 1 to the transition:

a 1 m ---→ a 2
and one in π 2 Sep of the form

(σ 2 , σ, σ F * σ 1 ) m : F -----→ (σ 2 , σ , σ F * σ 1 )
that is mapped under S 2 to the transition:

b 1 m : F -----→ b 2 .
(Note that we omit to write the change of perspective on the σ.) The first exists according to the hypothesis on S 1 , and the second because λ 2 is a 1-fibration on Frame transitions.

S i : π i Sep → C i S
is a 1-fibration on Code transitions, for i = 1, 2. In that case, the asynchronous graph morphism

S : π Sep → C 1 ; C 2 S
is also a Code 1-fibration. where S(x) = a. Recall that the frame rule is interpreted as

frame[R]( π Sep ) = σ R R frame[σ R ]( π Sep )
Therefore, the node x belongs to one of the copies of frame[σ R ]( π Sep ), for some σ R , and there is a node x above a in π Sep such that

λ(x) = (σ C * σ R , σ, σ F ) and λ (x ) = (σ C , σ, σ F * σ R )
with σ R R. By the hypothesis on S , there is a node y ∈ π Sep and a move

λ (y) = (σ C , σ [r → σ], σ F )
Hence, there is a lifting of t starting from x.

Case 2. Suppose, for example, that m = P (r). In that case, m = nop, and

λ(x) = (σ C * σ, σ, σ F ) and λ (x) = (σ C , σ [r → σ], σ F )
By the hypothesis on S , there is a node y ∈ π Sep and a move

λ (y) = (σ C * σ, σ [r → C], σ F )
This means that there is a move above T of the form (with labels instead of nodes): and a node x in C Sep above a. According to the side-condition P ⇒ def(B), we know that this transition is not in whenabort[B], because all the variables in B are necessarily well-defined. There are now three possibilities:

(σ C * σ, σ, σ F ) nop : C ------→ (σ C * σ,
Case 1: t ∈ when[r]( C S ). In that case the image of x under λ is of the form

λ(x) = (σ C , σ [r → C], σ F )
and t is also a transition in C Sep , whose image under λ is:

(µ, L {r}) m : C -----→ (µ , L {r})
such that the image of t under λ is:

(µ, L) m : C -----→ (µ , L ).
Moreover, by hypothesis, we can lift the transition t from C S to a move whose labels are of the form

(σ C , σ, σ F ) m : C
-----→ (σ C , σ , σ F ) Therefore, the same move is a lifting of t in C Sep , and its labels are

(σ C , σ [r → C], σ F ) m : C -----→ (σ C , σ [r → C], σ F )
Cases 2 and 3: t is in whentrue[B]( P (r) S ) or in V (r) S . Follows from the definitions.

A.6. The conjunction. In this section, we suppose that Γ is precise and that π is the following derivation tree:

. . . π 1

Γ {P 1 }C{Q 1 } . . . π 2 Γ {P 2 }C{Q 2 } Conj Γ {P 1 ∧ P 2 }C{Q 1 ∧ Q 2 }
This rule is not sound when the context Γ is not precise, see [START_REF] Gotsman | Precision and the Conjunction Rule in Concurrent Separation Logic[END_REF]. In out setting, precision implies that Eve has at most one way of lifting a given transition from the Code. This is very useful, because, on the one hand, the induction hypothesis tells us that there are two ways of lifting the same Code transition. And, on the other hand, precision implies that they are actually the same, and therefore define a move in the interpretation of Conj, which is defined using a synchronous product. Let us show, then, that λ(y 1 ) = λ(y 2 ). Since all the permissions are preserved, by definition of the strategies, the first and the last component of the two separated states coincide. Moreover, precision tells us that there is at most one sub-logical state that satisfies the invariants, which means that the middle components coincide as well the middle components coincide as well.

Appendix B. Proof of the 2-soundness theorem (Thm. 8.2)

In this section, we establish the 2-soundness theorem (Theorem 8.2) by induction on the proof π of a Hoare triple of the form Γ {P }C{Q}. First, we begin with the case of the Par rule, which we find the most interesting.

. . . π 1 Γ {P 1 }C 1 {Q 1 } . . . π 2 Γ {P 2 }C 2 {Q 2 } Par Γ {P 1 * P 2 }C 1 C 2 {Q 1 * Q 2 }
and that the interpretation

L i : π i Sep → C i L
is a 2-fibration, for i = 1, 2. In that case, the asynchronous graph morphism By definition of the parallel product of ATSs, since (B.1) is a tile, its two projections are tiles as well:

L : π Sep → C 1 C 2 L is also a 2-fibration. Proof. Write C = C 1 C 2 . Let us consider a tile in C L : b 1 |b 2 a 1 |a 2 ≈ c 1 |c 2 b 1 |b 2 m m m m (
b 1

a 1 ≈ c 1 b 1 v 1 u 1 v 1 u 1 b 2 a 2 ≈ c 2 b 2 v 2 u 2 v 2 u 2
By hypothesis, the asynchronous morphisms L 1 and L 2 are both 2-fibrations. This means that the following two squares above them in C 1 S and in C 2 S are tiles as well:

y 1 x 1 ∼ z 1 y 1 v 1 u 1 s 1 t 1 y 2 x 2 ∼ z 2 y 2 v 2 u 2 s 2 t 2
for some nodes y 1 and y 2 in C 1 S and C 2 S respectively. By definition of tiles in C 1 C 2 S , to show that there exists a tile completing (B.2) above (B.1), it suffices to show that the two states λ 1 (y 1 ) and λ 2 (y 2 ) are compatible, in the sense of Definition 7.1. This follows from the following lemma.

Lemma B.2. Suppose given two ATSs over separated states G 1 and G 2 , and two tiles:

y 1 x 1 ∼ z 1 y 1 v 1 u 1 s 1 t 1 y 2 x 2 ∼ z 2 y 2 v 2 u 2 s 2 t 2
where the upper paths are compatible. Then y 1 and y 2 , and the paths s 1 ; t 1 and s 2 ; t 2 define a path in G 1 G 2 .

Proof. By case analysis on the polarities of the transitions.

L i : π i Sep → C i L
is a 2-fibration, for i = 1, 2. In that case, the asynchronous graph morphism

L : π Sep → C 1 ; C 2 L is also a 2-fibration.
Proof. Recall that the semantics of sequential composition is defined by: and that its upper path is the image of the following tile by L Suppose, first, that m touches r; say m = P (r) for example. Since the square above is a tile, we know that, in that case, m is neither P (r) nor V (r). This implies that the path (B.3) is the image by hide[r] of a path:

C 1 ; C 2 L = C 1 L ; C 2 L π 1 ; π 2 Sep = π 1 Sep ; π 2 Sep This means that a tile in C 1 ; C 2 L ,
(σ C , σ 2 , σ F ) (σ C , σ 1 , σ F ) (σ C , σ 3 , σ F ) m m (B.
(σ C * σ, σ [r → C], σ F ) (σ C , σ [r → σ], σ F ) (σ C , σ 3 [r → C], σ F ) m P (r)
with σ C = σ C * σ. By induction, this path can be completed into a tile in π Sep of the form

(σ C * σ, σ [r → C], σ F ) (σ C , σ [r → σ], σ F ) ∼ (σ C , σ 3 [r → C], σ F ) (σ C , σ [r → σ], σ F ) m P (r) m P (r)
which implies that σ C = σ C * σ. Finally, this implies that (B.3) can be completed into a tile:

(σ C , σ, σ F ) (σ C , σ, σ F ) ∼ (σ C , σ 3 , σ F ) (σ C , σ, σ F ) m nop m nop
Note that this reasoning holds when m is replaced with a Frame move. (indeed, in the proof above, we accepted that m change σ F ). The case where neither m nor m touch r is similar.

B.4. Critical sections. Before we prove the 2-fibration lemma for the rule With, we analyze the structure of when[r]. Recall that this ATS is built in two steps (see §4.2): first, the nodes and transitions of G are lifted by adding the new resource r into the sets of locked resources of all the states (and in the case of separated states, we add that r is locked by the Code), and, second, we add Environment transitions to make it an ATS. Call the first kind of transition natural, and the second artificial. The artificial transitions correspond to the case where the Environment touches the lock while it is held by the Code. This is, of course, a highly incorrect behavior. Thankfully, the constraints on the Frame moves in the Machine model of Separated States, and hence in the interpretation of proofs, rule these transitions out, in the following sense. First, natural transitions are stable by homotopy.

Lemma B.5. Given a tile T in when[r](G), if the upper path is made of two natural transitions, then so does the lower path.

Proof sketch. In a tile, opposite transitions have the same footprints, and therefore the same behavior on locks.

In the interpretations of proofs, all Code transitions are natural. We can suppose that this tile is in when[r](G). According to the two lemmas above, it is of the form (where we write, instead of the nodes themselves, their images under λ )

L 2 {r} L 1 {r} ≈ L 3 {r} L 2 {r}
Γ {P 1 }C{Q 1 } . . . π 2 Γ {P 2 }C{Q 2 } Conj Γ {P 1 ∧ P 2 }C{Q 1 ∧ Q 2 }
where Γ is precise, and that the interpretation L i :

π i Sep -→ C L
is a 2-fibration, for i = 1, 2. In that case, the asynchronous morphism

L : π Sep -→ C L is also a 2-fibration.
Proof. Consider a tile T in C L such that its upper path can be lifted to a path p in π Sep . By definition of π Sep := π 1 Sep ∩ π 2 Sep , the path p corresponds to a path p 1 in π 1 Sep and p 2 in π 2 Sep , which all have the same image under λ, λ 1 and λ 2 respectively. Moreover, by hypothesis, the tile T can be lifted to tiles T 1 and T 2 in π 1 Sep and in π 2 Sep respectively, such that their upper paths are p 1 and p 2 , respectively. Since there is at most one tile which has a given upper path (Axiom 2 of asynchronous graphs), the two tiles have equal images under λ 1 and λ 2 . Therefore T 1 and T 2 define a tile in π Sep extending the path p.

(σ C , σ 2 , σ F * σ R ) (σ C , σ 1 , σ F * σ R ) ∼ (σ C , σ 3 , σ F * σ R ) (σ † C , σ 3 , σ F * σ R ) m m m m
which means that there is a tile that extends (B.7) above (B.8):

(σ C * σ R , σ 2 , σ F ) (σ C * σ R , σ 1 , σ F ) ∼ (σ C * σ R , σ 3 , σ F ) (σ † C * σ R , σ 3 , σ F ) m m m m

  vs. stateless semantics. Along the stateful description of the machine provided by the asynchronous graph (G, G ), comes a stateless description of the same machine, conveyed this time by an asynchronous graph (H, H ) where only the instructions are considered, not their action on the machine states. Accordingly, the graph H has a single node * and a transition a : * * m for each instruction m of the machine displayed in (1.4) parametrized by x ∈ Var, v ∈ Val and ∈ Loc. The graph H is moreover equipped with a permutation tile a • b H b • a for every pair a = a and b = b of instructions of the machine. The two asynchronous transition graphs (G, G ) and (H, H ) are related by an asynchronous graph homomorphism

  Definition 4.2 (ATS). An asynchronous transition system (ATS) is a Code-acyclic asynchronous graph with polarities (G, G ) equipped with a forward-closed subset |G| ⊆ ∂ 1 (G) of final nodes. A final node in |G| is called a returning node of the ATS. Definition 4.3. An ATS with machine model ( , ) is defined as an ATS (G, |G|) equipped with an asynchronous graph homomorphism

Figure 1 :

 1 Figure 1: Inference rules of Concurrent Separation Logic

  Proof. A Code transition in C 1 ; C 2 S is either a transition in C 1 S or a transition in C 2 S . The result follows from the hypotheses. A.3. The frame rule. Lemma A.3. Suppose that π is the derivation tree . . . π Γ {P }C{Q} Frame Γ {P * R}C{Q * R} and that the interpretation S : π Sep → C S is a 1-fibration on Code transitions. In that case, the asynchronous graph morphism S : π Sep → C S is also a Code 1-fibration. Proof. Let us consider a node x in π Sep and a Code transition a m : C -----→ b ∈ C S

  transition above. Hence, λ (y ) is of the formλ (y ) = (σ C , σ , σ F * σ R )which implies that there is a transitionx m : C -----→ y above the Code transition in frame[σ R ]( π Sep ) ⊆ π Sep with λ(y) = (σ C * σ R , σ , σ F )A.4. Resource introduction. The rule for resource introduction is interpreted using the hide[r] construction, which hides the new resource. The proof consists basically in showing that if some Code transition t can be lifted into a move T , then hide[r](t) can be lifted intro hide[r](T ). Lemma A.4. Suppose that π is the derivation tree . . . π Γ, r : J {P }C {Q} Res Γ {P * J}resource r do C {Q * J} and that the interpretation S : π Sep → C S is a 1-fibration on Code transitions. In that case, the asynchronous morphism S : π Sep -→ resource r do C S is also a 1-fibration on Code transitions. Proof. Let us consider a node x in π Sep and a Code transition t a m : C -----→ b where S(x) = a. By definition of resource r do C S , t is the image under hide[r] of a transition t : a m : C -----→ b ∈ C SCase 1. Suppose m is neither P (r) nor V (r). Then m = m and the situation is:λ(x) = (σ C * σ, σ, σ F ) and λ (x) = (σ C , σ [r → σ], σ F )By the hypothesis on S , there is a node y ∈ π Sep and a move x m : C -----→ y above the Code transition t and such that

  x m : C -----→ y above the Code transition T and such that

  σ, σ F ) A.5. Critical sections. Lemma A.5. Suppose that π is the derivation tree . . . π Γ {(P * J) ∧ B}C {Q * J} With Γ, r : J {P }with r when B do C {Q} and that the interpretation S : π Sep -→ C S is a 1-fibration on Code transitions. In that case, the asynchronous morphism S : π Sep -→ with r when B do C S is also a 1-fibration on Code transitions. Proof. Recall that, in that case, the semantics of the Code and of the derivation trees are defined as C Sep = whentrue[B]( P (r) S ; when[r]( C S ); V (r) S ) ⊕ whenabort[B] π Sep = whentrue[B](acquire[r]); when[r]( π Sep ); release[r] Consider a Code transition t of C S a m : C -----→ b

Lemma A. 6 .

 6 Suppose the interpretationS i : π i Sep → C Sis a 1-fibration on Code transitions, for i = 1, 2. In that case, the asynchronous graph morphismS : π Sep → C S is also a Code 1-fibration.Proof. Consider a Code transition of C S a m : C -----→ b and a node x in π Sep above a. By definition of the semantics of π, there exist two nodes x 1 ∈ π 1 Sep and x 2 ∈ π 2 Sep each above a and such that λ 1 (x 1 ) = λ 2 (x 2 ) = λ(x). Therefore, according to the hypotheses there exist two moves in π 1 Sep and in π 2 Sep each of the form x i m : C -----→ y i . It suffices to show that λ(y 1 ) = λ(y 2 ), since it implies that there exists y in π Sep such that x m : C -----→ y is above the transition on C S we considered.

B. 1 .

 1 The parallel rule. Lemma B.1. Suppose that π is the derivation tree

  B.1) such that there exist two transitions in C S y 1 |y 2 x 1 |x 2 z 1 |z 2 m m (B.2) that are sent through L onto the upper path in (B.1).

  is either a tile in C 1 L or a tile in C 2 L . By the hypothesis on L i , it is clear that in either case we can lift the tile in either π 1 Sep or in π 2 Sep , and thus in π 1 ; π 2 Sep . B.3. Resource introduction. Lemma B.4. Suppose that π is the derivation tree . . . π Γ, r : J {P }C {Q} Res Γ {P * J}resource r do C {Q * J} and that the interpretation L : π Sep → C L is a 2-fibration. In that case, the asynchronous morphism L : π Sep -→ resource r do C L is also a 2-fibration. Proof. Write C = resource r do C . Suppose there is a tile in C L of the form

  3)Recall that the semantics of resource introduction is given byresource r do C L := hide[r]( C L ) Res(π ) Sep := hide[r]( π Sep )By the definition of the semantics, it is the image under hide[r] of some tile

Lemma B. 6 .

 6 If G is an ATS over the machine model of separated states, then all the Code transitions of when[r] are natural. Proof sketch. Since the lock r is held be the Code, the Frame cannot touch it. Lemma B.7. Suppose that π is the derivation tree . . . π Γ {(P * J) ∧ B}C {Q * J} With Γ, r : J {P }with r when B do C {Q} and that the interpretationL : π Sep -→ C L is a 2-fibration.In that case, the asynchronous morphismL : π Sep -→ with r when B do C L is also a 2-fibration.Proof. Write C = with r when B do C . Recall that the semantics of C is defined as:C Sep = whentrue[B]( P (r) Sep ; when[r]( C Sep ); V (r) Sep ) ⊕ whenabort[B].By definition of sequential composition of ATSs, a tile in C L contains a Code transition from P (r) L (or V (r) L ) only if it is a Code/Frame tile. This case is easy because P (r) and the Adam move touch distinct components of the separated states (since it is a tile, Adam cannot touch the r component of σ), and λ is a Code-Frame 2-fibration by definition of ATSs.Consider a path of the following form in π Sep :(σ C , σ 2 [r → C], σ F ) (σ C , σ [r → C], σ F ) (σ C , σ 3 [r → C], σ F ) m m (B.4)and consider a tile in C L whose upper path is the image of the above path under L.

  , there is a tile in C L (on the same nodes, since the map when[r] is defined pointwise) of the form: and by the definition of the semantics of the rule With, there exists a tile in π Sep above the tile (B.6), which is of the form:(σ C , σ 2 , σ F ) (σ C , σ, σ F ) ∼ (σ C , σ 3 , σ F ) (σ C , σ 2 , σ F ) m m m mwhere the domain of the σ's does not contain r. This finally means that we can complete the path (B.4) into the following tile above (B.5) in π Sep :(σ C , σ 2 [r → C], σ F ) (σ C , σ [r → C], σ F ) ∼ (σ C , σ 3 [r → C], σ F ) (σ C , σ 2 [r → C], σ F )Suppose that π is the derivation tree . . . π 1

  Suppose π is the following derivation tree: . . . π 1Γ {P ∧ B}C 1 {Q} . . . π 2 Γ {P ∧ ¬B}C 2 {Q} If Γ {P }C{Q} where C := if B then C 1 else C 2 ,and that the interpretation

  L i :π i Sep -→ C i Lis a 2-fibration, for i = 1, 2. In that case, the asynchronous morphismL : π Sep -→ C L is also a 2-fibration.Proof. Recall that the semantics of if statements is defined asif B then C 1 else C 2 Sep = whentrue[B]( nop Sep ); C 1 Sep ⊕ whenfalse[B]( nop Sep ); C 2 Sep ⊕ whenabort[B]All non trivial tiles are either in C 1 L or in C 2 L . In either case, the hypothesis on L i tells us that this tile can be lifted to π i Sep .B.7. Disjunction.Lemma B.10. Suppose that π is the derivation tree . . .π 1 Γ {P 1 }C{Q 1 } . . . π 2 Γ {P 2 }C{Q 2 } Disj Γ {P 1 ∨ P 2 }C{Q 1 ∨ Q 2 }and that the interpretation

  L i :π i Sep -→ C Lis a 2-fibration, for i = 1, 2. In that case, the asynchronous morphismL : π Sep -→ C L is also a 2-fibration. Proof. Similarly to the previous case, if T is a tile in C L , there we can either lift it to π 1 Sep or to π 2 Sep , so in any case we can lift it to π Sep . B.8. The frame rule. Lemma B.11. Suppose that π is the derivation tree . . . π Γ {P }C{Q} Frame Γ {P * R}C{Q * R} and that the interpretationL : π Sep -→ C L is a 2-fibration.In that case, the asynchronous morphismL : π Sep -→ C L is also a 2-fibration. Proof. Consider a path in π Sep of the following form (it is in one of the frame[σ R ]( π Sep )) (σ C * σ R , σ 2 , σ F ) (σ C * σ R , σ 1 , σ F ) (σ C * σ R , σ 3 , σ F ) m m (B.7) and a tile in C L whose upper path is the image of (B.7) under L π : frame[σ R ], and according to the hypothesis on L π , the path (B.7) in frame[σ R ]( π Sep ) corresponds to a path in π Sep that is the upper path a tile of the form:

  Var of variable names, Val of values, Loc ⊆ Val of memory locations, and LockName of resources. In practice, we consider the case where Loc = N and Val = Z. (Memory states). A memory state µ is a pair (s, h) of partial functions with finite domains s : Var fin Val and h : Loc fin Val called the stack s and the heap h of the memory state µ. The set of memory states is denoted by State. The domains of the partial function s and of h are denoted by vdom(µ) and hdom(µ) respectively, and we write dom(µ) for their disjoint union. (Machine states). A machine state is either a pair s = (µ, L) consisting of a memory state µ and a subset of resources L ⊆ LockName, called the lock state, which describes the subset of locked resources in s; or an error state . The set of machine states is denoted by MState. Formally:

	Definition 2.1 Definition 2.2

  If they both have returning states, we identify ∂ 1 (G 1 ) with ∂ 1 (G 2 ); if only one of G 1 and G 2 has returning states, we keep this one as our returning states; otherwise the juxtaposition has no returning states.

Sequential composition. The sequential composition G; G of two ATSs G and G is the disjoint union of G and G where we identify the returning nodes of G and the initial nodes of G with the same underlying image under λ G and λ G . Because we remove the inaccessible nodes, when G has no returning nodes, G; G = G.

  ATSs G 1 and G 2 over the model Sep of separated states is defined in essentially the same way as the disjoint sum G 1 ⊕ G 2 . The only difference with the disjoint sum G 1 ⊕ G 2 is that the transitions (or moves) in G 1 ∪ G 2 are meant to justify the transitions of the same program C, whereas the transitions (or moves) of the disjoint sum G 1 ⊕ G 2 are meant to justify the transitions of two different programs C 1 and C 2 . So, given two derivation trees in CSL . . .π 1 Γ {P 1 }C{Q 1 } . . . π 2 Γ {P 2 }C{Q 2 }the asynchronous homomorphism associated to π 1 Sep ∪ π 2 Sep is of the form

  A.2. Sequential composition. The case of sequential composition is easy, since a Code transition of C 1 ; C 2 is either a transition from C 1 or a transition from C 2 , and both cases follow immediately from the induction hypotheses.

	Lemma A.2. Suppose that π is the derivation tree . . . π 1 . . . π 2
	Γ {P }C 1 {Q} Γ {P }C 1 ; C 2 {R} Γ {Q}C 2 {R}	Seq
	and that the interpretation

Acknowledgments

The authors are grateful to Richard Bornat, Stephen Brookes, Tony Hoare, François Pottier and Viktor Vafeiadis for discussions at an early stage of this work.

) define a permutation tile in the underlying machine model . As a matter of fact, one purpose of the machine model ( , ) is precisely to provide that piece of information necessary to construct the parallel product of G 1 and G 2 .

Appendix A. Proof of the 1-soundness theorem (Thm. 8.1)

In this section we prove the 1-soundness theorem of CSL. The proof is done by induction on the structure of the proof tree. Each case of the induction is given its own lemma. We focus on the non-leaf rules of CSL.

A.1. Parallel composition. We begin with the rule for parallel composition. The corresponding case in the induction is the following.

Lemma A.1. Suppose that π is the derivation tree . . . π 1

and that the interpretation