Skip to content

Commit f2dedc3

Browse files
sim642sim642
authored
Merge pull request #51 from goblint/thread-witnesses
Thread-modular witnesses benchmarking
2 parents 85f5cb1 + 7b3db36 commit f2dedc3

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+1770
-0
lines changed

‎thread-witnesses/.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
*-tmp.xml

‎thread-witnesses/README.md‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
# Thread-Modular Correctness Witnesses and their Validation
2+
## An Abstract Interpretation Perspective
3+
4+
### Layout
5+
* `autoactive/plain` — programs and GraphML witnesses from AutoActive artifact.
6+
* `autoactive/generated_yaml` — converted YAML witnesses.
7+
* `bench` — this repository.
8+
* `benchexec` — BenchExec version.
9+
* `CPAchecker-2.2-unix` — CPAchecker from SV-COMP 2023 archives.
10+
* `ourtool` — our tool, including source code. **NB! Although git authorship has been stripped, the contents of this directory do reveal the unanonymized tool name.**
11+
* `results` — results directory for scripts.
12+
* `sv-benchmarks` — SV-COMP 2022 benchmarks, at least ReachSafety-Loops.
13+
* `UAutomizer-linux` — Ultimate Automizer from SV-COMP 2023 archives.
14+
15+
### Scripts
16+
* `./st-same/run.sh` — single-threaded programs, same-framework.
17+
* `./st-cross/witnessToYaml.sh` — convert single-threaded cross-framework witnesses from GraphML to YAML (very slow!).
18+
* `./st-cross/run.sh` — single-threaded programs, cross-framework.
19+
* `./st-lit/run.sh` — single-threaded programs from literature.
20+
* `./mt/run.sh` — multi-threaded programs, same- and cross-framework.

‎thread-witnesses/mt/ourtool-validate-mine.xml‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
<?xml version="1.0"?>
2+
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
3+
<benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1">
4+
5+
<resultfiles></resultfiles>
6+
7+
<option name="--conf">conf/bench-yaml-validate.json</option>
8+
<option name="--enable">dbg.timing.enabled</option>
9+
10+
<!-- after-lock -->
11+
<option name="--enable">witness.invariant.loop-head</option>
12+
<option name="--enable">witness.invariant.after-lock</option>
13+
<option name="--disable">witness.invariant.other</option>
14+
<option name="--disable">witness.invariant.accessed</option>
15+
16+
<!-- validate2 -->
17+
<option name="--ana.base.privatization">mine</option>
18+
19+
<rundefinition name="protection-read">
20+
</rundefinition>
21+
22+
<rundefinition name="mine">
23+
</rundefinition>
24+
25+
<requiredfiles>RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</requiredfiles>
26+
<requiredfiles>RESULTSDIR/LOGDIR/mine/${taskdef_name}/witness.yml</requiredfiles>
27+
<option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</option>
28+
<option name="--witness.yaml.validate">RESULTSDIR/LOGDIR/mine/${taskdef_name}/witness.yml</option>
29+
30+
<tasks name="Pthread">
31+
<includesfile>../../Pthread.set</includesfile>
32+
<includesfile>../../SvComp-Pthread.set</includesfile>
33+
</tasks>
34+
35+
</benchmark>

