Commit 20d58498 authored by Dan Frumin's avatar Dan Frumin

Get rid of some clutter in the counter refinement

parent 3aa70947
......@@ -7,122 +7,57 @@ From iris.program_logic Require Import adequacy.
From iris_logrel.F_mu_ref_conc Require Import hax.
Definition CG_increment : val := λ: "x" <>,
"x" <- BinOp Add (#n 1) (! "x").
Definition CG_locked_increment : val := λ: "x" "l" <>,
Definition CG_increment : val := λ: "x" "l" <>,
acquire "l";;
CG_increment "x" #();;
"x" <- BinOp Add (#n 1) (! "x");;
release "l".
Definition counter_read : val := λ: "x" <>, !"x".
Definition CG_counter_body : val := λ: "x" "l",
(CG_locked_increment "x" "l", counter_read "x").
Definition CG_counter : expr := Let "l" newlock
((λ: "x", CG_counter_body "x" "l") (Alloc (#n 0))).
Definition CG_counter : expr :=
let: "l" := newlock in
let: "x" := ref (#n 0) in
(CG_increment "x" "l", counter_read "x").
Definition FG_increment : val := λ: "v", rec: "inc" <> :=
Let "c" (!"v") (If (CAS "v" "c" (BinOp Add (#n 1) "c"))
(Unit)
("inc" #())).
Definition FG_counter_body : val := λ: "x",
(FG_increment "x", counter_read "x").
Definition FG_counter : expr :=
FG_counter_body (Alloc (#n 0)).
let: "x" := Alloc (#n 0) in
(FG_increment "x", counter_read "x").
Section CG_Counter.
Context `{heapIG Σ, cfgSG Σ}.
(* Coarse-grained increment *)
(* Coarse-grained increment *)
Lemma CG_increment_type Γ :
typed Γ CG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
Proof.
typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
Proof.
unfold CG_increment. unlock.
eauto 10 with typeable.
eauto 25 with typeable.
Qed.
Hint Resolve CG_increment_type : typeable.
Lemma steps_CG_increment E ρ j K x n:
nclose specN E
spec_ctx ρ - x ↦ₛ (#nv n)
- j fill K (CG_increment (Loc x) Unit)
={E}= j fill K (Lit Unit) x ↦ₛ (#nv (S n)).
Proof.
iIntros (HNE) "#Hspec Hx Hj".
unfold CG_increment. unlock. (*TODO: need an unlock :( *)
tp_rec j; simpl.
tp_rec j; simpl.
tp_load j.
tp_op j. tp_normalise j.
tp_store j.
by iFrame.
Qed.
Lemma bin_log_related_CG_increment_r Γ K E1 E2 x n t τ :
nclose specN E1
x ↦ₛ (#nv n) -
(x ↦ₛ (#nv (S n)) - {E1,E2;Γ} t log fill K (Lit Unit) : τ) -
{E1,E2;Γ} t log fill K (App (CG_increment (Loc x)) Unit) : τ.
Proof.
iIntros (?) "Hx Hlog".
unfold CG_increment. unlock; simpl.
rel_rec_r.
rel_rec_r.
rel_load_r.
rel_op_r.
rel_store_r.
by iApply "Hlog".
Qed.
Lemma CG_locked_increment_type Γ :
typed Γ CG_locked_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
Proof.
unfold CG_locked_increment. unlock.
eauto 25 with typeable.
Qed.
Hint Resolve CG_locked_increment_type : typeable.
Lemma steps_CG_locked_increment E ρ j K x n l :
nclose specN E
spec_ctx ρ - x ↦ₛ (#nv n) - l ↦ₛ (#v false)
- j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
={E}= j fill K (Lit Unit) x ↦ₛ (#nv S n) l ↦ₛ (#v false).
Proof.
iIntros (HNE) "#Hspec Hx Hl Hj".
unfold CG_locked_increment. unlock. (* TODO: unlock needed :( *)
tp_rec j; simpl. rewrite !Closed_subst_id.
tp_rec j; simpl. rewrite !Closed_subst_id.
tp_rec j; tp_normalise j.
tp_bind j (acquire #l).
tp_apply j (steps_acquire _ _ _ _ l) with "Hl" as "Hl". tp_normalise j.
tp_rec j; tp_normalise j.
tp_bind j ((CG_increment #x) #())%E.
tp_apply j steps_CG_increment with "Hx" as "$". tp_normalise j.
tp_rec j; tp_normalise j.
tp_apply j lock.steps_release with "Hl" as "$". (*TODO: remove steps_release from tactics.v *)
done.
Qed.
Lemma bin_log_related_CG_locked_increment_r Γ K E1 E2 t τ x n l :
Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ x n l :
nclose specN E1
(x ↦ₛ (#nv n) - l ↦ₛ (#v false) -
(x ↦ₛ (#nv S n) - l ↦ₛ (#v false) -
({E1,E2;Γ} t log fill K (Lit Unit) : τ)) -
{E1,E2;Γ} t log fill K (((CG_locked_increment $/ (LocV x)) $/ (LocV l)) Unit)%E : τ)%I.
{E1,E2;Γ} t log fill K ((CG_increment $/ LocV x $/ LocV l) Unit)%E : τ)%I.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_locked_increment. unlock. simpl.
unfold CG_increment. unlock. simpl.
rewrite !Closed_subst_id.
rel_rec_r.
rel_bind_r (acquire #l).
iApply (bin_log_related_acquire_r with "Hl"); eauto. iIntros "Hl". simpl.
rel_rec_r.
rel_bind_r (CG_increment #x #())%E.
iApply (bin_log_related_CG_increment_r with "Hx"); auto. simpl. iIntros "Hx".
rel_load_r.
rel_op_r.
rel_store_r. simpl.
rel_rec_r.
iApply (bin_log_related_release_r with "Hl"); eauto.
by iApply "Hlog".
......@@ -137,31 +72,6 @@ Section CG_Counter.
Hint Resolve counter_read_type : typeable.
Lemma steps_counter_read E ρ j K x n :
nclose specN E
spec_ctx ρ - x ↦ₛ (#nv n)
- j fill K (App (counter_read (Loc x)) Unit)
={E}= j fill K (#n n) x ↦ₛ (#nv n).
Proof.
intros HNE. iIntros "#Hspec Hx Hj". unfold counter_read. unlock.
tp_rec j. tp_normalise j.
tp_rec j. tp_normalise j.
tp_load j.
by iFrame.
Qed.
Lemma CG_counter_body_type Γ :
typed Γ CG_counter_body
(TArrow (Tref TNat)
(TArrow LockType
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)))).
Proof.
unfold CG_counter_body. unlock.
eauto 15 with typeable.
Qed.
Hint Resolve CG_counter_body_type : typeable.
Lemma CG_counter_type Γ :
typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
......@@ -211,17 +121,6 @@ Section CG_Counter.
by iApply "Hlog".
Qed.
Lemma FG_counter_body_type Γ :
typed Γ FG_counter_body
(TArrow (Tref TNat)
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
Proof.
unfold FG_counter_body. unlock.
eauto 15 with typeable.
Qed.
Hint Resolve FG_counter_body_type : typeable.
Lemma FG_counter_type Γ :
typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
......@@ -319,14 +218,14 @@ Section CG_Counter.
(* TODO: try to use with_lock rules *)
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
Γ FG_increment $/ LocV cnt log CG_locked_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
Γ FG_increment $/ LocV cnt log CG_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
Proof.
iIntros "#Hinv".
iApply bin_log_related_arrow.
{ unfold FG_increment. unlock; simpl. reflexivity. }
{ unfold CG_locked_increment. unlock; simpl. reflexivity. }
{ unfold CG_increment. unlock; simpl. reflexivity. }
{ unfold FG_increment. unlock; simpl. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
{ unfold CG_locked_increment. unlock; simpl.
{ unfold CG_increment. unlock; simpl.
rewrite !Closed_subst_id. solve_closed. }
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
......@@ -341,12 +240,12 @@ Section CG_Counter.
{ iNext. iExists _. iFrame. }
done.
- iIntros (m) "[Hcnt [Hl Hcnt']]".
iApply (bin_log_related_CG_locked_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj. }
iApply (bin_log_related_CG_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj. }
iIntros "Hcnt' Hl".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. iFrame. }
simpl.
iApply bin_log_related_unit.
by rel_vals.
Qed.
Lemma counter_read_refinement l cnt cnt' Γ :
......@@ -389,13 +288,8 @@ Section CG_Counter.
iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
iIntros (cnt) "Hcnt".
rel_rec_r.
unfold FG_counter_body. unlock.
rel_rec_l.
unfold CG_counter_body. unlock.
do 2 rel_rec_r.
rel_rec_r.
(* establishing the invariant *)
iAssert (counter_inv l cnt cnt')
......@@ -406,12 +300,12 @@ Section CG_Counter.
iApply (bin_log_related_pair _ with "[]").
- rel_rec_l.
rel_rec_r.
unfold CG_locked_increment. unlock; simpl. rewrite !Closed_subst_id.
unfold CG_increment. unlock; simpl. rewrite !Closed_subst_id.
rel_rec_r.
replace (λ: <>, acquire #l ;; (CG_increment #cnt') #() ;; release #l)%E
with (CG_locked_increment $/ LocV cnt' $/ LocV l)%E.
replace (λ: <>, acquire #l ;; #cnt' <- BinOp Add (Nat 1) (! #cnt');; release #l)%E
with (CG_increment $/ LocV cnt' $/ LocV l)%E.
iApply (FG_CG_increment_refinement with "Hinv").
{ unfold CG_locked_increment. unlock; simpl.
{ unfold CG_increment. unlock; simpl.
rewrite !Closed_subst_id. reflexivity. }
- rel_rec_l.
rel_rec_r.
......
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