# «Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»

The simplest model for fractional permissions is a rational number in [0, 1]. A 0 means that neither reading nor writing are allowed; any nonzero means that reading is allowed; and a 1 gives permission to write—so permission for writing implies permission for reading. In this simple model, the join relation is addition if the total is less than or equal to 1, and two shares which sum to more than 1 do not join.

The existence of the unique identity element has been proven in Coq.

Just as with joinable types, in the Coq development, an uglier set of axoims than (8)–(12) is used. It has been proven in Coq that the presented axioms imply the ones used in the Coq development, with one minor exception: in the Coq development, the full and empty shares are explicitly constructed, instead of being shown to exist existentially. This explicit construction is useful for engineering purposes.

## CHAPTER 4. CONCURRENT SEPARATION LOGIC

As Parkinson explains in [Par05, ch. 5], this simple share model is not really suﬃcient for many applications. Among other problems, we cannot distinguish which half of the interval [0, 1] is owned because two shares both equal to the same rational number are indistinguishable.To model this ﬁner distinction, Parkinson proposed that a share be a subset of the natural numbers. The full share is then N, and the empty share the empty set. The join relation becomes the disjoint union operation10. Using this model, one can easily distinguish partial shares—two shares are equal only if the underlying sets are equal.

One drawback to using Parkinson’s model for our work is that it does not support the splitting axiom, since Parkinson allows ﬁnite subsets. The natural strategy for modifying Parkinson’s model to support the splitting axiom is to require that shares be inﬁnite subsets of the naturals. Unfortunately, inﬁnite subsets of the naturals do not support the intersection axiom, since the intersection of two inﬁnite sets can be ﬁnite.

One mathematically elegant solution is to deﬁne a share to be an equivalence class of sets of real numbers taken from the interval [0, 1], where two sets are in the same equivalence class if their symmetric diﬀerence has Lebesgue measure of 0. The join relation of two shares π1 and π2 is deﬁned as long as

If we write π to be the equivalence class containing S1 ∪ S2, then π1 ⊕ π2 = π. The join relation deﬁned in this way will have all of the desired properties.

The problem with this model is that although it is mathematically clean, it would require developing measure theory in Coq, which is a sizable amount of work. A somewhat mathematically uglier technique is to deﬁne a share as the disjoint union of half-open intervals (open at the top) with rational endpoints drawn from the set [0, 1), and to deﬁne the join operation as the disjoint union operation on sets. One advantage of this model is that it only uses the reals implicitly, since it manipulates only the rational endpoints. However, it still proved diﬃcult to implement in Coq11.

A third similar idea to use equivalence classes of reals where two sets are equivalent if their symmetric diﬀerence is countable. This is probably suﬃcient, but it was never implemented in Coq due to a general desire to avoid utilizing the real numbers unless absolutely necessary.

Using equivalence classes of naturals where two sets are equivalent if their symmetric diﬀerence is ﬁnite might also work, but has not been extensively developed.

Dockins [Doc08] developed a share model in which a share is modeled by a binary-tree data structure. Models developed from a computer science perspective are sometimes easier to model in Coq than models In fact, it was so painful that for most of the development time shares were simply inﬁnite subsets of the naturals, even though this meant that the intersection property was false.

## CHAPTER 4. CONCURRENT SEPARATION LOGIC

developed from a mathematical perspective. Dockins’s model satisﬁes all of our axioms, and is currently being used in the Coq development.To simplify the remainder of the presentation we will use the following convention. ◭◮ indicates the full share12, and ⊳⊲ indicates an empty share. Given a share π, we write ⌊π⌋ to indicate the “left half” of split(π) and ⌈π⌉ to indicate the “right half”; by the splitting rule, as long as π is not the empty share, then neither are ⌊π⌋ or ⌈π⌉. The left and right halves of the empty share are the empty share13 : ⌊⊳⊲⌋ = ⌈⊳⊲⌉ = ⊳⊲.

For the convienece of notation, we will write ◭⊲ for ⌊◭◮⌋ and ⊳◮ for ⌈◭◮⌉. Therefore,

associated with an assertion (in CSL) R, called the resource invariant of l. Just as with a maps-to assertion, we require that the share π be nonempty. A location cannot be both a normal memory cell and a lock. This restriction is enforced by not allowing a lock assertion and a

4.7.1 Resource invariants The resource invariant R of a lock l must hold before a thread can unlock the lock l, or the machine will get stuck. This means that the next thread to lock l will know that R holds. Locks are an exclusive form of access control, meaning that only one thread can hold a lock at a given time. Therefore, the thread that grabs the lock will know that no other thread will be able to touch the resource until the lock is unlocked again.

Resource invariants for locks must be closed to local variables, precise, and valid. An invariant R is closed to local variables when R does not depend on the values of the C minor locals. Since local variables are not usually shared in concurrency, this restriction is natural14.

An invariant R is precise when for all Q, the separating conjunction can only divide R ∗ Q in one way. An example of a precise predicate is a maps-to predicate. Requiring precision substantially simpliﬁes the reasoning and lets the system be deterministic15, and moreover is part of the standard presentation of CSL [O’H07].

The notion of validity is technical and will be deferred until chapter

7. However, in practice validity is not a diﬃcult requirement to satisfy On the other hand, Concurrent C minor can express the idea of memoryresident local variables, by permitting each function invocation to have a stackallocated memory block. Locations in these blocks can be addressed using load/store, and can be the subject of “maps-to” assertions. Stack-allocated addresses can be shared via the resource invariants of CSL. Before returning from a function, the thread must reclaim exclusive ownership of its stack block or the return command will get stuck.

It is unclear what kinds of trade-oﬀs are possible if one wishes to relax the precision requirement; Gotsman has recently been working in this area [Got08].

