Skip to content
Snippets Groups Projects
Commit 6639940c authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Ralf Jung
Browse files

Expand RDCSS comments

parent 8de152b1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/logatom/rdcss/rdcss.v
+ 123
− 89
View file @ 6639940c
......@@ -7,64 +7,97 @@ From iris_examples.logatom.rdcss Require Import spec.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
(** Using prophecy variables with helping: implementing a simplified version of
the restricted double-compare single-swap from "A Practical Multi-Word Compare-and-Swap Operation" by Harris et al. (DISC 2002)
*)
(** * Implementation of the functions. *)
(* 1) The M location l_m can differ when helping another thread in the same RDCSS instance
(Harris et al. refer to it as a location in the control section.)
2) The N location l_n identifies a single RDCSS instance.
(Harris et al. refer to it as a location in the data section.)
3) There are two kinds of values stored at N locations
3.1) The value is injL n for some n: no operation is on-going and the logical state is n.
3.2) The value is injR l_descr for some location l_descr (which we call a descriptor):
l_descr must point to a tuple (l_m, m1, n1, n2, p) for some M location l_m, values m1, n1, n2 and prophecy p.
In this case an operation is on-going with corresponding M location l_m.
*)
(*
(** We consider here an implementation of the RDCSS (Restricted Double-Compare
Single-Swap) data structure of Harris et al., as described in "A Practical
Multi-Word Compare-and-Swap Operation" (DISC 2002).
Our goal is to prove logical atomicity for the operations of RDCSS, and to
do so we will need to use prophecy variables! This Coq file is part of the
artifact accompanying the paper "The Future is Ours: Prophecy Variables in
Separation Logic" (POPL 2020). Proving logical atomicity for RDCSS appears
as a major case study in the paper, so it makes sense to read the relevant
sections first (§4 to §6) to better understand the Coq proof. The paper is
available online at: <https://plv.mpi-sws.org/prophecies/>. *)
(** * Implementation of the RDCSS operations *)
(** The RDCSS data structure manipulates two kinds of locations:
- N-locations (a.k.a. RDCSS locations) denoted [l_n] identify a particular
instance of RDCSS. (Harris et al. refer to them as locations in the data
section.) They are the locations that may be updated by a call to RDCSS.
- M-locations denoted [l_m] are not tied to a particular RDCSS instance.
(Harris et al. refer to them as locations in the control section.) They
are never directly modified by the RDCSS operation, but they are subject
to arbitrary interference by other heap operations.
An N-location can contain values of two forms.
- A value of the form [injL n] indicates that there is currently no active
RDCSS operation on the N-location, and that the location has the logical
value [n]. In that case, the N-location is in a "quiescent" state.
- A value of the form [injR descr] indicates that the RDCSS operation that
is identified by descriptor [descr] is ongoing. In that case, descriptor
[descr] must point to a tuple [(l_m, m1, n1, n2, p)] for some M-location
[l_m], integers [m1], [n1], [n2] and prophecy [p]. An N-location holding
a value of the form [injR descr] is in an "updating" state. *)
(** As mentioned in the paper, there are minor differences between our version
of RDCSS and the original one (by Harris et al.):
- In the original version, the RDCSS operation takes as input a descriptor
for the operation, whereas in our version the RDCSS operation allocates
the descriptor itself.
- In the original version, values (inactive state) and descriptors (active
state) are distinguished by looking at their least significant bits. Our
version rather relies on injections to avoid bit-level manipulations. *)
(** The [new_rdcss] operation creates a new RDCSS location. It corresponds to
the following pseudo-code:
<<
new_rdcss(n) := ref (injL n)
*)
>>
*)
Definition new_rdcss : val := λ: "n", ref (InjL "n").
(*
(** The [complete] function is used internally by the RDCSS operations. It can
be expressed using the following pseudo-code:
<<
complete(l_descr, l_n) :=
let (l_m, m1, n1, n2, p) := !l_descr in
let (l_m, m1, n1, n2, p) := !l_descr;
(* data = (l_m, m1, n1, n2, p) *)
let tid_ghost = NewProph in
let n_new = (if !l_m = m1 then n1 else n2) in
Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p tid_ghost ; #().
*)
let tid_ghost = NewProph;
let n_new = (if !l_m = m1 then n1 else n2);
Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p tid_ghost;
#().
>>
In this function, we rely on a prophecy variable to emulate a ghost thread
identifier. In particular, the corresponding prophecy variable [tid_ghost]
is never resolved. Here, the main reason for using a prophecy variable is
that we can use erasure to argue that it has no effect on the code. *)
Definition complete : val :=
λ: "l_descr" "l_n",
let: "data" := !"l_descr" in
(* data = (l_m, m1, n1, n2, p) *)
let: "data" := !"l_descr" in (* data = (l_m, m1, n1, n2, p) *)
let: "l_m" := Fst (Fst (Fst (Fst ("data")))) in
let: "m1" := Snd (Fst (Fst (Fst ("data")))) in
let: "n1" := Snd (Fst (Fst ("data"))) in
let: "n2" := Snd (Fst ("data")) in
let: "p" := Snd ("data") in
(* Create a thread identifier using NewProph.
tid_ghost is not used as a traditional prophecy, i.e. it is never resolved.
The reason we use NewProph is so that we can use the erasure theorem to argue that
it has no effect on the code.
*)
(* Create a thread identifier using NewProph. *)
let: "tid_ghost" := NewProph in
let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "tid_ghost" ;; #().
(*
get(l_n) :=
match: !l_n with
| injL n => n
| injR (l_descr) =>
complete(l_descr, l_n);
get(l_n)
end.
*)
Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "tid_ghost";;
#().
(** The [get] operation reads the value stored in an RDCSS location previously
created using [new_rdcss]. In pseudo-code, it corresponds to:
<<
rec get(l_n) :=
match !l_n with
| injL n => n
| injR l_descr => complete(l_descr, l_n);
get(l_n)
end
>>
*)
Definition get : val :=
rec: "get" "l_n" :=
match: !"l_n" with
......@@ -74,30 +107,32 @@ Definition get : val :=
"get" "l_n"
end.
(*
(** Finally, the [rdcss] operation corresponds to the following pseudo-code:
<<
rdcss(l_m, l_n, m1, n1, n2) :=
let p := NewProph in
let l_descr := ref (l_m, m1, n1, n2, p) in
(rec: rdcss_inner()
let (r, b) := CmpXchg(l_n, InjL n1, InjR l_descr) in
match r with
InjL n =>
if b then
complete(l_descr, l_n) ; n1
else
n
| InjR l_descr_other =>
complete(l_descr_other, l_n) ;
let p := NewProph;
let l_descr := ref (l_m, m1, n1, n2, p);
rec rdcss_inner() =
let (r, b) := CmpXchg(l_n, InjL n1, InjR l_descr) in
match r with
| InjL n =>
if b then
complete(l_descr, l_n); n1
else
n
| InjR l_descr_other =>
complete(l_descr_other, l_n);
rdcss_inner()
end
)()
end;
rdcss_inner()
>>
*)
Definition rdcss: val :=
λ: "l_m" "l_n" "m1" "n1" "n2",
(* allocate fresh descriptor *)
(* Allocate the descriptor for the operation. *)
let: "p" := NewProph in
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
(* start rdcss computation with allocated descriptor *)
(* Attempt to establish the descriptor to make the operation "active". *)
( rec: "rdcss_inner" "_" :=
let: "r" := CmpXchg "l_n" (InjL "n1") (InjR "l_descr") in
match: Fst "r" with
......@@ -110,8 +145,9 @@ Definition rdcss: val :=
(* CmpXchg failed, hence we could linearize at the CmpXchg *)
"n"
| InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *)
complete "l_descr_other" "l_n" ;;
(* A descriptor from a concurrent operation was read, try to help
and then restart. *)
complete "l_descr_other" "l_n";;
"rdcss_inner" #()
end
) #().
......@@ -138,7 +174,7 @@ Section rdcss.
Context {Σ} `{!heapG Σ, !rdcssG Σ, !gcG Σ }.
Context (N : namespace).
Local Definition descrN := N .@ "descr".
Local Definition descrN := N .@ "descr".
Local Definition rdcssN := N .@ "rdcss".
(** Updating and synchronizing the value RAs *)
......@@ -165,12 +201,12 @@ Section rdcss.
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with
| (_, LitV (LitProphecy tid)) :: _ => Some tid
| _ => None
| _ => None
end.
Inductive abstract_state : Set :=
| Quiescent : val → abstract_state
| Updating : loc → loc → val → val → val → proph_id → abstract_state.
| Quiescent : val → abstract_state
| Updating : loc → loc → val → val → val → proph_id → abstract_state.
Definition state_to_val (s : abstract_state) : val :=
match s with
......@@ -181,17 +217,14 @@ Section rdcss.
Definition own_token γ := (own γ (Excl ()))%I.
Definition pending_state P (n1 : val) (proph_winner : option proph_id) tid_ghost_winner (γ_n γ_a: gname) :=
(P ∗
⌜match proph_winner with None => True | Some p => p = tid_ghost_winner end⌝ ∗
own γ_n (● Excl' n1) ∗
own_token γ_a)%I.
(P ∗ ⌜from_option (λ p, p = tid_ghost_winner) True proph_winner⌝ ∗
own γ_n (● Excl' n1) ∗ own_token γ_a)%I.
(* After the prophecy said we are going to win the race, we commit and run the AU,
switching from [pending] to [accepted]. *)
Definition accepted_state Q (proph_winner : option proph_id) (tid_ghost_winner : proph_id) :=
((∃ vs, proph tid_ghost_winner vs) ∗
Q ∗
⌜match proph_winner with None => True | Some tid => tid = tid_ghost_winner end⌝)%I.
Q ∗ ⌜from_option (λ p, p = tid_ghost_winner) True proph_winner⌝)%I.
(* The same thread then wins the CmpXchg and moves from [accepted] to [done].
Then, the [γ_t] token guards the transition to take out [Q].
......@@ -203,7 +236,8 @@ Section rdcss.
owns *more than* half of its [l_descr] in the Updating state,
which means we know that the [l_descr] there and here cannot be the same. *)
Definition done_state Qn (l_descr : loc) (tid_ghost_winner : proph_id) (γ_t γ_a: gname) :=
((Qn ∨ own_token γ_t) ∗ (∃ vs, proph tid_ghost_winner vs) ∗ (l_descr ↦{1/2} -) ∗ own_token γ_a)%I.
((Qn ∨ own_token γ_t) ∗ (∃ vs, proph tid_ghost_winner vs) ∗
l_descr ↦{1/2} - ∗ own_token γ_a)%I.
(* Invariant expressing the descriptor protocol.
- We always need the [proph] in here so that failing threads coming late can
......@@ -252,7 +286,7 @@ Section rdcss.
(* We own *more than* half of [l_descr], which shows that this cannot
be the [l_descr] of any [descr] protocol in the [done] state. *)
⌜val_is_unboxed m1⌝ ∗
l_descr ↦{1/2 + q} (#l_m, m1, n1, n2, #p)%V ∗
l_descr ↦{1/2 + q} (#l_m, m1, n1, n2, #p)%V ∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_winner γ_n γ_t γ_s γ_a) ∗
□ pau P Q γ_n l_m m1 n1 n2 ∗ is_gc_loc l_m
end)%I.
......@@ -265,7 +299,7 @@ Section rdcss.
Global Instance is_rdcss_persistent γ_n l_n: Persistent (is_rdcss γ_n l_n) := _.
Global Instance rdcss_content_timeless γ_n n : Timeless (rdcss_content γ_n n) := _.
Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (Quiescent #0).
Lemma rdcss_content_exclusive γ_n l_n_1 l_n_2 :
......@@ -419,7 +453,7 @@ Section rdcss.
as a precondition. *)
Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : val) (p : proph_id) γ_n γ_t γ_s γ_a tid_ghost_inv P Q q:
val_is_unboxed m1 →
N ## gcN →
N ## gcN →
inv rdcssN (rdcss_inv γ_n l_n) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_n γ_t γ_s γ_a) -∗
□ pau P Q γ_n l_m m1 n1 n2 -∗
......@@ -434,7 +468,7 @@ Section rdcss.
wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures.
wp_apply wp_new_proph; first done.
iIntros (vs_ghost tid_ghost) "Htid_ghost". wp_pures.
wp_bind (! _)%E.
wp_bind (! _)%E.
(* open outer invariant *)
iInv rdcssN as (s) "(>Hln & Hrest)"=>//.
(* two different proofs depending on whether we are succeeding thread *)
......@@ -448,7 +482,7 @@ Section rdcss.
iMod (gc_access with "InvGC") as "Hgc"; first solve_ndisj.
(* open and *COMMIT* AU, sync B location l_n and A location l_m *)
iMod "AU" as (m' n') "[CC [_ Hclose]]".
iDestruct "CC" as "[Hgc_lm Hn◯]".
iDestruct "CC" as "[Hgc_lm Hn◯]".
(* sync B location and update it if required *)
iDestruct (sync_values with "Hn● Hn◯") as %->.
iMod (update_value _ _ _ (if decide (m' = m1 ∧ n' = n') then n2 else n') with "Hn● Hn◯")
......@@ -509,9 +543,9 @@ Section rdcss.
<<< gc_mapsto l_m m ∗ rdcss_content γ_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET n >>>.
Proof.
iIntros (Hm1_unbox Hn1_unbox) "Hrdcss". iDestruct "Hrdcss" as "(#InvR & #InvGC & Hdisj)".
iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
(* allocate fresh descriptor *)
wp_lam. wp_pures.
wp_lam. wp_pures.
wp_apply wp_new_proph; first done.
iIntros (proph_values p) "Hp".
wp_let. wp_alloc l_descr as "Hld".
......@@ -549,12 +583,12 @@ Section rdcss.
iModIntro. iDestruct "Hld" as "[Hld1 [Hld2 Hld3]]". iSplitR "Hld2 Token_t".
{ (* close outer invariant *)
iNext. iCombine "Hld1 Hld3" as "Hld1". iExists (Updating l_descr l_m m1 n n2 p).
eauto 15 with iFrame.
eauto 15 with iFrame.
}
wp_pures.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]");[ done..|].
iIntros "Ht". iMod ("Ht" with "Token_t") as "Φ". by wp_seq.
+ (* values do not match -> CmpXchg fails
+ (* values do not match -> CmpXchg fails
we can commit here *)
wp_cmpxchg_fail.
iMod "AU" as (m'' n'') "[[Hm◯ Hn◯] [_ Hclose]]"; simpl.
......@@ -568,7 +602,7 @@ Section rdcss.
- (* l_n ↦ injR l_ndescr' *)
(* a descriptor l_descr' is currently stored at l_n -> CmpXchg fails
try to help the on-going operation *)
wp_cmpxchg_fail.
wp_cmpxchg_fail.
iModIntro.
(* extract descr invariant *)
iDestruct "Hrest" as (q P Q tid_ghost γ_t γ_s γ_a) "(#Hm1'_unbox & [Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
......@@ -600,7 +634,7 @@ Section rdcss.
iExists (Quiescent n). iFrame. }
iModIntro.
iApply ("HΦ" $! l_n γ_n).
iSplitR; last by iFrame. by iFrame "#".
iSplitR; last by iFrame. by iFrame "#".
Qed.
(** ** Proof of [get] *)
......@@ -611,7 +645,7 @@ Section rdcss.
<<< rdcss_content γ_n n, RET n >>>.
Proof.
iIntros "Hrdcss". iDestruct "Hrdcss" as "(#InvR & #InvGC & Hdisj)".
iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
wp_load.
......@@ -619,7 +653,7 @@ Section rdcss.
- iMod "AU" as (au_n) "[Hn◯ [_ Hclose]]"; simpl.
iDestruct "Hrest" as "[Hln' Hn●]".
iDestruct (sync_values with "Hn● Hn◯") as %->.
iMod ("Hclose" with "Hn◯") as "HΦ".
iMod ("Hclose" with "Hn◯") as "HΦ".
iModIntro. iSplitR "HΦ". {
iNext. iExists (Quiescent au_n). iFrame.
}
......@@ -627,9 +661,9 @@ Section rdcss.
- iDestruct "Hrest" as (q P Q tid_ghost γ_t γ_s γ_a) "(#Hm1_unbox & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
iDestruct "Hm1_unbox" as %Hm1_unbox.
iModIntro. iSplitR "AU Hld'". {
iNext. iExists (Updating l_descr l_m m1 n1 n2 p). eauto 15 with iFrame.
iNext. iExists (Updating l_descr l_m m1 n1 n2 p). eauto 15 with iFrame.
}
wp_match.
wp_match.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld']"); [done..|].
iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
Qed.
......
theories/logatom/rdcss/spec.v
+ 8
− 2
View file @ 6639940c
......@@ -4,7 +4,14 @@ From iris.program_logic Require Export atomic.
From iris_examples.logatom.lib Require Export gc.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
(** A general logically atomic interface for RDCSS.
See [rdcss.v] for references and more details about this data structure. *)
_Note on the use of GC locations_: the specification of the [rdcss] operation
as given by [rdcss_spec] relies on the [gc_mapsto l_m m] assertion. It roughly
corresponds to the usual [l_m ↦ m] but with an additional guarantee that [l_m]
will not be deallocated. This guarantees that unique immutable descriptors can
be associated to each operation, and that they cannot be "reused". *)
Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
(* -- operations -- *)
new_rdcss : val;
......@@ -42,7 +49,6 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
}.
Arguments atomic_rdcss _ {_} {_}.
Existing Instances
is_rdcss_persistent rdcss_content_timeless
name_countable name_eqdec.
......
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