«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
the Hoare tuple is deﬁned using the various guards in a continuationpassing style8. There are many details here, which is common when building machine-checked proofs of large, realistic systems, but in simple terms, the Hoare tuple says that for any continuation κ, if the postcondition Q ensures the safety of κ, then the precondition P ensures the safety of c followed by κ.
Using this deﬁnition, Appel and Blazy prove, in Coq, soundness of the rules of sequential separation logic given in ﬁgure 2.6. The rules for skip, sequenceb, assignment, and loop are standard. The rule for storing the the heap requires that e and e2 be pure—that is, not read from the heap. Appel and Blazy demonstrate how to accommodate impure expressions by applying local program transformations. The if-then-else rule also requires that e be pure, which can be handled in closemod (s, A) closes the assertion A over any variables modiﬁed by s.
CHAPTER 2. RELATED WORK
Figure 2.6: Axiomatic Semantics of Separation Logic (without call and return) the same way.
The block and exit rules enable reasoning for nonlocal control ﬂow. Not pictured are the standard rules of separation logic such as the rule of consequence and the frame rule; also missing are the rules for call and return. For a full description of all of the rules and the consequences for sequential control ﬂow we refer the reader to [AB07].
The proofs of these rules with respect to the deﬁnition of the Hoare tuple is done in Coq [AB07]. The most diﬃcult rule to prove was the loop rule, which interacted complexly with the block and exit rules.
the memory model, and basic deﬁnitions, all of which are shared with CompCert. 19% is the deﬁnition of the C minor language and the model for permissions. 2% is the operators and rules of sequential separation logic, and the ﬁnal 42% is the proofs of soundness for those rules.
Like the correctness proofs of the compiler, the proofs of the soundness of the separation logic rules make a number of assumptions about the underlying semantics. Unfortunately, just as in the compiler correctness proofs, several of the assumptions used, such as determinancy of the step relation, are typically false in a concurrent setting. The challenge when adding concurrency will be in a large part how to adapt these sequential-language proofs to a concurrent language.
In the remainder of this thesis, since the focus is not on sequential control ﬂow, both the R and B parameters will be elided from the presentation. However, their existance forms a part of the motivation to design the concurrency system cleanly, which is why they were presented in full detail here: the Hoare tuple is complex enough to begin with, and there is every reason to avoid making it any more complicated than it already is.
With the combination of Appel and Blazy with the work of Leroy, it is possible to create an end-to-end guarantee: properties proven of the source code using separation logic will hold on the code that executes on the machine. Moreover, since the entire system is machine-checked endCHAPTER 2. RELATED WORK to-end, there is very high assurance that the actual program written, when run through the actual compiler used, will actually behave as speciﬁed in the source code.
2.6 Generation of proofs in CSL One issue not yet discussed is where the proofs in CSL come from. One obvious possibility is that they are generated by humans, ideally in some machine-checked setting, as the code is being written. However, this can involve a great deal of additional eﬀort if it is done directly, even considering that the amount of debugging time is dramatically less.
Appel [App06] presents one way to make the process simpler by giving a series of custom Coq tactics for reasoning about C minor programs in Coq. Using these tactics it is possible for a human to generate a proof more easily.
Another approach is given by Gotsman et al. [GBCS07]. Gotsman develops a separation-logic-based shape-analysis algorithm that can automatically generate correctness proofs for certain classes of simple concurrent programs.
Mansky [Man08] uses both approaches. First he takes a relatively
In general humans are able to verify very complex programs, but it takes an enormous amount of eﬀort. In contrast, automatic techniques can only handle relatively simple cases, but are able to do so with great eﬃciency. Clearly a reasonable approach is to combine the two, letting humans handle the diﬃcult parts of a program while using powerful inference techniques to automate the analysis of the simpler parts, but exactly how to do make everything ﬁt together is an open problem.
2.7 Gotsman et al.’s CSL Gotsman et al. independently developed a version of concurrent separation logic [GBC+ 07]. Their CSL is similar to ours, indicating that we
have independently discovered the natural extension of CSL to ﬁrstorder locks. Key diﬀerences between their work and ours include:
1. Our assertion language is more powerful, providing support for features such as impredicative quantiﬁcation, higher-order recursion, and ﬁrst-class function pointers. We are able to use this power to deﬁne very powerful assertions, such as the Hoare tuple, and check programs in a more modular way.
2. We can embed our assertions directly into the syntax of programs, while they must utilize a global table on the side.
velop our system in a highly modular way: the sequential reasoning is isolated from the concurrent reasoning in the model, and the isolation is strong enough to make the proof in Coq tractable.
This modularization leads to a very diﬀerent ﬂavor of soundness proof: while they argue via predicate transformers, we establish soundness in a more operational style.
4. We have a strategy for connecting to an existing certiﬁed compiler, and a thesis for why our results should hold on a machine with a weak memory model, thereby achieving an end-to-end system.
5. Gotsman’s system is designed to connect to the shape analysis tool presented in [GBCS07].
6. Gotsman also presents a method for guaranteeing that all locks
We suspect that it would not be diﬃcult to extend our work to support (6). One interesting avenue for future work would be to combine the positive aspects of the two approches, thereby achieving both (4) and (5) and an even larger end-to-end system.
2.8. MISCELLANEOUS RELATED WORK
2.8 Miscellaneous related work 2.8.1 A very modal model Our semantic model for assertions was built on top of ideas ﬁrst developed for the Princeton Foundational Proof-Carrying Code project for modeling mutable references [AM01, AAV02, AAV03, Ahm04]. Appel et al. [AMRV07] re-engineered this model by developing a modal logic with an underlying Kripke model to achieve greater modularity.
2.8.2 The C0 compiler Leinenbach et al. [LPP05] developed the C0 certiﬁed compiler. C0, like C minor, is a simpliﬁed version of the C language, and the C0 compiler translated C0 into the DLX machine language. This compiler was part of the larger Verisoft project, which built an entire machineveriﬁed hardware/software stack, from the gate level through a TCP/IP stack. The veriﬁcation was done in Isabelle/HOL. In comparison to the CompCert compiler, the C0 compiler is simpler, supporting very few optimizations.
2.8.3 Release Consistency Release consistency, proposed by Gharachorloo et al. [GLL+ 90], is a memory consistency model ﬁrst proposed in the systems/architecture community in 1990. This work was one of the ﬁrst to demonstrate the
CHAPTER 2. RELATED WORK beneﬁts of distinguishing lock/unlock memory accesses from ordinary loads and stores; we follow them in this regard.
Synchronization actions are guaranteed to be sequentially consistent, while normal accesses are not, with the exception that they must execute with respect to synchronization actions in program order. Assuming proper synchronization (similar in nature to that required by CSL), release consistency is consistent with sequential consistency; our thesis for why our system should be sound in the presence of weak memory models is similar.
Chapter 3 Concurrent C minor Concurrent C minor is a new high-level intermediate language suitable for writing concurrent programs. Here we present the new language, give an informal semantics, and present an example. Later we give three diﬀerent formal semanics for Concurrent C minor. First, in chapter 5, we give a simple concurrent operational semantics to demonstrate that we support a standard model for concurrent programming. Second, in chapter 8, we present a more complicated concurrent operational semantics that does additional bookkeeping to allow us to prove strong properties. Last, in chapter 9, we give an oracular semantics, which is a thread-local semantics for concurrent execution1.
Portions of this chapter have been published before as [HAZ08a] and [HAZ08b].
The Concurrent C minor language is built on top of the (sequential) C minor language ﬁrst developed by Leroy [Ler06] and then modiﬁed by Appel and Blazy [AB07]. The sequential features include: complex control ﬂow, such as function calls and multi-exit loops; support for the full ANSI C memory model, including pointer arithmeric and the ability to work with variable-sized data2 ; and certain other features useful in an intermediate language such as locally nameless variables.
In ﬁgure 2.3 we gave the grammar of Appel and Blazy’s version of C minor, which we extend here.
We extend C minor with ﬁve statements to construct Concurrent C
always passes to the next statement in the program.
The lock (e) statement evaluates e to an address v, then waits until it acquires lock v. The unlock (e) statement evaluates e to an address v and then releases the lock v. A lock at location v is locked when the memory contains a 0 at v and unlocked when memory contains a 1 at v.
Each lock comes with a resource invariant R which is an assertion that explains how the lock should be used and which addresses in memory it owns. R must hold before unlocking a lock, which means the next thread to grab the lock will know that R holds. This is standard in CSL [O’H07], but we go further and use the invariants at a crucial point in our unerased concurrent operational semantics to guarantee the absence of race conditions.
The unerased concurrent operational semantics checks the truth of lock invariants when unlocking a lock; failure of this check causes the operational semantics to get stuck, as explained in in chapter 8. The language of these assertions contains the full power of logical propositions (Coq’s Prop), so the operational semantics is nonconstructive, i.e., it is given by a classical relation3.
The set of memory locations controlled by a lock need not be static;
it can change over time depending on the state of memory (e.g., one can say, “this lock controls that variable-sized linked list”). As explained in section 2.5.2, if a thread tries to access memory it does not own, it gets We use a small, consistent set of classical axioms in Coq: extensionality, proposition extensionality, dependent unique choice, and relational choice.
CHAPTER 3. CONCURRENT C MINOR stuck. This protocol ensures the absence of read/write or write/write race conditions.
The statement make lock e R takes an address e and a lock invariant R, and declares e to be a lock with the associated invariant. make lock will get stuck if memory location e does not contain a 0, meaning that the lock is created in the locked state. The address is turned back into an ordinary location by free lock e, which also requires the location e to contain a 0. Both instructions are thread-local, i.e., they don’t synchronize with other threads or the scheduler. It is illegal to apply lock or unlock to nonlock addresses, or to apply ordinary load or store to locks.
The fork statement spawns a new thread, which calls function e on arguments e. No variables are shared between the caller and callee except through the function parameters. All functions in Concurrent C minor are given pre- and postconditions, and the parent passes to the child a portion of the memory it controls, speciﬁed by the precondition of the child. This portion typically contains visibility of some locks so that the two threads can communicate. Just as the operational semantics gets stuck at unlock if the lock invariant does not hold, it will get stuck at fork if the child’s precondition does not hold. A thread exits by returning from its top-level function call.
Although the syntax of Concurrent C minor requires the user to specify lock invariants and function pre- and postconditions, these can be taken directly from a program proof in concurrent separation logic.
Therefore, if the author of a Concurrent C minor program wishes to develop a veriﬁed program, it is not an extra burden to augment the source code with the appropriate invariants.
3.2 Programming with locks To illustrate programming in Concurrent C minor, we give an example program in ﬁgure 3.1. Here we explain the program’s behavior and present an informal proof that it is bug-free. For cross-referencing purposes we number both the lines of the program in ﬁgure 3.1 and the informal proof.
i. Every program in Concurrent C minor has a special function main, where the program begins. In Concurrent C minor, at function declaration it is necessary to give pre- and postconditions.
In the example program, main is declared in line 1, and both the pre- and postconditions are declared to be emp. The assertion language for pre- and postconditions is explained in section 4;
the emp precondition indicates that main can be run at any time, and the emp postcondition indicates that when main terminates