{'fraction_non_alphanumeric': 0.03962488677335133, 'fraction_numerical': 0.005221746620961583, 'mean_word_length': 4.485046273745738, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Flexible Refinement Proofs in Separation Logic

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. Our technique uses separation logic to reason about efficient concurrent implementations. It prescribes only a loose coupling between an abstract model and the concrete implementation. It thereby supports a wide range of program structures, data representations, and proof structures. We make only minimal assumptions about the underlying program logic, which allows our technique to be used in combination with a wide range of logics and to be automated using off-the-shelf separation logic verifiers. We formalize the technique, prove the central trace inclusion property, and demonstrate its usefulness on several case studies.


Introduction
Refinement is a powerful technique for the formal development of correct systems. It is especially useful for concurrent and distributed systems, because it allows one to establish system-wide invariants on the level of abstract models and preserve them when decomposing the system into its components. It is, thus, not surprising that several recent developments of verified systems employ refinement reasoning [2,10,14,19,22].
Traditionally, refinement is applied to mathematical models of software, for instance, in formalisms such as Event-B [1], TLA + [17], or the higher-order logics supported by interactive theorem provers such as Coq [8]. The final executable program is then produced automatically by a code generator. However, this approach generally leads to sub-optimal implementations that do not fully utilize the language features needed to produce efficient code, such as mutable heap structures and concurrency. Manually optimizing the generated code would forfeit the correctness guarantees provided by the formal development.
To address these shortcomings, recent work has combined refinement with bottom-up program verification techniques that support more features of modern programming languages [10,15,33,34]. While these approaches substantially increase the range of programs that can be developed using refinement, they come with their own limitations. First, several existing techniques restrict the structure of the executable program, which reduces expressiveness and limits the efficiency of the executable code. For instance, the methodology used in Iron-Fleet [10] supports protocol-level concurrency, but restricts the implementations of individual components to execute sequentially. Moreover, the structure of the code must closely follow the structure of the abstract TLA + model. Similarly, the Igloo methodology [33] does not allow threads to perform I/O operations concurrently. Second, most refinement techniques that support bottom-up code development are closely tied to a particular program logic, which often impedes adoption and automation. For example, refinement in DeepSpec [15] is tied to the VST logic [5], DISEL [32] comes with its own dedicated logic, and Trillium [34] leverages Iris [13]. All of these logics are very expressive, but require substantial manual effort. The underlying program logic may also impose limitations. For instance, Trillium inherits Iris's restriction to finitary behaviors, which precludes operations such as non-deterministically choosing from an infinite set. However, non-deterministic choice is essential for the specification of abstract system models, for instance, when the concrete algorithm to determine a value is an implementation decision that is taken in a later refinement step.
In this paper, we present a novel methodology to prove that an implementation refines an abstract model given as a transition system. Our methodology enables flexible refinement proofs along four dimensions: 1. Abstract model. We do not prescribe a specific formalism for abstract models, but support any transition system whose transition relation can be specified in first-order logic. 2. Program structure. Our methodology uses separation logic [29] to support efficient implementations, in particular, mutable state and arbitrary concurrency structures. 3. Logic and automation. We make only minimal assumptions about the underlying program logic, which allows our methodology to be used in combination with a wide range of logics and to be automated using off-the-shelf separation logic verifiers. 4. Proof structure. Our methodology prescribes only a very loose coupling between the abstract model and the concrete implementation. This maximizes flexibility when choosing the program structure (for instance, control flow, concurrency, and thread synchronization), the data representation (supporting for instance, local and shared state), and proof structure (for instance, allowing coupling invariants to be expressed via a combination of local assertions and lock invariants).
Approach. Our goal is to prove that a given implementation refines an abstract model, that is, each finite trace of the abstract model corresponds to a trace in the transition system. This trace inclusion property guarantees that any safety property proved for the abstract model also holds for the implementation.
Our abstract models are expressed as (possibly infinite) transition systems in the style of TLA + , Event-B, or other refinement frameworks. We assume that some variables of the abstract transition system (ATS ) are declared to be part of the environment in which the system executes. These are the variables that can be observed about an execution; that is, we require trace inclusion only after projecting traces to the environment variables. Consequently, a concrete implementation may perform arbitrary internal operations as long as it manipulates the environment according to ATS . A typical example for environment variables are the input and output streams of a program, but our methodology also supports other cases such as the variables shared between threads. We assume that a program manipulates the environment only via dedicated operations, such as the methods of an I/O library, whose specifications express how they manipulate the environment in terms of the environment variables of ATS .
To reason about ATS and the concrete implementation within one program logic, we embed ATS as global ghost state into the concrete implementation: each variable of ATS is represented as a ghost variable of the program. The concrete program must implement the transitions of ATS via atomic program operations and corresponding updates of the ghost state. We identify these operations via annotations in the code; they include in particular the operations used to manipulate the environment. Proof obligations enforce that each such operation performs a valid transition of ATS and that they execute atomically. We do not prescribe how these atomicity checks are performed: they are trivial for sequential programs, could be performed syntactically by identifying a set of atomic operations (such as compare-and-swap and native I/O operations), could be ensured via a global locking strategy, or could be discharged in a logic that can reason about atomicity, such as TaDA [30]. This approach allows us to use any separation logic that is able to reason about shared state, in particular, standard separation logic [29], concurrent separation logic [24], and the numerous separation logics for fine-grained concurrency, e.g., [9,30,31].
A key virtue of our methodology is that refinement proofs are organized around a minimal core, namely the proof obligations showing that the program manipulates the environment variables according to the abstract model. Discharging these proof obligations generally requires suitable coupling invariants between the abstract and the concrete state, as well as updates to the ghost state to maintain them. However, we do not prescribe how to express and prove those, which enables programmers to flexibly structure the code, data, and proof.
Contributions. We make the following technical contributions: -We present a novel verification methodology for refinement proofs that provides more flexibility than prior work in terms of the supported class of programs, the choice of verification logic and tools, and the organization of the refinement proof itself (Sec. 2).
-We formalize an instance of our methodology for a concurrent language and a standard separation logic. Our soundness proof shows trace inclusion, which implies that safety properties of the abstract model also hold for the concrete implementation (Sec. 3 and Sec. 4). -We demonstrate the expressiveness of our methodology by encoding a series of interesting examples into the Viper language [23]. Our evaluation shows in particular that our methodology can be automated with existing separation logic verifiers (Sec. 5). We will submit our examples as an artifact.

Overview
In this section, we explain our methodology on a simple example that prints all integers in ascending order, starting from an arbitrary, non-negative initial value. To illustrate the flexibility of our methodology, we refine an abstract model into a concurrent implementation. The concrete state is stored in local variables of the individual threads, which requires a non-trivial, decentralized coupling invariant. This section provides an informal overview; the details of the programming language and proof rules will be formalized in the next sections.
Abstract Model. The abstract model of our system is defined in Fig. 1. We represent the output stream of the system stdOut as a sequence of integers. This variable belongs to the environment, whereas count is internal to the system. The initial state has an arbitrary non-negative value for count, which illustrates the common case that abstract models choose values non-deterministically. A valid transition adds the current value of count to the output stream and then increments it.
Embedding of the Abstract Model. As explained in the introduction, we embed the abstract model as ghost state into the concrete implementation. To this end, we declare a global ghost variable: ghost var count: Int We assume that the environment variable stdOut is predeclared for each program. It is manipulated via a print(x) statement, which requires ownership of stdOut (in the sense of separation logic: stdOut − → _) and appends its argument x to the output stream. Other input and output channels, as well as other I/O operations are handled analogously.
To refine the abstract model, the concrete implementation may manipulate count and stdOut only according to the abstract model presented in Fig. 1 enforce this requirement by protecting both variables with a ghost lock. Like a regular lock, a ghost lock is equipped with a lock invariant that must be established when the lock is initialized and must be preserved by the operations between an acquire and a release operation. In contrast to a regular lock, a ghost lock is not present at run time; that is, it does not block execution and, thus, cannot cause deadlock. Erasing ghost locks from the program is sound because the operations between an acquire and a release must execute atomically.
In our language, we initialize the ghost lock with a dedicated Init ghost statement, which checks the Init assertion from the abstract model as well as the lock invariant (in particular, it transfers ownership of the variables in the lock invariant from the executing thread to the ghost lock). A dedicated Next ghost block statement acquires the ghost lock, executes the block of the statement, and then releases the ghost lock. Upon release, it checks that the Next assertion from the abstract model holds between the state in which the ghost lock was acquired and the state where it is released. That is, the Next statement executes one transition of the abstract model (or stutters). The block of a Next statement must be atomic; we enforce this requirement syntactically, that is, we check that the body consists of at most one atomic statement plus an arbitrary number of ghost operations. However, our methodology also supports more sophisticated approaches, for instance, logics that can prove atomicity [30]. Note that both Init and Next are ghost statements, that is, part of the specification. The executable program contains their blocks, but not the manipulation of the ghost lock. They are supported by any separation logic that handles locks.
The invariant of the ghost lock must contain at least fractional ownership [3] to each variable of the abstract model, which ensures that once the ghost lock has been initialized, those variables can be modified only within a Next statement and, thus, the Next relation of the abstract model is checked on each modification. In our example, the ghost lock invariant contains fractional ownership of the count variable and full ownership of stdOut: Our proof rules enforce that print-the only way to modify stdOut-can be executed only after the ghost lock has been initialized with an Init statement. Consequently, the above lock invariant guarantees that print operations can occur only within a Next block and, thus, all changes to the environment are checked to comply with the abstract model. We assume that print is atomic, which is standard for I/O operations. Fig. 2 shows the concrete implementation. After initializing the abstract state, the Init operation checks that the initial state is valid and creates the ghost lock that guards further updates to the abstract state, in particular, all executions of print. Note that our implementation fixes a concrete initial value for count, whereas the abstract model permits an arbitrary non-negative number (see Fig. 1). Resolving non-determinism is very common during refinement. We explain the body of the Init statement below. count := 0 ; Init { evenTurn := true ; lastEven := − 1 ; lastOdd := 0 ; lock L { /* even-thread */ /* odd-thread */ } } Fig. 2. The concrete implementation of our example. The even-thread is presented in Fig. 3; the odd-thread is analogous.
Concrete Program State and Coupling. Our concrete implementation uses two concurrent threads (parallel branches) that print the even and odd numbers, respectively. To synchronize these two threads, we declare a global Boolean variable that indicates whether the next number to be printed is even: var evenTurn: Bool This variable is protected by a global (regular, non-ghost) lock L. Fig. 3 shows the implementation of the thread that prints the even numbers; the other thread is analogous. Both threads loop indefinitely. In each iteration, they acquire the lock L (waiting until evenTurn is true resp. false), execute a transition (explained later), flip evenTurn, and release the lock. Each thread has a local variable c that counts how many numbers it has printed. This design illustrates that our methodology supports flexible combinations of global concrete state (such as evenTurn) and local concrete state (such as c). While global concrete state can easily be connected to the abstract state via lock invariants, local variables require more flexible ways of expressing the coupling invariant.
For instance, at the beginning of each loop iteration of the even-thread, the abstract counter count is equal to 2 * c in case evenTurn is true. This condition allows us to prove that the print operation in the loop body is indeed permitted by the abstract model. However, this coupling invariant cannot be included in a lock invariant because locks do not protect local variables. Nor can it be expressed as a loop invariant because that would require that the even-thread holds on to some ownership of count, which would prevent the odd-thread from ever updating it.
A relation between the local variable c and the shared variable count can be proved in many ways, for instance, by using classical rely-guarantee reasoning [12] or concurrent abstract predicates [9]. Our refinement methodology is compatible with any such logic. In our example, we use a standard encoding of the Owicki-Gries counter [26] in separation logic. For this purpose, we introduce two global ghost variables lastEven and lastOdd that keep track of the effect of each individual thread: ghost var lastEven: Int, lastOdd: Int We relate these ghost variables to the local variable c in each thread via the thread's loop invariant (see Fig. 3), and also to the global count via the lock invariant of lock L: The lock and the loop invariants together form the coupling invariant for our example. For the even-thread, we get lastEven = 2 * c − 1 from the loop invariant, evenTurn from the with-statement, and (evenTurn ⇒ count = lastOdd ∧ lastEven = lastOdd−1) from the lock invariant. These three conditions together imply count = 2 * c, which is required to show that the printed value is permitted by the abstract model.

Discussion.
Our example illustrates that our methodology enables flexible refinement proofs, which are required to support a wide range of efficient implementations. We refined an abstract model into a concurrent implementation that uses both local and mutable shared state, as well as thread synchronization via locks. The proof makes only minimal assumptions about the underlying program logic. Concretely, we use concurrent separation logic, locks, ghost variables, and fractional permissions. These features are supported and automated by many existing separation logic verifiers. For instance, an encoding of our example into Viper verifies automatically in around 3.8s. Combining our refinement methodology with other, more advanced program logics is possible.
Finally, our example demonstrates that our methodology enables flexible proof structures. Proofs are essentially derived backwards from those statements that manipulate environment variables, here, print. These statements require that the abstract state has been initialized and that the modification of the environment variables is permitted by the abstract model. Any proof structure that establishes these properties is compatible with our methodology. In our example, we use a combination of loop invariants and lock invariants, connected via global ghost variables, to establish the necessary coupling relation. This flexibility is essential to support a wide range of data, control, and concurrency structures.

Preliminaries: Concurrent Separation Logic
Our verification technique for refinement proofs does not depend on a particular program logic but can, in principle, be integrated into most separation logicbased verification techniques. To make this claim more concrete, we will formalize (in Sec. 4) our methodology on top of an elementary formalization of concurrent separation logic with fractional permissions by Vafeiadis [35]. Since Vafeiadis' soundness proof generalizes well to more advanced concurrent separation logics, such as [9], we expect the same when using our technique for refinement on top of such advanced logics.
This section briefly recapitulates the main ingredients of concurrent separation logic (CSL). More precisely, we introduce a small concurrent programming language, its underlying model of program states, and its operational semantics. Furthermore, we discuss CSL's assertion language and proof rules.

Programming Language
We consider a small programming language that supports heap-manipulating instructions, structured concurrency, and locks. More precisely, the set Cmds of commands in our programming language is given by the grammar where x is a variable in the set Vars, E is an expression over variables, and L is a lock identifier taken from the arbitrary, but finite set Locks = { L, . . . }. We briefly go over our language: in addition to the assignment x := E and the usual control-flow structures, C 1 C 2 is the parallel composition of C 1 and C 2 ; lock L { C } declares a new lock L that can be used in C and expires after termination of C; the conditional critical region (CCR) with L when E { C } acquires lock L if condition E holds (and waits otherwise), executes C, and releases L again upon termination of C; within L { C } is an internal command that we will use to indicate that C is executed while holding the lock L. Furthermore, [E] denotes the value at the memory address given by E. x := [E] reads the value at address E and assigns it to x; [E] := E' writes the value of E to the address E. Moreover, free (E) disposes of location E, and x := new(E) allocates a free memory address, assigns it to x, and stores E at that address. We use structured concurrency and global locks to simplify the formalization, but our methodology also supports dynamic threads and locks.

Program States
A program state (s, h) consists of a stack s, i.e., a valuation of variables, and a heap h modeling dynamically allocated memory. Formally, we fix a set Vals = { v, . . . } of values containing, e.g., Booleans, integers, and sequences. The set Stacks consists of all mappings s from variables in Vars to values in Vals, i.e.,
The set Heaps of heaps consists of all finite partial functions h that map addresses in their domain dom (h) ⊆ Addrs to permission-value pairs, i.e.,
For h(a) = (ρ, v), we define the projections perm(h(a)) = ρ and val(h(a)) = v. We The addition of h 1 ⊕ h 2 of heaps h 1 and h 2 is defined as For every stack s, which is obtained from h by removing a from its domain. Finally, the set NormHeaps of normal heaps consists of all heaps h that assign the full permission 1 to every address, i.e., We typically write h instead of h to highlight that a heap is normal; by slight abuse of notation, we use h(a) as a shortcut for val(h(a)). Clearly, for every heap h, there exists a heap h such that h ⊕ h is a normal heap.

Operational Semantics
The semantics of commands is defined in terms of a small-step execution relation. Toward a formal definition, we first clarify the semantics of expressions. We do not fix a specific syntax for expressions; instead, we assume that every expression E is associated with a function E : Stacks → Vals such that E(s) is the value obtained from evaluating E in stack s.
The set Confs of program configurations c consists of all command-stacknormal-heap triples plus a dedicated error state abort, that is, We use normal heaps because permissions are a reasoning concept that does not exist when executing a program. The small-step operational semantics of commands is defined as the execution relation → ⊆ Confs × Confs given by the rules in Fig. 4. Most rules in Fig. 4 are standard (cf. [35]) and reflect the behavior informally explained in Sec. 3.1; we briefly discuss particularities.
Usage and Declaration of Locks. The operational semantics uses the command structure to record which locks are currently declared and acquired, respectively. That is, lock L { C } indicates that L is declared in C; the internal command within L { C } indicates that C holds L during its execution. We denote by Locks(C) the set of all locks that are declared in C. Analogously, locked (C) denotes the set of all locks that are currently held by C. For example, if C is not of the form lock L { . . . } or within L { . . . }, and C is given by The semantics of lock L { C } consequently keeps the lock L declared and performs a step of C until termination; after that, the lock declaration expires.
CCRs and Parallel Composition. For CCRs with L when E { C }, we first check whether condition E holds in the current state. If so, we acquire lock L and enter the CCR by moving to the internal command within L { C }, which will execute C, and release the lock upon termination of C. If E does not hold, no transition is possible, i.e., we need to wait for other threads.
The rules for the parallel composition C 1 C 2 model all interleaved executions of C 1 and C 2 . They include a sanity check stating that C 1 and C 2 do not hold the same lock at the same time, i.e., locks provide mutual exclusion. Moreover, there is a rule that prematurely aborts executions whenever a command admits a data race, that is, C 1 (resp. C 2 ) writes to and C 2 (resp. C 1 ) accesses (i.e., reads from or writes to) the same address that is outside of a CCR, and thus without protection by a lock.
Rules of the small-step operational semantics for commands in Cmds. Here, locked(C) is the set of all locks L held by C, i.e., within L { . . . } is a sub-command of C. Furthermore, accesses(C, s) (resp. writes(C, s)) denotes the set of those addresses a that are not exclusively owned by C, i.e., appear only in sub-commands Next { . . . } or with L when E { . . . }), and are accessed (resp. modified) by C given stack s.

