UCOB: Unbounded-thread COverability analysis for Boolean programsThis page describes the tool UCOB. It implements the techniques presented in our FMCAD paper .
Install from source
- UCOB depends the API IJIT. To run UCOB, you first need to install IJIT. Please refer to more details in the IJIT repository.
- git clone the github repository
Using the binaries
- Unpack the UCOB binary for your architecture, using the tarball above.
- Make sure UCOB finds ijit library. Refer to more details in the here.
We distribute all benchmarks used in  here:
- 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.
- 11--17: OS code ([4-5]): code from the FreeBSD, NetBSD, Solaris and Linux open-source operating system.
- 18--22: pthread programs (): several programs that use C Posix Threads library.
- 23--28: mutex algorithms ([6-7]): code include test-and-set lock, multiple locks control access to a shared resource, and two ticket algorithms.
- 29--30: misc (): (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:
To generate TTS, you can use above command with option
satabs -DSATABS --concurrency --full-inlining --save-bps <input-file>
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.
. R. Allen and K. Kennedy. Optimizing Compilers for Modern Architectures. Morgan Kaufmann, 2002.
. Amino. Concurrent Building Blocks. amino-cbbs.sourceforge.net.
. B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes and D. Lea. Java Concurrency in Practice. Addison-Wesley, 2006.
. FreeBSD/Linux Kernel Cross Reference. svn.freebsd.org.
. A. Gupta, C. Popeea and A. Rybalchenko. Threader: A Constraint-Based Verifier for Multi-threaded Programs. CAV 2011.
. A. Kaiser, D. Kroening, and T. Wahl. Efficient Coverability Analysis by Proof Minimization. CONCUR 2012.
. J. Mellor-Crummey and M. Scott. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Trans. Comput. Syst., 1991.
. A. Donaldson, A. Kaiser, D. Kroening, M. Tautschnig, and T. Wahl. Counterexample-guided Abstraction Refinement for Symmetric Concurrent Programs. Form. Method. Syst. Des., 2012.
. P. Liu and T. Wahl. Infinite-State Backward Exploration of Boolean Broadcast Programs. FMCAD, 2014.