Artifact:

CUBA: Interprocedural Context-Unbounded Analysis of Concurrent Programs

Input Programs

The direct input to CUBA are concurrent pushdown systems (CPDS), a model described in Section 3 of our paper. (CPDS are translated from concurrent (recursive) Boolean programs. Boolean programs are in turn obtained from concurrent C/C++ or Java programs by predicate abstraction. We do not include resources for these translation steps in this artifact.)

1. Syntax of Boolean Programs

Syntax

2. Syntax of Concurrent Pushdown Systems (CPDS)

The syntax of CPDS is briefly summarized as follows (refer to Section 3 of the paper for more details):

3. Example

The following shows a Boolean program (left) and its translated pushdown system (right). (Recall that the input to CUBA is the pushdown system; we show the Boolean program for illustration purposes only.)

// shared variable
 decl x;

// Thread 1 will run foo
 void foo() {
    if (*)
      call foo();
    while (x) {
    }
    x := true;
 }

// Thread 2 will run bar
 void bar() {
    if (*)
      call bar();
    while (!x) {
    }
    x := false;
 }

// program entry point
 void main() {
    create_thread(&foo);
    create_thread(&bar);
 }


	
2 # shared state 0..1
# Thread 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 -
# Thread 2
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 -