Assertions
Syntax. The syntax of separation logic assertions includes, amongst others, all Boolean expressions E supported by our programming language Formally, the set SL of separation logic assertions is given by the grammar where E is a Boolean expression over variables, x is a variable in Vars, ρ is a permission in Perms, and I is a finite set such that each i ∈ I is associated with an assertion P i . We use syntactic sugar, such as P ⇒ Q, P ∨P and, in particular, We denote by FOL the set of all first-order logic formulas, i.e., those formulas that can be constructed from the first line of the above grammar.
Semantics. Assertions are interpreted over pairs (s, h) consisting of a stack s and a heap (with permissions) h. Tab. 1 shows the formal semantics of assertions.
Intuitively, emp specifies the empty heap; the points-to assertion E ρ − → E specifies that the heap contains exactly one address E that is mapped to E with permission ρ; E ρ − → E is an intuitionistic version stating that the heap contains at least permission ρ for the address E, which is mapped to E . E ρ − → _ and E ρ − → _ are analogous but do not require a specific value at the address given by E. The separating conjunction P * Q specifies that the heap can be partitioned into two parts such that one part satisfies P and the other part satisfies Q. i∈I P i is an iterative version of the separating conjunction. Finally, the magic wand P − * Q specifies that Q holds in a heap h after it has been extended by any heap that satisfies P (and can be added to h).
We call an assertion P valid, written |= P , if and only if s, h |= P holds for all stacks s ∈ Stacks and heaps h ∈ Heaps.
We denote by FV(P ) the set of free variables (i.e., those that are not bound by quantifiers) of assertion P . Moreover, P [x/v] denotes the substitution of every free occurrence of variable x in assertion P by v.

