UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Dara the explorer : coverage based exploration for model checking of distributed systems in Go Anand, Vaastav


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

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International