Concise outlines for a complex logic: a proof outline checker for TaDA

Standard separation logic enables the modular verification of heap-manipulating sequential [1, 2] and data-race free concurrent programs [3, 4]. More recently, numerous separation logics have been proposed that enable the verification of fine-grained concurrency by incorporating ideas from concurrent separation logic, Owicki-Gries [5], and rely-guarantee [6]. Examples include CAP [7], iCAP [8], CaReSL [9], CoLoSL [10], FCSL [11], GPS [12], RSL [13], and TaDA [14] (see Brookes et al. [15] for an overview). These logics are very expressive, but challenging to apply because they often comprise many complex proof rules. E.g., our running example (Fig. 1) consists of two statements, but requires over 20 rule applications in TaDA, many of which have non-trivial instantiations and subtle side conditions. This complexity seems inevitable for challenging verification problems involving, e.g., fine-grained concurrency or weak memory.

The complexity of advanced separation logics makes it difficult to develop proofs in these logics. It is, thus, crucial to have tools that check the validity of proofs and automate parts of the proof search. One way to provide this tool support is through proof checkers, which take as input a nearly complete proof and check its validity. They typically embed program logics into the higher-order logic of an interactive theorem prover such as Coq. Proof checkers exist, e.g., for RSL [13] and FCSL [11]. Alternatively, automated verifiers take as input a program with specifications and devise the proof automatically. They typically combine existing reasoning engines such as SMT solvers with logic-specific proof search algorithms. Examples are Smallfoot [16] and Grasshopper [17] for traditional separation logics, and Caper [18] for fine-grained concurrency.

Proof checkers and automated verifiers strike different trade-offs in the design space. Proof checkers are typically very expressive, enabling the verification of complex programs and properties, and produce foundational proofs: ultimately based on a language semantics, with a minimal trusted core. However, existing proof checkers offer little automation. Automated verifiers, on the other hand, significantly reduce the proof effort, but compromise on expressiveness and require substantial development effort, especially, to devise custom proof search algorithms (which increase the trusted core).

It is in principle possible to increase the automation of proof checkers by developing proof tactics, or to increase the expressiveness of automated verifiers by developing stronger custom proof search algorithms. However, such developments are too costly for the vast majority of program logics, which serve mostly a scientific or educational purpose. As a result, adequate tool support is very rare, which makes it difficult for developers of such logics, lecturers and students, as well as engineers to apply, and gain experience with, such logics.

To remedy the situation, several tools took inspiration from the idea of proof outlines [19, 20] (see, e.g., Pierce et al. [21] for a detailed discussion): formal proof skeletons that contain the key proof steps, but omit most of the details. Proof outlines are a standard notation to present program proofs in publications and teaching material. Proof outline checkers such as Starling [22] and VeriFast [23] take as input a proof outline and then check automatically that it represents a valid proof in the program logic. They provide automation for proof steps for which good proof search algorithms exist, and can support expressive logics by requiring annotations for complex proof steps. Due to this flexibility, proof outline checkers are especially useful for experimenting with a logic.

In this paper, we present Voila, a proof outline checker for TaDA [14], which goes beyond existing proof outline checkers and automated verifiers by supporting a substantially more complex program logic, which handles fine-grained concurrency, linearizability, abstract atomicity, and other advanced features. We believe that our systematic development of Voila generalizes to other complex logics. Our contributions are as follows:Outline Sec. 2 gives an overview of the TaDA logic and illustrates our approach. Section 3 presents the Voila proof outline language, and Sec. 4 summarizes how we verify proof outlines. We explain how we automatically expand a proof outline into a proof candidate in Sec. 5 and how we encode a proof candidate into Viper in Sec. 6. Sec. 7 provides a detailed soundness argument. In Sec. 8, we evaluate our technique by verifying several challenging examples. We discuss related work in Sec. 9 and conclude in Sec. 10.

Our full paper [28] contains a substantial appendix with many further details, including: the full version and Viper encoding of our running example, with TaDA levels (omitted from this paper, but supported by Voila) and nested regions; additional inference heuristics; general Viper encoding scheme; and the encoding of a custom guard algebra.

This paper is an extended version of a paper published at Formal Methods 2021 [29]. It has been revised to improve accessibility, particularly in Sec. 2, and extended with the soundness argument in Sec. 7.

