Reasoning about knowledge - Part 1

In this series of posts, I will talk about the reasoning about knowledge like how to reach an agreement under different harsh conditions. This field is called Epistemic modal logic and this post will mainly discuss reaching agreement in the presence of faults in the distributed system.

Introduction

Reaching an agreement in the presence of faults in the distributed system is an enduring problem in computer science and epistemic modal logic. The solutions of this problem are widely used in Cryptocurrency and aerospace industry.
One of the most famous algorithms is mentioned in Reaching Agreement in the Presence of Faults, which later became the well-known Byzantine Fault Tolerance problem.

Conventions

Faulty

The faulty in here refers to the fact that the processor can report whatever it wants, which means it can lie like report \(K_{1}\) to some processors and report \(K_{2}\) to another group of processors.

Interactive Consistency

Interactive Consistency requires following prerequisites:

  1. Non-faulty processors have the same vector.
  2. In every non-faulty processor, the element corresponding to a given non-faulty processor is the private value of that processor.


Problem

Consider there are \(n\) processors in which \(m\) processor(s) is(are) faulty \((n,m\in{}\mathbb{N}_{+})\).
Every processor \(p\) keeps a value \(V_{p}\). And every processor has a vector of \(n\) length, which comprises the values of every processor (include itself). The purpose is devising an algorithm which computes a vector that satisfies the interactive consistency.

Algorithm

The algorithm in the Reaching Agreement in the Presence of Faults is quite abstract and complex. In this section, I will spoil it down for you.
This algorithm only applies to the situation in which \(n>3m\). We will prove that the \(n>3m\) is the necessary and sufficient condition.
In order to describe the algorithm easily, we will describe it in a formal way.

Definitions

Sets

Let \(P\) be a set of processors.
We also need \(n\) trees. Each tree's root node is denoted by one processor's name respectively. Let \(T\) be a set of the trees.

Notation

For any tree \(t\), we denote the properties of that as \(S(d,f)\) in which \(d\) stands for the depth of the tree and \(f\) stands for the number of the faulty processors (include root node) in the subtree.

