* satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 version 3.0 results * Timeout: 1800s Memory limit: unlimitedkb Fri Jan 27 17:19:10 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 | 58 | SUCCESSFUL | 3 | 0 | 0 | 0.004 | 0.108 | 0.01 | 0.001 | 0 | 0.000499 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Fri Dec 9 04:50:45 GMT 2011 | 0 | valid | 46224kb | alexk | 0.14 | 0:00.13 |
regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.009 | 0.153 | 0.013 | 0 | 0 | 0.001025 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Fri Dec 9 04:50:46 GMT 2011 | 0 | valid | 46784kb | alexk | 0.25 | 0:00.18 |
regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 75 | SUCCESSFUL | 6 | 0 | 0 | 0.005 | 0.144 | 0.014 | 0 | 0 | 0.000619 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Fri Dec 9 04:50:47 GMT 2011 | 0 | valid | 46480kb | alexk | 0.19 | 0:00.17 |
regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.018 | 0.228 | 0.02 | 0.001 | 0 | 0.004357 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Fri Dec 9 04:50:49 GMT 2011 | 0 | valid | 52048kb | alexk | 0.35 | 0:00.27 |
regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 4 | 0 | 0 | 0 | 75 | SUCCESSFUL | 7 | 0 | 0 | 0.021 | 0.294 | 0.049 | 0.003 | 0 | 0.000731 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/05_read_write_lock/test.bin | Fri Dec 9 04:50:50 GMT 2011 | 0 | valid | 58976kb | alexk | 0.43 | 0:00.37 |
regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.016 | 0.17 | 0.011 | 0 | 0 | 0.000686 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/06_time_var_mutex/test.bin | Fri Dec 9 04:50:51 GMT 2011 | 0 | valid | 46736kb | alexk | 0.26 | 0:00.20 |
regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 22 | 0 | 0 | 0 | 2308 | SUCCESSFUL | 24 | 0 | 0 | 2.916 | 4.675 | 5.095 | 0.023 | 0 | 0.033178 | 51 | 18 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Fri Dec 9 04:50:53 GMT 2011 | 0 | valid | 53856kb | alexk | 16.20 | 0:12.74 |
regression/symmetry_aware_cav12threader/08_bakery/test | 108295 | 0 | 21 | 7 | 0 | 4 | 5177 | SUCCESSFUL | 17 | 0 | 0 | 3.141 | 81.67 | 11.134 | 0.029 | 29.1253 | 0.080258 | 94 | 16 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Fri Dec 9 04:51:06 GMT 2011 | 0 | valid | 228848kb | alexk | 108.63 | 1:36.01 |
regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.029 | 0.485 | 0.244 | 0.004 | 0 | 0.011655 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Fri Dec 9 04:52:44 GMT 2011 | 0 | valid | 51184kb | alexk | 0.98 | 0:00.77 |
regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11373 | SUCCESSFUL | 13 | 0 | 0 | 5.352 | 8.317 | 2.266 | 0.017 | 2.19222 | 0.124925 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Fri Dec 9 04:52:45 GMT 2011 | 0 | valid | 169136kb | alexk | 19.96 | 0:15.99 |
regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 5.386 | 8.222 | 2.293 | 0.018 | 2.19028 | 0.122897 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Fri Dec 9 04:53:02 GMT 2011 | 0 | valid | 169136kb | alexk | 19.79 | 0:15.96 |
regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 5.567 | 8.74 | 2.39 | 0.017 | 2.18316 | 0.121814 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Fri Dec 9 04:53:20 GMT 2011 | 0 | valid | 170032kb | alexk | 21.12 | 0:16.76 |
regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.013 | 0.17 | 0.019 | 0 | 0 | 0.000412 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test.bin | Fri Dec 9 04:53:37 GMT 2011 | 0 | valid | 46896kb | alexk | 0.27 | 0:00.21 |
regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | ERROR | 0 | 0 | -2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Fri Dec 9 04:53:39 GMT 2011 | 1 | valid | 49955328kb | alexk | 590.05 | 9:37.87 | ||||||||||||||
regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 6 | 9 | 0 | 0 | 1915 | SUCCESSFUL | 5 | 0 | 0 | 0.186 | 1.253 | 0.796 | 0.015 | 0 | 0.027277 | 6 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Fri Dec 9 05:03:19 GMT 2011 | 0 | valid | 70768kb | alexk | 2.63 | 0:02.29 |
regression/symmetry_aware_threader_ready/01_inc/test | 388 | 0 | 6 | 1 | 0 | 1 | 387 | SUCCESSFUL | 3 | 0 | 0 | 0.186 | 0.542 | 0.904 | 0.007 | 0.05007 | 0.004413 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Fri Dec 9 05:03:22 GMT 2011 | 0 | valid | 64144kb | alexk | 1.80 | 0:01.65 |
regression/symmetry_aware_threader_ready/02_inc_cas/test | 434 | 0 | 6 | 4 | 0 | 2 | 2281 | SUCCESSFUL | 0 | 0 | 0 | 0.268 | 1.183 | 0.59 | 0.003 | 0.387005 | 0.025584 | 9 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Fri Dec 9 05:03:25 GMT 2011 | 0 | valid | 146128kb | alexk | 2.40 | 0:02.05 |
regression/symmetry_aware_threader_ready/03_incdec/test | 761 | 0 | 10 | 2 | 0 | 2 | 6640 | SUCCESSFUL | 7 | 0 | 0 | 0.789 | 5.526 | 3.372 | 0.015 | 1.9159 | 0.120441 | 17 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Fri Dec 9 05:03:28 GMT 2011 | 0 | valid | 343744kb | alexk | 10.97 | 0:09.73 |
regression/symmetry_aware_threader_ready/04_incdec_cas/test | 0 | ERROR | 0 | 0 | -5 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Fri Dec 9 05:03:39 GMT 2011 | 130 | valid | 4942112kb | alexk | 1852.60 | 30:00.08 | ||||||||||||||
regression/symmetry_aware_threader_ready/05_tas/test | 1378 | 0 | 3 | 1 | 0 | 1 | 1835 | SUCCESSFUL | 4 | 0 | 0 | 0.018 | 0.76 | 0.013 | 0 | 0.149353 | 0.016631 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Fri Dec 9 05:33:40 GMT 2011 | 0 | valid | 149744kb | alexk | 0.99 | 0:00.79 |
regression/symmetry_aware_threader_ready/06_ticket/test | 0 | ERROR | 0 | 0 | -3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Fri Dec 9 05:33:42 GMT 2011 | 130 | valid | 16996160kb | alexk | 2073.41 | 30:00.02 | ||||||||||||||
regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 3 | 8 | 0 | 0 | 6514 | SUCCESSFUL | 3 | 0 | 0 | 0 | 0.054472 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Fri Dec 9 06:03:43 GMT 2011 | 0 | valid | 230880kb | alexk | 2.16 | 0:02.03 | ||||
regression/symmetry_aware_threader_ready/08_rand_cas/test | 0 | ERROR | 0 | 0 | -6 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Fri Dec 9 06:03:46 GMT 2011 | 130 | valid | 7365872kb | alexk | 2323.07 | 30:00.02 | ||||||||||||||
regression/symmetry_aware_threader_ready/09_fmaxsym/test | 2847 | 0 | 3 | 6 | 0 | 7 | 33765 | SUCCESSFUL | 2 | 0 | 0 | 6.374 | 31.951 | 0.206 | 0.023 | 25.6662 | 0.463786 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Fri Dec 9 06:33:47 GMT 2011 | 0 | valid | 561840kb | alexk | 52.75 | 0:38.56 |
regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 0 | ERROR | 0 | 0 | -4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Fri Dec 9 06:34:27 GMT 2011 | 130 | valid | 8326656kb | alexk | 2221.42 | 30:00.09 | ||||||||||||||
regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 2675 | 0 | 3 | 2 | 0 | 1 | 42579 | SUCCESSFUL | 2 | 0 | 0 | 0.209 | 4.568 | 0.207 | 0.021 | 0.366322 | 0.392217 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Fri Dec 9 07:04:28 GMT 2011 | 0 | valid | 566688kb | alexk | 5.54 | 0:05.01 |
regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 420165 | 0 | 11 | 3 | 0 | 4 | 8284 | SUCCESSFUL | 0 | 0 | 0 | 0.612 | 1456.83 | 2.156 | 0.133 | 1079.99 | 0.119196 | 45 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Fri Dec 9 07:04:34 GMT 2011 | 0 | valid | 8903760kb | alexk | 1506.13 | 24:19.75 |
regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 4 | 6 | 0 | 0 | SUCCESSFUL | 6 | 0 | 0 | 0.05 | 472.221 | 0.139 | 0.01 | 0 | 53.8851 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 07:28:55 GMT 2011 | 0 | valid | 28677520kb | alexk | 440.07 | 7:52.51 | |
regression/symmetry_aware_threader_ready/14_stack_cas/test | 202529 | 0 | 5 | 6 | 0 | 1 | SUCCESSFUL | 4 | 0 | 0 | 0.04 | 598.893 | 0.134 | 0.012 | 117.428 | 28.1418 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Fri Dec 9 07:36:50 GMT 2011 | 0 | valid | 31866944kb | alexk | 618.40 | 9:59.10 | |
regression/symmetry_aware_threader_ready/15_unverif/test | 1089 | 0 | 4 | 0 | 0 | 3 | 6312 | SUCCESSFUL | 5 | 0 | 0 | 0.16 | 1.342 | 0.366 | 0.002 | 0.428063 | 0.050637 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/15_unverif/test.bin | Mon Dec 19 12:18:25 GMT 2011 | 0 | valid | 109152kb | alexk | 2.35 | 0:01.87 |