Commit be63cb7e authored by Dan Frumin's avatar Dan Frumin

The `increment` fn in the counter module returns the previous value

parent bf3aca9a
......@@ -4,8 +4,10 @@ From iris_logrel.examples Require Import lock.
Definition CG_increment : val := λ: "x" "l" <>,
acquire "l";;
"x" <- #1 + !"x";;
release "l".
let: "n" := !"x" in
"x" <- #1 + "n";;
release "l";;
"n".
Definition counter_read : val := λ: "x" <>, !"x".
......@@ -17,7 +19,7 @@ Definition CG_counter : val := λ: <>,
Definition FG_increment : val := λ: "v", rec: "inc" <> :=
let: "c" := !"v" in
if: CAS "v" "c" (#1 + "c")
then #()
then "c"
else "inc" #().
Definition FG_counter : val := λ: <>,
......@@ -30,7 +32,7 @@ Section CG_Counter.
(* Coarse-grained increment *)
Lemma CG_increment_type Γ :
typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TNat))).
Proof. solve_typed. Qed.
Hint Resolve CG_increment_type : typeable.
......@@ -39,7 +41,7 @@ Section CG_Counter.
nclose specN E1
(x ↦ₛ # n - l ↦ₛ #false -
(x ↦ₛ # (S n) - l ↦ₛ #false -
({E1,E2;Δ;Γ} t log fill K #() : τ)) -
({E1,E2;Δ;Γ} t log fill K #n : τ)) -
{E1,E2;Δ;Γ} t log fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hl Hlog".
......@@ -49,10 +51,25 @@ Section CG_Counter.
iIntros "Hl".
rel_rec_r.
rel_load_r.
rel_let_r.
rel_op_r.
rel_store_r.
rel_rec_r.
rel_apply_r (bin_log_related_release_r with "Hl"); eauto.
iIntros "Hl". rel_seq_r.
by iApply ("Hlog" with "Hx Hl").
Qed.
Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ
(Hspec : nclose specN E1) :
x ↦ₛ #n -
(x ↦ₛ #n - {E1,E2;Δ;Γ} t log fill K #n : τ) -
{E1,E2;Δ;Γ} t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
Proof.
iIntros "Hx Hlog".
unfold counter_read. unlock. simpl.
rel_rec_r.
rel_load_r.
by iApply "Hlog".
Qed.
......@@ -63,48 +80,27 @@ Section CG_Counter.
Hint Resolve counter_read_type : typeable.
Lemma CG_counter_type Γ :
typed Γ CG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
typed Γ CG_counter (TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat))).
Proof. solve_typed. Qed.
Hint Resolve CG_counter_type : typeable.
(* Fine-grained increment *)
Lemma FG_increment_type Γ :
typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TNat)).
Proof. solve_typed. Qed.
Hint Resolve FG_increment_type : typeable.
Lemma bin_log_FG_increment_l Γ K E x (n : nat) t τ :
x ↦ᵢ #n -
(x ↦ᵢ # (S n) - {E;Δ;Γ} fill K #() log t : τ) -
{E;Δ;Γ} fill K (FG_increment #x #()) log t : τ.
Proof.
iIntros "Hx Hlog".
iApply bin_log_related_wp_l.
wp_bind (FG_increment #x).
unfold FG_increment. unlock.
wp_rec.
wp_rec.
wp_load.
wp_rec.
wp_binop.
wp_bind (CAS _ _ _).
iApply (wp_cas_suc with "[Hx]"); auto.
iNext. iIntros "Hx".
wp_if.
by iApply "Hlog".
Qed.
Lemma bin_log_FG_increment_r Γ K E1 E2 t τ (x : loc) (n : nat) :
Lemma bin_log_related_FG_increment_r Γ K E1 E2 t τ (x : loc) (n : nat) :
nclose specN E1
(x ↦ₛ # n -
(x ↦ₛ #(S n) -
{E1,E2;Δ;Γ} t log fill K #() : τ) -
{E1,E2;Δ;Γ} t log fill K #n : τ) -
{E1,E2;Δ;Γ} t log fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hlog".
unfold FG_increment. unlock. simpl_subst/=.
unlock FG_increment. simpl_subst/=.
rel_seq_r.
rel_load_r; rel_seq_r.
rel_op_r.
......@@ -114,7 +110,7 @@ Section CG_Counter.
Qed.
Lemma FG_counter_type Γ :
typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat))).
Proof. solve_typed. Qed.
Hint Resolve FG_counter_type : typeable.
......@@ -124,19 +120,6 @@ Section CG_Counter.
Definition counter_inv l cnt cnt' : iProp Σ :=
( n : nat, l ↦ₛ #false cnt ↦ᵢ #n cnt' ↦ₛ #n)%I.
Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ
(Hspec : nclose specN E1) :
x ↦ₛ #n -
(x ↦ₛ #n - {E1,E2;Δ;Γ} t log fill K #n : τ) -
{E1,E2;Δ;Γ} t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
Proof.
iIntros "Hx Hlog".
unfold counter_read. unlock. simpl.
rel_rec_r.
rel_load_r.
by iApply "Hlog".
Qed.
(* A logically atomic specification for
a fine-grained increment with a baked in frame. *)
(* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *)
......@@ -145,7 +128,7 @@ Section CG_Counter.
(|={E1,E2}=> n : nat, x ↦ᵢ #n R n
(( n : nat, x ↦ᵢ #n R n) ={E2,E1}= True)
( m, x ↦ᵢ # (S m) R m - P -
{E2,E1;Δ;Γ} fill K #() log t : τ))
{E2,E1;Δ;Γ} fill K #m log t : τ))
- ({E1;Δ;Γ} fill K ((FG_increment $/ LitV (Loc x)) #()) log t : τ).
Proof.
iIntros "HP #H".
......@@ -183,14 +166,15 @@ Section CG_Counter.
Qed.
(* A similar atomic specification for the counter_read fn *)
Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ :
Lemma bin_log_counter_read_atomic_l R P Γ E1 E2 K x t τ :
P -
(|={E1,E2}=> n : nat, x ↦ᵢ #n R n
(( n : nat, x ↦ᵢ #n R n) ={E2,E1}= True)
( m : nat, x ↦ᵢ #m R m -
( m : nat, x ↦ᵢ #m R m - P -
{E2,E1;Δ;Γ} fill K #m log t : τ))
- {E1;Δ;Γ} fill K ((counter_read $/ LitV (Loc x)) #()) log t : τ.
Proof.
iIntros "#H".
iIntros "HP #H".
unfold counter_read. unlock. simpl.
rel_rec_l.
rel_load_l_atomic.
......@@ -198,71 +182,82 @@ Section CG_Counter.
iExists _; iFrame "Hx". iNext.
iIntros "Hx".
iDestruct "Hfin" as "[_ Hfin]".
iApply "Hfin". by iFrame.
iApply ("Hfin" with "[Hx HR] HP"). by iFrame.
Qed.
(* TODO: try to use with_lock rules *)
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
{Δ;Γ} FG_increment $/ LitV (Loc cnt) log CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l) : TArrow TUnit TUnit.
{Δ;Γ} FG_increment #cnt log CG_increment #cnt' #l : TArrow TUnit TNat.
Proof.
iIntros "#Hinv".
rel_rec_l.
unlock CG_increment.
do 2 rel_rec_r.
replace (λ: <>, acquire #l;; let: "n" := ! #cnt' in #cnt' <- #1 + "n";; release #l;; "n")%E
with (CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l))%E; last first.
{ unlock CG_increment. by simpl_subst/=. }
iApply bin_log_related_arrow_val.
{ unfold FG_increment. unlock; simpl_subst. reflexivity. }
{ unfold CG_increment. unlock; simpl_subst. reflexivity. }
{ unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
{ unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) cnt' ↦ₛ #n)%I True%I _ _ _ [] cnt with "[Hinv]"); auto.
iAlways.
iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
iExists n. iFrame. clear n.
iAlways. iIntros (v v') "[% %]"; simplify_eq/=.
rel_apply_l
(bin_log_FG_increment_logatomic
(fun n => (l ↦ₛ #false) cnt' ↦ₛ #n)%I
True%I); first done.
iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')".
iExists _; iFrame. clear n.
iSplit.
- iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. iFrame. }
done.
- iIntros (m) "[Hcnt [Hl Hcnt']] _".
iApply (bin_log_related_CG_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj. }
- iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')".
iApply ("Hcl" with "[-]").
iNext. iExists _. iFrame.
- iIntros (m) "(Hcnt & Hl & Hcnt') _".
rel_apply_r (bin_log_related_CG_increment_r with "Hcnt' Hl").
{ solve_ndisj. }
iIntros "Hcnt' Hl".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. iFrame. }
simpl.
by rel_vals.
{ iNext. iExists _. iFrame. }
by iApply bin_log_related_nat.
Qed.
Lemma counter_read_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
{Δ;Γ} counter_read $/ LitV (Loc cnt) log counter_read $/ LitV (Loc cnt') : TArrow TUnit TNat.
Proof.
{Δ;Γ} counter_read #cnt log counter_read #cnt' : TArrow TUnit TNat.
Proof.
iIntros "#Hinv".
rel_rec_l. rel_rec_r.
iApply bin_log_related_arrow_val.
{ unfold counter_read. unlock. simpl. reflexivity. }
{ unfold counter_read. unlock. simpl. reflexivity. }
{ unfold counter_read. unlock. simpl. solve_closed. }
{ unfold counter_read. unlock. simpl. solve_closed. }
iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ #false) cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]").
rel_apply_l
(bin_log_counter_read_atomic_l
(fun n => (l ↦ₛ #false) cnt' ↦ₛ #n)%I
True%I); first done.
iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists n. iFrame "Hcnt Hcnt' Hl". clear n.
iSplit.
- iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". iApply "Hclose".
iNext. iExists n. by iFrame.
- iIntros (m) "(Hcnt & Hl & Hcnt') /=".
iApply (bin_log_counter_read_r _ _ _ [] with "Hcnt'").
- iIntros (m) "(Hcnt & Hl & Hcnt') _ /=".
rel_apply_r (bin_log_counter_read_r with "Hcnt'").
{ solve_ndisj. }
iIntros "Hcnt'".
iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
{ iNext. iExists _. by iFrame. }
rel_vals. simpl. eauto.
by iApply bin_log_related_nat.
Qed.
Lemma FG_CG_counter_refinement :
{Δ;} FG_counter log CG_counter :
TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
Proof.
unfold FG_counter, CG_counter.
iApply bin_log_related_arrow; try by (unlock; eauto).
......@@ -283,24 +278,15 @@ Section CG_Counter.
{ iExists _. by iFrame. }
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
iApply (bin_log_related_pair _ with "[]").
- rel_rec_l.
unlock CG_increment.
rel_rec_r.
rel_rec_r.
replace (λ: <>, acquire # l ;; #cnt' <- #1 + (! #cnt');; release # l)%E
with (CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l))%E; last first.
{ unfold CG_increment. unlock; simpl_subst/=. reflexivity. }
iApply (FG_CG_increment_refinement with "Hinv").
- rel_rec_l.
rel_rec_r.
iApply (counter_read_refinement with "Hinv").
iApply bin_log_related_pair.
- iApply (FG_CG_increment_refinement with "Hinv").
- iApply (counter_read_refinement with "Hinv").
Qed.
End CG_Counter.
Theorem counter_ctx_refinement :
FG_counter ctx CG_counter :
TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
Proof.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
apply FG_CG_counter_refinement.
......
......@@ -84,7 +84,7 @@ Section namegen_refinement.
iInv N as (n L) "(HB & Hc & HL)" "Hcl".
iModIntro. iNext. iIntros (l') "Hl'".
rel_rec_r.
rel_apply_r (bin_log_FG_increment_r with "Hc").
rel_apply_r (bin_log_related_FG_increment_r with "Hc").
{ solve_ndisj. }
iIntros "Hc".
rel_seq_r.
......
......@@ -374,24 +374,6 @@ Section refinement.
(c1 ↦ᵢ #(S n) c2 ↦ₛ #n shot γ own γ' (Excl ())))%I.
Program Definition TRV : D := λne _, True%I.
Lemma bin_log_related_FG_increment_r Δ Γ K E1 E2 t τ (x : loc) (n : nat) :
nclose specN E1
(x ↦ₛ # n -
(x ↦ₛ # (S n) -
({E1,E2;Δ;Γ} t log fill K #() : τ)) -
{E1,E2;Δ;Γ} t log fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hlog".
unlock FG_increment. simpl_subst/=.
rel_rec_r.
rel_load_r.
rel_rec_r. rel_op_r.
rel_cas_suc_r.
rel_if_r.
by iApply "Hlog".
Qed.
Lemma profiled_g `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
inv shootN (i6 c1 c2 γ γ') -
τg Δ (g1, g2) -
......
......@@ -52,7 +52,7 @@ Section liftings.
Lemma counter_atomic x E1 E2 Δ Γ :
atomic_logrel
(fun (n : nat) => x ↦ᵢ #n)%I
(fun (n : nat) (v : val) => v = #() x ↦ᵢ #(S n))%I
(fun (n : nat) (v : val) => v = #n x ↦ᵢ #(S n))%I
E2 E1
((FG_increment $/ LitV (Loc x)) #())
Δ Γ.
......@@ -65,8 +65,7 @@ Section liftings.
- iDestruct "Hlog" as "[Hlog _]". done.
- iDestruct "Hlog" as "[_ Hlog]".
iIntros (m) "[Hx HR1] HR2".
iSpecialize ("Hlog" $! m #()). simpl.
iApply "Hlog". by iFrame.
iApply ("Hlog" $! m #m). by iFrame.
Qed.
Lemma lift_atomic_ht {A : Type} (α : A iProp Σ) β Ei Eo e Δ
......@@ -122,7 +121,7 @@ Section liftings.
(* Increment refinement using the log atomic triple *)
Lemma FG_CG_increment_refinement2 l cnt cnt' Γ Δ :
inv counterN (counter_inv l cnt cnt') -
{Δ;Γ} FG_increment $/ LitV (Loc cnt) log CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l) : TArrow TUnit TUnit.
{Δ;Γ} FG_increment $/ LitV (Loc cnt) log CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l) : TArrow TUnit TNat.
Proof.
iIntros "#Hinv".
iApply bin_log_related_arrow_val.
......@@ -134,7 +133,7 @@ Section liftings.
iAlways. iIntros (v v') "[% %]"; simplify_eq/=.
pose (F := (fun (n : nat) => (l ↦ₛ #false) cnt' ↦ₛ #n)%I).
iPoseProof (counter_atomic cnt ( counterN) Δ Γ
$! [] _ TUnit True%I F)
$! [] _ _ True%I F)
as "Hrule /=".
iApply "Hrule". iSplitR; first done. iAlways.
iInv counterN as ">Hcnt" "Hcl". iModIntro.
......@@ -152,8 +151,7 @@ Section liftings.
iMod ("Hcl" with "[-]").
{ iNext. iExists _. iFrame. }
simpl.
by rel_vals.
by iApply bin_log_related_nat.
Qed.
End liftings.
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