Functions

  • Evaluator \(\sigma{}(w)\)

    \(\sigma{}(w)\) gives the value of the node which is denoted by the edge \(w\) (\(w\) is a string which comprises names of processors. e.g. \(w=p_{1}p_{2}p_{3}\)).
    Furthermore, we can deduce that \(\sigma{}(pw)=\sigma{}(p)\) where \(w\) comprises names of non-faulty processors since non-faulty processors always pass on the value directly.

  • Sender \(\varphi{}(w)\)

    \(\varphi{}(w)\) sends the value of \(\sigma{}(w)\) to every processor \(p\in{}\complement_{P}\scriptsize W\) (\(W\) is a set which comprises all the names of the processors in the \(w\)).

  • Receiver \(\xi{}(w,v)\to{}w'\)

    If the edge is not illegal(trying to override or \(w\) is not ended with the sender's name), \(\xi{}(w)\) will append the receiver's own name to the \(w\) (the new string is called \(w'\)). And store the received value \(v\) to the tree according to the edge \(w'\). Finally, it returns \(w'\)

Procedure

For a processor \(p\in{}P\), follow these steps:

  1. Performs \(\varphi{}(p)\).
  2. Receives the values from others by performing \(\xi{}(w,v)\). Then performs \(\varphi{}(w')\).
  3. Performs step 2 repeatedly until there is nothing to receive.
  4. (For the first time, starts from the bottom of the tree) Performs the \(majority\) function on a group of nodes which share the same parent, then replaces the value of the parent by the result of the \(majority\) function. In the end, moves to the upper level.
  5. Performs step 4 repeatedly until the top level.
  6. Redoes step 4 and 5 for every tree \(t\in{}T\).

The vector of the values of the root nodes of all the trees in \(T\) satisfies the interactive consistency.

Example

This is an example of the tree of processor \(p_{4}\) from viewpoint of \(p_{1}\) (\(n=4,m=1\)):

                              +--------+
                              |   p4   |
                              |        |
                              +----+---+
                              |    |   |
                              |    |   |
    +-------------------------+    |   +-------------------------+
    |                              |                             |
+---+---+                      +---+---+                     +---+---+
|   p2  |                      |   p3  |                     |   p1  |
|       |                      |       |                     |       |
+---+---+                      +---+---+                     +-------+
    |                              |
+---+---+                      +---+---+
|   p1  |                      |   p1  |
|       |                      |       |
+-------+                      +-------+



Proofs

Conventions

Interactive Consistency for tree

We call following rules Interactive Consistency for tree:

  1. For every viewpoint, the evaluated value of the tree is the same. (\(IC'_{1}\))

  1. If the root node of the tree is non-faulty, the evaluated value for every viewpoint should be \(\sigma{}(EdgeToRoot)\). (\(IC'_{2}\))

In particular, \(IC'_{1}\) follows from \(IC'_{2}\) if the root node is non-faulty.
If every tree \(t\in{}T\) satisfies both \(IC'_{1}\) and \(IC'_{2}\), the \(T\) satisfies interactive consistency.

Proof of correctness for \(n>3m\)

Lemma 1

Lemma 1: For all \(n>3m\) cases, tree \(t\in{}T\) satisfy \(IC'_{2}\) if the root node of the tree is non-faulty.
Proof: Let \(n=3m+k\ (k\in{}\mathbb{N}_{+})\). The degree of any node in depth \(d\) is: \[D_{d} = \begin{cases} n-d-1 &\text{if } d\in{}[0,m] \\ 0 &\text{if } d=m+1 \end{cases}\] For any subtree \(S(i,j)\text{ where }i\in{}[0,m),j\in{}[0,m]\): \[\tag{1} \begin{aligned} D_{i}-m &= n-d-1-m \\ &= 2m+k-d-1 \\ &\geq{} m+k \end{aligned}\] \(D_{i}-m\geq{}m+k\) indicates subtree \(S(i,j)\) can tolerate that at most \(m\) faulty processor(s) is(are) its child(ren) since the majority of its child is non-faulty processor.
The proof of the Lemma 1 is by induction on \(i\) \((m\geq{}2)\).

  • \(Basic\ i=m-1\) if the root node of subtree \(S(m-1,j)\) is non-faulty, by (1), we can know that it satisfies \(IC'_{2}\).
  • \(Induction\ Step\ i\in{}[0,m-2]\) We assume non-faulty-root subtrees \(S(i+1,j)\) satisfy \(IC'_{2}\), and prove it for non-faulty-subtree subtree \(S(i-1,j)\). By (1), we can prove it.

For \(m=1\), it is proved in the basic section in induction proof.
Therefore, tree \(t\in{}T\) of \(S(0,m)\) satisfies \(IC'_{2}\).\(\ \square\)

Theorem 1

Theorem 1 For all \(n>3m\) cases, tree \(t\in{}T\) satisfy both \(IC'_{1}\) and \(IC'_{2}\).
Proof Because \(IC'_{1}\) follows from \(IC'_{2}\) if the root node is non-faulty, we only need prove the case where the root node is faulty.
By the induction in the proof of Lemma 1, we know that every non-faulty processor can always get the same value with any non-faulty-subtree \(S(i,j)\text{ where }i\in{}[0,m),j\in{}[0,m]\). So we can replace the value of root node of \(S(i,j)\) with the evaluated value and eliminate every subtree of it.
Obviously, for any faulty-subtree \(t'\) whose child(ren) all satisfy \(IC'_{1}\), \(t'\) also satisfies \(IC'_{1}\).
Therefore, \(t\) satisfies \(IC'_{1}\). Hence, for all \(n>3m\) cases, tree \(t\in{}T\) satisfy both \(IC'_{1}\) and \(IC'_{2}\).\(\ \square\)

Proof of impossibility for \(n\leq{}3m\)

Proof Let \(n=3m-k\ (k\in{}\N)\). If \(n\leq{}3m\), then \(D_{i}-m\leq{}m-k\) in (1), which leads to inevitable failure of \(Basic\) in the induction of Lemma 1. Therefore, Theorem 1 can't be proved.\(\ \square\)

Conclusion

It took me at least 1 month to finish this post. The journey of learning this algorithm is quite hard for me but exciting. This algorithm is the bedrock of many other theories, Libra's consensus algorithm is also based on that. However, this algorithm has many restrictions such as no-latency communication between processors, which are very ideal and unrealistic in reality.
The incentive of writing this post is that few people are trying to spoil it down and prove the algorithm for others. Almost every post of proof or explanation of this algorithm I saw is copy-pasty post. I think it is essential for me to understand the algorithm thoroughly and write it down for both me and you.

References

  1. M. Pease, R. Shostak, and L. Lamport. 1980. Reaching Agreement in the Presence of Faults. J. ACM 27, 2 (April 1980), 228-234. DOI=http://dx.doi.org/10.1145/322186.322188
  2. Leslie Lamport, Robert Shostak, and Marshall Pease. 1982. The Byzantine Generals Problem. ACM Trans. Program. Lang. Syst. 4, 3 (July 1982), 382-401. DOI=http://dx.doi.org/10.1145/357172.357176