Synthesis of Fault-Tolerant Distributed Algorithms

Synthesis of Fault-Tolerant Distributed Algorithms

Fault-Tolerant Interactive Consistency

We synthesized an algorithm for achieving interative consistency in presence of transient, non-malicious and asymmetric faults. The work is described in detail in a NFM 2014 paper.

Here are some SAL models used for performing synthesis.

ls_syn_with_nil_liar_changes_initialized.sal: Result of synthesis; remove initialization in module named control to get partial model
NFM2014_submission16.sal : The starting SAL model with synthesis variables
NFM2014_submission16.qdimacs: The QBF formula generated from the SAL model.
NFM2014_submission16.variable_mapping . This file contains the mapping from variables of the SAL model NFM2014_submission16.sal to universally quantified variables in the QBF formula NFM2014_submission16.qdimacs
NFM2014_submission16_preprocessed.qdimacs

Draper Clock-Synchronization Protocol

In 1973, Daly, Hopkins, and McKenna (from Draper Lab.) presented a fault-tolerant digital clocking system at the FTCS conference. This is probably one of the first published system designs that is intended to tolerate arbitrary, asymmetric faults (i.e., Byzantine faults).

The following SAL models (05/14/2012) are two variant formalizations of this Draper Clock-Synchronization Protocol developed by Ashish Tiwari.

We also used QBF solvers to synthesize deterministic Byzantine consensus procedures. The following SAL models (08/19/2013) were used to perform synthesis. Note that the models have uninitialized parameters - and hence SAL will be unable to prove anything interesting about them. The models were used as automatically construct an input for a QBF solver.

clocksyncsynth_3.sal (true Byzantine model)
clocksyncsynth_Null_3.sal (faulty node gives correct val or Null)
clocksyncsynth_Null_3_with_history.sal (faulty node gives correct val or Null; good clocks allowed to keep history)

Brief summary of the synthesis results: In general, most synthesis results were negative; i.e., there exist no deterministic Byzantine fault-tolerant consensus algorithms. For case when faulty clock is disallowed ONE specific behavior, we can synthesize a deterministic consensus algorithm. When the faulty clock can send values in the set {Null,1} or in the set {Null,0}, but not values in the set {0,1}, then the result is the same: no deterministic algorithm exists. If we force the faulty clock to also 'behave' and follow the protocol that the good clocks are following, and then send values from {Null,1} if its value is 1 and values from the set {Null,0} if its value is 0, then the result, surprisingly, is STILL THE SAME. If bad clock is forced to remain bad in the same way for 2 time steps, then we get a positive result: in fact, two different solutions were synthesized.

Dijkstra's Reaching Mutual Exclution

We synthesized the second solution in Dijkstra's paper on an algorithm for reaching a state where $n$ processes in a ring get mutually exclusive turn to execute.

Here are some SAL models used for performing synthesis.

dijkstra_4_states.sal

SAL files referenced in the paper "Synthesis of a simple self-stabilizing system".

Publications

A. Gascon and A. Tiwari, "A Synthesized Algorithm for Interactive Consistency". pdf. In NFM 2014.

Talks/Lectures

This page is maintained by Ashish Tiwari.
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page