Is raft automatically proved?
169 views
Skip to first unread message
Vasileios Anagnostopoulos
Jan 21, 2015, 9:35:05 AM1/21/15
to raft...@googlegroups.com
I found a TLA+ specification and prose (Natural Language) proofs in the PHD thesis. I am not a model checking expert, starting as of lately.
But could the prose proofs be automated?
thank you for your time to answer me.
But could the prose proofs be automated?
thank you for your time to answer me.
Diego Ongaro
Jan 21, 2015, 12:31:36 PM1/21/15
to Vasileios Anagnostopoulos, raft...@googlegroups.com
Hi Vasileios,
You can find more information about the spec/proof in Chapter 8. I
never completed a machine-checked proof for Raft, as the approach I
took using TLAPS wasn't scaling well. A machine-checked proof is
certainly possible, however, and it's also entirely feasible. I know
of some others that are working on one using Coq, though I don't know
if they're ready to discuss it publicly.
If you're interested in model checking (you mentioned it too in your
email), you might want to check out this recent paper by Hugues Evrard
and Frédéric Lang, which uses Raft as a case study:
https://hal.inria.fr/hal-01086522 to appear in PDP'15.
Hope that answers your questions,
Diego
> --
> You received this message because you are subscribed to the Google Groups
> "raft-dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to raft-dev+u...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
You can find more information about the spec/proof in Chapter 8. I
never completed a machine-checked proof for Raft, as the approach I
took using TLAPS wasn't scaling well. A machine-checked proof is
certainly possible, however, and it's also entirely feasible. I know
of some others that are working on one using Coq, though I don't know
if they're ready to discuss it publicly.
If you're interested in model checking (you mentioned it too in your
email), you might want to check out this recent paper by Hugues Evrard
and Frédéric Lang, which uses Raft as a case study:
https://hal.inria.fr/hal-01086522 to appear in PDP'15.
Hope that answers your questions,
Diego
> You received this message because you are subscribed to the Google Groups
> "raft-dev" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to raft-dev+u...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Hugues Evrard
Jan 21, 2015, 1:10:57 PM1/21/15
to raft...@googlegroups.com
Hi Vasileios,
On 01/21/15 18:31, Diego Ongaro wrote:
>
> If you're interested in model checking (you mentioned it too in your
> email), you might want to check out this recent paper by Hugues Evrard
> and Frédéric Lang, which uses Raft as a case study:
> https://hal.inria.fr/hal-01086522 to appear in PDP'15.
>
Thanks Diego for the reference !
Note that the paper focus by large on our
formal-specification-to-distributed-implementation tool, named DLC, for
which Raft is used as a case study. In a nutshell, we model Raft in a
specification language called LNT, with which we can perform formal
verification techniques (model checking, and more!) using the CADP
toolbox (https://cadp.inria.fr/). Then, DLC is able to produce a
distributed implementation from the LNT model, so we obtain a rapid
distributed prototype from a formal specification.
Unfortunately, there was not enough room to discuss the verification
part, and to be honest I'm still working on polishing LNT-Raft in order
to perform verifications of reasonable configurations. Note that we have
a model checking approach, which is different from the proof approach
where Coq could be used.
As soon as I have a stable version of LNT-Raft uploaded somewhere on the
web, I'll announce it to this mailing list. In the meantime, I'll be
happy to discuss any effort concerning the formal verification of Raft.
Best,
--
Hugues Evrard
INRIA / LIG - Team CONVECS
On 01/21/15 18:31, Diego Ongaro wrote:
>
> If you're interested in model checking (you mentioned it too in your
> email), you might want to check out this recent paper by Hugues Evrard
> and Frédéric Lang, which uses Raft as a case study:
> https://hal.inria.fr/hal-01086522 to appear in PDP'15.
>
Note that the paper focus by large on our
formal-specification-to-distributed-implementation tool, named DLC, for
which Raft is used as a case study. In a nutshell, we model Raft in a
specification language called LNT, with which we can perform formal
verification techniques (model checking, and more!) using the CADP
toolbox (https://cadp.inria.fr/). Then, DLC is able to produce a
distributed implementation from the LNT model, so we obtain a rapid
distributed prototype from a formal specification.
Unfortunately, there was not enough room to discuss the verification
part, and to be honest I'm still working on polishing LNT-Raft in order
to perform verifications of reasonable configurations. Note that we have
a model checking approach, which is different from the proof approach
where Coq could be used.
As soon as I have a stable version of LNT-Raft uploaded somewhere on the
web, I'll announce it to this mailing list. In the meantime, I'll be
happy to discuss any effort concerning the formal verification of Raft.
Best,
--
Hugues Evrard
INRIA / LIG - Team CONVECS
Vasileios Anagnostopoulos
Jan 22, 2015, 3:28:22 AM1/22/15
to Hugues Evrard, raft...@googlegroups.com
Thank you very much I will check it out. Since I am an MC newbie, I would like to ask if nuSMV is suitable for this kind of task just to do some baby learning steps and have some diversity.
I still repeat that I am doing baby steps, I have seen a lot of hard math (hopf algebras, symmetric group combinatorics, graph algorithms, functional/harmonic analysis) and code but MC is something new for me and explore the software space. We modified Raft for another use case where we have created an algorithm but it is not ready until verified. When finished I will be happy to share.On Wed, Jan 21, 2015 at 8:28 PM, Hugues Evrard <hugues...@inria.fr> wrote:
Hi Vasileios, I just realized I forgot to include you in the receivers
of my previous response, so I forward it here in case you don't have
subscribed yet to the raft-dev mailing list.
Otherwise, sorry for the double send.
--
You received this message because you are subscribed to the Google
Groups "raft-dev" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to raft-dev+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--
Dr. Vasileios Anagnostopoulos (MSc,PhD)
Researcher/Developer
ICCS/NTUA 9 Heroon Polytechneiou Str., Zografou 15773 Athens,Greece
Hugues Evrard
Jan 23, 2015, 7:09:39 AM1/23/15
to Vasileios Anagnostopoulos, raft...@googlegroups.com
On 01/22/15 09:28, Vasileios Anagnostopoulos wrote:
> Thank you very much I will check it out. Since I am an MC newbie, I
> would like to ask if nuSMV is suitable for this kind of task just to do
> some baby learning steps and have some diversity.
>
I really don't know the details of nuSMV or symbolic model checking, so
> Thank you very much I will check it out. Since I am an MC newbie, I
> would like to ask if nuSMV is suitable for this kind of task just to do
> some baby learning steps and have some diversity.
>
I cannot comment about the relevance of this tools for a system like a
Raft cluster.
For what I know, nuSMV and CADP have quite different approaches, for
instance nuSMV is state-based (information is related to a system state)
and symbolic (encode the system in an symbolic expression), while CADP
is action-based (information is related to actions (events) of the
system) and usually generates the whole state space explicitly. nuSMV
uses techniques like SAT-solving to check properties, whereas EVALUATOR4
[0] (one of CADP model checkers) walks into the state space to verify a
property. It would be great to have a nuSMV model of Raft for comparison!
Besides, I suggest you to express the properties you want to check early
on. A model checker has two main inputs, a system and a property, and
one often focus on the system description, but it is nice to know early
on what property you want to verify.
Regarding Raft, you can start to model the leader election phase and
verify the Election Safety property. You can refer to the example in
section 3 of the PDP'15 paper for an overview on how it can be done with
CADP tools.
> I still repeat that I am doing baby steps, I have seen a lot of hard
> math (hopf algebras, symmetric group combinatorics, graph algorithms,
> functional/harmonic analysis) and code but MC is something new for me
> and explore the software space. We modified Raft for another use case
> where we have created an algorithm but it is not ready until verified.
> When finished I will be happy to share.
>
If you want to thoroughly demonstrate the correctness of a system, you
should look into proofs, where proof assistants such as Coq [1] can be used.
All the best for your project !
Hugues
[0] http://cadp.inria.fr/tools.html#section-5
EVALUATOR4 man page : http://cadp.inria.fr/man/evaluator4.html
[1] https://coq.inria.fr/
> For more options, visit https://groups.google.com/d/optout.
>
>
>
>
>
> --
> Dr. Vasileios Anagnostopoulos (MSc,PhD)
> Researcher/Developer
> ICCS/NTUA 9 Heroon Polytechneiou Str., Zografou 15773 Athens,Greece
> T (+30) 2107723404 M (+30) 6936935388
> E va...@mail.ntua.gr
> <mailto:va...@mail.ntua.gr><mailto:va...@mail.ntua.gr
>
>
>
>
>
> --
> Dr. Vasileios Anagnostopoulos (MSc,PhD)
> Researcher/Developer
> ICCS/NTUA 9 Heroon Polytechneiou Str., Zografou 15773 Athens,Greece
> T (+30) 2107723404 M (+30) 6936935388
> E va...@mail.ntua.gr
> <mailto:va...@mail.ntua.gr>> www.ntua.gr
> <http://www.ntua.gr><http://www.ntua.gr/>
Reply all
Reply to author
Forward
0 new messages