This paper demonstrates a framework for distributed protocols. The framework makes it possible to:
- walk through the states of system
- verify invariants of the system
- derive/verify implementations directly from the specifications
Point 3 separates it from other such proof assistants like TLA+ or Coq, which fall short on ensuring that the implementation follows specifications. The paper introduces a few fundamental distributed protocols which can then be combined to create more complex protocols. It uses type classes to make the implementation flexible and extensible.
The paper introduces a few concepts:
- A state-transition system (STS) which is local to each node
- A node which maintains its internal state and communicates with other nodes by message passing
- A protlet (protocol + droplet) specifies a logically independent fixed interaction between nodes
A protlet specifies the interaction that can happen between one ore more nodes. Multiple protlets can be used together to construct the functionality required by a distributed protocol. For e.g Paxos is implemented using two phases of quorum. The protlets are defined such that they are highly reusable. For e.g. ARPC (Asychronous RPC) is used in a batch calculator to batch together many operations before returning the result, and it is also used in a distributed lock where the client acquires the lock and calls a procedure on the server which the server can take any amount of time to complete before returning the result.
Each message contains labels which can be used to distinguish between two copies of the same protlet running on the same node. This is the case when the protlets have different functionality for e.g. there are two RPC protlets in the calculator example one does addition and the other multiplication.
The framework introduces a SpecNetwork data type which stores the global state of all protlets running on each node, indexed by their labels. Any message passing between two nodes creates a transition that changes the state of the target protlet. This makes it possible to track the global state after every step. Moreover the NetworkState object consists of the global state of SpecNetwork and the local states of each node. Each node contains not only it's current state but also the messages currently in the queue. This becomes useful in verification as explained later.
DPC also implements a function stepProtlet which tries execute each step of a protlet one by one blocking wherever it cannot proceed. One useful outcome of having a step based implementation is that:
- The next state for the entire system can be chosen from a list of possible next states
- The next state can be chosen by user input allowing the user to walk through the states of the system in a graphical interface
The implementation of a protlet is parameterized over a monad. There can be multiple possible implementations of it, some can be focused on efficiency others on correctness and so on. The paper presents three implementations:
- Pure implementation - This creates an eDSL which represents all the operations in running a distributed protocol like send and receive message. This implementation can be used to create traces and to check invariant properties at each step of the execution.
- Shared memory implementation - This considers nodes to be different execution threads that send and receive messages from a shared memory pool
- Web socket implementation - This implementation allows creating an executable that can be run on different hosts
A key difference between other proof assistants and DPC is that it does the verification dynamically. The pure implementation converts the eDSL specification to an AST. This AST is interpreted while generating a trace of the states its passing through. Since the state consists of both global and local states including the messages queue in each node, it can be checked to satisfy invariants for that path of execution. While this means that protocol cannot be verified statically it works out well enough in practice.
Protlet annotations is another concept introduced in dpc. It allows annotating a Protlet specification with checks that that must hold in the implementation. This builds correctness into declaration itself, however the framework is flexible enough to allow ignoring the rules of these annotations for implementations where efficiency is of greater concern.
- In the framework transitions occur when a node performs an action. This makes it difficult to model protocols in the data link layer wireless protocols which period based actions like slotted aloha and synchronous TDMA. But this may not be a very valid concern since this framework is focused on distributed protocols at the application layer.