Viewing profile — otrack

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+ specific…

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" an…

The situation is less dramatic than this article says. https://edri.org/our-work/chat-control-what-is-actually-goin...

So true.

Same here. The only clue I found are the following two lines in the Q/A section: "What consistency model does YDB use? To read data, YDB uses a model of strict data consistency."

On th topic, I would advice reading the boulangerie algorithm. An improved version of the original solution: https://lamport.azurewebsites.net/tla/boulangerie.html

sshell inherits the limitations of the FaaS infrastructure, including the time limit. Regarding the big data use case, more work is necessary to assess this, but the applications w…