Multi-Pushdown Systems with Budgets: Tool and Experimental Results

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine and Jari Stenman

Contents

1 The Tool
 1.1 Binaries
 1.2 Syntax of a Concurrent Program
 1.3 How To Use c2s
2 The experiments

1 The Tool

1.1 Binaries

c2s was implemented in Haskell. Here are binaries for Linux:

32-bit Linux distribution /x86:c2s-v0.1-linux-32.tar.gz
64-bit Linux distribution /x64 :c2s-v0.1-linux-64.tar.gz
c2s is in charge of transforming the code form a concurrent program to a sequential one such that verifying the sequential program is equivalent to verifying the concurrent one up to the context switch budget k. Now, in order to verify the generated sequential program you need to install a backend tool such as: Moped [1], Cbmc [2] or Esbmc [3].

1.2 Syntax of a Concurrent Program

The building blocks of concurrent programs are processes, procedures and statements. The grammar of statements is given in Figure 1. They consist of simple C-like statements, enriched with nop , assume , assert and atomic . We assume that assignments are atomic. For simplicity, the grammar rules out nested function calls, e.g. a = f(g(h(b)));.

⟨statement ⟩ ::= skip ; | ⟨identifier⟩ = ⟨value⟩ ; | assume ( ⟨expression⟩ ) ; | assert ( ⟨expression ⟩ ) ; | call ⟨identifier⟩ ( ⟨expression⟩* ) ; | return ; | if ( ⟨expression ⟩ ) { ⟨statement⟩+ } else { ⟨statement⟩+ } | while ( ⟨expression⟩ ) { ⟨statement ⟩+ } | atomic { ⟨statement⟩+ }

Figure 1: Statements Syntax

A procedure consists of a sequence of arguments, a set of local variables, and a sequence of statements. A process is composed of a finite set of global variables and a finite sequence of procedures. For each process, the first procedure in the sequence constitutes the entry point. Our code-to-code transformation deals only with boolean and integer types of variables. Variables of both types can be set to non-deterministic values using the following syntax:

1/* For Booleans. */ 
2bool b; 
3b = ?; 
4/* For integers. */ 
5int x; 
6x = ??;

Figure 2: Variables assigned to non-deterministic values.

In Figure 3 we show the Dekker mutual exclusion algorithm written in our language.

1bool x = false; 
2bool y = false; 
3int z = 0; 
4 
5program p1: 
6void main(){ 
7  x = true; 
8  if(!y) 
9  { 
10    /* Enter Critical Section */ 
11    z = z + 1; 
12    nop; 
13    assert( z == 1); 
14    /* Leave Critical Section */ 
15    atomic {x = false; z = z - 1;} 
16  } 
17} 
18 
19program p2: 
20void main(){ 
21  y = true; 
22  if(!x) 
23  { 
24    /* Enter Critical Section */ 
25    z = z + 1; 
26    nop; 
27    assert(z == 1); 
28    /* Leave Critical Section */ 
29    atomic {y = false; z = z - 1;} 
30  } 
31}

Figure 3: Dekker implemented in our language. The variable z is used as an instrumentation variable to check the mutual exclusion property.

1.3 How To Use c2s

Our tool should be used as a command line:

./c2s --src=filename1 --dest=fileneame2 --syntax=OutSyntax -k kval [-n nval]

Where:

filename1
The input filename wich should contain the concurrent program specification written in the syntax defined in the previous section 1.2.
filename2
The output filename.
OutSyntax
The syntax of the ouput file. It can be:
  1. REMOPLA syntax used by Moped.
  2. CPROVER syntax used by Cbmc and Esbmc.
kval
The context switch budget.
nval
The integer bit size used by Moped. This option is Moped-specific, since the bit size has to be specified in the REMOPLA program. For ESBMC and CBMC, the size (either 16, 32 or 64 bits) is given as an argument when running the tool. We used the smallest size (16 bits) for these tools.

Example for Cbmc:
To transform dekker.code to a sequential program that can be checked by Cbmc, with 0 as a context switch budget, you can do:

./c2s --src=dekker.code --dest=dekker.c --syntax=CPROVER -k 0

To verify the generated code, you can invoke Cbmc using:

./cbmc dekker.c --unwind 14 --16

The --unwind n Cbmc option unwinds loops n times in the program being verified. The --16 defines integer size in bits.

Example for Esbmc:
To transform dekker.code to a sequential program that can be checked by Esbmc, with 0 as a context switch budget, you can do:

./c2s --src=dekker.code --dest=dekker.c --syntax=CPROVER -k 0

To verify the generated code, you can invoke Esbmc using:

./esbmc dekker.c --unwind 14

The --unwind n Esbmc option unwinds loops n times in the program being verified.

Example for Moped:
If you want to transform dekker.code to be checked by Moped, with 0 as a context switch budget, you can do:

./c2s --src=dekker.code --dest=dekker.rem --syntax=REMOPLA -k 0 -n 2

The integer size here is 2 since in Dekker integer variables do not go above 1, so 22 - 1 = 3 is acceptable as an upper bound. To verify the generated code, you can invoke Moped using:

./moped dekker.rem error

2 The experiments

The experiments were ran on a 2.2 GHz Intel Core i7 with 4 GB of memory using Moped 2.0, CBMC 4.0, ESBMC 1.18 and Poirot 1.0 [4]. All the files (including some scipts for translating and running the tools) can be downloaded here. The operating systems used were Ubuntu (32-bit) and Windows 7 (32-bit).

Type of Analysis
Concurrent to Sequential
Concurrent
Examples
k 1
Moped
Cbmc
Esbmc
k2
Poirot
k3
Esbmc
Account 0 -. - -. - 1. 1 4 3. 34 10 -. -
BigNum 0 8.39 -.- -.- 26 -.- 234 -.-
Bluetooth3a 0 744.49 -.- -.- 1118.38 28
FP
Token Ring 0 0. 13 0. 2 0. 18 1 2. 72 4 1. 47
Account Bad 0 -.- 0.48 1.41 1 2.13 4 0.11
BigNum Bad 0 5. 9 13. 4 239. 4 26 -. - 26 -. -
Bluetooth1 1 4.18 0.37 1.28 2 1.92 5
NF
Bluetooth2 1 0. 64 5. 68 34. 38 3 2. 9 5 0. 5
Bluetooth3b 1 1.26 0.95 5.0 2 2.5 5
NF
Infinite Loop 1 1 4. 1 0. 2 0. 25 2 1. 45 1 0. 08
Infinite Loop 2 1 17.3 0.84 3.85 1 0.96 1 0.09
Token Ring Bad 0 0.13 0.16 0.26 2 2.74 4 0.27

Figure 4: We report the running times of our experimentation results in seconds. We use the symbol -.- to denote a timeout (set to 900 seconds). The column k1 contains the context-switch budget for our code-to-code translation. The columns k2 and k3 are the number of context switches given as input for Poirot and Esbmc respectively. NF: Bug Not Found. FP: False Positive.

Note: In the paper, we reported that Moped times out for both Account examples. This is true when we use 8 bit integers. If we use 4 bit integers, both Account and Account Bad terminate, in 37.35 resp. 2.31 seconds.

References

[1]   Moped home page: http://www.fmi.uni-stuttgart.de/szs/tools/moped/.

[2]   Cbmc home page: http://www.cprover.org/cbmc/.

[3]   Esbmc home page: http://esbmc.org/.

[4]   Poirot home page: http://research.microsoft.com/en-us/projects/poirot.