Distributed systems form the backbone of modern cloud systems. Failures indistributed systems can cause massive losses in the form of service outages and lossof revenue impacting real users of systems. Thus, it is imperative to find bugs indistributed systems before they are used in production systems.However, debugging distributed systems continues to elude us. Use of abstractmodelling languages such as TLA+, PlusCal, Coq, and SPIN that check the correct-ness of models of distributed systems have become popular in recent years but theyrequire a considerable amount of developer effort and do not necessarily find all thebugs in the implementation of the system. Model checkers that explore all possibleexecutions of the implementation of a distributed system suffer from state spaceexplosion, rendering them impractical as they are inefficiently scalable. To alleviatethis, we propose Dara, a model checker designed for Go systems that uses a novelcoverage-based strategy for ordering exploration of paths in the state space of thesystem according to the amount of code covered across nodes. Dara can find andreproduce concurrency bugs in go systems.

Read my M.Sc. thesis on Dara here.

Code implementation at