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

Now that we have proved all of the rules of CSL sound with respect to the oracular semantics of Concurrent C minor, half of our soundness task is done. The other half, covered in the remainder of this chapter, is to connect the oracular semantics to the concurrent semantics, which we do with progress and preservation theorems.

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

Now we connect the oracular semantics to the concurrent semantics.

First we deﬁne the notion of concurrent safety in ﬁgure 10.5. We say that a concurrent machine state S is concurrently immediately safe (just referred to as immediately safe when the context is clear) in three situations.

First, case c isafe level, the concurrent machine is immediately safe if the resource maps inside it have approximation level 0. Recall that since all resource maps in S must join together due to the consistency

10.3. SOUNDNESS OF THE ORACULAR APPROACH requirements on S, all those resource maps must have the same approximation level, and therefore it is suﬃcient to test the level of the alloc pool. Just as in section 10.1.1, we only provide guarantees about correct behavior for an arbitrarily large but ﬁnite amount of time.

Second, case c isafe sched, the concurrent machine is immediately safe if the schedule is trying to pick a nonexistent thread. Since we quantify over all schedules we do not have to worry that some of the schedules we quantify over wish to pick nonexistent threads; we also quantify over all schedules that pick only existing threads.

Third, case c isafe step, the concurrent machine is immediately safe if it can take a step. That is, “immediately safe” means “not stuck”.

We deﬁne the =⇒∗ relation as the composition of the concurrent step relation in the usual way with cases cstepstar 0 and cstepstar S.

We deﬁne csafe in the usual way: for any state S ′ reachable from S, S ′ is immediately safe.

Our major goal will be to prove concurrent safety from oracular safety. Due to the nature of the concurrent step relation, concurrent safety is actually quite a strong property. Recall from section 8.5 that the cstep-unlock rule requires that a lock’s resource invariant be true before unlocking. This means that concurrent safety implies that all resource invariants are obeyed. Since outside programs can only communicate with a program via locks, this implies that all outside communication is done correctly.

vation theorem. As usual, the progress theorem will deﬁne an invariant suﬃcient to guarantee that the concurrent machine is not stuck and the preservation theorem will guarantee that the invariant is preserved as the machine computes.

In ﬁgure 10.6 we deﬁne the property safe-as i. Informally, a concurrent continuation (Ω, σ, κ) is safe-as i if, supposing it is the ith thread of the ˆ concurrent machine consistent with oracle Ω, then if this thread is ever ready to run then it will be oracularly safe. There are two cases: in the ﬁrst, case safe-as never, the thread will never again be selected to run sequential code again; in the second, case safe-as eventually, the thread

10.3. SOUNDNESS OF THE ORACULAR APPROACH will eventually be selected to run again, and when it is selected, it will be safe. Recall that to be safe we must quantify over all oracles, so we do not need to worry about the actual oracle Ω′.

We deﬁne Ψ ⊢ all-threads-safe(S) to mean that each projection of S will be oracularly safe the next time it is ready and selected. Together with the consistency requirements on the concurrent machine state as explained in section 8.4, this is enough to prove progress.

Theorem 10.4 (Progress). If Ψ ⊢ all-threads-safe(S), then S is immediately safe.

Proof. Part of taking a step in the concurrent machine is proving that the next concurrent machine has the consistency property. More than half of the diﬃculty in the theorem is proving consistency of the next concurrent machine state. These properties would normally be proved in the preservation theorem, but due to the use of dependent types to guarantee consistency part of the preservation theorem is proved in the progress theorem.

By case analysis on the thread whose thread-id is at the head of the schedule. The initial case is on the concurrent control of the thread.

2. The concurrent control is Krun κ, so the thread is runnable.

