Advertisement

Automating Deductive Verification for Weak-Memory Programs

  • Alexander J. Summers
  • Peter Müller
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10805)

Abstract

Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to features such as higher-order assertions, modalities and rich permission resources.

In this paper, we provide the first encoding of a weak memory program logic using existing deductive verification tools. Our work enables, for the first time, the (unbounded) verification of C11 programs at the level of abstraction provided by the program logics; the only necessary user interaction is in the form of specifications written in the program logic.

We tackle three recent program logics: Relaxed Separation Logic and two forms of Fenced Separation Logic, and show how these can be encoded using the Viper verification infrastructure. In doing so, we illustrate several novel encoding techniques which could be employed for other logics. Our work is implemented, and has been evaluated on examples from existing papers as well as the Facebook open-source Folly library.

1 Introduction

Reasoning about programs running on weak memory is challenging because weak memory models admit executions that are not sequentially consistent, that is, cannot be explained by a sequential interleaving of concurrent threads. Moreover, weak-memory programs employ a range of operations to access memory, which require dedicated reasoning techniques. These operations include fences as well as read and write accesses with varying degrees of synchronisation.

Some of these challenges are addressed by the first program logics for weak-memory programs, in particular, Relaxed Separation Logic (RSL) [38], GPS [36], Fenced Separation Logic (FSL) [17], and FSL\({+}{+}\) [18]. These logics apply to interesting classes of C11 programs, but their tool support has been limited to embeddings in Coq. Verification based on these embeddings requires substantial user interaction, which is an obstacle to applying and evaluating these logics.
Fig. 1.

Syntax for memory accesses. na indicates a non-atomic operation; \(\tau \) indicates an atomic access mode (as defined in C11), discussed in later sections. \(\rho \), and assertions A and invariants \(\mathcal {Q}\) are program annotations, needed as input for our encoding. Expressions e include boolean and arithmetic operations, but no heap accesses. We assume that source programs are type-checked.

In this paper, we present a novel approach to automating deductive verification for weak memory programs. We encode large fractions of RSL, FSL, and FSL\({+}{+}\) (collectively referred to as the RSL logics) into the intermediate verification language Viper [27], and use the existing Viper verification backends to reason automatically about the encoded programs. This encoding reduces all concurrency and weak-memory features as well as logical features such as higher-order assertions and custom modalities to a much simpler sequential logic.

Defining an encoding into Viper is much more lightweight than developing a dedicated verifier from scratch, since we can reuse the existing automation for a variety of advanced program reasoning features. Compared to an embedding into an interactive theorem prover such as Coq, our approach leads to a significantly higher degree of automation than that typically achieved through tactics. Moreover, it allows users to interact with the verifier on the abstraction level of source code and annotations, without exposing the underlying formalism. Verification in Coq can provide foundational guarantees, whereas in our approach, errors in the encoding or bugs in the verifier could potentially invalidate verification results. We mitigate the former risk by a soundness argument for our encoding and the latter by the use of a mature verification system. We are convinced that both approaches are necessary: foundational verification is ideal for meta-theory development and application areas such as safety-critical systems, whereas our approach is well-suited for prototyping and evaluating logics, and for making a verification technique applicable by a wider user base.

The contributions of this paper are: (1) The first automated deductive verification approach for weak-memory logics. We demonstrate the effectiveness of this approach on examples from the literature, which are available online [3]. (2) An encoding of large fractions of RSL, FSL, and FSL\({+}{+}\) into Viper. Various aspects of this encoding (such as the treatment of higher-order features and modalities, as well as the overall proof search strategy) are generic and can be reused to encode other advanced separation logics. (3) A prototype implementation, which is available online [4].

Related Work. The existing weak-memory logics RSL [38], GPS [36], FSL [17], and FSL\({+}{+}\) [18] have been formalized in Coq and used to verify small examples. The proofs were constructed mostly manually, whereas our approach automates most of the proof steps. As shown in our evaluation, our approach reduces the overhead by more than an order of magnitude. The degree of automation in Coq could be increased through logic-specific tactics (e.g. [13, 32]), whereas our approach benefits from Viper’s automation for the intermediate language, which is independent of the encoded logic.

Jacobs [20] proposed a program logic for the TSO memory model that has been encoded in VeriFast [21]. This encoding requires a substantial amount of annotations, whereas our approach provides a higher degree of automation and handles the more complex C11 memory model.

Weak-memory reasoning has been addressed using techniques based on model-checking (e.g. [5, 6, 11]) and static analyses (e.g. [7, 16]). These approaches are fully automatic, but do not analyse code modularly, which is e.g. important for verifying libraries independently from their clients. Deductive verification enables compositional proofs by requiring specifications at function boundaries. Such specifications can express precise information about the (unbounded) behaviour of a program’s constituent parts.

Automating logics via encodings into intermediate verification languages is a proven approach, as witnessed by the many existing verifiers (e.g. [14, 15, 24, 25]) which target Boogie [8] or Why3 [9]. Our work is the first that applies this approach to logics for weak-memory concurrency. Our encoding benefits from Viper’s native support for separation-logic-style reasoning and several advanced features such as quantified permissions and permission introspection [26, 27], which are not available in other intermediate verification languages.