## CHAPTER 4. CONCURRENT SEPARATION LOGIC

because all the operators mentioned above as being exposed to the user, as well as all the operators presented in section 4.7 are valid.If an assertion R is closed, precise, and valid, then we say that R is tight. But how should we ensure that the user of our concurrent separation logic will always provide tight predicates? One choice is having side conditions, but this turns out to be annoying in the proofs. Instead, we utilize the new operators close, precisely, and validly. For all R, close R is closed, and moreover if R is closed, then close R = R. If R is not closed, then the meaning of the assertion close R depends on R and can be diﬃcult to predict; in many cases it becomes false. precisely R and validly R are deﬁned similarly with respect to precision and validity.

The formal deﬁnitions of close, precisely, and validly are technical and so are deferred until section 7.3.8.

**We deﬁne tightly as the composition of validly, close, and precisely:**

tightly R = validly (close (precisely R)). As expected, for all R, tightly R is tight, and tightly R = R if and only if R is tight16.

Using these deﬁnitions, it is possible to avoid stating explicit side conditions in the following way: when a lock with invariant R is unlocked, tightly R must hold; the next locking thread will then know tightly R holds after sucessfully acquiring the lock. If R is not tight, then the meaning of tightly R depends on R and is diﬃcult to predict.

Frequently it will be equal to false; in this case it will be impossible to The deﬁnition of tightly is somewhat subtle; for example, exchanging the order of the composition leads to a bad deﬁnition, because precision is a less orthogonal property than one might hope for.

4.7. NEW ASSERTIONS FOR CSL unlock the lock.

Partial ownership of a lock is suﬃcient to attempt to lock it. A thread that succeeds in locking a lock also gains the additional permission hold e R, which means that the expression e evaluates to a lock location l, with associated invariant R, and that the lock l is held by the thread in whose proof the hold assertion appears17.

The simplest way to guarantee that the permission hold e R is required to unlock e is to require that all lock invariants R satisfy the relation R = (hold e R)∗S for some additional assertion S. The simplest

**way to get this property is via the recursion operator µ:**

Because hold e R is always closed and precise, as long as S is closed and precise then (hold e R) ∗ S is as well. In other words, S is tight if and only if (hold e R)∗S is tight. One advantage of this approach is that lock invariants cannot be emp, a fact that is useful when establishing soundness18. See section 4.9.1 for a sample resource invariant created with the recursion µ operator.

Fractional ownership of the hold permission is possible, but does not seem to be very useful.

In fact, an alternative way of getting soundness is to do away with hold altogether, and simply to require that lock invariants be nonempty. The problem with allowing lock invariants to be empty is that it allows a thread to unlock a lock twice.

## CHAPTER 4. CONCURRENT SEPARATION LOGIC

**4.7.3 Functions**

We reason about ﬁrst-class functions with the assertion f : {P }{Q}, which means that the expression f evaluates to a function pointer that points to a function with precondition P and postcondition Q. A precondition P of a function is actually a map from function arguments e to an assertion; similarly, the postcondition Q is a map from the values returned by the function to an assertion19. To allow a function’s pre- and postconditions to be related to each other (e.g., function f returns an integer twice as large as its input), there is also an additional parameter for both P and Q. The ability to relate postconditions to preconditions is not so interesting for spawnable functions since the spawned functions never return to their parent. Therefore in this presentation we elide this extra parameter; see Appel and Blazy [AB07] for a discussion of how it is used for reasoning about sequential function call.

Since C minor separates the “data memory” from the “program memory,” functions do not have shares, and every function is visible to every thread20. A function can either be called (within the current thread) or spawned (as a new thread). We require that the preconditions of functions that will be spawned be precise. We enforce this requirement with the validly and precisely operators analogously to our use of tightly for lock invariants. This way it is simple to determine Our version of C minor supports multiple return values.

If one wished to verify self-modifying code, for example, functions would need shares.

4.8. CONCURRENT SEPARATION LOGIC HOARE RULES

One of the most important aspects of O’Hearn’s CSL is that it includes all of the rules of standard separation logic [O’H07]. Similarily, our CSL rules are a superset of the rules of Appel & Blazy presented in ﬁgure

2.6. Our new concurrent rules are presented in ﬁgure 4.1.

To use the make lock rule to reason about making a lock with invariant R at location e, full ownership of e is required. Moreover, that location must contain a 0; the operational semantics described in secCHAPTER 4. CONCURRENT SEPARATION LOGIC tion ?? will get stuck if these conditions are not met. Since a lock is considered to be locked when its location contains a 0, it is therefore created in the locked state, and the postcondition includes both the full ◭◮ visibility of the lock e ; R and the holding of the lock hold e R.

◭◮ Both e ; R and hold e R are required to reason about freeing a lock using the free lock rule. Since a thread can have a hold permission only if the lock is locked, this means that the location associated with the lock contains a 0.

To use the lock rule to reason about locking a lock e with associated invariant R, a thread needs to own some (typically partial) share π of e. After locking, the thread still has the same visibility of the lock as before, and in addition gains the assertion tightly R. If R is tight, then tightly R is equal to R.

The precondition for using the unlock rule for reasoning about unlocking a lock is tightly R. We also require as a side condition that the lock invariant R be equal to (hold e R) ∗ S for some S 21. Again, as long as R is tight (which is true if and only if S is tight) then the precondition is equal to R. If R is not tight, then tightly R is equal to false, meaning that the unlock statement cannot be proven to be safe using CSL.

The rule for fork is somewhat analogous to the rule for unlock. This is natural since in both cases resources are being transferred from the In the Coq development, this property is enforced not by a side condition but instead by using another operator like tightly; the presentation here is equivalent and cleaner.