We have two cases. Since thread i is at the head of the schedule, we know Ψ ⊢ StepOthers i S S. By allthreads-safe we know safe-as i, where i is the thread at the head of the schedule; there are two possibilities, but we know that it cannot be safe-as never, since thread i is ready to run. Therefore it must be safe-as eventually, and thread i must be oracularly safe. If it is safe because the thread has reached Kstop then we execute cstep-texit. Otherwise, the thread must be able to take

**an oracular step. There are three possibilities:**

10.3.2 Preservation The preservation theorem is more complex due to the existence of forks, since we need to know that the child will be safe if its precondition is satisﬁed. To guarantee that the child will be safe, we require an additional invariant, all-funs-spawnable, given in ﬁgure 10.7.

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

First we deﬁne the predicate version of the rkind function, prkind, which maps resources to resource kinds. Recall from section 8.4.6 that rkind is useful as an antecedent with unrestricted (dangerous) implication, and we will use prkind here for this purpose. Ifthen φ @ l has resource kind k.

Then we deﬁne Ψ ⊢ all-funs-spawnable(S). Recall that for any concurrent machine state S there exists a total resource map φT that is the join of all of the resource maps in S. all-funs-spawnable states that there exists a predicate Γ that is compatible with the program Ψ and that for any location f with kind kFUN, there exists a precondition P and postcondition Q such that

and that Γ implies, i.e. all the functions in φT are contained in Γ.

Together this means that all of the functions in Ψ are conservatively approximated by their pre- and postconditions in Γ. We use the prkind construction and quantify existentially instead of universally over the precondition P and postcondition Q here for the same reason as in

The predicate Γ is constructed by the user using the rules of CSL as explained in section 10.2.2.

** Lemma 10.1.**

If Ψ ⊢ all-funs-spawnable(S), and Ψ ⊢ S =⇒ S ′, then Ψ ⊢ all-funs-spawnable(S ′ ).

Proof. Proved by case analysis on the step relation.

In all cases except for cstep-seq, the total resource map φT does not change except perhaps becoming more approximate (resources are transfered from one part of the machine to another, but this does not change the total resource map).

In step cstep-seq, the total resource map does not get larger or add new functions. The use of rkind ensures that our use of “dangerous” implication is sound even as the total resource map becomes more approximate in much the same

** Lemma 10.2.**

If Ψ ⊢ all-threads-safe(S), Ψ ⊢ all-funs-spawnable(S), and Ψ ⊢ S =⇒ S ′, then Ψ ⊢ all-threads-safe(S ′ ).

Proof. There are three basic cases. The ﬁrst is that we need to show that the thread that was just selected and run is As of the writing of this thesis, the Coq proof of the preservation theorem is currently broken due to maintenence and cleaning elsewhere in the system, particularlly related to the function pool φfp ; however everything here claimed to be proved in Coq has been proved in Coq at one time.

## CHAPTER 10. A MODAL HOARE JUDGMENT AND

## ORACULAR SOUNDNESS

still safe. The second is that we need need to show that one of the threads that was not selected is still safe. The third only occurs with the fork rule, and it is when we need to show that the new child thread is safe.Theorem 10.5 (Preservation). If Ψ ⊢ all-threads-safe(S), Ψ ⊢ all-funs-spawnable(S), and Ψ ⊢ S =⇒ S ′, then Ψ ⊢ all-threads-safe(S ′ ) and Ψ ⊢ all-funs-spawnable(S ′ ).

Proof. By lemmas 10.1 and 10.2.

10.3.3 Safety Now that we have both the progress and preservation theorems, we are ready to prove concurrent safety from oracular safety.

Theorem 10.6 (Safety). If Ψ ⊢ all-threads-safe(S) and Ψ ⊢ all-funs-spawnable(S), then Ψ ⊢ csafe S.

Proof. By induction on the =⇒∗ relation and the progress and preservation theorems.

We are nearly done. Recall that a program in Concurrent C minor begins with a call to a special main function.

Corollary 10.1. For any schedule ℧ and arbitrary stratiﬁ

