Input Syntax

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):

  • # 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 symbol PDA. 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 state
    • s1 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 -