Proof System
The last step of our recapitulation of concurrent separation logic (CSL) presents the formal triples and proof rules for reasoning about commands. To formalize both, we first introduce lock environments and lock invariants.
Lock Environments. In contrast to the operational semantics (cf. Sec. 3.3), which has a global view on the full program state, the CSL proof system considers only the local state i.e., those parts of the current program state that are accessible to the local command. The remainder of the global state is either framed around the command or protected by locks. To this end, we associate every declared lock L with a lock invariant R that specifies the part of the global state that is protected by L. Formally, the assignment of lock invariants to locks is captured by a lock environment Γ , which is given by the grammar where L ∈ Locks and R is an SL assertion representing the lock invariant. Moreover, given a lock environment Γ , the lock invariant of lock L is Intuitively, if Γ (L) = R, then R specifies a portion of the global state that is not part of the local state but is shared with other threads and can be modified by them. In particular, if Γ (L) = emp, then L does not appear in Γ (or the declared invariant is emp) and nothing is shared with other threads.
Declaring, acquiring, and releasing the lock L can be understood as a transfer of the portion of the state specified by R between the local state and Γ , i.e., the part of the global state that is shared with other threads: whenever we declare L, R is shared with other threads and thus moved from the local state into Γ ; once the declaration expires, R is transferred back into the local state. Whenever we acquire the lock L, R is moved from Γ into the local state; whenever we release the lock L, R is moved back from the local state into Γ .
CSL Judgments. Judgments that can be derived in CSL are of the form where Γ is a lock environment such that L∈Locks Γ (L) describes the shared state, P ∈ SL is the precondition evaluated in the local state, C is a command in Cmds, and Q ∈ SL is the postcondition evaluated in the local state. Fig. 5 shows the standard proof rules of CSL [35]. In particular, the aforementioned transfer between local and shared state can be observed in the rules (Lock) and (With). A detailed discussion of the CSL proof rules is found in [24,4]. Finally, an assertion P is precise iff for all s, h1, h2, h 1 , h 2 , if def (h1 ⊕ h2) and h1 ⊕h2 = h 1 ⊕h 2 and s, h1 |= P and and s, h2 |= P , then h1 = h2.

