* /nas/mictau/SVNS/cbmc-r2030+concurrency
--unwind 2 --partial-loops version 4.2 results * Timeout: - Memory limit: unlimitedkb Thu May 23 06:47:40 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_hw_m32_prop1_prop2 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops ../ethoc_hw_m32_prop1_prop2.gb | Thu May 23 06:44:20 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 171888kb | 8 | 2 | 25 | 9 | 9 | 9 | 1 | 27 | 4 | 1036 | 1.444 | mictau | 1.66 | 0:01.72 | |||
ethoc_hw_m32_prop1_prop3 | Property VIOLATED | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops ../ethoc_hw_m32_prop1_prop3.gb | Thu May 23 06:44:23 BST 2013 | MiniSAT2 with simplifier | 10 | unknown | 2448316kb | 184 | 116 | 18 | 8 | 73 | 135 | 37 | 37 | 12 | 86 | 249 | 220 | 4633 | 45.216 | mictau | 46.14 | 0:47.15 |
ethoc_hw_m32_prop1_prop4 | Property HOLDS | /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops ../ethoc_hw_m32_prop1_prop4.gb | Thu May 23 06:45:12 BST 2013 | MiniSAT2 with simplifier | 0 | unknown | 4023552kb | 343 | 169 | 24 | 7 | 90 | 173 | 48 | 48 | 16 | 107 | 109 | 304 | 6073 | 144.265 | mictau | 145.68 | 2:27.37 |
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 (**).