Graph- versus Vector-Based Analysis of a Consensus Protocol

Giorgio Delzanno, Arend Rensink, Riccardo Traverso

Abstract

The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.
Original languageUndefined
Title of host publicationProceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)
EditorsDragan Bošnački, Stefan Edelkamp, Alberto Lluch Lafuente, Anton Wijs
PublisherEPTCS
Pages44-57
Number of pages14
DOIs
StatePublished - Apr 2014

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherEPTCS
Volume159
ISSN (Print)2075-2180
ISSN (Electronic)2075-2180

Fingerprint

Model checking
Parallel algorithms
Communication

Keywords

  • EWI-24980
  • GROOVE
  • Graph Transformation
  • IR-91953
  • Consensus Protocols
  • Model Checking
  • METIS-305983
  • SPIN

Cite this

Delzanno, G., Rensink, A., & Traverso, R. (2014). Graph- versus Vector-Based Analysis of a Consensus Protocol. In D. Bošnački, S. Edelkamp, A. Lluch Lafuente, & A. Wijs (Eds.), Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014) (pp. 44-57). (Electronic Proceedings in Theoretical Computer Science; Vol. 159). EPTCS. DOI: 10.4204/EPTCS.159.5

Delzanno, Giorgio; Rensink, Arend; Traverso, Riccardo / Graph- versus Vector-Based Analysis of a Consensus Protocol.

Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). ed. / Dragan Bošnački; Stefan Edelkamp; Alberto Lluch Lafuente; Anton Wijs. EPTCS, 2014. p. 44-57 (Electronic Proceedings in Theoretical Computer Science; Vol. 159).

Research output: Scientific - peer-reviewConference contribution

@inbook{55767b7ab50b472fb015682be411c0dd,
title = "Graph- versus Vector-Based Analysis of a Consensus Protocol",
abstract = "The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.",
keywords = "EWI-24980, GROOVE, Graph Transformation, IR-91953, Consensus Protocols, Model Checking, METIS-305983, SPIN",
author = "Giorgio Delzanno and Arend Rensink and Riccardo Traverso",
note = "10.4204/EPTCS.159.5",
year = "2014",
month = "4",
doi = "10.4204/EPTCS.159.5",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "EPTCS",
pages = "44--57",
editor = "Dragan Bošnački and Stefan Edelkamp and {Lluch Lafuente}, Alberto and Anton Wijs",
booktitle = "Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)",

}

Delzanno, G, Rensink, A & Traverso, R 2014, Graph- versus Vector-Based Analysis of a Consensus Protocol. in D Bošnački, S Edelkamp, A Lluch Lafuente & A Wijs (eds), Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). Electronic Proceedings in Theoretical Computer Science, vol. 159, EPTCS, pp. 44-57. DOI: 10.4204/EPTCS.159.5

Graph- versus Vector-Based Analysis of a Consensus Protocol. / Delzanno, Giorgio; Rensink, Arend; Traverso, Riccardo.

Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). ed. / Dragan Bošnački; Stefan Edelkamp; Alberto Lluch Lafuente; Anton Wijs. EPTCS, 2014. p. 44-57 (Electronic Proceedings in Theoretical Computer Science; Vol. 159).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Graph- versus Vector-Based Analysis of a Consensus Protocol

AU - Delzanno,Giorgio

AU - Rensink,Arend

AU - Traverso,Riccardo

N1 - 10.4204/EPTCS.159.5

PY - 2014/4

Y1 - 2014/4

N2 - The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.

AB - The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker Spin on the basis of a vector-based encoding of the algorithm.

KW - EWI-24980

KW - GROOVE

KW - Graph Transformation

KW - IR-91953

KW - Consensus Protocols

KW - Model Checking

KW - METIS-305983

KW - SPIN

U2 - 10.4204/EPTCS.159.5

DO - 10.4204/EPTCS.159.5

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 44

EP - 57

BT - Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)

PB - EPTCS

ER -

Delzanno G, Rensink A, Traverso R. Graph- versus Vector-Based Analysis of a Consensus Protocol. In Bošnački D, Edelkamp S, Lluch Lafuente A, Wijs A, editors, Proceedings of the 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014). EPTCS. 2014. p. 44-57. (Electronic Proceedings in Theoretical Computer Science). Available from, DOI: 10.4204/EPTCS.159.5