BENCHMARK INFORMATION benchmark definition: /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/ourtool.xml name: ourtool run sets: protection-read.Pthread, mine.Pthread, write+lock.Pthread date: Thu, 2023-02-02 12:32:27 UTC tool: Goblint heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty tool executable: ./goblint options: --conf conf/bench-yaml.json --enable dbg.timing.enabled --enable witness.invariant.loop-head --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.accessed parallel runs: 4 resource limits: - memory: 6000.0 MB - time: 900 s - cpu cores: 1 hardware requirements: - cpu cores: 1 - memory: 6000.0 MB ------------------------------------------------------------ SYSTEM INFORMATION host: goblint-new os: Linux-5.15.0-52-generic-x86_64-with-glibc2.35 cpu: AMD EPYC Processor (with IBPB) - cores: 16 - max frequency: 2250.0 MHz ram: 33662.087168 MB ------------------------------------------------------------ protection-read.Pthread Run set 1 of 3 with options '--conf conf/bench-yaml.json --enable dbg.timing.enabled --enable witness.invariant.loop-head --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.accessed --ana.base.privatization protection-read' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 1.94 3.35 None pthread/ctrace_comb.yml unknown 2.48 3.90 None pthread/knot_comb.yml unknown 4.68 6.07 None pthread/pfscan_comb.yml unknown 0.94 2.35 None pthread/smtprc_comb.yml unknown 14.98 15.03 None pthread/ypbind_comb.yml unknown 24.87 24.88 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml unknown 16.77 16.79 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 10.20 10.27 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 12.97 12.99 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 3.67 3.68 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 12.60 12.61 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 12.67 12.67 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 119.01 34.60 - mine.Pthread Run set 2 of 3 with options '--conf conf/bench-yaml.json --enable dbg.timing.enabled --enable witness.invariant.loop-head --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.accessed --ana.base.privatization mine' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 3.87 3.87 None pthread/ctrace_comb.yml unknown 4.35 4.35 None pthread/knot_comb.yml unknown 5.68 5.70 None pthread/pfscan_comb.yml unknown 2.18 2.18 None pthread/smtprc_comb.yml unknown 30.34 30.34 None pthread/ypbind_comb.yml unknown 80.28 80.30 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml TIMEOUT 901.00 901.11 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 29.04 29.05 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 33.21 33.22 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 7.32 7.32 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 41.76 41.76 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 48.36 48.37 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 2 done 1187.62 905.85 - write+lock.Pthread Run set 3 of 3 with options '--conf conf/bench-yaml.json --enable dbg.timing.enabled --enable witness.invariant.loop-head --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.accessed --ana.base.privatization write+lock' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 3.22 3.22 None pthread/ctrace_comb.yml unknown 3.66 3.66 None pthread/knot_comb.yml unknown 9.64 9.65 None pthread/pfscan_comb.yml unknown 1.80 1.80 None pthread/smtprc_comb.yml unknown 25.93 25.94 None pthread/ypbind_comb.yml unknown 55.94 55.95 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml TIMEOUT 901.05 901.16 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 16.31 16.31 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 19.40 19.41 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 5.86 5.86 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 41.57 41.58 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 45.19 45.19 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 3 done 1129.83 905.27 - Statistics: 36 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 36