Demonstration - Model Checking Knowledge in Consensus Protocols

This page provides demonstrations of a number of MCK scripts developed in the course of project DST RA ID10136.

The project is considering protocols for solving the consensus problem in faulty distributed systems: a number of agents each start the protocol with a vote for a value to be agreed upon by the participating agents. An unknown subset of these agents may be faulty, possibly behaving incorrectly in ways that depend on the failure model. The end goal of the protocol is to ensure that the non-faulty agents all decide upon the same value, which should be the vote of one of the non-faulty agents.

On this page, we focus on the Synchronous Byzantine Agreement (SBA) version of this problem, in which the non-faulty agents are required to make their decision simultaneously. We also restrict to the case where there are just two options for the decision: 0 or 1 (e.g., commit or abort a transaction).

A knowledge-theoretic analysis by Dwork and Moses (1990) of SBA has established that the exact information required by agents to make a simutaneous decision is a kind of common knowledge. For example, to decide a 0, the nonfaulty agents should know the (infinite) conjunction

(1) at least one non-faulty agent voted for 0, and
(2) all the nonfaulty agents know (1), and
(3) that all the nonfaulty agents know (2), and
etc.

This concept can be expressed as a (greatest) fixpoint of the equation X = all nonfaulty agents know (X and at least one nonfaulty agent voted 0).

Parameters for the models include:

The number of agents. We have considered larger values of the parameters, but there is generally a rapid explosion in running times. For efficiency of the demonstration, all the examples on this page use three agents and two values to be decided.
The failure model. This may be
- Crash: a faulty agent may stop operating at some point, sending an arbitrary subset of the messages it was supposed to send in that round, after which it sends no further messages.
- Atomic Crash: a faulty agent may stop operating at some point, either sending none of the messages it was supposed to send in that round, or sending all of the messages it was supposed to send.
- Sending Omissions: a faulty agent may omit to send any of the messages it is supposed to send, at any time.
- Receiving Omissions: a faulty agent always sends all its messages, but may omit to receive any of the messages it has been sent.
Each failure model also specifies an upper bound t on the number of faulty agents in any run of the systems. Always t is less than the number n of agents in the system. All the models are for synchronous, reliable network model: unless either the sender or the receiver fails, a message is delivered in the round in which it is sent.
A specific protocol intended to solve the problem in the given failure model.

The simplest of the protocols in this demonstration is the Flooding protocol of Lynch, Distrbuted Algorithms, Ch 6: each agent repeatedly sends, to all other agents, the set of votes for the decision to be made of which it is aware. (Initially, a agent is aware only of its own vote.) Lynch's protocol, is intended for the crash failure model, and specifies that all agents make a decision after round t+1. The variants allow decisions to be made at earlier times. They achieve this either by using information about the failure model, or by distributing or maintaining more information than in the flooding protocol. In some cases, what is verified is that the protocol inherently does NOT distribute enough information to allow a decision to be made earlier than in the flooding protocol.

Select an MCK script, and click "verify" to submit the script for processing.

Script	Result