Screenshots of Working with Boom
This document demonstrates some features of Boom. Boom offers several algorithms to analyze Boolean programs. In the following sections we illustrate (always using the same Boolean program) some of algorithms and options.
Verifying a concurrent Boolean program using the standard symbolic algorithm
Boolean programs create new threads dynamically using the start_thread instruction. However, in order to measure the performance of different algorithms, it is more convenient so replicate the whole program several times, which can be done with the --parallel option. Let's simulate 4 threads with the standard symbolic algorithm:During the run, the number of reached global states and thread states is printed. Since the states are not hold in a single BDD but rather state objects, the frontier set is stored as a list of objects. Its size is indicated with "frontier size". The size of the biggest BDD is denoted with "peakNodeCount".
When Boom terminates, the collected statistics of the model checking run are printed. Many entries are 0 because they do not matter with this algorithm. (The "QBF cache"-numbers originate from the usage of a QBF solver to simplify expressions). The interesting part is the number of lines (without blank lines), global and local variables:
==========================================[ Problem Statistics ]==========================================
| Distinct state objects found..........................: 0 |
| Constructed states....................................: 0 |
| Invisible transitions.................................: 0 |
| Visible transitions...................................: 0 |
| Persistent sets.......................................: 0 |
| States discarded using homomorph comparison...........: 0 |
| Transformed assertions into guarded gotos.............: 0 |
| Partially transformed assertions into guarded gotos...: 0 |
| Paths tested for fixpoint.............................: 0 |
| Paths cutted by fixpoint detection....................: 0 |
| Paths cutted by nondeterministic formula comparison...: 0 |
| Subsumed states excluded from fixpoint computation....: 0 |
| Paths cutted that don't lead to assertions............: 0 |
| Paths found...........................................: 0 |
| States merged.........................................: 0 |
| Failed merging attempts...............................: 0 |
| Max. stack depth......................................: 0 |
| Max. recursion depth..................................: 0 |
| Path splits...........................................: 0 |
| Global variables......................................: 17 |
| Max. local variables..................................: 24 |
| Max. visible variables................................: 41 |
| Locations.............................................: 1256 |
| Universal SAT summaries built.........................: 0 |
| Universal SAT summaries used..........................: 0 |
| Call graph depth of universal summaries...............: 0 |
| Size of biggest universal summary.....................: 0 |
| Failed attempts to build universal SAT summaries......: 0 |
| Path summaries built..................................: 0 |
| Path summaries used...................................: 0 |
| Nondet universal summaries used.......................: 0 |
| Universal summaries needed to refine traces...........: |
| QBF restarts for traces containing nondet summaries...: 0 |
| Spurious traces found.................................: 0 |
| SAT QBF instances.....................................: 0 |
| UNSAT QBF instances...................................: 0 |
| QBF cache hit.........................................: 176 |
| QBF cache miss........................................: 12 |
| QBF cache updates.....................................: 0 |
| QBF cache updates used................................: 0 |
| Diameter..............................................: 132 |
| Depth of thread-local fixpoint........................: 41 |
| Model type............................................: stabilized |
| Stable intervals......................................: |
| Conceivable global states.............................: 14408499177694135550378697838734857776136192 |
| Explicit global states................................: 112189628633205961230014045042625216512 |
| Conceivable thread states.............................: 424411488321536 |
| Explicit thread states................................: 16003048144896 |
| Unbounded model checking thread states................: 16003048144896 |
| Subsumed states.......................................: 0 |
| Free slot cache hit...................................: 0 |
| Split expansions performed one pro variable...........: 0 |
| Split expansions avoided..............................: 0 |
| Dynamic constraint generating statements..............: 0 |
| Dynamic non constraint generating statements..........: 0 |
| Static constraint generating statements...............: 0 |
| Static non constraint generating statements...........: 191 |
| Total number of split variables.......................: 0 |
| Independent stmts with same PC........................: 0 |
| Independent stmts with other PC.......................: 0 |
| Average of number of slots used.......................: 0 |
| Median of number of slots used........................: 0 |
| Max number of slots used..............................: 0 |
==========================================================================================================
|
29 minutes, that was a quite long! The next section shows how to the runtime can be reduced using a counter abstraction (a variant ofsymmetry reduction).
Verifying a concurrent Boolean program using symbolic counter abstraction
Plain symbolic reachability analysis on a replicated Boolean program does not make use of its inherent symmetry. Boom can apply counter-abstraction to such programs to factor out redundancy due to thread replication, which improves performance significantly.
geri@clfh6701:~/workspace/boom$ time build_release/boom --algo=splitglobalscmc benchmarks/cav_2009/mixcomwd/111/claim_003.bp --parallel=4 Parsing <benchmarks/cav_2009/mixcomwd/111/claim_003.bp> done. Semantic check... ok. Transforming program for model-checker... done. Configuration: Eliminate dead variables: yes (will be computed anyway) Optimizing program... Life variable analysis... Phase 1... done. Phase 2... done. Computing mod-ref-sets... done. Computing read-write-sets... done. Building bdd-program... Ordering BDD variables for concatenated layout... Creating hybrid transition relations...warning: assumption is always false! done. Starting counter abstraction symbolic simulation using BDDs... (Abstract transitions are constructed on-the-fly). Using static thread creation with 4 threads. Step 0: reached states = 0, new states = 0, reached thread states = 2199023255552, new thread states = 2199023255552, peakNodeCount = 21462, reached size = 1, frontier size = 1, elapsed time: 00:00:00.000183 Step 1: reached states = 0, new states = 0, reached thread states = 2748779069440, new thread states = 549755813888, peakNodeCount = 21462, reached size = 2, frontier size = 1, elapsed time: 00:00:00.000375 Step 2: reached states = 0, new states = 0, reached thread states = 4947802324992, new thread states = 2199023255552, peakNodeCount = 21462, reached size = 4, frontier size = 2, elapsed time: 00:00:00.000447 Step 3: reached states = 0, new states = 0, reached thread states = 6047313952768, new thread states = 1099511627776, peakNodeCount = 21462, reached size = 7, frontier size = 3, elapsed time: 00:00:00.000551 Step 4: reached states = 0, new states = 0, reached thread states = 7146825580544, new thread states = 1099511627776, peakNodeCount = 21462, reached size = 12, frontier size = 5, elapsed time: 00:00:00.000697 Step 5: reached states = 0, new states = 0, reached thread states = 7971459301376, new thread states = 824633720832, peakNodeCount = 22484, reached size = 18, frontier size = 6, elapsed time: 00:00:00.000939 Step 6: reached states = 0, new states = 0, reached thread states = 8521215115264, new thread states = 549755813888, peakNodeCount = 22484, reached size = 27, frontier size = 9, elapsed time: 00:00:00.001228 Step 7: reached states = 0, new states = 0, reached thread states = 9070970929152, new thread states = 549755813888, peakNodeCount = 22484, reached size = 38, frontier size = 11, elapsed time: 00:00:00.001616 Step 8: reached states = 0, new states = 0, reached thread states = 9345848836096, new thread states = 274877906944, peakNodeCount = 22484, reached size = 53, frontier size = 15, elapsed time: 00:00:00.002171 Step 9: reached states = 0, new states = 0, reached thread states = 9380208574464, new thread states = 34359738368, peakNodeCount = 22484, reached size = 71, frontier size = 18, elapsed time: 00:00:00.002845 Step 10: reached states = 0, new states = 0, reached thread states = 9397388443648, new thread states = 17179869184, peakNodeCount = 22484, reached size = 94, frontier size = 23, elapsed time: 00:00:00.003718 Step 11: reached states = 0, new states = 0, reached thread states = 9414568312832, new thread states = 17179869184, peakNodeCount = 22484, reached size = 121, frontier size = 27, elapsed time: 00:00:00.004772 ... Step 124: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124237, frontier size = 16, elapsed time: 00:00:27.943881 Step 125: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124246, frontier size = 11, elapsed time: 00:00:28.258760 Step 126: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124254, frontier size = 9, elapsed time: 00:00:28.569917 Step 127: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124259, frontier size = 6, elapsed time: 00:00:28.880632 Step 128: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124264, frontier size = 5, elapsed time: 00:00:29.199199 Step 129: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124267, frontier size = 3, elapsed time: 00:00:29.515011 Step 130: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124269, frontier size = 2, elapsed time: 00:00:29.954670 Step 131: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124270, frontier size = 1, elapsed time: 00:00:30.416061 Step 132: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124271, frontier size = 1, elapsed time: 00:00:30.726936 Step 133: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 124271, frontier size = 0, elapsed time: 00:00:31.041539 Model diameter = 133, reached global states = 0 Elapsed time: 00:00:31.041610 VERIFICATION SUCCESSFUL ===========================[ Problem Statistics ]=========================== | Distinct state objects found..........................: 345838 | | Constructed states....................................: 0 | | Invisible transitions.................................: 0 | | Visible transitions...................................: 0 | | Persistent sets.......................................: 0 | | States discarded using homomorph comparison...........: 0 | | Transformed assertions into guarded gotos.............: 0 | | Partially transformed assertions into guarded gotos...: 0 | | Paths tested for fixpoint.............................: 0 | | Paths cutted by fixpoint detection....................: 0 | | Paths cutted by nondeterministic formula comparison...: 0 | | Subsumed states excluded from fixpoint computation....: 0 | | Paths cutted that don't lead to assertions............: 0 | | Paths found...........................................: 0 | | States merged.........................................: 5086 | | Failed merging attempts...............................: 340752 | | Max. stack depth......................................: 0 | | Max. recursion depth..................................: 0 | | Path splits...........................................: 0 | | Global variables......................................: 17 | | Max. local variables..................................: 24 | | Max. visible variables................................: 41 | | Locations.............................................: 1256 | | Functions.............................................: 1 | | Recursive functions...................................: 0 | | Universal SAT summaries built.........................: 0 | | Universal SAT summaries used..........................: 0 | | Call graph depth of universal summaries...............: 0 | | Size of biggest universal summary.....................: 0 | | Failed attempts to build universal SAT summaries......: 0 | | Path summaries built..................................: 0 | | Path summaries used...................................: 0 | | Nondet universal summaries used.......................: 0 | | Universal summaries needed to refine traces...........: | | QBF restarts for traces containing nondet summaries...: 0 | | Spurious traces found.................................: 0 | | SAT QBF instances.....................................: 0 | | UNSAT QBF instances...................................: 0 | | QBF cache hit.........................................: 176 | | QBF cache miss........................................: 12 | | QBF cache updates.....................................: 0 | | QBF cache updates used................................: 0 | | Diameter..............................................: 132 | | Depth of thread-local fixpoint........................: 0 | | Model type............................................: | | Stable intervals......................................: | | Conceivable global states.............................: 0 | | Explicit global states................................: 0 | | Conceivable thread states.............................: 0 | | Explicit thread states................................: 16003048144896 | | Unbounded model checking thread states................: 0 | | Subsumed states.......................................: 431934 | | Free slot cache hit...................................: 0 | | Split expansions performed one pro variable...........: 0 | | Split expansions avoided..............................: 26460 | | Dynamic constraint generating statements..............: 26460 | | Dynamic non constraint generating statements..........: 624410 | | Static constraint generating statements...............: 1 | | Static non constraint generating statements...........: 190 | | Total number of split variables.......................: 1 | | Independent stmts with same PC........................: 0 | | Independent stmts with other PC.......................: 0 | | Average of number of slots used.......................: 3 | | Median of number of slots used........................: 4 | | Max number of slots used..............................: 4 | ============================================================================ real 0m31.789s user 0m29.058s sys 0m0.292s geri@clfh6701:~/workspace/boom$ |
That took 31 seconds instead of 29 minutes! The highlighted part denotes some statistics about the "split-expansion" that needs to be applied whenever a constraint between global and local variables is introduced via a statement. Note that in this example there was only 1 such statement, but the split expansion could be avoided in all 26460 occurences because the global variables had constant values.
Enabling Partial-Order Reduction
Boom features several flavors of partial-order reduction, which can be selected using the "--por" option. The following example demonstrates ample sets:
geri@clfh6701:~/workspace/boom$ time build_release/boom --algo=splitglobalscmc benchmarks/cav_2009/mixcomwd/111/claim_003.bp --parallel=4 --por=ample Parsing <benchmarks/cav_2009/mixcomwd/111/claim_003.bp> done. Semantic check... ok. Transforming program for model-checker... done. Configuration: Eliminate dead variables: yes (will be computed anyway) Optimizing program... Life variable analysis... Phase 1... done. Phase 2... done. Computing mod-ref-sets... done. Computing read-write-sets... done. Building bdd-program... Ordering BDD variables for concatenated layout... Creating hybrid transition relations...warning: assumption is always false! done. Starting counter abstraction symbolic simulation using BDDs... (Abstract transitions are constructed on-the-fly). Using static thread creation with 4 threads. Step 0: reached states = 0, new states = 0, reached thread states = 2199023255552, new thread states = 2199023255552, peakNodeCount = 21462, reached size = 1, frontier size = 1, elapsed time: 00:00:00.000343 Step 1: reached states = 0, new states = 0, reached thread states = 2748779069440, new thread states = 549755813888, peakNodeCount = 21462, reached size = 2, frontier size = 1, elapsed time: 00:00:00.000576 Step 2: reached states = 0, new states = 0, reached thread states = 4947802324992, new thread states = 2199023255552, peakNodeCount = 21462, reached size = 4, frontier size = 2, elapsed time: 00:00:00.000710 Step 3: reached states = 0, new states = 0, reached thread states = 6047313952768, new thread states = 1099511627776, peakNodeCount = 21462, reached size = 7, frontier size = 3, elapsed time: 00:00:00.000874 Step 4: reached states = 0, new states = 0, reached thread states = 7146825580544, new thread states = 1099511627776, peakNodeCount = 21462, reached size = 12, frontier size = 5, elapsed time: 00:00:00.001079 Step 5: reached states = 0, new states = 0, reached thread states = 7971459301376, new thread states = 824633720832, peakNodeCount = 22484, reached size = 18, frontier size = 6, elapsed time: 00:00:00.003982 Step 6: reached states = 0, new states = 0, reached thread states = 8521215115264, new thread states = 549755813888, peakNodeCount = 22484, reached size = 27, frontier size = 9, elapsed time: 00:00:00.004395 Step 7: reached states = 0, new states = 0, reached thread states = 9070970929152, new thread states = 549755813888, peakNodeCount = 22484, reached size = 38, frontier size = 11, elapsed time: 00:00:00.004847 ... Step 123: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101045, frontier size = 7, elapsed time: 00:00:20.345167 Step 124: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101049, frontier size = 5, elapsed time: 00:00:20.590417 Step 125: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101051, frontier size = 3, elapsed time: 00:00:20.831102 Step 126: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101052, frontier size = 2, elapsed time: 00:00:21.087648 Step 127: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101052, frontier size = 1, elapsed time: 00:00:21.330130 Step 128: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101053, frontier size = 1, elapsed time: 00:00:21.575776 Step 129: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101054, frontier size = 1, elapsed time: 00:00:21.813644 Step 130: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101055, frontier size = 1, elapsed time: 00:00:22.046830 Step 131: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101056, frontier size = 1, elapsed time: 00:00:22.284878 Step 132: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101057, frontier size = 1, elapsed time: 00:00:22.533693 Step 133: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 101057, frontier size = 0, elapsed time: 00:00:22.783074 Model diameter = 133, reached global states = 0 Elapsed time: 00:00:22.783146 VERIFICATION SUCCESSFUL ===========================[ Problem Statistics ]=========================== | Distinct state objects found..........................: 262966 | | Constructed states....................................: 0 | | Invisible transitions.................................: 52754 | | Visible transitions...................................: 0 | | Persistent sets.......................................: 0 | | States discarded using homomorph comparison...........: 0 | | Transformed assertions into guarded gotos.............: 0 | | Partially transformed assertions into guarded gotos...: 0 | | Paths tested for fixpoint.............................: 0 | | Paths cutted by fixpoint detection....................: 0 | | Paths cutted by nondeterministic formula comparison...: 0 | | Subsumed states excluded from fixpoint computation....: 0 | | Paths cutted that don't lead to assertions............: 0 | | Paths found...........................................: 0 | | States merged.........................................: 3418 | | Failed merging attempts...............................: 259548 | | Max. stack depth......................................: 0 | | Max. recursion depth..................................: 0 | | Path splits...........................................: 0 | | Global variables......................................: 17 | | Max. local variables..................................: 24 | | Max. visible variables................................: 41 | | Locations.............................................: 1256 | | Functions.............................................: 1 | | Recursive functions...................................: 0 | | Universal SAT summaries built.........................: 0 | | Universal SAT summaries used..........................: 0 | | Call graph depth of universal summaries...............: 0 | | Size of biggest universal summary.....................: 0 | | Failed attempts to build universal SAT summaries......: 0 | | Path summaries built..................................: 0 | | Path summaries used...................................: 0 | | Nondet universal summaries used.......................: 0 | | Universal summaries needed to refine traces...........: | | QBF restarts for traces containing nondet summaries...: 0 | | Spurious traces found.................................: 0 | | SAT QBF instances.....................................: 0 | | UNSAT QBF instances...................................: 0 | | QBF cache hit.........................................: 176 | | QBF cache miss........................................: 12 | | QBF cache updates.....................................: 0 | | QBF cache updates used................................: 0 | | Diameter..............................................: 132 | | Depth of thread-local fixpoint........................: 0 | | Model type............................................: | | Stable intervals......................................: | | Conceivable global states.............................: 0 | | Explicit global states................................: 0 | | Conceivable thread states.............................: 0 | | Explicit thread states................................: 16003048144896 | | Unbounded model checking thread states................: 0 | | Subsumed states.......................................: 195164 | | Free slot cache hit...................................: 0 | | Split expansions performed one pro variable...........: 0 | | Split expansions avoided..............................: 14704 | | Dynamic constraint generating statements..............: 14704 | | Dynamic non constraint generating statements..........: 333432 | | Static constraint generating statements...............: 1 | | Static non constraint generating statements...........: 190 | | Total number of split variables.......................: 1 | | Independent stmts with same PC........................: 0 | | Independent stmts with other PC.......................: 0 | | Average of number of slots used.......................: 3 | | Median of number of slots used........................: 4 | | Max number of slots used..............................: 4 | ============================================================================ real 0m23.406s user 0m21.105s sys 0m0.140s geri@clfh6701:~/workspace/boom$ |
Using partial-order reduction, the runtime has improved from 31 seconds to 23!
Simulating an unbounded number of threads
Boom supports an unbounded number of threads using the Karp-Miller coverability tree construction that is implemented on top of the counter abstraction algorithm.
geri@clfh6701:~/workspace/boom$ time build_release/boom --algo=splitglobalscmc benchmarks/cav_2009/mixcomwd/111/claim_003.bp --parallel=0 Parsing <benchmarks/cav_2009/mixcomwd/111/claim_003.bp> done. Semantic check... ok. Transforming program for model-checker... done. Configuration: Eliminate dead variables: yes (will be computed anyway) Optimizing program... Life variable analysis... Phase 1... done. Phase 2... done. Computing mod-ref-sets... done. Computing read-write-sets... done. Building bdd-program... Ordering BDD variables for concatenated layout... Creating hybrid transition relations...warning: assumption is always false! done. Starting counter abstraction symbolic simulation using BDDs... (Abstract transitions are constructed on-the-fly). Using Karp-Miller with dynamic thread creation with infinitely many initial threads. Step 0: reached states = 0, new states = 0, reached thread states = 2199023255552, new thread states = 2199023255552, peakNodeCount = 21462, reached size = 1, frontier size = 1, elapsed time: 00:00:00.000287 Step 1: reached states = 0, new states = 0, reached thread states = 2748779069440, new thread states = 549755813888, peakNodeCount = 21462, reached size = 2, frontier size = 1 (trashing: 0%), elapsed time: 00:00:00.000553 Step 2: reached states = 0, new states = 0, reached thread states = 4947802324992, new thread states = 2199023255552, peakNodeCount = 21462, reached size = 2, frontier size = 2 (trashing: 33%), elapsed time: 00:00:00.000704 Step 3: reached states = 0, new states = 0, reached thread states = 6047313952768, new thread states = 1099511627776, peakNodeCount = 21462, reached size = 3, frontier size = 2 (trashing: 33%), elapsed time: 00:00:00.000851 Step 4: reached states = 0, new states = 0, reached thread states = 7146825580544, new thread states = 1099511627776, peakNodeCount = 21462, reached size = 5, frontier size = 3 (trashing: 17%), elapsed time: 00:00:00.001042 Step 5: reached states = 0, new states = 0, reached thread states = 7971459301376, new thread states = 824633720832, peakNodeCount = 22484, reached size = 7, frontier size = 3 (trashing: 11%), elapsed time: 00:00:00.001333 Step 6: reached states = 0, new states = 0, reached thread states = 8521215115264, new thread states = 549755813888, peakNodeCount = 22484, reached size = 9, frontier size = 4 (trashing: 7.1%), elapsed time: 00:00:00.001840 Step 7: reached states = 0, new states = 0, reached thread states = 9070970929152, new thread states = 549755813888, peakNodeCount = 22484, reached size = 10, frontier size = 4 (trashing: 11%), elapsed time: 00:00:00.002296 ... Step 76: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 51, frontier size = 17 (trashing: 7.8%), elapsed time: 00:00:07.922843 Step 77: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 48, frontier size = 14 (trashing: 6.7%), elapsed time: 00:00:07.986182 Step 78: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 40, frontier size = 6 (trashing: 5.8%), elapsed time: 00:00:08.029797 Step 79: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 39, frontier size = 5 (trashing: 4.2%), elapsed time: 00:00:08.059757 Step 80: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 35, frontier size = 1 (trashing: 3.1%), elapsed time: 00:00:08.077117 Step 81: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 35, frontier size = 1 (trashing: 1.4%), elapsed time: 00:00:08.087384 Step 82: reached states = 0, new states = 0, reached thread states = 16003048144896, new thread states = 0, peakNodeCount = 23506, reached size = 35, frontier size = 0 (trashing: 0%), elapsed time: 00:00:08.092327 Model diameter = 82, reached global states = 0 Elapsed time: 00:00:08.092369 VERIFICATION SUCCESSFUL ===========================[ Problem Statistics ]=========================== | Distinct state objects found..........................: 13116 | | Constructed states....................................: 0 | | Invisible transitions.................................: 0 | | Visible transitions...................................: 0 | | Persistent sets.......................................: 0 | | States discarded using homomorph comparison...........: 0 | | Transformed assertions into guarded gotos.............: 0 | | Partially transformed assertions into guarded gotos...: 0 | | Paths tested for fixpoint.............................: 0 | | Paths cutted by fixpoint detection....................: 0 | | Paths cutted by nondeterministic formula comparison...: 0 | | Subsumed states excluded from fixpoint computation....: 0 | | Paths cutted that don't lead to assertions............: 0 | | Paths found...........................................: 0 | | States merged.........................................: 0 | | Failed merging attempts...............................: 13116 | | Max. stack depth......................................: 0 | | Max. recursion depth..................................: 0 | | Path splits...........................................: 0 | | Global variables......................................: 17 | | Max. local variables..................................: 24 | | Max. visible variables................................: 41 | | Locations.............................................: 1256 | | Functions.............................................: 1 | | Recursive functions...................................: 0 | | Universal SAT summaries built.........................: 0 | | Universal SAT summaries used..........................: 0 | | Call graph depth of universal summaries...............: 0 | | Size of biggest universal summary.....................: 0 | | Failed attempts to build universal SAT summaries......: 0 | | Path summaries built..................................: 0 | | Path summaries used...................................: 0 | | Nondet universal summaries used.......................: 0 | | Universal summaries needed to refine traces...........: | | QBF restarts for traces containing nondet summaries...: 0 | | Spurious traces found.................................: 0 | | SAT QBF instances.....................................: 0 | | UNSAT QBF instances...................................: 0 | | QBF cache hit.........................................: 176 | | QBF cache miss........................................: 12 | | QBF cache updates.....................................: 0 | | QBF cache updates used................................: 0 | | Diameter..............................................: 81 | | Depth of thread-local fixpoint........................: 0 | | Model type............................................: | | Stable intervals......................................: | | Conceivable global states.............................: 0 | | Explicit global states................................: 0 | | Conceivable thread states.............................: 0 | | Explicit thread states................................: 16003048144896 | | Unbounded model checking thread states................: 0 | | Subsumed states.......................................: 58828 | | Free slot cache hit...................................: 0 | | Split expansions performed one pro variable...........: 0 | | Split expansions avoided..............................: 10226 | | Dynamic constraint generating statements..............: 10226 | | Dynamic non constraint generating statements..........: 185209 | | Static constraint generating statements...............: 1 | | Static non constraint generating statements...........: 190 | | Total number of split variables.......................: 1 | | Independent stmts with same PC........................: 0 | | Independent stmts with other PC.......................: 0 | | Average of number of slots used.......................: 6 | | Median of number of slots used........................: 4 | | Max number of slots used..............................: 41 | ============================================================================ real 0m8.321s user 0m7.412s sys 0m0.020s geri@clfh6701:~/workspace/boom$ |
Simulating an unbounded number of threads takes one third of the time of an exact simulation of 4 threads. This is easy to see: the Karp-Miller construction for unbounded threads over-approximates the number of threads. The idea is to detect "thread creating" cycles and use a special value representing infinitely many threads. Thus, such a loop is only explored once. Whereas the counter abstraction algorithm always stores the exact number of threads and keeps increasing the number with each cycle of such a loop. If the number of threads is increased, the runtime of the counter-abstraction algorithm increases linearly with every additional thread. Therefore there is a number of threads n for every program for which the Karp-Miller construction performs better than the counter-abstraction.