Methodology and Formalization
We now present the details of our methodology and formalize it on top of the concurrent separation logic (CSL) introduced in Sec. 3. We first discuss how abstract models are encoded into program states. After that, we extend the programming language, its operational semantics, and the CSL proof system with refinement-specific commands and rules. Finally, we show that our methodology is sound, i.e., a proof in our program logic guarantees that the (finite) traces of the given implementation are included in the traces of the abstract model. Further details and proofs are provided in the appendix.

Abstract Models
Our methodology takes as input an abstract model that should be refined by a concrete implementation. More precisely, we assume that an abstract model is provided as a (potentially infinite-state) abstract transition system. Toward a formal definition, recall from Sec. 3.4 the definition of heap-independent assertions in first-order logic (FOL). Moreover, given a sequence of variables x = (x 1 , . . . , x k ) , we denote by x the same sequence in which each x i is replaced by a primed version, i.e., x = (x 1 , . . . , x k ).

Definition 1 (Abstract Transition System (ATS)
). An abstract transition system is a quadruple ATS (k, x, Init, Next), where x = (x 1 , . . . , x k ) is a repetition-free sequence of k ≥ 1 variables, the initial state formula Init( x) is an FOL assertion over x, and the next state formula Next( x, x ) is an FOL assertion over x and x .
We consider only ATSs that are stutter-invariant, that is, for all sequences of values v ∈ Vals k , the formula Next( v, v) is valid. Stutter invariance is desirable in the context of refinement proofs as concrete implementations should always be allowed to perform more fine-grained computation steps. Furthermore, every ATS can be turned into a stutter-invariant one by considering the modified nextstate formula Next( x, x ) ∨ 1≤i≤k x i = x i . Throughout the rest of this paper, we fix a stutter-invariant abstract transition system ATS (k, x, Init, Next) representing the abstract model we would like to prove refinement of.
To reason about refinement, we need to formalize the observable traces of ATS . Every evaluation of an ATS 's variables x constitutes one of its states. Formally, the state space of ATS is Σ ATS Vals k . A (finite) path of ATS is a sequence of states σ 1 . . . σ n , where n ≥ 1, such that 1. |= Init(σ 1 ), i.e., σ 1 is an initial state of ATS , and 2. for all i ∈ [1, n), we have |= Next(σ i , σ i+1 ), i.e., for every state but the last one, ATS admits a transition to the next state on the path.
We collect in the set Paths(ATS ) all finite paths of the transition system ATS . A trace then projects every state on a path to the values corresponding to those variables that are observable, e.g., variables modeling I/O channels as outlined in Sec. 2. For simplicity, we assume that exactly one variable, x 1 , is observable; generalizing to arbitrary sets of observable variables is straightforward. We denote by obs(σ) the projection of state σ to the value assigned to the observable variable x 1 , that is, if σ = (v 1 , . . . , v k ), then obs(σ) = v 1 .

