UCOB: Unbounded-thread COverability analysis for Boolean programs

This page describes the tool UCOB. It implements the techniques presented in our FMCAD paper [9].

1. Download

• Source code on github
• Binaries of UCOB for Linux, Mac OSX.

2. Installation

Install from source

1. UCOB depends the API IJIT. To run UCOB, you first need to install IJIT. Please refer to more details in the IJIT repository.
2. git clone the github repository
3. make

Using the binaries

1. Unpack the UCOB binary for your architecture, using the tarball above.
2. Make sure UCOB finds ijit library. Refer to more details in the here.

3. Benchmarks

Download

We distribute all benchmarks used in [9] here:

1. 01--10: thread-safe algorithms ([1-3]): code include atomic counters, concurrent pseudo-random number generator, maximum element finding algorithm, and stack data structure with concurrent operations.
2. 11--17: OS code ([4-5]): code from the FreeBSD, NetBSD, Solaris and Linux open-source operating system.
3. 18--22: pthread programs ([6]): several programs that use C Posix Threads library.
4. 23--28: mutex algorithms ([6-7]): code include test-and-set lock, multiple locks control access to a shared resource, and two ticket algorithms.
5. 29--30: misc ([8]): (29) requires single-thread predicates.

We use SATABS as the predicate abstraction engine to construct Boolean programs and thread-state transition system (TTS).
The following command is used to generate the Boolean programs:

 satabs -DSATABS --concurrency --full-inlining  --save-bps <input-file> 

To generate TTS, you can use above command with option --build-tts.

Input Format

The Boolean programs that UCOB takes use different labels (only numbers) from the Boolean programs generated by SATABS. Download the front end here to perform the translation. A sample program is:

	decl t := *;
	void main() begin
	decl m := 0;
	0: skip;
	1: goto 2, 3;
	2: start_thread goto 3; 
	3: t := 0;
	4: goto 5, 8;
	5: assume(t);
	6: m := 1;
	7: goto 9;
	8: assume(!t);
	9: t := !t;
	10: assert(!m);
	end

4. Bug reporting

Please send bug reports to us.

References