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

11.1. STATE OF THE COQ DEVELOPMENT Separation Logic with respect to the concurrent operational semantics of Concurrent C minor.

11.1 State of the Coq Development As we have indicated in the text, the Coq development is incomplete.

**The tasks that remain are:**

1. Integrate the cleaner deﬁnitions for joinable types and shares that were presented in chapter 4.

2. Add the function pool to the concurrent machine state. We are attempting to develop a better solution to the problem of global and immutable data in separation logic, and since the function pool is a bit of a hack we have held oﬀ implementing it in Coq until we can study the other alternatives in more detail.

3. Finish the modularization work presented in chapter 6. We have been modularizing the proof incrementally.

4. Do clean-ups as noted in the text.

5. Finish the proof of the CSL unlock rule.

6. Finish the preservation proof.

We developed a slogan when working on the proof, which was “As expected, it took longer than expected.” We also agree with the obserCHAPTER 11. CONCLUSIONS AND FUTURE WORK vation of Leroy, who noted that “Building [proof] scripts is surprisingly addictive, in a videogame kind of way” [Ler06].

One of the major beneﬁts of the project has been that it has a number

**of promising tasks for future work. These include:**

1. Modifying the CompCert compiler to handle concurrency. Our plan is to create an oracle semantics for each intermediate language of the compiler by applying our extension and then update the correctness proofs to show that the compiler preserves the behavior of each oracular semantics.

2. Developing techniques to reason about lock-free algorithms of various kinds. In practice, many of the concurrent algorithms used do not use locks, instead relying on various lock-free techniques such as atomic loads and stores. One goal is to see how we can apply our oracle semantics towards reasoning about these kinds of algorithms.

3. Reasoning in the presence of weak memory models. Modern processors execute memory accesses out of program order in a way

4. Exposing implication to end-user by improving dependent/stratiﬁed model. Because users of Hoare logics are accustomed to having full implication, it would be useful to be able to improve our assertion models to expose full implication to the CSL user.

5. Developing techniques to better reason about globals and shared immutable data in separation logic. We had a suprisingly diﬃcult time creating global values. We added the function pool to solve this problem, but we want to design a more elegant technique.

11.3 Concluding thoughts We have developed a soundness proof for a powerful new Concurrent Separation Logic with ﬁrst-class locks and threads. Along the way, we developed a modal substructural logic; designed a new style of concurrent operational semantics that did bookkeeping to guarantee behavior;

designed a new oracle semantics that presented a thread-local view of a concurrent machine and that allowed for the re-use of metaproofs of sequential language features; and provided a new modal deﬁnition of the Hoare tuple. Our Coq proofs have been almost completed, giving a high degree of assurance, and are designed to support the modiﬁcation of the CompCert compiler, thereby supporting the goal of providing an end-to-end guarantee about the behavior of concurrent programs.

Appendix A A Miniature Model in Coq A.1 Headers (* Aquinas Hobor *) Require Import List.

Parameter address : Type.

Parameter value : Type.

Parameter share : Type.

Parameter kind : Type.

Definition memory : Type := address - value.

A.2 Stratiﬁed Model Section Stratified_Model.

**Inductive res_n’ (inv : Type) : Type :=**

| NO’ | YES’: kind - share - (list inv) - res_n’ inv.

**Definition rmap_n’ (inv : Type) : Type :=**

address - res_n’ inv.

**Fixpoint inv_n (n: nat) : Type :=**

match n with | O = unit | S n = ((inv_n n) * (rmap_n’ (inv_n n) * memory - Prop))%type end.

**Definition res_n (n: nat) : Type :=**

res_n’ (inv_n n).

**Definition rmap_n (n: nat) : Type :=**

rmap_n’ (inv_n n).

A.3 Dependent Model Section Dependent_Model.

**Inductive resource’ : Type :=**

res_Level : forall (n : nat), res_n n - resource’.

Definition resource := resource’.