State Encoding.
To reason about the behavior of ATS s with the machinery offered by concurrent separation logic (cf. Sec. 3), we encode states of ATS s within program states-more precisely: as part of the heap. We fix a set GhostAddrs ⊆ Addrs of dedicated ghost addresses that cannot be allocated or disposed of-they thus need to be already allocated before program execution. Every variable x i of ATS is then encoded as a ghost address x i ∈ GhostAddrs at which we store the current evaluation of x i . We use stdOut as a synonym for x 1 -the address of the only observable variable x 1 .
Given a heap h, the contents of the addresses x 1 , . . . , x k in h encode the current state of ATS . We introduce a function get_state : Heaps → Σ ATS which extracts the transition system's state from the heap: While ghost addresses cannot be allocated or disposed, (ghost) commands can read and modify their contents just like with ordinary addresses. Hence, we can enrich a concrete implementation with ghost commands to model updates to the state of the abstract model ATS .
Ghost Locks. We employ a dedicated lock G to protect the ghost locations x 1 , . . . , x k representing the current state of the abstract model ATS from undesirable modifications. To this end, we require that any lock invariant G chosen for G contains some permission to each of the locations x 1 , . . . , x k -thus preventing modification of their content without acquiring G first. Formally: Assumption 1. For any lock invariant G associated with the ghost lock G, there exists a permission ρ > 0 such that the following entailment is valid: Our methodology prescribes that G is a ghost lock such that it can be safely erased at runtime and thus cannot block execution. To guarantee the above property, our formalization treats G differently from other locks: it is a dedicated lock that is invisible to programmers and thus can neither be declared nor locked by them. Instead, it will be governed by the refinement-specific ghost commands Init and Next in a way such that G is indeed a ghost lock.

