CUBA: Interprocedural Context-Unbounded Analysis of Concurrent Programs

1. Download

• Source code on github.
• Binaries of CUBA for
  

2. Installation

Install from source

1. git clone the github repository
2. make

Using the binaries

1. Unpack the CUBA binary for your architecture, using the tarball above.
2. Run it.

3. Usage

./cuba -f [--input-file] arg  -i [--initial] arg -s C -x -all 

./cuba -f [--input-file] arg  -i [--initial] arg -s C -all 

./cuba -h [--help]

More information:

• More information can be found on CUBA wiki
• An online tutorial

4. Benchmarks

Input Programs

The direct input to CUBA are concurrent pushdown systems, a model described in Section 3 of our paper. These systems are translated from concurrent (recursive) Boolean programs. We have a front-end to do the translation. Correspondingly, Boolean programs are obtained from concurrent C/C++ or Java programs by predicate abstraction.

Example

The following is one example of CUBA input: the Boolean program (left) and its translated pushdown system (right).

// shared variable
1 decl x;

// Thread 1 will run foo
 void foo() {
2    if (*)
3        foo();
4    while (x) {
     }
5    x = true;
 }

// Thread 2 will run foo
 void bar() {
6    if (*)
7        bar();
8    while (!x) {
     }
9    x = false;
 }

// the entry of programs
 void main() {
10    create_thread(&foo);
11    create_thread(&bar);
 }
	

2 # shared state 0..1
PDA 2 5 # a PDA converted from foo
0 2 -> 0 3 # an overwrite action
1 2 -> 1 3
0 2 -> 0 4
1 2 -> 1 4
0 3 -> 0 2 4 # a push action
1 3 -> 1 2 4
0 4 -> 0 5
1 4 -> 1 4
0 5 -> 1 6
1 5 -> 1 6
0 6 -> 1 - # a pop action, "-" = empty
1 6 -> 1 -
PDA 6 9 #  a PDA converted from bar
0 6 -> 0 7
1 6 -> 1 7
0 6 -> 0 8
1 6 -> 1 8
0 7 -> 0 6 8
1 7 -> 1 6 8
0 8 -> 0 8
1 8 -> 1 9
0 9 -> 0 10
1 9 -> 0 10
0 10 -> 0 -
1 10 -> 0 -

Syntax

The syntax of pushdown system is briefly summarized as follows (Please refer to the paper for more details):

• shared states: the number s in the first non-commented line. It represents the set of shared states [0...s-1].
• threads: separated by notation PDA.
• local states: defined by two numbers after PDA. Let l1, l2 be the numbers. Local states for this thread are [l1...l2].
• actions: there are three types. The pair (s1, l1) is the thread state before executing the action.
  • s1 l1 -> s2 l2: an overwrite action
  • s1 l1 -> s2 l2 l3: a push action
  • s1 l1 -> s2 - : a pop action: where notation "-" indicates an epsilon stack symbol

5. Technical Q & A

• Q: Why checking generators is easier?

A: The intuition is simply that we have more information about generators (namely, their static characterization) than about arbitrary states.

Second, we approximate the reachability of generators by approximating the set Z of reachable visible states. The set of reachable generators is a subset of Z. So the chance for Alg. 2 to converge deteriorates if "all Z are checked". The rule is: use the smallest set we can find that contains all reachable generators. Any larger test set is also sound, but less likely to converge.

• Q: How to specify safety property?

A: A safety property is an assertion in the (Boolean) program which then represented as a set of visible states in the pushdown system.

6. Bug reporting

Please send bug reports to us.