«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
ii. In line 2, the program allocates and initializes a 4-word block of memory5. The local variable i is initialzied to 0 in line 3.
iii. In line 4, the bookkeeping instruction make lock turns memory location L from a normal memory location into a lock with an invariant R(L); see ﬁgure 3.2 for a schematic of the invariant. Informally, the invariant says that the lock L guards the next three locations in memory. The ﬁrst two locations contain data values which are supposed to be equal. The last location contains a “continue” ﬂag; a 1 indicates that the child thread is still computing, whereas a 0 indicates that it has completed. In section 4.9 we will formally discuss the exact invariant used. Like all locks, the lock is created in the locked state.
iv. In line 5, the function f is spawned as a child thread, and is passed the parameter L, the address of the still-locked lock.
v. In line 6, the continue ﬁeld is set to 1, meaning that the child has not ﬁnished computing. Even though the child has already been started, this is safe because the child is not able to see the In the implemented Concurrent C minor, memory is byte-addressed; locks are word-sized and must be word-aligned. We simplify the presentation by assuming word addressing.
CHAPTER 3. CONCURRENT C MINOR continue ﬁeld until it grabs the lock L, which is currently being held by the parent.
vi. In lines 7–13, the main thread loops. First, in line 8, it checks to see whether the continue ﬂag has been reset to 0; if so, it breaks out of the loop. Then, in line 9, it modiﬁes the data cells by setting them equal to the local variable i, before unlocking the lock in line 10. Then it increments i in line 11, grabs the lock again in line 12, and loops back around.
vii. Control reaches line 14 after the child process has set the continue ﬂag to 0, indicating that it has completed. Accordingly, it should be safe to convert the location L from a lock back into a regular piece of memory, so we use the bookkeeping instruction free lock.
viii. In lines 15–16, there is a test that checks whether the two data cells contain the same value; if they do not, then the program gets stuck. Since both threads write to both data cells, it is not obvious whether this test will succeed. However, lines 9 and 24– 25, where the data ﬁelds are mutated, shows that as long as as the values are identical before they are modiﬁed, they will be identical afterwards. Since they both start as 0, we can informally conclude that they will be equal at this point in the program. In 4.9.2 we will formally prove that they are equal.
x. Line 21 declares the child process f. The precondition of the function f is that the argument l is a lock with invariant R(l), while the postcondition emp indicates that when the child terminates it will have given up all of its resources (including the lock passed as an argument).
xi. In lines 22–29, the child loops. It grabs the lock on line 23, and then modiﬁes the protected data in lines 24–25. On line 26, the child tests to see if the ﬁrst data cell is larger than 10; if so, it sets the continue ﬂag to 0 in line 27, unlocks the lock in line 28, and exits the thread by returning from the function in line 29.
Otherwise, the thread unlocks the lock in line 31, and loops back around.
The explanation given above indicates what the example program does and why it is correct. In section 4.9 we give parts of the formal proof of correctness. Mansky provides a fully systematic proof of correctness in Coq using our Concurrent Separation Logic in [Man08].
Concurrent Separation Logic
Concurrent Separation Logic for Concurrent C minor is a new program logic for reasoning about the correctness of programs written in Concurrent C minor. Here we present the assertions of the logic, give the Hoare rules using those assertions to reason about the concurrent language features, and demonstrate the power of the system by verifying the example program presented in section 3.2. The semantics of assertions and the Hoare tuple are quite complicated and so are deferred until chapters 7 and 10, respectively1.
To support reasoning in Concurrent Separation Logic, we have many of the usual assertions of Hoare logic: true and false; conjunction ∧ and disjunction ∨; universal and existential quantiﬁers ∀ and ∃; equirePortions of this chapter have been published before as [HAZ08a] and [HAZ08b].
CHAPTER 4. CONCURRENT SEPARATION LOGIC cursive assertions µF ; assertions in the base (Coq) logic [A]Coq ; and assertions that a C minor expression e evaluates to a value v, e ⇓ v. C minor expressions can read the heap but not write to it. Most of our separation logic operators take only pure expressions, i.e., those that do not read the heap. Appel and Blazy [AB07, §4] show how to bridge the pure-impure gap in Separation Logic by local program transformations.
We support impredicative quantiﬁcation—that is, our universal and existential quantiﬁers range over all types, including assertions themselves. This powerful form of quantiﬁcation is useful for reasoning about complex language features such as objects, higher-order functional programs, and generics.
We do not expose full implication to the user, since it interacts complexly with the underlying model. We do support many kinds of limited implication, however. Similarily, we do not expose full negation.
The problems surrounding implication are explained in section 7.3.7.
4.2 Sequential separation logic assertions To these Hoare logic assertions we add the standard assertions of separation logic: the empty heap emp, which gives no permission to access memory; the singleton “maps-to” e → v, which gives permission to access the location e, and asserts that location e currently contains the value v 2 ; and the separating conjunction P ∗ Q, which says that the Since C minor allows for variable-sized data, the actual relation used in the proofs also handles the size of the data, but this detail has been elided for the
4.3. FRACTIONAL OWNERSHIP memory can be divided (not necessarily uniquely) into two parts, the ﬁrst of which satisﬁes P and the second of which satisﬁes Q. We augment the maps-to assertion with the concept of fractional ownership.
4.3 Fractional ownership First-class locks are only useful if more than one thread has the ability to try to grab the lock at the same time. Fractional ownership allows the the ownership of an address to be split into pieces. With partial ownership of a standard location, reading from that location is allowed but writing to it is not. With partial ownership of a lock location, trying to acquire the lock is allowed.
Fractional ownerships also enable the veriﬁcation of concurrent algorithms that utilize a multiple-reader, single-writer protocol; moreover, they can also simplify sequential reasoning. For example, at a function call, a caller can pass just the read permission for an address to the callee. After the callee returns, the caller will know that the callee did not modify the address (but could have read it)3.
Further applications of fractional ownership can be found in Boyland [Boy03] and Bornat et al. [BCOP05].
CHAPTER 4. CONCURRENT SEPARATION LOGIC Shares come with a join relation π1 ⊕ π2 = π, which indicates that the shares π1 and π2 combine to form the new share π. Not every pair of shares π1 and π2 join—often there is no π that will serve. We write πa ⊥ πb to mean that πa and πb join; that is, ∃πc. πa ⊕ πb = πc.
Conversely, we write πa ⊥ πb to mean that πa and πb do not join; that is, πa ⊥ πb ≡ ¬ (πa ⊥ πb ). We write πa ⊂ πc to mean that πa joins with some other share πb to equal πc ; that is, πa ⊂ πc ≡ ∃πb. πa ⊕ πb = πc.
4.4 Stratiﬁed separation algebras Our shares and the join relation are similar to the notion of a separation algebra as deﬁned by Calcagno et al. [COY07]. A separation algebra is a partial commutative monoid with a cancellation property. That is, a
separation algebra has the following properties:
1. Determinism: (πa ⊕ πb = π1 ) ⇒ (πa ⊕ πb = π2 ) ⇒ π1 = π2
2. Associativity: (π1 ⊕ π2 = πa ) ⇒ (πa ⊕ π3 = π) ⇒
3. Commutativity: (π1 ⊕ π2 = π) ⇒ (π2 ⊕ π1 = π)
4. Cancellation: (π1 ⊕ πa = π) ⇒ (π2 ⊕ πa = π) ⇒ π1 = π2
5. Identity: ∃πe. ∀π. πe ⊕ π = π (1)–(5) gives a clean, standard deﬁnition, and it is possible to develop a model for shares with it (the identity is the empty share). However,
4.4. STRATIFIED SEPARATION ALGEBRAS it will not be suﬃcient when the join relation is extened to resource maps in chapter 7, since the model presented there has multiple distinct empty resource maps. From an engineering perspective the generalization to multiple identity elements is simpler if it is done uniformly, since it means a lemma library needs to be developed only once. Accordingly,
we replace (5) with (6), which swaps the order of the quantiﬁers:
6. Multiple identities: ∀π. ∃πe(π). πe(π) ⊕ π = π The idea of multiple identity elements in a commutative setting is unusual, since there is a standard proof that in such a setting, if two identity elements join with each other then they must be equal.
If πe1 and πe2 are identity elements, and if
Proof. πe1 ⊥πe2 means that there exists π such that πe1 ⊕ πe2 = π. Since πe1 is an identity, we know that πe1 ⊕ πe2 = πe2. By cancellation, π = πe2. By commutativity, we know πe2 ⊕ πe1 = π. Since πe2 is an identity, πe2 ⊕ πe1 = πe1. By cancellation, we know that π = πe1. Thus, by transitivity of equality, πe1 = πe2. Proved in Coq.
However, join is a partial function, which means that not every element must join with a given identity. Therefore, it is reasonable to imagine a set of identity elements, each of which can join with certain other elements. Since if two identity elements join they must be the same
CHAPTER 4. CONCURRENT SEPARATION LOGIC element, this means that the sets of elements that join to particular empty elements form an equivalence class.
One additional property that we want for our join relation is
7. Split identities: ∀πa, πb, πe. (πa ⊕ πb = πe ) ⇒ identity πe ⇒ identity πa This property says that if two elements join to an identity element, then both must be an identity element as well; it is a kind of monotonicity property. Property (7) is not true for all separation algebras (e.g., Z with addition); however, it is true for common examples of separation algebras (e.g., sets of N with the disjoint union operation), and does not
4.5. ADDITIONAL PROPERTIES FOR SHARES pose serious diﬃculties in a model. Accordingly, for us, a join relation has properties (1)–(4) and (6)–(7); it is a separation algebra with the pathological4 combination of multiple and split identities, which we call a stratiﬁed separation algebra 5. We call a type with a join relation that obeys the stratiﬁed separation algebra axioms a joinable type. Our Coq development has many diﬀerent examples of joinable types.
4.5 Additional properties for shares A share and its join operation must satisfy the properties of a joinable type from section 4.4. In addition a share must have some additional
properties that are not always true for all separation algebras or separation logics:
8. Nonoverlapping: ∀πa, πb, πc. (πa ⊕ πb = πc ) ⇒ ¬identity πa ⇒
9. Splittability: there is a named total function split, which takes a
share and returns a pair of shares, and obeys the following rule:
These axioms are provided so that the user of CSL is able to develop more modular proofs. Property (8) gives the user a ﬁner ability to distinguish shares from one another6. Property (9) allows the user to develop proofs of modules without the need to handle a share that cannot be further split. Property (10), illustrated in the diagram above, guarantees a more subtle kind of splitting, and helps the user develop more modular proofs.
Properties (8)–(10) could probably be included in the deﬁnition of a joinable type instead of being guaranteed only for shares7. However, shares have two fundemental properties that distinguish them from
other joinable types:
11. Full share: ∃πf. ∀π. π ⊂ πf
12. Nontrivial: ∃π. ¬identity π The usefulness of this ability is discussed in section 4.6. Property (8) is similar in some ways to property (7) in that both in some sense constrain the existance of inverses, but the precise relationship of property (7) to property (8) is not fully clear.
That (8)–(10) are deﬁned only for shares, while (7) is deﬁned for all joinable types could very well be historical accident relating to how the proof was developed;
for some future work it might be useful to determine whether (8)–(10) should be moved to joinable, or perhaps whether (7) should be moved to shares.
4.6. SHARE MODELS Property (11) implies that shares have a partial order, with a (unique) top element, the full share. The partial ordering also guarantees the existence of a unique bottom element, the empty share8. Finally, property (12) guarantees that the system is nontrivial and completes the axiomitization. Accordingly, in our system, shares have properties (1)–(4) and (6)–(12)9.
Lifting joinability from shares to assertions. Given the above properties for shares, we can model the separating conjunction as a join relation in a more general way than Appel and Blazy. Two mapsπ π to assertions e → v and e → v separate if and only if π1 ⊥ π2. Two maps-to assertions about diﬀerent locations always join. The assertion emp is the identity element.