Does the TLA+ specification miss a state change ?

[Hugues Evrard]

Hi all,

I am a PhD student in the Convecs team at INRIA (France), which works on formal
methods. I am currently modeling Raft in LNT (a formal specification
language developed by Convecs) in order to use the CADP [1] toolbox for
verifications.

While reading through the Raft paper [2] and the TLA+ specification [3], it
seems to me that the specification misses a small state change. I am not fluent
in TLA+ though, so I may have just misunderstood the specification.

Liked depicted in Figure 4 in the paper, if a candidate discover a current
leader, it must become a follower. However, according to the formal
specification, it seems to me that a candidate which discover a leader with the
same term will not change state to become a follower.

Let's illustrate with a small example:
- SC is candidate for term t
- SL was also candidate for the same term, and has become leader for term t
- SL sends a heartbeat with term t to SC
- SC receives the heartbeat (i.e. a append entries request with 0
entry) with term t

At that point, according to the TLA+ specification, in Receive:
- UpdateTerm is not "evaluated", since m.mterm == currentTerm[SC]
- SC evaluates HandleAppendEntriesRequest:
- it will accept the heartbeat
- however, the state variable is not changed anywhere inside
HandleAppendEntriesRequest, so SC continue to be in state candidate

It seems to me that HandleAppendEntriesRequest should set the state of i to
follower as soon as m.mterm == currentTerm. I looked at the implementation of
LogCabin [4] and goraft [5], and candidates do "step down" to follower when a
new leader is elected.

I don't think this impacts the protocol correctness, since a non-elected
candidate behaves almost like a follower, the main difference being a candidate
never grant its vote to another one (and in the example the leader for this term
is already elected anyway). It could even be on purpose that the state is not
changed, as less variable modifications may simplify the formal specification.

What do you think about it ?

[1] http://cadp.inria.fr
[2] http://ramcloud.stanford.edu/raft.pdf
[3] https://ramcloud.stanford.edu/~ongaro/raft.tla
[4] https://github.com/logcabin/logcabin
[5] https://github.com/goraft/raft

Thanks,
--
Hugues Evrard
Inria & LIG - Team CONVECS - http://convecs.inria.fr - @convecs

[Diego Ongaro]

Hi Hugues,

Thanks for your very clear description of the problem. You're right:
it looks like that transition is missing from the spec. The intended
behavior is for candidates to go back to the follower state whenever
they receive an AppendEntries request from a leader of an equal or
greater term, and the spec doesn't do this for leaders of the same
term. That was just an omission on my part, and I'll fix it for my
thesis (thanks for the bug report). Fortunately, as you point out,
it's of little consequence to safety, since no vote information is
lost. Moreover, Restart(i) models a node restarting, which has servers
go back to Follower state anyhow, so it's already in the spec that
this server MAY make the Candidate->Follower transition and keep its
current term safely.

I'd also be interested to learn more about how you're modeling Raft
and the tools you're using. Maybe we can chat sometime?

Best,
Diego

[Hugues Evrard]

Hi Diego,

Thanks for your quick reply!

I am modeling Raft using the specification language LNT, whose syntax is close
to mainstream imperative and functional languages. The LNT model looks more like
an implementation: for each kind of received message, depending on the server
variables (state, term, etc), what shall we do. I guess that's what made me
notice the missing transition in the TLA+ spec.

The LNT model of Raft I'm working on is not polished yet, but I will be
happy to provide it once it's clean enough.

For an glimpse of LNT, you can have a look at the specification of a "Dynamic
reconfiguration protocol for mobile agents" [1], one of the demo shipped with
CADP. The files SPEC.lnt and DATA.lnt are the model, the prop*.mcl files are
properties (e.g. deadlock freedom) verified using the model checker tool of
CADP. Others demos are available from [2].

For my thesis, I am working on automatic distributed code generation from LNT,
and I plan to use Raft as an application example. I'll let you know if I manage
to get the LNT model "run" on a bunch of servers.

Feel free to contact me by mail for any information!

[1] ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_29/
[2] http://cadp.inria.fr/demos.html

Yours,
Hugues


----- Mail original -----
> De: "Diego Ongaro" <onga...@gmail.com>
> À: "Hugues Evrard" <hugues...@inria.fr>
> Cc: raft...@googlegroups.com
> Envoyé: Lundi 17 Février 2014 20:48:10
> Objet: Re: Does the TLA+ specification miss a state change ?