VeriFIT Repository of Test Cases for Concurrency Testing

Repository description

This repository contains test cases which our group VeriFIT uses in papers targeting concurrency testing in Java. Each test case contains all data needed for its compilation (i.e. source code, script demonstrating its build process in common environment) and short documentation describing the program.

Available test cases

The programs are provided as they are with no warranty. Please inform us by sending an email if you like them and use them in your work. We appreciate any comments or suggestions as well.

Name	Language	Size	Error type
Airlines	Java	0.3 kLOC, 8 classes	Atomicity violation
Animator	Java	1.5 kLOC, 31 classes	Data race, Atomicity violation
Bank	Java	0.1 kLOC, 2 classes	Data race, Atomicity violation
Cache4j	Java	1.7 kLOC, 66 classes	No known error
Crawler	Java	1.2 kLOC, 19 classes	Atomicity violation
Dining philosophers	Java	0.1 kLOC, 6 classes	Deadlock
Elevator	Java	1.2 kLOC, 12 classes	Data race, atomicity violation
FTPServer	Java	12.2 kLOC, 120 classes	Data race, atomicity violation
HEDC	Java	12.7 kLOC, 747 classes	No known error
Moldyn	Java	0.8 kLOC, 14 classes	No known error
Montecarlo	Java	1.4 kLOC, 22 classes	No known error
Raytracer	Java	1.0 kLOC, 22 classes	No known error
Rover	Java	5.4 kLOC, 82 classes	Atomicity violation, deadlock
Sor	Java	7.2 kLOC, 256 classes	No known error
Tsp	Java	0.4 kLOC, 8 classes	No known error
TIDOrbJ	Java	84.3 kLOC, 1399 classes	Atomicity violation

Links to similar repositories and/or benchmarks

If you know an interesting site with benchmarks and/or programs containing concurrency and are not yet listed here, please let us know. This page focus on software testing and therefore only benchmarks with this purpose are listed (i.e., e.g., SAT competition benchmark is not listed here).

ClabureDB: Database of big real-life projects with a list of uniformly described bug reports classified as real errors or false positives. The database contains 1150 bug-reports of 11 error types produced by several bug-detection tools run on the Linux 2.6.28 kernel. The database also contains bug reports for examples from Competition on Software Verification (listed bellow).
Software-artifact Infrastructure Repository: The repository contains many Java and C, C++, and C# software systems, in multiple versions, together with supporting artifacts such as test suites, fault data, and scripts. The repository also includes documentation on how to use these objects in experimentation, supporting tools that facilitate experimentation, and information on the processes used to select, organize, and enhance the artifacts, and supporting tools that help with these processes.
Qualitas Corpus: The Qualitas Corpus is a curated collection of software systems intended to be used for empirical studies of code artefacts. The primary goal is to provide a resource that supports reproducible studies of software. The current release of the Corpus contains open-source Java software systems, often multiple versions.
Database of Java programs curated by IBM HRL: Database of 40 small programs (most of them have less than 300 LoC) written in Java and containing well documented concurrency error such as atomicity violations, deadlocks, orphaned thread, etc. The database is not publicly available. Please contact Rachel Brill from IBM HRL to get access.
Competition on Software Verification (SV-COMP) benchmarks: A database of 7000 small programs of various size containing various classes of errors (including concurrency). The database also contain programs that are very hard to verify. 2868 of them are used for the competition, rest is maintained for demonstration purposes. Most of the programs are in C and preprocessed by CIL.
SF100 Benchmark: Randomly selected 100 Java projects from SourceForge. The benchmark is not only very large but more importantly it is statistically sound and representative for open source Java projects.
Dacapo Benchmark: A benchmark suite which is intended as a tool for Java benchmarking by the programming language, memory management and computer architecture communities. It consists of a set of open source, real world applications with non-trivial memory loads.
NECLA Verification Benchmarks: A set of 15 C/C++ programs with various C/C++ specific bugs including real programs and various bug pattern sources.
CPROVER Benchmarking Toolkit: A set of 8 C/C++ real programs (including Linux 2.6.19 kernel) and patches which makes them verifiable by model checking tool.
VerifyThis: VerifyThis is a collection of problems (and solutions) in formal verification of object-oriented software. The benchmark contains 43 problems and solutions.
Challenge Benchmarks for Verification of Real-time Programs: Set of 6 Java and C programs with real problems including 1 concurrency problem.

Acknowledgement

This work was supported by the Czech Ministry of Education (project Kontakt II LH13265) and the EU/Czech Interdisciplinary Excellence Research Teams Establishment project (CZ.1.07/2.3.00/30.0005).