By the deﬁnition of the Hoare tuple we can prove the initial call to the main function safe on any world that satisﬁes its precondition.

**Therefore we have the following theorem, expressed as a deductive rule:**

then the unerased concurrent machine state (℧, θ :: nil, L0, φmp, φfp, m) is safe.

Proof. Proved from corollary 10.1.

How hard will this theorem be for the CSL user to use? Premise 1 is developed by the user using the rules of CSL as explained in section 10.2.2. Premise 2 is simple: a function pool of arbitrary stratiﬁcation can be built from Γ by the user. Premise 3 is simple: an alloc pool of arbitrary stratiﬁcation can be built. Premise 4 is simple: the empty lock pool is easy to construct. Premise 5 is simple as long as the user does not forget the main function. Premise 6 is simple; the single thread is easy to construct. The diﬃculty of premise 7 depends entirely on how diﬃcult the user wishes to make the precondition of main to satisfy; we point out that emp is very easy to satisfy.

Therefore, we have shown that if a user proves his program sound with CSL, then assuming that his main function’s precondition is satisable his program will be safe when run on the concurrent machine. Our only remaing task is to connect to the erased concurrent operational semantics from chapter 5.

Note: No parallel decomposition lemma. Unlike in previous work [Bro07], we do not require a parallel decomposition lemma. We can avoid such a lemma because

1. We put resource maps into the concurrent operational semantics.

2. In the progress lemma we prove that the next state obeys the consistency requirements, which guarantees that the threads have disjoint resource maps.

3. In the store operation in the sequential semantics we get stuck if we try to write to memory we do not own.

4. We prove the safety of the parent in the CSL fork rule.

5. We prove the safety of the child in the preservation lemma.

In previous semantics the parallel decomposition lemma was a source

In chapter 3 we introduced Concurrent C minor. In chapter 4 we gave Concurrent C minor an axiomatic semantics, Concurrent Separation Logic, and in chapter 8 we gave Concurrent C minor an operational semantics. We have now proved our logic sound with respect to our operational semantics.

Chapter 11

**Conclusions and FutureWork**

We have proved the soundness of a sophisticated Concurrent Separation Logic with ﬁrst-class locks and threads with respect to the concurrent operational semantics of Concurrent C minor. Our soundness proof is largely implemented in Coq in a highly modular way, so that the actions of other threads do not complicate the parts of the soundness proof about sequential features and the complexities of sequential control ﬂow do not complicate the parts of the proof about the concurrent features. Moreover, we have a strategy for applying our techniques to the CompCert certiﬁed compiler, so that in the future we will be able to have an end-to-end result: proved properties of concurrent source programs will be true of the code that executes on the machine.

In chapter 3 we presented the Concurrent C minor language and

gave an example program in section 3.2. Then in chapter 4 we developed a new concurrent separation logic and demonstrated its power by using it to verify an example program. In chapter 5 we gave Concurrent C minor a formal erased concurrent operational semantics.

In chapter 6 we presented engineering techniques that allow for signiﬁcant modularization, particularly in the context of a compiler with multiple intermediate languages.

In chapter 7 we developed a new modal substructural logic and showed how to reason about complex parts of the underlying model by reasoning in the logic.

In chapter 8 we developed an unerased concurrent operational semantics that was easier to reason about than the erased concurrent operational semantics from chapter 5. We proved an erasure theorem that showed that the unerased semantics was a conservative approximation to the erased semantics.

The concurrent operational semantics of chapter 8 was not easy to use for reasoning about the sequential features of the Concurrent C minor language, so in chapter 9 we developed a thread-local oracle semantics for it.

Finally, in chapter 10 we developed a new modal Hoare tuple using the oracle semantics and showed how to use it to prove the rules of CSL sound. We also showed how to combine results from the oracular semantics into a result on the concurrent semantics with a progress and preservation lemma, thereby proving the soundness of Concurrent