Revising for tomorrow's lecture

This commit is contained in:
Adam Chlipala 2022-02-13 14:16:33 -05:00
parent 22118d90be
commit 0cba7c9f61
2 changed files with 6 additions and 12 deletions

View file

@ -411,17 +411,14 @@ Definition increment2_sys := parallel increment_sys increment_sys.
* added to the shared counter so far. *)
Definition contribution_from (pr : increment_program) : nat :=
match pr with
| Unlock => 1
| Done => 1
| Unlock | Done => 1
| _ => 0
end.
(* Second big idea: the program counter also tells us whether a thread holds the lock. *)
Definition has_lock (pr : increment_program) : bool :=
match pr with
| Read => true
| Write _ => true
| Unlock => true
| Read | Write _ | Unlock => true
| _ => false
end.
@ -435,11 +432,9 @@ Definition shared_from_private (pr1 pr2 : increment_program) :=
* e.g. that they shouldn't both be in the critical section at once. *)
Definition instruction_ok (self other : increment_program) :=
match self with
| Lock => True
| Read => has_lock other = false
| Lock | Done => True
| Read | Unlock => has_lock other = false
| Write n => has_lock other = false /\ n = contribution_from other
| Unlock => has_lock other = false
| Done => True
end.
(** Now we have the ingredients to state the invariant. *)

View file

@ -1458,7 +1458,7 @@ Let's define a suitable invariant for factorial.
\end{eqnarray*}
It is an almost-routine exercise to prove that $I$ really is an invariant, using Theorem \ref{invariant_induction}.
The key new ingredient we need is \emph{inversion}, a principle for deducing which inference rules may have been used to prove a fact.
The key new ingredient we need is \emph{inversion}, a principle for deducing which inference rules may have been used to prove a fact.\index{inversion}
For instance, at one point in the proof, we need to draw a conclusion from a premise $s \in \mathcal F_0$, meaning that $s$ is an initial state.
By inversion, because set $\mathcal F_0$ is defined by a single inference rule, that rule must have been used to conclude the premise, so it must be that $s = \mathsf{WithAccumulator}(n_0, 1)$.
@ -1544,6 +1544,7 @@ Consider \texttt{global} as a variable shared across all threads, while each thr
The meaning of \texttt{lock()} and \texttt{unlock()} is as usual\index{locks}, where at most one thread can hold the lock at once, claiming it via \texttt{lock()} and relinquishing it via \texttt{unlock()}.
When variable \texttt{global} is initialized to 0 and $n$ threads run this code at once and all terminate, we expect that \texttt{global} finishes with value $n$.
Of course, bugs in this program, like forgetting to include the locking, could lead to all sorts of wrong answers, with any value between 1 and $n$ possible with the right demonic thread interleaving.
(Here ``demonic'' refers to consideration of worst-case behavior, with respect to the desired correctness property.)\index{demonic choice}
\encoding
To prove that we got the program right, let's formalize it as a transition system. First, our state set:
@ -1561,11 +1562,9 @@ We will account for the value of variable \texttt{global} separately, in a way t
In particular, we will define a transition system for a single thread as $\mathcal L = \angled{(\mathbb N \times \mathbb B) \times P, \mathcal L_0, \to_{\mathcal L}}$.
We define the state to include not only the thread-local state $P$ but also the value of \texttt{global} (in $\mathbb N$) and whether the lock is currently taken (in $\mathbb B$, the Booleans, with values $\top$ [true] and $\bot$ [false]).
There is one designated initial state.
$$\infer{((0, \bot), \mathsf{Lock}) \in \mathcal L_0}{}$$
Four inference rules explain the four transitions between program counters that a single thread can make, reading and writing shared state as needed.
$$\infer{((g, \bot), \mathsf{Lock}) \to_{\mathcal L} ((g, \top), \mathsf{Read})}{}
\quad \infer{((g, \ell), \mathsf{Read}) \to_{\mathcal L} ((g, \ell), \mathsf{Write}(g))}{}$$
$$\infer{((g, \ell), \mathsf{Write}(n)) \to_{\mathcal L} ((n+1, \ell), \mathsf{Unlock})}{}