«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
129 (* See section 6.XX *) 131 Axiom step_allocpool: forall ge st st’, 132-134 (* See figure 5.8 *)
(lines 118–119); the other possibility (lines 104–111 and 120) is related to the C minor memory model and is covered in section 6.3.2.
The axiom step fun on lines 124–125 says that the step relation must be deterministic. This property is heavily used in both the CompCert compiler proofs and the soundness proofs of sequential separation logic developed by Appel and Blazy.
The axiom step not any younger is a technical axiom required by the model of resources, resource maps, and predicates, and will be explained in chapter 7.
6.3.2 Deﬁnitions and axioms for the C minor
Here we give a brief explanation of some deﬁnitions and axioms required by the CompCert memory model; Leroy et al. [LB08, Ler06] give a fuller explanation of the memory model and the reasons behind its design decisions.
The resource RESERVED is used to indicate memory locations that have not been allocated, but can be allocated in the future. The resource CT is used because C minor is byte-addressed; accordingly, since locks are four bytes long, the ﬁrst byte has resource LK and the next three have resource CT.
104 (* Required for CompCert memory model *) 105 Definition rmap_memory_model_rmap_ok (phi phi’:rmap) := 106 forall addr, 107 (phi @ addr = RESERVED phi pfullshare /\ 108 ((phi’ @ addr = VAL phi’ pfullshare) \/ 109 (phi’ @ addr = NO phi’))) \/ 110 (phi @ addr = VAL phi pfullshare /\ 111 phi’ @ addr = NO phi’).
131 Axiom step_allocpool: forall ge st st’, 132 step ge st st’ allocpool * TT) (filter ge st) allocpool * TT) (filter ge st’)).
The deﬁnition rmap memory model rmap ok on lines 104–111 gives two additional ways the resource map is able to change. In the ﬁrst, on lines 107–109, resource is allowed to change from RESERVED to VAL or NO; this happens when memory is allocated. In the second, on lines 110–111, resource is allowed to change from VAL to NO; this happens when memory is deallocated.
The axiom step allocpool on lines 131–134 is an elegant way of expressing that one never “runs out” of allocatable memory. Instead of expressing this fact directly, the axiom is deﬁned in terms of a predicate allocpool, which must be a satisﬁed by some portion of the resource map (TT is the predicate true). The deﬁnition of allocpool is both technical and not relevant to concurrency, and so we do not present it here.
CHAPTER 6. ENGINEERING ISOLATION 135 Inductive stepstar (ge:genv): state- state- Prop := 136 | stepstar_0: forall st, 137 stepstar ge st st 138 | stepstar_S: forall st1 st2 st3, 139 step ge st1 st2 stepstar ge st2 st3 stepstar ge st1 st3.
143 Inductive immed_safe (ge : genv) (st: state) : Prop := 144 | immed_safe_step: forall st’, 145 step ge st st’ immed_safe ge st 147 | immed_safe_rmap:
148... level of resource map is 0; see chapter 6... immed_safe ge st.
151 Definition safe (ge: genv) (st: state) : Prop := 152 forall st’, stepstar ge st st’ - immed_safe ge st’.
Figure 6.7: Basic deﬁnitions for Extensible Semantics 6.
3.3 Common deﬁnitions for core semantics Finally, there are some common deﬁnitions for all core semantics which are given in ﬁgure 6.7. stepstar is deﬁned in the standard inductive way to allow for ﬁnite composed applications of step. On lines 144–146, immed safe says that a state is immediately safe if it can take a step; on lines 147–149 there is an additional way to be immediately safe, which is if the “level” of the resource map in the state is 0; this is required for the model of resource maps and will be explained in chapter 7.
6.4 Building an extension Once we have a core language, such as the C minor of Appel and Blazy, we want to extend it, for example with concurrency primatives. By using a “bolt-on” model for extensions, we can ensure that changes to the core semantics do not aﬀect the extensions and vise versa.
6.4.1 Examples of extensions Here we discuss diﬀerent examples of extensions deﬁnable in our setting.
The null extension One very simple extension is the null extension, which is the extension that does not implement any functionality. In this case the combination of the core language and the extension is equivalent to just the core language.
The operating system extension A more complex extension is the simple operating system extension.
This extension implements three external functions: read, which gets input from the user; write, which sends output to the user; and exit, which terminates the program and returns control to the operating system.
CHAPTER 6. ENGINEERING ISOLATION The sequential sub-machine extension To deﬁne the semantics of Concurrent C minor we will build two diﬀerent concurrency extensions. In chapter 8, we will build a small extension called the sequential sub-machine extension that only knows how to execute the concurrent instructions make lock and free lock, getting stuck on lock, unlock, and fork. We will use this extension to build the concurrent operational semantics of Concurrent C minor.
The oracular concurrency extension Later, in chapter 9, we will build a more powerful extension using the concurrent operational semantics, called the oracular concurrency extension. That extension will be able to execute all ﬁve of the concurrent instructions, and we will use it to prove our CSL sound.
6.4.2 The EXTENSION module type An extension must satisfy the module type given in ﬁgure 6.8. Unlike the core, extensions are quite simple. There is a type oracle (in mathematical notation Ω), which acts as “private data” for the extension and is hidden from the core semantics. The oracle type must be inhabited, so we provide a witness, an oracle.
The point of an extension is to handle external function calls. However, any given extension need not handle all external functions; it is useful to be able to query the extension to determine which external functions it handles. The parameter handles gives an easy test for this.
6.4. BUILDING AN EXTENSION 155 Module Type EXTENSION.
156 Parameter oracle: Type.
157 Parameter an_oracle: oracle.
159 Parameter handles: external_function - bool.
161 Parameter consult: external_function oracle * world * predicate) option (oracle * world) - Prop.
165 Axiom consult_obeys_rmap: forall c o1 w1 P o2 w2, 166 consult c (o1, w1, P) (o2, w2) match (w1,w2) with ((_,_,rmap,m),(_,_,rmap’,m’)) = 168 forall addr, (readable (rmap @ addr) /\ 169 readable (rmap’ @ addr)) m addr = m’ addr)) 171 end.
173 (* Determinism *) 174 Axiom consult_fun: forall c a b1 b2, 175 consult c a b1 - consult c a b2 - b1=b2.
177 (* Required for model of resource maps *) 178 Axiom consult_not_any_younger:
179 (* See section 6.XX *) 181 (* Required for CompCert memory model *) 182 Axiom consult_allocpool: forall c ora w P ora’ w’, 183 consult c (ora, w, P) (Some (ora’, w’)) allocpool * TT) w allocpool * TT) w’).
187 End EXTENSION.
Figure 6.8: Interface for extension
ENGINEERING ISOLATION To actually handle the external function call, the extension provides a consult relation, which takes an external function (i.e. a natural number that encodes which function is being called), a tuple (Ω, w, P ), which are the arguments to the external call, and an option of tuple (Ω, w), which are the results.
In general, consult only modiﬁes world, since world is exactly the part of the state that is shared between all of the languages of the CompCert compiler. However, the extension is allowed to use some auxiliary private state in the oracle. In the operating system extension this would encapsulate the state of the operating system; in the oracular concurrency extension it encapsulates the state of the other threads.
The predicate P in the consult function is used to implement make lock. It would also be useful to implement an assert function that took a predicate instead of an expression.
Like step, the consult relation is partial and can get stuck. When consult returns None, the result is not that the consult failed, but that control never returns. Two examples of this result would be modeling the exit system call in the operating system extension and modeling the lock instruction, where e.g. the call can deadlock, in the oracular concurrency extension. When consult returns a new oracle and world, the world is passed back to the core semantics and the oracle is provided as a parameter on the next consult, thereby allowing the extension to use the oracle as shared state. In general the oracle is able to return a completely diﬀerent world (memory, resource map, etc.) than the one
6.5. GLUING A CORE AND EXTENSION TOGETHER it was given.
In addition, like the core semantics, an extension must satisfy a variety of axioms10. The key axiom is consult obeys rmap, which is given on lines 165–171. This axiom is somewhat diﬀerent from the one deﬁned for the core on lines 96–102 in ﬁgure 6.5. Instead, this one guarantees that as long as an address is readable both before and after consulting then the memory at that address is unchanged by the consult.
All of the other axioms are very similar to the ones given for the core in ﬁgures 6.5 and 6.6.
6.5 Gluing a core and extension together Once one has built a core semantics and an extension, one would like to glue them together to have a complete semantics. We deﬁne a functor Oraclize in Coq that takes two modules as arguments, the ﬁrst of module type EXTENSIBLE SEMANTICS, and the second of module type EXTENSION. This functor then builds a step relation of the following
The Coq implementation of the oracular step relation is in ﬁgure 6.9.
The oracular step has three cases. Case one is given on lines 4–8.
First, in line 5 we ensure that the state is not at an external function Just as with the core axioms, it has been shown in Coq that the concurrency extension meets these axioms, but it is unclear if other axioms are required as the proof is being re-engineered into this format.
CHAPTER 6. ENGINEERING ISOLATION Module Oraclize (Core: EXTENSIBLE_SEMANTICS) (Ext: EXTENSION).
1 Inductive oracle_step 2 (ge: genv) (ora1 : oracle) (st1 : state) 3 (ora2: oracle) (st2: state) : Prop := 4 | step_core:
5 at_external (snd (snd (from_state st1))) = None ora1 = ora2 - 7 step ge st1 st2 - 8 oracle_step ge ora1 st1 ora2 st2 9 | step_external_Some:
10 forall phi m core f vargs P rho’ rho’ core’, 11 st1 = to_state (phi, m, core) at_external core = Some (f,vargs,P) consult f (ora1,(snd ge,vargs,phi,m), P) 14 (Some (ora2,(_,rho’,phi’,m’))) after_external rho’ core = Some core’ st2 = to_state (phi’,m’,core’) oracle_step ge ora1 st1 ora2 st2 18 | step_external_None:
19 forall phi m core f vargs P, 20 st1 = to_state (phi, m, core) at_external core = Some (f,vargs,P) consult f (ora1,(snd ge,vargs,phi,m),P) None ora1 = ora2 - 24 st1 = st2 - 25 oracle_step ge ora1 st1 ora2 st2.
call; in this case line 6 ensures that the oracle is constant since the core semantics is not allowed to modify the it. On line 7, the core semantics steps, and on line 8 the parts are put back together.
Both cases two and three deal with external function calls. Case two is given on lines 9–17, and handles the case when the external function returns. We verify that the state is at an external function call on line
12. On lines 13–14, we consult the oracle using the extension. After consulting we reconstruct the state on lines 15–16, and on line 17 the parts are put back together.
Case three is given on lines 18–25 and handles the case when the external function never returns control. We verify that the state is at an external function call on line 21. On line 22, we consult the oracle using the extension, and receive None back as the return, indicating that the extension never releases control back to the core. In this case, the semantics loops around forever by setting the next state and oracle to be equal to the previous one on lines 23–24, and then putting the parts back together on line 25. Since the third case results in an inﬁnite loop, it is trivially safe.
Along with this deﬁnition, the Oracalize functor has a number of lemmas about the relation, which are proven from the axioms on the core and extension.
CHAPTER 6. ENGINEERING ISOLATION
6.6 Notation for the rest of the thesis We have now given an explanation of how to modularize an extensible semantics in Coq. To simplify the presentation in the rest of the thesis, we will do the following. First, we will assume that the core semantics is “hardwired” to the C minor of Appel and Blazy. The core semantics will have a step relation given by
Where a state σ is a pair of world w (that is, those parts of state that do not include program syntax: locals ρ, resource map φ, and memory m) and control κ (the parts of the state that do include program syntax).
Appel and Blazy deﬁne several diﬀerent controls, but for this presentation we only s · κ and Kstop, as deﬁned in chapter 5.
Second, we will pretend that the new concurrent statements make lock, free lock, lock, unlock, and fork are just normal statements added to sequential C minor, instead of extended function calls. These statements take values instead of expressions as parameters for simplicity.
Third, we will hide most of the modularization between core and extension. To build an extension, one constructs a partial function consult:
consult : program × oracle × state → option(oracle × state),
consultation, and an oracle Ω′ and state σ ′ are the optional output.