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
- Supported compilers (must support c++11):
- GCC
- Clang
- MSVC
- Libraries: BOOST, version >= 1.56
DAVE allows to verify masterless consensus algorithm known as replob. For detailed information please read the following articles:
- Replicated Object. Part 1: Introduction
- Replicated Object. Part 2: God Adapter
- Replicated Object. Part 7: Masterless Consensus Algorithm
Configuration parameters:
- Number of nodes
nodes
: 3 - Maximum number of failed nodes per each execution
maxFailedNodes
: 1 - 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:
- Nonfailed nodes must commit.
- Failed node may or may not commit.
- Any committed node (failed or nonfailed) must have the same committed sequence prefix of messages: agreement.