BENCHMARK INFORMATION benchmark definition: /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/ourtool-validate-write+lock-tmp.xml name: ourtool-validate-write+lock-tmp run sets: protection-read.Pthread, mine.Pthread, write+lock.Pthread date: Tue, 2023-01-31 09:03:51 UTC tool: Goblint heads/yaml-witness-unassume-bench-0-g353653ad6-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 write+lock --witness.yaml.unassume '/mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/${rundefinition_name}/${taskdef_name}/witness.yml' --witness.yaml.validate '/mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/write+lock/${taskdef_name}/witness.yml' 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-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 write+lock --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/write+lock/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 2.95 2.95 None pthread/ctrace_comb.yml unknown 4.55 4.55 None pthread/knot_comb.yml unknown 8.31 8.31 None pthread/pfscan_comb.yml unknown 2.01 2.01 None pthread/smtprc_comb.yml ERROR (3) 20.09 20.16 None pthread/ypbind_comb.yml unknown 43.43 43.45 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 15.57 15.57 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 17.92 17.93 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 6.59 6.60 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 39.34 39.36 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 41.62 41.63 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 263.61 61.34 - 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 write+lock --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/write+lock/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 2.78 2.78 None pthread/ctrace_comb.yml unknown 4.58 4.58 None pthread/knot_comb.yml unknown 7.89 7.89 None pthread/pfscan_comb.yml unknown 2.35 2.36 None pthread/smtprc_comb.yml ERROR (3) 20.27 20.39 None pthread/ypbind_comb.yml EXCEPTION (Failure) 0.11 0.12 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml EXCEPTION (Failure) 0.18 0.18 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 15.36 15.37 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 17.51 17.55 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 6.28 6.29 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 38.16 38.18 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 41.41 41.43 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 2 done 157.13 41.93 - 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 write+lock --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/${rundefinition_name}/${taskdef_name}/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/write+lock/${taskdef_name}/witness.yml' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------- pthread/aget_comb.yml unknown 2.95 2.95 None pthread/ctrace_comb.yml unknown 4.62 4.62 None pthread/knot_comb.yml unknown 9.01 9.01 None pthread/pfscan_comb.yml unknown 3.02 3.02 None pthread/smtprc_comb.yml ERROR (3) 20.02 20.04 None pthread/ypbind_comb.yml unknown 42.98 42.99 None svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.yml EXCEPTION (Failure) 0.23 0.24 None svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.yml unknown 14.93 14.94 None svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.yml unknown 18.24 18.26 None svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.yml unknown 6.18 6.18 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.yml unknown 37.87 37.90 None svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.yml unknown 41.43 41.44 None -------------------------------------------------------------------------------------------------------------------------------------------------- Run set 3 done 201.73 43.35 - Statistics: 36 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 36