| * satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 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 | 47 | SUCCESSFUL | 3 | 0 | 0 | 0.004 | 0.066 | 0.01 | 0 | 0 | 0.000385 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Fri Dec 9 04:24:47 GMT 2011 | 0 | valid | 46224kb | alexk | 0.09 | 0:00.08 |
| regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.009 | 0.089 | 0.012 | 0.001 | 0 | 0.001042 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Fri Dec 9 04:24:48 GMT 2011 | 0 | valid | 46592kb | alexk | 0.08 | 0:00.11 |
| regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 139 | SUCCESSFUL | 6 | 0 | 0 | 0.006 | 0.087 | 0.012 | 0.001 | 0 | 0.001185 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Fri Dec 9 04:24:50 GMT 2011 | 0 | valid | 46480kb | alexk | 0.15 | 0:00.11 |
| regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.019 | 0.152 | 0.019 | 0.001 | 0 | 0.004327 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Fri Dec 9 04:24:51 GMT 2011 | 0 | valid | 52048kb | alexk | 0.17 | 0:00.20 |
| regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 4 | 0 | 0 | 0 | 75 | SUCCESSFUL | 7 | 0 | 0 | 0.018 | 0.225 | 0.046 | 0.003 | 0 | 0.000752 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:24:52 GMT 2011 | 0 | valid | 58976kb | alexk | 0.40 | 0:00.30 |
| regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.018 | 0.104 | 0.013 | 0 | 0 | 0.000668 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:24:53 GMT 2011 | 0 | valid | 46736kb | alexk | 0.19 | 0:00.14 |
| regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 22 | 0 | 0 | 0 | 2308 | SUCCESSFUL | 24 | 0 | 0 | 2.574 | 4.046 | 4.506 | 0.017 | 0 | 0.03342 | 51 | 18 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Fri Dec 9 04:24:55 GMT 2011 | 0 | valid | 53856kb | alexk | 13.55 | 0:11.17 |
| regression/symmetry_aware_cav12threader/08_bakery/test | 108295 | 0 | 21 | 7 | 0 | 4 | 5177 | SUCCESSFUL | 17 | 0 | 0 | 2.777 | 58.464 | 7.677 | 0.021 | 22.008 | 0.058307 | 94 | 16 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Fri Dec 9 04:25:07 GMT 2011 | 0 | valid | 228832kb | alexk | 80.33 | 1:08.97 |
| regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.028 | 0.381 | 0.246 | 0.004 | 0 | 0.011034 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Fri Dec 9 04:26:17 GMT 2011 | 0 | valid | 50976kb | alexk | 0.76 | 0:00.67 |
| regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 3.988 | 6.062 | 1.54 | 0.014 | 1.59385 | 0.092723 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Fri Dec 9 04:26:19 GMT 2011 | 0 | valid | 169136kb | alexk | 14.90 | 0:11.64 |
| regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 4.636 | 7.505 | 1.998 | 0.013 | 2.14326 | 0.123281 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Fri Dec 9 04:26:31 GMT 2011 | 0 | valid | 169136kb | alexk | 17.53 | 0:14.19 |
| regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 5.512 | 8.178 | 2.364 | 0.016 | 2.27552 | 0.125952 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Fri Dec 9 04:26:47 GMT 2011 | 0 | valid | 170032kb | alexk | 19.79 | 0:16.11 |
| regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.012 | 0.109 | 0.017 | 0 | 0 | 0.000325 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:27:04 GMT 2011 | 0 | valid | 46912kb | alexk | 0.16 | 0:00.14 |
| regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | 2756 | SUCCESSFUL | 0 | 0 | 0 | 1.773 | 0.755 | 0.053 | 0 | 0 | 0.034315 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Fri Dec 9 04:27:05 GMT 2011 | 0 | valid | 91024kb | alexk | 2.79 | 0:02.61 |
| regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 1 | 0 | 0 | 0 | 7 | SUCCESSFUL | 3 | 0 | 0 | 0.047 | 0.058 | 0 | 0 | 0 | 7.4e-05 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Fri Dec 9 04:27:09 GMT 2011 | 0 | valid | 49024kb | alexk | 0.13 | 0:00.13 |
| regression/symmetry_aware_threader_ready/01_inc/test | 77 | 0 | 6 | 1 | 0 | 1 | 163 | SUCCESSFUL | 3 | 0 | 0 | 0.192 | 0.328 | 0.979 | 0.007 | 0.004241 | 0.001553 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Fri Dec 9 04:27:10 GMT 2011 | 0 | valid | 46928kb | alexk | 1.62 | 0:01.52 |
| regression/symmetry_aware_threader_ready/02_inc_cas/test | 53 | 0 | 6 | 4 | 0 | 2 | 196 | SUCCESSFUL | 0 | 0 | 0 | 0.27 | 0.27 | 0.645 | 0.003 | 0.006609 | 0.001579 | 9 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Fri Dec 9 04:27:13 GMT 2011 | 0 | valid | 49008kb | alexk | 1.29 | 0:01.20 |
| regression/symmetry_aware_threader_ready/03_incdec/test | 118 | 0 | 10 | 2 | 0 | 2 | 987 | SUCCESSFUL | 7 | 0 | 0 | 0.784 | 1.098 | 3.241 | 0.014 | 0.022965 | 0.011378 | 17 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Fri Dec 9 04:27:15 GMT 2011 | 0 | valid | 55440kb | alexk | 5.71 | 0:05.16 |
| regression/symmetry_aware_threader_ready/04_incdec_cas/test | 10071 | 0 | 17 | 8 | 0 | 4 | 7619 | SUCCESSFUL | 2 | 0 | 0 | 1.215 | 10.777 | 5.996 | 0.024 | 4.69831 | 0.085802 | 83 | 12 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Fri Dec 9 04:27:21 GMT 2011 | 0 | valid | 128992kb | alexk | 23.82 | 0:18.06 |
| regression/symmetry_aware_threader_ready/05_tas/test | 44 | 0 | 3 | 1 | 0 | 1 | 62 | SUCCESSFUL | 4 | 0 | 0 | 0.027 | 0.156 | 0.02 | 0.001 | 0.002194 | 0.000583 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Fri Dec 9 04:27:40 GMT 2011 | 0 | valid | 47392kb | alexk | 0.26 | 0:00.21 |
| regression/symmetry_aware_threader_ready/06_ticket/test | 10 | 0 | 2 | 2 | 0 | 2 | 104 | SUCCESSFUL | 5 | 0 | 0 | 1.232 | 0.174 | 0.023 | 0.003 | 0.001086 | 0.001144 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Fri Dec 9 04:27:42 GMT 2011 | 0 | valid | 48528kb | alexk | 1.47 | 0:01.44 |
| regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 3 | 8 | 0 | 0 | 209 | SUCCESSFUL | 3 | 0 | 0 | 1.107 | 0.128 | 0.588 | 0.008 | 0 | 0.0021 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Fri Dec 9 04:27:44 GMT 2011 | 0 | valid | 50384kb | alexk | 1.88 | 0:01.84 |
| regression/symmetry_aware_threader_ready/08_rand_cas/test | 46594 | 0 | 15 | 15 | 0 | 1 | 10285 | SUCCESSFUL | 2 | 0 | 0 | 4.974 | 54.368 | 43.853 | 0.04 | 32.8304 | 0.147967 | 60 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Fri Dec 9 04:27:47 GMT 2011 | 0 | valid | 361168kb | alexk | 126.21 | 1:43.28 |
| regression/symmetry_aware_threader_ready/09_fmaxsym/test | 74 | 0 | 3 | 6 | 0 | 7 | 390 | SUCCESSFUL | 2 | 0 | 0 | 9.551 | 0.323 | 0.338 | 0.034 | 0.042288 | 0.003314 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Fri Dec 9 04:29:31 GMT 2011 | 0 | valid | 61056kb | alexk | 10.35 | 0:10.26 |
| regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 618 | 0 | 10 | 2 | 0 | 4 | 1930 | SUCCESSFUL | 0 | 0 | 0 | 0.369 | 1.142 | 0.692 | 0.071 | 0.069366 | 0.016873 | 31 | 6 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Fri Dec 9 04:29:43 GMT 2011 | 0 | valid | 75056kb | alexk | 2.55 | 0:02.28 |
| regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 74 | 0 | 3 | 2 | 0 | 1 | 567 | SUCCESSFUL | 2 | 0 | 0 | 0.211 | 0.192 | 0.207 | 0.021 | 0.002764 | 0.003724 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Fri Dec 9 04:29:46 GMT 2011 | 0 | valid | 49968kb | alexk | 0.69 | 0:00.64 |
| regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 1577 | 0 | 9 | 3 | 0 | 4 | 2136 | SUCCESSFUL | 0 | 0 | 0 | 0.464 | 1.152 | 1.077 | 0.069 | 0.196792 | 0.016775 | 24 | 5 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Fri Dec 9 04:29:48 GMT 2011 | 0 | valid | 67200kb | alexk | 3.06 | 0:02.77 |
| regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 4 | 6 | 0 | 0 | 4522 | SUCCESSFUL | 6 | 0 | 0 | 0.029 | 0.415 | 0.086 | 0.007 | 0 | 0.034052 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 04:29:52 GMT 2011 | 0 | valid | 106336kb | alexk | 0.59 | 0:00.54 |
| regression/symmetry_aware_threader_ready/14_stack_cas/test | 387 | 0 | 5 | 6 | 0 | 1 | 3904 | SUCCESSFUL | 4 | 0 | 0 | 0.036 | 0.604 | 0.124 | 0.008 | 0.03901 | 0.029009 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Fri Dec 9 04:29:53 GMT 2011 | 0 | valid | 104704kb | alexk | 0.89 | 0:00.78 |
| regression/symmetry_aware_threader_ready/15_unverif/test | 21 | 0 | 2 | 0 | 0 | 2 | 49 | SUCCESSFUL | 3 | 0 | 0 | 0.073 | 0.081 | 0.011 | 0.001 | 0.000724 | 0.000296 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:21 GMT 2011 | 0 | valid | 46672kb | alexk | 0.20 | 0:00.17 |