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: Tue, 2023-01-31 08:56:44 UTC tool: Goblint heads/yaml-witness-unassume-bench-0-g353653ad6-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: 14 resource limits: - memory: 1000.0 MB - time: 60 s - cpu cores: 1 hardware requirements: - cpu cores: 1 - memory: 1000.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 2.04 2.04 None pthread/ctrace_comb.yml unknown 2.52 2.53 None pthread/knot_comb.yml unknown 4.78 4.81 None pthread/pfscan_comb.yml unknown 0.89 0.90 None pthread/smtprc_comb.yml unknown 15.38 15.39 None pthread/ypbind_comb.yml unknown 25.93 25.93 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml unknown 18.95 18.96 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 10.33 10.34 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 12.42 12.43 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 4.19 4.19 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 14.36 14.39 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 14.78 14.80 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 126.82 26.27 - 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 4.16 4.17 None pthread/ctrace_comb.yml unknown 4.87 4.87 None pthread/knot_comb.yml unknown 5.98 5.99 None pthread/pfscan_comb.yml unknown 2.40 2.40 None pthread/smtprc_comb.yml unknown 30.96 30.97 None pthread/ypbind_comb.yml TIMEOUT 61.02 61.03 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml TIMEOUT 61.02 61.03 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 29.32 29.32 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 34.24 34.25 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 7.39 7.40 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 42.25 42.28 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 50.24 50.27 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 2 done 334.10 61.35 - 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.34 3.34 None pthread/ctrace_comb.yml unknown 3.77 3.77 None pthread/knot_comb.yml unknown 9.70 9.71 None pthread/pfscan_comb.yml unknown 1.87 1.87 None pthread/smtprc_comb.yml unknown 26.11 26.12 None pthread/ypbind_comb.yml unknown 53.75 53.76 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml TIMEOUT 61.01 61.02 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 16.08 16.09 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 18.56 18.57 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 6.06 6.07 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 41.04 41.06 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 43.32 43.36 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 3 done 284.86 61.49 - Statistics: 36 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 36