Skip to content

Commit

Permalink
using cancellable invariants for message pass
Browse files Browse the repository at this point in the history
  • Loading branch information
hei411 committed Oct 22, 2024
1 parent 80579d3 commit f8b4a43
Showing 1 changed file with 26 additions and 18 deletions.
44 changes: 26 additions & 18 deletions theories/coneris/examples/message_pass.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From iris.algebra Require Import excl_auth.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Export invariants cancelable_invariants.
From clutch.coneris Require Import coneris par spawn lib.flip.

Local Open Scope Z.
Expand All @@ -15,52 +15,60 @@ Definition prog (l:loc) : expr:=
else "y"
)%V !(#l))

);; !#l.
).

Section proof.
Context `{!conerisGS Σ, !spawnG Σ, inG Σ (excl_authR boolO)}.
Context `{!conerisGS Σ, !spawnG Σ, inG Σ (excl_authR boolO), cinvG Σ}.
Lemma prog_spec l:
{{{ ↯(/2)%R ∗ ∃ v, l↦v }}}
prog l
{{{
RET #0; True
v, RET v; l↦#0
}}}.
Proof.
iIntros (Φ) "[Herr [%v Hl]] HΦ".
rewrite /prog.
wp_store.
iMod (own_alloc (●E false ⋅ ◯E false)) as (γ) "[Hauth Hfrag]".
{ by apply excl_auth_valid. }
iMod (inv_alloc nroot _ (l↦#0 ∗ own γ (●E true) ∨ l↦ #(-1) ∗ own γ (●E false))%I with "[Hl Hauth]") as "#I"; first (iRight; iFrame).
iMod (cinv_alloc _ nroot (l↦#0 ∗ own γ (●E true) ∨ l↦ #(-1) ∗ own γ (●E false))%I with "[Hl Hauth]") as "[%γ1 [#I Hc]]"; first (iRight; iFrame).
wp_pures.
wp_apply (wp_par (λ _, own γ (◯E true))%I (λ _, True)%I with "[Herr Hfrag][]").
iDestruct "Hc" as "[Hc Hc']".
iApply pgl_wp_fupd.
wp_apply (wp_par (λ _, own γ (◯E true) ∗ cinv_own γ1 (1/2)%Qp)%I (λ _, cinv_own γ1 (1/2)%Qp)%I with "[Herr Hfrag Hc][Hc']").
- wp_apply (wp_flip_adv _ _ (λ x, if x then 0 else 1)%R with "[$]").
+ intros []; lra.
+ lra.
+ iIntros ([]) "Herr"; last by iDestruct (ec_contradict with "[$]") as "%".
wp_pures.
iInv "I" as ">[[H Hauth]|[H Hauth]]" "Hclose".
iMod (cinv_acc_strong with "[I] [$]") as "K"; [done|done|..].
iDestruct "K" as "[>[[H Hauth]|[H Hauth]] [Hc Hclose]]".
* iCombine "Hauth Hfrag" gives "%K". by apply excl_auth_agree_L in K.
* wp_store.
iMod (own_update_2 _ _ _ (●E true ⋅ ◯E true) with "Hauth Hfrag") as "[Hauth Hfrag]".
{ by apply excl_auth_update. }
iMod ("Hclose" with "[H Hauth]"); first (iLeft; iFrame). iModIntro. iFrame.
iMod ("Hclose" with "[H Hauth]"); first (iLeft; iLeft; iFrame).
iFrame.
by rewrite -union_difference_L.
- iLöb as "IH".
wp_bind (!_)%E.
iInv "I" as ">[[??]|[??]]" "Hclose".
iMod (cinv_acc_strong with "[I] [$]") as "K"; [done|done|..].
iDestruct "K" as "[>[[H Hauth]|[H Hauth]] [Hc Hclose]]".
+ wp_load.
iMod ("Hclose" with "[-]"); first (iLeft; iFrame).
iMod ("Hclose" with "[-Hc]"); first (iLeft; iLeft; iFrame).
rewrite -union_difference_L; last done.
iModIntro.
by wp_pures.
+ wp_load.
iMod ("Hclose" with "[-]"); first (iRight; iFrame).
iModIntro. wp_pures. iApply "IH".
- iIntros (??) "[Hfrag _]".
iNext. wp_pures.
iInv "I" as ">[[H Hauth]|[H Hauth]]" "Hclose".
+ wp_load.
iMod ("Hclose" with "[H Hauth]"); first (iLeft; iFrame). iModIntro.
by iApply "HΦ".
iMod ("Hclose" with "[-Hc]"); first (iLeft; iRight; iFrame).
rewrite -union_difference_L; last done.
iModIntro. wp_pures. by iApply "IH".
- iIntros (??) "[[Hfrag Hc] Hc']".
iCombine "Hc Hc'" as "Hc".
iNext.
iMod (cinv_cancel with "[][$]") as "H"; [done|done|].
iDestruct "H" as ">[[H Hauth]|[H Hauth]]".
+ iModIntro. by iApply "HΦ".
+ iCombine "Hauth Hfrag" gives "%K". by apply excl_auth_agree_L in K.
Qed.

Expand Down

0 comments on commit f8b4a43

Please sign in to comment.