Flexible Refinement Proofs in Separation Logic

Aurel Bílý Christoph Matheja Peter Müller

A. Bílý et al.

Department of Computer Science, ETH Zurich, Switzerland

{aurel.bily, cmatheja<EMAIL_ADDRESS>
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],  [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 IronFleet [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 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:

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

* Program structure. Our methodology uses separation logic [29] to support efficient implementations, in particular, mutable state and arbitrary concurrency structures.

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

* 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).

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 , Event-B, or other refinement frameworks. We assume that some variables of the abstract transition system () 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 . 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 .

To reason about and the concrete implementation within one program logic, we embed as global ghost state into the concrete implementation: each variable of is represented as a ghost variable of the program.

The concrete program must implement the transitions of 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 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.

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:overview).

* 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:preliminaries and sec:methodology).

* 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:evaluation). 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.

\[
\begin{array}{l}
\texttt{Vars:} \;	\texttt{count: Int,~stdOut: Seq[Int]}\\
\texttt{Init:} \;0 \leq 	\texttt{count} \wedge 	\texttt{stdOut} = []\\
\texttt{Next:} \;	\texttt{stdOut}' = 	\texttt{stdOut ++ [count]} \wedge
\texttt{count}' = 	\texttt{count} + 1
\end{array}
\]

Abstract model of our example. Here, unprimed and primed variables refer the variables values before and after the transition, respectively.

Abstract Model.
The abstract model of our system is defined in fig:example-abstract. We represent the output stream of the system  as a sequence of integers. This variable belongs to the environment, whereas  is internal to the system. The initial state has an arbitrary non-negative value for , which illustrates the common case that abstract models choose values non-deterministically. A valid transition
adds the current value of  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:

We assume that the environment variable  is predeclared for each program. It is manipulated via a  statement, which requires ownership of  (in the sense of separation logic: $\alloc{\texttt{stdOut}}{}$) and appends its argument  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  and  only according to the abstract model presented in fig:example-abstract. We 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  ghost statement, which checks the  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  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  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  statement executes one transition of the abstract model (or stutters). The block of a  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  and  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  statement and, thus, the  relation of the abstract model is checked on each modification. In our example, the ghost lock invariant contains fractional ownership of the  variable and full ownership of :

\[
\alloc{\texttt{count}}{\frac{2}{3}} ~\sep~
\alloc{\texttt{stdOut}}{}
\]

Our proof rules enforce that —the only way to modify $\texttt{stdOut}$—can be executed only after the ghost lock has been initialized with an  statement. Consequently, the above lock invariant guarantees that  operations can occur only within a  block and, thus, all changes to the environment are checked to comply with the abstract model. We assume that  is atomic, which is standard for I/O operations.

\begin{align*}
& \Assign{\texttt{count}}{0}\Seq \\[-1mm]
& \Initialize~\{ \\[-1mm]
& \qquad \Assign{\texttt{evenTurn}}{\True}\Seq
\Assign{\texttt{lastEven}}{-1}\Seq
\Assign{\texttt{lastOdd}}{0}\Seq \\[-1mm]
& \qquad \DeclareLock{\Lock} \{ ~
\text{/* even-thread */} \,\Par\, \text{/* odd-thread */ }~ \} \\[-1mm]
& \}
\end{align*}

The concrete implementation of our example. The even-thread is presented in fig:example-even; the odd-thread is analogous.

fig:example-main shows the concrete implementation. After initializing the abstract state, the  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 . Note that our implementation fixes a concrete initial value for , whereas the abstract model permits an arbitrary non-negative number (see fig:example-abstract). Resolving non-determinism is very common during refinement. We explain the body of the  statement below.

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:

This variable is protected by a global (regular, non-ghost) lock $\Lock$.

\begin{align*}
& \texttt{var}~\Assign{\texttt{c}}{0}\Seq \\[-3mm]
& \While{\True}~\texttt{invariant~lastEven} \xmapsto{\frac{1}{2}} 2 * \texttt{c} - 1\\[-1mm]
& \{ \\[-1mm]
& \qquad\With{\Lock}{\texttt{evenTurn}}~\{ \\[-1mm]
& \qquad\qquad\Next~\{\quad\texttt{/*}~\text{print + ghost update}~\texttt{*/} \\[-1mm]
& \qquad \qquad\qquad \Print{2 * \texttt{c}}\Seq
\Assign{\texttt{count}}{\texttt{count}+1}~\}\quad \\[-1mm]
& \qquad\qquad \Assign{\texttt{lastEven}}{\texttt{lastEven} + 2}\Seq \\[-1mm]
& \qquad\qquad \Assign{\texttt{evenTurn}}{\texttt{!evenTurn}}\Seq \\[-1mm]
& \qquad\qquad \Assign{\texttt{c}}{\texttt{c}+1}~\\[-1mm]
& \qquad\}\quad\texttt{/*}~\text{release lock \Lock}~\texttt{*/} \\[-1mm]
&  \}
\end{align*}

Implementation of the thread that prints the even numbers. The  block marks an atomic transition; its body is atomic because the  statement is atomic and the subsequent assignment is a ghost statement.

fig:example-even 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 $\Lock$ (waiting until  is true resp. false), execute a transition (explained later), flip , and release the lock.

Each thread has a local variable  that counts how many numbers it has printed. This design illustrates that our methodology supports flexible combinations of global concrete state (such as ) and local concrete state (such as ). 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  is equal to $2*\texttt{c}$ in case  is true. This condition allows us to prove that the  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 , which would prevent the odd-thread from ever updating it.

A relation between the local variable  and the shared variable  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  and  that keep track of the effect of each individual thread:

We relate these ghost variables to the local variable  in each thread via the thread's loop invariant (see fig:example-even), and also to the global  via the lock invariant of lock $\Lock$:

\[
\begin{array}{l}
\pt{\texttt{evenTurn}}{}{\_} \sep
\pt{\texttt{lastEven}}{\frac{1}{2}}{\_} \sep
\pt{\texttt{lastOdd}}{\frac{1}{2}}{\_} \sep
\pt{\texttt{count}}{\frac{1}{3}}{\_} \sep\\
(\texttt{evenTurn} \Rightarrow 	\texttt{count} = 	\texttt{lastOdd} \wedge 	\texttt{lastEven} = 	\texttt{lastOdd} - 1) \sep \\
(\neg \texttt{evenTurn} \Rightarrow 	\texttt{count} = 	\texttt{lastEven} \wedge 	\texttt{lastOdd} = 	\texttt{lastEven} - 1)
\end{array}
\]

The lock and the loop invariants together form the coupling invariant for our example. For the even-thread, we get $\texttt{lastEven} = 2*c-1$ from the loop invariant,  from the -statement, and
$(\texttt{evenTurn} \Rightarrow 	\texttt{count} = 	\texttt{lastOdd} \wedge 	\texttt{lastEven} = 	\texttt{lastOdd} - 1)$ from the lock invariant. These three conditions together imply $	\texttt{count}=2*c$, which is required to show that the printed value is permitted by the abstract model.

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, . 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 logic-based verification techniques.

To make this claim more concrete, we will formalize (in sec:methodology)
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 of commands in our programming language is
given by the grammar

\begin{align*}
\Command \quad\cceq\quad
& \SimpleCommand \\
|~ & \Command \Seq \Command \\
|~ & \If{\BB} \Block{ \Command } \Else \Block{ \Command } \\
|~ & \While{\EE} \Block{\Command} \\
|~ & \Command \Par \Command \\
|~ & \DeclareLock{\Lock}\Block{\Command} \\
|~ & \With{\Lock}{\EE} \Block{ \Command } \\
|~ & \Within{\Lock} \Block{ \Command }  semantics
\end{align*}

\begin{align*}
\SimpleCommand \quad\cceq\quad
& \Skip \\
|~ & \Assign{\Var}{\EE} \\
|~ & \Mutation{\EE}{\EE} \\
|~ & \Lookup{\Var}{\EE} \\
|~ & \Free{\EE} \\
|~ & \New{\Var}{\EE} \\
& \\
\end{align*}

where $x$ is a variable in the set $\Vars$,
$\EE$ is an expression over variables,
and $\Lock$ is a lock identifier taken from the arbitrary, but finite
set $\Locks = \Set{\Lock,\ldots}$.

We briefly go over our language:
in addition to the assignment $\Assign{x}{\EE}$ and the usual control-flow structures,
$\Command_1\Par\Command_2$ is the parallel composition of $\Command_1$ and $\Command_2$;
$\DeclareLockBlock{\Lock}{\Command}$ declares a new lock $\Lock$ that can be used in $\Command$ and expires after termination of $\Command$;
the conditional critical region (CCR)
$\WithBlock{\Lock}{\EE}{\Command}$ acquires lock if condition $\EE$ holds (and waits otherwise), executes , and releases again upon termination of $\Command$;
$\WithinBlock{\Lock}{\Command}$ is an internal command that we will use to indicate that $\Command$ is executed while holding the lock $\Lock$.
Furthermore,  denotes the value at the memory address given by .
$\Lookup{\Var}{\EE}$ reads the value at address and assigns it to ;
' writes the value of $\EE'$ to the address .
Moreover,  disposes of location , and $\New{\Var}{\EE}$ allocates a free memory address, assigns it to , and stores 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 $(\Stack,\PHeap)$ consists of a stack , , a valuation
of variables, and a heap modeling dynamically allocated memory.
Formally, we fix a set $\Vals = \Set{\Val,\ldots}$ of values containing, , Booleans, integers, and sequences. The set consists of all mappings from variables in $\Vars$
to values in $\Vals$, ,

