diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 4e1c61d..0f23113 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -342,11 +342,13 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu nth_error linvs a = Some I -> hoare_triple linvs I (Unlock a) (fun _ => emp)%sep -(* When forking into two threads, divide the (local) heap among them. *) +(* When forking into two threads, divide the (local) heap among them. + * For simplicity, we never let parallel compositions terminate, + * so it is appropriate to assign a contradictory overall postcondition. *) | HtPar : forall P1 c1 Q1 P2 c2 Q2, hoare_triple linvs P1 c1 Q1 -> hoare_triple linvs P2 c2 Q2 - -> hoare_triple linvs (P1 * P2)%sep (Par c1 c2) (fun _ => Q1 tt * Q2 tt)%sep + -> hoare_triple linvs (P1 * P2)%sep (Par c1 c2) (fun _ => [| False |])%sep (* Now we repeat these two structural rules from before. *) | HtConsequence : forall {result} (c : cmd result) P Q (P' : hprop) (Q' : _ -> hprop), @@ -372,6 +374,18 @@ Proof. reflexivity. Qed. +Lemma HtStrengthenFalse : forall linvs {result} (c : cmd result) P (Q' : _ -> hprop), + hoare_triple linvs P c (fun _ => [| False |])%sep + -> hoare_triple linvs P c Q'. +Proof. + simplify. + eapply HtStrengthen; eauto. + simplify. + unfold himp; simplify. + cases H0. + tauto. +Qed. + Lemma HtWeaken : forall linvs {result} (c : cmd result) P Q (P' : hprop), hoare_triple linvs P c Q -> P' ===> P @@ -451,8 +465,8 @@ Ltac use_IH H := conseq; [ apply H | .. ]; ht. Ltac loop_inv0 Inv := (eapply HtWeaken; [ apply HtLoop with (I := Inv) | .. ]) || (eapply HtConsequence; [ apply HtLoop with (I := Inv) | .. ]). Ltac loop_inv Inv := loop_inv0 Inv; ht. -Ltac fork0 P1 P2 := apply HtWeaken with (P := (P1 * P2)%sep); [ apply HtPar | ]. -Ltac fork P1 P2 := fork0 P1 P2 || (eapply HtStrengthen; [ fork0 P1 P2 | ]). +Ltac fork0 P1 P2 := apply HtWeaken with (P := (P1 * P2)%sep); [ eapply HtPar | ]. +Ltac fork P1 P2 := fork0 P1 P2 || (eapply HtStrengthenFalse; fork0 P1 P2). Ltac use H := (eapply use_lemma; [ eapply H | cancel; auto ]) || (eapply HtStrengthen; [ eapply use_lemma; [ eapply H | cancel; auto ] | ]). @@ -544,7 +558,6 @@ Proof. cancel. cancel. - cancel. Qed. (* Hm, we used exactly the same proof code for each thread, which makes sense, @@ -573,7 +586,6 @@ Proof. fork (emp%sep) (emp%sep); eauto. cancel. - cancel. Qed. @@ -690,8 +702,6 @@ Proof. cancel. cancel. cancel. - - cancel. Qed. @@ -817,8 +827,6 @@ Proof. cancel. cancel. cancel. - - cancel. Qed. @@ -1189,10 +1197,9 @@ Lemma invert_Par : forall linvs c1 c2 P Q, -> exists P1 P2 Q1 Q2, hoare_triple linvs P1 c1 Q1 /\ hoare_triple linvs P2 c2 Q2 - /\ P ===> P1 * P2 - /\ Q1 tt * Q2 tt ===> Q tt. + /\ P ===> P1 * P2. Proof. - induct 1; simp; eauto 10. + induct 1; simp; eauto 7. symmetry in x0. apply unit_not_nat in x0; simp. @@ -1200,11 +1207,10 @@ Proof. symmetry in x0. apply unit_not_nat in x0; simp. - eauto 10 using himp_trans. + eauto 8 using himp_trans. exists (x * R)%sep, x0, (fun r => x1 r * R)%sep, x2; simp; eauto. - rewrite H2; cancel. - rewrite <- H4; cancel. + rewrite H3; cancel. Qed. (* Temporarily transparent again! *) @@ -1518,12 +1524,10 @@ Proof. eapply IHstep in H2. simp. eexists; propositional. - eapply HtStrengthen. + apply HtStrengthenFalse. econstructor. eassumption. eassumption. - simp. - cases r; auto. eapply use_himp; try eassumption. cancel. eapply use_himp; try eassumption. @@ -1534,16 +1538,14 @@ Proof. eapply IHstep in H0. simp. eexists; propositional. - eapply HtStrengthen. + apply HtStrengthenFalse. econstructor. eassumption. eassumption. - simp. - cases r; auto. eapply use_himp; try eassumption. cancel. eapply use_himp; try eassumption. - rewrite H3. + rewrite H4. cancel. Qed. diff --git a/frap_book.tex b/frap_book.tex index 7f9e04d..7bc46fc 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -4816,14 +4816,15 @@ $$\infer{\hoare{P'}{c}{Q'}}{ \modularity When two threads use disjoint regions of memory, it is trivial to apply this rule of Concurrent Separation Logic to verify the threads independently. -$$\infer{\hoare{P_1 * P_2}{c_1 || c_2}{\lambda r. \; Q_1(r) * Q_2(r)}}{ +$$\infer{\hoare{P_1 * P_2}{c_1 || c_2}{\lambda \_. \; \lift{\bot}]}}{ \hoare{P_1}{c_1}{Q_1} & \hoare{P_2}{c_2}{Q_2} }$$ The separating conjunction $*$ turned out to be just the right way to express the idea of ``splitting the heap into a part for the first thread and a part for the second thread.'' Because $c_1$ and $c_2$ touch disjoint memory regions, all of their memory operations commute\index{commutativity}, so that we need not worry about the state-explosion problem, in all the ways that the scheduler might interleave their steps. +Note that, since for simplicity our running example family of concurrent object languages includes no way for parallel compositions to terminate, it makes sense to assign a contradictory overall postcondition. -However, with realistic shared-memory programs, we don't get off that easy. +However, with realistic shared-memory programs, we don't get off as easy as the parallel-composition rule suggests. Threads \emph{do} share memory regions, using \emph{synchronization}\index{synchronization} to tame the state-explosion problem. Our object language includes locks as its example of synchronization, and Concurrent Separation Logic is specialized to locks. We may keep the simplistic-seeming rule for parallel composition and implicitly enrich its power by adding a twist, in the form of some other rules. @@ -4901,7 +4902,7 @@ The first is representative of a family of lemmas that we prove, one for each sy As another example incorporating more of the complexities of concurrency, we have this lemma. \begin{lemma} - If $\hoare{P}{c_1 || c_2}{Q}$, then there exist $P_1$, $P_2$, $Q_1$, and $Q_2$ such that $\hoare{P_1}{c_1}{Q_1}$, $\hoare{P_2}{c_2}{Q_2}$, $P \Rightarrow P_1 * P_2$, and $Q_1(()) * Q_2(()) \Rightarrow Q(())$. + If $\hoare{P}{c_1 || c_2}{Q}$, then there exist $P_1$, $P_2$, $Q_1$, and $Q_2$ such that $\hoare{P_1}{c_1}{Q_1}$, $\hoare{P_2}{c_2}{Q_2}$, and $P \Rightarrow P_1 * P_2$. \end{lemma} \begin{proof} By induction on the derivation of $\hoare{P}{c_1 || c_2}{Q}$.