srv

srv.v

@@ -15,10 +15,12 @@ Definition srv : val :=
 Definition wait: val :=
   rec: "wait" "p" :=
     match: !"p" with
-      InjR "r" => "p" <- #0 ;; "r"
+      InjR "r" => "p" <- InjR #0 ;; "r"
     | InjL "_" => "wait" "p"
     end.
 
+Local Opaque wait.
+
 Definition mk_srv : val :=
   λ: "f",
      let: "p" := ref (InjR #0)%V in
@@ -26,7 +28,7 @@ Definition mk_srv : val :=
      Fork (srv "f" "p");;
      λ: "x",
         acquire "l";;
-                "p" <- InjL "x";;
+        "p" <- InjL "x";;
         let: "ret" := wait "p" in
         release "l";;
         "ret".
@@ -57,15 +59,62 @@ Section proof.
   Context `{!heapG Σ, !lockG Σ, !srvG Σ} (N : namespace).
 
   Definition srv_inv
-             (γ: gname) (p: loc)
+             (γx γ1 γ2: gname) (p: loc)
              (Q: val → val → Prop): iProp Σ :=
-    ((∃ x: val, p ↦ InjRV x) ∨
-     (∃ (x: val) (γ2: gname), p ↦ InjLV x ★ own γ ((1/2)%Qp, DecAgree x) ★ own γ2 (Excl ())) ∨
-     (∃ (x y: val) (γ2: gname), p ↦ InjRV y ★ own γ ((1/2)%Qp, DecAgree x) ★ ■ Q x y ★ own γ2 (Excl ())))%I.
-
-  Lemma srv_inv_timeless γ p Q: TimelessP (srv_inv γ p Q).
-  Proof. apply _. Qed.
+    ((∃ (x: val),   p ↦ InjRV x ★ own γ1 (Excl ())) ∨
+     (∃ (x: val),   p ↦ InjLV x ★ own γx ((1/2)%Qp, DecAgree x) ★ own γ2 (Excl ())) ∨
+     (∃ (x y: val), p ↦ InjRV y ★ own γx ((1/2)%Qp, DecAgree x) ★ ■ Q x y ★ own γ2 (Excl ())))%I.
   
+  Lemma srv_inv_timeless γx γ1 γ2 p Q: TimelessP (srv_inv γx γ1 γ2 p Q).
+  Proof. apply _. Qed.
+
+  Lemma wait_spec (Φ: val → iProp Σ) (Q: val → val → Prop) x γx γ1 γ2 p:
+    heapN ⊥ N →
+    heap_ctx ★ inv N (srv_inv γx γ1 γ2 p Q) ★
+    own γx ((1/2)%Qp, DecAgree x) ★ own γ1 (Excl ()) ★
+    (∀ y, own γ2 (Excl ()) -★ own γx (1%Qp, DecAgree x) -★ ■ Q x y-★ Φ y)
+    ⊢ WP wait #p {{ Φ }}.
+  Proof.
+    iIntros (HN) "(#Hh & #Hsrv & Hx & Hempty & HΦ)".
+    iLöb as "IH".
+    wp_rec. wp_bind (! #p)%E.
+    iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
+    + (* collision with Hempty *) admit.
+    + (* not finished *)
+      iDestruct "Hinv" as (x') "(Hp & Hx' & Hissued)".
+      wp_load.
+      iVs ("Hclose" with "[Hp Hx' Hissued]").
+      { iNext. iRight. iLeft. iExists x'. by iFrame. }
+      iVsIntro. wp_match. by iApply ("IH" with "Hx Hempty").
+    + (* finished *)
+      iDestruct "Hinv" as (x' y) "(Hp & Hx' & % & Hissued)".
+      (* assert (x = x'). *)
+      (* { admit. (* should use the properties of agreement monoid to fix this *) } *)
+      wp_load. iVs ("Hclose" with "[Hp Hx' Hissued]").
+      { iNext. iRight. iRight. iExists x', y. by iFrame. }
+      iVsIntro. wp_match.
+      wp_bind (_ <- _)%E.
+      iInv N as ">[Hinv|[Hinv|Hinv]]" "Hclose".
+      - (* colission *) admit.
+      - (* impossible ... this is why irreversibility is important *)
+        admit.
+      -  iDestruct "Hinv" as (x'' y') "(Hp & Hx' & % & Hissued)".
+         assert (x = x'').
+         { admit. (* should use the properties of agreement monoid to fix this *) }
+         subst. wp_store.
+         iVs ("Hclose" with "[Hp Hempty]").
+         { iNext. iLeft. iExists #0. by iFrame. }
+         iVsIntro. wp_seq.
+         assert (y = y').
+         { admit. (* exclusivity *) }
+         subst.
+         iClear "Hx". iClear "Hx'".
+         iAssert (own γx (1%Qp, DecAgree x'')) as "Hx".
+         { admit. }
+         iSpecialize ("HΦ" $! y' with "Hissued Hx").
+         by iApply "HΦ".
+  Admitted.
+                        
   Lemma mk_srv_spec (f: val) Q:
     heapN ⊥ N →
     heap_ctx ★ □ (∀ x:val, WP f x {{ v, ■ Q x v }})
@@ -73,39 +122,52 @@ Section proof.
   Proof.
     iIntros (HN) "[#Hh #Hf]".
     wp_let. wp_alloc p as "Hp".
-    iVs (own_alloc (Excl ())) as (γ1) "Hγ1"; first done.
-    iVs (own_alloc (1%Qp, DecAgree #0)) as (γ2) "Hγ2"; first done.
-    iVs (inv_alloc N _ (srv_inv γ1 γ2 p Q) with "[Hp Hγ1]") as "#?".
+    iVs (own_alloc (Excl ())) as (γ1) "Hempty"; first done. (* black token *)
+    iVs (own_alloc (Excl ())) as (γ2) "Hissued"; first done. (* white token *)
+    iVs (own_alloc (1%Qp, DecAgree #0)) as (γx) "Hx"; first done.
+    iVs (inv_alloc N _ (srv_inv γx γ1 γ2 p Q) with "[Hp Hempty]") as "#?".
     { iNext. rewrite /srv_inv. iLeft. iExists #0. by iFrame. }
     wp_let. wp_bind (newlock _).
     iApply newlock_spec=>//. iFrame "Hh".
-    iAssert (∃ x: val, own γ2 (1%Qp, DecAgree x))%I with "[Hγ2]" as "Hinv"; first by eauto.
-    iFrame "Hinv". iIntros (lk γ) "#Hlk".
+    iAssert (∃ x, own γx (1%Qp, DecAgree x) ★ own γ2 (Excl ()))%I with "[Hissued Hx]" as "Hinv".
+    { iExists #0. by iFrame. }
+    iFrame "Hinv". iIntros (lk γlk) "#Hlk".
     wp_let. wp_apply wp_fork.
     iSplitL.
     - (* client closure *)
       iVsIntro. wp_seq. iVsIntro.
       iAlways. iIntros (x).
-      iLöb as "IH". wp_rec.
-      wp_bind (acquire _). iApply acquire_spec.
-      iFrame "Hlk". iIntros "Hlked Ho". iDestruct "Ho" as (x') "Ho".
+      wp_let. wp_bind (acquire _). iApply acquire_spec.
+      iFrame "Hlk". iIntros "Hlked Ho".
+      iDestruct "Ho" as (x') "[Hx Hissued]".
       wp_seq. wp_bind (_ <- _)%E.
       iInv N as ">Hinv" "Hclose".
       rewrite /srv_inv.
       iDestruct "Hinv" as "[Hinv|[Hinv|Hinv]]".
-      + iDestruct "Hinv" as (x'') "Hp".
+      + iDestruct "Hinv" as (x'') "[Hp Hempty]".
         wp_store.
-        iAssert (own γ2 (1%Qp, DecAgree x') -★ (own γ2 ((1/2)%Qp, DecAgree x) ★ own γ2 ((1/2)%Qp, DecAgree x)))%I as "Hsplit".
+        iAssert (own γx (1%Qp, DecAgree x') -★ (own γx ((1/2)%Qp, DecAgree x) ★ own γx ((1/2)%Qp, DecAgree x)))%I as "Hsplit".
         { admit. }
-        iDestruct ("Hsplit" with "Ho") as "[Ho1 Ho2]".
-        iVs ("Hclose" with "[Hlked Hp Ho1]").
-        * rewrite /locked. iNext. iRight. iLeft.
-          iExists x. iFrame.
+        iDestruct ("Hsplit" with "Hx") as "[Hx1 Hx2]".
+        iVs ("Hclose" with "[Hp Hissued Hx1]").
+        { rewrite /locked. iNext. iRight. iLeft.
+          iExists x. by iFrame. }
+        (* now prove things about wait *)
+        iVsIntro. wp_seq.
+        wp_bind (wait _).
+        iApply (wait_spec with "[Hempty Hx2 Hlked]"); first by auto.
+        { iFrame "Hh". iFrame "~". iFrame.
+          iIntros (y) "Hempty Hx HQ".
+          wp_let.
+          wp_bind (release _).
+          iApply release_spec.
+          iFrame "Hlk Hlked".
+          iSplitL "Hempty Hx".
+          - iExists x. by iFrame.
+          - by wp_seq.
+        }
       + (* Impossible: reenter locked *)
         iExFalso. admit.
       + (* Impossible: reenter locked *)
-        iExFalso. admit.
-      
-     
-
-      
\ No newline at end of file
+        iExFalso. admit.      
+  Admitted.

sync.v

@@ -4,6 +4,8 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.tests Require Import atomic.
+From iris.algebra Require Import dec_agree frac.
+From iris.program_logic Require Import auth.
 Import uPred.
 
 (* See CaReSL paper §3.2 *)
@@ -83,31 +85,36 @@ Section proof.
     iFrame.
     by wp_seq.
   Qed.
+End proof.
 
-  (* a general way to get atomic triple from mk_styc *)
-
-  Definition atomic_triple' {A: Type}
-             (ϕ: A → iProp Σ)
-             (β: A → A → val → iProp Σ)
-             (Ei Eo: coPset)
-             (e: expr) : iProp Σ :=
-    (∀ P Q, (P ={Eo, Ei}=> ∃ g g',
-                                ϕ g ★
-                                (∀ v, β g g' v ={Ei, Eo}=★ Q v)
-            ) -★ {{ P }} e @ ⊤ {{ Q }})%I.
+Section generic.
+  Context {A: Type} `{∀ x y : A, Decision (x = y)}.
   
-End proof.
+  Definition syncR := authR (optionUR (prodR fracR (dec_agreeR A))).
 
-From iris.algebra Require Import dec_agree frac.
-From iris.program_logic Require Import auth.
+  Class syncG Σ := SyncG { sync_tokG :> inG Σ syncR }.
+  Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
 
-Definition pcas_R := authR (optionUR (prodR fracR (dec_agreeR (val * val)))).
+  Section triple.
+    Context `{!heapG Σ, !lockG Σ, !syncG Σ} (N : namespace).
 
-Class pcasG Σ := PcasG { pcas_tokG :> inG Σ pcas_R }.
-Definition pcasΣ : gFunctors := #[GFunctor (constRF pcas_R)].
+    Definition gFragR (g: A) : syncR := ◯ Some ((1/2)%Qp, DecAgree g).
+    Definition gFullR (g: A) : syncR := ● Some ((1/2)%Qp, DecAgree g).
+    
+    Definition gFrag (γ: gname) (g: A) : iProp Σ := own γ (gFragR g).
+    Definition gFull (γ: gname) (g: A) : iProp Σ := own γ (gFullR g).
+  
+    Definition atomic_triple'
+               (β: A → A → val → iProp Σ)
+               (Ei Eo: coPset)
+               (e: expr) γ : iProp Σ :=
+      (∀ Q, (∀ g g' r, (True ={Eo, Ei}=> gFrag γ g) ★
+                     (gFrag γ g' ★ β g g' r ={Ei, Eo}=> Q r)) -★ WP e {{ Q }})%I.
+  End triple.
+End generic.
 
 Section atomic_pair.
-  Context `{!heapG Σ, !lockG Σ, !pcasG Σ} (N : namespace).
+  Context `{!heapG Σ, !lockG Σ, !(@syncG (val * val) _ Σ)} (N : namespace).
   
   Definition pcas_seq : val :=
     λ: "l1" "l2" "a" "b",
@@ -156,33 +163,22 @@ Section atomic_pair.
           let: "v" := pcas_seq "l1" "l2" "a" "b" in
           release "lk";;
           "v".
-
-  Definition gFullR (x1 x2: val) : pcas_R := ● Some ((1/2)%Qp, DecAgree (x1, x2)).
-  Definition gFragR (x1 x2: val) : pcas_R := ◯ Some ((1/2)%Qp, DecAgree (x1, x2)).
-
-  Definition gFull (x1 x2: val) γ: iProp Σ := own γ (gFullR x1 x2).
-  Definition gFrag (x1 x2: val) γ :iProp Σ := own γ (gFragR x1 x2).
-
-  Definition β (x1 x2 x1' x2' v a b: val) : iProp Σ :=
-    ((v = #true  ∧ x1 = a ∧ x2 = a ∧ x1' = b ∧ x2' = b) ∨
-     (v = #false ∧ x1 = a ∧ x2 = a ∧ x1' = b ∧ x2' = b))%I.
   
-  Definition is_pcas γ (f: val) (Ei Eo: coPset) : iProp Σ :=
-    (∀ (a b: val) (Q: val → iProp Σ),
-      (∀ x1 x2 x1' x2' (r: val),
-         (True ={Ei, Eo}=> gFrag x1 x2 γ) ★
-         (gFrag x1' x2' γ ★ β x1 x2 x1' x2' r a b ={Eo, Ei}=> Q r)) -★ WP f a b {{ Q }})%I.
+  Definition β (a b: val) (xs xs': val * val) (v: val) : iProp Σ :=
+    ((v = #true  ∧ fst xs = a ∧ snd xs = a ∧ fst xs' = b ∧ snd xs' = b) ∨
+     (v = #false ∧ fst xs = a ∧ snd xs = a ∧ fst xs' = b ∧ snd xs' = b))%I.
+
+  Definition is_pcas γ (f: val): iProp Σ :=
+    (∀ a b: val, atomic_triple' (β a b) heapN (⊤ ∖ nclose N) (f a b) γ)%I.
 
-  Lemma pcas_atomic_spec (x10 x20: val): (* let's fix Eo as ⊤, and Ei as heapN *)
-    heapN ⊥ N →
-    heap_ctx
-    ⊢ WP mk_pcas x10 x20 {{ f, ∃ γ, □ is_pcas γ f (⊤ ∖ nclose N) heapN }}.
+  Lemma pcas_atomic_spec (x10 x20: val):
+    heapN ⊥ N → heap_ctx ⊢ WP mk_pcas x10 x20 {{ f, ∃ γ, □ is_pcas γ f }}.
   Proof.
     iIntros (HN) "#Hh". repeat wp_let.
     wp_alloc l1 as "Hl1". wp_let.
-    wp_alloc l2 as "Hl2". iVs (own_alloc (gFullR x10 x20 ⋅ gFragR x10 x20)) as (γ) "Hγ"; first by done.
+    wp_alloc l2 as "Hl2". iVs (own_alloc (gFullR (x10, x20) ⋅ gFragR (x10, x20))) as (γ) "Hγ"; first by done.
     iDestruct (own_op with "Hγ") as "[Hfull Hfrag]".
-    iAssert (∃ x1 x2, l1 ↦ x1 ★ l2 ↦ x2 ★ gFull x1 x2 γ)%I with "[-Hfrag]" as "HR".
+    iAssert (∃ x1 x2, l1 ↦ x1 ★ l2 ↦ x2 ★ gFull γ (x1, x2))%I with "[-Hfrag]" as "HR".
     { iExists x10, x20. by iFrame. }
     wp_let.
     wp_bind (newlock _). iApply newlock_spec=>//.
@@ -209,24 +205,26 @@ Section atomic_pair.
         wp_if. wp_store.
         wp_store. wp_let.
         wp_let.
-        iDestruct ("H" $! a a b b #true) as "[Hvs1 Hvs2]".
+        iDestruct ("H" $! (a, a) (b, b) #true) as "[Hvs1 Hvs2]".
         rewrite /is_lock.
         iDestruct "Hlk" as (l) "(% & _ & % & Hinv)".
         iInv N as ([]) ">[Hl _]" "Hclose".
         * iVs ("Hvs1" with "[]") as "Hfraga"; first by auto.
           subst. wp_store.
-          iAssert (β a a b b #true a b) as "Hβ".
+          iAssert (β a b (a, a) (b, b) #true) as "Hβ".
           { iLeft. eauto. }
-          iAssert (gFrag a a γ ★ gFull a a γ -★ gFrag b b γ ★ gFull b b γ)%I as "H".
+          iAssert (gFrag γ (a, a) ★ gFull γ (a, a) -★ gFrag γ (b, b) ★ gFull γ (b, b))%I as "H".
           { admit. }
           iDestruct ("H" with "[Hfraga HFulla]") as "[HFragb HFullb]"; first by iFrame.
+          
           iVs ("Hvs2" with "[HFragb Hβ]"); first by iFrame.
           rewrite /lock_inv.
           iVsIntro. iVs ("Hclose" with "[-~]").
           { iNext. iExists false.
             iFrame. iExists b, b. by iFrame. }
           iVsIntro. wp_seq. done.
-Admitted.
+  Admitted.
+End atomic_pair.
 
 Section sync_atomic.
   Context `{!heapG Σ, !lockG Σ} (N : namespace) {A: Type}.