Commit ca9003d1 authored by Dan Frumin's avatar Dan Frumin

A logically atomic specification for `counter_read`

parent 79a8f92f
......@@ -16,7 +16,7 @@ Definition CG_locked_increment : val := λ: "x" "l" <>,
release "l".
(* with_lock (λ: "l", CG_increment "x" "l") "l". *)
Definition counter_read : val := λ: "x" "y", !"x".
Definition counter_read : val := λ: "x" <>, !"x".
Definition CG_counter_body : val := λ: "x" "l",
(CG_locked_increment "x" "l", counter_read "x").
......@@ -268,6 +268,21 @@ Section CG_Counter.
Definition counter_inv l cnt cnt' : iProp Σ :=
( n, l ↦ₛ (#v false) cnt ↦ᵢ (#nv n) cnt' ↦ₛ (#nv n))%I.
Lemma bin_log_counter_read_r Γ E1 E2 K x n t τ
(Hspec : nclose specN E1) :
x ↦ₛ (#nv n)
- (x ↦ₛ (#nv n)
- {E1,E2;Γ} t log fill K (#n n)%E : τ)%I
- {E1,E2;Γ} t log fill K (lamsubst counter_read (LocV x) #())%E : τ.
Proof.
iIntros "Hx Hlog".
Transparent counter_read. unfold counter_read. unlock. simpl.
iApply bin_log_related_rec_r; auto. simpl.
iApply (bin_log_related_load_r with "Hx"); auto.
Opaque counter_read.
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 *)
......@@ -278,7 +293,7 @@ Section CG_Counter.
{E2,E1;Γ} fill K (Lit Unit) log t : τ))
- ({E1,E1;Γ} fill K ((lamsubst FG_increment (LocV x)) Unit) log t : τ).
Proof.
iIntros "#H".
iIntros "#H".
Transparent FG_increment. unfold FG_increment. unlock. simpl.
iLöb as "IH".
iApply (bin_log_related_rec_l _ E1 K); auto. iNext. simpl.
......@@ -318,6 +333,27 @@ Section CG_Counter.
iApply "IH".
Qed.
(* A similar atomic specification for the counter_read fn *)
Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ :
(|={E1,E2}=> n, x ↦ᵢ (#nv n) R(n)
(( n, x ↦ᵢ (#nv n) R(n)) ={E2,E1}= True)
( m, x ↦ᵢ (#nv m) R(m) -
{E2,E1;Γ} fill K (#n m) log t : τ))
- {E1,E1;Γ} fill K (lamsubst counter_read (LocV x) #())%E log t : τ.
Proof.
iIntros "#H".
Transparent counter_read. unfold counter_read. unlock. simpl.
iApply (bin_log_related_rec_l _ E1 _); auto. iNext. simpl.
Opaque bin_log_related. (* TODO: why is this needed? *)
iApply (bin_log_related_load_l).
iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
iExists _; iFrame "Hx".
iIntros "Hx".
rewrite ->uPred.and_elim_r. (* TODO: a tactic for this *)
iApply "Hfin". by iFrame.
Opaque counter_read.
Qed.
(* TODO: try to use with_lock rules *)
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
......@@ -388,21 +424,30 @@ Section CG_Counter.
Transparent counter_read.
unfold counter_read. unlock.
iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.
iApply bin_log_related_rec; simpl. iAlways. cbn.
iApply (bin_log_related_load_l _ _ _ []).
iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose".
iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.
iApply bin_log_related_arrow. iAlways.
iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
(* :( *)
replace (λ: <>, ! #cnt)%E
with (lamsubst counter_read (LocV cnt)); last first.
{ unfold counter_read. unlock. reflexivity. }
replace (λ: <>, ! #cnt')%E
with (lamsubst counter_read (LocV cnt')); last first.
{ unfold counter_read. unlock. reflexivity. }
iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#v false)) cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists (#nv n). iFrame "Hcnt".
iIntros "Hcnt". simpl.
iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto.
{ solve_ndisj. }
iIntros "Hcnt'".
iMod ("Hclose" with "[Hl Hcnt Hcnt']").
{ iNext. iExists _. by iFrame. }
simpl.
iApply (bin_log_related_val); auto.
intros. simpl. eauto.
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'").
{ solve_ndisj. }
iIntros "Hcnt'".
iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
{ iNext. iExists _. by iFrame. }
iApply (bin_log_related_val); intros; simpl; eauto.
Qed.
Lemma FG_CG_counter_refinement :
......
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