Figure 1 shows the first half of our running example, adapted from the original TaDA publication [14]: the TaDA proof outline of the lock procedure of a spinlock, whose atomic specifications capture its essence as a primitive for mutual exclusion. In Sec. 2.4, we then discuss a non-atomic specification derived from lock that conceptually ties a lock to an invariant. As in the original publication [14], the outline in Fig. 1 shows only two out of 22 proof steps, and omits most side conditions. In a TaDA proof outline, a proof step corresponds to the application of a TaDA rule, including suitable pre- and postconditions. Our outline shows applications of the rules MakeAtomic and UpdateRegion. Deriving the shown pre- and postconditions may require additional rule applications, which are omitted.

We use our running example to introduce the necessary TaDA background, explain TaDA proof outlines, and illustrate the corresponding Voila proof outlines.

Proof outlines annotate programs with rule applications of a given program logic. These annotations indicate where to apply rules and how to instantiate their meta-variables. The goal of a proof outline is to convey the essential proof steps; ideally, consumers of such outlines can then construct a full proof with modest effort. Consumers may be human readers [19], or tools that automatically check the validity of a proof outline [22, 23, 32]; our focus is on the latter.

The key challenge of designing a proof outline language is to define annotations that accomplish this goal with low annotation overhead for proof outline authors. To approach this challenge systematically, we classify the rules of the program logic (here: TaDA) into three categories: (1) For some rules, the program prescribes where and how to apply them, i.e., they do not require any annotations. We call such rules syntax-driven rules. An example in standard Hoare logic is the assignment rule, where the assignment statement prescribes how to manipulate the adjacent assertions. (2) Some rules can be applied and instantiated in many meaningful ways. For such rules, the author of the proof outline needs to indicate where or how to apply them through suitable annotations. Since such rules often indicate essential proof steps, we call them key rules. In proof outlines for standard Hoare logic, the while-rule typically requires an annotation how to apply it, namely the loop invariant. (3) The effort of authoring a proof outline can be greatly reduced by applying some rules heuristically, based on information already present in the outline. We call such rules bridge rules. Heuristics reduce the annotation overhead, but may lead to incompleteness if they fail; a proof outline language may provide annotations to complement the heuristics in such situations, slightly blurring the distinction between key and bridge rules. E.g., the Dafny verifier [33] applies heuristics to guess termination measures for loops, but also offers an annotation to provide a measure manually, if necessary. Another common example is the rule of consequence: SMT-based verifiers (such as Voila) automatically discharge most entailment checks, but may require additional user annotations in cases where the underlying SMT solver is incomplete.

The rule classification depends on the proof search capabilities of the verification tool that is used to check the proof outline. We use Viper [25], which provides a high degree of automation for standard separation logic and, thus, allows us to focus on the specific aspects of TaDA.

In the rest of this section, we give an overview of the Voila proof outline language and, in particular, discuss which TaDA rules are supported as syntax-driven, key, and bridge rules. Voila’s grammar can be found in the full paper [28], showing that Voila strongly resembles TaDA, but requires fewer technical details.

Background Definitions. Voila’s syntax for declaring regions and transitions closely resembles TaDA, but e.g., subscripts are replaced by additional parameters, such as the region identifier r. A region declaration defines the region’s content via an interpretation assertion, and its value via a state function. The latter may refer to region parameters, as well as values bound in the interpretation, such as v in the example from Fig. 3. The region’s transition system is declared by introducing the guards and the permitted actions, i.e., transitions. Voila includes several built-in guard algebras (adopted from Caper [18]); additional ones can be encoded, see the full paper [28]. A region declaration introduces a corresponding region predicate, which has an additional out-parameter that yields the region’s abstract state (e.g., s in the precondition of procedure lock in Fig. 3), as defined by the state function. We omit this out-parameter when its value is irrelevant.

Specifications. Voila proof outlines require specifications for procedures, and invariants for loops; we again chose a TaDA-like syntax for familiarity. Explicit loop invariants are required by Viper, but also enable us to automatically instantiate certain bridge rules (see framing in Sec. 5).

Recall that specifications in TaDA are written as atomic or non-atomic triples, and include an interference context and an atomicity context. Voila simplifies the notation significantly by requiring these contexts only for abstractly-atomic procedure specifications; for all statements and rule applications, they are determined automatically, despite changing regularly during a proof. For procedures with abstractly-atomic behavior (modifier abstract_atomic), the interference context is declared through the interference clause. E.g., for procedure lock from Fig. 3, it corresponds to TaDA’s interference context .