Outline. The next four sections present our encoding for the core features of the C11 memory model: we discuss non-atomic locations in Sect. 2, release-acquire accesses in Sect. 3, fences in Sect. 4, and compare-and-swap in Sect. 5. We discuss soundness and completeness of our encoding in Sect. 6 and evaluate our approach in Sect. 7. Section 8 concludes. Further details of our encoding and examples are available in our accompanying technical report (hereafter, TR) [35]. A prototype implementation of our encoding (with all examples) is available as an artifact [4].
Fig. 2.

Assertion syntax of the RSL logics. The top row of constructs are standard for separation logics; those in the second row are specific to the RSL logics, and explained throughout the paper. Invariants \(\mathcal {Q}\) are functions from values to assertions (cf. Sect. 3).

2 Non-atomic Locations

We present our encoding for a small imperative programming language similar to the languages supported by the RSL logics. C11 supports non-atomic memory accesses and different forms of atomic accesses. The access operations are summarised in Fig. 1. We adopt the common simplifying assumption [36, 38] that memory locations are partitioned into those accessed only via non-atomic accesses (non-atomic locations), and those accessed only via C11 atomics (atomic locations). Read and write statements are parameterised by a mode \(\sigma \), which is either na (non-atomic) or one of the atomic access modes \(\tau \). We focus on non-atomic accesses in this section and discuss atomics in subsequent sections.
Fig. 3.

Adapted RSL rules for non-atomics. Read access requires a non-zero permission. Write access requires either write permission or that the location is uninitialised. The underscore \(\_\) stands for an arbitrary value.

RSL Proof Rules. Non-atomic memory accesses come with no synchronisation guarantees; programmers need to ensure that all accesses to non-atomic locations are data-race free. The RSL logics enforce this requirement using standard separation logic [28, 31]. We show the syntax of assertions in Fig. 2, which will be explained throughout the paper. A points-to assertion Open image in new window denotes a transferable resource, providing permission to access the location l, and expressing that l has been initialised and its current value is e. Here, k is a fraction \(0 < k \le 1\); \(k=1\) denotes the full (or exclusive) permission to read and write location l, whereas \(0< k < 1\) provides (non-exclusive) read access [12]. Points-to resources can be split and recombined, but never duplicated or forged; when transferring such a resource to another thread it is removed from the current one, avoiding data races by construction. The RSL assertion \(\textsf {Uninit}(l)\) expresses exclusive access to a location l that has been allocated, but not yet initialised; l may be written to but not read from. The main proof rules for non-atomic locations, adapted from RSL [38], are shown in Fig. 3.

Encoding. The Viper intermediate verification language [27] supports an assertion language based on Implicit Dynamic Frames [33], a program logic related to separation logic [29], but which separates permissions from value information. Viper is object-based; the only memory locations are field locations e.f (in which e is a reference, and f a field name). Permissions to access these heap locations are described by accessibility predicates of the form Open image in new window , where k is a fraction as for points-to predicates above (k defaults to 1). Assertions that do not contain accessibility predicates are called pure. Unlike in separation logics, heap locations may be read in pure assertions.

We model C-like memory locations l using a field Open image in new window of a Viper reference l. Consequently, a separation logic assertion Open image in new window is represented in Viper as Open image in new window We assume that memory locations have type Open image in new window , but a generalisation is trivial. Viper’s conjunction Open image in new window treats permissions like a separating conjunction, requiring the sum of the permissions in each conjunct, and acts as logical conjunction for pure assertions (just as \(*\) in separation logic).

Viper provides two key statements for encoding proof rules: Open image in new window A adds the permissions denoted by the assertion A to the current state, and assumes pure assertions in A. This can be used to model gaining new resources, e.g., acquiring a lock in the source program. Dually, Open image in new window A checks that the current state satisfies A (otherwise a verification error occurs), and removes the permissions that A denotes; the values of any locations to which no permission remains are havoced (assigned arbitrary values). For example, when forking a new thread, its precondition is exhaled to transfer the necessary resources from the forking thread. Inhale and exhale statements can be seen as the permission-aware analogues of the assume and assert statements of first-order verification languages [25].
Fig. 4.

Viper encoding of the RSL assertions and the rules for non-atomic memory accesses from Fig. 3.

The encoding of the rules for non-atomics from Fig. 3 is presented in Fig. 4. Open image in new window denotes the encoding of an RSL assertion A as a Viper assertion, and analogously Open image in new window for source-level statements s.

The first two lines show background declarations. The assertion encodings follow the explanations above. Allocation is modelled by obtaining a fresh reference (via Open image in new window ) and inhaling permissions to its Open image in new window and Open image in new window fields; assuming Open image in new window reflects that the location is not yet initialised. Viper implicitly checks the necessary permissions for field accesses (verification fails otherwise). Hence, the translation of a non-atomic read only needs to check that the read location is initialised before obtaining its value. Analogously, the translation of a non-atomic write only stores the value and records that the location is now initialised.

