From 92d6baf8762c84dbdac3d1bd5415d9f12f1f3290 Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Thu, 11 Jul 2019 01:04:25 +0200
Subject: [PATCH] addressed comments MR 26
---
theories/logatom/rdcss/rdcss.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 233fd939..eaac4b40 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -161,9 +161,10 @@ Section rdcss.
(** Definition of the invariant *)
+ (* Extract the TID of the winner from the prophecy value. The winner is the first thread that performs a CAS. *)
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with
- | ((_, _)%V, LitV (LitProphecy tid)) :: _ => Some tid
+ | (_, LitV (LitProphecy tid)) :: _ => Some tid
| _ => None
end.
--
GitLab