Commit 1999bbc7 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc clean up in counter.

parent cd2f9a5d
......@@ -4,14 +4,43 @@ From iris_logrel.F_mu_ref_par Require Import lang examples.lock typing
soundness_binary context_refinement.
Import uPred.
Definition CG_increment (x : expr) : expr :=
Lam (Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)]))).
Definition CG_locked_increment (x l : expr) : expr :=
with_lock (CG_increment x) l.
Definition CG_locked_incrementV (x l : expr) : val :=
with_lockV (CG_increment x) l.
Definition counter_read (x : expr) : expr := Lam (Load x.[ren (+2)]).
Definition counter_readV (x : expr) : val := LamV (Load x.[ren (+2)]).
Definition CG_counter_body (x l : expr) : expr :=
Pair (CG_locked_increment x l) (counter_read x).
Definition CG_counter : expr :=
App
(Lam $ App (Lam (CG_counter_body (Var 1) (Var 3)))
(Alloc ( 0)))
newlock.
Definition FG_increment (x : expr) : expr :=
Lam $ App
(Lam $
(* try increment *)
If (CAS x.[ren (+4)] (Var 1) (BinOp Add ( 1) (Var 1)))
Unit (* increment succeeds we return unit *)
(App (Var 2) (Var 3)) (* increment fails, we try again *))
(Load x.[ren (+2)]) (* read the counter *).
Definition FG_counter_body (x : expr) : expr :=
Pair (FG_increment x) (counter_read x).
Definition FG_counter : expr :=
App (Lam (FG_counter_body (Var 1))) (Alloc ( 0)).
Section CG_Counter.
Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
(* Coarse-grained increment *)
Definition CG_increment (x : expr) : expr :=
Lam ((Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)])))).
Lemma CG_increment_type x Γ :
typed Γ x (Tref TNat)
typed Γ (CG_increment x) (TArrow TUnit TUnit).
......@@ -56,11 +85,6 @@ Section CG_Counter.
Global Opaque CG_increment.
Definition CG_locked_increment (x l : expr) :=
with_lock (CG_increment x) l.
Definition CG_locked_incrementV (x l : expr) : val :=
with_lockV (CG_increment x) l.
Lemma CG_locked_increment_to_val x l :
to_val (CG_locked_increment x l) = Some (CG_locked_incrementV x l).
Proof. by rewrite with_lock_to_val. Qed.
......@@ -98,92 +122,77 @@ Section CG_Counter.
Lemma steps_CG_locked_increment N E ρ j K x n l :
nclose N E
Spec_ctx N ρ x ↦ₛ (v n) l ↦ₛ (v false)
j fill K (App
(CG_locked_increment (Loc x) (Loc l)) Unit)
={E}=> j fill K Unit x ↦ₛ (v S n) l ↦ₛ (v false).
j fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
={E}=> j fill K Unit x ↦ₛ (v S n) l ↦ₛ (v false).
Proof.
iIntros {HNE} "[#Hspec [Hx [Hl Hj]]]".
iPvs (steps_with_lock
_ _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; last done.
- iIntros {K'} "[#Hspec [Hx Hj]]".
iApply steps_CG_increment; first done. iFrame "Hspec Hj Hx"; trivial.
- iFrame "Hspec Hj Hx"; trivial.
- by iFrame "Hspec Hj Hx".
Unshelve. all: trivial.
Qed.
Global Opaque CG_locked_increment.
Definition counter_read (x : expr) : expr := (Lam (Load x.[ren (+2)])).
Definition counter_readV (x : expr) : val := (LamV (Load x.[ren (+2)])).
Lemma counter_read_to_val x: to_val (counter_read x) = Some (counter_readV x).
Lemma counter_read_to_val x : to_val (counter_read x) = Some (counter_readV x).
Proof. trivial. Qed.
Lemma counter_read_of_val x: of_val (counter_readV x) = counter_read x.
Lemma counter_read_of_val x : of_val (counter_readV x) = counter_read x.
Proof. trivial. Qed.
Global Opaque counter_readV.
Lemma counter_read_type x Γ :
typed Γ x (Tref TNat)
typed Γ (counter_read x) (TArrow TUnit TNat).
typed Γ x (Tref TNat) typed Γ (counter_read x) (TArrow TUnit TNat).
Proof.
intros H1. repeat econstructor.
eapply (context_weakening [_; _]); trivial.
Qed.
Lemma counter_read_closed (x : expr) :
( f, x.[f] = x)
f, (counter_read x).[f] = counter_read x.
( f, x.[f] = x) f, (counter_read x).[f] = counter_read x.
Proof. intros H1 f. asimpl. unfold counter_read. by rewrite ?H1. Qed.
Lemma counter_read_subst (x: expr) f :
(counter_read x).[f] = counter_read x.[f].
(counter_read x).[f] = counter_read x.[f].
Proof. unfold counter_read. by asimpl. Qed.
Lemma steps_counter_read N E ρ j K x n :
nclose N E
Spec_ctx N ρ x ↦ₛ (v n)
j fill K (App (counter_read (Loc x)) Unit)
={E}=> j fill K ( n) x ↦ₛ (v n).
={E}=> j fill K ( n) x ↦ₛ (v n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iPvs (step_lam _ _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
asimpl.
iPvs (step_load _ _ _ j K _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
iFrame "Hspec Hj"; trivial.
iPvsIntro. iFrame "Hj Hx"; trivial.
Unshelve. all: trivial.
iPvs (step_load _ _ _ j K with "[Hj Hx]") as "[Hj Hx]"; eauto.
{ by iFrame "Hspec Hj". }
iPvsIntro. by iFrame "Hj Hx".
Qed.
Opaque counter_read.
Definition CG_counter_body (x l : expr) : expr :=
Pair (CG_locked_increment x l) (counter_read x).
Lemma CG_counter_body_type x l Γ :
typed Γ x (Tref TNat)
typed Γ l LockType
typed Γ (CG_counter_body x l)
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
intros H1 H2; repeat econstructor;
eauto using CG_locked_increment_type, counter_read_type.
Qed.
Lemma CG_counter_body_closed (x l : expr) :
( f, x.[f] = x)
( f, l.[f] = l)
( f, x.[f] = x) ( f, l.[f] = l)
f, (CG_counter_body x l).[f] = CG_counter_body x l.
Proof.
intros H1 H2 f. asimpl.
rewrite CG_locked_increment_closed; trivial. by rewrite counter_read_closed.
Qed.
Definition CG_counter : expr :=
App (Lam (App (Lam (CG_counter_body (Var 1) (Var 3)))
(Alloc ( 0)))) newlock.
Lemma CG_counter_type Γ :
typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
......@@ -199,17 +208,6 @@ Section CG_Counter.
Qed.
(* Fine-grained increment *)
Definition FG_increment (x : expr) : expr :=
Lam (App (Lam
(* try increment *)
(If (CAS x.[ren (+4)] (Var 1) (BinOp Add ( 1) (Var 1)))
Unit (* increment succeeds we return unit *)
(App (Var 2) (Var 3)) (* increment fails, we try again *)
)
)
(Load x.[ren (+2)]) (* read the counter *)
).
Lemma FG_increment_type x Γ :
typed Γ x (Tref TNat)
typed Γ (FG_increment x) (TArrow TUnit TUnit).
......@@ -228,13 +226,10 @@ Section CG_Counter.
( f, x.[f] = x) f, (FG_increment x).[f] = FG_increment x.
Proof. intros H f. asimpl. unfold FG_increment. rewrite ?H; trivial. Qed.
Definition FG_counter_body (x : expr) : expr :=
Pair (FG_increment x) (counter_read x).
Lemma FG_counter_body_type x Γ :
typed Γ x (Tref TNat)
typed Γ (FG_counter_body x)
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
intros H1; econstructor.
- apply FG_increment_type; trivial.
......@@ -249,9 +244,6 @@ Section CG_Counter.
rewrite ?H1. by rewrite counter_read_closed.
Qed.
Definition FG_counter : expr :=
App (Lam (FG_counter_body (Var 1))) (Alloc ( 0)).
Lemma FG_counter_type Γ :
typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
......@@ -259,8 +251,7 @@ Section CG_Counter.
constructor. apply FG_counter_body_type; by constructor.
Qed.
Lemma FG_counter_closed f :
FG_counter.[f] = FG_counter.
Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed.
Ltac prove_disj N n n' :=
......@@ -269,63 +260,56 @@ Section CG_Counter.
assert (Hneq : n n') by omega;
set (Hdsj := ndot_ne_disjoint N n n' Hneq); set_solver_ndisj.
Lemma FG_CG_counter_refinement N Δ
{HΔ : x v, PersistentP (Δ x v)}
:
(@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)) HΔ).
Lemma FG_CG_counter_refinement N Δ {HΔ : x v, PersistentP (Δ x v)} :
(@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)) HΔ).
Proof.
(* executing the preambles *)
intros vs Hlen. destruct vs; [|inversion Hlen].
intros [|v vs] Hlen; simplify_eq.
cbn -[FG_counter CG_counter].
intros ρ j K. iIntros "[#Hheap [#Hspec [_ Hj]]]".
rewrite ?empty_env_subst.
unfold CG_counter, FG_counter.
iIntros {ρ j K} "(#Hheap & #Hspec & _ & Hj)".
rewrite ?empty_env_subst /CG_counter /FG_counter.
iPvs (steps_newlock _ _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
as {l} "[Hj Hl]"; eauto.
rewrite fill_app; simpl.
iFrame "Hspec Hj"; trivial.
rewrite fill_app; simpl.
{ rewrite fill_app /=. by iFrame. }
rewrite fill_app /=.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst; simpl.
rewrite counter_read_subst; simpl.
asimpl. rewrite CG_locked_increment_subst /=.
rewrite counter_read_subst /=.
iPvs (step_alloc _ _ _ j (K ++ [AppRCtx (LamV _)]) _ _ _ _ with "[Hj]")
as {cnt'} "[Hj Hcnt']"; eauto.
rewrite fill_app; simpl.
iFrame "Hspec Hj"; trivial.
{ rewrite fill_app; simpl. by iFrame. }
rewrite fill_app; simpl.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
asimpl. rewrite CG_locked_increment_subst; simpl.
rewrite counter_read_subst; simpl.
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 (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt".
simpl.
iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {cnt} "Hcnt /=".
(* establishing the invariant *)
iAssert (( n, l ↦ₛ (v false) cnt ↦ᵢ (v n) cnt' ↦ₛ (v n) )%I)
with "[Hl Hcnt Hcnt']" as "Hinv".
{ iExists _. iFrame "Hl Hcnt Hcnt'"; trivial. }
{ iExists _. by iFrame. }
iPvs (inv_alloc (N .@ 4) with "[Hinv]") as "#Hinv"; trivial.
{ iNext; iExact "Hinv". }
(* splitting increment and read *)
iApply wp_lam; trivial. iNext. asimpl.
rewrite counter_read_subst; simpl.
rewrite counter_read_subst /=.
iApply wp_value; simpl.
{ rewrite counter_read_to_val; trivial. }
iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)).
simpl. rewrite CG_locked_increment_of_val counter_read_of_val.
{ by rewrite counter_read_to_val. }
iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl.
rewrite CG_locked_increment_of_val counter_read_of_val.
iFrame "Hj".
iExists (_, _), (_, _). simpl; repeat iSplit; trivial.
iExists (_, _), (_, _); simpl; repeat iSplit; trivial.
- (* refinement of increment *)
iAlways. clear j K. iIntros {j K v} "[#Heq Hj]".
rewrite CG_locked_increment_of_val. simpl.
destruct v; iDestruct "Heq" as "[% %]"; simpl in *;subst.
rewrite CG_locked_increment_of_val /=.
destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=.
iLöb as "Hlat".
iApply wp_lam; trivial. asimpl.
iNext.
iApply wp_lam; trivial. asimpl. iNext.
(* fine-grained reads the counter *)
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
......@@ -344,7 +328,7 @@ Section CG_Counter.
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> (N .@4) as {n'} "[Hl [Hcnt Hcnt']]".
(* performing CAS *)
destruct (eq_nat_dec n n') as [|Hneq]; subst.
destruct (decide (n = n')) as [|Hneq]; subst.
+ (* CAS succeeds *)
(* In this case, we perform increment in the coarse-grained one *)
iPvs (steps_CG_locked_increment
......@@ -355,7 +339,7 @@ Section CG_Counter.
iNext; iFrame "Hcnt"; iIntros "Hcnt".
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_true. iNext. iApply wp_value; trivial.
iExists _; iSplitL; [|iSplit]; trivial. simpl; trivial.
iExists UnitV; iFrame; auto.
+ (* CAS fails *)
(* In this case, we perform a recursive call *)
iApply (wp_cas_fail _ _ _ _ (v n')); simpl; trivial;
......@@ -367,21 +351,20 @@ Section CG_Counter.
- (* refinement of read *)
iAlways. clear j K. iIntros {j K v} "[#Heq Hj]".
rewrite ?counter_read_of_val.
destruct v; iDestruct "Heq" as "[% %]".
simpl in *; subst; simpl.
iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=.
Transparent counter_read.
unfold counter_read at 2.
iApply wp_lam; trivial. simpl.
iNext.
iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iPvs (steps_counter_read
_ _ _ _ _ _ _ _ with "[Hj Hcnt']") as "[Hj Hcnt']".
iPvs (steps_counter_read (N .@ 3) with "[Hj Hcnt']") as "[Hj Hcnt']".
{ prove_disj N 3 4. }
{ by iFrame "Hspec Hcnt' Hj". }
iApply wp_load; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iNext. iFrame "Hcnt"; iIntros "Hcnt".
iFrame "Hcnt"; iIntros "> Hcnt".
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iExists (v _); iFrame "Hj". iExists _; by iSplit.
iExists (v _); eauto.
Unshelve.
all: abstract prove_disj N 3 4.
Qed.
......
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