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](syntax.jpg)
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):
- # of shared states: the number given in the first (non-commented) line. Calling that number
s
, the set of shared states is{0,...,s-1}
. - thread programs: the program of a new thread is introduced by the terminal symbol
PDA
. - set of local states: defined by two numbers
l1,l2
after the symbolPDA
. The local states for the thread currently being defined are then{l1,...,l2}
. - actions: there are three types, classified by what they do to the stack of the thread, although each action also allows the modification of the shared state:
s1 l1 -> s2 l2
: overwrite the local states1 l1 -> s2 l2 l3
: push a new stack frame (also modifies of the current local state)s1 l1 -> s2 -
: pop a stack frame
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 -