BENCHMARK INFORMATION benchmark definition: /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/ourtool-validate-protection-read-tmp.xml name: ourtool-validate-protection-read-tmp run sets: protection-read.Pthread, mine.Pthread, write+lock.Pthread date: Thu, 2023-02-02 13:03:13 UTC tool: Goblint heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty tool executable: ./goblint options: --conf conf/bench-yaml-validate.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 --witness.yaml.unassume '/mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/${rundefinition_name}/${taskdef_name}/witness.yml' --witness.yaml.validate '/mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/protection-read/${taskdef_name}/witness.yml' 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-validate.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 --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/protection-read/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 1.90 1.91 None pthread/ctrace_comb.yml unknown 3.19 3.20 None pthread/knot_comb.yml unknown 4.30 4.30 None pthread/pfscan_comb.yml unknown 0.91 0.91 None pthread/smtprc_comb.yml ERROR (3) 12.34 12.35 None pthread/ypbind_comb.yml unknown 22.13 22.13 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml unknown 16.78 16.79 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 9.97 9.97 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 12.84 12.87 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 3.85 3.86 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 12.31 12.32 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 12.47 12.48 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 113.23 33.11 - mine.Pthread Run set 2 of 3 with options '--conf conf/bench-yaml-validate.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 --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/protection-read/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 1.97 1.97 None pthread/ctrace_comb.yml unknown 3.20 3.20 None pthread/knot_comb.yml unknown 4.31 4.31 None pthread/pfscan_comb.yml TIMEOUT 901.21 901.27 None pthread/smtprc_comb.yml ERROR (3) 12.25 12.25 None pthread/ypbind_comb.yml unknown 22.08 22.08 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml EXCEPTION (Failure) 0.15 0.15 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 10.02 10.02 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 12.68 12.69 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 3.80 3.80 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 12.39 12.40 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 12.41 12.42 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 2 done 996.73 901.52 - write+lock.Pthread Run set 3 of 3 with options '--conf conf/bench-yaml-validate.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 --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt-900/ourtool.2023-02-02_12-32-27.files/protection-read/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 1.96 1.96 None pthread/ctrace_comb.yml unknown 3.23 3.23 None pthread/knot_comb.yml unknown 4.31 4.32 None pthread/pfscan_comb.yml TIMEOUT 901.22 901.27 None pthread/smtprc_comb.yml ERROR (3) 12.36 12.36 None pthread/ypbind_comb.yml unknown 22.11 22.11 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml EXCEPTION (Failure) 0.16 0.16 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 10.10 10.10 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 12.70 12.70 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 3.80 3.81 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 12.30 12.30 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 12.50 12.50 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 3 done 996.98 901.55 - Statistics: 36 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 36