From 37857a80af037f7ffc2baf24187db8816ed55794 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Wed, 27 Mar 2019 15:32:14 +0100
Subject: [PATCH] Updated is_chan to lock buffer resources. Introduced
 Authoritative Exclusive buffer CMRA.

---
 _CoqProject        |   2 +
 theories/buffer.v  |  56 +++++++++
 theories/channel.v | 282 ++++++++++++++++++++++++++++-----------------
 3 files changed, 236 insertions(+), 104 deletions(-)
 create mode 100644 theories/buffer.v

diff --git a/_CoqProject b/_CoqProject
index d611a29..39c6a8c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,6 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/list.v
+theories/buffer.v
 theories/channel.v
+
diff --git a/theories/buffer.v b/theories/buffer.v
new file mode 100644
index 0000000..042f276
--- /dev/null
+++ b/theories/buffer.v
@@ -0,0 +1,56 @@
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl auth.
+From iris.base_logic.lib Require Import auth.
+Set Default Proof Using "Type".
+
+(* Buffer CMRA *)
+Definition buff_type := list val.
+
+Definition buffUR : ucmraT :=
+  optionUR (exclR (leibnizC (buff_type))).
+
+Definition to_buff (b : buff_type) : buffUR :=
+  Excl' (b: leibnizC buff_type).
+
+Class buffG (Σ :gFunctors) := BuffG {
+  buffG_authG :> authG Σ buffUR;
+}.
+
+Definition buffΣ : gFunctors :=
+  #[GFunctor (authR buffUR)].
+
+Instance subG_buffG {Σ} :
+  subG buffΣ Σ → buffG Σ.
+Proof. solve_inG. Qed.
+
+Section buff.
+  Context `{!buffG Σ} (N : namespace).
+
+  Lemma excl_eq γ x y :
+      own γ (● to_buff y) -∗ own γ (◯  to_buff x) -∗ ⌜x = y⌝%I.
+  Proof.
+    iIntros "Hauth Hfrag".
+    iDestruct (own_valid_2 with "Hauth Hfrag") as %Hvalid.
+    apply auth_valid_discrete_2 in Hvalid.
+    destruct Hvalid as [Hincl _].
+    apply Excl_included in Hincl.
+    unfold to_buff.
+    rewrite Hincl.
+    iFrame.
+    eauto.
+  Qed.
+
+  Lemma excl_update γ x y z :
+      own γ (● to_buff y) -∗ own γ (◯  to_buff x) -∗ |==> own γ (● to_buff z) ∗ own γ (◯  to_buff z).
+  Proof.
+    iIntros "Hauth Hfrag".
+    iDestruct (own_update_2 with "Hauth Hfrag") as "H".
+    { eapply (auth_update _ _ (to_buff z) (to_buff z)).
+      eapply option_local_update.
+      eapply exclusive_local_update. done. }
+    rewrite own_op.
+    done.
+  Qed.
+
+End buff.
diff --git a/theories/channel.v b/theories/channel.v
index 32b6889..cfe0c42 100644
--- a/theories/channel.v
+++ b/theories/channel.v
@@ -2,12 +2,15 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl.
+From iris.algebra Require Import excl auth.
+From iris.base_logic.lib Require Import auth.
 From iris.heap_lang.lib Require Import lock.
 From iris.heap_lang.lib Require Import spin_lock.
 From osiris Require Import list.
+From osiris Require Import buffer.
 Set Default Proof Using "Type".
 
+
 Definition new_list : val :=
   λ: <>, lnil #().
 
@@ -45,13 +48,10 @@ Definition try_recv : val :=
     let lk := get_lock "c" in
     acquire lk;;
     let l := (get_side "c" (dual_side "s")) in
-    let v :=
-        match: !l with
-          SOME "p" => l <- Snd "p";; SOME (Fst "p")
-        | NONE => NONE
-        end in
-    release lk;;
-    v.
+    match: !l with
+      SOME "p" => l <- Snd "p";; release lk;; SOME (Fst "p")
+    | NONE => release lk;; NONE
+    end.
 
 Definition recv : val :=
   rec: "go" "c" "s" :=
@@ -61,56 +61,69 @@ Definition recv : val :=
     end.
 
 Section channel.
-  Context `{!heapG Σ, !lockG Σ} (N : namespace).
-  
+  Context `{!heapG Σ, !lockG Σ, !buffG Σ} (N : namespace).
+
   Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
-    (∃ l':loc, ⌜l = #l'⌝ ∧ ∃ hd : val, l' ↦ hd ∗ ⌜is_list hd xs⌝)%I.
+    (∃ l':loc, ∃ hd : val, ⌜l = #l'⌝ ∧ l' ↦ hd ∗ ⌜is_list hd xs⌝)%I.
 
   Definition is_side (s : val) : Prop :=
     s = left ∨ s = right.
-    
-  Definition is_chan (γ : gname) (c : val) (ls rs : list val) (R : iProp Σ) : iProp Σ :=
-    (∃ l r lk : val, ⌜c = ((l, r), lk)%V⌝ ∧ is_lock N γ lk R ∗ is_list_ref l ls ∗ is_list_ref r rs)%I.
+  
+  Definition is_chan (lkγ lsγ rsγ : gname) (c : val) (ls rs : list val) : iProp Σ :=
+    (∃ l r lk : val, ⌜c = ((l, r), lk)%V⌝ ∧
+                     own lsγ (◯  to_buff ls) ∗ own rsγ (◯  to_buff rs) ∗
+                     is_lock N lkγ lk
+                       (∃ ls rs, 
+                           is_list_ref l ls ∗ own lsγ (● to_buff ls) ∗
+                           is_list_ref r rs ∗ own rsγ (● to_buff rs)))%I.
 
-  Lemma new_chan_spec (R : iProp Σ) :
-    {{{ R }}}
+  Lemma new_chan_spec :
+    {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c; is_chan γ c [] [] R }}}.
+    {{{ c lkγ lsγ rsγ, RET c; is_chan lkγ lsγ rsγ c [] [] }}}.
   Proof. 
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /new_list /=.
+    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newlock /new_list /=.
     repeat wp_lam. wp_alloc lk as "Hlk".
     repeat wp_lam. wp_alloc r as "Hr".
     repeat wp_lam. wp_alloc l as "Hl".
     wp_pures.
-    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-    iMod (inv_alloc N _ (lock_inv γ lk R) with "[-Hl Hr HΦ]") as "#?".
-    { iIntros "!>". iExists false. by iFrame. }
+    iMod (own_alloc (Excl ())) as (lkγ) "Hγlk"; first done.
+    iMod (own_alloc (Auth (Excl' (to_buff [])) (to_buff []))) as (lsγ) "Hls"; first done.
+    iMod (own_alloc (Auth (Excl' (to_buff [])) (to_buff []))) as (rsγ) "Hrs"; first done.
+    rewrite auth_both_op.
+    rewrite own_op. rewrite own_op.
+    iDestruct "Hls" as "[Hlsa Hlsf]".
+    iDestruct "Hrs" as "[Hrsa Hrsf]".
+    iMod (inv_alloc N _ (lock_inv lkγ lk (∃ (ls rs : list val), is_list_ref #l ls ∗ own lsγ (● to_buff ls) ∗ is_list_ref #r rs ∗ own rsγ (● to_buff rs)))%I with "[Hlk Hγlk Hr Hl Hlsa Hrsa]") as "Hlk".
+    {
+      iNext. iExists _. iFrame. iFrame.
+      iExists [], []. iFrame.
+      iSplitL "Hl"=> //; iExists _, _; iSplit=> //; iFrame=> //. 
+    }
     iModIntro.
     iApply "HΦ".
     iExists _, _, _.
+    iFrame "Hlsf Hrsf".
     iSplit=> //.
-    iSplitR.
-    - unfold is_lock. iExists _. iSplit=> //.
-    - iSplitL "Hl"; iExists _; iSplit=> //; iExists (InjLV #()); iSplit => //.
+    unfold is_lock. iExists _. iSplit=> //.
   Qed.
 
-  (* Insert a value 'v' in the buffer of a given channel 'c', based on the given side 's' *)
-  Definition send_upd γ c ls rs R s v : iProp Σ :=
+  Definition send_upd lkγ lsγ rsγ c ls rs s v : iProp Σ :=
     match s with
-    | left  => is_chan γ c (ls ++ [v]) rs R
-    | right => is_chan γ c ls (rs ++ [v]) R
+    | left  => is_chan lkγ lsγ rsγ c (ls ++ [v]) rs
+    | right => is_chan lkγ lsγ rsγ c ls (rs ++ [v])
     | _ => ⌜False⌝%I
     end.
 
-  Lemma send_spec (γ : gname) (c v s : val) (ls rs : list val) (R : iProp Σ) :
-    {{{ is_chan γ c ls rs R ∗ ⌜is_side s⌝%I }}}
+  Lemma send_spec (lkγ lsγ rsγ : gname) (c v s : val) (ls rs : list val) :
+    {{{ is_chan lkγ lsγ rsγ c ls rs ∗ ⌜is_side s⌝%I }}}
       send c s v
-    {{{ RET #(); send_upd γ c ls rs R s v }}}.
+    {{{ RET #(); send_upd lkγ lsγ rsγ c ls rs s v }}}.
   Proof.
     iIntros (Φ) "[Hc #Hs] HΦ". 
     iRevert "Hs". iIntros (Hs).
     rewrite -wp_fupd /send /=.
-    iDestruct "Hc" as (l r lk Hc) "[#Hlk [Hl Hr]]".
+    iDestruct "Hc" as (l r lk Hc) "[Hlsf [Hrsf #Hlk]]".
     wp_lam.
     wp_pures.
     subst.
@@ -119,86 +132,126 @@ Section channel.
     wp_bind (acquire lk).
     iApply acquire_spec=> //.
     iNext.
-    iIntros "[Hlocked HR]".
+    iIntros "[Hlocked Hl]".
+    iDestruct "Hl" as (ls' rs') "[Hls [Hlsa [Hrs Hrsa]]]".    
+    iDestruct (excl_eq with "Hlsa Hlsf") as %Heqls. rewrite -(Heqls).
+    iDestruct (excl_eq with "Hrsa Hrsf") as %Heqrs. rewrite -(Heqrs).
     wp_seq.
-    wp_pures.
-    inversion Hs; 
-      [iDestruct "Hl" as (lb Hb bhd) "[Hl #Hbhd]" |
-       iDestruct "Hr" as (lb Hb bhd) "[Hr #Hbhd]"];
-      subst;
-      wp_pures;
-      wp_bind (lsnoc (Load #lb) v);
-      wp_load;
-      iApply lsnoc_spec=> //;
-      iIntros (hd' Hhd');
-      iNext;
-      wp_store;
-      wp_pures;
-      iApply (release_spec N γ lk R with "[Hlocked HR]") => //;
-      iFrame; eauto;
-      iModIntro;
-      iIntros (_);
-      iModIntro;
-      iApply "HΦ";
-      iExists _, _, _;
-      iSplitR;
-      eauto;
-      iSplitL "Hlk"=> //;
-      iSplitL "Hl"=> //;
-      iExists _;
-      iSplitR;
+    wp_pures.    
+    inversion Hs.
+    - iDestruct "Hls" as (lb Hb bhd) "[Hl #Hbhd]".
+      iDestruct (excl_update _ _ _ (ls ++ [v]) with "Hlsa Hlsf") as ">[Hlsa Hlsf]".
+      subst.
+      wp_pures.
+      wp_bind (lsnoc (Load #lb) v).
+      wp_load.
+      iApply lsnoc_spec=> //.
+      iIntros (hd' Hhd').
+      iNext.
+      wp_store.
+      wp_pures.
+      eauto.
+      iApply (release_spec N lkγ lk with "[Hlocked Hl Hlsa Hrsa Hrs]") => //.
+      {
+        iFrame; eauto.
+        iSplitR. iApply "Hlk".
+        iFrame. iExists _, _. iFrame.
+        iExists _, _. iSplit=> //. iFrame. iPureIntro => //.
+      }
+      iModIntro.
+      iIntros (_).
+      iModIntro.
+      iApply "HΦ".
+      iExists _, _, _.
+      iSplitR=> //.
+      iSplitL "Hlsf"=> //.
+      iSplitL "Hrsf"=> //.
+    - iDestruct "Hrs" as (lb Hb bhd) "[Hr #Hbhd]".
+      iDestruct (excl_update _ _ _ (rs ++ [v]) with "Hrsa Hrsf") as ">[Hrsa Hrsf]".
+      subst.
+      wp_pures.
+      wp_bind (lsnoc (Load #lb) v).
+      wp_load.
+      iApply lsnoc_spec=> //.
+      iIntros (hd' Hhd').
+      iNext.
+      wp_store.
+      wp_pures.
       eauto.
+      iApply (release_spec N lkγ lk with "[Hlocked Hr Hlsa Hrsa Hls]") => //.
+      {
+        iFrame; eauto.
+        iSplitR. iApply "Hlk".
+        iFrame. iExists _, _. iFrame.
+        iExists _, _. iSplit=> //. iFrame. iPureIntro => //.
+      } 
+      iModIntro.
+      iIntros (_).
+      iModIntro.
+      iApply "HΦ".
+      iExists _, _, _.
+      iSplitR=> //.
+      iSplitL "Hlsf"=> //.
+      iSplitL "Hrsf"=> //.
   Qed.
 
-  Definition try_recv_upd γ c ls rs R s v : iProp Σ :=
+  Definition try_recv_upd  lkγ lsγ rsγ c ls rs s v : iProp Σ :=
     match s with
     | left => match v with
-              | NONEV => (is_chan γ c ls rs R ∧ ⌜rs = []⌝)%I
-              | SOMEV w => (∃ rs', is_chan γ c ls rs' R ∧ ⌜rs = w::rs'⌝)%I
+              | NONEV => (is_chan lkγ lsγ rsγ c ls rs ∧ ⌜rs = []⌝)%I
+              | SOMEV w => (∃ rs', is_chan  lkγ lsγ rsγ c ls rs' ∧ ⌜rs = w::rs'⌝)%I
               | _ => ⌜False⌝%I
               end
     | right => match v with
-               | NONEV => (is_chan γ c ls rs R ∧ ⌜ls = []⌝)%I
-               | SOMEV w => (∃ ls', is_chan γ c ls' rs R ∧ ⌜ls = w::ls'⌝)%I
+               | NONEV => (is_chan  lkγ lsγ rsγ c ls rs ∧ ⌜ls = []⌝)%I
+               | SOMEV w => (∃ ls', is_chan  lkγ lsγ rsγ c ls' rs ∧ ⌜ls = w::ls'⌝)%I
                | _ => ⌜False⌝%I
                end 
     | _ => ⌜False⌝%I
     end.
 
-  Lemma try_recv_spec (γ : gname) (c v s : val) (ls rs : list val) (R : iProp Σ) :
-    {{{ is_chan γ c ls rs R ∗ ⌜is_side s⌝%I }}}
+  Lemma try_recv_spec ( lkγ lsγ rsγ : gname) (c v s : val) (ls rs : list val) :
+    {{{ is_chan lkγ lsγ rsγ c ls rs ∗ ⌜is_side s⌝%I }}}
       try_recv c s
-    {{{ v, RET v;  try_recv_upd γ c ls rs R s v }}}.
+    {{{ v, RET v;  try_recv_upd  lkγ lsγ rsγ c ls rs s v }}}.
   Proof.
     iIntros (Φ) "[Hc #Hs] HΦ". 
     iRevert "Hs". iIntros (Hs).
     rewrite -wp_fupd /send /=.
-    iDestruct "Hc" as (l r lk Hc) "[#Hlk [Hl Hr]]".
+    iDestruct "Hc" as (l r lk Hc) "[Hlsf [Hrsf #Hlk]]".
     subst.
     wp_lam.
     wp_pures.
     wp_bind (acquire _).
     iApply acquire_spec=> //.
     iNext.
-    iIntros "[Hlocked HR]".
+    iIntros "[Hlocked Hl]".
+    iDestruct "Hl" as (ls' rs') "[Hls [Hlsa [Hrs Hrsa]]]".
+    iDestruct (excl_eq with "Hlsa Hlsf") as %Heqls. rewrite -(Heqls).
+    iDestruct (excl_eq with "Hrsa Hrsf") as %Heqrs. rewrite -(Heqrs).
     wp_seq.
-    wp_bind (release _).
-    wp_bind (Snd _).
-    wp_pures.
-    iApply (release_spec N γ lk R with "[Hlocked HR]") => //.
-    iFrame. eauto.
-    iNext. iIntros (_).
     wp_pures.
     inversion Hs; subst.
     - wp_pures.
-      iDestruct "Hr" as (rl Hr rhd) "[Hr #Hrhd]".
+      iDestruct "Hrs" as (rl Hr rhd) "[Hrs #Hrhd]".
       wp_pures.
       subst.
       wp_load.
       iRevert "Hrhd". iIntros (Hrhd).
       unfold is_list in Hrhd.
-      destruct rs.
+      destruct rs'.
       + subst.
+        wp_pures.
+        wp_bind (release _).
+        wp_pures.
+        iApply (release_spec N lkγ lk with "[Hlocked Hls Hrs Hlsa Hrsa]") => //.
+        {
+          iFrame; eauto.
+          iSplitR. iApply "Hlk".
+          iFrame. iExists _, _. iFrame.
+          iExists _, _. iFrame=> //.
+        }
+        iNext. iIntros (_).
         wp_pures.
         iModIntro.
         iApply "HΦ".
@@ -206,36 +259,52 @@ Section channel.
         iExists _, _, _.
         iSplit=> //.
         iFrame.
-        iSplitR. eauto.
-        iExists _.
-        iSplit=> //.
-        iExists _.
-        iSplit=> //.
+        iApply "Hlk".
       + subst.
         destruct Hrhd as [hd' [Hrhd Hrhd']].
         subst.
         wp_pures.
-        wp_store. wp_pures. iModIntro.
+        wp_store. wp_pures. 
+        iDestruct (excl_update _ _ _ (rs') with "Hrsa Hrsf") as ">[Hrsa Hrsf]".
+        wp_bind (release _).
+        wp_pures.
+        iApply (release_spec N lkγ lk with "[Hlocked Hls Hrs Hlsa Hrsa]") => //.
+        {
+          iFrame; eauto.
+          iSplitR. iApply "Hlk".
+          iFrame. iExists _, _. iFrame.
+          iExists _, _. iFrame=> //.
+        }
+        iNext. iIntros (_).
+        wp_pures.
         iApply "HΦ".
         iExists _.
+        iModIntro.
         iSplit=> //.
         iExists _, _, _.
         iSplit=> //.
-        iSplit=> //.
-        iFrame. 
-        iExists _.
-        iSplit=>//.
-        iExists _.
-        iSplit=> //.
+        iFrame.
+        iApply "Hlk".
     - wp_pures.
-      iDestruct "Hl" as (ll Hl lhd) "[Hl #Hlhd]".
+      iDestruct "Hls" as (ls Hl lhd) "[Hls #Hlhd]".
       wp_pures.
       subst.
       wp_load.
       iRevert "Hlhd". iIntros (Hlhd).
       unfold is_list in Hlhd.
-      destruct ls.
+      destruct ls'.
       + subst.
+        wp_pures.        
+        wp_bind (release _).
+        wp_pures.
+        iApply (release_spec N lkγ lk with "[Hlocked Hls Hrs Hlsa Hrsa]") => //.
+        {
+          iFrame; eauto.
+          iSplitR. iApply "Hlk".
+          iFrame. iExists _, _. iFrame.
+          iExists _, _. iFrame=> //.
+        }
+        iNext. iIntros (_).
         wp_pures.
         iModIntro.
         iApply "HΦ".
@@ -243,27 +312,32 @@ Section channel.
         iExists _, _, _.
         iSplit=> //.
         iFrame.
-        iSplitR. eauto.
-        iExists _.
-        iSplit=> //.
-        iExists _.
-        iSplit=> //.
+        iApply "Hlk".
       + subst.
         destruct Hlhd as [hd' [Hlhd Hlhd']].
         subst.
         wp_pures.
-        wp_store. wp_pures. iModIntro.
+        wp_store. wp_pures. 
+        iDestruct (excl_update _ _ _ (ls') with "Hlsa Hlsf") as ">[Hlsa Hlsf]".
+        wp_bind (release _).
+        wp_pures.
+        iApply (release_spec N lkγ lk with "[Hlocked Hls Hrs Hlsa Hrsa]") => //.
+        {
+          iFrame; eauto.
+          iSplitR. iApply "Hlk".
+          iFrame. iExists _, _. iFrame.
+          iExists _, _. iFrame=> //.
+        }
+        iNext. iIntros (_).
+        wp_pures.
         iApply "HΦ".
         iExists _.
+        iModIntro.
         iSplit=> //.
         iExists _, _, _.
         iSplit=> //.
-        iSplit=> //.
-        iFrame. 
-        iExists _.
-        iSplit=>//.
-        iExists _.
-        iSplit=> //.
-  Qed.  
+        iFrame.
+        iApply "Hlk".
+  Qed. 
 
 End channel.
\ No newline at end of file
-- 
GitLab