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

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

[1]. R. Allen and K. Kennedy. Optimizing Compilers for Modern Architectures. Morgan Kaufmann, 2002.

[2]. Amino. Concurrent Building Blocks. amino-cbbs.sourceforge.net.

[3]. B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes and D. Lea. Java Concurrency in Practice. Addison-Wesley, 2006.

[4]. FreeBSD/Linux Kernel Cross Reference. svn.freebsd.org.

[5]. A. Gupta, C. Popeea and A. Rybalchenko. Threader: A Constraint-Based Verifier for Multi-threaded Programs. CAV 2011.

[6]. A. Kaiser, D. Kroening, and T. Wahl. Efficient Coverability Analysis by Proof Minimization. CONCUR 2012.

[7]. J. Mellor-Crummey and M. Scott. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Trans. Comput. Syst., 1991.

[8]. A. Donaldson, A. Kaiser, D. Kroening, M. Tautschnig, and T. Wahl. Counterexample-guided Abstraction Refinement for Symmetric Concurrent Programs. Form. Method. Syst. Des., 2012.

[9]. P. Liu and T. Wahl. Infinite-State Backward Exploration of Boolean Broadcast Programs. FMCAD, 2014.