Key Rules. In addition to procedure and loop specifications, Voila requires user input only for the following fundamental TaDA rules: UpdateRegion, MakeAtomic, UseAtomic, and OpenRegion; applications of all other rules are automated. Since they capture the core ideas behind TaDA, these rules are among the most complex rules of the logic and admit a vast proof search space. Therefore, their annotation is essential, for both human readers [14, 24] and automatic checkers. As seen in Fig. 3, the annotations for these key rules include only the used region and, for updates, the used guard; all other information present in the corresponding TaDA rules is derived automatically.

Bridge Rules. All other TaDA rules are applied automatically, and thus have no Voila counterparts. This includes all structural rules for manipulating triple atomicity (e.g., AWeakening1, AExists), interference contexts (e.g., Substitution, AWeakening2), and levels (e.g., AWeakening3). Their applications are heuristically derived from the program, applications of key rules, and adjacent triples. TaDA’s frame rule is also automatically applied by leveraging Viper’s built-in support for framing, combined with additional encoding steps to satisfy TaDA’s frame stability side condition. Finally, TaDA entailments are bridge rules when they can be automated by the used verification tool. For Viper, this is the case for standard separation logic entailments, which constitute the majority of entailments to perform. To support TaDA’s view shifts [24, 34]—entailments similar to the classical rule of consequence, but involving arbitrary definitions of regions and guard algebras—Voila provides specialized annotations.

Our approach, and corresponding implementation, enables the following workflow: users provide a proof outline and possibly some annotations for complex entailments. If the outline summarizes a valid proof, verification is automatic, without a tedious process of manually applying additional rules. If the outline is invalid, our tool reports which specification (e.g., loop invariant) it could not prove or which key rule application it could not verify, and why (e.g., missing guard).

Achieving this workflow, however, is challenging: by design, proof outlines provide the important proof steps, but are not complete proofs. Consider, e.g., the TaDA and Voila outlines from Fig. 1 and Fig. 3, respectively. Applying UpdateRegion produces an atomic triple in its conclusion, whereas the while-rule requires a non-atomic triple for the loop body. A complete proof needs to perform the necessary adjustment through additional applications of bridge rules, which are not present in the proof outlines, and thus need to be inferred.

Our workflow is enabled by first expanding proof outlines into proof candidates, in two main steps: step 1 automatically inserts the applications of all syntax-driven rules; step 2 expands further by applying heuristics to insert bridge rule applications. The resulting proof candidate contains the applications of all rules of the program logic. Afterwards, we check that the proof candidate corresponds to a valid proof, by encoding it as a Viper program that checks whether all proof rules are applied correctly. Our actual implementation deviates slightly from this conceptual structure, e.g., because Viper does not require one to make the application of all syntax-driven rules, framing, and entailment checking explicit.

Automatically expanding a proof outline is ultimately a proof search problem, with a vast search space in case of complex logics such as TaDA. Our choice of key rules (and corresponding annotations) reduces the search space, but it remains vast, due to TaDA’s many structural rules that can be applied to almost all triples. To further reduce the search space, without introducing additional annotation overhead, we devised (and enforce) a normal form for proof candidate triples. Our normal form allows us to define heuristics for the application of bridge rules locally, based only on adjacent rule applications, without having to inspect larger proof parts. This locality reduces the search space substantially, and enables us to automatically close the gap between user-provided proof outline and finally verified proof candidate. Out of the 22 rule applications for our running example, our heuristics infer 17 applications of bridge rules. Three syntax-driven rules are also applied automatically, such that only two key rules require manual annotations. The complete TaDA proof shown in App. A details all inferred applications of bridge rules and syntax-driven rules.

It might be helpful to consider an analogy with standard Hoare logic: its rule of consequence can be applied to each Hoare triple. A suitable normal form could restrict proofs to use the rule of consequence only at the beginning of the program and for each loop (as in a weakest-precondition calculus). A heuristic can then infer the concrete applications, in particular, the entailments used in the rule application, treating the rule as a bridge rule.

