otrack
Joined 7 years ago
Karma
135
Submissions
31
Member since
Jan 27
Recent submissions
Comment · 11 months ago
Thank you, dgacmu! We are currently working on a TLA+ specification with master's students, and we plan to verify it with TLC and Apalache. I discovered that Iulian's TLA+ specification was missing a ballot variable [1] by injecting a trace, because exhaustive exploration was not tractable. Therefore, state-space explosion is likely to become a problem (systems of interest contain 7–9 processes with non‑transitive conflicts). In that case, intermediate abstractions will be necessary, which may naturally lead us to theorem proving.
Once the specification is ready, I'll post about it here. :)
Comment · 1 year ago
Author here.
Lamport simply calls his protocol "Paxos" to refer to both the single‑decree and multi‑decree versions. This is also the case in his other works, e.g., "Fast Paxos" and "Generalized Paxos." The term "Multi‑Paxos" is a later community/industry shorthand for the repeated or optimized use of single‑decree Paxos.
Comment · 1 year ago
The situation is less dramatic than this article says.
https://edri.org/our-work/chat-control-what-is-actually-goin...
Comment · 1 year ago
So true.
https://www.otrack.org/