DAVE

Description

Distributed Asynchronous Verification Emulator (DAVE) is a software to verify the correctness of distributed and hence asynchronous algorithms in case of different failings including node crashes, disconnections etc

Build Requirements

• Supported compilers (must support c++11):
  • GCC
  • Clang
  • MSVC
• Libraries: BOOST, version >= 1.56

Replicated Object Verification

DAVE allows to verify masterless consensus algorithm known as replob. For detailed information please read the following articles:

1. Replicated Object. Part 1: Introduction
2. Replicated Object. Part 2: God Adapter
3. Replicated Object. Part 7: Masterless Consensus Algorithm

Configuration parameters:

1. Number of nodes nodes: 3
2. Maximum number of failed nodes per each execution maxFailedNodes: 1
3. Minimal node id of unreliable node minUnreliableNode: 1 (meaning that node #0 is always reliable while others are not).

struct Config
{
    int nodes = 3;
    int maxFailedNodes = 1;
    int minUnreliableNode = 1;
    // ...
};

Number of performed executions to check all variants for the Calm version:

Concurrent Messages	Client Nodes	Verified Variants
1	#0	59 986
2	#0, #1	148 995 211
3	#0, #1, #2	734 368 600

Clients propose the messages started from node #0.

Verification checks:

1. Nonfailed nodes must commit.
2. Failed node may or may not commit.
3. Any committed node (failed or nonfailed) must have the same committed sequence prefix of messages: agreement.