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

Using this partial function, one deﬁnes the oracular step with three cases as given in ﬁgure 6.10. The ﬁrst case covers the situation when the core semantics is stepping. The second case covers when the oracle is taking control for an extended statement, but eventually returning control to the core. The third case is for when the extension does not return control to the core semantics, and therefore the program enters an inﬁnite loop. For our work, the third case is only used when a deadlock occurs during the execution of a lock statement.

Chapter 7 A Modal Substructural Logic In chapter 4 we deﬁned Concurrent Separation Logic, and in sections 6.2.1–6.2.2 we axiomatized resource and rmap and explained that the assertions of CSL were modeled as predicates.

In section 7.1 we explain the diﬃculties in providing a model for CSL assertions. In section 7.2 we explain the stratiﬁcation technique that allows us to provide a sound deﬁnition for resources and resource maps. Finally, in section 7.3 we explain how to use a modal logic to reason cleanly about the underlying model and deﬁne the assertions of CSL1.

Portions of this chapter have been published before as [HAZ08a], [HAZ08b], [DAH08], and [BDH+ 08].

7.1 Modelling diﬃculties In section 6.2.1 we explained that a predicate is a function from a tuple of globals, locals, resource map, and memory to a proposition in the Calculus of Co-Inductive Constructions (Coq’s Prop). Though the ability to judge globals is important for developing proofs in CSL, modeling assertions about them is not diﬃcult, so for the rest of this chapter, we elide globals to simplify the presentation; we also elide issues related to the C minor memory model outlined in section 6.3.2.

In section 6.2.1, it was also explained that neither resource maps nor memories depend on the syntax of programs and so can be used with any CompCert language, which further justiﬁes using them whenever possible to express invariants in the soundness proof.

7.1.1 Semantic vs. Syntactic There are two basic approaches to programming language research. The ﬁrst, more common today, is syntactic, where objects are uninterpreted symbols and are deﬁned by judgements showing how they are to be used. The second, which is the approach we have taken, is semantic, where objects are given formal deﬁnitions and judgements showing how they should be used are proved from those deﬁnitions as lemmas.

We initially chose to give a semantic deﬁnition for our separation logic—instead of deﬁning it syntactically and proving soundness via metaproofs—for three reasons. First, semantic systems are more exMODELLING DIFFICULTIES tensible than syntactic ones. It is easy to deﬁne a new assertion, and unless the underlying semantics of the language must be changed to accomodate that assertion, all of the previously proved facts still hold automatically. Therefore in section 6.2.1 we were able to give a subset of the assertions of our CSL, including “maps-to” e → v and “is a lock π with invariant R” e ; R, without worrying that we were leaving anything out. If a user decides we have left out a useful assertion, he can deﬁne it himself.

Second, after examining the Princeton Foundational Proof-Carrying Code (FPCC) project [App01] we found evidence that semantic methods scaled better than syntactic ones in large, machine-checked, realistic systems [BDH+ 08].

Third, we had more experience with semantic methods in the context of a large project. Partially as a result of this experience, we ﬁnd semantic proofs more natural than syntactic ones, and easier to construct.

Fourth, although we do not have any hard evidence for this opinion, we believe that semantic methods are less brittle than syntactic proofs when confronted with the kinds of engineering changes common in a large project.

The recursive nature of ﬁrst-class locks makes them very diﬃcult to model semantically since it is easy to slip into Cantor’s paradox. We

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

want a model that is something like the one in ﬁgure 7.1, where + and × are the sum and product type constructors and we write ≈ to mean “we wish we could deﬁne things this way”.

The idea is that a resource can either be NO, which indicates that the location cannot be used, or YES, which indicates that the resource can be used in some way. A YES resource takes a kind, which can be one of three choices: kVAL, which indicates that the location contains data; kLK, which indicates that the location is a lock; and kFUN, which indicates that the location contains a function. A YES resource also takes an pshare and list(predicate). As explained in section 6.2.2, a pshare is a nonempty share as deﬁned in section 4.5. The “high-level” resource pseudoconstructors VAL, LK, and FUN are deﬁned in terms of YES.

An rmap associates every location in memory with a resource. As explained in section 6.2.1, locals, rmap, and mem are bundled together into a world. A predicate then is a function from world to Prop.

In both cases, there is a contravariant occurrence of resource within its own deﬁnition. In other words, the cardinality of resource is strictly larger than the cardinality of resource, a contradiction even in untyped set theory. Thus these deﬁnitions are unsound.

7.1.3 From mutable references to lock invariants To provide a sound deﬁnition we adapt techniques developed for modeling mutable references in the FPCC project [AAV03, Ahm04]. It was surprising to us that the semantics of mutable references were relevant to the semantics of ﬁrst-class locks. However, reading from a mutable reference is similar to locking a lock, in the sense that both actions are a way of getting information from the outside world. Analogously, storing to a mutable reference is similar to unlocking a lock, in the sense that both actions are a way of notifying the outside world of a change of state.

The indexed model developed for modelling mutable references in FPCC was extremely diﬃcult to explain and very complex to use. It was developed in higher-order logic (HOL) encoded in the Twelf theorem prover; limitations on the expressiveness of HOL required extensive, very heavyweight G¨delization techniques to deﬁne the model and prove o it sound, resulting in more than 20,000 lines of proof for this part of the model alone. Also, the underlying model was exposed to the rest of the proof of the type system in various unpleasant ways.

to create a modal model. This model was deﬁned and proved sound in Coq in approximately 1,000 lines. The enormous diﬀerence in size is due to a combination of several factors: ﬁrst, substantial redesign of the deﬁnitions and better proof techniques; second, the natural diﬀerence

