ConcurrentSeparationLogic: stop bothering to choose postconditions for parallel compositions, which can't terminate (addresses #52)

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 fork0 P1 P2 := apply HtWeaken with (P := (P1 * P2)%sep); [ eapply HtPar | ].
-Ltac fork P1 P2 := fork0 P1 P2 || (eapply HtStrengthen; [ fork0 P1 P2 | ]).
+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
+      /\ P ===> P1 * P2.
-      /\ Q1 tt * Q2 tt ===> Q tt.
 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 H3; cancel.
-  rewrite <- H4; 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.
 

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}$.