[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Chris Newcombe <chris.n...@xxxxxxxxx>*Date*: Sun, 26 May 2013 23:08:27 -0700 (PDT)

TLA+ spec and informal proofs of safety : http://raftuserstudy.s3-website-us-west-1.amazonaws.com/proof.pdf

The main motivation seems to have been to find a consensus algorithm that is easier to understand than Paxos.

They do give some statistical results of quizzing a group of students on both algorithms. They don't give defect-rates from any implementations.

I could not find that proof online, in a few minutes of searching.

Chris

Chris

[1]

The safety proof shows invariants that hold in everystate of every execution that the speciﬁcation allows. Itsmain lemma states that a leader only marks a log entrycommitted if every subsequent leader must also have thisentry. (Safety follows easily from this lemma.) We havean informal proof [19] for Raft which is relatively precise and complete (about 9 pages or 3500 words long).We also have a mechanically-checked version of the mainlemma and other portions of the proof using the TLAproof system [3]. However, this version relies on invariants whose proofs have not been mechanically checked(for example, we have not proven the type safety of thespeciﬁcation).

- Prev by Date:
**Blog post that uses TLA+ in a debate about properties of system designs** - Next by Date:
**Re: [tlaplus] Blog post that uses TLA+ in a debate about properties of system designs** - Previous by thread:
**Re: [tlaplus] Blog post that uses TLA+ in a debate about properties of system designs** - Next by thread:
**embed PlusCal and TLA+ specs in latex papers** - Index(es):