Skip to content
Snippets Groups Projects
Commit 92d6baf8 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy
Browse files

addressed comments MR 26

parent b8fa6f43
No related branches found
No related tags found
1 merge request!26Continuation change, extract_proph_winner change
Hide whitespace changes
Inline Side-by-side
theories/logatom/rdcss/rdcss.v
+ 2
− 1
View file @ 92d6baf8
...@@ -161,9 +161,10 @@ Section rdcss. ...@@ -161,9 +161,10 @@ Section rdcss.
(** Definition of the invariant *) (** 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 := Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with match pvs with
| ((_, _)%V, LitV (LitProphecy tid)) :: _ => Some tid | (_, LitV (LitProphecy tid)) :: _ => Some tid
| _ => None | _ => None
end. end.
......
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