| * satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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 | 30 | SUCCESSFUL | 3 | 0 | 0 | 0.005 | 0.064 | 0.01 | 0.001 | 0 | 0.000244 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Fri Dec 9 00:30:10 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.008 | 0.094 | 0.012 | 0.001 | 0 | 0.001135 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Fri Dec 9 00:30:11 GMT 2011 | 0 | valid | 46784kb | alexk | 0.09 | 0:00.12 |
| regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 75 | SUCCESSFUL | 6 | 0 | 0 | 0.006 | 0.081 | 0.014 | 0 | 0 | 0.000627 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Fri Dec 9 00:30:12 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.019 | 0.129 | 0.019 | 0.001 | 0 | 0.004141 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Fri Dec 9 00:30:13 GMT 2011 | 0 | valid | 52048kb | alexk | 0.15 | 0:00.17 |
| regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 4 | 0 | 0 | 0 | 101 | SUCCESSFUL | 7 | 0 | 0 | 0.034 | 0.215 | 0.044 | 0.003 | 0 | 0.001119 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:30:14 GMT 2011 | 0 | valid | 55904kb | alexk | 0.39 | 0:00.30 |
| regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.03 | 0.1 | 0.011 | 0.001 | 0 | 0.000686 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:30:16 GMT 2011 | 0 | valid | 46800kb | alexk | 0.16 | 0:00.15 |
| regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 13 | 0 | 0 | 0 | 1199 | SUCCESSFUL | 24 | 0 | 0 | 37.559 | 3.649 | 3.013 | 0.011 | 0 | 0.017154 | 17 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Fri Dec 9 00:30:17 GMT 2011 | 0 | valid | 58496kb | alexk | 46.66 | 0:44.27 |
| regression/symmetry_aware_cav12threader/08_bakery/test | 49863 | 0 | 18 | 7 | 0 | 4 | 5116 | SUCCESSFUL | 17 | 0 | 0 | 60.982 | 30.635 | 9.904 | 0.026 | 14.5158 | 0.059235 | 60 | 13 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Fri Dec 9 00:31:02 GMT 2011 | 0 | valid | 197264kb | alexk | 111.53 | 1:41.60 |
| regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.029 | 0.373 | 0.244 | 0.004 | 0 | 0.011005 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Fri Dec 9 00:32:45 GMT 2011 | 0 | valid | 50976kb | alexk | 0.73 | 0:00.66 |
| regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 69.869 | 7.476 | 2.201 | 0.016 | 2.18826 | 0.120182 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Fri Dec 9 00:32:47 GMT 2011 | 0 | valid | 169136kb | alexk | 82.58 | 1:19.61 |
| regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 50.455 | 7.671 | 2.189 | 0.018 | 2.17292 | 0.125476 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Fri Dec 9 00:34:08 GMT 2011 | 0 | valid | 169136kb | alexk | 63.78 | 1:00.38 |
| regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 44.556 | 6.587 | 1.444 | 0.012 | 1.75634 | 0.09506 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Fri Dec 9 00:35:09 GMT 2011 | 0 | valid | 170032kb | alexk | 55.50 | 0:52.63 |
| regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.008 | 0.09 | 0.011 | 0.001 | 0 | 0.000289 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:36:03 GMT 2011 | 0 | valid | 46912kb | alexk | 0.09 | 0:00.11 |
| regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | 2756 | SUCCESSFUL | 0 | 0 | 0 | 4.992 | 0.505 | 0.035 | 0.003 | 0 | 0.021114 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Fri Dec 9 00:36:04 GMT 2011 | 0 | valid | 90912kb | alexk | 5.66 | 0:05.55 |
| regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 1 | 0 | 0 | 0 | 7 | SUCCESSFUL | 3 | 0 | 0 | 0.03 | 0.043 | 0 | 0 | 0 | 5.7e-05 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Fri Dec 9 00:36:10 GMT 2011 | 0 | valid | 49024kb | alexk | 0.09 | 0:00.08 |
| regression/symmetry_aware_threader_ready/01_inc/test | 77 | 0 | 6 | 1 | 0 | 1 | 163 | SUCCESSFUL | 3 | 0 | 0 | 0.488 | 0.307 | 0.609 | 0.005 | 0.004109 | 0.001546 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Fri Dec 9 00:36:12 GMT 2011 | 0 | valid | 47008kb | alexk | 1.36 | 0:01.42 |
| regression/symmetry_aware_threader_ready/02_inc_cas/test | 177 | 0 | 7 | 4 | 0 | 2 | 187 | SUCCESSFUL | 0 | 0 | 0 | 1.446 | 0.401 | 0.625 | 0.005 | 0.018042 | 0.001645 | 15 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:36:14 GMT 2011 | 0 | valid | 59344kb | alexk | 2.53 | 0:02.48 |
| regression/symmetry_aware_threader_ready/03_incdec/test | 118 | 0 | 10 | 2 | 0 | 2 | 987 | SUCCESSFUL | 7 | 0 | 0 | 3.686 | 1.098 | 2.081 | 0.008 | 0.024091 | 0.012056 | 17 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Fri Dec 9 00:36:18 GMT 2011 | 0 | valid | 55968kb | alexk | 7.29 | 0:06.89 |
| regression/symmetry_aware_threader_ready/04_incdec_cas/test | 8793 | 0 | 18 | 8 | 0 | 4 | 4583 | SUCCESSFUL | 2 | 0 | 0 | 7.751 | 6.963 | 4.409 | 0.018 | 2.94361 | 0.045783 | 84 | 13 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:36:26 GMT 2011 | 0 | valid | 108288kb | alexk | 23.04 | 0:19.17 |
| regression/symmetry_aware_threader_ready/05_tas/test | 42 | 0 | 2 | 1 | 0 | 1 | 58 | SUCCESSFUL | 4 | 0 | 0 | 0.049 | 0.121 | 0.009 | 0 | 0.001907 | 0.00065 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Fri Dec 9 00:36:46 GMT 2011 | 0 | valid | 47456kb | alexk | 0.23 | 0:00.18 |
| regression/symmetry_aware_threader_ready/06_ticket/test | 11 | 0 | 2 | 2 | 0 | 2 | 104 | SUCCESSFUL | 5 | 0 | 0 | 3.907 | 0.132 | 0.015 | 0.002 | 0.001092 | 0.001129 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Fri Dec 9 00:36:47 GMT 2011 | 0 | valid | 48912kb | alexk | 4.05 | 0:04.06 |
| regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 3 | 8 | 0 | 0 | 209 | SUCCESSFUL | 3 | 0 | 0 | 3.433 | 0.104 | 0.372 | 0.004 | 0 | 0.001593 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Fri Dec 9 00:36:52 GMT 2011 | 0 | valid | 49968kb | alexk | 3.94 | 0:03.92 |
| regression/symmetry_aware_threader_ready/08_rand_cas/test | 18288 | 0 | 13 | 15 | 0 | 1 | 7144 | SUCCESSFUL | 2 | 0 | 0 | 25.719 | 21.6 | 21.825 | 0.025 | 15.6516 | 0.072202 | 42 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:36:57 GMT 2011 | 0 | valid | 201120kb | alexk | 75.85 | 1:09.19 |
| regression/symmetry_aware_threader_ready/09_fmaxsym/test | 61 | 0 | 2 | 6 | 0 | 7 | 379 | SUCCESSFUL | 2 | 0 | 0 | 114.524 | 0.295 | 0.256 | 0.012 | 0.083488 | 0.003533 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Fri Dec 9 00:38:07 GMT 2011 | 0 | valid | 68416kb | alexk | 114.89 | 1:55.10 |
| regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 354 | 0 | 7 | 2 | 0 | 4 | 2214 | SUCCESSFUL | 0 | 0 | 0 | 3.396 | 1.074 | 0.48 | 0.047 | 0.053316 | 0.015901 | 13 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Fri Dec 9 00:40:04 GMT 2011 | 0 | valid | 104448kb | alexk | 5.18 | 0:05.01 |
| regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 52 | 0 | 2 | 2 | 0 | 1 | 447 | SUCCESSFUL | 2 | 0 | 0 | 0.435 | 0.138 | 0.159 | 0.01 | 0.002074 | 0.002712 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Fri Dec 9 00:40:10 GMT 2011 | 0 | valid | 50048kb | alexk | 0.79 | 0:00.75 |
| regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 400 | 0 | 6 | 3 | 0 | 4 | 1443 | SUCCESSFUL | 0 | 0 | 0 | 4.672 | 0.624 | 0.682 | 0.038 | 0.050903 | 0.012908 | 5 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Fri Dec 9 00:40:12 GMT 2011 | 0 | valid | 64400kb | alexk | 6.15 | 0:06.02 |
| regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 4 | 6 | 0 | 0 | 4522 | SUCCESSFUL | 6 | 0 | 0 | 0.03 | 0.421 | 0.086 | 0.005 | 0 | 0.034333 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 00:40:19 GMT 2011 | 0 | valid | 106320kb | alexk | 0.65 | 0:00.55 |
| regression/symmetry_aware_threader_ready/14_stack_cas/test | 334 | 0 | 4 | 6 | 0 | 1 | 3493 | SUCCESSFUL | 4 | 0 | 0 | 0.063 | 0.431 | 0.082 | 0.007 | 0.034685 | 0.023788 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --abstractor cartesian --max-cube-length 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Fri Dec 9 00:40:20 GMT 2011 | 0 | valid | 104816kb | alexk | 0.67 | 0:00.59 |
| regression/symmetry_aware_threader_ready/15_unverif/test | 21 | 0 | 2 | 0 | 0 | 2 | 49 | SUCCESSFUL | 3 | 0 | 0 | 0.285 | 0.094 | 0.012 | 0 | 0.000642 | 0.00029 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 --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:13 GMT 2011 | 0 | valid | 46704kb | alexk | 0.43 | 0:00.40 |