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

The ﬁnal case, rule Ω-steps, is when control returns after running the other threads. In this case we project out the ith thread from the new concurrent machine state S ′′ and proceed with the new oracle, world, and control that came from running the concurrent machine.

rent machine itself requires classical reasoning to ﬁnd a world satisfying an unlock assertion because we allow users to use a classical logic, and second, determining whether control will return to a given thread reduces the halting problem. The nonconstructivity of our operational semantics is not a bug: we are not building an interpreter, we are building a speciﬁcation for correctness proofs of compilers and program logics.

As explained in section 6.6, we deﬁne the oraclular step relation using the consult relation. As explained in that section, the oracular step uses the underlying step relation (which is the step relation for sequential C minor) when executing core statements.

**We use the oracular step to keep “unimportant” details of the concurrent machine from interfering with proofs about the sequential language. The key features of the oracular step are the following:**

1. It is deterministic, which simpliﬁes sequential metatheory

2. When it encounters a synchonization operation, it is able to make progress with the oracle, whereas a regular step relation gets stuck

3. It composes with itself, whereas the regular step relation does not (because memory will change between steps due to other threads)

With these properties we can prove properties of the sequential features of Concurrent C minor in a natural way.

9.5 Conclusion In chapter 8 we gave Concurrent C minor a formal concurrent operational semantics. That semantics was easy to use for reasoning about the concurrent features of the language, but not natural to use for reasoning about sequential features. In this chapter we have deﬁned an oracular semantics for Concurrent C minor to support natural reasoning about sequential features.

We have not yet formally stated the precise relationship between the oracular semantics and the concurrent semantics. The oracular semantics is built from the concurrent semantics, but we wish to reason somewhat diﬀerently. The oracular semantics is a “thread-local” version of the semantics, so it is natural to think that if we could prove properties of each thread using the oracular semantics, then we could combine those proofs into a proof of the entire concurrent machine.

However, we are not yet in a position to formally state the connection, which will be the subject of section 10.3.

Chapter 10 A Modal Hoare Judgment and Oracular Soundness In chapter 3 we introduced Concurrent C minor. In chapter 4 we gave Concurrent C minor an axiomatic semantics, Concurrent Separation Logic. In chapter 8 we gave Concurrent C minor an operational semantics. At last we are ready to connect these two semantics by proving the soundness of the CSL axioms with respect to the operational semantics.

Our CSL axiomatic semantics is designed to reason about one thread at a time, and we noted in chapter 8 that the concurrent operational semantics was not particularly easy to use for reasoning about such sequential computation. In chapter 9 we developed an oracle semantics that presents a single-threaded view of the concurrent machine and is suitable for reasoning about one thread at a time.

We connect our axiomatic semantics to our operational semantics in

Here we develop the deﬁnition for the Hoare tuple. First, in section 10.1.1, we explain a simple continuation-passing deﬁnition in the style of Appel and Blazy [AB07]. Then in section 10.1.2 we explain why this style of deﬁnition will not allow us to embed predicates into program syntax as we wish to do for the make lock statement of Concurrent C minor. Finally, we show how to redeﬁne the Hoare tuple using our modal logic of chapter 7 and explain how the new deﬁnition allows us to embed predicates into program syntax.

10.1.1 A continuation-passing Hoare judgment Our semantic model for Hoare tuples is rooted in the idea of safety, deﬁned in ﬁgure 10.1. We start with the notion of immediately safe.

A state σ is immediately safe if it is not stuck; in other words, if it is safely halted or can take a step. A state can be safely halted in two Portions of this chapter have been published before as [HAZ08a] and [HAZ08b].

10.1. A MODAL HOARE JUDGMENT

ways. The ﬁrst, case isafe stop, is the standard way of saying that the machine has been safely halted when the code has reached the end of the computation. The second, case isafe level, is less standard. After we reach approximation level 0, we will no longer be able to age the resource maps; moreover, all of the stratiﬁed predicates are now unit and therefore no longer guarantee anything.

This does not mean that the program is now unsafe; it means that the program’s observer has stopped caring about the computation. We prove our programs sound starting with arbitrarily large amounts of stratiﬁcation. Therefore, our programs are proved sound with regard to any ﬁnite amount of time. If we wish to know that our program is safe

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

for 100 steps of computation, we stratify predicates to level 100 (we age the world at most once per step of computation). If we wish to know that our program is safe for 100 billion steps of computation, we stratify predicates to level 100 billion. The third way of being immediately safe, case isafe step, is the standard way of observing that if we can take a step then we are not stuck.We deﬁne the −→∗ relation in the usual way as the composition of the −→ relation with cases stepstar 0 and stepstar S. We then dene safe in the usual way: for any state σ ′ reachable from σ, σ ′ is immediately safe. Notice that we quantify universally over all initial oracles Ω; in section 9.3 we explained that quantifying over all oracles instead of simply valid ones is sound due to the Ω-invalid case of the oracular consult relation: if we get an invalid oracle we are safe if we try to consult it because we loop forever. The unrestricted universal quantiﬁcation simpliﬁes the proofs that do not use the oracle since it means that they do not have to carry around validity premises about the oracle, which would weaken the isolation between the sequential and concurrent reasoning.

Blazy. This is a simpler deﬁnition than the one they use, which supports the frame rule in a more semantic style, and has additional parameters to handle nonlocal exits from blocks and functions. Their rule was given

10.1. A MODAL HOARE JUDGMENT

** Figure 10.2: Na¨ continuation-passing style deﬁnition of Hoare tuple ıve in full in ﬁgure 2.**