Normal Form. Our normal form is established by a combination of syntactic checks and proof obligations in the final Viper encoding. Its main restrictions are as follows: (1) A triple is atomic if and only if the enclosed Voila outline statement is abstract atomic, namely a CAS operation, a call to an abstract atomic procedure, or a key rule statement. As a consequence, we can infer the triple kinds from statements and key rule applications. Due to this restriction, Voila cannot express specifications that combine atomic and non-atomic behaviors. However, such specifications do not occur frequently (see Sec. 5.2.3 in [24] for an example) and could be supported via additional annotations. (2) All triple preconditions, as well as the postconditions of non-atomic triples, are stable, i.e., cannot be invalidated by (legal) concurrent operations. In contrast, TaDA requires stability only for certain assertions. Our stronger requirement enables us to rely on stability at various points in the proof instead of having to check it—most importantly, when Viper automatically applies its frame rule. To enforce this restriction, we eagerly stabilize assertions through suitable weakening steps. (3) In atomic triples, the state of every region is bound by exactly one interference quantifier ( ), which simplifies the manipulation of interference contexts, e.g., for procedure calls. To the best of our knowledge, this restriction does not limit the expressiveness of Voila proofs. (4) Triples must hold for a range of atomicity contexts , rather than just a single context. This stronger proof obligation rules out certain applications of MakeAtomic –which we have seen only in contrived examples—but it increases automation substantially and improves procedure modularity.

By design, our normal form prevents Voila from constructing certain TaDA proofs. However, the only practical limitation is that Voila does not support TaDA’s combination of atomic and non-atomic behavior in a single triple. As far as we are aware, all other normal form restrictions do not limit expressiveness for practical examples, or can be worked around in systematic ways.

Heuristics. We employ five main heuristics: (1) to determine when to change triple atomicity, (2) to ensure stable frames by construction, (3) to compute atomicity context ranges, (4) to compute levels, and (5) to compute interference contexts in procedure body proofs. All heuristics are based on inspecting adjacent rule applications and their proof state. We briefly discuss the first three heuristics here, and refer readers to the full paper [28] for the remaining two heuristics. There, we give a more detailed explanation, and illustrate our heuristics in the context of our running example. (1)  Changing triple atomicity corresponds to an application of (at least) TaDA rule AWeakening1, necessary when a non-atomic composite statement (e.g., the while statement in Fig. 1) has an abstract-atomic sub-statement (e.g., the atomic CAS in Fig. 1). We infer all applications of this rule. (2)  A more complex heuristic is used in the context of framing: TaDA’s frame rule requires the frame, i.e., the assertion preserved across a statement, to be stable. For simple statements such as heap accesses, it is sound to rely on Viper’s built-in support for framing. For composite statements with arbitrary user-provided footprints (assertions such as a loop invariant describing which resources the composite statement may modify), we greedily infer frame rule applications that attempt to preserve all information outside the footprint. The inferred applications are later encoded in Viper such that the resulting frame is stable, by applying suitable weakening steps. (3)  Atomicity context ranges are heuristically inferred from currently-owned tracking-resources and level information. Atomicity contexts are not manipulated by a specific TaDA rule, but they need to be instantiated when applying rules: most importantly, TaDA’s procedure call rule, but also e.g., MakeAtomic and UpdateRegion (see Fig. 2).

For our running example from Fig. 1, four of our heuristics are necessary to complete the proof candidate. The heuristic (1) is necessary around UpdateRegion to change the triple atomicity. The heuristic (2) is necessary around the CAS operation to frame information about the arguments. The heuristic (3) is necessary so that clients can call the Lock procedure. Lastly, the heuristic (4) is necessary around UpdateRegion to change levels.

Proof candidates—i.e., the user-provided program with heuristically inserted bridge rule applications—do not necessarily represent valid proofs, e.g., when users provide incorrect loop invariants. To check whether a proof candidate actually represents a valid proof, we need to verify (1) that each rule is applied correctly, in particular, that its premises and side conditions hold, and (2) that the property shown by the proof candidate entails the intended specification. To validate proof candidates automatically, we use the existing Viper tool [25]. In this section, we give a high-level overview of how we encode proof candidates into the Viper language.