Note that Viper’s implicit permission checks are both necessary and sufficient to encode the RSL rules in Fig. 3. In particular, the assertions Open image in new window and \(\textsf {Uninit}(l)\) both provide the permissions to write to location l. By including Open image in new window in the encoding of both assertions, we avoid the disjunction of the RSL rule.

Like the RSL logics, our approach requires programmers to annotate their code with access modes for locations (as part of the Open image in new window statement), and specifications such as pre and postconditions for methods and threads. Given these inputs, Viper constructs the proof automatically. In particular, it automatically proves entailments, and splits and combines fractional permissions (hence, the equivalence in Fig. 3 need not be encoded). Automation can be increased further by inferring some of the required assertions, but this is orthogonal to the encoding presented in this paper.

3 Release-Acquire Atomics

The simplest form of C11 atomic memory accesses are release write and acquire read operations. They can be used to synchronise the transfer of ownership of (and information about) other, non-atomic locations, using a message passing idiom, illustrated by the example in Fig. 5. This program allocates two non-atomic locations a and b, and an atomic location l (initialised to 0), which is used to synchronise the three threads that are spawned afterwards. The middle thread makes changes to the non-atomics a and b, and then signals completion via a release write of 1 to l; conceptually, it gives up ownership of the non-atomic locations via this signal. The other threads loop attempting to acquire-read a non-zero value from l. Once they do, they each gain ownership of one non-atomic location via the acquire read of 1 and access that location. The release write and acquire reads of value 1 enforce ordering constraints on the non-atomic accesses, preventing the left and right threads from racing with the middle one.
Fig. 5.

An example illustrating “message passing” of non-atomic ownership, using release acquire atomics (inspired by an example from [17]). Annotations are shown in Open image in new window . This example corresponds to Open image in new window in our evaluation (Sect. 7).

RSL Proof Rules. The RSL logics capture message-passing idioms by associating a location invariant \(\mathcal {Q}\) with each atomic location. Such an invariant is a function from values to assertions; we represent such functions as assertions with a distinguished variable symbol \(\mathcal {V}\) as parameter. Location invariants prescribe the intended ownership that a thread obtains when performing an acquire read of value \(\mathcal {V}\) from the location, and that must correspondingly be given up by a thread performing a release write. The main proof rules [38] are shown in Fig. 6.

When allocating an atomic location for release/acquire accesses (first proof rule), a location invariant \(\mathcal {Q}\) must be chosen (as an annotation on the allocation). The assertions \(\textsf {Rel}(l,\mathcal {Q})\) and \(\textsf {Acq}(l,\mathcal {Q})\) record the invariant to be used with subsequent release writes and acquire reads. To perform a release write of value e (second rule), a thread must hold the \(\textsf {Rel}(l,\mathcal {Q})\) assertion and give up the assertion \(\mathcal {Q}[e/\mathcal {V}]\). For example, the line \([l]_{\texttt {rel}}~{:=}~1\) in Fig. 5 causes the middle thread to give up ownership of both non-atomic locations a and b. The assertion \(\textsf {Init}(l)\) represents that atomic location l is initialised; both \(\textsf {Init}(l)\) and \(\textsf {Rel}(l,\mathcal {Q})\) are duplicable assertions; once obtained, they can be passed to multiple threads.

Multiple acquire reads might read the value written by a single release write operation; RSL prevents ownership of the transferred resources from being obtained (unsoundly) by multiple readers in two ways. First, \(\textsf {Acq}(l,\mathcal {Q})\) assertions cannot be duplicated, only split by partitioning the invariant \(\mathcal {Q}\) into disjoint parts. For example, in Fig. 5, \(\textsf {Acq}(l,\mathcal {Q}_1)\) is given to the left thread, and \(\textsf {Acq}(l,\mathcal {Q}_2)\) to the right. Second, the rule for acquire reads adjusts the invariant in the \(\textsf {Acq}\) assertion such that subsequent reads of the same value will not obtain any ownership.
Fig. 6.

Adapted RSL rules for release-acquire atomics.

Encoding. A key challenge for encoding the above proof rules is that \(\textsf {Rel}\) and \(\textsf {Acq}\) are parameterised by the invariant \(\mathcal {Q}\); higher-order assertions are not directly supported in Viper. However, for a given program, only finitely many such parameterisations will be required, which allows us to apply defunctionalisation [30], as follows. Given an annotated program, we assign a unique index to each syntactically-occurring invariant \(\mathcal {Q}\) (in particular, in allocation statements, and as parameters to \(\textsf {Rel}\) and \(\textsf {Acq}\) assertions in specifications). Furthermore, we assign unique indices to all immediate conjuncts of these invariants. We write \(\textit{indices}\) for the set of indices used. For each i in \(\textit{indices}\), we write Open image in new window for the invariant which i indexes. For an invariant \(\mathcal {Q}\), we write \({\langle }{\mathcal {Q}}{\rangle }\) for its index, and Open image in new window for the set of indices assigned to its immediate conjuncts.

