Commit 17e193a3 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

made the top comment clearer

parent 55d07b4f
......@@ -13,18 +13,16 @@ Set Default Proof Using "Type".
(** * Implementation of the functions. *)
(* 1) l_m corresponds to the A location in the paper and can differ when helping another thread
in the same RDCSS instance.
2) l_n corresponds to the B location in the paper and identifies a single RDCSS instance.
3) Values stored at the B location have type
Val + Ref (Ref * Val * Val * Val * Proph)
3.1) If the value is injL n, then no operation is on-going and the logical state is n.
3.2) If the value is injR (Ref (l_m', m1', n1', n2', p)), then an operation is on-going
with corresponding A location l_m'. The reference pointing to the tuple of values
corresponds to the descriptor in the paper. We use the name l_descr for such a
descriptor reference.
(* 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.
*)
(*
......
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