From 45fa64d69e4bf2963e254e2bbd0b831a15785054 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 2 May 2021 12:56:47 -0400 Subject: [PATCH] Revising for this week's lectures --- ProofByReflection.v | 11 +++++------ SharedMemory.v | 28 ++++++++++++++-------------- frap_book.tex | 3 +-- 3 files changed, 20 insertions(+), 22 deletions(-) diff --git a/ProofByReflection.v b/ProofByReflection.v index 88a27c1..3be91a4 100644 --- a/ProofByReflection.v +++ b/ProofByReflection.v @@ -26,7 +26,7 @@ Set Asymmetric Patterns. (* Proving that particular natural-number constants are even is certainly * something we would rather have happen automatically. The Ltac-programming - * techniques that we learned last week make it easy to implement such a + * techniques that we learned previously make it easy to implement such a * procedure. *) Inductive isEven : nat -> Prop := @@ -136,7 +136,7 @@ Unset Printing All. Theorem even_255 : isEven 255. Proof. - (*prove_even_reflective.*) + Fail prove_even_reflective. Abort. (* Coq reports that [reflexivity] can't prove [false = true], which makes * perfect sense! *) @@ -166,7 +166,6 @@ Print true_galore. * to case-analyze a [Prop] in any way in Gallina. We must _reify_ [Prop] into * some type that we _can_ analyze. This inductive type is a good candidate: *) -(* begin thide *) Inductive taut : Set := | TautTrue : taut | TautAnd : taut -> taut -> taut @@ -368,7 +367,7 @@ Section monoid. (* We can make short work of theorems like this one: *) - Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d. + Theorem t1 : forall a b c d, a + b + c + e + d = a + (b + c) + d. Proof. simplify; monoid. @@ -596,8 +595,8 @@ Section my_tauto. * module of the standard library, which (unsurprisingly) presents a view of * lists as sets. *) - (* The [eq_nat_dec] below is a richly typed equality test on [nat]s. We'll - * get to the ideas behind it in a later class. *) + (* The [eq_nat_dec] below is a richly typed equality test on [nat]s. + * See SubsetTypes.v for a review. *) Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. (* We define what it means for all members of a variable set to represent diff --git a/SharedMemory.v b/SharedMemory.v index 822d809..cdfde9d 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -13,8 +13,8 @@ Set Asymmetric Patterns. Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30). Definition heap := fmap nat nat. -Hint Extern 1 (_ <= _) => linear_arithmetic : core. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. +Local Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. (** * An object language with shared-memory concurrency *) @@ -25,7 +25,7 @@ Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. * theoretical benefits; we'll start with the most venerable style, shared * memory. *) -(* We'll build on the mixed-embedding languages from the last two chapter. +(* We'll build on the mixed-embedding languages from the last two chapters. * Let's simplify the encoding by only working with commands that generate * [nat]. *) Inductive cmd := @@ -95,9 +95,9 @@ Definition trsys_of (h : heap) (l : locks) (c : cmd) := {| * technique. Recall that model checking is all about reducing a problem to a * reachability question in a finite-state system. Our programs here have the * (perhaps surprising!) property that termination is guaranteed, for any - * initial state, regardless of how the scheduler behaves. Therefore, all - * programs of this language are finite-state and thus, in principle, amenable - * to model checking! (We were careful to leave out looping constructs.) + * initial state, regardless of how the scheduler behaves. However, + * counterintuitively, program execution does *not* need to be finite-state, + * and thus amenable to model checking, though we will stick to examples that are. * Let's define a simple two-thread program and model-check it. *) (* Throughout this file, we'll only be verifying that no thread could ever reach @@ -204,7 +204,7 @@ Definition trsys_ofL (h : heap) (l : locks) (c : cmd) := {| (* Now we prove some basic facts; commentary resumes before [step_runLocal]. *) -Hint Constructors step stepL : core. +Local Hint Constructors step stepL : core. Lemma run_Return : forall h l r h' l' c, step^* (h, l, Return r) (h', l', c) @@ -266,7 +266,7 @@ Proof. eauto. Qed. -Hint Resolve StepBindRecur_star StepParRecur1_star StepParRecur2_star : core. +Local Hint Resolve StepBindRecur_star StepParRecur1_star StepParRecur2_star : core. Lemma runLocal_idem : forall c, runLocal (runLocal c) = runLocal c. Proof. @@ -725,7 +725,7 @@ Proof. first_order; eauto. Qed. -Hint Constructors summarize : core. +Local Hint Constructors summarize : core. (* The next two lemmas show that, once a summary is accurate for a command, it * remains accurate throughout the whole execution lifetime of the command. *) @@ -805,7 +805,7 @@ Proof. linear_arithmetic. Qed. -Hint Constructors boundRunningTime : core. +Local Hint Constructors boundRunningTime : core. (* Key property: taking a step of execution lowers the running-time bound. *) Lemma boundRunningTime_step : forall c n h l h' l', @@ -843,7 +843,7 @@ Qed. (* Here we get a bit naughty and begin to depend on *classical logic*, as with * the *law of the excluded middle*: [forall P, P \/ ~P]. You may not have - * noticed that we've never applied that principle explicitly so far! *) + * noticed that we've rarely applied that principle explicitly so far! *) (* A very useful property: when a command has bounded running time, any * execution starting from that command can be *completed* to one ending in a @@ -1032,7 +1032,7 @@ Inductive stepsi : nat -> heap * locks * cmd -> heap * locks * cmd -> Prop := -> stepsi i st2 st3 -> stepsi (S i) st1 st3. -Hint Constructors stepsi : core. +Local Hint Constructors stepsi : core. Theorem steps_stepsi : forall st1 st2, step^* st1 st2 @@ -1041,7 +1041,7 @@ Proof. induct 1; first_order; eauto. Qed. -Hint Constructors stepC : core. +Local Hint Constructors stepC : core. (* The next few lemmas are quite technical. Commentary resumes for * [translate_trace]. *) @@ -1412,7 +1412,7 @@ Proof. (* We computed an inexact running time. By filling in zeroes for some * existential variables, we commit to a concrete bound. *) - Grab Existential Variables. + Unshelve. exact 0. exact 0. exact 0. diff --git a/frap_book.tex b/frap_book.tex index 52d5a41..a36019b 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -5013,7 +5013,7 @@ New component $l$ is a \emph{lockset}\index{lockset}, recording which locks are $$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{ \smallstep{(h, l, c_1)}{(h', l', c'_1)} } -\quad \infer{\smallstep{(h, l, x \leftarrow \mt{Return} \; v; c_2(x))}{(h, k, c_2(v))}}{}$$ +\quad \infer{\smallstep{(h, l, x \leftarrow \mt{Return} \; v; c_2(x))}{(h, l, c_2(v))}}{}$$ $$\infer{\smallstep{(h, l, \mt{Read} \; a)}{(h, l, \mt{Return} \; \msel{h}{a})}}{} \quad \infer{\smallstep{(h, l, \mt{Write} \; a \; v)}{(\mupd{h}{a}{v}, l, \mt{Return} \; 0)}}{}$$ @@ -5222,7 +5222,6 @@ The whole thing is wrapped up into transition systems as $\mathbb T_C(h, l, c_1, Our proof of soundness for this reduction will depend on having some constant upper bound on program execution time. This relation computes a conservative overapproximation. - $$\infer{\tof{\mt{Return} \; r}{n}}{} \quad \infer{\tof{\mt{Fail}}{n}}{} \quad \infer{\tof{\mt{Read} \; a}{n+1}}{}