‎thread-witnesses/mt/ourtool-validate-protection-read.xml‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
<?xml version="1.0"?>
2+
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
3+
<benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1">
4+
5+
<resultfiles></resultfiles>
6+
7+
<option name="--conf">conf/bench-yaml-validate.json</option>
8+
<option name="--enable">dbg.timing.enabled</option>
9+
10+
<!-- after-lock -->
11+
<option name="--enable">witness.invariant.loop-head</option>
12+
<option name="--enable">witness.invariant.after-lock</option>
13+
<option name="--disable">witness.invariant.other</option>
14+
<option name="--disable">witness.invariant.accessed</option>
15+
16+
<!-- validate1 -->
17+
<option name="--ana.base.privatization">protection-read</option>
18+
19+
<rundefinition name="protection-read">
20+
</rundefinition>
21+
22+
<rundefinition name="mine">
23+
</rundefinition>
24+
25+
<requiredfiles>RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</requiredfiles>
26+
<requiredfiles>RESULTSDIR/LOGDIR/protection-read/${taskdef_name}/witness.yml</requiredfiles>
27+
<option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</option>
28+
<option name="--witness.yaml.validate">RESULTSDIR/LOGDIR/protection-read/${taskdef_name}/witness.yml</option>
29+
30+
<tasks name="Pthread">
31+
<includesfile>../../Pthread.set</includesfile>
32+
<includesfile>../../SvComp-Pthread.set</includesfile>
33+
</tasks>
34+
35+
</benchmark>

‎thread-witnesses/mt/ourtool.xml‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
<?xml version="1.0"?>
2+
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
3+
<benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1">
4+
5+
<resultfiles>**.yml</resultfiles>
6+
7+
<option name="--conf">conf/bench-yaml.json</option>
8+
<option name="--enable">dbg.timing.enabled</option>
9+
10+
<!-- after-lock -->
11+
<option name="--enable">witness.invariant.loop-head</option>
12+
<option name="--enable">witness.invariant.after-lock</option>
13+
<option name="--disable">witness.invariant.other</option>
14+
<option name="--disable">witness.invariant.accessed</option>
15+
16+
<rundefinition name="protection-read">
17+
<option name="--ana.base.privatization">protection-read</option>
18+
</rundefinition>
19+
20+
<rundefinition name="mine">
21+
<option name="--ana.base.privatization">mine</option>
22+
</rundefinition>
23+
24+
<tasks name="Pthread">
25+
<includesfile>../../Pthread.set</includesfile>
26+
<includesfile>../../SvComp-Pthread.set</includesfile>
27+
</tasks>
28+
29+
</benchmark>

‎thread-witnesses/mt/run.sh‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#!/bin/bash
2+
3+
shopt -s extglob
4+
5+
MYBENCHDIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
6+
RESULTSDIR=$MYBENCHDIR/../../../results/mt
7+
OURTOOLPARALLEL=4
8+
VALIDATEPARALLEL=4
9+
10+
mkdir $RESULTSDIR
11+
12+
# Run verification
13+
cd $MYBENCHDIR/../../../ourtool
14+
# read-only and overlay dirs for Value too large for defined data type workaround
15+
benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $OURTOOLPARALLEL $MYBENCHDIR/ourtool.xml
16+
17+
# Extract witness directory
18+
cd $RESULTSDIR
19+
LOGDIR=`echo ourtool.*.files`
20+
echo $LOGDIR
21+
22+
# Construct validation XMLs
23+
cd $MYBENCHDIR
24+
sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" ourtool-validate-protection-read.xml > ourtool-validate-protection-read-tmp.xml
25+
sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" ourtool-validate-mine.xml > ourtool-validate-mine-tmp.xml
26+
27+
# Run validation
28+
cd $MYBENCHDIR/../../../ourtool
29+
benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/ourtool-validate-protection-read-tmp.xml
30+
benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/ourtool-validate-mine-tmp.xml
31+
32+
# Merge witness validation results
33+
cd $RESULTSDIR
34+
python3 $MYBENCHDIR/../../../benchexec/contrib/mergeBenchmarkSets.py -o . ourtool.*.results.protection-read.Pthread.xml.bz2 ourtool-validate-protection-read-tmp.*.results.protection-read.Pthread.xml.bz2 ourtool-validate-mine-tmp.*.results.protection-read.Pthread.xml.bz2
35+
python3 $MYBENCHDIR/../../../benchexec/contrib/mergeBenchmarkSets.py -o . ourtool.*.results.mine.Pthread.xml.bz2 ourtool-validate-protection-read-tmp.*.results.mine.Pthread.xml.bz2 ourtool-validate-mine-tmp.*.results.mine.Pthread.xml.bz2
36+
37+
# Generate table with merged results and witness validation results
38+
sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator.xml > table-generator.xml
39+
table-generator -x table-generator.xml
40+
41+
# Decompress all tool outputs for table HTML links
42+
unzip -o ourtool.*.logfiles.zip
43+
unzip -o ourtool-validate-protection-read-tmp.*.logfiles.zip
44+
unzip -o ourtool-validate-mine-tmp.*.logfiles.zip

