| * satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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 | 42 | SUCCESSFUL | 3 | 0 | 0 | 0.002 | 0.068 | 0.006 | 0.001 | 0 | 0.000265 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Fri Dec 9 04:29:55 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.006 | 0.086 | 0.008 | 0 | 0 | 0.000681 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Fri Dec 9 04:29:57 GMT 2011 | 0 | valid | 46784kb | alexk | 0.13 | 0:00.10 |
| regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 75 | SUCCESSFUL | 6 | 0 | 0 | 0.004 | 0.097 | 0.008 | 0.001 | 0 | 0.000467 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Fri Dec 9 04:29:58 GMT 2011 | 0 | valid | 46480kb | alexk | 0.10 | 0:00.11 |
| regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.012 | 0.14 | 0.012 | 0.001 | 0 | 0.003018 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Fri Dec 9 04:29:59 GMT 2011 | 0 | valid | 52048kb | alexk | 0.19 | 0:00.17 |
| regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 4 | 0 | 0 | 0 | 75 | SUCCESSFUL | 7 | 0 | 0 | 0.011 | 0.207 | 0.03 | 0.002 | 0 | 0.000637 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:30:00 GMT 2011 | 0 | valid | 58976kb | alexk | 0.35 | 0:00.25 |
| regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.01 | 0.101 | 0.007 | 0.001 | 0 | 0.000459 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:30:01 GMT 2011 | 0 | valid | 46736kb | alexk | 0.20 | 0:00.12 |
| regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 22 | 0 | 0 | 0 | 2308 | SUCCESSFUL | 24 | 0 | 0 | 2.009 | 3.721 | 3.474 | 0.016 | 0 | 0.03256 | 51 | 18 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Fri Dec 9 04:30:03 GMT 2011 | 0 | valid | 53856kb | alexk | 11.37 | 0:09.24 |
| regression/symmetry_aware_cav12threader/08_bakery/test | 108295 | 0 | 21 | 7 | 0 | 4 | 5177 | SUCCESSFUL | 17 | 0 | 0 | 2.315 | 59.577 | 7.399 | 0.015 | 23.0081 | 0.071757 | 94 | 16 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Fri Dec 9 04:30:13 GMT 2011 | 0 | valid | 228848kb | alexk | 77.92 | 1:09.33 |
| regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.017 | 0.361 | 0.15 | 0.003 | 0 | 0.009779 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Fri Dec 9 04:31:23 GMT 2011 | 0 | valid | 51152kb | alexk | 0.65 | 0:00.54 |
| regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 3.258 | 6.037 | 1.361 | 0.011 | 1.67673 | 0.092261 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Fri Dec 9 04:31:25 GMT 2011 | 0 | valid | 169136kb | alexk | 13.29 | 0:10.69 |
| regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 3.264 | 5.945 | 1.353 | 0.011 | 1.65867 | 0.090471 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Fri Dec 9 04:31:37 GMT 2011 | 0 | valid | 169136kb | alexk | 13.37 | 0:10.59 |
| regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 3.302 | 6.452 | 1.419 | 0.012 | 1.71034 | 0.090646 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Fri Dec 9 04:31:48 GMT 2011 | 0 | valid | 170032kb | alexk | 14.28 | 0:11.21 |
| regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.009 | 0.109 | 0.01 | 0 | 0 | 0.000254 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:32:01 GMT 2011 | 0 | valid | 46912kb | alexk | 0.12 | 0:00.13 |
| regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | 141833 | SUCCESSFUL | 0 | 0 | 0 | 1.155 | 26.383 | 0.034 | 0.002 | 0 | 3.04433 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Fri Dec 9 04:32:02 GMT 2011 | 0 | valid | 2038400kb | alexk | 27.99 | 0:27.59 |
| regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 6 | 9 | 0 | 0 | 1915 | SUCCESSFUL | 5 | 0 | 0 | 0.162 | 0.928 | 0.671 | 0.013 | 0 | 0.021484 | 6 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Fri Dec 9 04:32:30 GMT 2011 | 0 | valid | 70768kb | alexk | 2.17 | 0:01.81 |
| regression/symmetry_aware_threader_ready/01_inc/test | 147 | 0 | 6 | 1 | 0 | 1 | 229 | SUCCESSFUL | 3 | 0 | 0 | 0.181 | 0.376 | 0.869 | 0.004 | 0.0112 | 0.002365 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Fri Dec 9 04:32:33 GMT 2011 | 0 | valid | 50336kb | alexk | 1.51 | 0:01.44 |
| regression/symmetry_aware_threader_ready/02_inc_cas/test | 104 | 0 | 6 | 4 | 0 | 2 | 417 | SUCCESSFUL | 0 | 0 | 0 | 0.284 | 0.375 | 0.618 | 0.005 | 0.030162 | 0.004108 | 9 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:32:36 GMT 2011 | 0 | valid | 60432kb | alexk | 1.38 | 0:01.29 |
| regression/symmetry_aware_threader_ready/03_incdec/test | 187 | 0 | 10 | 2 | 0 | 2 | 1598 | SUCCESSFUL | 7 | 0 | 0 | 0.734 | 1.378 | 2.913 | 0.013 | 0.099971 | 0.021284 | 17 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Fri Dec 9 04:32:38 GMT 2011 | 0 | valid | 85104kb | alexk | 5.63 | 0:05.06 |
| regression/symmetry_aware_threader_ready/04_incdec_cas/test | 37702 | 0 | 17 | 8 | 0 | 4 | 11241 | SUCCESSFUL | 2 | 0 | 0 | 0.957 | 43.338 | 3.748 | 0.015 | 24.9049 | 0.09584 | 83 | 12 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:32:44 GMT 2011 | 0 | valid | 1436304kb | alexk | 52.06 | 0:48.09 |
| regression/symmetry_aware_threader_ready/05_tas/test | 288 | 0 | 3 | 1 | 0 | 1 | 377 | SUCCESSFUL | 4 | 0 | 0 | 0.029 | 0.277 | 0.022 | 0 | 0.025154 | 0.004357 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Fri Dec 9 04:33:34 GMT 2011 | 0 | valid | 64048kb | alexk | 0.42 | 0:00.33 |
| regression/symmetry_aware_threader_ready/06_ticket/test | 1317 | 0 | 8 | 2 | 0 | 5 | 16984 | SUCCESSFUL | 9 | 0 | 0 | 5.092 | 9.232 | 3.628 | 0.069 | 4.44972 | 0.206527 | 7 | 5 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Fri Dec 9 04:33:35 GMT 2011 | 0 | valid | 227248kb | alexk | 19.88 | 0:18.03 |
| regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 3 | 8 | 0 | 0 | 1344 | SUCCESSFUL | 3 | 0 | 0 | 1.041 | 0.264 | 0.517 | 0.006 | 0 | 0.013216 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Fri Dec 9 04:33:54 GMT 2011 | 0 | valid | 79536kb | alexk | 1.82 | 0:01.84 |
| regression/symmetry_aware_threader_ready/08_rand_cas/test | 316532 | 0 | 15 | 15 | 0 | 1 | 68033 | SUCCESSFUL | 2 | 0 | 0 | 4.476 | 798.326 | 30.773 | 0.04 | 414.742 | 1.28644 | 60 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:33:57 GMT 2011 | 0 | valid | 7365888kb | alexk | 850.26 | 13:53.65 |
| regression/symmetry_aware_threader_ready/09_fmaxsym/test | 408 | 0 | 3 | 6 | 0 | 7 | 3762 | SUCCESSFUL | 2 | 0 | 0 | 9.862 | 2.521 | 0.284 | 0.031 | 1.6832 | 0.052499 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Fri Dec 9 04:47:52 GMT 2011 | 0 | valid | 185936kb | alexk | 13.20 | 0:12.71 |
| regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 10224 | 0 | 10 | 2 | 0 | 4 | 2867 | SUCCESSFUL | 0 | 0 | 0 | 0.582 | 21.075 | 1.094 | 0.118 | 13.6828 | 0.029097 | 31 | 6 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:48:06 GMT 2011 | 0 | valid | 418912kb | alexk | 24.26 | 0:22.88 |
| regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 351 | 0 | 3 | 2 | 0 | 1 | 4719 | SUCCESSFUL | 2 | 0 | 0 | 0.344 | 0.742 | 0.342 | 0.036 | 0.034648 | 0.04591 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Fri Dec 9 04:48:29 GMT 2011 | 0 | valid | 105680kb | alexk | 1.49 | 0:01.48 |
| regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 74365 | 0 | 11 | 3 | 0 | 4 | 2874 | SUCCESSFUL | 0 | 0 | 0 | 0.76 | 86.644 | 3.341 | 0.168 | 42.0492 | 0.027341 | 45 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:48:32 GMT 2011 | 0 | valid | 1388928kb | alexk | 91.51 | 1:30.93 |
| regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 4 | 6 | 0 | 0 | 125207 | SUCCESSFUL | 6 | 0 | 0 | 0.052 | 17.116 | 0.147 | 0.011 | 0 | 1.56088 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --abstractor cartesian --max-cube-length 1 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Fri Dec 9 04:50:04 GMT 2011 | 0 | valid | 1689760kb | alexk | 17.38 | 0:17.34 |
| regression/symmetry_aware_threader_ready/14_stack_cas/test | 9024 | 0 | 5 | 6 | 0 | 1 | 105283 | SUCCESSFUL | 4 | 0 | 0 | 0.055 | 20.382 | 0.191 | 0.013 | 2.86349 | 1.30421 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:50:23 GMT 2011 | 0 | valid | 1665504kb | alexk | 21.01 | 0:20.65 |
| regression/symmetry_aware_threader_ready/15_unverif/test | 82 | 0 | 2 | 0 | 0 | 2 | 298 | SUCCESSFUL | 3 | 0 | 0 | 0.072 | 0.124 | 0.011 | 0 | 0.005291 | 0.001876 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 --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:23 GMT 2011 | 0 | valid | 50864kb | alexk | 0.24 | 0:00.21 |