Programming Language and Operational Semantics
We now extend the programming language from Sec. 3.1 with an output operation print(E) and the refinement-specific commands Init { C } and Next { C }. Formally, we expand the grammar in Sec. 3.1 as follows: We use ghost addresses taken from GhostAddrs to formalize the semantics of each of the above commands; Fig. 6 summarizes how we formally extend the execution relation → from Sec. 3.3. We briefly go over the new rules: print(E) appends the value of E to the standard output stream, which we represent by a mathematical sequence stored at the ghost address stdOut ∈ GhostAddrs. Print thus modifies the only observable variable of the abstract mode ATS . If stdOut has not been allocated, we abort execution.
The command Init { C } is, operationally speaking, a dedicated command for declaring the ghost lock G. In fact, the rule (Init) desugars it to an explicit lock declaration lock G { C }. 1 Conceptually, Init takes the important role of marking the system as initialized, i.e., after entering Init, the concrete model must be in an observable state that matches the (observable part of) the abstract model's initial state. The command Next { C } is, operationally speaking again, a dedicated command for the conditional critical region that acquires the ghost lock G, executes C, and releases G, that is, it can be viewed as syntactic sugar for with G when true { C }. However, to ensure that G is indeed a ghost lock and can thus be safely erased at runtime, we additionally require that every command C put into a Next { C } block is atomic. That is, C can be executed in a single step without interference from other threads. Consequently, Next { C } is atomic and thus executed in a single step, as reflected by the (Next) rule: if the execution of C terminates in a configuration c, then Next { C } transitions to configuration c in a single step.
We assume that I/O operations, such as print(E), are atomic and that adding ghost code to an atomic command yields an atomic command. Apart from these assumptions, our methodology does not prescribe how to ensure atomicity-be it through known atomic statements, a global locking strategy, or formal proofs of atomicity in a program logic (cf. Sec. 2).
Observable Traces. To formalize program refinement, we need to define the observable traces induced by a program configuration. Similar to the definition of traces of the abstract model ATS , we project every program configuration in an execution c 1 . . . c n to its observable state once the system has been initialized, which is recorded by the operational semantics in its command structure: Definition 4. A command C is initialized, written init (C), if and only if the ghost lock G is declared in C, i.e., G ∈ Locks(C).
In our formalization, only the content of the standard output stream, which is modified via print(E) calls, is observable. The observable state obs(c) of a configuration c is defined as the empty or singleton sequence A trace is then obtained from a (finite) execution by mapping configurations to their observable state and concatenating the resulting sequences: The definition of obs() ignores the observable state as long as the system is not initialized, i.e., we have not reached Init { . . . } yet. This is justified as long as observable state is never modified before initialization and, thus, the implementation performs no observable action that needs to be matched by the abstract model. Our proof system will guarantee this property.

Proof System
Recall from Sec. 3.5 the proof system of concurrent separation logic (CSL). We now extend CSL to a sound program logic for proving refinement in the extended programming language introduced earlier in this section. Our assertion language is the same as for CSL, i.e., it consists of all SL assertions (see Sec. 3.4). Judgments. Judgments that can be derived in our logic (notice the R to distinguish our judgments from CSL judgments) are of the form where Γ is a lock environment such that L∈Locks Γ (L) describes the shared state, P ∈ SL is the precondition evaluated in the local state, C is a command and Q ∈ SL is the postcondition evaluated in the local state. Fig. 7 shows the proof rules for the new commands Init, Next, and print(E). Furthermore, our proof system inherits all proof rules from CSL (cf. Fig. 5 where we tacitly replace by R and exclude dedicated ghost locks in the rules (Lock) and (With)). We briefly go over the rules for the new commands: Initialization Blocks. The rule (Init) can be viewed as a stronger version of the rule (Lock), which declares two locks at once-the ghost lock G with lock invariant G and a second dedicated ghost lock I with an empty lock invariant.
The ghost lock G has already been used in our operational semantics; it governs access to the state of the abstract model ATS . The lock I is never acquired but serves as a marker in our proof system to record that an initialization block has been reached; we will explain why we need it in more detail further below.
(Init) is a stronger version of (Lock); in addition to declaring a lock, it verifies that the abstract model's state, i.e., the contents y 1 , . . . , y k of the ghost addresses x 1 , . . . , x k , is a valid initial state in ATS , i.e., Init(y 1 , . . . , y k ) holds. By Assumption 1, we know that the ghost lock's invariant G holds the necessary permissions to access the contents of these ghost addresses.
Regarding the second ghost lock I, notice that the output stream, that is, the observable content of stdOut, needs to be part of the program state before initialization, since the ghost address stdOut cannot be allocated by the implementation itself. In Def. 5, we formalized the traces of an implementation in a way such that the content of stdOut is ignored before initialization. The underlying rationale is that the implementation performs no observable action before it is initialized and we know the state of the abstract model ATS . To guarantee that there are indeed no modifications of observable state-in our case: there are no print(E) calls-before initialization, we use the ghost lock I. It acts as a token that is created upon initialization, stays in the lock environment, since it is never acquired (in contrast to the ghost lock G), and needs to be part of the lock environment Γ for all rules that modify observable state, such as (Print).
Next Blocks. The rule (Next) can be viewed as a specialized version of the rule (With), applied to ghost lock G and wait condition true. However, it contains an additional premise to ensure that executing Next { C } can be simulated by taking a single transition of ATS . Since C is atomic, the postcondition Next( o, y) in the premise achieves this effect (where o and y capture the state of ATS before and after execution of Next { C }). For initialized commands, Assumption 1 guarantees that changes to the transition system's state are possible only when holding the lock G, i.e., inside of Next { C } blocks; outside of such blocks, ATS will perform a stutter step for every step of the concrete implementation.
Print Statements. Finally, to understand the (Print) rule, we notice that print(E) is-if we ignore atomicity-syntactic sugar for the command where x is a fresh variable that is not used anywhere else. Assuming that print(E) and C are identical, the rule (Print) can then be derived using the standard rules in Fig. 5 (in sequential separation logic, i.e., for Γ = ∅).