‎thread-witnesses/mt/table-generator.xml‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
<?xml version="1.0" ?>
2+
<!DOCTYPE table PUBLIC "+//IDN sosy-lab.org//DTD BenchExec table 1.10//EN" "https://www.sosy-lab.org/benchexec/table-1.10.dtd">
3+
<table>
4+
5+
<result filename="ourtool.*.results.protection-read.Pthread.xml.bz2.merged.xml.bz2">
6+
<column title="status"/>
7+
<!-- <column title="score"/> -->
8+
<column title="witness" href="./LOGDIR/protection-read/${taskdef_name}/witness.yml">witness</column>
9+
<column title="entries">total generation entries: (\d+)</column>
10+
<column title="cputime"/>
11+
<!-- <column title="walltime"/> -->
12+
<!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> -->
13+
<column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column>
14+
<column title="vars">vars = (\d+)</column>
15+
<column title="evals">evals = (\d+)</column>
16+
<column title="live">live: (\d+)</column>
17+
</result>
18+
19+
<result filename="ourtool-validate-protection-read-tmp.*.results.protection-read.Pthread.xml.bz2">
20+
<column title="status"/>
21+
<column title="confirmed"> confirmed: (\d+)</column>
22+
<column title="unconfirmed"> unconfirmed: (\d+)</column>
23+
<column title="refuted"> refuted: (\d+)</column>
24+
<column title="error"> error: (\d+)</column>
25+
<column title="cputime"/>
26+
<!-- <column title="walltime"/> -->
27+
<!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> -->
28+
<column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column>
29+
<column title="vars">vars = (\d+)</column>
30+
<column title="evals">evals = (\d+)</column>
31+
<column title="live">live: (\d+)</column>
32+
</result>
33+
34+
<result filename="ourtool-validate-mine-tmp.*.results.protection-read.Pthread.xml.bz2">
35+
<column title="status"/>
36+
<column title="confirmed"> confirmed: (\d+)</column>
37+
<column title="unconfirmed"> unconfirmed: (\d+)</column>
38+
<column title="refuted"> refuted: (\d+)</column>
39+
<column title="error"> error: (\d+)</column>
40+
<column title="cputime"/>
41+
<!-- <column title="walltime"/> -->
42+
<!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> -->
43+
<column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column>
44+
<column title="vars">vars = (\d+)</column>
45+
<column title="evals">evals = (\d+)</column>
46+
<column title="live">live: (\d+)</column>
47+
</result>
48+
49+
<result filename="ourtool.*.results.mine.Pthread.xml.bz2.merged.xml.bz2">
50+
<column title="status"/>
51+
<!-- <column title="score"/> -->
52+
<column title="witness" href="./LOGDIR/mine/${taskdef_name}/witness.yml">witness</column>
53+
<column title="entries">total generation entries: (\d+)</column>
54+
<column title="cputime"/>
55+
<!-- <column title="walltime"/> -->
56+
<!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> -->
57+
<column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column>
58+
<column title="vars">vars = (\d+)</column>
59+
<column title="evals">evals = (\d+)</column>
60+
<column title="live">live: (\d+)</column>
61+
</result>
62+
63+
<result filename="ourtool-validate-protection-read-tmp.*.results.mine.Pthread.xml.bz2">
64+
<column title="status"/>
65+
<column title="confirmed"> confirmed: (\d+)</column>
66+
<column title="unconfirmed"> unconfirmed: (\d+)</column>
67+
<column title="refuted"> refuted: (\d+)</column>
68+
<column title="error"> error: (\d+)</column>
69+
<column title="cputime"/>
70+
<!-- <column title="walltime"/> -->
71+
<!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> -->
72+
<column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column>
73+
<column title="vars">vars = (\d+)</column>
74+
<column title="evals">evals = (\d+)</column>
75+
<column title="live">live: (\d+)</column>
76+
</result>
77+
78+
<result filename="ourtool-validate-mine-tmp.*.results.mine.Pthread.xml.bz2">
79+
<column title="status"/>
80+
<column title="confirmed"> confirmed: (\d+)</column>
81+
<column title="unconfirmed"> unconfirmed: (\d+)</column>
82+
<column title="refuted"> refuted: (\d+)</column>
83+
<column title="error"> error: (\d+)</column>
84+
<column title="cputime"/>
85+
<!-- <column title="walltime"/> -->
86+
<!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> -->
87+
<column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column>
88+
<column title="vars">vars = (\d+)</column>
89+
<column title="evals">evals = (\d+)</column>
90+
<column title="live">live: (\d+)</column>
91+
</result>
92+
93+
</table>

