Merge branch 'new_atomic' into 'master'

port to new atomic triples

See merge request !7

_CoqProject

 -Q theories iris_atomic
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-theories/atomic.v
 theories/sync.v
-theories/atomic_incr.v
 theories/simple_sync.v
 theories/flat.v
 theories/atomic_sync.v

opam

@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
 depends: [
-  "coq-iris" { (= "dev.2018-07-13.0.cbf73155") | (= "dev") }
+  "coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") }
 ]

theories/atomic.v

-(* Logically atomic triple *)
-
-From iris.base_logic Require Export fancy_updates.
-From iris.program_logic Require Export hoare weakestpre.
-Import uPred.
-
-Section atomic.
-  Context `{irisG Λ Σ} {A: Type}.
-
-  (* NOTE: This triple differs from the one described in the Iris 1.0 paper by
-  not having any laters.  That works for this case study, but would not work for
-  the case study described in the paper. *)
-
-  (* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
-  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
-  Definition atomic_triple
-             (α: A → iProp Σ) (* atomic pre-condition *)
-             (β: A → val _ → iProp Σ) (* atomic post-condition *)
-             (Ei Eo: coPset) (* inside/outside masks *)
-             (e: expr _) : iProp Σ :=
-    (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
-                       α x ∗
-                       ((α x ={Ei, Eo}=∗ P) ∧
-                        (∀ v, β x v ={Ei, Eo}=∗ Q v))
-     ) -∗ {{ P }} e @ ⊤ {{ Q }})%I.
-End atomic.

theories/atomic_incr.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang proofmode notation.
-From iris_atomic Require Import atomic.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang.lib Require Import par.
-
-Section incr.
-  Context `{!heapG Σ} (N : namespace).
-
-  Definition incr: val :=
-    rec: "incr" "l" :=
-       let: "oldv" := !"l" in
-       if: CAS "l" "oldv" ("oldv" + #1)
-         then "oldv" (* return old value if success *)
-         else "incr" "l".
-
-  (* TODO: Can we have a more WP-style definition and avoid the equality? *)
-  Definition incr_triple (l: loc) :=
-    atomic_triple (fun (v: Z) => l ↦ #v)%I
-                  (fun v ret => ⌜ret = #v⌝ ∗ l ↦ #(v + 1))%I
-                  ∅
-                  ⊤
-                  (incr #l).
-
-  Lemma incr_atomic_spec: ∀ (l: loc), incr_triple l.
-  Proof.
-    iIntros (l).
-    rewrite /incr_triple.
-    rewrite /atomic_triple.
-    iIntros (P Q) "#Hvs".
-    iLöb as "IH".
-    iIntros "!# HP".
-    wp_rec.
-    wp_bind (! _)%E.
-    iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
-    wp_load.
-    iMod ("Hvs'" with "Hl") as "HP".
-    iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
-    iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
-    destruct (decide (x = x')).
-    - subst.
-      iDestruct "Hvs'" as "[_ Hvs']".
-      iSpecialize ("Hvs'" $! #x').
-      wp_cas_suc.
-      iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iModIntro. wp_if. done.
-    - iDestruct "Hvs'" as "[Hvs' _]".
-      wp_cas_fail.
-      iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
-      iModIntro. wp_if. by iApply "IH".
-  Qed.
-End incr.
-
-
-Section user.
-  Context `{!heapG Σ, !spawnG Σ} (N : namespace).
-
-  Definition incr_2 : val :=
-    λ: "x",
-       let: "l" := ref "x" in
-       incr "l" ||| incr "l";;
-       !"l".
-
-  (* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
-  Lemma incr_2_safe:
-    ∀ (x: Z), (WP incr_2 #x {{ _, True }})%I.
-  Proof.
-    iIntros (x).
-    rewrite /incr_2 /=.
-    wp_lam.
-    wp_alloc l as "Hl".
-    iMod (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
-    wp_let.
-    wp_bind (_ ||| _)%E.
-    iAssert (□ WP incr #l {{ _, True }})%I as "#?".
-    { (* prove worker triple *)
-      iDestruct (incr_atomic_spec l) as "Hincr"=>//.
-      rewrite /incr_triple /atomic_triple.
-      iSpecialize ("Hincr"  $! True%I (fun _ => True%I) with "[]").
-      - iIntros "!# _".
-        (* open the invariant *)
-        iInv N as (x') ">Hl'" "Hclose".
-        (* mask magic *)
-        iMod (fupd_intro_mask' _ ∅) as "Hvs"; first set_solver.
-        iModIntro. iExists x'. iFrame "Hl'". iSplit.
-        + (* provide a way to rollback *)
-          iIntros "Hl'".
-          iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
-        + (* provide a way to commit *)
-          iIntros (v) "[Heq Hl']".
-          iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
-      - iDestruct "Hincr" as "#HIncr". iAlways. by iApply "HIncr". }
-    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[] []"); [done..|].
-    iIntros (v1 v2) "_ !>".
-    wp_seq. iInv N as (x') ">Hl" "Hclose".
-    wp_load. iApply "Hclose". eauto.
-  Qed.
-End user.

theories/atomic_sync.v

 
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre hoare atomic.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import agree frac.
-From iris_atomic Require Import atomic sync misc.
+From iris_atomic Require Import sync misc.
+
+(** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
 
 Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
@@ -27,9 +29,7 @@ Section atomic_sync.
   (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
   Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) :=
     (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x →
-                       atomic_triple (fun g => gHalf γ g ∗ □ α g)%I
-                                     (fun g v => ∃ g', gHalf γ g' ∗ β g g' v)%I
-                                     ∅ ⊤ (f' x))%I.
+                       <<< ∀ g, gHalf γ g ∗ □ α g >>> f' x @ ⊤ <<< ∃ v, ∃ g', gHalf γ g' ∗ β g g' v, RET v >>>)%I.
 
   (* TODO: Use our usual style with a generic post-condition. *)
   (* TODO: We could get rid of the x, and hard-code a unit. That would
@@ -57,22 +57,21 @@ Section atomic_sync.
     iSplitL "Hg2"; first done. iIntros "!#".
     iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
     iIntros (f') "#Hsynced {Hsyncer}".
-    iAlways. iIntros (α β x) "#Hseq".
-    iIntros (P Q) "#Hvss !# HP".
+    iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
+    iApply wp_atomic_intro. iIntros (Φ') "?".
     (* TODO: Why can't I iApply "Hsynced"? *)
-    iSpecialize ("Hsynced" $! P Q x).
-    iApply wp_wand_r. iSplitL "HP".
-    - iApply ("Hsynced" with "[]")=>//.
+    iSpecialize ("Hsynced" $! _ Φ' x).
+    iApply wp_wand_r. iSplitL.
+    - iApply ("Hsynced" with "[]")=>//; last iAccu.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
       (* we should view shift at this point *)
-      iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
-      iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
+      iApply fupd_wp. iMod "HP" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
       iDestruct (m_frag_agree with "Hg1 Hg2") as %Heq. subst.
       iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
       iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
       { iApply "Hseq". iFrame. done. }
       iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
-      iMod ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
+      iMod ("HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
       iSpecialize ("Hvs2" $! v).
       iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
       rewrite Qp_div_2.

theories/sync.v

@@ -10,7 +10,7 @@ Section sync.
   (* TODO: We could get rid of the x, and hard-code a unit. That would
      be no loss in expressiveness, but probably more annoying to apply.
      How much more annoying? And how much to we gain in terms of things
-     becomign easier to prove? *)
+     becoming easier to prove? *)
   Definition synced R (f f': val) :=
     (□ ∀ P Q (x: val), {{ R ∗ P }} f x {{ v, R ∗ Q v }} →
                        {{ P }} f' x {{ Q }})%I.

theories/treiber.v

-From iris.program_logic Require Export weakestpre.
+From stdpp Require Import namespaces.
+From iris.program_logic Require Export weakestpre atomic.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import frac auth gmap csum.
-From iris_atomic Require Import atomic misc.
+From iris_atomic Require Import misc.
 
 Definition new_stack: val := λ: <>, ref (ref NONE).
 
@@ -98,32 +99,25 @@ Section proof.
   Qed.
 
   Definition push_triple (s: loc) (x: val) :=
-  atomic_triple (fun xs_hd: list val * loc =>
-                     let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I
-                (fun xs_hd ret =>
-                   let '(xs, hd) := xs_hd in 
-                   ∃ hd': loc,
-                     ⌜ret = #()⌝ ∗ s ↦ #hd' ∗ hd' ↦ SOMEV (x, #hd) ∗ is_list hd xs)%I
-                ∅
-                ⊤
-                (push #s x).
+    <<< ∀ (xs : list val) (hd : loc), s ↦ #hd ∗ is_list hd xs >>>
+      push #s x @ ⊤
+    <<< ∃ hd' : loc, s ↦ #hd' ∗ hd' ↦ SOMEV (x, #hd) ∗ is_list hd xs, RET #() >>>.
   
   Lemma push_atomic_spec (s: loc) (x: val) :
     push_triple s x.
   Proof.
-    rewrite /push_triple /atomic_triple.
-    iIntros (P Q) "#Hvs".
-    iLöb as "IH". iIntros "!# HP". wp_rec.
+    rewrite /push_triple. iApply wp_atomic_intro.
+    iIntros (Φ) "HP". iLöb as "IH". wp_rec.
     wp_let. wp_bind (! _)%E.
-    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
+    iMod "HP" as (xs hd) "[[Hs Hhd] [Hvs' _]]".
     wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
     iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
     wp_bind (CAS _ _ _)%E.
-    iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
+    iMod "HP" as (xs' hd') "[[Hs Hhd'] Hvs']".
     destruct (decide (hd = hd')) as [->|Hneq].
     * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
-      iMod ("Hvs'" $! #() with "[-]") as "HQ".
-      { iExists l. iSplitR; first done. by iFrame. }
+      iMod ("Hvs'" with "[-]") as "HQ".
+      { by iFrame. }
       iModIntro. wp_if. eauto.
     * wp_cas_fail.
       iDestruct "Hvs'" as "[Hvs' _]".
@@ -132,30 +126,24 @@ Section proof.
   Qed.
 
   Definition pop_triple (s: loc) :=
-  atomic_triple (fun xs_hd: list val * loc =>
-                   let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I
-                (fun xs_hd ret =>
-                   let '(xs, hd) := xs_hd in
-                   (⌜ret = NONEV⌝ ∗ ⌜xs = []⌝ ∗ s ↦ #hd ∗ is_list hd []) ∨
-                   (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ∗ ⌜ret = SOMEV x⌝ ∗
-                                          ⌜xs = x :: xs'⌝ ∗ s ↦ #hd' ∗ is_list hd' xs'))%I
-                ∅
-                ⊤
-                (pop #s).
+    <<< ∀ (xs : list val) (hd : loc), s ↦ #hd ∗ is_list hd xs >>>
+      pop #s @ ⊤
+    <<< match xs with [] => s ↦ #hd ∗ is_list hd []
+                | x::xs' => ∃ q (hd': loc), hd ↦{q} SOMEV (x, #hd') ∗ s ↦ #hd' ∗ is_list hd' xs' end,
+    RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
 
   Lemma pop_atomic_spec (s: loc):
     pop_triple s.
   Proof.
-    rewrite /pop_triple /atomic_triple.
-    iIntros (P Q) "#Hvs".
-    iLöb as "IH". iIntros "!# HP". wp_rec.
+    rewrite /pop_triple. iApply wp_atomic_intro.
+    iIntros (Φ) "HP". iLöb as "IH". wp_rec.
     wp_bind (! _)%E.
-    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
+    iMod "HP" as (xs hd) "[[Hs Hhd] Hvs']".
     destruct xs as [|y' xs'].
     - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
       iDestruct "Hhd" as (q) "[Hhd Hhd']".
-      iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
-      { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
+      iMod ("Hvs'" with "[-Hhd]") as "HQ".
+      { iFrame. eauto. }
       iModIntro. wp_let. wp_load. wp_match.
       eauto.
     - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
@@ -165,20 +153,19 @@ Section proof.
       { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
       iModIntro. wp_let. wp_load. wp_match. wp_proj.
       wp_bind (CAS _ _ _).
-      iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
+      iMod "HP" as (xs hd'') "[[Hs Hhd''] Hvs']".
       destruct (decide (hd = hd'')) as [->|Hneq].
       + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
-        iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
-        { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
-          destruct xs as [|x' xs''].
-          - simpl. iDestruct "Hhd''" as (?) "H".
-            iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
-          - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
-            iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
-            subst.
-            iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
-            repeat (iSplitR "Hxs1 Hs"; first done).
-            iFrame. }
+        destruct xs as [|x' xs''].
+        { simpl. iDestruct "Hhd''" as (?) "H".
+          iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
+        simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
+        iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
+        iMod ("Hvs'" with "[-]") as "HQ".
+        { iExists (q / 2 / 2)%Qp, _.
+          iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
+          repeat (iSplitR "Hxs1 Hs"; first done).
+          iFrame. }
         iModIntro. wp_if. wp_proj. eauto.
       + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
         iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.