Open Collections

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

University of British Columbia

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.

Text

2020-08-26

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/75692

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/