Specifying Distributed Hash Tables with Allen Temporal Logic

Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHT protocols to scale to millions of nodes. The correct operation of DHTs is therefore essential for the proper functioning of these systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. We propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation both to establish a number of DHT-derived properties and to generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.