\[ \Stacks \ddefeq \Vars \to \Vals~. \]

Moreover, we fix a countably infinite set $\Locs$ of memory addresses, and the set $\PermsSym \defeq \Perms$ of fractional permissions, where permission $\Perm = \PermWrite$ means write access, $\Perm \in (0,1)$ means read access, and $\Perm = \PermNone$ means no access, respectively.

The set of heaps consists of all finite partial functions that map addresses in their domain $\dom{\PHeap} \subseteq \Locs$ to permission-value pairs, ,

\begin{align*}
\PHeaps \ddefeq \Locs \fpto (\PermsSym \times \Vals)~.
\end{align*}

For $\PHeap(\Loc) = (\Perm,\Val)$, we define the projections
$\HPerm{\PHeap(\Loc)} = \Perm$ and $\HVal{\PHeap(\Loc)} = \Val$.
We denote by $\Set{\Loc_1 \xmapsto{\Perm_1} \Val_1, \ldots, \Loc_n \xmapsto{\Perm_n} \Val_n}$ the heap $\PHeap$ with $\dom{\PHeap} = \Set{\Loc_1,\ldots,\Loc_n}$ and $\PHeap(\Loc_i) = (\Perm_i,\Val_i)$, where $i \in \Set{1,\ldots,n}$; the empty heap is denoted by $\EmptyHeap$.

The addition of $\PHeap_1 \Add \PHeap_2$ of heaps $\PHeap_1$ and $\PHeap_2$ is defined as

\begin{align*}
(\PHeap_1 \Add \PHeap_2)(\Loc) \ddefeq
\begin{cases}
(\Perm_1 + \Perm_2,\Val) & \tif \Loc \in \dom{\PHeap_1} \cap \dom{\PHeap_2} \tand \PHeap_1(\Loc) = (\Perm_1,\Val)  \\
& \qquad\qquad \tand \PHeap_2(\Loc) = (\Perm_2,\Val) \tand \Perm_1 + \Perm_2 \leq \PermWrite \\
\PHeap_1(\Loc) & \tif \Loc \in \dom{\PHeap_1} \setminus \dom{\PHeap_2} \\
\PHeap_2(\Loc) & \tif \Loc \in \dom{\PHeap_2} \setminus \dom{\PHeap_1} \\
\undefined & \text{otherwise}.
\end{cases}
\end{align*}

