| * satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 version 3.0 results * Timeout: 1800s Memory limit: unlimitedkb Fri Jan 27 17:19:11 2012 |
|||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Benchmark | Broadcast assignment operations executed | Invalid states requiring more than 1 passive thread | Iterations | Local predicates | Max number of slots used | Mixed predicates | Non-broadcast assignment operations executed | Result | Shared predicates | Spurious assignment transitions requiring more than 1 passive thread | Spurious guard transitions requiring more than 1 passive thread | Time abstractor | Time model checker | Time refiner | Time simulator | Time spent in broadcast assignment operations | Time spent in non-broadcast assignment operations | Total transition refinements | Transition refinements | commandline | date | exitcode | expected | maxmem | user | usertime | wallclock |
| regression/symmetry_aware_cav12threader/01_spin2003/test | 0 | 0 | 2 | 0 | 0 | 0 | 42 | SUCCESSFUL | 3 | 0 | 0 | 0.002 | 0.068 | 0.006 | 0.001 | 0 | 0.000269 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Fri Dec 9 00:40:22 GMT 2011 | 0 | valid | 46224kb | alexk | 0.10 | 0:00.08 |
| regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.006 | 0.086 | 0.008 | 0 | 0 | 0.000681 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Fri Dec 9 00:40:23 GMT 2011 | 0 | valid | 46800kb | alexk | 0.13 | 0:00.10 |
| regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 75 | SUCCESSFUL | 6 | 0 | 0 | 0.004 | 0.084 | 0.009 | 0 | 0 | 0.00044 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Fri Dec 9 00:40:24 GMT 2011 | 0 | valid | 46496kb | alexk | 0.13 | 0:00.10 |
| regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.012 | 0.135 | 0.012 | 0 | 0 | 0.003063 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Fri Dec 9 00:40:26 GMT 2011 | 0 | valid | 52048kb | alexk | 0.23 | 0:00.16 |
| regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 4 | 0 | 0 | 0 | 75 | SUCCESSFUL | 7 | 0 | 0 | 0.021 | 0.248 | 0.031 | 0.001 | 0 | 0.00082 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/05_read_write_lock/test.bin | Fri Dec 9 00:40:27 GMT 2011 | 0 | valid | 55904kb | alexk | 0.36 | 0:00.31 |
| regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.018 | 0.101 | 0.007 | 0.001 | 0 | 0.000471 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/06_time_var_mutex/test.bin | Fri Dec 9 00:40:28 GMT 2011 | 0 | valid | 46800kb | alexk | 0.16 | 0:00.13 |
| regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 13 | 0 | 0 | 0 | 1199 | SUCCESSFUL | 24 | 0 | 0 | 23.105 | 3.109 | 1.831 | 0.007 | 0 | 0.011866 | 17 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Fri Dec 9 00:40:29 GMT 2011 | 0 | valid | 58496kb | alexk | 29.98 | 0:28.08 |
| regression/symmetry_aware_cav12threader/08_bakery/test | 49863 | 0 | 18 | 7 | 0 | 4 | 5116 | SUCCESSFUL | 17 | 0 | 0 | 38.742 | 25.708 | 6.024 | 0.016 | 12.1752 | 0.055426 | 60 | 13 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Fri Dec 9 00:40:59 GMT 2011 | 0 | valid | 221616kb | alexk | 81.37 | 1:10.53 |
| regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.028 | 0.435 | 0.25 | 0.004 | 0 | 0.011156 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Fri Dec 9 00:42:10 GMT 2011 | 0 | valid | 51152kb | alexk | 0.88 | 0:00.73 |
| regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 43.479 | 6.223 | 1.377 | 0.01 | 1.71213 | 0.094835 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Fri Dec 9 00:42:12 GMT 2011 | 0 | valid | 169136kb | alexk | 53.99 | 0:51.12 |
| regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 43.715 | 6.187 | 1.375 | 0.012 | 1.67949 | 0.092765 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Fri Dec 9 00:43:04 GMT 2011 | 0 | valid | 169136kb | alexk | 54.24 | 0:51.32 |
| regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 44.794 | 6.903 | 1.424 | 0.012 | 1.73641 | 0.092381 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Fri Dec 9 00:43:57 GMT 2011 | 0 | valid | 170048kb | alexk | 56.61 | 0:53.17 |
| regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.014 | 0.105 | 0.017 | 0 | 0 | 0.000256 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test.bin | Fri Dec 9 00:44:51 GMT 2011 | 0 | valid | 46912kb | alexk | 0.16 | 0:00.14 |
| regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | 141833 | SUCCESSFUL | 0 | 0 | 0 | 4.963 | 26.765 | 0.035 | 0.001 | 0 | 3.23975 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Fri Dec 9 00:44:52 GMT 2011 | 0 | valid | 2059104kb | alexk | 32.16 | 0:31.78 |
| regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 6 | 9 | 0 | 0 | 1915 | SUCCESSFUL | 5 | 0 | 0 | 0.215 | 1.092 | 0.88 | 0.017 | 0 | 0.02709 | 6 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Fri Dec 9 00:45:25 GMT 2011 | 0 | valid | 70752kb | alexk | 2.68 | 0:02.25 |
| regression/symmetry_aware_threader_ready/01_inc/test | 147 | 0 | 6 | 1 | 0 | 1 | 229 | SUCCESSFUL | 3 | 0 | 0 | 0.784 | 0.402 | 0.996 | 0.005 | 0.011516 | 0.002395 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Fri Dec 9 00:45:28 GMT 2011 | 0 | valid | 50560kb | alexk | 2.23 | 0:02.20 |
| regression/symmetry_aware_threader_ready/02_inc_cas/test | 334 | 0 | 7 | 4 | 0 | 2 | 290 | SUCCESSFUL | 0 | 0 | 0 | 2.298 | 0.583 | 0.907 | 0.005 | 0.079137 | 0.002821 | 15 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Fri Dec 9 00:45:32 GMT 2011 | 0 | valid | 68528kb | alexk | 4.04 | 0:03.81 |
| regression/symmetry_aware_threader_ready/03_incdec/test | 187 | 0 | 10 | 2 | 0 | 2 | 1598 | SUCCESSFUL | 7 | 0 | 0 | 4.95 | 1.341 | 2.177 | 0.011 | 0.110485 | 0.018963 | 17 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Fri Dec 9 00:45:36 GMT 2011 | 0 | valid | 88256kb | alexk | 9.11 | 0:08.50 |
| regression/symmetry_aware_threader_ready/04_incdec_cas/test | 28213 | 0 | 18 | 8 | 0 | 4 | 6444 | SUCCESSFUL | 2 | 0 | 0 | 7.741 | 44.394 | 4.358 | 0.02 | 25.0431 | 0.072719 | 84 | 13 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Fri Dec 9 00:45:46 GMT 2011 | 0 | valid | 1073776kb | alexk | 60.69 | 0:56.55 |
| regression/symmetry_aware_threader_ready/05_tas/test | 286 | 0 | 2 | 1 | 0 | 1 | 373 | SUCCESSFUL | 4 | 0 | 0 | 0.077 | 0.242 | 0.015 | 0.001 | 0.025603 | 0.004295 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Fri Dec 9 00:46:44 GMT 2011 | 0 | valid | 64032kb | alexk | 0.39 | 0:00.34 |
| regression/symmetry_aware_threader_ready/06_ticket/test | 1483 | 0 | 6 | 2 | 0 | 5 | 15264 | SUCCESSFUL | 9 | 0 | 0 | 61.488 | 10.909 | 2.857 | 0.055 | 5.83274 | 0.213033 | 5 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Fri Dec 9 00:46:45 GMT 2011 | 0 | valid | 262224kb | alexk | 77.35 | 1:15.33 |
| regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 3 | 8 | 0 | 0 | 1344 | SUCCESSFUL | 3 | 0 | 0 | 5.666 | 0.28 | 0.587 | 0.007 | 0 | 0.013722 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Fri Dec 9 00:48:02 GMT 2011 | 0 | valid | 79520kb | alexk | 6.56 | 0:06.55 |
| regression/symmetry_aware_threader_ready/08_rand_cas/test | 357469 | 0 | 13 | 15 | 0 | 1 | 74568 | SUCCESSFUL | 2 | 0 | 0 | 27.836 | 847.756 | 22.282 | 0.031 | 487.599 | 0.933336 | 42 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Fri Dec 9 00:48:09 GMT 2011 | 0 | valid | 9086240kb | alexk | 911.52 | 14:57.94 |
| regression/symmetry_aware_threader_ready/09_fmaxsym/test | 395 | 0 | 2 | 6 | 0 | 7 | 3716 | SUCCESSFUL | 2 | 0 | 0 | 183.713 | 4.448 | 0.257 | 0.015 | 3.54748 | 0.054309 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Fri Dec 9 01:03:08 GMT 2011 | 0 | valid | 194576kb | alexk | 188.51 | 3:08.45 |
| regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 4053 | 0 | 7 | 2 | 0 | 4 | 13970 | SUCCESSFUL | 0 | 0 | 0 | 5.683 | 12.934 | 0.8 | 0.075 | 5.19032 | 0.152569 | 13 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Fri Dec 9 01:06:18 GMT 2011 | 0 | valid | 577568kb | alexk | 20.50 | 0:19.51 |
| regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 329 | 0 | 2 | 2 | 0 | 1 | 4599 | SUCCESSFUL | 2 | 0 | 0 | 0.719 | 0.602 | 0.246 | 0.018 | 0.032983 | 0.041595 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Fri Dec 9 01:06:38 GMT 2011 | 0 | valid | 105696kb | alexk | 1.70 | 0:01.60 |
| regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 49025 | 0 | 8 | 3 | 0 | 4 | 26302 | SUCCESSFUL | 0 | 0 | 0 | 7.428 | 74.372 | 2.807 | 0.11 | 33.1166 | 0.347254 | 24 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Fri Dec 9 01:06:41 GMT 2011 | 0 | valid | 957088kb | alexk | 105.06 | 1:24.74 |
| regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 4 | 6 | 0 | 0 | 125207 | SUCCESSFUL | 6 | 0 | 0 | 0.045 | 16.853 | 0.134 | 0.011 | 0 | 1.55728 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 01:08:07 GMT 2011 | 0 | valid | 1689760kb | alexk | 17.09 | 0:17.05 |
| regression/symmetry_aware_threader_ready/14_stack_cas/test | 8972 | 0 | 4 | 6 | 0 | 1 | 104957 | SUCCESSFUL | 4 | 0 | 0 | 0.103 | 19.38 | 0.141 | 0.01 | 2.89223 | 1.28449 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Fri Dec 9 01:08:25 GMT 2011 | 0 | valid | 1665920kb | alexk | 19.88 | 0:19.65 |
| regression/symmetry_aware_threader_ready/15_unverif/test | 82 | 0 | 2 | 0 | 0 | 2 | 298 | SUCCESSFUL | 3 | 0 | 0 | 0.287 | 0.126 | 0.011 | 0.001 | 0.004632 | 0.001909 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/15_unverif/test.bin | Mon Dec 19 12:18:15 GMT 2011 | 0 | valid | 50928kb | alexk | 0.50 | 0:00.43 |