* satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --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 | 58 | SUCCESSFUL | 3 | 0 | 0 | 0.004 | 0.103 | 0.01 | 0.001 | 0 | 0.000486 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Fri Dec 9 01:08:46 GMT 2011 | 0 | valid | 46240kb | alexk | 0.17 | 0:00.12 |
regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.009 | 0.14 | 0.013 | 0 | 0 | 0.000991 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Fri Dec 9 01:08:48 GMT 2011 | 0 | valid | 46784kb | alexk | 0.18 | 0:00.17 |
regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 139 | SUCCESSFUL | 6 | 0 | 0 | 0.005 | 0.137 | 0.014 | 0 | 0 | 0.001171 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Fri Dec 9 01:08:49 GMT 2011 | 0 | valid | 46496kb | alexk | 0.24 | 0:00.16 |
regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.019 | 0.245 | 0.019 | 0.002 | 0 | 0.004418 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Fri Dec 9 01:08:50 GMT 2011 | 0 | valid | 52048kb | alexk | 0.41 | 0:00.29 |
regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 4 | 0 | 0 | 0 | 75 | SUCCESSFUL | 7 | 0 | 0 | 0.038 | 0.291 | 0.049 | 0.003 | 0 | 0.000817 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/05_read_write_lock/test.bin | Fri Dec 9 01:08:51 GMT 2011 | 0 | valid | 55904kb | alexk | 0.43 | 0:00.39 |
regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.028 | 0.17 | 0.01 | 0.001 | 0 | 0.000614 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/06_time_var_mutex/test.bin | Fri Dec 9 01:08:53 GMT 2011 | 0 | valid | 46800kb | alexk | 0.27 | 0:00.21 |
regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 13 | 0 | 0 | 0 | 1199 | SUCCESSFUL | 24 | 0 | 0 | 37.417 | 4.459 | 2.943 | 0.014 | 0 | 0.017767 | 17 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Fri Dec 9 01:08:54 GMT 2011 | 0 | valid | 58496kb | alexk | 48.26 | 0:44.87 |
regression/symmetry_aware_cav12threader/08_bakery/test | 49863 | 0 | 18 | 7 | 0 | 4 | 5116 | SUCCESSFUL | 17 | 0 | 0 | 61.292 | 36.56 | 9.556 | 0.022 | 15.0462 | 0.062461 | 60 | 13 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Fri Dec 9 01:09:40 GMT 2011 | 0 | valid | 236032kb | alexk | 125.38 | 1:47.48 |
regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.028 | 0.47 | 0.25 | 0.004 | 0 | 0.01172 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Fri Dec 9 01:11:29 GMT 2011 | 0 | valid | 51184kb | alexk | 1.04 | 0:00.76 |
regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 51.133 | 7.181 | 1.63 | 0.017 | 1.77862 | 0.101063 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Fri Dec 9 01:11:31 GMT 2011 | 0 | valid | 169136kb | alexk | 63.79 | 1:00.00 |
regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11373 | SUCCESSFUL | 13 | 0 | 0 | 72.564 | 8.355 | 2.33 | 0.015 | 2.13539 | 0.120115 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Fri Dec 9 01:12:32 GMT 2011 | 0 | valid | 169152kb | alexk | 87.29 | 1:23.31 |
regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 66.3 | 9.05 | 2.163 | 0.017 | 2.27858 | 0.124581 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Fri Dec 9 01:13:56 GMT 2011 | 0 | valid | 170048kb | alexk | 81.81 | 1:17.59 |
regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.013 | 0.161 | 0.016 | 0.001 | 0 | 0.000365 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test.bin | Fri Dec 9 01:15:15 GMT 2011 | 0 | valid | 46912kb | alexk | 0.24 | 0:00.20 |
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 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Fri Dec 9 01:15:16 GMT 2011 | 1 | valid | 56886608kb | alexk | 916.96 | 15:26.64 | ||||||||||||||
regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 6 | 9 | 0 | 0 | 1915 | SUCCESSFUL | 5 | 0 | 0 | 0.204 | 1.151 | 0.879 | 0.015 | 0 | 0.021716 | 6 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Fri Dec 9 01:30:46 GMT 2011 | 0 | valid | 70752kb | alexk | 2.50 | 0:02.31 |
regression/symmetry_aware_threader_ready/01_inc/test | 388 | 0 | 6 | 1 | 0 | 1 | 387 | SUCCESSFUL | 3 | 0 | 0 | 0.538 | 0.446 | 0.633 | 0.005 | 0.04947 | 0.004294 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Fri Dec 9 01:30:49 GMT 2011 | 0 | valid | 64384kb | alexk | 1.80 | 0:01.63 |
regression/symmetry_aware_threader_ready/02_inc_cas/test | 1242 | 0 | 7 | 4 | 0 | 2 | 1062 | SUCCESSFUL | 0 | 0 | 0 | 2.3 | 2.021 | 0.935 | 0.008 | 1.07944 | 0.012463 | 15 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Fri Dec 9 01:30:52 GMT 2011 | 0 | valid | 140768kb | alexk | 5.63 | 0:05.27 |
regression/symmetry_aware_threader_ready/03_incdec/test | 769 | 0 | 10 | 2 | 0 | 2 | 6660 | SUCCESSFUL | 7 | 0 | 0 | 5.69 | 7.639 | 3.371 | 0.012 | 4.13702 | 0.122379 | 17 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Fri Dec 9 01:30:58 GMT 2011 | 0 | valid | 354416kb | alexk | 18.16 | 0:16.74 |
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 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Fri Dec 9 01:31:16 GMT 2011 | 130 | valid | 2999568kb | alexk | 1826.39 | 30:00.05 | ||||||||||||||
regression/symmetry_aware_threader_ready/05_tas/test | 1376 | 0 | 2 | 1 | 0 | 1 | 1831 | SUCCESSFUL | 4 | 0 | 0 | 0.079 | 1.012 | 0.015 | 0.001 | 0.221833 | 0.023335 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Fri Dec 9 02:01:18 GMT 2011 | 0 | valid | 150128kb | alexk | 1.29 | 0:01.11 |
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 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Fri Dec 9 02:01:20 GMT 2011 | 130 | valid | 18932448kb | alexk | 2278.56 | 30:00.03 | ||||||||||||||
regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 3 | 8 | 0 | 0 | 6514 | SUCCESSFUL | 3 | 0 | 0 | 3.417 | 0.987 | 0.372 | 0.004 | 0 | 0.051187 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Fri Dec 9 02:31:22 GMT 2011 | 0 | valid | 230880kb | alexk | 4.95 | 0:04.79 |
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 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Fri Dec 9 02:31:27 GMT 2011 | 130 | valid | 9086240kb | alexk | 3533.70 | 30:00.06 | ||||||||||||||
regression/symmetry_aware_threader_ready/09_fmaxsym/test | 2948 | 0 | 2 | 6 | 0 | 7 | 34759 | SUCCESSFUL | 2 | 0 | 0 | 185.661 | 90.004 | 0.273 | 0.018 | 77.0115 | 0.764158 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Fri Dec 9 03:01:29 GMT 2011 | 0 | valid | 590448kb | alexk | 293.04 | 4:35.97 |
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 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Fri Dec 9 03:06:06 GMT 2011 | 130 | valid | 8524992kb | alexk | 1788.39 | 30:00.17 | ||||||||||||||
regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 2653 | 0 | 2 | 2 | 0 | 1 | 42459 | SUCCESSFUL | 2 | 0 | 0 | 0.442 | 4.693 | 0.15 | 0.01 | 0.39478 | 0.411135 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Fri Dec 9 03:36:08 GMT 2011 | 0 | valid | 568880kb | alexk | 5.75 | 0:05.30 |
regression/symmetry_aware_threader_ready/12_fmaxsymopt_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 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Fri Dec 9 03:36:14 GMT 2011 | 130 | valid | 10572416kb | alexk | 1835.87 | 30:00.12 | ||||||||||||||
regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 4 | 6 | 0 | 0 | SUCCESSFUL | 6 | 0 | 0 | 0.029 | 407.006 | 0.085 | 0.007 | 0 | 33.1511 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 04:06:16 GMT 2011 | 0 | valid | 28682752kb | alexk | 424.25 | 6:47.13 | |
regression/symmetry_aware_threader_ready/14_stack_cas/test | 201900 | 0 | 4 | 6 | 0 | 1 | SUCCESSFUL | 4 | 0 | 0 | 0.096 | 700.798 | 0.127 | 0.011 | 139.433 | 32.9212 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Fri Dec 9 04:13:04 GMT 2011 | 0 | valid | 31876688kb | alexk | 718.31 | 11:41.04 | |
regression/symmetry_aware_threader_ready/15_unverif/test | 851 | 0 | 3 | 0 | 0 | 3 | 4752 | SUCCESSFUL | 5 | 0 | 0 | 0.903 | 1.036 | 0.2 | 0.001 | 0.342961 | 0.037959 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 --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:17 GMT 2011 | 0 | valid | 104640kb | alexk | 2.49 | 0:02.14 |