Commit c67a9a51 authored by Ralf Jung's avatar Ralf Jung

give readable names to the two possible states of the counter

parent 82d08c14
...@@ -159,13 +159,13 @@ Section conditional_counter. ...@@ -159,13 +159,13 @@ Section conditional_counter.
end. end.
Inductive abstract_state : Set := Inductive abstract_state : Set :=
| injl : Z abstract_state | Quiescent : Z abstract_state
| injr : Z proph_id abstract_state. | Updating : Z proph_id abstract_state.
Definition state_to_val (s : abstract_state) : val := Definition state_to_val (s : abstract_state) : val :=
match s with match s with
| injl n => InjLV #n | Quiescent n => InjLV #n
| injr n p => InjRV (#n,#p) | Updating n p => InjRV (#n,#p)
end. end.
Global Instance state_to_val_inj : Inj (=) (=) state_to_val. Global Instance state_to_val_inj : Inj (=) (=) state_to_val.
...@@ -217,8 +217,8 @@ Section conditional_counter. ...@@ -217,8 +217,8 @@ Section conditional_counter.
f #b c {1/2} #l l {1/2 + q} (state_to_val s) f #b c {1/2} #l l {1/2 + q} (state_to_val s)
own γ_b ( Excl' b) own γ_b ( Excl' b)
match s with match s with
| injl n => c {1/2} #l own γ_n ( Excl' n) | Quiescent n => c {1/2} #l own γ_n ( Excl' n)
| injr n p => | Updating n p =>
P Q l_ghost_winner γ_t γ_s, P Q l_ghost_winner γ_t γ_s,
(* There are two pieces of per-[state]-protocol ghost state: (* There are two pieces of per-[state]-protocol ghost state:
- [γ_t] is a token owned by whoever created this protocol and used - [γ_t] is a token owned by whoever created this protocol and used
...@@ -239,7 +239,7 @@ Section conditional_counter. ...@@ -239,7 +239,7 @@ Section conditional_counter.
Global Instance counter_content_timeless γs b n : Timeless (counter_content γs b n) := _. Global Instance counter_content_timeless γs b n : Timeless (counter_content γs b n) := _.
Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (injl 0). Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (Quiescent 0).
Lemma counter_content_exclusive γs f1 c1 f2 c2 : Lemma counter_content_exclusive γs f1 c1 f2 c2 :
counter_content γs f1 c1 - counter_content γs f2 c2 - False. counter_content γs f1 c1 - counter_content γs f2 c2 - False.
...@@ -327,7 +327,7 @@ Section conditional_counter. ...@@ -327,7 +327,7 @@ Section conditional_counter.
iFrame "#∗". iSplitR "Hl"; iExists _; done. } iFrame "#∗". iSplitR "Hl"; iExists _; done. }
iModIntro. iSplitR "HQ". iModIntro. iSplitR "HQ".
{ iNext. iDestruct "Hc" as "[Hc1 Hc2]". { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
iExists _, l_new, _, (injl n). iFrame. } iExists _, l_new, _, (Quiescent n). iFrame. }
iApply wp_fupd. wp_seq. iApply "HQ". iApply wp_fupd. wp_seq. iApply "HQ".
iApply state_done_extract_Q; done. iApply state_done_extract_Q; done.
Qed. Qed.
...@@ -457,7 +457,7 @@ Section conditional_counter. ...@@ -457,7 +457,7 @@ Section conditional_counter.
wp_load. destruct s as [n|n p]. wp_load. destruct s as [n|n p].
- iDestruct "Hrest" as "(Hc' & Hv)". - iDestruct "Hrest" as "(Hc' & Hv)".
iModIntro. iSplitR "AU Hl'". iModIntro. iSplitR "AU Hl'".
{ iModIntro. iExists _, _, (q/2)%Qp, (injl n). iFrame. } { iModIntro. iExists _, _, (q/2)%Qp, (Quiescent n). iFrame. }
wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done. wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
iIntros (l_ghost p') "Hp'". iIntros (l_ghost p') "Hp'".
wp_let. wp_alloc ly as "Hly". wp_let. wp_alloc ly as "Hly".
...@@ -481,7 +481,7 @@ Section conditional_counter. ...@@ -481,7 +481,7 @@ Section conditional_counter.
iFrame. destruct (val_to_some_loc l_ghost); simpl; done. } iFrame. destruct (val_to_some_loc l_ghost); simpl; done. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". { iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *) (* close invariant *)
iNext. iExists _, _, _, (injr n p'). eauto 10 with iFrame. iNext. iExists _, _, _, (Updating n p'). eauto 10 with iFrame.
} }
wp_if. wp_apply complete_spec; [done..|]. wp_if. wp_apply complete_spec; [done..|].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam. iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
...@@ -496,7 +496,7 @@ Section conditional_counter. ...@@ -496,7 +496,7 @@ Section conditional_counter.
iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #P_AU]". iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #P_AU]".
iSplitR "Hl' AU". iSplitR "Hl' AU".
(* close invariant *) (* close invariant *)
{ iModIntro. iExists _, _, _, (injr n p). iFrame. eauto 10 with iFrame. } { iModIntro. iExists _, _, _, (Updating n p). iFrame. eauto 10 with iFrame. }
wp_let. wp_load. wp_match. wp_pures. wp_let. wp_load. wp_match. wp_pures.
wp_apply complete_spec; [done..|]. wp_apply complete_spec; [done..|].
iIntros "_". wp_seq. by iApply "IH". iIntros "_". wp_seq. by iApply "IH".
...@@ -519,7 +519,7 @@ Section conditional_counter. ...@@ -519,7 +519,7 @@ Section conditional_counter.
with "[Hl_f Hl_c Hl_n Hb● Hn●]") as "#InvC". with "[Hl_f Hl_c Hl_n Hb● Hn●]") as "#InvC".
{ iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]". { iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]".
iDestruct "Hl_n" as "[??]". iDestruct "Hl_n" as "[??]".
iExists true, l_n, (1/2)%Qp, (injl 0). iFrame. } iExists true, l_n, (1/2)%Qp, (Quiescent 0). iFrame. }
iModIntro. iModIntro.
iApply ("HΦ" $! (#l_f, #l_c)%V (γ_b, γ_n)). iApply ("HΦ" $! (#l_f, #l_c)%V (γ_b, γ_n)).
iSplitR; last by iFrame. iExists γ_b, γ_n, l_f, l_c. iSplit; done. iSplitR; last by iFrame. iExists γ_b, γ_n, l_f, l_c. iSplit; done.
...@@ -559,12 +559,12 @@ Section conditional_counter. ...@@ -559,12 +559,12 @@ Section conditional_counter.
iDestruct (sync_counter_values with "Hn● Hn◯") as %->. iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame. iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame.
iModIntro. iSplitR "HΦ Hl'". { iModIntro. iSplitR "HΦ Hl'". {
iNext. iExists b, c, (q/2)%Qp, (injl au_n). iFrame. iNext. iExists b, c, (q/2)%Qp, (Quiescent au_n). iFrame.
} }
wp_let. wp_load. wp_match. iApply "HΦ". wp_let. wp_load. wp_match. iApply "HΦ".
- iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #PAU]". - iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #PAU]".
iModIntro. iSplitR "AU Hl'". { iModIntro. iSplitR "AU Hl'". {
iNext. iExists b, c, (q/2)%Qp, (injr n p). eauto 10 with iFrame. iNext. iExists b, c, (q/2)%Qp, (Updating n p). eauto 10 with iFrame.
} }
wp_let. wp_load. wp_match. repeat wp_proj. wp_bind (complete _ _ _ _ _)%E. wp_let. wp_load. wp_match. repeat wp_proj. wp_bind (complete _ _ _ _ _)%E.
wp_apply complete_spec; [done..|]. wp_apply complete_spec; [done..|].
......
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