Commit 58f5ee24 authored by Dan Frumin's avatar Dan Frumin

Update some examples

parent f2045770
......@@ -37,6 +37,8 @@ Definition FG_counter : expr :=
Section CG_Counter.
Context `{cfgSG Σ}.
Context `{heapIG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
......@@ -257,10 +259,11 @@ Section CG_Counter.
Lemma FG_CG_counter_refinement :
[] FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
iIntros (Δ [|??] ρ ?) "#(Hheap & Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
iIntros (Δ [|??] ρ ?) "#(Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_counter CG_counter].
rewrite ?empty_env_subst /CG_counter /FG_counter.
iApply fupd_wp.
iMod (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) _ with "[Hj]")
as (l) "[Hj Hl]"; eauto.
{ rewrite fill_app /=. by iFrame. }
......@@ -278,13 +281,14 @@ Section CG_Counter.
Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end.
all: trivial.
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply (wp_alloc with "[]"); trivial; iFrame "#"; iNext; iIntros (cnt) "Hcnt /=".
iApply (wp_bind [AppRCtx (RecV _)]).
iApply wp_wand_l. iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply (wp_alloc); trivial; iFrame "#"; iNext; iIntros (cnt) "Hcnt /=".
(* establishing the invariant *)
iAssert (( n, l ↦ₛ (#v false) cnt ↦ᵢ (#nv n) cnt' ↦ₛ (#nv n) )%I)
with "[Hl Hcnt Hcnt']" as "Hinv".
{ iExists _. by iFrame. }
iApply fupd_wp.
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
{ iNext; iExact "Hinv". }
(* splitting increment and read *)
......@@ -305,11 +309,12 @@ Section CG_Counter.
(* fine-grained reads the counter *)
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply wp_atomic; eauto.
iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
iApply (wp_load with "[Hcnt]"); [|iFrame; iFrame "#"|]. solve_ndisj.
iApply (wp_load with "[Hcnt]"); [iNext; by iFrame|].
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'"; trivial. }
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
iApply wp_rec; trivial. asimpl. iNext.
(* fine-grained performs increment *)
iApply (wp_bind [IfCtx _ _; CasRCtx (LocV _) (NatV _)]);
......@@ -318,6 +323,7 @@ Section CG_Counter.
iNext. iModIntro.
iApply (wp_bind [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply wp_atomic; eauto.
iInv counterN as (n') ">[Hl [Hcnt Hcnt']]" "Hclose".
(* performing CAS *)
destruct (decide (n = n')) as [|Hneq]; subst.
......@@ -326,19 +332,20 @@ Section CG_Counter.
iMod (steps_CG_locked_increment
_ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iApply (wp_cas_suc with "[Hcnt]"); trivial; [|iFrame; iFrame "Hheap"|].
solve_ndisj. iNext. iIntros "Hcnt".
iApply (wp_cas_suc with "[Hcnt]"); auto.
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'"; trivial. }
simpl.
iApply wp_if_true. iNext. iApply wp_value; trivial.
iExists UnitV; iFrame; auto.
+ (* CAS fails *)
(* In this case, we perform a recursive call *)
iApply (wp_cas_fail _ _ _ (#nv n') with "[Hcnt]"); simpl; trivial;
[inversion 1; subst; auto | | iFrame; iFrame "Hheap"|]. solve_ndisj.
iApply (wp_cas_fail _ _ _ (#nv n') with "[Hcnt]"); auto;
[inversion 1; subst; auto | ].
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _; iFrame "Hl Hcnt Hcnt'"; trivial. }
{ iNext. iExists _; iFrame "Hl Hcnt Hcnt'". }
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of read *)
iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj".
......@@ -347,14 +354,15 @@ Section CG_Counter.
Transparent counter_read.
unfold counter_read at 2.
iApply wp_rec; trivial. simpl.
iNext. iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
iMod (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']".
{ solve_ndisj. }
iNext.
iApply wp_atomic; eauto.
iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
iMod (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']"; first by solve_ndisj.
{ by iFrame "Hspec Hcnt' Hj". }
iApply (wp_load with "[Hcnt]"); [|iFrame; iFrame "Hheap"|]. solve_ndisj.
iApply (wp_load with "[Hcnt]"); eauto.
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _; iFrame "Hl Hcnt Hcnt'"; trivial. }
{ iNext. iExists _; iFrame "Hl Hcnt Hcnt'". }
iExists (#nv _); eauto.
Unshelve. solve_ndisj.
Qed.
......@@ -364,7 +372,8 @@ Theorem counter_ctx_refinement :
[] FG_counter ctx CG_counter :
TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
set (Σ := #[irisΣ state; auth.authΣ heapUR; auth.authΣ cfgUR]).
eapply (binary_soundness Σ);
auto using FG_counter_closed, CG_counter_closed, FG_CG_counter_refinement.
set (Σ := #[invΣ ; gen_heapΣ loc val ; authΣ cfgUR]).
set (HG := soundness_unary.HeapPreIG Σ _ _).
eapply (binary_soundness Σ _); auto.
intros. apply FG_CG_counter_refinement.
Qed.
......@@ -2,11 +2,14 @@ From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.base_logic Require Import namespaces.
(** [newlock = alloc false] *)
Definition newlock : expr := Alloc (# false).
(** [acquire = λ x. if cas(x, false, true) then #() else acquire(x) ] *)
Definition acquire : expr :=
Rec (If (CAS (Var 1) (# false) (# true)) (Unit) (App (Var 0) (Var 1))).
(** [release = λ x. x <- false] *)
Definition release : expr := Rec (Store (Var 1) (# false)).
(** [with_lock e l = λ x. (acquire l) ;; e x ;; (release l)] *)
Definition with_lock (e : expr) (l : expr) : expr :=
Rec
(App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)])))
......@@ -76,7 +79,8 @@ Qed.
Section proof.
Context `{cfgSG Σ}.
Context `{heapIG Σ}.
Lemma steps_newlock E ρ j K :
nclose specN E
spec_ctx ρ j fill K newlock
......
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