«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
7.3.1 Assertions in the modal substructural logic An assertion in the modal substructural logic is just a predicate. Accordingly one deﬁnes it by giving a function from world to Prop. We say that a world w forces a predicate P, written
Since our assertions are just functions from world to Prop, we have what is called a shallow embedding of our modal substructural logic in Coq. This would not be the case if we deﬁned our own proposition language (calling it, e.g., nuProp) and used it instead of Coq’s Prop.
The shallow embedding signiﬁcantly simpliﬁes the process of creating the machine-checked proofs. We are able to use tactics developed for Prop with our predicates; for example, we can use the destruct tactic to break apart the conjunction in our modal logic. Also, we are able to use Coq’s native variable-binding mechanisms, thereby avoiding the binder issues raised in the POPLmark quagmire [ABF+ 05].
Almost all of our assertions are public in the sense that the remainder of the proof can see and use the deﬁnitions to reason about the underlying model. One exception is the deﬁnition of higher-order recursion operator µHO, which is opaque; the rest of the proof is given fold-unfold rules to reason about that operator as explained in section 7.3.9.
In the rest of this chapter we will give a selection of operators in our logic, explain their use, and provide their models.
7.3.2 Logical operators In ﬁgure 7.5 we give some basic logical operators and their models.
that we avoid variable capture.
[·]Coq useful because it ensures that the entire expressive power of Coq is available in the logic. The simplest use of [·]Coq is to deﬁne the predicates true and false8. We will see a more powerful use of [·]Coq when we deﬁne the precisely operator in section 7.3.8.
One of the advantages of our approach is that it is easy to deﬁne new operators in terms of old ones; we have done this in the deﬁnitions of true and false. Although both are predicates—that is, functions from world to Prop—their deﬁnition does not contain a λ; instead they utilize the λ in [·]Coq.
To avoid “symbol explosion” in the presentation, we overload many symbols to operate both at the Prop and predicate levels. Since the two have diﬀerent types in Coq, only one will be possible in any given context.
CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC Conjunction ∧ and disjunction ∨ are deﬁned by lifting the operations deﬁned on Prop. We also lift the universal and existential quantiﬁers ∀ and ∃. Since we use the quantiﬁers at the Prop level in the deﬁnitions of universal and existential quantiﬁcation in our logic, we have full impredicative quantiﬁcation: v can thus range over values, predicates, worlds, shares, and any other types deﬁnable in Coq.
We deﬁne the operator exactly so that we can precisely specify the resource map if we wish; exactly is not particularly useful in the CSL correctness proofs of programs, but is used in both the soundness proofs and in deﬁning the concurrent operational semantics in chapter 8.
7.3.3 Modal operators In ﬁgure 7.6 we give some modal operators and their models9. Recall that a world is a tuple of locals ρ, resource map φ, and memory m. The modal operators enable us to reason cleanly and orthogonally about these elements.
The simplest modal operator is close, which is used to remove the eﬀect of the locals ρ on a predicate’s behavior by universally quantifying over them. Thus, for any predicate P, close P ignores the locals ρ. If P already ignores ρ, then close P = P and we say that P is closed.
fashionably P, written P. In previous work [AMRV07] approximately was called later, and for this reason the Coq development refers to this operator as later. Each quantiﬁes over the resource map φ in a diﬀerent way. Unlike with the locals ρ, we cannot simply use universal quantiﬁcation over all possible φ, since the underlying model does not allow a stratiﬁed resource map φn to say anything meaningful about stratiﬁed resource maps φn+m+1 of higher stratiﬁcation.
While a stratiﬁed resource map φn cannot say anything meaningful about resource maps of higher stratiﬁcation, it can describe properties of resource maps of lesser stratiﬁcation φn−m−1. This was the underlying
CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC idea behind the approximation operator agen deﬁned in section 7.2.4.
The ⊲ P operator models the central idea of that section as a modal operator. If (ρ, φ, m) |= ⊲ P, then P may or may not hold on (ρ, φ, m), but will hold on all φ′ strictly more approximate than φ: (ρ, φ′, m) |= P.
Since all that is required for close P = P is that P not depend on local variables, it is natural to wonder which P have the property that ⊲ P = P. Due to the irreﬂexivity of age (n + 1), ⊲ P = P is a very strong requirement; in fact
This makes sense, since the most approximate predicate—that is, the one that gives the least information—is true. The essentially irreﬂexive nature of the ⊲ operator was a key technical insight of the modal model of Appel et al. [AMRV07], and we will see its expressive power when we see how to invert YES in section 7.3.10.
In the modal logic, ⊲ serves two purposes. The ﬁrst is to give a compact characterization of approximation, which it does very well.
The second is somewhat diﬀerent; it is to restrict the “wildness” of terms in the underlying stratiﬁed model. There is a natural idea that if w |= P, and if w ′ is a more approximate version of w, then w ′ |= P.
In informal terms, if w is “good enough” to guarantee P, then if w
7.3. REASONING ABOUT THE MODEL WITH A MODALSUBSTRUCTURAL LOGIC becomes a little more approximate, it should be even easier for it to guarantee P. Reformulated in the modal logic, we would very much like our P to have the property that
This will be true as long as φ has level greater than 5, but false as φ nears level 0.
The modal operator necessarily P, written P, forces predicates to be necessary. In ﬁgure 7.6 we give two equivalent deﬁntions for P.
The second deﬁnition of in ﬁgure 7.6 shows that it is very similar to a reﬂexive version of ⊲, and leads naturally to the proof that for all P,
is not particularly restrictive; P is necessary as long as it does not try to expose the underlying stratiﬁed construction. In fact, almost all of the operators presented here are necessary automatically, or become necessary when applied to necessary predicates. Therefore, as long as we build our CSL proofs using the operators presented here, we can ignore the existence of unnecessary predicates. One major exception is that implication is not automatically necessary even when applied to necessary predicates; this is discussed in section 7.3.7.
The modal operator fashionably P, written P, quantiﬁes over the φ in the world in a diﬀerent way. While ⊲ P and P were primarily concerned with reasoning about the underlying stratiﬁed construction, P is used to force P to ignore φ, similar to the way that close P is used to force P to ignore ρ.
Unlike in close P, where we quantify over all possible ρ, in P we cannot quantify over all possible φ, since resource maps of level n are not able to say anything meaningful about resource maps of level n+ m+ 1.
7.3. REASONING ABOUT THE MODEL WITH A MODALSUBSTRUCTURAL LOGIC Accordingly, we quantify over all resource maps of the same level; this is the strongest meaningful quantiﬁcation possible. Put another way, P is only allowed to utilize one fact about the resource map φ, which is its level. If we want to quantify over all resource maps at this level of
We use the modal operator everywhere P, written !P, to quantify over the memory m. The deﬁnitions of !P and close P are similar, since the memory m is similar to the locals ρ in the sense that neither has a particularly complicated structure that interferes with the model. If a predicate P ignores the memory, then
and we say that P is ubiquitous. Just as there are many closed predicates, there are many ubiquitous ones.
7.3.4 Substructural operators In ﬁgure 7.7 we give three basic substructural operators and their models. The assertion emp holds if the resource map φ only contains NO resources. Recall from section 7.2.6 that NO takes a resource map φ as a parameter and creates a resource stratiﬁed to the same level as φ, which it packages up into a dependent pair. Since a predicate is a function from world, we can use the resource map contained in the world.
Figure 7.7: Models of substructural assertions YES φ k π P at location l and NO elsewhere.
YES then creates a list of predicates stratiﬁed to level φ; we will take advantage of this in section 7.3.10 when we express what can be concluded from
The requirement that all other locations are NO is standard for separation logic; larger structures are built with the separating conjunction.
Since we have deﬁned our join relations as a stratiﬁed separation algebra, we model the separating conjunction P ∗ Q in a way similar to Calcagno et al. [COY07]. When
Using the separating conjunction it is possible to describe complex substructural properties of the underlying model in an elegant way.
7.3.5 Reasoning in the modal substructural logic The motivation for deﬁning the modal substructural logic is that we have found it much easier to reason about the model using the logic than to reason on the underlying model directly. The proofs of the soundness of CSL can become very complicated, and it is not unusual to have 50 or more premises leading to a goal. In that context, it is vital to be able to express properties concisely in order to reason about them with minimal mental overhead.
One advantage of using our logic is that we can prove a large number of lemmas describing how the logic behaves; a small subset of them are pictured in ﬁgure 7.8. Most of the lemmas take the form of equalities in the logic, which is quite convenient since we can use powerful rewrite tactics in Coq.
A very useful strategy we used while developing the soundness proof was to express the premises and goal of a lemma in the logic, and then use the kinds of rules given in ﬁgure 7.8 to prove the goal from the hypothesis. Sometimes it was not possible complete the proof entirely in the logic, in which case we had two choices: to deﬁne a new logic
CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC
Figure 7.8: Rules for reasoning in the modal substructural logic
3. REASONING ABOUT THE MODEL WITH A MODALSUBSTRUCTURAL LOGIC operator to express the property and then continue to reason in the logic, or to dip brieﬂy out of the logic and reason instead directly on the underlying model. The choice made depended on the diﬃculty of proving the underlying fact and a guess as to the amount of use the new operator would have. Dockins et al. [DAH08] discuss this in more detail.
To give an example of reasoning in the modal logic, we prove that
Of course, this can be proved directly on the underlying model, but the details and multiple quantiﬁers can quickly overwhelm an understanding of what is going on, particularly in the context of a larger proof, leading to a considerably longer and more frusterating proving experience.
7.3. REASONING ABOUT THE MODEL WITH A MODALSUBSTRUCTURAL LOGIC 7.3.6 Modelling the assertions of Concurrent
is kLK. The share π is projected into the right half of the full share in the style of the isomorphism noted by Parkinson [Par05]. In our share models there is an isomorphism between any two nonempty shares, and project uses that isomorphism to squeeze π into ◭⊲. For example,
Finally, we put the lock invariant R into the predicate list.
The hold l R assertion is deﬁned quite similarly to the lock assertion,
CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC
resource map contains a YES at location f whose kind is kFUN. The share is ◭◮, and the predicate list contains the pre- and postconditions P and Q.
7.3.7 Logical Implication Almost all of our operators are suitable for use in a CSL proof about programs. However, there are a few operators that we do recommend avoiding in that context, particularly full logical implication, which
7.3. REASONING ABOUT THE MODEL WITH A MODALSUBSTRUCTURAL LOGIC interacts complexly with the underlying stratiﬁed model, and which was conspicuously missing from the basic logical operators deﬁned in ﬁgure 7.5. We deﬁne four related implication operators in ﬁgure 7.10;
the ﬁrst two are dangerous in the sense that if not used carefully they will expose wild predicates in the underlying model.
Of course nothing prevents the use of the dangerous forms of implication; since the system is semantic instead of syntactic, an end-user can utilize any operator he wishes. However, full implication can be more diﬃcult to use than expected, and so we recommend that CSL proofs avoid it. Full implication is largely used in the soundness proofs of the model itself, indicating that it can be useful in carefully controlled situations. For most situations, however, we reccomend the use of the safer, more restricted forms of implication given in the second part of ﬁgure 7.10.