This is a tool to convert reachability in concurrent Boolean programs within k context-switches (for any fixed k) to reachability in sequential programs.

See the following paper for the theory behind the conversion:

  • Reducing context-bounded concurrent reachability to sequential reachability
    Computer Aided Verification (CAV), 21st International Conference, Grenoble, France, 2009.

    • We have two conversions: an eager conversion which is simple, but guesses global valuations that may not be reachable, and a more involved lazy conversion that converts in such a way that all reachable states of the sequential program correspond to reachable states of the concurrent program.

    The Linux binaries for the two conversions are available:

  • The Eager Conversion
  • The Lazy Conversion
    • Here's a sample conversion of a small program modeling a Bluetooth device driver with 2 stoppers and two adders, and the corresponding sequential programs (for #context-switches=1,2,3,..6).

    Context
    switches    		 Eager Lazy
       4 processes: 2 adders and 2 stoppers (cbp file)
    1 bp file bp file
    2 bp file bp file
    3 bp file bp file
    4 bp file bp file
    5 bp file bp file
    6 bp file bp file


    Experimental results

    Here is a summary of experimental results on these Bluetooth examples (the resulting sequential programs were run on Moped).

    Context
    switches    		 Reach? Eager
    time(s)    		 Lazy
    time(s)
       
    2 processes: 1 adder and 1 stopper
    1 No 0.1 0.1
    2 No 0.3 0.2
    3 No 43.3 1.4
    4 No 73.6 5.5
    5 No 930.0 20.2
    6 No - 66.8
        
    3 processes: 2 adder and 1 stoppers
    1 No 0.2 0.1
    2 No 0.9 0.8
    3 No 135.9 6.3
    4 Yes 1601.0 2.6
    5 Yes - 18.0
    6 Yes - 122.9
        
    3 processes: 1 adders and 2 stopper
    1 No 0.1 0.1
    2 No 0.7 0.9
    3 Yes 70.1 0.4
    4 Yes 597.2 2.9
    5 Yes - 14.0
    6 Yes - 66.1
       
       4 processes: 2 adders and 2 stoppers
    1 No 0.2 0.1
    2 No 1.6 2.0
    3 Yes 177.6 0.8
    4 Yes Out of memory 7.5
    5 Yes Out of memory 66.5
    6 Yes Out of memory 535.9
    Legend:
    "-" denotes timeout in 30 minutes.