Our encoding of the RSL rules from Fig. 6 is summarised in Fig. 7. To encode duplicable assertions such as \(\textsf {Init}(l)\), we make use of Viper’s wildcard permissions [27], which represent unknown positive permission amounts. When exhaled, these amounts are chosen such that the amount exhaled will be strictly smaller than the amount held (verification fails if no permission is held) [19]. So after inhaling an \(\textsf {Init}(l)\) assertion (that is, a Open image in new window permission), it is possible to exhale two Open image in new window permissions, corresponding to two \(\textsf {Init}(l)\) assertions. Note that for atomic locations, we only use the Open image in new window field’s permissions, not its value.

We represent a \(\textsf {Rel}(l,\_)\) assertion for some invariant via a Open image in new window permission to a Open image in new window field; this is represented via the Open image in new window macro1, and is used as the precondition for a release write (we must hold some \(\textsf {Rel}\) assertion, according to Fig. 6). The specific invariant associated with the location l is represented by storing its index as the value of the Open image in new window field; when encoding a release write, we branch on this value to exhale the appropriate assertion.
Fig. 7.

Viper encoding of the RSL rules for release-acquire atomics from Fig. 6. The operations in italics (e.g. foreach) are expanded statically in our encoding into conjunctions or statement sequences. The value of the Open image in new window field will be explained in Sect. 5.

Analogously to \(\textsf {Rel}\), we represent an \(\textsf {Acq}\) assertion for some invariant using a Open image in new window permission (the Open image in new window macro), which is the precondition for executing an acquire read. However, to support splitting, we represent the invariant in a more fine-grained way, by recording individual conjuncts separately. Each conjunct i of the invariant is modelled as an abstract predicate instance Open image in new window , which can be inhaled and exhaled individually. This encoding handles the common case that invariants are split along top-level conjuncts, as in Fig. 5. More complex splits can be supported through additional annotations: see App. C of the TR [35].

A release write is encoded by checking that some \(\textsf {Rel}\) assertion is held, and then exhaling the associated invariant for the value written. Moreover, it records that the location is initialised. The RSL rule for acquire reads adjusts the \(\textsf {Acq}\) invariant by obliterating the assertion for the value read. Instead of directly representing the adjusted invariant (which would complicate our numbering scheme), we track the set of values read as state in our encoding. We complement each Open image in new window predicate instance with an (uninterpreted) Viper function Open image in new window , returning a set of indices2).

An acquire read checks that the location is initialised and that we have some \(\textsf {Acq}\) assertion for the location. It assigns an unknown value to the lhs variable x, which is subsequently constrained by the invariant associated with the \(\textsf {Acq}\) assertion as follows: We check for each index whether we both currently hold an Open image in new window predicate for that index3, and if so, have not previously read the value x from that conjunct of our invariant. If these checks succeed, we inhale the indexed invariant for x, and then include x in the values read.

The encoding presented so far allows us to automatically verify annotated C11 programs using release writes and acquire reads (e.g., the program of Fig. 5) without any custom proof strategies [3]. In particular, we can support the higher-order \(\textsf {Acq}\) and \(\textsf {Rel}\) assertions through defunctionalisation and enable the splitting of invariants through a suitable representation.

4 Relaxed Memory Accesses and Fences

In contrast to release-acquire accesses, C11’s relaxed atomic accesses provide no synchronisation: threads may observe reorderings of relaxed accesses and other memory operations. Correspondingly, RSL’s proof rules for relaxed atomics provide weak guarantees, and do not support ownership transfer. Memory fence instructions can eliminate this problem. Intuitively, a release fence together with a subsequent relaxed write allows a thread to transfer away ownership of resources, similarly to a release write. Dually, an acquire fence together with a prior relaxed read allows a thread to obtain ownership of resources, similarly to an acquire read. This reasoning is justified by the ordering guarantees of the C11 model [17].

FSL Proof Rules. FSL and FSL\({+}{+}\) provide proof rules for fences (see Fig. 8). They use modalities Open image in new window (“up”) and Open image in new window (“down”) to represent resources that are transferred through relaxed accesses and fences. An assertion Open image in new window represents a resource A which has been prepared, via a release fence, to be transferred by a relaxed write operation; dually, Open image in new window represents resources A obtained via a relaxed read, which may not be made use of until an acquire fence is encountered. The proof rule for relaxed write is identical to that for a release write (cf. Fig. 6), except that the assertion to be transferred away must be under the Open image in new window modality; this can be achieved by the rule for release fences. The rule for a relaxed read is the same as that for acquire reads, except that the gained assertion is under the Open image in new window modality. The modality can be removed by a subsequent acquire fence. Finally, assertions may be rewritten under modalities, and both modalities distribute over all other logical connectives.

Figure 9 shows an example program, which is a variant of the message-passing example from Fig. 5. Comparing the left-hand one of the three parallel threads, a relaxed read is used in the spin loop; after the loop, this thread will hold the assertion Open image in new window . The subsequent Open image in new window statement allows the modality to be removed, allowing the non-atomic location a to be accessed. Dually, the middle thread employs a Open image in new window statement to place the ownership of the non-atomic locations under the Open image in new window modality, in preparation for the relaxed write to l.
Fig. 8.

