* satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 version 3.0 results * Timeout: 1800s Memory limit: unlimitedkb Fri Jan 27 17:19:09 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.002 | 0.081 | 0.006 | 0 | 0 | 0.000328 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Thu Dec 8 21:54:38 GMT 2011 | 0 | valid | 45968kb | alexk | 0.17 | 0:00.09 |
regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.005 | 0.113 | 0.008 | 0.001 | 0 | 0.000651 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Thu Dec 8 21:54:39 GMT 2011 | 0 | valid | 46784kb | alexk | 0.14 | 0:00.13 |
regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 139 | SUCCESSFUL | 6 | 0 | 0 | 0.004 | 0.098 | 0.008 | 0.001 | 0 | 0.000749 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Thu Dec 8 21:54:40 GMT 2011 | 0 | valid | 46496kb | alexk | 0.14 | 0:00.11 |
regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.009 | 0.174 | 0.011 | 0.001 | 0 | 0.002876 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Thu Dec 8 21:54:41 GMT 2011 | 0 | valid | 52048kb | alexk | 0.27 | 0:00.20 |
regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 3 | 0 | 0 | 0 | 55 | SUCCESSFUL | 7 | 0 | 0 | 0.004 | 0.168 | 0.021 | 0.002 | 0 | 0.00041 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/05_read_write_lock/test.bin | Thu Dec 8 21:54:42 GMT 2011 | 0 | valid | 44464kb | alexk | 0.38 | 0:00.19 |
regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 138 | SUCCESSFUL | 7 | 0 | 0 | 0.005 | 0.118 | 0.006 | 0.001 | 0 | 0.000831 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/06_time_var_mutex/test.bin | Thu Dec 8 21:54:44 GMT 2011 | 0 | valid | 46336kb | alexk | 0.19 | 0:00.13 |
regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 24 | 0 | 0 | 0 | 2796 | SUCCESSFUL | 24 | 0 | 0 | 0.076 | 3.548 | 2.546 | 0.012 | 0 | 0.030896 | 94 | 20 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Thu Dec 8 21:54:45 GMT 2011 | 0 | valid | 54096kb | alexk | 8.89 | 0:06.20 |
regression/symmetry_aware_cav12threader/08_bakery/test | 123755 | 0 | 23 | 7 | 0 | 4 | 2311 | SUCCESSFUL | 17 | 0 | 0 | 0.095 | 40.458 | 7.723 | 0.021 | 18.304 | 0.029845 | 167 | 19 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Thu Dec 8 21:54:52 GMT 2011 | 0 | valid | 197904kb | alexk | 61.64 | 0:48.32 |
regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.017 | 0.329 | 0.145 | 0.004 | 0 | 0.007066 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Thu Dec 8 21:55:41 GMT 2011 | 0 | valid | 51184kb | alexk | 0.68 | 0:00.50 |
regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9102 | 0 | 11 | 10 | 0 | 2 | 11391 | SUCCESSFUL | 13 | 0 | 0 | 0.154 | 5.16 | 1.276 | 0.011 | 1.28737 | 0.071759 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Thu Dec 8 21:55:43 GMT 2011 | 0 | valid | 169136kb | alexk | 9.48 | 0:06.62 |
regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9102 | 0 | 11 | 10 | 0 | 2 | 11391 | SUCCESSFUL | 13 | 0 | 0 | 0.156 | 5.189 | 1.272 | 0.011 | 1.29961 | 0.072351 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Thu Dec 8 21:55:51 GMT 2011 | 0 | valid | 169136kb | alexk | 9.60 | 0:06.64 |
regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9102 | 0 | 11 | 10 | 0 | 2 | 11402 | SUCCESSFUL | 14 | 0 | 0 | 0.179 | 5.63 | 1.339 | 0.012 | 1.34231 | 0.071746 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Thu Dec 8 21:55:58 GMT 2011 | 0 | valid | 169904kb | alexk | 10.47 | 0:07.18 |
regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 62 | SUCCESSFUL | 5 | 0 | 0 | 0.004 | 0.13 | 0.011 | 0.001 | 0 | 0.00033 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test.bin | Thu Dec 8 21:56:07 GMT 2011 | 0 | valid | 46528kb | alexk | 0.23 | 0:00.15 |
regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | SUCCESSFUL | 0 | 0 | 0 | 0.072 | 251.326 | 0.034 | 0.002 | 0 | 25.4195 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Thu Dec 8 21:56:08 GMT 2011 | 0 | valid | 19056352kb | alexk | 258.06 | 4:11.45 | |
regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 6 | 9 | 0 | 0 | 2311 | SUCCESSFUL | 5 | 0 | 0 | 0.111 | 0.856 | 0.492 | 0.01 | 0 | 0.019096 | 6 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Thu Dec 8 22:00:20 GMT 2011 | 0 | valid | 74752kb | alexk | 1.80 | 0:01.49 |
regression/symmetry_aware_threader_ready/01_inc/test | 146 | 0 | 7 | 2 | 0 | 2 | 826 | SUCCESSFUL | 5 | 0 | 0 | 0.026 | 0.473 | 0.786 | 0.004 | 0.025781 | 0.00669 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Thu Dec 8 22:00:23 GMT 2011 | 0 | valid | 72880kb | alexk | 1.38 | 0:01.29 |
regression/symmetry_aware_threader_ready/02_inc_cas/test | 1708 | 0 | 7 | 4 | 0 | 2 | 1199 | SUCCESSFUL | 0 | 0 | 0 | 0.014 | 2.645 | 0.416 | 0.003 | 1.80981 | 0.010779 | 21 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Thu Dec 8 22:00:25 GMT 2011 | 0 | valid | 187264kb | alexk | 3.39 | 0:03.08 |
regression/symmetry_aware_threader_ready/03_incdec/test | 6866 | 0 | 16 | 4 | 0 | 3 | 11086 | SUCCESSFUL | 9 | 0 | 0 | 0.086 | 20.807 | 3.825 | 0.016 | 15.0233 | 0.154803 | 43 | 12 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Thu Dec 8 22:00:29 GMT 2011 | 0 | valid | 640208kb | alexk | 26.90 | 0:24.76 |
regression/symmetry_aware_threader_ready/04_incdec_cas/test | 417279 | 0 | 24 | 8 | 0 | 4 | 69966 | SUCCESSFUL | 2 | 0 | 0 | 0.065 | 902.651 | 5.052 | 0.021 | 446.665 | 0.568999 | 108 | 19 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Thu Dec 8 22:00:55 GMT 2011 | 0 | valid | 21867664kb | alexk | 940.29 | 15:07.82 |
regression/symmetry_aware_threader_ready/05_tas/test | 1685 | 0 | 3 | 1 | 0 | 1 | 2335 | SUCCESSFUL | 4 | 0 | 0 | 0.01 | 0.755 | 0.012 | 0 | 0.159147 | 0.019644 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Thu Dec 8 22:16:04 GMT 2011 | 0 | valid | 156528kb | alexk | 0.94 | 0:00.78 |
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 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Thu Dec 8 22:16:06 GMT 2011 | 130 | valid | 14148288kb | alexk | 2141.52 | 30:00.14 | ||||||||||||||
regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 4 | 8 | 0 | 0 | 6533 | SUCCESSFUL | 3 | 0 | 0 | 0.085 | 0.786 | 0.976 | 0.009 | 0 | 0.046166 | 5 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Thu Dec 8 22:46:07 GMT 2011 | 0 | valid | 230848kb | alexk | 1.92 | 0:01.86 |
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 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Thu Dec 8 22:46:10 GMT 2011 | 130 | valid | alexk | |||||||||||||||||
regression/symmetry_aware_threader_ready/09_fmaxsym/test | 1930 | 0 | 3 | 6 | 0 | 7 | 21716 | SUCCESSFUL | 2 | 0 | 0 | 0.17 | 8.045 | 0.188 | 0.019 | 4.30768 | 0.206169 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Thu Dec 8 23:16:11 GMT 2011 | 0 | valid | 499504kb | alexk | 9.38 | 0:08.43 |
regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 276619 | 0 | 13 | 2 | 0 | 4 | 185678 | SUCCESSFUL | 0 | 0 | 0 | 0.05 | 1513.42 | 1.065 | 0.104 | 627.526 | 4.69157 | 45 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Thu Dec 8 23:16:20 GMT 2011 | 0 | valid | 12056160kb | alexk | 1827.97 | 25:14.65 |
regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 3003 | 0 | 3 | 2 | 0 | 1 | 47401 | SUCCESSFUL | 2 | 0 | 0 | 0.049 | 5.116 | 0.204 | 0.021 | 0.469953 | 0.414761 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Thu Dec 8 23:41:36 GMT 2011 | 0 | valid | 621712kb | alexk | 5.91 | 0:05.39 |
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 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Thu Dec 8 23:41:43 GMT 2011 | 130 | valid | 9168176kb | alexk | 1838.41 | 30:00.10 | ||||||||||||||
regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 5 | 6 | 0 | 0 | SUCCESSFUL | 6 | 0 | 0 | 0.026 | 402.932 | 0.096 | 0.008 | 0 | 33.2001 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 00:11:44 GMT 2011 | 0 | valid | 28682720kb | alexk | 420.22 | 6:43.07 | |
regression/symmetry_aware_threader_ready/14_stack_cas/test | 202588 | 0 | 7 | 6 | 0 | 1 | SUCCESSFUL | 4 | 0 | 0 | 0.041 | 699.444 | 0.294 | 0.022 | 135.336 | 32.4138 | 4 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Fri Dec 9 00:18:28 GMT 2011 | 0 | valid | 31867024kb | alexk | 718.58 | 11:39.81 | |
regression/symmetry_aware_threader_ready/15_unverif/test | 7786 | 0 | 8 | 0 | 0 | 3 | 3601 | SUCCESSFUL | 5 | 0 | 0 | 0.013 | 2.735 | 0.638 | 0.003 | 1.03753 | 0.04048 | 30 | 5 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 4 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/15_unverif/test.bin | Mon Dec 19 11:41:35 GMT 2011 | 0 | valid | 114096kb | alexk | 4.58 | 0:03.39 |