Soundness
Intuitively, soundness means that deriving Γ R {P } C {Q} implies that, for every execution of C that starts in a configuration with a local state given by P and a shared state given by Γ , the trace of the execution is also a trace of the abstract model ATS . We now formalize and prove the above soundness claim for our refinement logic. We build upon Vafeiadis' [35] existing soundness proof for CSL (cf. Sec. 3). Hence, we first restate the main ingredients for proving CSL sound, where we slightly generalize to simplify their re-use. Let succ(c, c ) be a predicate over two program configurations; we will use succ(c, c ) only if there is a transition c → c . Soundness of CSL as well as our refinement logic is based on the following notion of configuration safety: Definition 6 (Generalized Configuration Safety). The n-step safety predicate safe n succ (C, s, h, Γ, Q) is recursively defined as follows: Vafeiadis [35] used the above notions of configuration safety and validity to prove that every CSL judgment that can be derived using the rules in Fig. 5 yields a valid triple; the original soundness proof for CSL is due to Brookes [4]. Formally: Compared to CSL, our refinement logic introduces one rule for each of the new commands Init { C }, Next { C }, and print(E) (see Fig. 7). If we only consider configuration safety as in CSL, then, as discussed in Sec. 4.3, each of these rules is either a special case of the existing rules ((Print)) or a variant of an existing rule with an even stronger precondition ((Init), (Next)). Hence, the soundness of CSL carries over to our logic (recall that R indicates refinement judgments): App. C provides further details. To formalize that the implementation refines the abstract model ATS , we extend the above definition of configuration safety such that, if the system is initialized, every concrete transition c → c taken is simulated by a transition of ATS (or stutters). Moreover, if the system becomes initialized after a step, we require that the encoded state of ATS is a valid initial state.
Our formalization uses the state extraction function get_state from Def. 3 to refer to the abstract model's state encoded in the heap. We then consider the configuration safety predicate safe n refsucc (C, s, h, Γ, Q), where the predicate refsucc((C, s, h), (C , s , h )) holds iff (i) if init (C) holds, then |= Next(get_state(h), get_state(h )); (ii) if init (C) does not hold and init (C ) holds, then |= Init(get_state(h )). As for CSL, our refinement logic is sound in the sense that formally derived judgments yield valid triples: Proof (Sketch). The proof is by structural induction over the rules of our refinement logic (found in Fig. 5 and Fig. 7). In each case, we show that the predicate safe n+1 refsucc (C, s, h, Γ, Q) holds; we first invoke Lemma 1 such that only two proof obligations remain for every possible step  We will use validity in the proof of trace inclusion. Furthermore, we need to define the initial configurations that determine the traces of the concrete implementation. We consider those traces of the concrete implementation that start in a (global) state that at least covers the local state specified by the precondition P and the shared state described by the lock invariants in Γ .
Definition 9 (Initial Configurations). For a command C, an assertion P , and a lock environment Γ , the set I(C, P, Γ ) of initial configurations is To guarantee trace inclusion, we exclude commands that suddenly become "uninitialized" because the Init { C } block expires but execution continues, e.g., Init { C } ; x 2 := 17 ; Init{ C }. Such ill-formed commands can easily be detected by a syntactic check. More precisely, we call a command C continuously initialized if there exist commands C 1 , C 2 such that C 1 contains no sub-command of the form Init { . . . } and C = (C 1 ; Init { C 2 }). Theorem 3 (Soundness). For every continuously-initialized command C, A detailed proof is found in App. E.

Evaluation
To evaluate our verification technique, we verified seven case studies using the separation logic-based automated verifier Viper [23]. All of our examples verify using Viper's existing verification backends, demonstrating that our methodology is supported by readily available verification tools. We will make our case studies available as an artifact. The examples show the flexibility of our proofs in the four dimensions mentioned in Sec. 1 and are summarized in Tab. 2. We briefly describe each of the examples in the following. alternating demonstrates how multiple threads can collaborate to achieve the overall behavior of an abstract system. This example is described in Sec. 2.
barrier is an adaptation of the barrier example from Armada [22], originally from Cohen and Schirmer [7]. In this example, multiple threads are started and must pass a barrier before exiting. A guarded transition system is used to ensure that each thread can only perform transitions related to its own state.
cons _ producer is an example with a consumer-producer setup, in which one thread adds values to a shared buffer and the other consumes them. We show that at all points an invariant is maintained, namely the relationship between the number of values produced, the number of values consumed, and the number of values left in the shared buffer. echo _ server demonstrates the use of I/O methods to model both standard input and standard output.
ring _ leader implements leader election in a ring, with a TLA + specification adapted from the TLA + examples repository, based on Chang and Roberts [6].
trees _ product and trees _ record are both examples demonstrating data refinement: the abstract model uses a mathematical datatype to represent a tree of values, whereas the implementation uses a heap-allocated array representation of the tree. The trees _ record example further demonstrates dynamic threading to process the input tree in parallel, and a two-state monotonicity invariant.
Discussion. Our case studies demonstrate that our methodology is highly flexible w.r.t. to the structure of both programs and proofs. In particular, they use local and shared mutable state (including dynamic heap data structures), concurrency with dynamic thread creation and synchronization via locks and barriers, as well as three different reasoning idioms.
The evaluation also shows that our methodology enables automating refinement proofs using an off-the-shelf verification tool. While we used Viper as a concrete tool, no example relies on features that are genuinely Viper-specific, which supports the claim that our approach is flexible w.r.t. to the underlying logic. The verification time for each example is below 8s, which demonstrates that our methodology is well-suited for SMT-based automation.