Adapted FSL rules for relaxed atomics and fences.

Fig. 9.

A variant of the message-passing example of Fig. 5, combining relaxed memory accesses and fences to achieve ownership transfer. The example is also a variant of Fig. 2 of the FSL paper [17], which is included in our evaluation ( Open image in new window ) in Sect. 7.

Encoding. The main challenge in encoding the FSL rules for fences is how to represent the two new modalities. Since these modalities guard assertions which cannot be currently used or combined with modality-free assertions, we model them using two additional heaps to represent the assertions under each modality. The program heap (along with associated permissions) is a built-in notion in Viper, and so we cannot directly employ three heaps. Therefore, we construct the additional “up” and “down” heaps, by axiomatising bijective mappings Open image in new window and Open image in new window between a real program reference and its counterparts in these heaps. That is, technically our encoding represents each source location through three references in Viper’s heap (rather than one reference in three heaps). Assertions Open image in new window are then represented by replacing all references r in the encoded assertion A with their counterpart Open image in new window . We write Open image in new window for the transformation which performs this replacement. For example, Open image in new window . We write Open image in new window for the analogous transformation for the Open image in new window function.
Fig. 10.

Viper encoding of the FSL rules for relaxed atomics and memory fences from Fig. 8. We omit triggers for the quantifiers for simplicity, but see [3].

The extension of our encoding is shown in Fig. 10. We employ a Viper domain to introduce and axiomatise the mathematical functions for our Open image in new window and Open image in new window mappings. By axiomatising inverses for these mappings, we guarantee bijectivity. Bijectivity allows Viper to conclude that (dis)equalities and other information is preserved under these mappings. Consequently, we do not have to explicitly encode the last two rules of Fig. 8; they are reduced to standard assertion manipulations in our encoding. An additional Open image in new window function labels references with an integer identifying the heap to which they belong ( Open image in new window for real references, Open image in new window and Open image in new window for their “down” and “up” counterparts); this labelling provides the verifiers with the (important) information that these notional heaps are disjoint.

Our handling of relaxed reads and writes is almost identical to that of acquire reads and release writes in Fig. 7; this similarity comes from the proof rules, which only require that the modalities be inserted for the invariant. Our encoding for release fences requires an annotation in the source program to indicate which assertion to prepare for release by placing it under the Open image in new window modality.

Our encoding for acquire fences does not require any annotations. Any assertion under the Open image in new window modality can (and should) be converted to its corresponding version without the modality because Open image in new window is strictly less-useful than A itself. To encode this conversion, we find all permissions currently held in the down heap, and transfer these permissions and the values of the corresponding locations over to the real heap. These steps are encoded for each field and predicate separately; Fig. 10 shows the steps for the Open image in new window field. We first define a set Open image in new window to be precisely the set of all references Open image in new window to which some permission to Open image in new window is currently held, i.e., Open image in new window . For each such reference, we Open image in new window exactly the same amount of permission to the corresponding Open image in new window location, equate the heap values, and then remove the permission to the down locations.

With our encoding based on multiple heaps, reasoning about assertions under modalities inherits all of Viper’s native automation for permission and heap reasoning. We will reuse this idea for a different purpose in the following section.

5 Compare and Swap

