Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 64 additions & 38 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,95 +3,90 @@
Dara is a hybrid model checker which verifies properties of distributed systems written in Golang. The Dara pipeline is implemented in three distinct git repositories.

+ [godist](https://github.com/DARA-Project/GoDist) : Contains a custom version of Go v1.10, which provides the necessary interposition to schedule Go threads and capture system calls.
+ [dara](https://github.com/DARA-Project/dara) : Contains the model inference, model refinement, the abstract model checker, and trace filtering pieces of Dara.
+ [dara](https://github.com/DARA-Project/dara) : Contains the stand alone model inference, model refinement, the abstract model checker, and trace filtering pieces of Dara.
+ [godist-scheduler](https://github.com/DARA-Project/GoDist-Scheduler) : Contains the concrete state explorer and the replay engine.

System-specific repositories (for systems we check with Dara):
+ [BTCD-applications](https://github.com/DARA-Project/BTCD-Applications) : Contains information for verifying [BTCD](https://github.com/btcsuite/btcd), a full node bitcoin implementation in Golang.
+ [Dara-ETCD](https://github.com/DARA-Project/Dara-Etcd) : Contains information for verifying [ETCD](https://github.com/etcd-io/etcd), a distributed key-value store that uses the Raft consensus algorithm.

## How to install
## Record/Replay Quickstart

### Prerequisites

- Go 1.4+
- GOPATH environment variable set. You can check by running `echo $GOPATH`.

### Installation

To be able to run Dara, you must have all the following things installed.
For doing Record/Replay, you only need to have godist and godist-scheduler installed.
It is suggested that you install them in the following order.

### Cloning Repos
#### Cloning Repos

Go packaging relies heavily on the GOPATH environment variable. We recommend that
all your repos should be located under the GOPATH root.
So, you should clone all repos as follows (this assumes that you have the GOPATH environment variable set) :

```
> cd $GOPATH/src/github.com
> mkdir DARA-Project
> cd DARA-Project
> git clone https://github.com/DARA-Project/GoDist.git
> git clone https://github.com/DARA-Project/dara.git
> git clone https://github.com/DARA-Project/GoDist-Scheduler.git
cd $GOPATH/src/github.com
mkdir DARA-Project
cd DARA-Project
git clone https://github.com/DARA-Project/GoDist.git
git clone https://github.com/DARA-Project/GoDist-Scheduler.git
```

### Installing GoDist
#### Installing GoDist

Installing GoDist (its binary name is dgo) requires that you have some version of Go (>=1.4) on your computer.

Below steps assume that you have Go 1.10 and its sources are installed on your machine at "/usr/lib/go-1.10".
To install GoDist, execute the following commands:

```
> cd $GOPATH/src/github.com/DARA-Project/GoDist/src
> export GOROOT_BOOTSTRAP="/usr/lib/go-1.10"
> ./make.bash
> sudo ln -s $GOPATH/src/github.com/DARA-Project/GoDist/bin/go /usr/bin/dgo
cd $GOPATH/src/github.com/DARA-Project/GoDist/src
export GOROOT_BOOTSTRAP="/usr/lib/go-1.10"
./make.bash
sudo ln -s $GOPATH/src/github.com/DARA-Project/GoDist/bin/go /usr/bin/dgo
```

You can check if the installation of dgo succeeded by executing the following command and comparing its output

```
> which dgo # Output should be /usr/bin/dgo
which dgo # Output should be /usr/bin/dgo
```

### Installing dara
#### Installing GoDist-Scheduler

Installing the Model Inference Unit (dara) requires you to have docker. Run the following commands for installation:
Currently this is not being USED.

```
> cd $GOPATH/src/github.com/DARA-Project/dara
> sudo docker build -t dara/1.0 -f ./docker/Dockerfile .
```

### Installing GoDist-Scheduler

#### Dependencies
##### Dependencies

Install the dependencies for global scheduler as follows:

```
> cd $GOPATH/src/github.com/DARA-Project/GoDist-Scheduler
> ./dependencies.sh
cd $GOPATH/src/github.com/DARA-Project/GoDist-Scheduler
./dependencies.sh
```

#### Installation
##### Installation

Once you have the above installed, you are ready to install the global scheduler:

```
> cd $GOPATH/src/github.com/DARA-Project/GoDist-Scheduler
> dgo install
cd $GOPATH/src/github.com/DARA-Project/GoDist-Scheduler
dgo install
```

## How to use
### How to use

### Record + Replay usage
##### Record + Replay usage

#### Environment setup
##### Environment setup

Recording and replaying requires shared memory for IPC and for the environment to be set up for communication between the global scheduler and the local Go runtimes. This is automated by a run.sh script in the GoDist-Scheduler repo: [example run.sh](https://github.com/DARA-Project/GoDist-Scheduler/blob/master/examples/SimpleFileRead/run.sh)

The same run.sh script is also used to record and replay exectuions.

#### Record
##### Record

To record the execution of a program, run the following command in the same directory as the run script and the program:

Expand All @@ -101,10 +96,41 @@ To record the execution of a program, run the following command in the same dire

The recorded execution schedule will be written to a file called ```Schedule.json```

#### Replay
##### Replay

To replay the execution of a program, run the following command in the same directory as the run script and the program,

```
> sudo -E ./run.sh -replay=true
```


## Installing dara

How to install the start alone model inference, model refinement, the abstract model checker, and trace filtering pieces of Dara. *Note:* This requires you to have access to the Dara repository.

### Prerequisites

- Go 1.4+
- GOPATH environment variable set. You can check by running `echo $GOPATH`.
- Docker

### Cloning

```
cd $GOPATH/src/github.com
mkdir DARA-Project
cd DARA-Project
git clone https://github.com/DARA-Project/dara.git

```

### Installing dara

Installing the Model Inference Unit (dara) requires you to have docker. Run the following commands for installation:
Currently this is not being USED.

```
> cd $GOPATH/src/github.com/DARA-Project/dara
> sudo docker build -t dara/1.0 -f ./docker/Dockerfile .
```