From 17e193a3c5ae57509c6ce5a9e0340f98b34ce594 Mon Sep 17 00:00:00 2001 From: Gaurav Parthasarathy <gauravp@student.ethz.ch> Date: Tue, 9 Jul 2019 22:29:41 +0200 Subject: [PATCH] made the top comment clearer --- theories/logatom/rdcss/rdcss.v | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v index f7c195e6..fa6ba380 100644 --- a/theories/logatom/rdcss/rdcss.v +++ b/theories/logatom/rdcss/rdcss.v @@ -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. *) (* -- GitLab