Viper Language. Viper uses a variation of separation logic [35, 36] whose assertions separate access permissions from value information: separation logic’s points-to assertion x.f \(\mapsto \)  v is expressed as acc(x.f) && x.f == v, and separation logic predicates [30] are similarly split into a predicate (abstracting over permissions) and a heap-dependent function (abstracting over values). Well-definedness checks ensure that the heap is accessed only under sufficient permissions. Viper provides a simple imperative language, which includes in particular two statements to manipulate the verification state: exhale A asserts all logical constraints in assertion A, removes the permissions in A from the current state (or fails if the permissions are not available) and assigns non-deterministic values to the corresponding memory locations (to reflect that the environment could now modify them); inhale A conversely assumes constraints and adds permissions.

Regions and Assertions. TaDA’s regions introduce various resources such as region predicates and guards. We encode these into Viper permissions and predicates as summarized in Fig. 6 (left). Each region R gives rise to a corresponding predicate, which is defined by the region interpretation. A region’s abstract state may be accessed by a Viper function R_State, which is defined based on the region’s state clause, and depends on the region predicate. Moreover, we introduce an abstract Viper predicate R_g for each guard g of the region.

These declarations allow us to encode most TaDA assertions in a fairly straightforward way. E.g., the assertion \(\text {Lock}_{r}(\texttt {x}, s)\) from Fig. 1 is encoded as a combination of a region predicate and the function yielding its abstract state: Lock(r,x) && Lock_State(r,x) == s. We encode region identifiers as references in Viper, which allows us to use the permissions and values of designated fields to represent resources and information associated with a region instance. E.g., we use the permission acc(r.diamond) to encode the TaDA resource .

Rule Applications. Proof candidates are tree structures, where each premise of a rule application R is established as the conclusion of another rule application, as illustrated above. In TaDA, the statement of the premise \(s_p\) is guaranteed to be a substatement of the statement of the conclusion \(s_c\). To check the validity of a candidate, we check the validity of each rule application. For rules that are natively supported by Viper (e.g., the assignment rule), Viper performs all necessary checks. Each other rule application is checked via an encoding into the following sequence of Viper instructions: (1) Exhale the precondition \(P_c\) of the conclusion to check that the required assertion holds. (2) Inhale the precondition \(P_p\) of the premise since it may be assumed when proving the premise. (3) After the encoding of the proof for the premise, exhale the postcondition \(Q_p\) of the premise to check that it was established by the proof for the premise. (4) Inhale the postcondition \(Q_c\) of the conclusion. Steps 2 and 3 are performed for each premise of the rule. Moreover, we assert the side conditions of each rule. If a proof candidate is invalid, e.g., composes incompatible rules, one of the checks above fails and the candidate is rejected.

Using this encoding of rule applications as building blocks, we can assemble entire procedure proofs as follows: for each procedure, we inhale its precondition, encode the rule application for its body, and then exhale its postcondition.

Example: Stabilizing Assertions. Recall that an assertion A is stable if and only if the environment cannot invalidate A by performing any legal region updates. In practice, this means that the environment cannot hold a guard that allows it to change the state of a region in a way that violates A. The challenge of checking stability as a side condition is to avoid higher-order quantification over region instances and guards, which is hard to automate. We address this challenge by eagerly stabilizing assertions in the Viper encoding, i.e., we weaken Viper’s verification state such that the remaining information about the state is stable. We achieve this effect by first assigning non-deterministic values to the region state and then constraining these to be within the states permitted by the region’s transition system, taking into account the guards the environment could hold. The Viper code for stabilizing instances of lock can be found in the full paper [28].

Voila is sound if the successful verification of a procedure in Voila implies that the procedure’s specification can be derived in TaDA. That is, our soundness argument builds on the soundness of the TaDA logic itself, which has been proven separately [37] w.r.t. an operational semantics. Voila succeeds if the encoded proof candidate of the procedure successfully verifies in Viper. Consequently, to show soundness of Voila, we need to show that successful verification of a proof candidate in Viper implies the existence of a corresponding TaDA proof for the given procedure and its specification.

Notations. Before we formalize our argument, we introduce basic terminology and notation. As discussed in Sec. 6, proof candidates are derivation trees in the TaDA logic. We refer to the proof candidate that is inferred for a Voila outline statement \(s\) as the proof candidate for \(s\). We introduce a function \(C\) to model the inference of proof candidates, where \(C( s )\) is the proof candidate of the Voila outline statement \(s\). The entire proof candidate for a procedure is obtained by applying \(C\) to the procedure’s body. For a proof candidate \(p\), \(p\)’s root is the last rule application of \(p\), which derives the overall conclusion, and \(p\)’s children are the proof candidates whose roots are rule applications to the premises of that last rule application in \(p\).

