«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
We denote a thread list by θ, and the ith thread by θi. A concurrent state S is a tuple of schedule ℧, thread list θ, and memory m.
In ﬁgure 5.2 we present our erased concurrent step relation with seven cases.
The ﬁrst case, er-cstep-seq, covers running a sequential statement (including make lock and free lock). We select thread i, add the memory m, and run the sequential step relation; afterwards we put the thread back into place with new locals ρ′ and control κ′ and continue stepping with new memory m′. We do not change the schedule, and so do not context switch.
Figure 5.2: Erased concurrent step relation
ERASED CONCURRENT OPERATIONALSEMANTICS out of statements in a thread; in this case we switch to another thread by removing the head of the scheduler. We do not delete thread θi from θ, so threads never change position in line. If the thread is selected again, we will just context switch again.
The third case, er-cstep-prelock, covers what happens when a thread wants to start grabbing a lock. We move to the Klock v ctl state and context switch so that other threads have a chance to grab the lock.
The fourth case, er-cstep-nolock, covers the “spin” case of the spin lock. In the memory m lock value is 0, indicating that the lock is locked by some other thread. We context switch and keep waiting for the lock.
The ﬁfth case, er-step-lock, covers the case when we grab the lock.
In the memory m the lock has value 1, indicating that it is unlocked, and so we switch it to value 0, so that no other thread can grab the lock. At a lower level of the compiler this will become a test-and-set or compare-and-swap instruction, making the load from m and the store to m′ atomic at all intermediate compiler levels. We then transition to the runnable Krun κ state and start running the thread.
The sixth case, er-step-unlock, covers the case when we release a lock. In the memory m we test to make sure that the lock is currently locked, and then update it so that it is unlocked. We context switch after an unlock so that other threads can tell that we have released it.
The seventh case, er-step-fork, covers the case when we fork a child thread. In that case we add the new thread to the thread list and context switch so that it has a chance to run.
5.3. REASONABLENESS OF INTERLEAVING MODEL
5.3 Reasonableness of interleaving model Our semantics has a nonpreemptive thread model. We chose this concurrency model because a sequentially consistent interleaving model is inappropriate for our context.
Sequentially consistent interleaving is too weak because actual processors go beyond interleaving at every step. They have weak memory models, where instructions are dynamically reordered by the processor in a way that is sequentially undetectable. Unfortunately, in the context of concurrency, the weak memory models can change the behavior of a program and thereby cause particularly wicked bugs.
On the other hand, sequentially consistent interleaving models make us do more work than required. The key is that we are not considering all programs, but only programs that are data-race free, i.e., wellsynchronized and veriﬁable in CSL. For well-synchronized programs interleaving only at concurrent instructions is equivalent to full interleaving; this was the key idea behind Dijkstra’s invention of semaphores.
In fact, we interleave the minimum number of times that preserves the semantics of a full-interleaving semantics. For example, in case er-stepprelock, we context switch even if the lock was already unlocked to let the other threads have a chance to grab it.
In future work we plan to extend our proofs to cover weak memory models. However, it is a mistake to prove that code at the C minor level obeys weak memory models. Instead, we will preserve our “rarely interleaving” semantics all the way through the compiler until we reach
CHAPTER 5. ERASED CONCURRENT OPERATIONALSEMANTICS machine code; only then will we prove the correctness of our semantics for well-synchronized programs executing on a machine with a weak memory model.
5.4 Conclusion In chapter 3 we introduced Concurrent C minor. Here we gave Concurrent C minor a formal erased concurrent operational semantics. Our erased semantics is a reasonable model for conventional concurrency.
It is not easy to prove properties about our erased semantics. It is easier to reason about the unerased semantics deﬁned in chapter 8. In section 8.6 we prove an erasure theorem that says that the unerased semantics is a conservative approximation to the erased semantics given here. In chapter 9 we deﬁne an oracular semantics that is suitable for reasoning about one thread at a time. In chapter 10 we model our CSL on that oracular semantics, and prove that properties proved with the oracular semantics hold on the unerased concurrent operational semantics. The erasure theorem then guarantees that the properties hold on our erased semantics.
Chapter 6 Engineering Isolation In chapter 3 we presented the Concurrent C minor language and gave an example program in 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 the remainder of this thesis we will present a soundness proof of our Concurrent Separation Logic with respect to the operational semantics of Concurrent C minor. Since the soundness proof is developed in Coq it has aspects of both a mathematical proof and also an engineered software artifact. These aspects have inﬂuenced each other: part of the diﬃculty in developing the mathematical ideas was that they had to integrate cleanly into existing Coq proofs; conversely, at times the engineering process became too diﬃcult and new mathematical techniques had to be developed to simplify the engineering task.
In this chapter, we focus particularly on engineering design choices
that allow for greater modularity in the mechanized Coq proof1. The material in this chapter has not been fully integrated into our Coq development, which uses a somewhat less modular design; work is ongoing to bring the Coq development into closer agreement. In chapter 7, we will develop the modal substructural logic underlying CSL assertions.
In chapter 8 we will explain the operational semantics of Concurrent C minor. In chapter 9 we will introduce the oracle semantics for Concurrent C minor. Finally, in chapter 10, we will construct a modular proof of the soundness of Concurrent Separation Logic using the oracle semantics.
Note to readers uninterested in engineering a large proof in Coq. Readers who are largely uninterested in or unfamiliar with Coq engineering eﬀorts should read section 6.1, and then may skip this chapter until section 6.6, where we deﬁne the notation and brieﬂy cover the ideas we will use in the rest of the thesis.
Modules are an engineering technique that isolate parts of a software system from each other. By dividing up the system into isolated components, it becomes easier to understand, maintain, upgrade, and re-use.
In our work, we use modules to isolate the sequential and concurrent parts of the system from each other. In general, reasoning about sequential features or concurrent features is complicated enough; to reason This chapter has not been previously published.
6.1. MODULARIZATION GOALS about both simultaneously would be very diﬃcult. Also, if our isolation is strong enough, it will be easier to modify the CompCert compiler to compile Concurrent C minor since the existing sequential proofs will not have to be changed very much.
6.1.1 Core, glue, and extension
Languages like C minor have many complex features. At the level of syntax, adding new features is generally done by directly adding new statements into the set of statements already in the language. However, this is not very modular, as many proofs are done using case analysis, and all such proofs must be redone when new statements are added.
Moreover, the semantics of the new language cannot be directly built from the semantics of the old language.
Instead of directly mixing features, we design a “glue” interface layer that allows a core language to be extended with new features.
The glue combines the syntax and semantics of the core and extension to build a new language. The relationship between the core, glue, and extension is illustrated in ﬁgure 6.1. Since the glue isolates the core and extension from each other, the glue allows us to re-use proofs about the component parts as lemmas in proofs about the combined language.
CHAPTER 6. ENGINEERING ISOLATION
We will take as the core the C minor of Appel and Blazy [AB07] and as the extension a semantics of the concurrent statements make lock, free lock, lock, unlock, and fork. We glue these together to make Concurrent C minor.
6.1.2 Level independence A major goal of our Concurrent C minor project is to extend the correctness proofs of the CompCert compiler [Ler06] from the sequential
trated in table 6.1. From the source language of C minor to the target language of PowerPC, each sequential language is attached to some semantics of concurrency specialized to that language with its own language-dependent glue.
While this method would work, it would require much more substantial modiﬁcations to the CompCert compiler and correctness proofs than ideal, since the reasoning about the statements would have to be done diﬀerently for each intermediate language. This would also mean that a change to the new statements would require changing all of the proofs about the intermediate languages. One question is how well the glue isolates the core and extension from each other, and also how much the glue depends on the two of them.
Ideally, the core and extension could be so isolated from each other that each language could use the same extension to add new behavior, as illustrated in table 6.2. To do this, the new statements must ﬁt uniformly into all of the intermediate languages of the CompCert compiler.
While this does make the initial engineering work harder, the beneﬁt should be a substantially easier time modifying the compiler to handle new extensions2.
Since the compiler has not yet been modiﬁed, it is quite likely that some additional engineering work beyond what is presented in this chapter will be necessary for that process. In particular, there are concerns that the “oracle” used to build the concurrency extension is not fully level independent. Hopefully, however, this material will provide a good start in the proper direction.
CHAPTER 6. ENGINEERING ISOLATION
We now present an extension system which takes a “core” small-step semantics and extends with certain additional instructions. We will then use this extensible semantics to build Concurrent C minor on top of the C minor of Appel and Blazy[AB07], and then later use it again build an oracular semantics for Concurrent C minor.
6.2.1 Basic deﬁnitions All of the languages of the CompCert compiler share certain common deﬁnitions, including those given in ﬁgure 6.23.
Coq code shown in this chapter has been simpliﬁed for the presentation.
6.2. SHARED DEFINITIONS FOR GLUE 1 (* Definitions shared in all CompCert languages *) 3 (* Memory addresses *) 4 Definition addr := Z * Z 6 (* Identifiers *) 7 Definition ident := nat.
9 (* Values *) 10 Inductive val := 11 | Vundef: val 12 | Vint: int - val 13 | Vfloat: float - val 14 | Vptr: addr - val.
16 Definition globals := ident - option addr.
18 Definition locals := ident - option val.
20 (* Lines 21 - 53 are explained in section 5.2.2 *) 21 (* Permissions *) 22 Parameter resource : Type.
24 (* A map from address to permissions *) 25 Parameter rmap : Type.
26-53 (see figure 5.5) 55 Definition mem := address - val.
57 Definition world := 58 globals * locals * rmap * mem.
59 Definition predicate := world - Prop.
61 Definition ext_fun := ident.
Figure 6.2: Shared deﬁnitions in all CompCert languages
ENGINEERING ISOLATION Addresses are pairs of integers, which give a block and oﬀset; this allows for greater modularity in the compiler. Identiﬁers (names of variables) are natural numbers. There are four kinds of values: int, ﬂoat, pointer, and undeﬁned4. A mapping from identiﬁers to addresses allows global variables to be used.
Locals. Local variables are tricky to handle uniformly, since each CompCert language has its own representation. To allow reasoning to operate more smoothly with the languages at each level in the compiler, we deﬁne a level-independent deﬁnition of locals as a map from N to value. Then, each language’s glue will be responsible for converting its own private representation of local variables into the shared one when required.
Resource map. A resource map is a generalization of the footprint deﬁned by Appel and Blazy [AB07]. Recall from section 2.5.2 that a footprint is a map from addresses to permissions. For Appel and Blazy, a permission was simply a binary value, where true meant that memory access to that address was allowed and false meant that memory access was forbidden. In our setting, resource maps and permissions are more complex and are explained in section 6.2.2. Like the rest of the shared deﬁnitions, the model of resource maps does not depend on any particular program syntax, meaning that every language in CompCert can use the same deﬁnition.
that the same memory model is used for the source, target, and all intermediate languages. For this presentation we simplify the CompCert memory model so that memory is a map from addresses to values;
Leroy et al. [LB08, Ler06] explain the CompCert memory model in more detail.