5 in chapter 2. In the Coq development we include all of the features they describe to handle the nonlocal exits and semantic frame rule, but here we eliminate many of the more advanced features, which are for sequential control ﬂow, to concentrate on the key ideas.

Next, we deﬁne the Hoare tuple Γ ⊢ {P } c {Q}. For any sequence of instructions κ, if Γ ∗ Q guards κ then Γ ∗ P must guard the statement c followed by κ. We add the parameter Γ, which is the assertion that describes the functions, to both the pre- and postconditions as a convenience for the user, so that he does not have to write {Γ ∗ P } c {Γ ∗ Q}.

This is a continuation-passing style deﬁnition, and it may not be obvious at ﬁrst glance that it is equivalent to the informal notion of “if we start with a state that satisﬁes P, and we run s, and s terminates,

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

then we end with a state that satisﬁes Q”. It is equivalent because we are quantifying over all instruction sequences κ that are guarded by Q.For any property of Q that is checkable with our operational semantics, we can develop a small tester sequence that tests the property and gets stuck if it does not hold. If we are still concerned, it is easy to add a statement that asserts that the predicate Q holds and if it does not then gets stuck.

This deﬁnition is one of partial correctness; in other words it does not assume that the statement s will terminate. However, since it asserts that s · κ is safe if P holds, then it does imply that the statement s does not get stuck.

Using this deﬁnition, we can prove all of the sequential rules of separation logic except for the rule for call. In fact, as mentioned above, Appel and Blazy use a more complex version of this deﬁnition to prove all of the rules of sequential separation logic with respect to C minor in Coq. Unfortunately, in the current context, we cannot use the deﬁnition of the Hoare tuple given in ﬁgure 10.2 to prove the soundness

**of the function call CSL rule:**

The problem is that the program Ψ, used in function call to match a function name with a function body, is free in the deﬁnition of the Hoare rule. Obviously, a sound deﬁnition should not have any free variable;

10.1. A MODAL HOARE JUDGMENT unfortunately, ﬁxing the problem is not easy. One solution is to make Ψ a parameter of the Hoare tuple, an approach taken by Schirmer [Sch06]. However, this solution requires the CSL use to drag around his entire program through his correctness proofs, which is unfortunate, and makes function pointers more diﬃcult to use. Moreover, the user already is passing around a description of the functions in Γ—why should he also pass around the program Ψ?

We cannot simply quantify universally over the program Ψ; this makes the call rule easy to use—but impossible to prove, so it will not do. Another bad idea is to quantify existentially over the program Ψ;

this makes the call rule easy to prove—but impossible to use.

We are fast running out of options. Appel and Blazy put the program Ψ into the world w and let predicates judge program syntax.

However, in our context this solution is not good enough since we do not wish to put program syntax into worlds.

10.1.2 Embedding predicates into syntax We cannot put program syntax into the world due to the make lock l R statement. This statement takes a semantic predicate R—i.e., a function from world to Prop—that becomes the resource invariant of the new lock l. Thus, a predicate is embedded into program syntax.

Since program syntax is directly exposed to the user, we wish to provide a simple inductive deﬁnition for program syntax and avoid complex stratiﬁcation techniques. If we wish to avoid stratiﬁcation techniques,

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

then the deﬁnition for the type of “predicate” must come before the definition of program syntax. Since a predicate is a function from world to Prop, a world cannot contain program syntax, which is why a world is simply a tuple of locals ρ, resource map φ, and memory m.One very important predicate is f : {P }{Q}, i.e., “f is a function

deﬁnition of the Hoare tuple, there was no relation at all, since Ψ was a free variable.

As we discussed, we do not wish to provide Ψ as a parameter to the Hoare tuple. Instead, what we want to do is quantify over all “good” programs Ψ – that is programs compatible with Γ. The idea is to add an additional premise after a universal quantiﬁcation; this way we hope to have a deﬁnition that is both possible to use and possible to prove.

What we are looking for is some relation Γ ⊢ Ψ, called the believe relation, which says that the program Ψ is compatible with Γ. Compatible with Γ means that if there is an assertion f : {P }{Q} in Γ, then we can believe that assertion about the function body Ψ(f ).

Recall that we use ≈ to mean “we wish we could deﬁne things this way”. This deﬁnition says that for any program Ψ compatible with Γ, if Q guards κ, then P must guard c · κ.

What remains is to deﬁne the relation Γ ⊢ Ψ. The obvious choice is

In other words, for any function assertion that is part of Γ, the Hoare tuple guarantees that the body of that function has precondition P and postcondition Q.

Unfortunately, there is a problem with these deﬁnitions: the definition of the Hoare tuple depends on the believe relation, while the deﬁnition of the believe relation depends on the deﬁnition of the Hoare tuple. Worst of all, this dependence is contravariant, meaning that no solution exists, even in untyped set theory.

Fortunately, we have our modal logic from chapter 7, which was developed to handle just this kind of thorny contravariant recursive situation.

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

Although we originally developed it to model lock invariants, we can use it to deﬁne the Hoare tuple itself since the logic has powerful features such as impredicative quantiﬁcation and higher-order recursion.The Hoare tuple we explain here is much simpler than the one in

**the Coq development. The major simpliﬁcations include:**

1. No globals in the world type. As in chapter 7, we removed from the world type the map from global names to addresses.

2. No relation between function pre- and postconditions. As in chapter 7, we have removed the extra parameter that relates function pre- and postconditions to each other.

3. No marshaling of arguments. As explained in chapter 8, we have a method of marshaling arguments at function call so that our function preconditions can judge them. We omit this feature here for simplicity.