‎thread-witnesses/st-cross/convert.xml‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
<?xml version="1.0"?>
2+
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
3+
<benchmark tool="cpachecker" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1">
4+
5+
<option name="-heap">10000M</option>
6+
<option name="-timelimit">900s</option>
7+
8+
<resultfiles>**/invariantWitnesses/*</resultfiles>
9+
<!-- <resultfiles>**</resultfiles> -->
10+
<option name="-witness2invariant"/>
11+
<option name="-skipRecursion"/>
12+
13+
<rundefinition name="ourtool">
14+
<requiredfiles>RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml</requiredfiles>
15+
<option name="-setprop">invariantStore.witness=RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml</option>
16+
</rundefinition>
17+
18+
<tasks>
19+
<include>../plain/*.yml</include>
20+
<propertyfile expectedverdict="true">../properties/unreach-call.prp</propertyfile>
21+
</tasks>
22+
23+
</benchmark>

‎thread-witnesses/st-cross/ourtool-validate-self.xml‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
<?xml version="1.0"?>
2+
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
3+
<benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1">
4+
5+
<resultfiles></resultfiles>
6+
7+
<option name="--conf">conf/svcomp-yaml-validate.json</option>
8+
<option name="--enable">dbg.timing.enabled</option>
9+
<option name="--set">ana.activated[+]</option><option>apron</option>
10+
<option name="--set">ana.apron.domain</option><option>polyhedra</option>
11+
12+
<tasks>
13+
<include>../plain/*.yml</include>
14+
<propertyfile expectedverdict="true">../properties/unreach-call.prp</propertyfile>
15+
</tasks>
16+
17+
<rundefinition name="ourtool-yaml">
18+
<requiredfiles>RESULTSDIR/LOGDIR/ourtool/${taskdef_name}/witness.yml</requiredfiles>
19+
<option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR/ourtool/${taskdef_name}/witness.yml</option>
20+
<option name="--witness.yaml.validate">RESULTSDIR/LOGDIR/ourtool/${taskdef_name}/witness.yml</option>
21+
</rundefinition>
22+
23+
<rundefinition name="ourtool-graphml">
24+
<requiredfiles>RESULTSDIR/LOGDIR3/ourtool/${taskdef_name}/witness.yml</requiredfiles>
25+
<option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR3/ourtool/${taskdef_name}/witness.yml</option>
26+
<option name="--witness.yaml.validate">RESULTSDIR/LOGDIR3/ourtool/${taskdef_name}/witness.yml</option>
27+
</rundefinition>
28+
29+
</benchmark>

0 commit comments

Comments
 (0)