C11 includes atomic read-modify-write operations, commonly used to implement high-level synchronisation primitives such as locks. FSL\({+}{+}\) [18] provides proof rules for compare-and-swap (CAS) operations. An atomic compare and swap Open image in new window reads and returns the value of location l; if the value read is equal to e, it also writes the value \(e'\) (otherwise we say that the CAS fails).

\(\mathbf{FSL}{+}{+}\) Proof Rules. FSL++ provides an assertion \(\textsf {RMWAcq}(l,\mathcal {Q})\), which is similar to \(\textsf {Acq}(l, \mathcal {Q})\), but is used for CAS operations instead of acquire reads. A successful CAS both obtains ownership of an assertion via its read operation and gives up ownership of an assertion via its write operation.

FSL\({+}{+}\) does not support general combinations of atomic reads and CAS operations on the same location; the way of reading must be chosen at allocation via the annotation \(\rho \) on the allocation statement (see Fig. 1). In contrast to the \(\textsf {Acq}\) assertions used for atomic reads, \(\textsf {RMWAcq}\) assertions can be freely duplicated and their invariants need not be adjusted for a successful CAS: when using only CAS operations, each value read from a location corresponds to a different write.

Our presentation of the relevant proof rules is shown in Fig. 11. Allocating a location with annotation \(\texttt {RMW}\) provides a \(\textsf {Rel}\) and a \(\textsf {RMWAcq}\) assertion, such that the location can be used for release writes and CAS operations.

For the CAS operation, we present a single, general proof rule instead of four rules for the different combinations of access modes in FSL\({+}{+}\). The rule requires that l is initialised (since its value is read), \(\textsf {Rel}\) and \(\textsf {RMWAcq}\) assertions, and an assertion \(P'\) that provides the resources needed for a successful CAS. If the CAS fails (that is, \(x\not = e\)), its precondition is preserved.

If the CAS succeeds, it has read value e and written value \(e'\). Assuming for now that the access mode \(\tau \) permits ownership transfer, the thread has acquired \(\mathcal {Q}[e/\mathcal {V}]\) and released \(\mathcal {Q}[e'/\mathcal {V}]\). As illustrated in Fig. 12(i), these assertions may overlap. Let T denote the assertion characterising the overlap; then assertion A denotes \(\mathcal {Q}[e/\mathcal {V}]\) without the overlap, and P denotes \(\mathcal {Q}[e'/\mathcal {V}]\) without the overlap. The net effect of a successful CAS is then to acquire A and to release P, while T remains with the location invariant across the CAS. Automating the choice of T, A, and P is one of the main challenges of encoding this rule. Finally, if the access mode \(\tau \) does not permit ownership transfer (that is, fences are needed to perform the transfer), A and P are put under the appropriate modalities.
Fig. 11.

Adapted FSL\({+}{+}\) rules for compare and swap operations. FV yields the free variables of an assertion.

Fig. 12.

An illustration of (i) the proof rule for CAS operations and (ii) our Viper encoding; the dashed regions denote the relevant heaps employed in the encoding.

Encoding. Our encoding of CAS operations uses several techniques presented in earlier sections: see App. E of the TR [35] for details. We represent \(\textsf {RMWAcq}\) assertions analogously to our encoding of \(\textsf {Acq}\) assertions (see Sect. 3). We use the value of field Open image in new window (cf. Fig. 7) to distinguish holding some \(\textsf {RMWAcq}\) assertion from some \(\textsf {Acq}\) assertion. Since \(\textsf {RMWAcq}\) assertions are duplicable (cf. Fig. 11), we employ Open image in new window permissions for the corresponding Open image in new window predicates.

Our encoding of the proof rule for CAS operations is somewhat involved; we give a high-level description here, and relegate the details to App. E of the TR. We focus on the more-interesting case of a successful CAS here. The key challenge is how to select assertion T to satisfy the premises of the rule. Maximising this overlap is desirable in practice since this reduces the resources to be transferred, and which must interact in some cases with the modalities. Our Viper encoding indirectly computes this largest-possible T as follows (see Fig. 12(ii) for an illustration).

We introduce yet another heap (“tmp”) in which we inhale the invariant \(\mathcal {Q}[e/\mathcal {V}]\) for the value read. Now, we exhale the invariant \(\mathcal {Q}[e'/\mathcal {V}]\) for the value written, but adapt the assertions as follows: for each permission in the invariant, we take the maximum possible amount from our “tmp” heap; these permissions correspond to T. Any remainder is taken from the current heap (either the real or the “up” heap, depending on \(\tau \)); these correspond to P. Any permissions remaining in the “tmp” heap after this exhale correspond to the assertion A and are moved (in a way similar to our \(\texttt {fence}_{\texttt {acq}}\) encoding in Fig. 10) to either the real or “down” heap (depending on \(\tau \)).

This combination of techniques results in an automatic support for the proof rule for CAS statements. This completes the core of our Viper encoding, which now handles the complete set of memory access constructs from Fig. 1.

6 Soundness and Completeness

We give a brief overview of the soundness argument for our encoding here, and also discuss where it can be incomplete compared with a manual proof effort; further details are included in App. F of the TR [35].

Soundness. Soundness means that if the Viper encoding of a program and its specification verifies, then there exists a proof of the program and specification using the RSL logics. We can show this property in two main steps. First, we show that the states before and after each encoded statement in the Viper program satisfy several invariants. For example, we never hold permissions to a non-atomic reference’s Open image in new window field but not its Open image in new window field. Second, we reproduce a Hoare-style proof outline in the RSL logics. For this purpose, we define a mapping from states of the Viper program back to RSL assertions and show two properties: (1) When we map the initial and final states of an encoded program statement to RSL assertions, we obtain a provable Hoare triple. (2) Any automatic entailment reasoning performed by Viper coincides with entailments sound in the RSL logics. These two facts together imply that our technique will only verify (encoded) properties for which a proof exists in the RSL logics; i.e. our technique is sound.

Completeness. Completeness means that all programs provable in the RSL logics can be verified via their encoding into Viper. By systematically analysing each rule of these logics, we identify three sources of incompleteness of our encoding: (1) It does not allow one to strengthen the invariant in a \(\textsf {Rel}{}\) assertion; strengthening the requirement on writing does not allow more programs to be verified [37]. (2) For a \(\texttt {fence}_{\texttt {acq}}\), our encoding removes all assertions from under a Open image in new window modality. As explained in Sect. 4, the ability to choose not to remove the modality is not useful in practice. (3) The ghost state employed in FSL\({+}{+}\) can be defined over a custom permission structure (partial commutative monoid), which is not possible in Viper. This is the only incompleteness of our encoding arising in practice; we will discuss an example in Sect. 7.

7 Examples and Evaluation

We evaluated our work with a prototype front-end tool [4], and some additional experiments directly at the Viper level [3]. Our front-end tool accepts a simple input language for C11 programs, closely modelled on the syntax of the RSL logics. It supports all features described in this paper, with the exception of invariant rewriting (cf. App. C of the TR [35]) and ghost state (App. D of the TR), which will be simple extensions. We encoded examples which require these features, additional theories, or custom permission structures manually into Viper, to simulate what an extended version of our prototype will be able to achieve.
Fig. 13.

The results of our evaluation. Examples including _err are expected to generate errors; those with Stronger are variants of the original code with less-efficient atomics and a correspondingly different proof. “Time” reports the verification time in seconds, including the generation of the Viper code. Under “Size”, we measure lines of code, number of distinct functions/threads, and number of loops. Under “Specs”, “PP” stands for the necessary pairs of pre and post-conditions; “LI” stands for loop invariants required. “Other Annot.” counts any other annotations needed. For examples that have been verified in Coq, we report the number of manual proof steps (in addition to pre-post pairs) and provide a reference to the proof.

Our encoding supports several extra features which we used in our experiments but mention only briefly here: (1) We support the FSL\({+}{+}\) rules for ghost state: see App. D of the TR. (2) Our encoding handles common spin loop patterns without requiring loop invariant annotations. (3) We support fetch-update instructions (e.g. atomic increments) natively, modelled as a CAS which never fails.

Examples. We took examples from the RSL [38] and FSL [17] papers, along with variants in which we seeded errors, to check that verification fails as expected (and in comparable time). We also encoded the Rust reference-counting (ARC) library [1], which is the main example from FSL\({+}{+}\) [18]. The proof there employs a custom permission structure, which is not yet supported by Viper. However, following the suggestion of one of the authors [37], we were able to fully verify two variants of the example, in which some access modes are strengthened, making the code slightly less efficient but enabling a proof using a simpler permission model. For these variants, we required counting permissions [10], which we expressed with additional background definitions (see [3] for details, and App. B of the TR [35] for the code). Finally, we tackled seven core functions of a reader-writer-spinlock from the Facebook Folly library [2]. We were able to verify five of them directly. The other two employ code idioms which seem to be beyond the scope of the RSL logics, at least without sophisticated ghost state. For both functions, we also wrote and verified alternative implementations. The Rust and Facebook examples demonstrate a key advantage of building on top of Viper; both require support for extra theories (counting permissions as well as modulo and bitwise arithmetic), which we were able to encode easily.

Performance. We measured the verification times on an Intel Core i7-4770 CPU (3.40 GHz, 16 Gb RAM) running Windows 10 Pro and report the average of 5 runs. For those examples supported by our front-end, the times include the generation of the Viper code. As shown in Fig. 13, verification times are reasonable (generally around 10 s, and always under a 40 s).

Automation. Each function (and thread) must be annotated with an appropriate pre and post-condition, as is standard for modular verification. In addition, some of our examples require loop invariants and other annotations (e.g. on allocation statements). Critically, the number of such annotations is very low. In particular, our annotation overhead is between one and two orders of magnitude lower than the overhead of existing mechanised proofs (using the Coq formalisations for [18, 38] and a recent encoding [22] of RSL into Iris [23]). Such ratios are consistent with other recent Coq-mechanised proofs based on separation logic (e.g. [39]), which suggests that the strong soundness guarantees provided by Coq have a high cost when applying the logics. By contrast, once the specifications are provided, our approach is almost entirely automatic.

8 Conclusions and Future Work

We have presented the first encoding of modern program logics for weak memory models into an automated deductive program verifier. The encoding enables programs (with suitable annotations) to be verified automatically by existing back-end tools. We have implemented a front-end verifier and demonstrated that our encoding can be used to verify weak-memory programs efficiently and with low annotation overhead. As future work, we plan to tackle other weak-memory logics such as GPS [36]. Building practical tools that implement such advanced formalisms will provide feedback that inspires further improvements of the logics.

Footnotes

  1. 1.

    Viper macros can be defined for assertions or statements, and are syntactically expanded (and their arguments substituted) on use.

  2. 2.

    Viper’s heap-dependent functions are mathematical functions of their parameters and the resources stated in their preconditions (here, Open image in new window ) [27, 34].

  3. 3.

    A Open image in new window expression yields the permission fraction held for a field or predicate instance.

Notes

Data Availability Statement and Acknowledgements

The artifact accompanying our submission is available in the TACAS figshare repository [4] at https://doi.org/10.6084/m9.figshare.5900233.v1.

We are grateful to Viktor Vafeiadis and Marko Doko for many explanations of the RSL logics and helpful discussions about our encoding. We thank Christiane Goltz for her work on the prototype tool, and Malte Schwerhoff for implementing additional features. We thank Marco Eilers for his assistance with the online appendix, and Arshavir Ter-Gabrielyan for automating our artifact assembly for various operating systems. We also thank Andrei Dan, Lucas Brutschy and Malte Schwerhoff for feedback on earlier versions of this manuscript.

References

  1. 1.
    ARC (Atomic Reference Counting) Rust library. https://doc.rust-lang.org/std/sync/struct.Arc.html
  2. 2.
    Facebook Folly reader-writer spinlock implementation. https://github.com/facebook/folly/blob/master/folly/RWSpinLock.h
  3. 3.
    Online appendix of Viper-encoded examples. http://viper.ethz.ch/onlineappendix-rsl-encoding/
  4. 4.
    RSL to Viper front-end. figshare.  https://doi.org/10.6084/m9.figshare.5900233.v1
  5. 5.
    Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. CoRR, abs/1701.08682 (2017)Google Scholar
  6. 6.
    Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 134–156. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_8CrossRefGoogle Scholar
  7. 7.
    Alglave, J., Cousot, P.: Ogre and pythia: an invariance proof method for weak consistency models. In: POPL 2017, pp. 3–18. ACM, New York (2017)CrossRefGoogle Scholar
  8. 8.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006).  https://doi.org/10.1007/11804192_17CrossRefGoogle Scholar
  9. 9.
    Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wrocław, Poland, pp. 53–64, August 2011Google Scholar
  10. 10.
    Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of POPL 2005, pp. 259–270. ACM, New York (2005)CrossRefGoogle Scholar
  11. 11.
    Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_29CrossRefzbMATHGoogle Scholar
  12. 12.
    Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44898-5_4CrossRefGoogle Scholar
  13. 13.
    Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 234–245. ACM, New York (2011)Google Scholar
  14. 14.
    Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03359-9_2CrossRefGoogle Scholar
  15. 15.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33826-7_16CrossRefGoogle Scholar
  16. 16.
    Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Effective abstractions for verification under relaxed memory models. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 449–466. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46081-8_25CrossRefzbMATHGoogle Scholar
  17. 17.
    Doko, M., Vafeiadis, V.: A program logic for C11 memory fences. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 413–430. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49122-5_20CrossRefGoogle Scholar
  18. 18.
    Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 448–475. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54434-1_17CrossRefGoogle Scholar
  19. 19.
    Heule, S., Leino, K.R.M., Müller, P., Summers, A.J.: Abstract read permissions: fractional permissions without the fractions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 315–334. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35873-9_20CrossRefzbMATHGoogle Scholar
  20. 20.
    Jacobs, B.: Verifying TSO programs. CW Reports CW660, Department of Computer Science, KU Leuven, May 2014Google Scholar
  21. 21.
    Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17164-2_21CrossRefGoogle Scholar
  22. 22.
    Kaiser, J.-O., Dang, H.-H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong Logic for weak memory: reasoning about release-acquire consistency in Iris. In: ECOOP 2017, vol. 74. LIPIcs, pp. 17:1–17:29. Schloss Dagstuhl-Leibniz (2017)Google Scholar
  23. 23.
    Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696–723. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54434-1_26CrossRefGoogle Scholar
  24. 24.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_20CrossRefzbMATHGoogle Scholar
  25. 25.
    Leino, K.R.M., Müller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00590-9_27CrossRefGoogle Scholar
  26. 26.
    Müller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 405–425. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41528-4_22CrossRefzbMATHGoogle Scholar
  27. 27.
    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49122-5_2CrossRefzbMATHGoogle Scholar
  28. 28.
    O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44802-0_1CrossRefGoogle Scholar
  29. 29.
    Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Logical Methods Comput. Sci. 8(3:01), 1–54 (2012)Google Scholar
  30. 30.
    Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: ACM Annual Conference, vol. 2, ACM 1972, pp. 717–740. ACM (1972)Google Scholar
  31. 31.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS. IEEE Computer Society Press (2002)Google Scholar
  32. 32.
    Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Proceedings of PLDI 2015, pp. 77–87. ACM, New York (2015)CrossRefGoogle Scholar
  33. 33.
    Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1–2:58 (2012)CrossRefGoogle Scholar
  34. 34.
    Summers, A.J., Drossopoulou, S.: A formal semantics for isorecursive and equirecursive state abstractions. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 129–153. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39038-8_6CrossRefGoogle Scholar
  35. 35.
    Summers, A.J., Müller, P.: Automating deductive verification for weak-memory programs (extended version). arXiv:1703.06368 (2018)CrossRefGoogle Scholar
  36. 36.
    Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. In: OOPSLA, pp. 691–707. ACM (2014)CrossRefGoogle Scholar
  37. 37.
    Vafeiadis, V.: Personal communication, December 2016Google Scholar
  38. 38.
    Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA, pp. 867–884. ACM (2013)CrossRefGoogle Scholar
  39. 39.
    Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 59–79. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_4CrossRefGoogle Scholar

Copyright information

© The Author(s) 2018

<SimplePara><Emphasis Type="Bold">Open Access</Emphasis> This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.</SimplePara> <SimplePara>The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.</SimplePara>

Authors and Affiliations

  1. 1.Department of Computer ScienceETH ZurichZurichSwitzerland

Personalised recommendations