We write $\isDefined{\PHeap_1 \Add \PHeap_2}$ if ($\PHeap_1 \Add \PHeap_2(a)$ is well-defined for all $a \in \dom{\PHeap_1} \cup \dom{\PHeap_2}$.
$\PHeap\Update{\Loc}{\Val}$ denotes the heap $\PHeap$ except that $\Loc$ maps to $\Val$ (with permission $\PermWrite$), ,

\begin{align*}
\PHeap\Update{\Loc}{\Val}(\Loc') \ddefeq
\begin{cases}
(\PermWrite, \Val) & \tif \Loc' = \Loc \\
\PHeap(\Loc') & \tif \Loc' \neq \Loc~.
\end{cases}
\end{align*}

For every stack $\Stack$, $\Stack\Update{\Var}{\Val}$ is defined analogously.
We define the heap
$\PHeap\Delete{\Loc} \defeq \Set{\Loc' \mapsto \PHeap(\Loc') \mid \Loc' \in \dom{\PHeap} \setminus \{\Loc\}}$, which is obtained from $\PHeap$ by removing $\Loc$ from its domain.
Finally, the set of normal heaps consists of all heaps $\Heap$ that assign the  full permission $\PermWrite$ to every address, ,

\begin{align*}
\Heaps \ddefeq \Set{ \PHeap \in \PHeaps ~|~ \forall \Loc \in \dom{\PHeap} \mydot \HPerm{\PHeap(\Loc)} = \PermWrite }~.
\end{align*}

We typically write $\Heap$ instead of $\PHeap$ to highlight that a heap is normal; by slight abuse of notation, we use $\Heap(\Loc)$ as a shortcut for $\HVal{\Heap(\Loc)}$.
Clearly, for every heap $\PHeap$, there exists a heap $\PHeap'$ such that $\PHeap \Add \PHeap'$ 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
$\EE$ is associated with a function
$\EE\colon \Stacks \to \Vals$
such that $\EE(\Stack)$ is the value obtained from evaluating $\EE$ in stack $\Stack$.

The set $\Confs$ of program configurations consists of all
command-stack-normal-heap triples plus a dedicated error state , that is,

\begin{align*}
\Confs \ddefeq (\Commands \times \Stacks \times \Heaps) ~\cup~ \Set{\Abort}~.
\end{align*}

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 $\OpRel \subseteq \Confs \times \Confs$ given by the rules in fig:operational.

Rules of the small-step operational semantics for commands in $\Commands$.
Here, $\Locked{\Command}$ is the set of all locks $\Lock$ held by $\Command$, ,
$\WithinBlock{\Lock}{\ldots}$ is a sub-command of $\Command$.
Furthermore, $\Reads{\Command}{\Stack}$ (resp. $\Writes{\Command}{\Stack}$) denotes the
set of those addresses $\Loc$ that are not exclusively owned by $\Command$, , appear
only in sub-commands $\NextBlock{\ldots}$ or $\WithBlock{\Lock}{\EE}{\ldots}$), and
are accessed (resp. modified) by given stack $\Stack$.

Most rules in fig:operational are standard ( [35]) and reflect the behavior informally explained in sec:sound:language; 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, $\DeclareLockBlock{\Lock}{\CC}$ indicates that is declared in ; the internal command $\WithinBlock{\Lock}{\CC}$ indicates that holds $\Lock$ during its execution.
We denote by $\DLocks{\CC}$ the set of all locks that are declared in .
Analogously,  denotes the set of all locks that are currently held by .
For example, if $\CC'$ is not of the form $\DeclareLockBlock{\Lock}{\ldots}$ or $\WithinBlock{\Lock}{\ldots}$, and
$\CC$ is given by

\begin{align*}
\DeclareLockBlock{\Lock_1}{
\DeclareLockBlock{\Lock_2}{
\ldots
\DeclareLockBlock{\Lock_n}{
\WithinBlock{\Lock_1'}{
\ldots
\WithinBlock{\Lock_m'}{
\CC'
} \ldots
\end{align*}

then $\DLocks{\CC} = \Set{ \Lock_1, \ldots, \Lock_n}$
and $\Locked{\CC} = \Set{ \Lock_1', \ldots, \Lock_m' }$.

The semantics of $\DeclareLockBlock{\Lock}{\CC}$ consequently keeps the lock $\Lock$ declared and performs a step of $\CC$ until termination; after that, the lock declaration expires.

CCRs and Parallel Composition.
For CCRs $\WithBlock{\Lock}{\EE}{\CC}$, we first check whether condition holds in the current state.
If so, we acquire lock $\Lock$ and enter the CCR by moving to the internal command $\WithinBlock{\Lock}{\CC}$, which will execute , and release the lock upon termination of .
If does not hold, no transition is possible, , we need to wait for other threads.

The rules for the parallel composition $\CC_1 \Par \CC_2$ model all interleaved executions of $\CC_1$ and $\CC_2$.
They include a sanity check stating that $\CC_1$ and $\CC_2$ do not hold the same lock at the same time, , locks provide mutual exclusion.
Moreover, there is a rule that prematurely aborts executions whenever a command admits a data race, that is, $\CC_1$ (resp. $\CC_2$) writes to and $\CC_2$ (resp. $\CC_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.

§.§ Assertions

The syntax of separation logic assertions
includes, amongst others,
all Boolean expressions $\EE$ supported by our programming language
Formally, the set $\SL$ of separation logic assertions is given by the grammar

\begin{align*}
\PP \cceq
\EE ~|~ &  \PP \wedge \PP ~|~
\neg \PP ~|~
\fa{\Var} \PP ~|~ \ex{\Var} \PP \tag{FOL} \\
|~ & \emp ~|~ \pt{\EE}{\Perm}{\EE}
~|~  \PP \sep \PP ~|~ \PP \mw \PP~ ~|~ \bigstar_{i \in I}\,\PP_i~,
\tag{SL}
\end{align*}

where $\EE$ is a Boolean expression over variables,
$\Var$ is a variable in $\Vars$,
$\Perm$ is a permission in $\PermsSym$,
and $I$ is a finite set such that each $i \in I$ is associated with an assertion $\PP_i$.

We use syntactic sugar, such as
$\PP \Implies \PQ$, $\PP \vee \PP$ and, in particular,
$\apt{\EE}{\Perm}{\EE} \defeq \pt{\EE}{\Perm}{\EE} \sep \True$, $\alloc{\EE}{\Perm} \defeq \ex{y} \apt{\EE}{\Perm}{y}$, and
$\acc{\EE}{\Perm} \defeq \ex{y} \apt{\EE}{\Perm}{y}$.

We denote by $\FOL$ the set of all first-order logic formulas, , those
formulas that can be constructed from the first line of the above grammar.

Assertions are interpreted over pairs $(\Stack,\PHeap)$ consisting of a stack and a heap (with permissions) .
tab:assertion-semantics shows the formal semantics of assertions.

Intuitively, $\emp$ specifies the empty heap;
the points-to assertion $\pt{\EE}{\Perm}{\EE'}$ specifies that the heap contains
exactly one address $\EE$ that is mapped to $\EE'$ with permission $\Perm$;
$\apt{\EE}{\Perm}{\EE'}$ is an intuitionistic version stating that the heap contains
at least permission $\Perm$ for the address $\EE$, which is mapped to $\EE'$.
$\alloc{\EE}{\Perm}$ and $\acc{\EE}{\Perm}$ are analogous but do not require a specific
value at the address given by $\EE$.
The separating conjunction $\PP \sep \PQ$ specifies that the heap can be partitioned into two parts such that one part satisfies and the other part satisfies .
$\bigstar_{i \in I}\,\PP_i$ is an iterative version of the separating conjunction.
Finally, the magic wand $\PP \mw \PQ$ specifies that holds in a heap after it has been extended by any heap that satisfies (and can be added to ).

We call an assertion $\PP$ valid, written $\valid \PP$, if and only if
$\Stack,\PHeap \models \PP$ holds for all stacks $\Stack \in \Stacks$ and heaps $\PHeap \in \PHeaps$.

Semantics of assertions.

$\PP$     $\Stack, \PHeap \models \PP \qiff$

$\EE$     (s) =

$\PQ \wedge \PR$     $\Stack, \PHeap \models \PQ$ and $\Stack, \PHeap \models \PR$

$\neg\PQ$     $\Stack, \PHeap \not\models \PQ$

$\fa{\Var} \PQ$     for all $\Val \in \Vals$, $\Stack\Update{\Var}{\Val},\PHeap \models \PQ$

$\ex{\Var} \PQ$     exists $\Val \in \Vals$ s.t. $\Stack\Update{\Var}{\Val},\PHeap \models \PQ$

$\emp$     $\dom{\PHeap} = \emptyset$

$\PQ \sep \PR$     exists $\PHeap_1,\PHeap_2$ s.t. $\PHeap = \PHeap_1 \PermAdd \PHeap_2$
and $\Stack,\PHeap_1 \models \PQ$ and $\Stack,\PHeap_2 \models \PR$

$\PQ \mw \PR$     for all $\PHeap'$, ($\isDefined{\PHeap \Add \PHeap'}$ and $\Stack, \PHeap' \models \PQ$) implies
$\Stack,\PHeap \PermAdd \PHeap' \models \PR$

$\bigstar_{i \in I}\,\PP_i$     $I = \emptyset$ or exists $j \in I$ s.t. $\Stack,\PHeap \models \PP_j \sep \bigstar_{i \in I \setminus \{j\}}\,\PP_i$

We denote by $\FV{\PP}$ the set of free variables (, those that are not bound by quantifiers) of assertion $\PP$.
Moreover, $\PP\subst{\Var}{\Val}$ denotes the substitution of every free occurrence of
variable $\Var$ in assertion $\PP$ by $\Val$.

§.§ 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 ( sec:sound:semantics), which has a global view on the full program state, the CSL proof system considers only the local state , 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 $\Lock$ with a lock invariant $\PR$ that specifies the part of the global state that is protected by $\Lock$.

Formally, the assignment of lock invariants to locks is
captured by a lock environment $\LockEnv$, which is given by the grammar

\begin{align*}
\LockEnv \cceq &
\emptyset ~|~ \LockEnv, \LockDef{\Lock}{\PR}~,
\end{align*}

where $\Lock \in \Locks$ and $\PR$ is an $\SL$ assertion representing the lock invariant.
Moreover, given a lock environment $\LockEnv$,
the lock invariant of lock $\Lock$ is

\begin{align*}
\LockEnv(\Lock) \ddefeq
\begin{cases}
\PR & \tif \LockEnv = \LockEnv', \LockDef{\Lock}{\PR} \\
\LockEnv'(\Lock) & \tif \LockEnv = \LockEnv', \LockDef{\Lock'}{\PR'} \tand \Lock' \neq \Lock  \\
\emp & \tif \LockEnv = \emptyset~.
\end{cases}
\end{align*}

Intuitively, if $\LockEnv(\Lock) = \PR$, then $\PR$ 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 $\LockEnv(\Lock) = \emp$, then $\Lock$ does not appear in $\LockEnv$ (or the declared invariant is $\emp$) and nothing is shared with other threads.

Declaring, acquiring, and releasing the lock $\Lock$ can be understood as a transfer of the portion of the state specified by $\PR$ between the local state and , , the part of the global state that is shared with other threads:
whenever we declare , is shared with other threads and thus moved from the local state into ; once the declaration expires, is transferred back into the local state.
Whenever we acquire the lock $\Lock$, is moved from $\LockEnv$ into the local state; whenever we release the lock $\Lock$, $\PR$ is moved back from the local state into $\LockEnv$.

CSL Judgments.

Judgments that can be derived in CSL are of the form

\begin{align*}
\striple{\PP}{\CC}{\PQ}~,
\end{align*}

is a lock environment such that $\bigstar_{\Lock \in \Locks} \LockEnv(\Lock)$
describes the shared state,
$\PP \in \SL$ is the precondition evaluated in the local state,
is a command in , and
$\PQ \in \SL$ is the postcondition evaluated in the local state.

fig:proof-rules 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].

Inference rules inherited from concurrent separation logic.
Here, $\Perm$ is a permission; $\Mod{\Command}$ denotes all variables
modified by command , , those that appear on the left-hand side of
assignments. Moreover, $\FV{\EE}$, $\FV{\CC}$, and $\FV{\LockEnv}$ denote the
free variables of in expression $\EE$, command (, all variables accessed by ),
and lock environment (, the union of $\FV{\LockEnv(\Lock)}$
for all $\Lock \in \Locks$), respectively.
Furthermore,  we define
$\FV{A,B,C} \defeq \FV{A} \cup \FV{B} \cup \FV{C}$.
Finally, an assertion $\PP$ is precise iff
for all $\Stack$, $\PHeap_1,\PHeap_2,\PHeap_1',\PHeap_2'$,
if _1 _2 and
$\PHeap_1 \Add \PHeap_2 = \PHeap_1' \Add \PHeap_2'$
and $\Stack,\PHeap_1 \models \PP$ and
and $\Stack,\PHeap_2 \models \PP$, then $\PHeap_1 = \PHeap_2$.

§ METHODOLOGY AND FORMALIZATION

We now present the details of our methodology and formalize it on
top of the concurrent separation logic (CSL) introduced in

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, , 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:sound:assertions the definition
of heap-independent assertions in first-order logic ().
Moreover, given a sequence of variables $\vec{x} = (x_1, \ldots, x_k)$ , we denote by
$\Primed{\vec{x}}$ the same sequence in which each $x_i$ is replaced
by a primed version, , $\Primed{\vec{x}} = (\Primed{x_1}, \ldots, \Primed{x_k})$.

An abstract transition system is a quadruple
$\AbsTS \defeq (\AbsLength,\AbsVars, \AbsInit, \AbsNext)$, where

* $\AbsVars = (\AbsVar{1}, \ldots, \AbsVar{\AbsLength})$ is a
repetition-free sequence of $\AbsLength \geq 1$ variables,

* the initial state formula $\AbsInit(\AbsVars)$ is an $\FOL$ assertion over $\AbsVars$, and

* the next state formula $\AbsNext(\AbsVars, \Primed{\AbsVars})$ is an $\FOL$ assertion over $\AbsVars$ and $\Primed{\AbsVars}$.

We consider only ATSs that are stutter-invariant,
that is, for all sequences of values $\vec{\Val} \in \Vals^{\AbsLength}$, the formula
$\AbsNext(\vec{\Val},\vec{\Val})$ 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 next-state
\AbsNext(\AbsVars,\Primed{\AbsVars}) ~\vee~ \bigwedge_{1 \leq i \leq \AbsLength} \Primed{\AbsVar{i}} = \AbsVar{i}$.

Throughout the rest of this paper, we fix a stutter-invariant
abstract transition system
$\AbsTS \defeq (\AbsLength,\AbsVars, \AbsInit, \AbsNext)$ representing
the abstract model we would like to prove refinement of.

To reason about refinement, we need to formalize the observable traces
of $\AbsTS$.
Every evaluation of an 's variables $\AbsVars$
constitutes one of its states.
Formally, the state space of $\AbsTS$ is $\AbsStates \defeq \Vals^{\AbsLength}$.
A (finite) path of $\AbsTS$ is a sequence of states $\AbsState_1 \ldots \AbsState_n$, where $n \geq 1$, such that

* $\valid \AbsInit(\AbsState_1)$, , $\AbsState_1$ is an initial state of , and

* for all $i \in [1,n)$, we have $\valid \AbsNext(\AbsState_i,\AbsState_{i+1})$, ,
for every state but the last one, $\AbsTS$ admits a transition to the next state on the path.

We collect in the set $\AbsPaths$ all finite paths of the transition system $\AbsTS$.

A trace then projects every state on a path to the values corresponding to those variables
that are observable, , variables modeling I/O channels as outlined in sec:overview.
For simplicity, we assume that exactly one variable, $\AbsVar{1}$,
is observable; generalizing to arbitrary sets of observable variables is
We denote by $\Obs{\AbsState}$ the projection of state $\AbsState$ to the value assigned
to the observable variable $\AbsVar{1}$, that is, if $\AbsState = (\Val_1,\ldots,\Val_\AbsLength)$, then
$\Obs{\AbsState} = \Val_1$.

The set $\AbsTraces$ of observable traces of $\AbsTS$ is given by

\begin{align*}
\AbsTraces \ddefeq \{
\Obs{\AbsState_1} \ldots \Obs{\AbsState_n}
& n \in \Nats \tand \\
& \AbsState_1 \ldots \AbsState_n \in \AbsPaths
\}. \tag*{\EndDef}
\end{align*}

State Encoding.

To reason about the behavior of $\AbsTS$s with the machinery
offered by concurrent separation logic ( sec:preliminaries),
we encode states of $\AbsTS$s within program states—more precisely: as part of the heap.

We fix a set $\ALocs \subseteq \Locs$ of dedicated ghost addresses that cannot be allocated or disposed of—they thus need to be already allocated before program execution.

Every variable $\AbsVar{i}$ of is then encoded as a ghost address
$\AbsLoc{i} \in \ALocs$ at which we store the current evaluation of
We use $\stdout$ as a synonym for $\AbsLoc{1}$—the address of the only observable variable $\AbsVar{1}$.

Given a heap $\PHeap$, the contents of the addresses $\AbsLocs$ in $\PHeap$
encode the current state of $\AbsTS$.
We introduce a function $\AbsLocsOfName\colon \PHeaps \to \AbsStates$
which extracts the transition system's state from the heap:

The state extraction function $\AbsLocsOfName\colon \PHeaps \to \AbsStates$ is

\begin{align*}
\AbsLocsOf{\PHeap} \ddefeq
\begin{cases}
(\Val_1,\ldots,\Val_\AbsLength) & \tif \AbsLocs \in \dom{\PHeap} \tand \\
& \quad \text{for all } i \in [1,\AbsLength], ~ \PHeap(\AbsLoc{i}) = (\Perm_i,\Val_i) \\
& \qquad\qquad\qquad\qquad \tand \Perm_i > \PermNone \\
\undefined & \text{otherwise}~. $\EndDef$
\end{cases}
\end{align*}

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 .

Ghost Locks.

We employ a dedicated lock $\GhostLock$ to protect the ghost locations
$\AbsLocs$ representing the current state of the abstract model $\AbsTS$
from undesirable modifications.
To this end, we require that any lock invariant $\GhostInv$ chosen for $\GhostLock$
contains some permission to each of the locations $\AbsLocs$—thus preventing modification of their content without acquiring $\GhostLock$ first. Formally:

For any lock invariant $\GhostInv$ associated with the ghost lock $\GhostLock$,
there exists a permission $\Perm > 0$ such that the following entailment is valid:

\begin{align*}
\valid~~ \big(
\GhostInv
\quad\Rightarrow\quad
\acc{\AbsLoc{1}}{\Perm} \sep \ldots \sep
\acc{\AbsLoc{\AbsLength}}{\Perm}
\big)
\tag*{\EndDef}
\end{align*}

Our methodology prescribes that 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 $\GhostLock$
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 $\Initialize$ and $\Next$ in a way such that
$\GhostLock$ is indeed a ghost lock.

§.§ Programming Language and Operational Semantics

We now extend the programming language from
sec:sound:language with
an output operation $\Print{\EE}$
the refinement-specific commands $\InitializeBlock{\CC}$ and $\NextBlock{\CC}$.
Formally, we expand the grammar in
sec:sound:language as follows:

\[
\Command \cceq
\Print{\EE}
~|~ \InitializeBlock{\CC} ~|~ \NextBlock{\CC}
~|~ \ldots
\]

We use ghost addresses taken from $\ALocs$ to formalize
the semantics of each of the above commands; fig:operational:novel summarizes how we formally extend the execution relation $\OpRel$ from sec:sound:semantics.
We briefly go over the new rules:

Extension of the rules in fig:operational that determine the operational semantics.
Here, $\OpRelTrans$ denotes the reflexive and transitive closure of execution relation $\OpRel$.

$\Print{\EE}$ appends the value of $\EE$ to the standard output stream, which we represent by a mathematical sequence stored at the ghost address $\stdout \in \ALocs$.
Print thus modifies the only observable variable of the abstract mode $\AbsTS$.
If $\stdout$ has not been allocated, we abort execution.

The command $\InitializeBlock{\CC}$ is, operationally speaking, a dedicated command for declaring the ghost lock $\GhostLock$.
In fact, the rule Init desugars it to an explicit lock declaration $\DeclareLockBlock{\GhostLock}{\CC}$.[While we do not allow programmers to explicitly use the ghost lock $\GhostLock$, the rules of our operational semantics can use it like any other lock.]
Conceptually, $\Initialize$ takes the important role of marking the system as initialized, , after entering $\Initialize$, the concrete model must be in an observable state that matches the (observable part of) the abstract model's initial state.

The command  is, operationally speaking again, a dedicated command for the conditional critical region
that acquires the ghost lock $\GhostLock$, executes $\CC$, and releases $\GhostLock$, that is, it can be viewed as syntactic sugar for $\WithBlock{\GhostLock}{\True}{\Command}$.

However, to ensure that $\GhostLock$ is indeed a ghost lock and can thus be safely erased at runtime, we additionally require that every command $\CC$ put into a $\NextBlock{\CC}$ block is atomic.
That is, $\CC$ can be executed in a single step without interference from other threads.
Consequently, $\NextBlock{\CC}$ is atomic and thus executed in a single step, as reflected by the Next rule: if the execution of $\Command$ terminates in a configuration $\Configuration$, then
$\NextBlock{\CC}$ transitions to configuration $\Configuration$ in a single step.

We assume that I/O operations, such as $\Print{\EE}$, 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 ( sec:overview).

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 ,
we project every program configuration in an execution
$\Configuration_1 \ldots \Configuration_n$ to its observable state once the system has been initialized, which is recorded by the operational semantics in its command structure:

A command $\Command$ is initialized, written $\isInit{\Command}$, if and only if the ghost lock $\GhostLock$ is declared in $\Command$, , $\GhostLock \in \DLocks{\Command}$.

In our formalization, only the content of the standard output stream, which is modified via $\Print{\EE}$ calls, is observable.
The observable state $\Obs{\Configuration}$ of a configuration
$\Configuration$ is defined as the empty or singleton sequence

\begin{align*}
\Obs{\Configuration} \ddefeq
\begin{cases}
\left[ \Heap(\stdout) \right] & \tif \Configuration = (\Conf{\CC}{\Stack}{\Heap})
\tand \isInit{\CC} \\
\left[ ~ \right] & \text{otherwise}.
\end{cases}
\end{align*}

A trace is then obtained from a (finite) execution
by mapping configurations to their observable state and concatenating the resulting sequences:

The set  of finite traces induced by a set
$\InitialConfs \subseteq \Confs$ is

\begin{align*}
\Traces{\InitialConfs} \ddefeq \{\,
\Obs{\Configuration_1} \ldots \Obs{\Configuration_n}
\mid\, &
n \in \Nats
\tand \Configuration_1 \in \InitialConfs, \Configuration_2,\ldots,\Configuration_n \in \Confs \\
& \tand \Configuration_1 \OpRel \ldots \OpRel \Configuration_n
\,\}~. \tag*{\EndDef}
\end{align*}

The definition of $\Obs{}$ ignores the observable state as long as the system is not initialized, , we have not reached $\InitializeBlock{\ldots}$ 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:sound:logic 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, , it consists of all $\SL$ assertions (see sec:sound:assertions).

Judgments that can be derived in our logic
(notice the $\vdash_{\refineIndicator}$ to distinguish our judgments from CSL judgments)
are of the form

\begin{align*}
\srtriple{\PP}{\CC}{\PQ}~,
\end{align*}

is a lock environment such that $\bigstar_{\Lock \in \Locks} \LockEnv(\Lock)$
describes the shared state,
$\PP \in \SL$ is the precondition evaluated in the local state,
is a command
$\PQ \in \SL$ is the postcondition evaluated in the local state.

fig:proof-rules-novel shows the proof rules for the new commands $\Initialize$, $\Next$, and $\Print{\EE}$.
Furthermore, our proof system inherits all proof rules from CSL ( fig:proof-rules where we tacitly replace $\vdash$ by $\vdash_{\refineIndicator}$ and exclude dedicated
ghost locks in the rules $\Rule{Lock}$ and $\Rule{With}$).
We briefly go over the rules for the new commands:

Proof rules for the new commands.
Here, $\vec{o} = (o_1,\ldots,o_\AbsLength)$ are fresh variables.
Moreover, for some $\Perm > 0$,
$\Aabsvars{\vec{y}} \defeq
\apt{\AbsLoc{1}}{\Perm}{y_1} \sep \ldots \sep
\apt{\AbsLoc{\AbsLength}}{\Perm}{y_\AbsLength}$.

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 $\GhostLock$ with
lock invariant $\GhostInv$ and a second dedicated ghost lock $\InitLock$ with an empty lock

The ghost lock $\GhostLock$ has already been used in our operational semantics; it governs
access to the state of the abstract model .
The lock $\InitLock$ 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, , the contents
$y_1,\ldots,y_\AbsLength$ of the ghost addresses $\AbsLocs$, is a valid initial state in , ,
$\AbsInit(y_1,\ldots,y_\AbsLength)$ holds.
By ass:ghostlock, we know that the ghost lock's invariant $\GhostInv$
holds the necessary permissions to access the contents of these ghost addresses.

Regarding the second ghost lock $\InitLock$,
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:cmd:traces, 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 .
To guarantee that there are indeed no modifications of observable state—in our case: there are no $\Print{\EE}$ calls—before initialization, we use the ghost lock $\InitLock$.
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 $\GhostLock$), 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 $\GhostLock$ and wait condition . However, it contains an additional premise to ensure that
executing $\NextBlock{\CC}$ can be simulated by taking a single transition of . Since $\CC$ is atomic, the postcondition $\AbsNext(\vec{o},\vec{y})$ in the premise achieves this effect (where $\vec{o}$ and $\vec{y}$
capture the state of $\AbsTS$ before and after execution of $\NextBlock{\CC}$).

For initialized commands, ass:ghostlock guarantees that changes to the transition
system's state are possible only when holding the lock $\GhostLock$, , inside
of $\NextBlock{\CC}$ blocks; outside of such blocks, $\AbsTS$ will
perform a stutter step for every step of the concrete implementation.

Print Statements.
Finally, to understand the Print rule,
we notice that $\Print{\EE}$ is—if we ignore atomicity—syntactic sugar for the command

\[
\Command \ddefeq
\Lookup{\Var}{\stdout}\Seq\Mutation{\stdout}{\Append{\EE}{\Var}},
\]
where $\Var$
is a fresh variable that is not used anywhere else.
Assuming that $\Print{\EE}$ and $\Command$ are identical,
the rule Print can then be derived using the standard rules in fig:proof-rules (in sequential separation logic, , for $\LockEnv = \emptyset$).

§.§ Soundness

Intuitively, soundness means that deriving $\srtriple{\PP}{\CC}{\PQ}$ implies that, for every execution of $\CC$
that starts in a configuration with a local state given by $\PP$ and a shared state given by $\LockEnv$,
the trace of the execution is also a trace of the abstract model $\AbsTS$.

We now formalize and prove the above soundness claim for our refinement logic.
We build upon Vafeiadis' [35] existing soundness proof for CSL ( sec:preliminaries).
Hence, we first restate the main ingredients for proving CSL sound, where we slightly generalize to simplify their re-use.

Let $\Succ(\Configuration,\Configuration')$ be a predicate over two program configurations; we will use $\Succ(\Configuration,\Configuration')$ only if there is a transition
$\Configuration \OpRel \Configuration'$.
Soundness of CSL as well as our refinement logic is based
on the following notion of configuration safety:

The $n$-step safety predicate
is recursively defined as follows:

* $\Safe{\Succ}{0}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ holds always.

* $\Safe{\Succ}{n+1}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ holds if and only if

* $\Reads{\CC}{\Stack} \subseteq \dom{\PHeap}$;

* for all $\HeapF$, if $\isDefined{\PHeap \Add \HeapF}$, then $(\Conf{\CC}{\Stack}{\PHeap \Add \Heap}) \NOpRel \Abort$;

* if $\CC = \Skip$, then $\Stack,\Heap \models \PQ$;

* for all $\CC'$, $\Stack'$, $\HeapF$, $\HeapS$, $\PHeap'$, if
$\Stack,\HeapS \models \bigstar_{\Lock \in \Locked{\CC'}\setminus\Locked{\CC}} \LockEnv(\Lock)$

$(\Conf{\CC}{\Stack}{\PHeap \Add \HeapS \Add \HeapF}) \OpRel (\Conf{\CC'}{\Stack'}{\PHeap'})$, then there exist $\PHeap''$ and $\HeapS'$ such that

* $\PHeap' = \PHeap'' \Add \HeapS' \Add \HeapF$;

* $\Stack',\HeapS' \models \bigstar_{\Lock \in \Locked{\CC}\setminus\Locked{\CC'}} \LockEnv(\Lock)$;

* $\Succ(\CC,\Stack,\PHeap\Add\HeapS\Add\HeapF,\CC',\Stack',\PHeap')$ holds; and

* $\Safe{\Succ}{n}{\CC'}{\Stack'}{\PHeap''}{\LockEnv}{\PQ}$ holds.

Intuitively, $\Safe{\Succ}{n}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ means that every configuration $\Configuration$ with command $\CC$,
local state $\PHeap$ and
shared state $\HeapS$ given by $\LockEnv$, and, optionally,
additional global state $\HeapF$,
is safe w.r.t. lock environment $\LockEnv$ and postcondition $\PQ$ for $n \geq 0$ steps; that is,
every configuration $\Configuration'$ reached from $\Configuration$ via one transition
(1) has no data race,
(2) does not abort execution,
(3) satisfies postcondition $\PQ$ if execution terminated,
(4 a,b) respects the lock invariants in $\LockEnv$,
(4 c) if we reached $\Configuration'$ via a transition $\Configuration'' \OpRel \Configuration'$,
then $\Succ(\Configuration'', \Configuration')$ holds, and
(4 d) is itself safe for $n-1$ steps.

We write $\semtriple{}{\LockEnv}{\PP}{\CC}{\PQ}$ (read: the triple $\{\PP\}\,\CC\,\{\PQ\}$ is valid given lock environment $\LockEnv$)
if and only if

\[
\forall n, \Stack, \PHeap\colon \quad
\Stack,\PHeap \models \PP \qimplies
\Safe{\True}{n}{\CC}{\Stack}{\Heap}{\LockEnv}{\PQ}~.
\]

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:proof-rules yields a valid triple; the original soundness proof
for CSL is due to Brookes [4].

If $\striple{\PP}{\CC}{\PQ}$, then $\semtriple{}{\LockEnv}{\PP}{\CC}{\PQ}$.

Compared to CSL, our refinement logic introduces one rule
for each of the new commands $\InitializeBlock{\CC}$, $\NextBlock{\CC}$, and $\Print{\EE}$ (see fig:proof-rules-novel).
If we only consider configuration safety as in CSL,
then, as discussed in sec:methodology:logic,
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 $\vdash_{\refineIndicator}$ indicates refinement judgments):

If $\srtriple{\PP}{\CC}{\PQ}$, then $\semtriple{}{\LockEnv}{\PP}{\CC}{\PQ}$.

app:refine-found provides further details.
To formalize that the implementation refines the abstract model , we extend the above definition of configuration safety such that, if the system is initialized, every concrete transition $\Configuration \OpRel \Configuration'$ taken is simulated by a transition of $\AbsTS$ (or stutters).
Moreover, if the system becomes initialized after a step, we require that the encoded state of $\AbsTS$ is a valid initial state.

Our formalization uses the state extraction function $\AbsLocsOfName$ from def:methodology:get-state to refer to the abstract model's state encoded in the heap.
We then consider the configuration safety predicate
where the predicate $\RSucc((\CC,\Stack,\PHeap),(\CC',\Stack',\PHeap'))$ holds iff

* if $\isInit{\CC}$ holds, then
$\valid \AbsNext(\AbsLocsOf{\PHeap},\AbsLocsOf{\PHeap'})$;

* if $\isInit{\CC}$ does not hold and $\isInit{\CC'}$ holds, then $\valid \AbsInit(\AbsLocsOf{\PHeap'})$.

We write $\rsemtriple{\LockEnv}{\PP}{\CC}{\PQ}$ (read: the triple $\{\PP\}\,\CC\,\{\PQ\}$ is valid for refinement of  given $\LockEnv$)
if and only if

\[
\forall n, \Stack, \PHeap\colon \quad
\Stack,\PHeap \models \PP \qimplies
\Safe{\RSucc}{n}{\CC}{\Stack}{\Heap}{\LockEnv}{\PQ}~.
\]

As for CSL, our refinement logic is sound in the sense
that formally derived judgments yield valid triples:

If $\srtriple{\PP}{\CC}{\PQ}$, then $\rsemtriple{\LockEnv}{\PP}{\CC}{\PQ}$.

The proof is by structural induction over the rules of our refinement logic
(found in fig:proof-rules and fig:proof-rules-novel).
In each case, we show that the predicate
$\Safe{\RSucc}{n+1}{\CC}{\Stack}{\Heap}{\LockEnv}{\PQ}$ holds;
we first invoke lem:safety such that only two proof obligations remain
for every possible step

\begin{align*}
\Configuration = (\Conf{\CC}{\Stack}{\PHeap \Add \HeapS \Add \HeapF}) \OpRel (\Conf{\CC'}{\Stack'}{\PHeap'' \Add \HeapS' \Add \HeapF}) = \Configuration'
\tag{$\dag$}
\end{align*}

considered in def:conf-safe.(4):
(a) $\RSucc(\Configuration,\Configuration')$
(b) $\Safe{\RSucc}{n}{\CC'}{\Stack'}{\Heap''}{\LockEnv}{\PQ}$.

There are three main cases:

First, for axioms and Next,
we have $\CC' = \Skip$; then (a) is immediate, since
$\neg\isInit{\CC}$ and $\neg\isInit{\CC'}$ hold; (b) follows from
lem:soundness-skip below.

Second, for the Init rule, (a) is immediate by the rule's premise;
(b) follows from lem:soundness-ghost-lock below.

Third, and finally, for all other rules, (a) and (b) follow directly from the induction
Further details are found in app:refine-sound.

For all $n,\Stack,\Heap,\LockEnv,\PQ$, if $\Stack,\Heap \models \PQ$, then

If $\CC$ contains no two different sub-commands $\CC_1$ and $\CC_2$ such that
$\Locked{\CC_1} \cap \Locked{\CC_2} \neq \emptyset$
and $\FV{\GhostInv} \cap \Mod{\Command} = \emptyset$, then

\[
\rtriple{}{\LockEnvG}{\PP}{\Command}{\PQ}
\qimplies
\rsemtriple{\LockEnv}{\PP \sep \GhostInv}{\DeclareLock{\GhostLock}\Block{\Command}}{\PQ \sep \GhostInv}.
\]

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 $\PP$ and the shared state described by the lock invariants in

For a command $\CC$, an assertion $\PP$, and a lock environment $\LockEnv$,
the set $\SoundInitials$ of initial configurations is

\begin{align*}
\SoundInitials \ddefeq \{ (\Conf{\CC}{\Stack}{\PHeap \Add \HeapS \Add \HeapF}) ~|~
& \isDefined{\PHeap \Add \HeapS \Add \HeapF} \tand \Stack,\PHeap \models \PP \\
& \tand \Stack, \HeapS \models \bigstar_{\Lock \in \Locks \setminus \Locked{\CC}} \LockEnv(\Lock)  \}~.
\end{align*}

To guarantee trace inclusion, we exclude commands that suddenly become “uninitialized” because the $\InitializeBlock{\CC}$ block expires but execution continues, , $\InitializeBlock{\CC'}\Seq\Assign{\AbsLoc{2}}{17}\Seq\Initialize\Block{\CC''}$. Such ill-formed commands can easily be detected by a syntactic check.
More precisely, we call a command $\CC$ continuously initialized if
there exist commands $\CC_1,\CC_2$ such that $\CC_1$ contains no sub-command of the form
$\InitializeBlock{\ldots}$ and $\CC = (\CC_1 \Seq \InitializeBlock{\CC_2})$.

For every continuously-initialized command $\CC$,

\[ \srtriple{\PP}{\CC}{\PQ} \qimplies \Traces{\SoundInitials} \subseteq \AbsTraces~. \]

A detailed proof is found in app:trace-inclusion.

§ 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:introduction and are summarized in tab:evaluation. We briefly describe each of the examples in the following.

demonstrates how multiple threads can collaborate to achieve the overall behavior of an abstract system. This example is described in sec:overview.

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.

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.

demonstrates the use of I/O methods to model both standard input and standard output.

implements leader election in a ring, with a specification adapted from the examples repository, based on Chang and Roberts [6].

and  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  example further demonstrates dynamic threading to process the input tree in parallel, and a two-state monotonicity invariant.

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.

[1]
Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge
University Press (2010)

[2]
Appel, A.W., Beringer, L., Chlipala, A., Pierce, B.C., Shao, Z., Weirich, S.,
Zdancewic, S.: Position paper: the science of deep specification.
Philosophical Transactions of the Royal Society A  375 (Oct 2017)

[3]
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R.
(ed.) Static Analysis (SAS). pp. 55–72 (2003)

[4]
Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci.
375(1-3),  227–270 (2007)

[5]
Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: A
separation logic tool to verify correctness of C programs. J. Autom.
Reasoning  61(1-4),  367–422 (2018)

[6]
Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding
in circular configurations of processes. Communications of the ACM
22(5),  281–283 (1979)

[7]
Cohen, E., Schirmer, B.: From total store order to sequential consistency: A
practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.)
Interactive Theorem Proving. pp. 403–418. Springer Berlin Heidelberg,
Berlin, Heidelberg (2010)

[8]
Coq Development Team, T.: The Coq Reference Manual, version 8.10
(2019), available electronically at <http://coq.inria.fr/documentation>

[9]
Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.:
Concurrent abstract predicates. In: D'Hondt, T. (ed.) European Conference on
Object-Oriented Programming (ECOOP). Lecture Notes in Computer Science,
vol. 6183, pp. 504–528. Springer (2010)

[10]
Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts,
M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed
systems correct. In: Miller, E.L., Hand, S. (eds.) Symposium on Operating
Systems Principles (SOSP). pp. 1–17. ACM (2015)

[11]
Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular
refinement reasoning for concurrent programs. In: International Conference on
Computer Aided Verification. pp. 449–465. Springer (2015)

[12]
Jones, C.B.: Developing methods for computer programs including a notion of
interference. Ph.D. thesis, University of Oxford, UK (1981),

[13]
Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.:
Iris from the ground up: A modular foundation for higher-order concurrent
separation logic. Journal of Functional Programming  (2018)

[14]
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P.,
Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch,
H., Winwood, S.: sel4: formal verification of an OS kernel. In: Matthews,
J.N., Anderson, T.E. (eds.) Symposium on Operating Systems Principles (SOSP).
pp. 207–220. ACM (2009)

[15]
Koh, N., Li, Y., Li, Y., Xia, L., Beringer, L., Honoré, W., Mansky, W.,
Pierce, B.C., Zdancewic, S.: From C to interaction trees: specifying,
verifying, and testing a networked server. In: Mahboubi, A., Myreen, M.O.
(eds.) Certified Programs and Proofs (CPP). pp. 234–248. ACM (2019)

[16]
Kragl, B., Qadeer, S., Henzinger, T.A.: Refinement for structured concurrent
programs. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification
(CAV). Lecture Notes in Computer Science, vol. 12224, pp. 275–298. Springer

[17]
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and
Software Engineers. Addison-Wesley (2002)

[18]
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness.
In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial
Intelligence, and Reasoning (LPAR). Lecture Notes in Computer Science,
vol. 6355, pp. 348–370. Springer (2010)

[19]
Leroy, X.: Formal certification of a compiler back-end or: programming a
compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.)
Principles of Programming Languages (POPL). pp. 42–54. ACM (2006)

[20]
Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent
distributed key-value stores. In: Bodík, R., Majumdar, R. (eds.)
Principles of Programming Languages (POPL). pp. 357–370. ACM (2016)

[21]
Liu, S., Sandur, A., Meseguer, J., Ölveczky, P.C., Wang, Q.: Generating
correct-by-construction distributed implementations from formal maude
designs. In: Lee, R., Jha, S., Mavridou, A. (eds.) NASA Formal Methods.
Lecture Notes in Computer Science, vol. 12229, pp. 22–40. Springer (2020)

[22]
Lorch, J.R., Chen, Y., Kapritsos, M., Parno, B., Qadeer, S., Sharma, U.,
Wilcox, J.R., Zhao, X.: Armada: low-effort verification of high-performance
concurrent programs. In: Donaldson, A.F., Torlak, E. (eds.) Programming
Language Design and Implementation (PLDI). pp. 197–210. ACM (2020)

[23]
Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification
infrastructure for permission-based reasoning. In: Jobstmann, B., Leino,
K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation
(VMCAI). LNCS, vol. 9583, pp. 41–62. Springer (2016)

[24]
O'Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P.,
Yoshida, N. (eds.) Concurrency Theory (CONCUR). Lecture Notes in Computer
Science, vol. 3170, pp. 49–67. Springer (2004)

[25]
Oortwijn, W., Huisman, M.: Practical abstractions for automated verification of
message passing concurrency. In: Ahrendt, W., Tarifa, S.L.T. (eds.)
Integrated Formal Methods (iFM). Lecture Notes in Computer Science, vol.
11918, pp. 399–417. Springer (2019)

[26]
Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An
axiomatic approach. Commun. ACM  19(5),  279–285 (1976).
10.1145/360051.360224, <https://doi.org/10.1145/360051.360224>

[27]
Penninckx, W., Jacobs, B., Piessens, F.: Sound, modular and compositional
verification of the input/output behavior of programs. In: Vitek, J. (ed.)
European Symposium on Programming (ESOP). Lecture Notes in Computer Science,
vol. 9032, pp. 158–182. Springer (2015)

[28]
Rahli, V., Vukotic, I., Völp, M., Veríssimo, P.J.E.: Velisarios:
Byzantine fault-tolerant protocols powered by coq. In: Ahmed, A. (ed.)
European Symposium on Programming (ESOP). Lecture Notes in Computer Science,
vol. 10801, pp. 619–650. Springer (2018)

[29]
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures.
pp. 55–74 (2002)

[30]
da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: A logic for
time and data abstraction. In: European Conference on Object-Oriented
Programming (ECOOP). Lecture Notes in Computer Science, vol. 8586, pp.
207–231. Springer (2014)

[31]
Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained
concurrent programs. In: Grove, D., Blackburn, S.M. (eds.) Programming
Language Design and Implementation (PLDI). pp. 77–87. ACM (2015)

[32]
Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed
protocols. PACMPL  2(POPL),  28:1–28:30 (2018)

[33]
Sprenger, C., Klenze, T., Eilers, M., Wolf, F.A., Müller, P., Clochard, M.,
Basin, D.: Igloo: Soundly linking compositional refinement and separation
logic for distributed system verification. In: Object-Oriented Programming
Systems, Languages, and Applications (OOPSLA). vol. 4. ACM (2020)

[34]
Timany, A., Gregersen, S.O., Stefanesco, L., Gondelman, L., Nieto, A.,
Birkedal, L.: Trillium: Unifying refinement and higher-order distributed
separation logic. CoRR  abs/2109.07863 (2021)

[35]
Vafeiadis, V.: Concurrent separation logic and operational semantics. In:
MFPS. Electronic Notes in Theoretical Computer Science, vol. 276, pp.
335–351. Elsevier (2011)

[36]
Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.:
Planning for change in a formal verification of the Raft consensus
protocol. In: Avigad, J., Chlipala, A. (eds.) Certified Programs and Proofs
(CPP). pp. 154–165 (2016)

[37]
Xia, L., Zakowski, Y., He, P., Hur, C., Malecha, G., Pierce, B.C., Zdancewic,
S.: Interaction trees: representing recursive and impure programs in coq.
Proc. ACM Program. Lang.  4(POPL),  51:1–51:32 (2020)

§ QUICK REFERENCE

As a quick reference, tab:notation summarizes the notational conventions that have
been introduced in sec:preliminaries (above the line) and sec:methodology (below the line).

§ LEMMAS FROM CSL

We will use the following lemmas taken from [35]:

For all $n,\Stack,\Heap,\LockEnv,\PQ$, if $\Stack,\Heap \models \PQ$, then

If $\forall n\colon \Safe{\True}{n}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PQ}$
and $\isDefined{\PHeap \Add \HeapF}$ and

\[
\Conf{\CC}{\Stack}{\PHeap \Add \HeapF} \OpRelTrans \Conf{\Skip}{\Stack'}{\Heap'},
\]

then there exists $\PHeap''$ such that $\Heap' = \PHeap'' \Add \HeapF$ and
$\Stack', \PHeap'' \models \PQ$.

§ PROOF OF LEM:SAFETY

§.§.§ Claim.

If $\srtriple{\PP}{\CC}{\PQ}$, then $\semtriple{}{\LockEnv}{\PP}{\CC}{\PQ}$.

By def:valid:csl, it suffices to show that

\begin{align}
& \srtriple{\PP}{\CC}{\PQ} \qimplies \\
& \qquad \forall n, \Stack, \PHeap\colon
\qquad  \Stack,\PHeap \models \PP \qimplies
\Safe{\True}{n}{\CC}{\Stack}{\Heap}{\LockEnv}{\PQ}~. \notag
\end{align}

Since $\Safe{\True}{0}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ holds always by def:conf-safe, it suffices to prove that
$\Safe{\True}{n+1}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ holds
for an arbitrary, but fixed $n \in \Nats$.

By structural induction over the rules for of our refinement logic for deriving judgments $\srtriple{\PP}{\CC}{\PQ}$
(found in fig:proof-rules and fig:proof-rules-novel).

We present the case $\Rule{Print}$ in detail further below.
As discussed in sec:methodology:logic,
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:csl-sound.

The case Print.
Recall the rule

\[
\inference[\Rule{Print}]{
\rtriple{}{\LockEnv,\LockDef{\InitLock}{\emp}}{
\pt{\OutVar}{\PermWrite}{\EE'}
\Print{\EE}
\pt{\OutVar}{\PermWrite}{(\Append{\EE}{\EE'})}
\]

and assume

\begin{align}
\Stack,\PHeap \models \pt{\OutVar}{\PermWrite}{\EE'}.
\end{align}

\begin{align}
\PHeap \eeq \Set{ \stdout \xmapsto{\PermWrite} \EE'(\Stack) }.
\label{eq:cs:3}
\end{align}

We discharge all items in def:conf-safe to show that

\begin{align}
\Safe{\True}{n+1}{\Print{\EE}}{\Stack}{\PHeap}{\LockEnv,\LockDef{\InitLock}{\emp}}{\pt{\OutVar}{\PermWrite}{(\Append{\EE}{\EE'})}}.
\end{align}

For 1, consider the following:

\begin{align}
& \Reads{\Print{\EE}}{\Stack} = \Set{\stdout} \\
\eeq & \dom{\Heap} \tag{by \eqref{cs:3}}
\end{align}

2 is immediate by (<ref>) and the rules of our operational semantics.
3 is trivial.
For 4, assume $\CC'$, $\Stack'$, $\HeapF$, $\HeapS$, $\PHeap'$ such that

\begin{align}
& \Stack,\HeapS \models \bigstar_{\Lock \in \Locked{\CC'}\setminus\Locked{\CC}} \LockEnv(\Lock)
\\
\tand \notag \\
(\Conf{\Print{\EE}}{\Stack}{\PHeap \Add \HeapS \Add \HeapF}) \OpRel (\Conf{\CC'}{\Stack'}{\PHeap'})
\end{align}

By our operational semantics and (<ref>), there is only one transition as above.
For this transition, we have

\begin{align}
& \CC' = \Skip, \qand
\HeapS = \emp, \qand \\
& \Heap' = \Set{ \stdout \xmapsto{\PermWrite} \Append{\EE(\Stack)}{\EE'(\Stack)} } \Add \HeapF
\end{align}

Hence, for $\PHeap'' = \Heap'$ and $\HeapS' = \emp$,
(a)-(c) hold immediately.
(d) holds by lem:aux:skip.

§ MISSING LEMMAS FOR THE PROOF OF THM:REFINE-SOUND

§.§ Proof of lem:soundness-skip

§.§.§ Claim.

For all $n,\Stack,\Heap,\LockEnv,\PQ$, if $\Stack,\Heap \models \PQ$, then

By definition, $\Safe{\RSucc}{0}{\Skip}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ holds always.

\begin{align}
\Stack,\Heap \models \PQ.
\end{align}

By lem:aux:skip, we know that

\begin{align}
\Safe{\True}{n+1}{\Skip}{\Stack}{\PHeap}{\LockEnv}{\PQ}.
\label{eq:sk}
\end{align}

Then $\Safe{\RSucc}{n+1}{\Skip}{\Stack}{\PHeap}{\LockEnv}{\PQ}$ holds as well, because
(1-3) holds by (<ref>).
Furthermore, since our operational semantics does not admit any transition starting with
command , 4 holds vacuously.

§.§ Proof of lem:soundness-ghost-lock

§.§.§ Claim.

If $\CC$ contains no two different sub-commands $\CC_1$ and $\CC_2$ such that
$\Locked{\CC_1} \cap \Locked{\CC_2} \neq \emptyset$
and $\FV{\GhostInv} \cap \Mod{\Command} = \emptyset$,

\[
\rtriple{}{\LockEnvG}{\PP}{\Command}{\PQ}
\qimplies
\rsemtriple{\LockEnv}{\PP \sep \GhostInv}{\DeclareLock{\GhostLock}\Block{\Command}}{\PQ \sep \GhostInv}.
\]

By structural induction on the rules of our refinement logic we show that
and $\Stack,\PHeap \sep \GhostInv \models \PP$ implies

\begin{align}
\forall n\in\Nats\colon \quad
\Safe{\RSucc}{n}{\DeclareLockBlock{\GhostInv}{\CC}}{\Stack}{\Heap}{\LockEnv}{\PQ \sep \GhostInv}~.
\end{align}

We present the case for the Next in detail as it is the only rule, where the
predicate $\RSucc$ 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:proof-rules-novel the rule

\begin{align*}
\inference[\Rule{Next}]{
\isAtomic{\CC} \\
%\Perm > 0 &
%\vec{o} = (o_1,\ldots,o_\AbsLength),~\text{fresh}
\srtriple{
(\Aabsvars{\vec{o}} \wedge \GhostInv) \sep \PP
\Command
\underbrace{\exists \vec{y} \mydot \Aabsvars{\vec{y}} \wedge \AbsNext(\vec{o},\vec{y}) \wedge
\GhostInv) \sep \PQ)}_{\PR}
\rtriple{}{\LockEnv,\LockDef{\GhostLock}{\GhostInv}}{
\PP
\NextBlock{\Command}
\PQ
\end{align*}

and assume that

\begin{align} %\label{def:valid:refinement}n}
\Stack, \PHeap \models \PP \sep \GhostInv.
\label{eq:next1}
\end{align}

We then need to show that, for all $n \in \Nats$,

\begin{align} %\label{def:valid:refinement}n}
\Safe{\RSucc}{n}{\DeclareLockBlock{\GhostLock}{\NextBlock{\CC}}}{\Stack}{\Heap}{\LockEnv}{\PQ \sep \GhostInv}.
\end{align}

The case $n = 0$ always holds by def:conf-safe.
For $n > 0$, we discharge (1)-(4):

* (1) is immediate, since
$\Reads{\DeclareLockBlock{\GhostLock}{\NextBlock{\CC}}}{\Stack} = \emptyset$;

* (2) is immediate, by lem:safety and the rules of our operational

* (3) is trivial; and

* for (4) assume
$\CC'$, $\Stack'$, $\HeapF$, $\HeapS$, $\PHeap'$ such that

\begin{align}
&      \Stack,\HeapS \models \bigstar_{\Lock \in \Locked{\CC'}\setminus\Locked{\CC}} \LockEnv(\Lock) \\
& \tand \notag\\
& (\Conf{\CC}{\Stack}{\PHeap \Add \HeapS \Add \HeapF}) \OpRel (\Conf{\CC'}{\Stack'}{\PHeap'}).
\end{align}

Our operational semantics has exactly one rule that admits such a transition, namely
the one with premise
$\Conf{\Command}{\Stack}{\Heap \Add \HeapS \Add \HeapF} \OpRelTrans \Conf{\Skip}{\Stack'}{\Heap'}$.
Now, by the Next rule's premise and lem:safety, we have

\begin{align}
\forall m\colon \Safe{\True}{m}{\CC}{\Stack}{\PHeap}{\LockEnv}{\PR}.
\end{align}

Hence, by lem:aux:atom, there exist $\PHeap''$
such that

\begin{align}
\Heap' \eeq \PHeap'' \Add (\HeapS \Add \HeapF) \tand \\
\Stack', \PHeap'' \models \PR.
\end{align}

Then (4a) holds for $\PHeap''$ as above and $\HeapS' = \EmptyHeap$;
(4b) holds, since $\Locked{\DeclareLockBlock{\GhostLock}{\NextBlock{\CC}}\DeclareLockBlock{\GhostLock}{\NextBlock{\CC}}} = \Locked{\DeclareLockBlock{\GhostLock}{\Skip}}$;
(4c) follows from
(<ref>) and $\Stack', (\Heap'' \Add (\HeapS \Add \HeapF)) \models \PR$, where $\PR$ is the Next rule's postcondition; and
(dc) holds by lem:soundness-skip.

§ PROOF OF THM:TRACE-INCLUSION

§.§.§ Claim.

For every continuously initialized command $\CC$,

\[ \srtriple{\PP}{\CC}{\PQ} \qimplies \Traces{\SoundInitials} \subseteq \AbsTraces~. \]

By thm:refine-sound, we have

\begin{align}
\rsemtriple{\LockEnv}{\PP}{\CC}{\PQ}
\label{eq:ti1}
\end{align}

Moreover, since $\isInit{\CC}$ holds iff $\GhostLock \in \Locks{\CC}$ and there is no proof rule for (sub-)commands of the form
$\DeclareLock{\GhostLock}{\ldots}$, we have

\begin{align}
\neg\isInit{\CC}
\label{eq:ti2}
\end{align}

Now, assume that

\begin{align}
\Configuration_1 = (\Conf{\CC_1}{\Stack_1}{\Heap_1}) \in \SoundInitialsFor{\CC_1}
\label{eq:ti3}
\end{align}

and, for some arbitrary, but fixed, $n \in \Nats$,

\begin{align}
\Configuration_1 \OpRel \Configuration_2
\OpRel \ldots \OpRel \Configuration_n~.
\label{eq:ti4}
\end{align}

By (<ref>), (<ref>), def:sound-initials, and def:valid:refinement we have

\begin{align}
\Safe{\RSucc}{n+2}{\CC}{\Stack}{\Heap}{\LockEnv}{\PQ}~.
\end{align}

By def:conf-safe.(2) and (<ref>), we can safely assume that

\begin{align}
\forall i \in \Set{1,\ldots,n}\colon \quad
\Configuration_i = (\Conf{\CC_i}{\Stack_i}{\Heap_i})~.
\end{align}

We distinguish two cases:
First, assume there exists an $m' \in \Set{1,\ldots,n}$ such that $\isInit{\Command_{m'}}$;
let $m$ be the minimal such index $m'$.
By (<ref>), we know that $m \geq 2$.
Hence, by thm:incl-m below,

\begin{align}
\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_n} \in \AbsPaths
\label{eq:incl}
\end{align}

Now, if $\Command_n = \Skip$, then we have:

\begin{align*}
& \Traces{\SoundInitialsFor{\CC_1}}  \\
~\ni~ & \Obs{\Configuration_1} \ldots \Obs{\Configuration_n} \\
\eeq & \underbrace{\Obs{\Configuration_1} \ldots \Obs{\Configuration_{m-1}}}_{\eeq \Emptyseq} \Obs{\Configuration_{m}} \ldots \Obs{\Configuration_{n-1}}
\underbrace{\Obs{\Configuration_n}}_{\eeq \Emptyseq}
\tag{Def. of $\Obs{.}$, $\neg\isInit{\Skip}$} \\
\eeq & \Obs{\Configuration_{m}} \ldots \Obs{\Configuration_{n-1}}
\tag{Def. of $\Obs{.}$; $m$ is minimal by assumption} \\
\eeq &
\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_{n-1}} \tag{Def. of $\Obs{.}$} \\
~\in~ & \AbsPaths. \tag{by (\ref{eq:incl})}
\end{align*}

Conversely, if $\Command_n \neq \Skip$, then we have:

\begin{align*}
& \Traces{\SoundInitialsFor{\CC_1}}  \\
~\ni~ & \Obs{\Configuration_1} \ldots \Obs{\Configuration_n} \\
\eeq & \underbrace{\Obs{\Configuration_1} \ldots \Obs{\Configuration_{m-1}}}_{\eeq \Emptyseq} \Obs{\Configuration_{m}} \ldots \Obs{\Configuration_{n-1}} \Obs{\Configuration_n} \\
\eeq & \Obs{\Configuration_{m}} \ldots \Obs{\Configuration_{n-1}} \Obs{\Configuration_n}
\tag{Def. of $\Obs{.}$; $m$ is minimal by assumption} \\
\eeq &
\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_n} \tag{Def. of $\Obs{.}$} \\
~\in~ & \AbsPaths. \tag{by (\ref{eq:incl})}
\end{align*}

Second, assume there for all $m' \in \Set{1,\ldots,n}$, we have $\neg\isInit{\Command_{m'}}$.
Then, by Def. of $\Obs{.}$, we have

\begin{align}
\Traces{\SoundInitialsFor{\CC_1}}
~\ni~ \Obs{\Configuration_1} \ldots \Obs{\Configuration_n}
\eeq \Emptyseq
~\in~ \AbsPaths.
\end{align}

For all $2 \leq m \leq n$ and all
$(\Conf{\CC_1}{\Stack_1}{\Heap_1}), \ldots, (\Conf{\CC_n}{\Stack_n}{\Heap_n})$, if

*  $\CC_1$ is continuously initialized and

*  $\rsemtriple{}{\PP}{\CC_1}{\PQ}$ and

*  $(\Conf{\CC_1}{\Stack_1}{\Heap_1}) \in \SoundInitials$ and

*  $\Conf{\CC_1}{\Stack_1}{\Heap_1} \OpRel \ldots
\OpRel \Conf{\CC_n}{\Stack_n}{\Heap_n}$ and

*  $\isInit{\CC_m}$ and, for all $j < m$, not $\isInit{\CC_j}$,

then $\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_n} \in \AbsPaths$.

By induction on $n$.

Induction base. Assume im1-im5 hold for $n = m = 2$.
By im3, there exist heaps $\PHeap$, $\HeapS$ such that

\begin{align}
& \Heap_1 \eeq \PHeap \Add \HeapS \\
& \Stack_1, \PHeap \eeq \PP \\
& \Stack_1, \HeapS \models
\bigstar_{\Lock \in \Locks \setminus \Locked{\CC_1}} \LockEnv(\Lock) \\
\end{align}

Hence, by im2,

\begin{align}
\Safe{\RSucc}{3}{\CC_1}{\Stack_1}{\PHeap}{\LockEnv}{\PQ}~.
\end{align}

Now, consider the transition

\begin{align}
\Conf{\CC_1}{\Stack_1}{\PHeap \Add \HeapS \Add \EmptyHeap} \OpRel \ldots \OpRel \Conf{\CC_2}{\Stack_2}{\Heap_2}
\end{align}

which exists by im4. By im5, we have
$\isInit{\CC_1}$ does not hold and $\isInit{\CC_2}$ holds.
Hence, by (4c) and definition of $\RSucc$,

\begin{align}
\valid \AbsInit(\AbsLocsOf{\Heap_2})
\end{align}

and thus also $\AbsLocsOf{\Heap_2} \in \AbsPaths$.

Induction hypothesis.
For an arbitrary, but fixed, $n \geq 2$, assume that im1-im5 imply
$\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_n} \in \AbsPaths$.

Induction step.
Assume that im1-im5 hold for some $2 \leq m \leq n+1$, where $n \geq 2$.
The case $m = n + 1$ is analogous to the induction base.
Hence, assume $m < n +1$.
By im3, there exist heaps $\PHeap$, $\HeapS$ such that

\begin{align}
& \Heap_1 \eeq \PHeap \Add \HeapS \\
& \Stack_1, \PHeap \eeq \PP \\
& \Stack_1, \HeapS \models
\bigstar_{\Lock \in \Locks \setminus \Locked{\CC_1}} \LockEnv(\Lock) \\
\end{align}

Hence, by im2,

\begin{align}
\Safe{\RSucc}{n+3}{\CC_1}{\Stack_1}{\PHeap}{\LockEnv}{\PQ}~.
\end{align}

By repeated unfolding the above predicate,
we know that there exist $\PHeap'$ and $\HeapS'$ such that

\begin{align}
& \Heap_n \eeq \PHeap' \Add \HeapS' \\
& \Safe{\RSucc}{2}{\CC_n}{\Stack_n}{\PHeap'}{\LockEnv}{\PQ} \\
& \Stack_1, \HeapS \models
\bigstar_{\Lock \in \Locks \setminus \Locked{\CC_n}} \LockEnv(\Lock) \\
\end{align}

Now, consider the transition below, which exists by im4.

\begin{align}
\Conf{\CC_n}{\Stack_n}{\PHeap' \Add \HeapS' \Add \EmptyHeap} \OpRel \ldots \OpRel \Conf{\CC_{n+1}}{\Stack_{n+1}}{\Heap_{n+1}}
\end{align}

Since $m < n + 1$, im1 and im5 yield that $\isInit{\CC_n}$ holds.
By  (4c) and definition of $\RSucc$, this means

\begin{align}
\valid \AbsNext(\AbsLocsOf{\PHeap_n},\AbsLocsOf{\PHeap_{n+1}})
\end{align}

By I.H., we also know that

\begin{align}
\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_n} \in \AbsPaths
\end{align}

\begin{align}
\AbsLocsOf{\Heap_m} \ldots \AbsLocsOf{\Heap_n}\AbsLocsOf{\Heap_{n+1}} \in \AbsPaths,
\end{align}

which finishes the proof.