7.2 A substructural modal model The sketch of the modal substructural model given in ﬁgure 7.2 is divided into three parts. The ﬁrst section shows how we provide a sound deﬁnition in the presence of contravariance in a way that preserves impredicativity. The second section shows how dependent types can hide the stratiﬁcation in the underlying model. The third section gives some deﬁnitions that are useful when translating the dependent model into the underlying stratiﬁed model2.

◦ model. We use = to mean that the deﬁnition is opaque to the rest of For further details of the stratiﬁcation and soundness of the construction we refer to Appel et al. [AMRV07] and Richards [Ric08]; both refer to the 1,000 line Coq development cited earlier. Appel [App08] has also illustrated some of the modiﬁcations required to support substructural reasoning.

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

the proof; that is, the rest of the proof knows that the deﬁnition exists, but is not able to “look inside” and see the details of the deﬁnition. We use = to mean that the deﬁnition is completely public, and that the rest of the proof is able to use it directly.

There are a number of diﬀerences between the presentation here

**and the Coq development. The most important ones are these:**

1. Here predicates judge only locals, resource maps, and memory;

as explained in section 6.2.1, in the Coq development, predicates also judge globals.

2. Here we ignore issues related to byte addressability. In the Coq development, we must handle this issue. In particular, we need to ensure that the ﬁrst byte of a lock cannot be separated from the following three bytes. We do this by maintaining validity predicates about valid resource maps.

3. As explained in section 4.7.3, in the presentation we do not support the relation of function preconditions to function postconditions; i.e., we do not have a way of expressing that a call to an increment function returns a value exactly one larger than its parameter. In the actual Coq development, both our CSL and the underlying model support this additional expressiveness. In the model this is done by parameterizing predicate lists over an additional type and value parameter.

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

4. Here we use the → type constructor to construct the types of rmapn and rmap. In the Coq development we use a quasifunctor called Joinmap that helps preserve certain separation properties.

5. Our presentation here is less modular than the Coq development.

6. It is nontrivial to produce deﬁnitions that will be acceptable to the Coq theorem prover from the deﬁnitions as given in the presentation, largely due to the heavy use of dependent types in the model. In appendix A we give a very compact Coq development that implements the core ideas presented in ﬁgure 7.2; this miniature development should help a reader who wishes to understand (or build) a larger Coq implementation. In the real Coq development, the entire modal substructural model has been completely deﬁned and proved sound.

7.2.1 An impredicative stratiﬁed model The idea is that we will stratify predicates, resources, and rmaps; we write predicaten to mean a predicate at level n, resourcen to mean a resource at level n, and rmapn to mean a resource map at level n.

To ensure a well-founded construction, we deﬁne predicate0 as unit.

A resource at level n is only allowed to contain predicates of level n;

similarly, a resource map at level n is a map from address to resourcen.

As discussed in section 6.2.1, we bundle locals, resourcen, and memory together into a worldn. A predicate at level n + 1 is a pair of predicaten

7.2. A SUBSTRUCTURAL MODAL MODEL and a map from worldn to Prop. Thus, a predicate at level n+1 contains a list of predicates for all levels between n and 0, in addition to the map

**from worldn to Prop. As an example, consider n = 3:**

predicate3 = (unit × (world1 → Prop)) × (world2 → Prop).

We deﬁne predicaten as a pair because it lets us deﬁne “aging” the predicate in section 7.2.4 in a relatively simple way.

By stratifying in this manner we make the deﬁnitions well-deﬁned.

The stratiﬁed construction was one of the major technical accomplishments of the indexed model for mutable references that Ahmed et. al [AAV03, Ahm04] developed for the FPCC project.

One major advantage of this construction over previous models [AM01, AAV02] is that it supports impredicative quantiﬁcation. That is, since the result type of predicaten is Prop (as opposed to, e.g., some kind of stratiﬁed Propn ), it is possible to deﬁne universal and existential quantiﬁers for predicaten that can quantify over all of the types in Coq, even including predicaten. This is much stronger and more useful than predicative quantiﬁcation, where a predicaten could at most quantify over predicaten−1.

One major drawback in the model developed for FPCC is that the

resourcen, worldn, and rmapn, indicating that the rest of the proof cannot see the underlying stratiﬁcation.

7.2.2 Dependent types to hide stratiﬁcation The second section in ﬁgure 7.2 contains one of the major insights in the modal model of Appel et. al [AMRV07], namely the ability to hid the underlying indexes in the model from the rest of the proof by using dependent types. Explicit reasoning about the indexes can therefore be contained to a small part of the overall soundness proof.

We use both sum (Σ) and product (Π) dependent types in our definitions. An element s : Σα. (β : α → Type) is a dependent pair, written s = {a : α, b : β(a)}, where the type of the second component depends on the value of the ﬁrst component3.

An element f : Πα. (β : α → Type) is a dependent function f = λa : α.(b a) : β(a), where b : α → β(a). Thus, the type of the function’s result depends on the value of the function’s parameter. One way to interpret this is that the Π type operator deﬁnes a family of related types, indexed by the value.

Using the Σ dependent type constructor, we are able to deﬁne resource as a dependent pair of a natural n and a stratiﬁed resourcen at level n. Similarily, we deﬁne rmap as a dependent pair of a natural n and a stratiﬁed rmapn at level n. These deﬁnitions elegantly hide the underlying stratiﬁcation by bundling it into a dependent pair, and are To express a normal pair we use the typical notation (a, b); the notation {a, b} is reserved to indicate the presence of dependent types.

7.2. A SUBSTRUCTURAL MODAL MODEL the deﬁnitions axiomatized in section 6.2.2. Finally, predicate is deﬁned as was promised in section 6.2.1, as a function from a pair of rmap and mem to Prop.