Violat

Find test harnesses that expose atomicity violations.

This project demonstrates that many of the methods in Java’s library of concurrent collections are non-linearizable. For each non-linearizable method in the selected collection classes, a small test harness witnesses violations via stress testing with OpenJDK’s jcstress tool.

Requirements

This project depends essentially on recent Java and JavaScript environments, and in particular on:

• Node.js runtime for JavaScript: version 10.0 or greater
• Java SE Development Kit: version 8
• Gradle build tool: at least version 6
• Maven project management tool
• Java Pathfinder if the JPF-based tester is desired (in which JDK 8 is required)

Installation

Install the latest version from npm:

$ npm i -g violat

Or from a working copy of the Github repository:

$ cd /path/to/my/working/copy/of/violat && npm link

Usage

See usage instructions with:

$ violat-validator

Development

Link a local copy of the Github repository:

$ cd /path/to/my/working/copy/of/violat && npm link

Release a new version to npm:

$ npm version [major|minor|patch]
$ npm publish

Experiments

To reproduce the experiments reported in the CAV 2018 paper Monitoring Weak Consistency:

$ cd /path/to/my/working/copy/of/violat
$ git checkout cav-2018-submission
$ npm link
$ npm run monitoring-experiments

NOTE these experiments may require an older version of Node.js, e.g., version 8.12.0.

To reproduce the experiments reported in the POPL 2019 paper Weak-Consistency Specification via Visibility Relaxation:

$ cd /path/to/my/working/copy/of/violat
$ git checkout atomicity-submission-data
$ npm link
$ npm run experiments

NOTE these experiments may require an older version of Node.js, e.g., version 8.12.0.

Various Use Cases

Validate (weak) consistency of a given implementation

Validate a given implementation for consistency, according to the given consistency specification, against randomly-generated test programs:

$ violat-validator resources/specs/java/util/concurrent/ConcurrentHashMap.json

Generate histories admitted by a given implementation

Add to the set of histories generated in violat-output/histories with the violat-histories command:

$ violat-histories resources/specs/java/util/concurrent/ConcurrentHashMap.json

Check generated histories for (weak) consistency

Check the histories stored in violat-output/histories with the violat-history-checker command:

TODO FIXME

Visualize generated histories and data

Install and start a web server to visualize histories and history-checking results:

$ npm i -g http-server
$ http-server violat-output

Then point the web browser to one of the URLS output by the history checker:

http://localhost:8080/histories/**/*.html

Or point the web browser to the plot of data generated by the history checker:

http://localhost:8080/results/plot.html