Testing Distributed Systems for Linearizability

Designing a distributed system poses a significant challenge, as need to keep track of a lot of constraints including but not restricted to consistency, fault-tolerance, and performance expectations. However, once such a system is designed, it raises a question about proving the correctness of the system. To provide a foolproof method of correctness, formal methods are widely used, however writing specifications for the overall distributed system requires dedicated effort, as formal methods are more of mathematical models, which is equivalent to the coded models, and needs expertise in formal method specification. The use of formal methods is the best approach in terms of finding some subtle bugs beforehand. In opposing this, another low-effort way is to use linearizibility to test the system.

Part of the Distributed Systems Papers series (14 parts)

1. RAFT Consensus Algorithm
2. Amazon DynamoDB - Distributed Transactions
3. Amazon DynamoDB - Architecture
4. Introduction to Map-Reduce
5. Introduction to Google File System
6. Fault-Tolerant Virtual Machines
7. Testing Distributed Systems for Linearizability ← you are here
8. Intro to Zookeeper
9. Chain Replication
10. Properties of Distributed Transaction
11. Frangipani - A Scalable Distributed FileSystem
12. Amazon Aurora DB Design Considerations
13. Introduction to Bitcoin Protocol
14. Byzantine Consensus

Definition:

An execution history is supposed to be linearizable if the order of the operation matches real-time for non-concurrent operations, and each read request responds with the most recent write operation. By definition, linearizability ensures strong consistency of the distributed system.

Linearizable:

The general approach to test linearizability is to first capture the execution history by introducing different types of faults randomly. Then the captured execution history is fed into linearizable checkers like Jespen or Knossos.

Example of a linearizable execution history:

Example of a linearizable execution history: linearizable

Example of a non-linearizable execution history:

Example of a non-linearizable execution history: non linearizable

To be explored:

• Explore how Knossos and Jespen work, use them in application

References:

1. Distributed Systems Safety Tool: Knossos
2. Distributed Systems Safety Research: Jespen
3. Jepsen 9: A Fsyncing Feeling • Kyle Kingsbury • GOTO 2018
4. Testing Distributed Systems for Linearizability