No description, website, or topics provided.
Switch branches/tags
Nothing to show
Clone or download

README.md

DARA

Distributed Systems Hybrid Model Checker

Dara is a model checker to find property violations in distributed systems implemented in Go lang. Currently Dara only checks safety properties and only supports homogeneous systems (where each node executes the same code). Note that this project is an active work in progress.

More precisely, Dara is hybrid model checker. It combines the speed of abstract model checkers with the correctness and ease of use of concrete model checkers. Dara uses concrete model checking to extract an abstract model of the system. This model is then checked by an abstract model checker (SPIN) to verify a user-provided property. Property violations are replayed in the actual system to generate reproducible concrete counter-example system executions.

Installation

Docker

Dara is distributed as a docker container. To install Dara's docker distribution run the following command from Dara's root directory.

./build.sh

Native

Dara has dependencies on a number of analysis tools. Specifically Dara requires a working installation of

Supported versions of each tool can be found in Dara's Dockerfile.

Instrumentation

TODO MAKE THIS AUTOMATIC At the moment all instrumentation is done manually using Dinv instrumentation. See Dinv, Dinv documentation for full support. All sending and receiving lines of code must be instrumented, Dara requires that the state of each message be logged for analysis. Processes tracing is done using Dinv dump statements. Ideally this will be done automatically at the entrance and exit of every function.

Running

Dara is organized as a set of servers which perform analysis, and a client, which organizes calls to servers. Running a Dara container automatically launches a set of analysis servers. Servers automatically register with a centralized name server to pool their resources for all Dara clients.

Name Server

The current name server is run from the UBC NSS lab at IP 198.162.52.148 cerf.

Resetting the Name Server

In the case where cerf has been rebooted the nameserver must also be restarted. This has two steps 1) configure ip tables on cerf, 2) run darad.sh

configure ip tables

sudo ip addr add 198.162.52.148/24 dev eth1

Run darad.sh

In the root directory of this project run ./darad.sh