As discussed in Sec. 6, proof candidates are encoded to Viper statements by encoding all rule applications of the proof candidate. For a proof candidate \(p\), \(\llbracket \, p \, \rrbracket \) denotes the Viper statement that \(p\) is encoded to. We use the same notation to encode TaDA assertions and expressions. Viper verification states model the entire knowledge of the Viper verifier at a specific point in a Viper program. Technically, each Viper verification state is a set of concrete Viper states; this set can be characterized by a Viper assertion. For a Viper assertion A, \(\Upsilon ( A )\) denotes the initial Viper verification state after inhaling A only. The expression \(\textsf {post}(c, \upsilon )\) denotes the Viper verification state resulting from verifying a Viper statement c starting from the Viper verification state \(\upsilon \). The function \(\textsf {post}\) is analogous to the strongest postcondition of standard Hoare logic. We refer to \(\upsilon \) and \(\textsf {post}(c, \upsilon )\) as the Viper verification pre- and poststate of c, respectively. The special error Viper verification state \(\lightning \) models that an assertion failed during verification. We use \(s\), \(p\), \(\upsilon \) to range over Voila outline statements, proof candidates, and Viper verification states, respectively.

We evaluated Voila on nine benchmark examples from Caper’s test suite, with the Treiber’s stack [39] variant BagStack being the most complex example, and report verification times and annotation overhead. Each example has been verified in two versions: a version with Caper’s comparatively weak non-atomic specifications, and another version with TaDA’s strong atomic specifications; see Sec. 9 for a more detailed comparison of Voila and Caper. An additional example, CounterCl, demonstrates the encoding of a custom guard algebra not supported in Caper (see the full paper [28]). To evaluate the performance for both successful and failing verification attempts, we seeded four examples with errors in the loop invariant, procedure postcondition, code, and region specification, respectively. Our benchmark suite is relatively small, but each example involves nontrivial specifications. To the best of our knowledge, no other (semi-)automated tool is able to verify similarly strong specifications.

Performance. Fig. 7 shows the runtime for each example in seconds. All measurements were carried out on a Lenovo W540 with an Intel Core i7-4800MQ and 16GB of RAM, running Windows 10 x64 and Java HotSpot JVM 18.9 x64; Voila was compiled using Scala 2.12.7. We used a recent checkout of Viper and Z3 4.5.0 x64 (we failed to compile Caper against newer versions of Z3). Each example was verified ten times (on a continuously-running JVM); after removing the highest and lowest measurement, the remaining eight values were averaged. Caper (which compiles to native code) was measured analogously.

Overall, Voila’s verification times are good; most examples verify in under five seconds. Voila is slower than Caper and its logic-specific symbolic execution engine, but it exhibits stable performance for successful and failing runs, which is crucial in the common case that proof outlines are developed interactively, such that the checker is run frequently on incorrect versions. As demonstrated by the error-seeded versions of TLockCl and BagStack, Caper’s performance is less stable.

Another interesting observation is that strong specifications typically do not take significantly longer to verify, although only they require the full spectrum of TaDA ingredients and make use of TaDA’s most complex rules, MakeAtomic and UpdateRegion. Notable exceptions are: BagStack, where only the strong specification requires sequence theory reasoning; and TLock and BoundedCtr, whose complex transition systems with many disjunctions significantly increase the workload when verifying atomicity rules such as MakeAtomic.

Automation. Voila’s annotation overhead, averaged over the programs with strong specifications from Fig. 7, is 0.8 lines of proof annotations (not counting declarations and procedure specifications; neither for Caper) per line of code, which demonstrates the high degree of automation Voila achieves. Caper has an average annotation overhead of 0.13 for its programs from Fig. 7, but significantly weaker specifications. Verifying only the latter in Voila does not reduce annotation overhead significantly since Voila was designed to support TaDA’s strong specifications. The overhead reported for encodings into interactive theorem provers such as Coq [13, 40‐42] is typically much higher, ranging between 10 and 20.