**Inductive rmap’ : Type :=**

rm_Level : forall (n : nat), rmap_n n - rmap’.

Definition rmap := rmap’.

Definition predicate : Type := (rmap * memory) - Prop.

End Dependent_Model.

## APPENDIX A. A MINIATURE MODEL IN COQ

A.4 Private deﬁnitions relating public toSection Private_Defs.

**Definition level (rm: rmap) : nat :=**

match rm with rm_Level n _ = n end.

**Fixpoint stratify (n : nat) (P : predicate) : inv_n n :=**

match n as n return inv_n n with | O = tt

End Private_Defs.

A.5. PUBLIC INTERFACE TO ACQUIRE RESOURCE A.5 Public interface to acquire resource Section Public_Interface.

**Definition resource_at (rm: rmap) (addr: address) : resource :=**

match rm with rm_Level n rm_n = res_Level n (rm_n addr) end.

**Definition NO (rm: rmap) : resource :=**

res_Level (level rm) (NO’ (inv_n (level rm))).

Definition YES (rm: rmap)

Lemma. The unlock rule of CSL is sound.

Proof. As discussed in section 10.2.3, we ﬁrst need to show that the precondition of the CSL lock rule guarantees that the concurrent step relation will not be stuck in cases Ω-diverges and Ω-steps. The precondition of the lock rule is tightly R, and in addition we have the fact that R = (hold e R ∗ S). We need to show that these guarantee that we can take a step with the cstep-unlock rule of the concurrent machine. We are guaranteed that we are at the head of the scheduler by the StepOthers relation, which handles the ﬁrst premise. Since we know tightly R, and R = (hold e R ∗ S), we know tightly (hold e R ∗ S). Since hold is tight, we know hold e R. By the consistency requirements on the concurrent machine state, if this permission is in a thread’s resource

map, the lock must be locked, so m(e) must be equal to 0, which handles the second premise. The third premise, involving the new memory m′ is true by construction. The forth premise, which says that we can split oﬀ a world φlock from φ, is always true, although in most cases φlock is not uniquely determined. The sixth premise, which is that we have hold e R, has already been demonstrated. The seventh premise, which is that tightly R holds on the resource map φlock, is guaranteed since it held on the resource map φ. Moreover, since all tight predicates are precise, this guarantees that φlock is unique. The eigth premise, which is that we can add the newly unlocked lock to the lock pool, is true by constrction and because we can prove that it was not in the lock pool before, since due to the consistency requirements lock pools can only hold unlocked locks and prior to this point the lock was locked. The nineth premise, the construction of new thread list, is true by construction. The tenth premise, that we can context switch, is true because as long as we have remaining stratiﬁcation levels we can context switch, and if we had run out of stratiﬁcation levels then we would have been immediately safe. Now that we have proved all of the premises to the cstep-unlock rule, we must prove that the new concurrent machine state S’ is consistent. From section 8.4 we must prove six properties. First, we must show that there exists a new total resource map. The lock rule does not add or remove from the total resource map, instead simply

of stratiﬁcation this is possible to do. Second, we must show that the scheduler is still longer than the remaining stratiﬁcation; since context switch removes exactly one item from the scheduler and ages the worlds exactly once this is simple. Third, we must prove that if any threads are waiting on a memory location then that location is a lock. Since we have not modiﬁed any of the other threads, and are not waiting on a lock ourselves, and have not freed any locks, this is simple. Fourth, we must have a well-formed alloc pool; since we have not changed it this is trivial. Fifth, we must have a well-formed function pool; since we have not changed it this is trivial. Sixth and last, we must show that we still have a well formed lock pool. As discussed, the property P3 behaves correctly as the world ages; since we have not touched any of the other locks in the lock pool, and the consistency requirements on the concurrent machine state ensures that the newly unlocked lock’s memory locations do not overlap with any previously unlocked lock’s memory locations, all of the other locks in the lock pool are still sound. For the lock we are unlocking, we need to show that there exists a lock invariant for it—but this is easy, since we have that as a premise—and that the invariant holds tightly on the lock’s resource map; however this is just premise seven from the cstep-unlock rule. Therefore, we have a consistant machine state and so are able to take a step with the cstep-unlock rule. Now we have to prove the postcondition of the rule. Fortunately

