Distributed Consensus, Revisited

Rachele Fuzzati, Massimo Merro
2007
Journal paper

We provide a novel model to formalize a well-known algorithm, by Chandra and Toueg, that solves Consensus among asynchronous distributed processes in the presence of a particular class of failure detectors (Diamond S or, equivalently, Omega), under the hypothesis that only a minority of processes may crash. The model is defined as a global transition system that is unambigously generated by local transition rules. The model is syntax-free in that it does not refer to any form of programming language or pseudo code. We use our model to formally prove that the algorithm is correct.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts

Related publications

Rachele Fuzzati, Massimo Merro
2007
Journal paper

Abstract

Official source

https://infoscience.epfl.ch/record/104369?ln=en

About this result

Related concepts (10)

Related concepts

Related publications (6)

Related publications

Programming language

A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer

Failure detector

In a distributed computing system, a failure detector is a computer application or a subsystem that is responsible for the detection of node failures or crashes. Failure detectors were first introduce

Pseudocode

In computer science, pseudocode is a plain language description of the steps in an algorithm or another system. Pseudocode often uses structural conventions of a normal programming language, but is i

Distributed Consensus, Revisited

Rachele Fuzzati, Massimo Merro

2006

Style Checking With Scala.Meta

Eugene Burmako, Mathieu Baptiste Demarne

In many companies, code reviews are big parts of the day-to-day life of an engineer. Some can argue that the time spent on someone else’s code is time that some cannot spent on her or his own work. Code reviews usually allow to find two kinds of issues. The first kind consists of high-level design errors compared to the specifications of the program while the second type consists of style problems. In this report, we argue that the search of the later kind of error can be automated, as the set of style issues is usually well defined for a programming language. We propose modifications to a linter tool called Obey, which allows to analyze Abstract Syntax Trees of Scala code, raise warnings and suggest changes that can be automatically persisted. Over the course of this project we worked jointly with Codacy, a company proposing automated code reviews, to have an industrial application which would allow users to define their own set of rules. This report also presents the results of this real life testing.

2015

Two approaches to portable macros

Eugene Burmako, Fengyun Liu

For any programming language that supports macros and has multiple implementations (each with different AST definitions), there is a common problem: how to make macros that operate on ASTs portable among different compiler implementations? Implementing portable macros is especially important for statically typed languages like Scala, as IDE vendors usually have different implementations of the language in order to support rich IDE features. Unportable macros compromise IDE features and degrade programming experience. We describe two approaches to the portability problem based on two different views on macros: (1) the tree-based approach, which views macros as operations on abstract syntax trees, solves the problem by defining standard abstract syntax trees; (2) the syntax-based approach, which views macros as operations on abstract syntax, solves the problem by defining standard abstract syntax. We show that the latter has significant practical advantages, especially in supporting semantic macros that use type information of ASTs to transform user code. Based on the idea, we implemented a new macro system, Gestalt, for the experimental Scala compiler, Dotty. The new implementation solves several long-standing problems of the current Scala macro system and demonstrates advantages over alternative approaches. Our solution has been adopted in the official new Scala macro system.

2017