Commit 8a9e568c authored by Dan Frumin's avatar Dan Frumin

Merge branch 'flockv3'

parents 05f79935 23ae69a1
......@@ -3,7 +3,6 @@
theories/lib/list.v
theories/lib/mset.v
theories/lib/spin_lock.v
theories/lib/flock.v
theories/lib/locking_heap.v
theories/lib/U.v
......
opam-version: "1.2"
name: "coq-iris-c-monad"
maintainer: "Unmaintained"
maintainer: "Dan Frumin"
authors: "Dan Frumin, Leon Gondelman, Robbert Krebbers"
homepage: "https://gitlab.science.ru.nl/lgg/iris-c-monad"
bug-reports: "https://gitlab.science.ru.nl/lgg/iris-c-monad/issues"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
......
......@@ -67,8 +67,8 @@ Section a_wp.
is_mset env X
full_locking_heap σ)%I.
Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) :=
([ map] i p I, flock_res γ i p.1 p.2)%I.
Definition flock_resources (γ : flock_name) (I : gmap prop_id lock_res) :=
([ map] i X I, flock_res amonadN γ i X)%I.
(** DF: The outer `WP` here is needed to be able to preform some reductions inside a heap_lang context.
Without this, the `a_wp_awp` rule is not provable.
......@@ -80,10 +80,10 @@ Section a_wp.
Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
tc_opaque (WP e {{ ev,
(γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)),
(γ : flock_name) (env : val) (l : val) (I : gmap prop_id lock_res),
is_flock amonadN γ l -
flock_resources γ I -
([ map] p I, p.1) (env_inv env R) -
([ map] X I, res_prop X) (env_inv env R) -
WP ev env l {{ v, Φ v flock_resources γ I }}
}})%I.
......@@ -132,20 +132,20 @@ Section a_wp_rules.
Lemma awp_insert_res e Φ R1 R2 :
R1 -
AWP e @ (R1 R2) {{ v, R1 - Φ v }} -
AWP e @ (R1 R2) {{ v, R1 ={}= Φ v }} -
AWP e @ R2 {{ Φ }}.
Proof.
iIntros "HR1 Hawp". rewrite /awp /=.
iApply (wp_wand with "Hawp").
iIntros (v) "HΦ".
iIntros (γ env l I) "#Hflock Hres #Heq".
iMod (flock_res_single_alloc _ (dom (gset prop_id) I) with "Hflock HR1") as (j) "[% Hres']"; first done.
pose (I' := <[j:= (R1,1%Qp)]>I).
iMod (flock_res_alloc_strong _ (dom (gset prop_id) I) with "Hflock HR1") as (j ρ) "[% Hres']"; first done.
pose (I' := <[j:= (LockRes R1 1 ρ)]>I).
assert (I !! j = None) by by eapply not_elem_of_dom.
iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
{ rewrite /flock_resources /I'.
rewrite big_sepM_insert; last done. iFrame. }
{ rewrite big_sepM_insert; last done. simpl. iRewrite "Heq".
rewrite big_sepM_insert //. iFrame. }
{ rewrite big_sepM_insert // /=. iRewrite "Heq".
rewrite (assoc _ R1 _ R2).
rewrite (comm _ R1 (env_inv env)).
rewrite -(assoc _ _ R1 R2). done. }
......@@ -153,8 +153,8 @@ Section a_wp_rules.
iApply (wp_wand with "HΦ").
iIntros (w) "[HΦ HI]". rewrite /flock_resources /I'.
rewrite big_sepM_insert /=; last done. iDestruct "HI" as "[HR1 $]".
iMod (flock_res_single_dealloc with "Hflock HR1") as (R') "[HR' Heq']"; first done.
iApply "HΦ". iModIntro. do 2 iNext. by iRewrite "Heq'".
iMod (flock_res_dealloc with "Hflock HR1") as "HR"; try done.
by iApply "HΦ".
Qed.
Lemma awp_wand e (Φ Ψ : val iProp Σ) R :
......@@ -207,31 +207,31 @@ Section a_wp_rules.
Proof.
iIntros "Hwp". rewrite /awp /=. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[HI Hcl]". iRewrite "Heq1" in "HI".
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq1" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
wp_apply (newlock_cancel_spec amonadN); first done.
wp_apply (newflock_spec amonadN); first done.
iIntros (k γ') "#Hlock2".
iMod (flock_res_single_alloc _ (dom (gset prop_id) I) _ _ (env_inv env Q)%I
with "Hlock2 [$Henv $HQ]") as (i') "[% Hres]"; first done.
iMod (flock_res_alloc_strong _ _ _ (env_inv env Q)%I with "Hlock2 [$HQ $Henv]") as (s ρ) "[_ Hres]"; first done.
wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[i' := ((env_inv env Q)%I,1%Qp)]} with "Hlock2 [Hres] []").
- iApply ("Hwp" $! _ _ _ {[s:=(LockRes _ 1 ρ)]} with "Hlock2 [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
+ rewrite big_sepM_singleton //.
- iIntros (w) "[HR Hres]".
rewrite /flock_resources big_sepM_singleton /=.
iMod (flock_res_single_dealloc with "Hlock2 Hres") as (Q') "[HQ' #Heq2]"; first done.
iMod (flock_res_dealloc with "Hlock2 Hres") as "[Henv HQ]"; try done.
wp_let.
iAssert ( (env_inv env Q))%I with "[HQ']" as "[Henv HQ]".
{ iNext. by iRewrite "Heq2". }
iDestruct ("HR" with "HQ") as "[HR HΦ]".
iMod ("Hcl" with "[HR Henv]") as "[Hflocked Hres]".
iMod ("Hcl" with "[HR Henv]") as "Hflocked".
{ iNext. iRewrite "Heq1". iFrame. }
wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
iIntros "_". wp_pures. iFrame.
wp_apply (release_cancel_spec' with "[$Hlock1 $Hflocked]").
iIntros "$". wp_pures. iFrame.
Qed.
Lemma awp_atomic_env (ev : val) R Φ :
......@@ -241,16 +241,19 @@ Section a_wp_rules.
Proof.
iIntros "Hwp". rewrite /awp /=. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[HI Hcl]". iRewrite "Heq" in "HI".
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq" in "HI".
iDestruct "HI" as "[Henv HR]".
iDestruct ("Hwp" with "Henv HR") as "Hwp".
wp_pures; simpl.
iSpecialize ("Hwp" with "Henv HR").
wp_apply (wp_wand with "Hwp").
iIntros (w) "[Henv [HR HΦ]]". wp_pures.
iRewrite "Heq" in "Hcl".
iMod ("Hcl" with "[$HR $Henv]") as "[Hflocked Hres]".
wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
iIntros "_". wp_pures. iFrame.
iMod ("Hcl" with "[$HR $Henv]") as "Hflocked".
wp_apply (release_cancel_spec' with "[$Hlock $Hflocked]").
iIntros "$". wp_pures. iFrame.
Qed.
Lemma awp_par (Ψ1 Ψ2 : val iProp Σ) e1 e2 R (Φ : val iProp Σ) :
......@@ -265,7 +268,7 @@ Section a_wp_rules.
wp_apply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
pose (I' := fmap (λ x, (x.1, (x.2/2)%Qp)) I).
pose (I' := fmap (λ X, LockRes (res_prop X) (res_frac X/2) (res_name X)) I).
iAssert (flock_resources γ I' flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
{ rewrite /flock_resources -big_sepM_sepM.
rewrite /I' big_sepM_fmap /=.
......@@ -301,23 +304,24 @@ Section a_wp_run.
iNext. iIntros (env) "Henv". wp_let.
iMod locking_heap_init as (?) "Hσ".
pose (amg := AMonadG Σ _ _ _ _).
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "#Hlock". rewrite- wp_fupd.
iMod (flock_res_single_alloc _ _ _ (env_inv env R)%I
with "Hlock [Henv Hσ $HR]") as (i) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
iSpecialize ("Hwp" $! amg).
wp_apply (newflock_spec amonadN); first done.
iIntros (k γ') "#Hlock". iApply wp_fupd.
iMod (flock_res_alloc_strong _ _ _ (env_inv env R)%I
with "Hlock [Henv Hσ $HR]") as (s ρ) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
wp_let.
iMod (wp_value_inv with "Hwp") as "Hwp".
wp_let. wp_bind (ev env k).
wp_bind (ev env k).
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[i := ((env_inv env R)%I,1%Qp)]} with "Hlock [Hres] []").
- iApply ("Hwp" $! _ _ _ {[s := LockRes _ 1 ρ]} with "Hlock [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
+ rewrite big_sepM_singleton //.
- iIntros (w) "[HΦ Hres]".
rewrite /flock_resources big_sepM_singleton /=.
iMod (flock_res_single_dealloc with "Hlock Hres") as (R') "[HR' #Heq]"; first done.
iMod (flock_res_dealloc with "Hlock Hres") as "[Henv HR]"; try done.
wp_let.
iApply "HΦ". iNext. iRewrite -"Heq" in "HR'". iDestruct "HR'" as "[_ $]".
iApply "HΦ". iFrame.
Qed.
End a_wp_run.
......
This diff is collapsed.
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.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
( b : bool, l #b if b then True else own γ (Excl ()) R)%I.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
( l: loc, lk = #l inv N (lock_inv γ l R))%I.
Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
Proof. solve_proper. Qed.
(** The main proofs. *)
Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
Proof. apply _. Qed.
Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ):
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
iModIntro. iApply "HΦ". iExists l. eauto.
Qed.
Lemma try_acquire_spec γ lk R :
{{{ is_lock γ lk R }}} try_acquire lk
{{{ b, RET #b; if b is true then locked γ R else True }}}.
Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed.
Lemma acquire_spec γ lk R :
( Φ,
is_lock γ lk R - (locked γ R - |={}=> Φ #()%V) - WP acquire lk {{ Φ }})%I.
Proof.
iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
- iIntros "[Hlked HR]". iMod ("HΦ" with "[$Hlked $HR]"). by wp_pures.
- iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
Lemma release_spec γ lk R :
{{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l ->) "#Hinv". wp_lam.
iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
Typeclasses Opaque is_lock locked.
Markdown is supported
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