dc.contributor.author | Georgiou, Chryssis | en |
dc.contributor.author | Hadjiprocopiou, Procopis | en |
dc.contributor.author | Musiał, Peter M. | en |
dc.creator | Georgiou, Chryssis | en |
dc.creator | Hadjiprocopiou, Procopis | en |
dc.creator | Musiał, Peter M. | en |
dc.date.accessioned | 2019-11-13T10:40:09Z | |
dc.date.available | 2019-11-13T10:40:09Z | |
dc.date.issued | 2010 | |
dc.identifier.issn | 0302-9743 | |
dc.identifier.uri | http://gnosis.library.ucy.ac.cy/handle/7/53983 | |
dc.description.abstract | Paxos is a well known algorithm for achieving consensus in distributed environments with uncertain processing and communication timing. Implementations of its variants have been successfully used in the industry (eg., Chubby by Google, Autopilot cluster management in Bing by Microsoft, and many others). This paper addresses the challenge of the manual coding of complex distributed algorithms, such as Paxos, where this is an error prone process. Our approach in ensuring correct implementation is to use a verified automated translator to compile a source specification that has been proven to be itself correct. We use specification of the Paxos algorithm in the General Timed Automata (GTA) model, an extension of I/O Automata, as input to an augmented compiler for the Input/Output Automata notation (a.k.a., the IOA compiler) in order to generate executable Java code. The resulting code is interfaced with MPI for communication needs. We have extended the IOA compiler to support a version of the GTA model, which uses time-passage actions such as ν(t), to model the passage of time by t time units. A time-based version of Paxos is used to demonstrate the capabilities of our extension. In this paper we describe the process to be followed in order to compile time-based Paxos, or similar algorithms. The utility of our approach is supported by an experimental evaluation of our Paxos implementation on a collection of workstations. To the best of our knowledge, our case study constitutes the first example of a time-dependent distributed algorithm that has been specified, verified and implemented in an automated way, using a common formal methodology. © 2010 Springer-Verlag. | en |
dc.source | 14th International Conference on Principles of Distributed Systems, OPODIS 2010 | en |
dc.source.uri | https://www.scopus.com/inward/record.uri?eid=2-s2.0-78650898691&doi=10.1007%2f978-3-642-17653-1_19&partnerID=40&md5=5973c95c21da7926e0bdba98b7effabf | |
dc.subject | Specifications | en |
dc.subject | Algorithms | en |
dc.subject | Automation | en |
dc.subject | Program compilers | en |
dc.subject | Time-dependent | en |
dc.subject | Time units | en |
dc.subject | Distributed algorithm | en |
dc.subject | Compile time | en |
dc.subject | Distributed environments | en |
dc.subject | Experimental evaluation | en |
dc.subject | Cluster management | en |
dc.subject | Error-prone process | en |
dc.subject | I/O Automata | en |
dc.subject | Input/output automata | en |
dc.subject | Java codes | en |
dc.subject | Manual coding | en |
dc.subject | MicroSoft | en |
dc.subject | Paxos algorithms | en |
dc.subject | Timed Automata | en |
dc.subject | Uncertain processing | en |
dc.title | On the automated implementation of time-based Paxos using the IOA compiler | en |
dc.type | info:eu-repo/semantics/article | |
dc.identifier.doi | 10.1007/978-3-642-17653-1_19 | |
dc.description.volume | 6490 LNCS | en |
dc.description.startingpage | 235 | |
dc.description.endingpage | 252 | |
dc.author.faculty | 002 Σχολή Θετικών και Εφαρμοσμένων Επιστημών / Faculty of Pure and Applied Sciences | |
dc.author.department | Τμήμα Πληροφορικής / Department of Computer Science | |
dc.type.uhtype | Article | en |
dc.description.notes | <p>Conference code: 83362</p> | en |
dc.source.abbreviation | Lect. Notes Comput. Sci. | en |
dc.contributor.orcid | Georgiou, Chryssis [0000-0003-4360-0260] | |
dc.gnosis.orcid | 0000-0003-4360-0260 | |