We compare Voila to three groups of tools: automated verifiers, focusing on automation; proof checkers, focusing on expressiveness; and proof outline checkers, designed to strike a balance between automation and expressiveness. Closest to our work in the kind of supported logic is the automated verifier Caper [18], from which we drew inspiration, e.g., for how to specify region transition systems. Caper supports an improved version of CAP [7], a predecessor logic of TaDA. Caper’s symbolic execution engine achieves an impressive degree of automation, which, for more complex examples, is higher than Voila’s. Caper’s automation also covers slightly more guard algebras than Voila. However, the automation comes at the price of expressiveness, compared to Voila: postconditions are often significantly weaker because the logic does not support linearizability (or any other notion of abstract atomicity). E.g., Caper cannot prove that the spinlock’s unlock procedure actually releases the lock. As was shown in Sec. 8, Caper is typically faster than Voila, but exhibits less stable performance when a program or its specifications are wrong.

Other automated verifiers for fine-grained concurrency reasoning are SmallfootRG [43], which can prove memory safety, but not functional correctness, and CAVE [44], which can prove linearizability, but cannot reason about non-linearizable code (which TaDA and Voila can). VerCors [45] combines a concurrent separation logic with process-algebraic specifications; special program annotations are used to relate concrete program operations to terms in the abstract process algebra model. Reasoning about the resulting term sequences is automated via model checking, but is non-modular. Summers et al. [46] present an automated verifier for the RSL family of logics [13, 40, 47] for reasoning about weak-memory concurrency. Their tool also encodes into Viper and requires very few annotations because proofs in the RSL logics are more stylized than in TaDA.

A variety of complex separation logics [11‐13, 40, 47‐51] are supported by proof checkers, typically via Coq encodings. As discussed in the introduction, such tools strike a different trade-off than proof outline checkers: they provide foundational proofs, but typically offer little automation, which hampers experimenting with logics. Diaframe [52] introduces a proof search strategy for Iris [53], achieving foundational proofs and a high degree of automation. This strategy applies rules based on the syntactic shape of the verification goal. To improve completeness, users can provide hints that specify how certain goals are split into subgoals. In contrast to TaDA and our work, Diaframe does not support abstract atomicity.

Starling [22] is a proof outline checker and closest to Voila in terms of the overall design, but it focuses on proofs that are easy to automate. To achieve this, it uses a simple instantiation of the Views meta-logic [34] as its logic. Starling’s logic does not enable the kind of strong, linearizability-based postconditions that Voila can prove (see the discussion of Caper above). Starling generates proof obligations that can be discharged by an SMT solver, or by GRASShopper [17] if the program requires heap reasoning. The parts of an outline that involve the heap must be written in GRASShopper’s input language. In contrast, Voila does not expose the underlying system, and users can work on the abstraction level of TaDA.

VeriFast [23] can be seen as an outline checker for a separation logic with impressive features such as higher-order functions and predicates. It has no dedicated support for fine-grained concurrency, but the developers manually encoded examples such as concurrent stacks and queues. VeriFast favors expressiveness over automation: proofs often require non-trivial specification adaptations and substantial amounts of ghost code, but the results typically verify quickly.

We introduced Voila, a novel proof outline checker that supports most of TaDA’s features, and achieves a high degree of automation and good performance. This combination enables concise proof outlines with a strong resemblance of TaDA.

Voila is the first deductive verifier that can reason automatically about a procedure’s effect at its linearization point, which is essential for a wide range of concurrent programs. Earlier work either proves much weaker properties (the preservation of basic data structure invariants rather than the functional behavior of procedures) or requires substantially more user input (entire proofs rather than concise outlines).

We believe that our systematic approach to developing Voila can be generalized to other complex logics. In particular, encoding proof outlines into an existing verification framework allows one to develop proof outline checkers efficiently, without developing custom proof search algorithms. Our work also illustrates that an intermediate verification language such as Viper is suitable for encoding a highly-specialized program logic such as TaDA. During the development of Voila, we uncovered and fixed several soundness and modularity issues in TaDA, which the original authors acknowledged and had partly not been aware of. We view this as anecdotal evidence of the benefits of tool support that we described in the introduction.

Voila supports the vast majority of TaDA’s features; most of the others can be supported with additional annotations. The main exception are TaDA’s hybrid assertions, which combine atomic and non-atomic behavior. Adding support for those is future work. Other plans include an extension of the supported logic, e.g., to handle extensions of TaDA [37, 54].