ALGORITHMIC METHODS FOR THE VERIFICATION OF CONSISTENCY IN DISTRIBUTED SYSTEMS

Abstract

Nowadays, we are all end users of distributed systems. A distributed system is a collection of computers in order to improve performance by sharing of resources. Indeed, with the internet's massive explosion, these systems have become necessary. Unfortunately, due to the parallelism and communication latency over large networks, distributed systems may produce unexpected (inconsistent) behaviors if they are not correctly designed and implemented. For instance, a flight seat can be assigned to two users of a flight booking system at the same time. This thesis addresses the problem of verifying that an implementation of a concurrent/distributed system provides to the clients the expected consistency guarantees (i.e., strong, weak or eventual consistency). In particular, we consider the problem of testing concurrent/distributed systems to determine if they are offering the consistency level expected by their users. For a given computation of a concurrent/distributed system, the test confirms the consistency or inconsistency of the system during that computation. We propose dynamic verification approaches with respect to some well-known consistency models, i.e., executing a large number of test programs and verifying them against a given consistency model. The main consistency criterion that we consider in this thesis is a fundamental model called sequential consistency. The verification problem of this model is known to be NP-hard. The reason is that in order to prove that a computation is conform to this consistency model, one need to find a total order on write operations that explains the execution. Therefore, one need to enumerate all the possible total orders, in the worst case. In the beginning, we are interested in verifying the conformance to consistency models that are checkable in polynomial time using saturation-based techniques. We consider causal consistency in its different variants. Then, we build on this work in order to propose an approach for verifying sequential consistency using a strong causal consistency variant. This approach is improved by proposing another weaker model based on more natural and simpler saturation rules. These approaches allow to avoid falling systematically in the worst case i.e., enumerating explicitly the exponential number of the possible total orders between the computation writes. These two approaches are generalized afterward to cover another consistency model that is a relaxation of the sequential consistency model called total store ordering. The problem of verifying this model is also known to be NP-hard. Indeed, the proposed generalizations use suitable models for approximating the total store ordering model. We implement all these approaches and perform benchmark on real life applications.