| * /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions version 4.2 results * Timeout: - Memory limit: unlimitedkb Thu May 23 02:17:41 2013 |
||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Benchmark | Result | commandline | date | dec-procedure | exitcode | expected | maxmem | mt_atomic-block (**) | mt_fr (**) | mt_max_per_address | mt_num_unique_addresses | mt_po (**) | mt_rf (**) | mt_rf-at-least-one (**) | mt_rfi (**) | mt_thread-spawn (*) (**) | mt_tot_subevent_count | mt_ws (**) | mt_ws-preceding (**) | ssa-size | time_dec_proc | user | usertime | wallclock |
| ethoc_sw_hw_m32_prop5 | Property VIOLATED | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions ../ethoc_sw_hw_m32_prop5.gb | Thu May 23 01:39:43 BST 2013 | MiniSAT2 with simplifier | 10 | unknown | 38641760kb | 278 | 6335 | 179 | 13 | 541 | 10781 | 407 | 407 | 18 | 560 | 1397 | 827 | 16707 | 1673.46 | mictau | 1680.67 | 28:19.74 |
| ethoc_sw_hw_m32_prop6 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions ../ethoc_sw_hw_m32_prop6.gb | Thu May 23 02:08:04 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 30618848kb | 277 | 6331 | 181 | 13 | 543 | 10823 | 409 | 409 | 18 | 562 | 1397 | 827 | 16683 | 324.25 | mictau | 335.51 | 5:46.00 |
| ethoc_sw_hw_m32_prop7 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions ../ethoc_sw_hw_m32_prop7.gb | Thu May 23 02:13:51 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 29000892kb | 277 | 6217 | 178 | 13 | 536 | 10674 | 402 | 402 | 18 | 555 | 1397 | 827 | 16635 | 208.367 | mictau | 219.50 | 3:48.87 |
| ethoc_sw_hw_m32_sequential_prop5 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions ../ethoc_sw_hw_m32_sequential_prop5.gb | Thu May 23 01:17:59 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 8917856kb | 17710 | 422.208 | mictau | 426.76 | 7:11.03 | ||||||||||||
| ethoc_sw_hw_m32_sequential_prop6 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions ../ethoc_sw_hw_m32_sequential_prop6.gb | Thu May 23 01:25:11 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 8844800kb | 17686 | 421.74 | mictau | 426.14 | 7:10.54 | ||||||||||||
| ethoc_sw_hw_m32_sequential_prop7 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 1 --partial-loops --no-unwinding-assertions ../ethoc_sw_hw_m32_sequential_prop7.gb | Thu May 23 01:32:23 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 8751412kb | 17648 | 431.17 | mictau | 435.32 | 7:19.82 | ||||||||||||
The benchmarks were run on a Linux 3.5.0-26-generic 8x Intel(R) Xeon(R) CPU X5667 (3.07GHz) system equipped with 49453040kb RAM.
(*) This is the total number of extra threads spawned in addition to the
main thread. In the paper we report that total number, i.e.,
mt_thread-spawn + 1.
(**) The number of concurrency constraints reported in the paper is the sum
of all columns marked (**).