Commit cac30916 authored by Dan Frumin's avatar Dan Frumin

Port the lock & counter examples to tp_tactics

parent 1f632bb2
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_logrel.F_mu_ref_conc Require Import tactics soundness_binary.
From iris.program_logic Require Import adequacy.
Definition CG_increment (x : expr) : expr :=
......@@ -66,22 +66,11 @@ Section CG_Counter.
|={E}=> j fill K (Unit) x ↦ₛ (#nv (S n)).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iMod (step_load _ _ j (K ++ [StoreRCtx (LocV _); BinOpRCtx _ (#nv _)])
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial.
rewrite ?fill_app. simpl.
iMod (step_nat_binop _ _ j (K ++ [StoreRCtx (LocV _)])
_ _ _ with "[Hj]") as "Hj"; eauto.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial. simpl.
rewrite ?fill_app. simpl.
iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
iFrame "Hspec Hj"; trivial.
iModIntro.
iFrame "Hj Hx"; trivial.
Unshelve. all: trivial.
tp_rec j.
tp_load j.
tp_op j. tp_normalise j.
tp_store j. tp_normalise j.
by iFrame.
Qed.
Global Opaque CG_increment.
......@@ -127,8 +116,7 @@ Section CG_Counter.
={E}= j fill K Unit x ↦ₛ (#nv S n) l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
iMod (steps_with_lock
_ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last done.
iMod (steps_with_lock _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last by iFrame.
- iIntros (K') "[#Hspec [Hx Hj]]".
iApply steps_CG_increment; first done. iFrame "Hspec Hj Hx"; trivial.
- by iFrame "Hspec Hj Hx".
......@@ -167,11 +155,9 @@ Section CG_Counter.
={E}= j fill K (#n n) x ↦ₛ (#nv n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iMod (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
asimpl.
iMod (step_load _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto.
{ by iFrame "Hspec Hj". }
iModIntro. by iFrame "Hj Hx".
tp_rec j.
tp_load j. tp_normalise j.
by iFrame.
Qed.
Opaque counter_read.
......@@ -268,22 +254,16 @@ Section CG_Counter.
as (l) "[Hj Hl]"; eauto.
{ rewrite fill_app /=. by iFrame. }
rewrite fill_app /=.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
tp_rec j.
asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
iMod (step_alloc _ _ j (K ++ [AppRCtx (RecV _)]) _ _ _ _ with "[Hj]")
as (cnt') "[Hj Hcnt']"; eauto.
{ rewrite fill_app; simpl. by iFrame. }
rewrite fill_app; simpl.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
tp_alloc j as cnt' "Hcnt'". tp_normalise j.
tp_rec j. tp_normalise j.
asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
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); trivial; iFrame "#"; iNext; iIntros (cnt) "Hcnt /=".
iModIntro. wp_bind (Alloc _).
iApply wp_alloc; eauto. 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".
......@@ -307,8 +287,7 @@ Section CG_Counter.
iLöb as "Hlat".
iApply wp_rec; trivial. asimpl. iNext.
(* fine-grained reads the counter *)
iApply (wp_bind [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
wp_bind (Load _).
iApply wp_atomic; eauto.
iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
iApply (wp_load with "[Hcnt]"); [iNext; by iFrame|].
......@@ -317,12 +296,10 @@ Section CG_Counter.
{ iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
iApply wp_rec; trivial. asimpl. iNext.
(* fine-grained performs increment *)
iApply (wp_bind [IfCtx _ _; CasRCtx (LocV _) (NatV _)]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
wp_bind (BinOp Add _ _).
iApply wp_nat_binop; simpl.
iNext. iModIntro.
iApply (wp_bind [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
wp_bind (CAS _ _ _).
iApply wp_atomic; eauto.
iInv counterN as (n') ">[Hl [Hcnt Hcnt']]" "Hclose".
(* performing CAS *)
......@@ -357,14 +334,13 @@ Section CG_Counter.
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". }
iMod (steps_counter_read with "[$Hspec $Hj $Hcnt']") as "[Hj Hcnt']"; first by solve_ndisj.
iApply (wp_load with "[Hcnt]"); eauto.
iNext. iIntros "Hcnt".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _; iFrame "Hl Hcnt Hcnt'". }
iExists (#nv _); eauto.
Unshelve. solve_ndisj.
Unshelve. all: solve_ndisj.
Qed.
End CG_Counter.
......
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.base_logic Require Import namespaces.
......@@ -87,7 +88,8 @@ Section proof.
|={E}=> l, j fill K (Loc l) l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec Hj]".
by iMod (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
tp_alloc j as l "Hl". tp_normalise j.
by iExists _; iFrame.
Qed.
Global Opaque newlock.
......@@ -98,15 +100,10 @@ Section proof.
|={E}=> j fill K Unit l ↦ₛ (#v true).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
iMod (step_cas_suc _ _ j (K ++ [IfCtx _ _])
_ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
{ rewrite fill_app /=. iFrame "Hspec Hj Hl"; eauto. }
rewrite fill_app /=.
iMod (step_if_true _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
{ by iFrame. }
by iIntros "!> {$Hj $Hl}".
Unshelve. all:trivial.
tp_rec j.
tp_cas_suc j.
tp_if_true j. tp_normalise j.
by iFrame.
Qed.
Global Opaque acquire.
......@@ -117,11 +114,9 @@ Section proof.
|={E}=> j fill K Unit l ↦ₛ (#v false).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release.
iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done.
iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
{ by iFrame. }
by iIntros "!> {$Hj $Hl}".
Unshelve. all: trivial.
tp_rec j.
tp_store j. tp_normalise j.
by iFrame.
Qed.
Global Opaque release.
......@@ -136,28 +131,23 @@ Section proof.
|={E}=> j fill K (of_val v) Q l ↦ₛ (#v false).
Proof.
iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]".
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
tp_rec j; eauto using to_of_val.
asimpl. rewrite H1.
iMod (steps_acquire _ _ j (K ++ [AppRCtx (RecV _)])
_ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
{ rewrite fill_app /=. iFrame "Hspec Hj Hl"; eauto. }
rewrite fill_app; simpl.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
(* TODO: a tp_apply tactic similar to that of iApply *)
tp_bind j (App acquire (Loc l)).
iMod (steps_acquire _ _ j with "[$Hspec $Hj $Hl]") as "[Hj Hl]"; eauto.
tp_rec j.
asimpl. rewrite H1.
iMod (H2 (K ++ [AppRCtx (RecV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto.
{ rewrite fill_app /=. iFrame "Hspec Hj HP"; eauto. }
rewrite ?fill_app /=.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
tp_bind j (App e _).
iMod (H2 with "[$Hspec $Hj $HP]") as "[Hj HQ]".
tp_normalise j.
tp_rec j; eauto using to_of_val.
asimpl.
iMod (steps_release _ _ j (K ++ [AppRCtx (RecV _)]) _ _ with "[Hj Hl]")
as "[Hj Hl]"; eauto.
{ rewrite fill_app /=. by iFrame. }
rewrite ?fill_app /=.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. iModIntro; by iFrame.
Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end.
trivial.
tp_bind j (App release _).
iMod (steps_release with "[$Hspec $Hj $Hl]") as "[Hj Hl]"; auto.
tp_rec j.
tp_normalise j. asimpl.
by iFrame.
Qed.
Global Opaque with_lock.
......
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