automatic data race analysis for Linux device drivers
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
BoogieBinaries
Model
Scripts
Source
driversuite
testsuite
.gitignore
LICENSE.TXT
README.md
Vagrantfile
findtools.py
tester.py
whoop.py
whoop.sln

README.md

Whoop

Whoop is a SMACK-based symbolic data race analyzer for Linux device drivers.

Prerequisites

  1. LLVM 3.5
  2. SMACK 1.5
  3. Z3 4.3.2
  4. Corral
  5. Chauffeur

Build instructions

  1. Clone this project.
  2. Compile using Visual Studio or Mono.

We also have vagrant support for building a virtual machine with the toolchain installed. To do this use the following from the project's root directory:

vagrant up

How to use

The input to Whoop is a Linux driver. To use Whoop do the following:

.\whoop.py ${DRIVER}.c

To use Corral for precise bug-finding do the following:

.\whoop.py ${DRIVER}.c --find-bugs --yield-race-check

Tool options

Use --verbose for verbose mode. Use --time for timing information.

Publications