Related Work
In this section, we survey refinement techniques that combine abstract models and executable code.
Various approaches [20,28,32,36] develop implementations that are correct by construction by refining abstract models within Coq and then extracting executable OCaml programs. Similarly, Liu et al. [21] model distributed systems in Maude's rewriting logic and compile them into implementations running in distributed Maude sessions. The code extracted by these approaches is typically sub-optimal (for instance, does not use mutable data structures) and cannot interface with existing libraries, which is often necessary in practice. In contrast, our methodology uses bottom-up verification and can handle efficient implementations using concurrency and mutable state.
Trillium [34] is a refinement technique based on separation logic. Like our methodology, it supports a wide range of program and data structures. Trillium is based on Iris [13] and formalized in Coq, which enables foundational proofs at the expense of substantial manual effort. Trillium inherits some of Iris's limitations. In particular, it is limited to finitary behaviors and, thus, does not support the common case that abstract models choose a value non-deterministically from an infinite set. Moreover, Trillium expresses coupling invariants via Iris's invariants, which complicates reasoning about system initialization, especially allocation. Our methodology does not have these limitations. Trillium supports liveness properties, which we do not handle yet.
Armada [22] supports the verification of concurrent, high-performance code written in a C-like language. To achieve refinement against an abstract model, the user specifies a sequence of steps to gradually transform the implementation into the specification. Non-trivial refinement steps require complex Dafny [18] proofs showing a connection between two state machines. Unlike Armada, our methodology does not convert programs to state machines and the coupling between the abstract model and the implementation can be much looser.
The CIVL verifier [11,16] also organizes the refinement proof into multiple layers. Each layer is a structured concurrent program, where the concurrent behavior is reflected in the program structure. This structure simplifies the proof obligations and allows automation, but also reduces program flexibility. Refinement steps are based on a set of trusted tactics. By contrast, our methodology imposes no restrictions on the program or proof structure.
Igloo [33] connects abstract models to concrete implementations via dedicated I/O specifications [27]. Similarly to our work, they support a variety of separation logics to reason about concrete implementations. However, their technique does not allow threads to perform I/O operations concurrently, whereas our methodology has no such limitation.
Similar to our methodology, IronFleet [10] embeds abstract models as ghost state into executable programs and automates verification using an SMT-based verifier, in their case Dafny. However, their refinement technique imposes severe restrictions on the executable program. It must be sequential and its structure must mirror the structure of the abstract model. IronFleet supports both safety and liveness properties, whereas our approach focuses on safety properties and leaves liveness as future work.
The refinement technique [15] used in DeepSpec [2] is based on the Verified Software Toolchain (VST) [5], a framework for verifying C programs via a separation logic embedded in Coq. Instead of transition systems, they specify the intended system behavior using interaction trees [37], which are embedded into VST's separation logic. In contrast, our methodology allows us to apply standard separation logics and existing program verifiers.
Oortwijn and Huisman [25] embed process calculus models into a concurrent SL, which is automated using Viper. Their refinement approach preserves state assertions, but it is unclear whether arbitrary trace properties are preserved.

Conclusion
We have introduced a methodology for refinement proofs in separation logic that is flexible in terms of the type of abstract model used, the structure of the concrete implementation, the underlying logic and tool chain, as well as the structure of the proofs themselves. We have formalized the methodology on top of concurrent separation logic and demonstrated its applicability on several case studies using the automated verifier Viper. As future work, we plan to extend our methodology to liveness properties.

B Lemmas from CSL
We will use the following lemmas taken from [35]: Since safe 0 true (C, s, h, Γ, Q) holds always by Def. 6, it suffices to prove that safe n+1 true (C, s, h, Γ, Q) holds for an arbitrary, but fixed n ∈ N. By structural induction over the rules for of our refinement logic for deriving judgments Γ R {P } C {Q} (found in Fig. 5 and Fig. 7).
We present the case (Print) in detail further below. As discussed in Sec. 4.3, the rule (Init) is a variant of the CSL rule (Lock) with a stronger precondition, and the rule (Next) is a special case of the CSL rule (With); we thus omit detailed proofs. since all other rules are identical to the CSL proof rules; their proof is thus completely analogous to the proof of Thm. 1.
The case ( Print). Recall the rule Consequently, We discharge all items in Def. 6 to show that For Def. 6.1, consider the following: accesses(print(E), s) = { stdOut } = dom (h) (by (3)) Def. 6.2 is immediate by (3) and the rules of our operational semantics. Def. 6.3 is trivial. For Def. 6.4, assume C , s , h F , h S , h such that s, h S |= L∈locked(C )\locked(C) Γ (L) and By our operational semantics and (3), there is only one transition as above. For this transition, we have C = skip, and h S = emp, and Hence, for h = h and h S = emp, Def. 6. Proof. By definition, safe 0 refsucc (skip, s, h, Γ, Q) holds always. Assume s, h |= Q.

D.2 Proof of Lemma 3
Claim. If C contains no two different sub-commands C 1 and C 2 such that locked(C 1 ) ∩ locked(C 2 ) = ∅ and FV(G) ∩ Mod(C) = ∅, Proof (Sketch). By structural induction on the rules of our refinement logic we show that Γ, G : G R {P } C {Q} and s, h * G |= P implies ∀n ∈ N : safe n refsucc (lock G { C }, s, h, Γ, Q * G) .
We present the case for the (Next) in detail as it is the only rule, where the predicate refsucc is not immediately discharged by either applying the induction hypothesis or performing a stutter step. The remaining cases are very similar to Vafeiadis [35] soundness proof for CSL (and in particular require an additional complete induction on n for some cases, such as parallel composition).
The case (Next). Recall from Fig. 7 the rule (Next) atomic (C) and assume that s, h |= P * G.
We then need to show that, for all n ∈ N, safe n refsucc (lock G { Next { C } }, s, h, Γ, Q * G) .