Continuation change, extract_proph_winner change (!26) · Merge requests · Iris / examples · GitLab

Snippets Groups Projects

The source project of this merge request has been removed.

Merged Ghost User requested to merge (removed):master into master 5 years ago

1 unresolved thread

The continuation Q is moved to the top level in the Accepted state.

extract_proph_winner now only considers the first element in the list and does not restrict the first value.

Activity

Ghost User added 9 commits 5 years ago
added 9 commits

91d0f581...77e03801 - 8 commits from branch iris:master

b8fa6f43 - merge with original repo

Compare with previous version
Ralf Jung @jung started a thread on an old version of the diff 5 years ago

Resolved
Last reply by Ralf Jung 5 years ago

Ralf Jung @jung started a thread on the diff 5 years ago

Resolved

Ralf Jung @jung · 5 years ago

Owner

LGTM, other than comment nits!

Ghost User added 1 commit 5 years ago

added 1 commit

92d6baf8 - addressed comments MR 26

Compare with previous version

Ghost User resolved all discussions 5 years ago

resolved all discussions

Ralf Jung @jung started a thread on an old version of the diff 5 years ago

theories/logatom/rdcss/rdcss.v

161	161
162	162	(** Definition of the invariant *)
163	163
	164	(* Extract the TID of the winner from the prophecy value. The winner is the first thread that performs a CAS. *)
Ralf Jung @jung · 5 years ago Owner Should be a coqdoc comment. I had the `**` on purpose. :) Ghost User changed this line in version 4 of the diff 5 years ago changed this line in version 4 of the diff Ghost User @ghost · 5 years ago Author Contributor should be fixed Please register or sign in to reply

Ghost User added 1 commit 5 years ago

added 1 commit

19480ebd - minor change

Compare with previous version

Ralf Jung mentioned in commit 5 years ago

mentioned in commit a58a15e2

Ralf Jung merged 5 years ago

merged

Please register or sign in to reply