does return control, case Ω-steps, we need only satisfy the postcondition of emp, and since we have given away our precondition by putting it into the lock pool, it is easy to satisfy.

Lemma. The child resulting from the fork is safe-as i.

Proof. By all-funs-spawnable, we know that there exists a Γ which believe can connect to the program Ψ. By the precondition to the cstep-fork rule, we know f : {validly precisely P }{Q} for some precondition P and postcondition Q. Since this implies that rkind(φT @ f ) = Some kFUN, by the second half of all-funs-spawnable we know that there exists some (possibly diﬀerent) precondition P ′ and postcontcondition Q′ such that f : {P ′ }{Q′ } and Γ ⊂ true ∗ f : {P ′}{Q′ }. By YES inversion we know that ⊲ validly precisely P = ⊲ P ′. By the deﬁnition of believe, we know ⊲ Htuple(Γ, P ′, Ψ(f ), Q′). By the precondition to the

rule, we will have P ′ and Htuple(Γ, P ′, Ψ(f ), Q′ ). By the deﬁnition of Htuple and since we have believe Htuple Γ Ψ, by fold-unfold we know

By the cstep-fork rule, the child will be started with initial control1 call f · Kstop and an initial world satisfying ⊲ validly precisely P, i.e., P ′. The key action of the call statement is to step from this control to the control Ψ(f ) · Kstop. Since the function pool φfp is passed into each function as it runs, and since the function pool contains all of the functions in Γ, at the time when the thread is running we will know Γ∗P ′. By the deﬁnition of pguard, we will thus know psafe Ψ Ψ(f )·Kstop, which means that the child is safe-as i.

We remove the function arguments for simplicity.

Bibliography [AAV02] Amal Ahmed, Andrew W. Appel, and Roberto Virga. A stratiﬁed semantics of general references embeddable in higher-order logic. In 17th Annual IEEE Symp. on Logic in Computer Science, pages 75–86, June 2002.

[AAV03] Amal Ahmed, Andrew W. Appel, and Roberto Virga. An indexed model of impredicative polymorphism and mutable references. http://www.cs.princeton.edu/~appel/papers/ impred.pdf, January 2003.

[AB07] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step C minor. In 20th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2007), 2007.

[ABF+ 05] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoﬀrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the

[Ahm04] Amal J. Ahmed. Semantics of Types for Mutable State.

PhD thesis, Princeton University, Princeton, NJ, November

2004. Tech Report TR-713-04.

[AM01] Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657–683, September 2001.

[App01] Andrew W. Appel. Foundational proof-carrying code. In Symp. on Logic in Computer Science (LICS ’01), pages 247–258. IEEE, 2001.

[App08] Andrew W. Appel. A core resource calculus for higher-order separation logics. unpublished manuscript, 2008.

[BCOP05] Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. Permission accounting in separation logic. In POPL ’05: 32nd ACM Symp. on Principles of Programming Languages, pages 259–270, 2005.

[BDH+ 08] C. J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, and David Walker. Comparing semantic and syntactic methods in mechanized proof frameworks. In Proceedings of the 2nd International Workshop on Proof-Carrying Code (PCC 2008), 2008.

[Boy03] J. Boyland. Checking interference with fractional permissions. In Static Analysis: 10th International Symposium, pages 55–72, 2003.

[Bro07] Stephen Brookes. A semantics for concurrent separation logic. Theoretical Computer Science, 375(1):227–270, May 2007.

[COY07] Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. Local action and abstract separation logic. In LICS 2007 IEEE Symposium on Logic in Computer Science, 2007.