New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Civl] Fix ChangRoberts #858

Merged

shazqadeer merged 3 commits into master from fix-cr

Mar 9, 2024

Contributor

shazqadeer commented Mar 8, 2024 •

edited

Loading

This PR provides a new proof for the Chang Roberts protocol for leader election. The new proof is different from the existing Civl proof in two ways:

Stronger specification is proved. The new proof proves that a unique leader will be elected in all terminal states. The old proof only proved that conflicting leaders are not elected.
The modeling of the protocol avoids the use of channels and achieves all communication asynchronous calls.

Shaz Qadeer added 3 commits

March 8, 2024 12:00


          first commit

ff0ae45


          added new version

179130c


          real fix

f05aae5

shazqadeer requested a review from bkragl

March 9, 2024 15:49

shazqadeer merged commit 6e9cce4 into master

4 checks passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet