«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
In contrast, almost all of the other cases of the concurrent step relation do context switch. The context switch relation, CSwitch (S) = S ′, handles all of the details of performing a context switch by removing the head of the schedule (thus allowing the next thread to execute) and aging all of the worlds.
Thread exit (cstep-texit) does not remove the thread from the list, but scheduling a terminated thread simply results in a context switch.
As explained in chapter 4, we do not reason about the resources that threads free (or fail to free) on termination, so we do not place any restrictions on φ.
Figure 8.4 contains the portion of the step relation that is responsible for executing the fully-concurrent statements.
Three rules describe lock acquisition. Rule cstep-prelock checks to make sure that the location that the thread is attempting to lock is a lock in the thread’s resource map and then changes the thread’s status from runnable (Krun) to waiting on a lock (Klock). Finally, cstep-prelock context switches to give other threads a chance to grab the lock ﬁrst.
Rule cstep-nolock is the “block” case of a blocking lock—we try to grab the lock, but it is not yet available. In this case we simply context switch.
the resource map of the thread. By the restrictions on the lock pool contained in the consistant machine state, this resource map satisﬁes the lock’s resource invariant4. Rule cstep-lock does not context switch after grabbing the lock. If we wished to context switch here it would not be diﬃcult to modify our proofs; however it is unnecessary (since we quantify over all schedulers) and so we do not do it. See section 5.3 for a further discussion of interleaving.
The cstep-unlock rule reverses the lock rule. It ﬂips the memory location associated with the lock from a 0 to a 1 and puts the resource map associated with the lock φlock into the lock pool L. It is able to uniquely identify this resource map due to the premise
since tightly P is tight, and therefore precise. Since P is an arbitrary predicate in (classical) logic, this premise makes our semantics nonconstructive, i.e., noncomputable. See section 8.6 for further discussion of why this abstraction is reasonable.
In the Coq development we use a diﬀerent premise, (ρ, φlock, m) |= ⊲ tightly P, The invariant is satisﬁed on all more approximate resource maps due to the way YES inversion works. To establish that it holds at the current level of approximation is impossible in the general case, but in the case that actually occurs in the proof of the lock rule of CSL, a complex induction is able to prove that it holds immediately.
Perhaps a modiﬁcation of this rule would somehow lead to a simpler proof of the CSL lock rule.
CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICSwhich is related to the ⊲ discussed in 8.4.6. When we remove the ⊲ there we can simultaneously remove the ⊲ in the cstep-unlock rule.
Finally, cstep-fork creates a new thread. Because we spawn functioncalls as opposed to arbitrary commands that might have free C-minor variables, we don’t need complex side-conditions on free variables and
can use the empty environment ρ0 in the new thread. There is a nonconstructive test that the function’s precondition is satisﬁed:
(marshal(v), φchild, m) |= validly precisely P.
In this test the parameters of the function call are marshaled into a local environment ρ so that the predicate will be able to judge them. Like the unlock rule, this test is nonconstructive. The sequential semantics does not need such a test at every function call; we need it here to know what world is transferred by the (precise) predicate P that is the function’s precondition. Preconditions of nonspawnable (ordinary) functions need not be precise.
8.6 Reasonableness of the step relation Our semantics has two features that are unusual in a concurrent semantics. The ﬁrst unusual feature, exhibited in the cstep-seq and cstep-lock rules, is that the semantics does not interleave at every instruction. We discussed this feature in section 5.3.
tests in the cstep-unlock and cstep-fork rules. If we are executing a program for which we have a proof in CSL, then we can prove that the test will always succeed. However, the presence of these nonconstructive tests is unsatisfying. More generally, the presence of resource maps in the semantics is worrying: we need to verify that they are not allowing unrealistic behavior. We can defend both the nonconstructive tests and the presence of resource maps in the semantics by relating our semantics to the erased semantics deﬁned in chapter 5.
The erased machine deﬁned in chapter 5 is similar to the unerased machine deﬁned in this chapter; the diﬀerence is that in the erased machine all of the resource maps have been removed. The unerased machine is actually a conservative approximation to the erased one, as
demonstrated by the erasure theorem:
Theorem (Erasure). If Ψ ⊢ (℧, θ, L, φmp, φfp, m) =⇒
Proof. By case analysis on the =⇒ relation. We observe that each case in that relation has a corrosponding case in the =⇒e relation with a subset of the premises. In each case the schedule, locals (inside a thread), concurrent controls (inside a thread), thread list (up to erasure), and memory are identical. For the cstep-seq case we use lemma 8.2.
This is a useful sanity check: the real machine takes no decisions
CHAPTER 8. CONCURRENT OPERATIONAL SEMANTICSbased on erasable information; the erased semantics simply gets stuck less often.
When to erase. One could imagine proving safety of a concurrent program with respect to the unerased semantics, then erasing, and last compiling. However, this would be a mistake since the compiler may do concurrency-unsafe optimizations. Instead, we should preserve the resource maps in the semantics of each intermediate representation as we compile from Concurrent C minor to machine language; this gives the compiler a speciﬁcation of concurrency-safe optimizations. After we have reached machine language, we can use the resource maps to prove that our interleaving model is sound for machines with weak memory models. We erase last.
We have now given a formal concurrent operational semantics for Concurrent C minor. This semantics isolates the behavior of the sequential step relation from the concurrent reasoning, making it easy to use to reason about concurrent features such as locking a lock. However, it is not a major goal to use our operational semantics to reason about the sequential features of Concurrent C minor. To do so we deﬁne an oracular semantics for Concurrent C minor in chapter 9.
Chapter 9 Oracle Semantics In chapter 3 we introduced Concurrent C minor, and in chapter 8 we gave it a formal concurrent operational semantics. That semantics allows for natural reasoning about the fully concurrent operations of Concurrent C minor, such as lock and unlock. However, it does not allow for natural reasoning about the sequential language features such as control ﬂow. In this chapter we deﬁne an oracular semantics for Concurrent C minor that is ideal for reasoning about sequential language features in the context of a concurrent program1.
A compiler, or a Hoare tuple, considers a single thread at a time. The compiler (and its correctness proof) wants to compile code uniformly even around the concurrent operations. Similarly, in a CSL proof, the Portions of this chapter have been published before as [HAZ08a] and [HAZ08b].
may contain concurrent operations, but, because of C minor’s nonlocal exits, a soundness proof for the sequence rule of separation logic is complicated even without the headaches of concurrency. We want a semantics of single-threaded computation in a concurrent context.
The sequential submachine of section 8.2 is single-threaded but incomplete because it gets stuck at the fully-concurrent operations lock, unlock, and fork. What we want is a deterministic sequential operational semantics2 that knows how to handle concurrent communications, which it will do by consulting an oracle.
The correctness proofs of the CompCert compiler and the sequential separation logic proofs use determinism to simplify their task.
9.1. WHY AN ORACULAR SEMANTICS Figure 9.1 demonstrates the value of this type of semantics. In the left column is a sequence of statements in Concurrent C minor. The ﬁrst two statements are sequential statements, the third is a fully-concurrent lock statement, and the ﬁnal statement is sequential. In the middle column is a series of states σ (i.e., memory, locals, etc.) from a sequential semantics such as the sequential submachine; the series starts with some initial state σ0. In the right column is a series of oracle Ω and state σ pairs for a new oracular semantics; we start with the same state σ0 as in the regular sequential semantics, as well as some intitial oracle Ω0.
As each statement is executed, the states in the middle and right columns are updated by the action of the statement. After executing the ﬁrst statement, which is a store to memory, in the middle column we have a new state σ1. In the right column, we get exactly the same state σ1. Since a store instruction is not a concurrent instruction, we do not use the oracle and so it is unchanged. Assuming that the substatements s1 and s2 do not contain concurrent instructions, we reach the subsequent state σ2.
Now we reach a concurrent statement, lock. Here, the standard sequential semantics is stuck; the sequential submachine is not able to determine the result of the lock instruction, since it depends on the other threads. However, on the right-hand side, the semantics is able to take advantage of the oracle Ω0. The oracle represents all of the other threads in the concurrent machine. The right-hand semantics consults the oracle, which predicts what the state σ3 will be after the concurrent
CHAPTER 9. ORACLE SEMANTICS machine executes the lock instruction, and also produces a new oracle Ω1, which will be usable for the next concurrent instruction. After the concurrent instruction, the right-hand side is able to continue to process sequential statements as before.
To build the desired semantics we will build an oracular machine using our extension system explained in chapter 6. Our extension will handle all of the concurrent instructions of Concurrent C minor.
Like any extension, we must deﬁne the type of an oracle and build a partial function consult. When we constructed the sequential submachine in section 8.2, we used the unit oracle. Here, we deﬁne a more
meaningful oracle as follows:
thread number i, we ﬁrst split the alloc and function pools from the resource map φ, leaving the remaining resource map φt. The predicate allocpool is precise, and the function pool contains all of the functions and nothing more, so splitting them oﬀ is deterministic. Next we can
9.3 Concurrent consult relation We need to build a consult relation to execute the concurrent statements of Concurrent C minor. The consult function constructs a concurrent machine S from the oracle and then runs the other theads in that machine until control returns.
We run the other threads with the StepOthers relation, deﬁned in ﬁgure 9.3. The StepOthers relation takes a thread-ID i and two concurrent machine states S and S ′. We say that thread i is ready when i is at the head of the schedule in S. When we step other threads we have two choices. The ﬁrst case, SO-done, says that if thread i is ready, then we have ﬁnished stepping other threads and control has returned to thread i. The second case, SO-step, says that if thread i is not ready, then we take a step in the concurrent machine and then test again.
when the oracular machine wants to consult.
In the ﬁrst case, Ω-invalid, there is no concurrent machine state S compatible with the concurrent continuation. This happens if the oracle Ω is somehow incompatible with the world w. There are a variety of ways that this could be the case; one simple example is that one of the threads inside the oracle thinks that it has full ownership of a location that is also owned by the world w. Of course, in the concurrent machine this is forbidden by the consistency requirements.
It our proofs it is convienent to quantify universally over all oracles, instead of of simply quantifying over valid oracles, which would require an additional premise in the deﬁnitions and proofs. By looping safely if
CHAPTER 9. ORACLE SEMANTICS we are handed an invalid oracle by the universal quantiﬁcation, we can gracefully handle invalid oracles without requiring such a premise. By returning None from the consult function we indicate that the semantics should loop endlessly, thereby trivially becoming safe.
In the remaining two cases, we are able to construct a concurrent machine S, and take at least one concurrent step. This step uses the cstep-seq case in the concurrent step relation to execute a make lock or free lock, uses cstep-prelock to execute the ﬁrst part of a lock, uses cstep-unlock to execute an unlock, or uses cstep-fork to execute a fork.
After taking this step, the machine decides (classically) whether control will return to the current thread by branching on the StepOthers judgement. Rule Ω-diverges handles the case when control does not return, for example if the schedule is unfair, if another thread executes an illegal instruction, or if the current thread is deadlocked. In these cases the oracle machine loops endlessly, thereby becoming trivially safe. The idea that we are safe if another thread blows up may seem strange: the point is that we are proving the safety of this thread. If another thread causes the concurrent machine to get stuck, it is not this thread’s fault.