Skip to content
GitLab
Commit 37857a80 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Updated is_chan to lock buffer resources. 

Introduced Authoritative Exclusive buffer CMRA.
parent 40da9e24
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ 37857a80
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/list.v
theories/buffer.v
theories/channel.v
theories/buffer.v 0 → 100644
View file @ 37857a80
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.
theories/channel.v
View file @ 37857a80
......@@ -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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment