Commit 41064dbb authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

some formatting changes and adjusted spec file

parent f1b868e3
......@@ -38,8 +38,8 @@ Definition new_data : val :=
("lm", "lln").
(*
set_value(ctr, b) :=
ctr.1 <- b
set_value(data, m1) :=
data.1 <- m1
*)
Definition set_value : val :=
λ: "data" "m1",
......@@ -77,7 +77,7 @@ Definition get : val :=
match: !"ln" with
InjL "n" => "n"
| InjR "args'" =>
(* args' = ( (m1, (n1, n2)) , p) *)
(* args' = ( (m1, (n1, n2)), p) *)
let: "m1" := (Fst (Fst "args'")) in
let: "n1" := (Fst (Snd (Fst "args'"))) in
let: "n2" := (Snd (Snd (Fst "args'"))) in
......@@ -100,7 +100,7 @@ rdcss_minor(data, m1, n1, n2) :=
complete(lln, lm, lnew, m1, n1, n2, p); #true
else rdcss_minor(data, m1, n1, n2)
else #false
| injR "( (m1', (n1', n2')), p')" =>
| injR ( (m1', (n1', n2')), p') =>
complete(lln, lm, ln, m1', n1', n2', p');
rdcss_minor(data, m1, n1, n2)
end.
......@@ -213,27 +213,28 @@ Section rdcss_minor.
Remember that the thread winning the CAS might be just helping. The token
is owned by the thread whose request this is.
In this state, [l_ghost_winner] serves as a token to make sure that
only the CAS winner can transition to here, and owning half of[l] serves as a
"location" token to ensure there is no ABA going on. Notice how [counter_inv]
owns *more than* half of its [l], which means we know that the [l] there
only the CAS winner can transition to here, and owning half of [ln] serves as a
"location" token to ensure there is no ABA going on. Notice how [data_inv]
owns *more than* half of its [ln], which means we know that the [ln] there
and here cannot be the same. *)
Definition done_state Q (l l_ghost_winner : loc) (γ_t : gname) :=
((Q own_token γ_t) l_ghost_winner - l {1/2} -)%I.
Definition done_state Q (ln l_ghost_winner : loc) (γ_t : gname) :=
((Q own_token γ_t) l_ghost_winner - ln {1/2} -)%I.
(* We always need the [proph] in here so that failing threads coming late can
always resolve their stuff.
Moreover, we need a way for anyone who has observed the [done] state to
prove that we will always remain [done]; that's what the one-shot token [γ_s] is for. *)
Definition state_inv P Q (p : proph_id) n (c_l l l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
Definition state_inv P Q (p : proph_id) n (lln ln l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
( vs, proph p vs
(own γ_s (Cinl $ Excl ())
(c_l {1/2} #l ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
(lln {1/2} #ln ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
accepted_state (Q #true) (val_to_some_loc vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q #true) l l_ghost_winner γ_t))%I.
own γ_s (Cinr $ to_agree ()) done_state (Q #true) ln l_ghost_winner γ_t))%I.
Definition pau P Q γs m1 n1 n2 :=
( P - AU << (m n : Z), data_content γs m n >> @ ∖↑N,
<< data_content γs m (if (decide ((m = m1) (n = n1))) then n2 else n), COMM Q (if decide (n = n1) then #true else #false) >>)%I.
<< data_content γs m (if (decide ((m = m1) (n = n1))) then n2 else n),
COMM Q (if decide (n = n1) then #true else #false) >>)%I.
Definition data_inv γ_m γ_n lm lln :=
( (m : Z) (ln : loc) (q : Qp) (s : abstract_state),
......@@ -255,10 +256,10 @@ Section rdcss_minor.
Local Hint Extern 0 (environments.envs_entails _ (data_inv _ _ _ _)) => unfold data_inv.
Definition is_data (γs : gname * gname) (ctr : val) :=
( (γ_b γ_n : gname) (f c : loc),
⌜γs = (γ_b, γ_n) ctr = (#f, #c)%V
inv dataN (data_inv γ_b γ_n f c))%I.
Definition is_data (γs : gname * gname) (data : val) :=
( (γ_m γ_n : gname) (lm lln : loc),
⌜γs = (γ_m, γ_n) data = (#lm, #lln)%V
inv dataN (data_inv γ_m γ_n lm lln))%I.
Global Instance is_data_persistent γs ctr : Persistent (is_data γs ctr) := _.
......@@ -496,7 +497,7 @@ Section rdcss_minor.
iIntros (proph_values p') "Hp'".
wp_let. wp_alloc ly as "Hly".
wp_let. wp_bind (CAS _ _ _)%E.
(* open outer invariant again to CAS c_l *)
(* open outer invariant again to CAS lln *)
iInv dataN as (m2 ln'' q2 s) "(>Hlm & >Hlln & >Hln & >Hm● & Hrest)".
destruct (decide (ln' = ln'')) as [<- | Hn].
* (* CAS succeeds *)
......
......@@ -31,7 +31,7 @@ Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
is_data N γs v -
<<< (m n: Z), data_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #() >>>;
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>;
set_value_spec N γs v (new_m: Z) :
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
......
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