SharedMemory: update book text

SharedMemory.v

@@ -125,7 +125,7 @@ Example two_increments := two_increments_thread || two_increments_thread.
 
 (* Next, we do one of our standard boring (and slow; sorry!) model-checking
  * proofs, where tactics explore the finite state space for us. *)
-(*Theorem two_increments_ok :
+Theorem two_increments_ok :
   invariantFor (trsys_of $0 {} two_increments)
                (fun p => let '(_, _, c) := p in
                          notAboutToFail c = true).
@@ -153,7 +153,7 @@ Proof.
 
   simplify.
   propositional; subst; equality.
-Qed.*)
+Qed.
 
 (* Notice how every step of the process needs to consider all possibilities of
  * threads that could run next, which, in general, gives us state spaces of size
@@ -364,7 +364,7 @@ Qed.
 
 (* Now watch as we verify that last example in fewer steps, with a smaller
  * invariant! *)
-(*Theorem two_increments_ok_again :
+Theorem two_increments_ok_again :
   invariantFor (trsys_of $0 {} two_increments)
                (fun p => let '(_, _, c) := p in
                          notAboutToFail c = true).
@@ -387,7 +387,7 @@ Proof.
 
   simplify.
   propositional; subst; equality.
-Qed.*)
+Qed.
 
 
 (** * Optimization #2: partial-order reduction *)
@@ -417,7 +417,7 @@ Example independent_threads :=
 
 (* Unfortunately, our existing model-checker does in fact follow the
  * "exponential" strategy to build the state space. *)
-(*Theorem independent_threads_ok :
+Theorem independent_threads_ok :
   invariantFor (trsys_of $0 {} independent_threads)
                (fun p => let '(_, _, c) := p in
                          notAboutToFail c = true).
@@ -437,7 +437,7 @@ Proof.
 
   simplify.
   propositional; subst; equality.
-Qed.*)
+Qed.
 
 (* It turns out that we can actually do model-checking where at each point we
  * only explore the result of running *the first thread that is ready*!  Such a

frap_book.tex

@@ -4099,16 +4099,9 @@ $$\infer{\summ{\mt{Lock} \; a}{(r, w, \ell)}}{
   a \in \ell
 }$$
 
-Another relation summarizes a command as a flat list of threads, each with its own summary of the above variety.
+$$\infer{\summ{c_1 || c_2}{(r, w, \ell)}}{
-
+  \summ{c_1}{(r, w, \ell)}
-\newcommand{\summT}[2]{\mt{summarizeThreads}(#1, #2)}
+  & \summ{c_1}{(r, w, \ell)}
-
-$$\infer{\summT{c_1 || c_2}{\concat{S_1}{S_2}}}{
-  \summT{c_1}{S_1}
-  & \summT{c_2}{S_2}
-}
-\quad \infer{\summT{c}{(c, s)}}{
-  \summ{c}{s}
 }$$
 
 \newcommand{\na}[1]{\mt{nextAction}(#1)}
@@ -4140,30 +4133,29 @@ Given a next atomic action and a summary of another thread, it is now easy to de
 \newcommand{\pors}[1]{\mt{porSafe}(#1)}
 
 With these ingredients, we can define a predicate $\mt{porSafe}$ that figures out when a state is eligible for the partial-order reduction optimization, which is to force the first thread to run next, ignoring the other threads for now.
-(With a bit more complexity, we could also support other strict subsets of the threads that are selected to run.)
+In working out the formal details, we will confine ourselves to commands $c_1 || c_2$ with distinguished ``first threads'' $c_1$, though everything can be generalized to other settings (and doing that generalization could be a worthwhile exercise for the reader, though it requires a lot of logical bookkeeping).
-This optimization is only safe when the first thread can take a step and when that step commutes with any actions that other threads might perform.
+This optimization is only safe when the first thread can take a step and when that step commutes with any action that other threads (combined into $c_2$) might perform.
-Formally, we define $\pors{h, l, \concat{(c, s)}{S}}$ as follows, recalling that $s$ is a summary of thread $c$, and $S$ is the remaining threads, with their own summary information.
+Formally, we define $\pors{h, l, c_1, c_2, s}$ as follows, where $s$ should be a valid summary of $c_2$.
 \begin{itemize}
-\item There is some $c_0$ where $\na{c} = c_0$.  That is, thread $c$ has some atomic action lined up to run next.
+\item There is some $c_0$ where $\na{c_1} = c_0$.  That is, thread $c_1$ has some uniquely determined atomic action lined up to run next.
-\item There exist $h'$, $l'$, and $c'$ such that $\smallstep{(h, l, c)}{(h', l', c')}$.  That is, thread $c$ is actually able to take a step, which might not be possible if e.g. trying to take a lock that is already held.
+\item There exist $h'$, $l'$, and $c'_1$ such that $\smallstep{(h, l, c_1)}{(h', l', c'_1)}$.  That is, thread $c_1$ is actually able to take a step, which might not be possible if e.g. trying to take a lock that is already held.
-\item For every $(c_1, s) \in S$, we have $\commu{c_0}{s}$.  That is, all actions that other threads might perform commute with $c_0$, the first action of $c$.
+\item And the crucial compatibility condition: $\commu{c_0}{s}$.  That is, all actions that other threads might perform commute with $c_0$, the first action of $c_1$.
 \end{itemize}
 
-\newcommand{\smallstepC}[2]{#1 \to_C #2}
+\newcommand{\smallstepC}[3]{#1 \to_C^{#2} #3}
 
-With the applicability condition defined, it is now straightforward to define an optimized step relation.
+With the applicability condition defined, it is now straightforward to define an optimized step relation, parameterized on an accurate summary $s$ for $c_2$.
 
-$$\infer{\smallstepC{(h, l, \concat{(c, s)}{S})}{(h', l', \concat{(c', s)}{S})}}{
+$$\infer{\smallstepC{(h, l, c_1 || c_2)}{s}{(h', l', c'_1 || c_2)}}{
-  \smallstep{(h, l, c)}{(h', l', c')}
+  \smallstep{(h, l, c_1)}{(h', l', c'_1)}
 }$$
 
-$$\infer{\smallstepC{(h, l, S)}{(h', l', \concat{S_1}{\concat{(c', s)}{S_2}})}}{
+$$\infer{\smallstepC{(h, l, c_1 || c_2)}{s}{(h', l', c_1 || c'_2)}}{
-  \neg \pors{h, l, S}
+  \neg \pors{h, l, c_1, c_2, s}
-  & S = \concat{S_1}{\concat{(c, s)}{S_2}}
+  & \smallstep{(h, l, c_2)}{(h', l', c'_2)}
-  & \smallstep{(h, l, c)}{(h', l', c')}
 }$$
 
-The whole thing is wrapped up into transition systems as $\mathbb T_C(h, l, S) = \angled{\{(h, l, S)\}, \to_C}$.
+The whole thing is wrapped up into transition systems as $\mathbb T_C(h, l, c_1, c_2, s) = \angled{\{(h, l, c_1 || c_2)\}, \to_C^s}$.
 
 \newcommand{\tof}[2]{\mt{timeOf}(#1, #2)}
 
@@ -4191,24 +4183,23 @@ It may be surprising that, in our formal mixed embedding, there exist commands w
 We leave it as an exercise to the reader to find a concrete example.
 (Actually, the Coq code includes an example and its proof of unboundedness.)
 
-One last ingredient is to work with a relation $\to^i$, which is the $i$-way self-composition of $\to^*$.
+One last ingredient is to work with a relation $\to^i$, which is the $i$-way self-composition of $\to$.
 It is easy to show that whenever $x \to^* y$, there exists $i$ such that $x \to^i y$.
 
-\newcommand{\smallstepsC}[2]{#1 \to_C^* #2}
+\newcommand{\smallstepsC}[3]{#1 \to_C^{#2*} #3}
 
 With these ingredients, we can state the reduction theorem.
-We overload $\mt{natf}$ to apply to threads summaries $S$, where $\natf{S}$ iff for every $(c, s) \in S$ we have $\mt{natf}(c)$.
 \abstraction
 \begin{theorem}
-  If $\summT{c}{S}$ and $\tof{c}{n}$, then to prove $\mt{natf}$ as an invariant of $\mathbb T(h, l, c)$, it suffices to prove $\mt{natf}$ as an invariant of $\mathbb T_C(h, l, S)$.
+  If $\summ{c_2}{s}$ and $\tof{c_1 || c_2}{n}$, then to prove $\mt{natf}$ as an invariant of $\mathbb T(h, l, c_1 || c_2)$, it suffices to prove $\mt{natf}$ as an invariant of $\mathbb T_C(h, l, c_1, c_2, s)$.
 \end{theorem}
 \begin{proof}
   We assume for the sake of contradiction that there exists some derivation $\smallsteps{(h, l, c)}{(h', l', c')}$, where $\neg \natf{h', l', c'}$.
   First, since $c$ runs in bounded time, by Lemma \ref{completion}, we can \emph{complete} that execution to continue running to some $(h'', l'', c'')$, which is a stuck state.
   By Lemma \ref{stillFailing}, $\neg \natf{h'', l'', c''}$.
   Next, we conclude that there exists $i$ such that $(h, l, c) \to^i (h'', l'', c'')$.
-  By Lemma \ref{translate_trace}, there exist $h'$, $l'$, and $S'$ where $\smallstepsC{(h, l, S)}{(h', l', S')}$ and $\neg \natf{S'}$.
+  By Lemma \ref{translate_trace}, there exist $h'$, $l'$, and $c'$ where $\smallstepsC{(h, l, c_1 || c_2)}{s}{(h', l', c')}$ and $\neg \natf{c'}$.
-  These facts contradict our assumption that $\mt{natf}$ is an invariant of $\mathbb T_C(h, l, S)$.
+  These facts contradict our assumption that $\mt{natf}$ is an invariant of $\mathbb T_C(h, l, c_1, c_2, s)$.
 \end{proof}
 
 \begin{lemma}\label{completion}
@@ -4226,31 +4217,31 @@ We overload $\mt{natf}$ to apply to threads summaries $S$, where $\natf{S}$ iff
 \end{proof}
 
 \begin{lemma}\label{translate_trace}
-  If $(h, l, c) \to^i (h', l', c')$, and $(h', l', c')$ is stuck and about to fail, and $\summT{c}{S}$, then there exist $h'$, $l'$, and $S'$ such that $\smallstepsC{(h, l, S)}{(h', l', S')}$ and $\neg \natf{S'}$.
+  If $(h, l, c_1 || c_2) \to^i (h', l', c')$, and $(h', l', c')$ is stuck and about to fail, and $\summ{c_2}{s}$, then there exist $h'$, $l'$, and $c''$ such that $\smallstepsC{(h, l, c_1 || c_2)}{s}{(h', l', c'')}$ and $\neg \natf{c''}$.
 \end{lemma}
 \begin{proof}
   By induction on $i$.
   Note that induction on the structure of a derivation $\smallsteps{(h, l, c)}{(h', l', c')}$ would \emph{not} be sufficient here, as we will see in the proof sketch below that we sometimes invoke the induction hypothesis on an execution trace that is not just the tail of the one we started with.
 
-  If $i = 0$, then $(h, l, c)$ is already about to fail, and the conclusion follows trivially.
+  If $i = 0$, then $(h, l, c_1 || c_2)$ is already about to fail, and the conclusion follows trivially.
 
   Otherwise, $i = i' + 1$ for some $i'$.
-  We proceed by cases on the truth of $\pors{h, l, S}$.
+  We proceed by cases on the truth of $\pors{h, l, c_1, c_2, s}$.
 
-  If $\neg \pors{h, l, S}$, then we invert the derivation $(h, l, c) \to^i (h', l', c')$ to conclude $\smallstep{(h, l, c)}{(h'', l'', c'')}$ and $(h'', l'', c'') \to^{i'} (h', l', c')$ for some intermediate state.
+  If $\neg \pors{h, l, c_1, c_2, s}$, then we invert the derivation $(h, l, c_1 || c_2) \to^i (h', l', c')$ to conclude $\smallstep{(h, l, c_1 || c_2)}{(h'', l'', c'')}$ and $(h'', l'', c'') \to^{i'} (h', l', c')$ for some intermediate state.
   $\to_C$ is easily able to match that first step, as the optimization is disabled, and the rest follows directly by appeal to the induction hypothesis.
 
-  Otherwise, $\pors{h, l, S}$, and the key optimization is enabled, so that $\to_C$ only allows the first thread to run.
+  Otherwise, $\pors{h, l, c_1, c_2, s}$, and the key optimization is enabled, so that $\to_C$ only allows the first thread to run.
-  The next deduction is not immediate, because the first original step $\smallstep{(h, l, c)}{(h'', l'', c'')}$ may have chosen a thread beside the first.
+  The next deduction is not immediate, because the first original step $\smallstep{(h, l, c_1 || c_2)}{(h'', l'', c'')}$ may have chosen a thread beside $c_1$.
-  However, the trace $(h, l, c) \to^{i'+1} (h', l', c')$ \emph{must} eventually pick the first thread to run, and we apply Lemma \ref{translate_trace_commute} to \emph{commute} that eventual step to the front of the derivation, showing its equivalence to one that runs the first thread and then takes $i'$ additional steps to $(h', l', c')$.
+  However, the trace $(h, l, c_1 || c_2) \to^{i'+1} (h', l', c')$ \emph{must} eventually pick the first thread to run, and we apply Lemma \ref{translate_trace_commute} to \emph{commute} that eventual step to the front of the derivation, showing its equivalence to one that runs the first thread and then takes $i'$ additional steps to $(h', l', c')$.
   At this point the induction hypothesis applies to those $i'$ steps, to finish the proof.
 \end{proof}
 
 \begin{lemma}\label{translate_trace_commute}
-  If $(h, l, c) \to^{i+1} (h', l', c')$, where that last state is stuck, and if $\summT{c}{\concat{(c_0, s)}{S}}$, $\na{c_0} = x$, and $S$ is an accurate summary of threads that all commute with $x$, and $\smallstep{(h, l, c_0)}{(h_0, l_0, c'_0)}$, then there exists $c''$ such that $\summT{c''}{\concat{(c'_0, s)}{S}}$ and $(h_0, l_0, c'') \to^i (h', l', c')$.
+  If $(h, l, c_1 || c_2) \to^{i+1} (h', l', c')$, where that last state is stuck, and if $\summ{c_2}{s}$, $\na{c_1} = x$, $\commu{x}{s}$, and $\smallstep{(h, l, c_1)}{(h_0, l_0, c'_1)}$, then $(h_0, l_0, c'_1 || c_2) \to^i (h', l', c')$.
 \end{lemma}
 \begin{proof}
-  By induction on the derivation of $(h, l, c) \to^{i+1} (h', l', c')$, appealing to a few crucial lemmas, such as single-step determinism of any state in $\mt{nextAction}$'s domain, plus the soundness of $\mt{commutes}$ with respect to single steps of pairs of commands, plus the fact that single steps preserve the accuracy of summaries.
+  By induction on the derivation of $(h, l, c_1 || c_2) \to^{i+1} (h', l', c')$, appealing to a few crucial lemmas, such as single-step determinism of any state in $\mt{nextAction}$'s domain, plus the soundness of $\mt{commutes}$ with respect to single steps of pairs of commands, plus the fact that single steps preserve the accuracy of summaries.
 \end{proof}
 
 \section{Partial-Order Reduction More Generally}
@@ -4300,7 +4291,7 @@ This reduced state transition system never gets around to running the second thr
 To plug this soundness hole, we add a final condition on the ample sets.
 
 \begin{description}
-  \item[Fairness] \index{fairness}If there is a cycle in the state space where $\alpha$ is enabled at some point, then $\alpha \in \mathcal A(s)$ for some $s$ in the cycle.
+  \item[Fairness] \index{fairness}If there is a cycle in the finite state space where $\alpha$ is enabled at some point, then $\alpha \in \mathcal A(s)$ for some $s$ in the cycle.
 \end{description}
 
 This condition effectively forces the ample set for the example program above to include the second thread.