-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #51 from goblint/thread-witnesses
Thread-modular witnesses benchmarking
- Loading branch information
Showing
60 changed files
with
1,770 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| *-tmp.xml |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| # Thread-Modular Correctness Witnesses and their Validation | ||
| ## An Abstract Interpretation Perspective | ||
|
|
||
| ### Layout | ||
| * `autoactive/plain` — programs and GraphML witnesses from AutoActive artifact. | ||
| * `autoactive/generated_yaml` — converted YAML witnesses. | ||
| * `bench` — this repository. | ||
| * `benchexec` — BenchExec version. | ||
| * `CPAchecker-2.2-unix` — CPAchecker from SV-COMP 2023 archives. | ||
| * `ourtool` — our tool, including source code. **NB! Although git authorship has been stripped, the contents of this directory do reveal the unanonymized tool name.** | ||
| * `results` — results directory for scripts. | ||
| * `sv-benchmarks` — SV-COMP 2022 benchmarks, at least ReachSafety-Loops. | ||
| * `UAutomizer-linux` — Ultimate Automizer from SV-COMP 2023 archives. | ||
|
|
||
| ### Scripts | ||
| * `./st-same/run.sh` — single-threaded programs, same-framework. | ||
| * `./st-cross/witnessToYaml.sh` — convert single-threaded cross-framework witnesses from GraphML to YAML (very slow!). | ||
| * `./st-cross/run.sh` — single-threaded programs, cross-framework. | ||
| * `./st-lit/run.sh` — single-threaded programs from literature. | ||
| * `./mt/run.sh` — multi-threaded programs, same- and cross-framework. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| <?xml version="1.0"?> | ||
| <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd"> | ||
| <benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1"> | ||
|
|
||
| <resultfiles></resultfiles> | ||
|
|
||
| <option name="--conf">conf/bench-yaml-validate.json</option> | ||
| <option name="--enable">dbg.timing.enabled</option> | ||
|
|
||
| <!-- after-lock --> | ||
| <option name="--enable">witness.invariant.loop-head</option> | ||
| <option name="--enable">witness.invariant.after-lock</option> | ||
| <option name="--disable">witness.invariant.other</option> | ||
| <option name="--disable">witness.invariant.accessed</option> | ||
|
|
||
| <!-- validate2 --> | ||
| <option name="--ana.base.privatization">mine</option> | ||
|
|
||
| <rundefinition name="protection-read"> | ||
| </rundefinition> | ||
|
|
||
| <rundefinition name="mine"> | ||
| </rundefinition> | ||
|
|
||
| <requiredfiles>RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</requiredfiles> | ||
| <requiredfiles>RESULTSDIR/LOGDIR/mine/${taskdef_name}/witness.yml</requiredfiles> | ||
| <option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</option> | ||
| <option name="--witness.yaml.validate">RESULTSDIR/LOGDIR/mine/${taskdef_name}/witness.yml</option> | ||
|
|
||
| <tasks name="Pthread"> | ||
| <includesfile>../../Pthread.set</includesfile> | ||
| <includesfile>../../SvComp-Pthread.set</includesfile> | ||
| </tasks> | ||
|
|
||
| </benchmark> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| <?xml version="1.0"?> | ||
| <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd"> | ||
| <benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1"> | ||
|
|
||
| <resultfiles></resultfiles> | ||
|
|
||
| <option name="--conf">conf/bench-yaml-validate.json</option> | ||
| <option name="--enable">dbg.timing.enabled</option> | ||
|
|
||
| <!-- after-lock --> | ||
| <option name="--enable">witness.invariant.loop-head</option> | ||
| <option name="--enable">witness.invariant.after-lock</option> | ||
| <option name="--disable">witness.invariant.other</option> | ||
| <option name="--disable">witness.invariant.accessed</option> | ||
|
|
||
| <!-- validate1 --> | ||
| <option name="--ana.base.privatization">protection-read</option> | ||
|
|
||
| <rundefinition name="protection-read"> | ||
| </rundefinition> | ||
|
|
||
| <rundefinition name="mine"> | ||
| </rundefinition> | ||
|
|
||
| <requiredfiles>RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</requiredfiles> | ||
| <requiredfiles>RESULTSDIR/LOGDIR/protection-read/${taskdef_name}/witness.yml</requiredfiles> | ||
| <option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml</option> | ||
| <option name="--witness.yaml.validate">RESULTSDIR/LOGDIR/protection-read/${taskdef_name}/witness.yml</option> | ||
|
|
||
| <tasks name="Pthread"> | ||
| <includesfile>../../Pthread.set</includesfile> | ||
| <includesfile>../../SvComp-Pthread.set</includesfile> | ||
| </tasks> | ||
|
|
||
| </benchmark> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| <?xml version="1.0"?> | ||
| <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd"> | ||
| <benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1"> | ||
|
|
||
| <resultfiles>**.yml</resultfiles> | ||
|
|
||
| <option name="--conf">conf/bench-yaml.json</option> | ||
| <option name="--enable">dbg.timing.enabled</option> | ||
|
|
||
| <!-- after-lock --> | ||
| <option name="--enable">witness.invariant.loop-head</option> | ||
| <option name="--enable">witness.invariant.after-lock</option> | ||
| <option name="--disable">witness.invariant.other</option> | ||
| <option name="--disable">witness.invariant.accessed</option> | ||
|
|
||
| <rundefinition name="protection-read"> | ||
| <option name="--ana.base.privatization">protection-read</option> | ||
| </rundefinition> | ||
|
|
||
| <rundefinition name="mine"> | ||
| <option name="--ana.base.privatization">mine</option> | ||
| </rundefinition> | ||
|
|
||
| <tasks name="Pthread"> | ||
| <includesfile>../../Pthread.set</includesfile> | ||
| <includesfile>../../SvComp-Pthread.set</includesfile> | ||
| </tasks> | ||
|
|
||
| </benchmark> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,44 @@ | ||
| #!/bin/bash | ||
|
|
||
| shopt -s extglob | ||
|
|
||
| MYBENCHDIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd ) | ||
| RESULTSDIR=$MYBENCHDIR/../../../results/mt | ||
| OURTOOLPARALLEL=4 | ||
| VALIDATEPARALLEL=4 | ||
|
|
||
| mkdir $RESULTSDIR | ||
|
|
||
| # Run verification | ||
| cd $MYBENCHDIR/../../../ourtool | ||
| # read-only and overlay dirs for Value too large for defined data type workaround | ||
| benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $OURTOOLPARALLEL $MYBENCHDIR/ourtool.xml | ||
|
|
||
| # Extract witness directory | ||
| cd $RESULTSDIR | ||
| LOGDIR=`echo ourtool.*.files` | ||
| echo $LOGDIR | ||
|
|
||
| # Construct validation XMLs | ||
| cd $MYBENCHDIR | ||
| sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" ourtool-validate-protection-read.xml > ourtool-validate-protection-read-tmp.xml | ||
| sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" ourtool-validate-mine.xml > ourtool-validate-mine-tmp.xml | ||
|
|
||
| # Run validation | ||
| cd $MYBENCHDIR/../../../ourtool | ||
| benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/ourtool-validate-protection-read-tmp.xml | ||
| benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/ourtool-validate-mine-tmp.xml | ||
|
|
||
| # Merge witness validation results | ||
| cd $RESULTSDIR | ||
| 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 | ||
| 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 | ||
|
|
||
| # Generate table with merged results and witness validation results | ||
| sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator.xml > table-generator.xml | ||
| table-generator -x table-generator.xml | ||
|
|
||
| # Decompress all tool outputs for table HTML links | ||
| unzip -o ourtool.*.logfiles.zip | ||
| unzip -o ourtool-validate-protection-read-tmp.*.logfiles.zip | ||
| unzip -o ourtool-validate-mine-tmp.*.logfiles.zip |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,93 @@ | ||
| <?xml version="1.0" ?> | ||
| <!DOCTYPE table PUBLIC "+//IDN sosy-lab.org//DTD BenchExec table 1.10//EN" "https://www.sosy-lab.org/benchexec/table-1.10.dtd"> | ||
| <table> | ||
|
|
||
| <result filename="ourtool.*.results.protection-read.Pthread.xml.bz2.merged.xml.bz2"> | ||
| <column title="status"/> | ||
| <!-- <column title="score"/> --> | ||
| <column title="witness" href="./LOGDIR/protection-read/${taskdef_name}/witness.yml">witness</column> | ||
| <column title="entries">total generation entries: (\d+)</column> | ||
| <column title="cputime"/> | ||
| <!-- <column title="walltime"/> --> | ||
| <!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> --> | ||
| <column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column> | ||
| <column title="vars">vars = (\d+)</column> | ||
| <column title="evals">evals = (\d+)</column> | ||
| <column title="live">live: (\d+)</column> | ||
| </result> | ||
|
|
||
| <result filename="ourtool-validate-protection-read-tmp.*.results.protection-read.Pthread.xml.bz2"> | ||
| <column title="status"/> | ||
| <column title="confirmed"> confirmed: (\d+)</column> | ||
| <column title="unconfirmed"> unconfirmed: (\d+)</column> | ||
| <column title="refuted"> refuted: (\d+)</column> | ||
| <column title="error"> error: (\d+)</column> | ||
| <column title="cputime"/> | ||
| <!-- <column title="walltime"/> --> | ||
| <!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> --> | ||
| <column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column> | ||
| <column title="vars">vars = (\d+)</column> | ||
| <column title="evals">evals = (\d+)</column> | ||
| <column title="live">live: (\d+)</column> | ||
| </result> | ||
|
|
||
| <result filename="ourtool-validate-mine-tmp.*.results.protection-read.Pthread.xml.bz2"> | ||
| <column title="status"/> | ||
| <column title="confirmed"> confirmed: (\d+)</column> | ||
| <column title="unconfirmed"> unconfirmed: (\d+)</column> | ||
| <column title="refuted"> refuted: (\d+)</column> | ||
| <column title="error"> error: (\d+)</column> | ||
| <column title="cputime"/> | ||
| <!-- <column title="walltime"/> --> | ||
| <!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> --> | ||
| <column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column> | ||
| <column title="vars">vars = (\d+)</column> | ||
| <column title="evals">evals = (\d+)</column> | ||
| <column title="live">live: (\d+)</column> | ||
| </result> | ||
|
|
||
| <result filename="ourtool.*.results.mine.Pthread.xml.bz2.merged.xml.bz2"> | ||
| <column title="status"/> | ||
| <!-- <column title="score"/> --> | ||
| <column title="witness" href="./LOGDIR/mine/${taskdef_name}/witness.yml">witness</column> | ||
| <column title="entries">total generation entries: (\d+)</column> | ||
| <column title="cputime"/> | ||
| <!-- <column title="walltime"/> --> | ||
| <!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> --> | ||
| <column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column> | ||
| <column title="vars">vars = (\d+)</column> | ||
| <column title="evals">evals = (\d+)</column> | ||
| <column title="live">live: (\d+)</column> | ||
| </result> | ||
|
|
||
| <result filename="ourtool-validate-protection-read-tmp.*.results.mine.Pthread.xml.bz2"> | ||
| <column title="status"/> | ||
| <column title="confirmed"> confirmed: (\d+)</column> | ||
| <column title="unconfirmed"> unconfirmed: (\d+)</column> | ||
| <column title="refuted"> refuted: (\d+)</column> | ||
| <column title="error"> error: (\d+)</column> | ||
| <column title="cputime"/> | ||
| <!-- <column title="walltime"/> --> | ||
| <!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> --> | ||
| <column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column> | ||
| <column title="vars">vars = (\d+)</column> | ||
| <column title="evals">evals = (\d+)</column> | ||
| <column title="live">live: (\d+)</column> | ||
| </result> | ||
|
|
||
| <result filename="ourtool-validate-mine-tmp.*.results.mine.Pthread.xml.bz2"> | ||
| <column title="status"/> | ||
| <column title="confirmed"> confirmed: (\d+)</column> | ||
| <column title="unconfirmed"> unconfirmed: (\d+)</column> | ||
| <column title="refuted"> refuted: (\d+)</column> | ||
| <column title="error"> error: (\d+)</column> | ||
| <column title="cputime"/> | ||
| <!-- <column title="walltime"/> --> | ||
| <!-- <column title="memory" sourceUnit="B" displayUnit="MB"/> --> | ||
| <column title="solvetime" sourceUnit="s" displayUnit="s">solving +([0-9.]+) ?s</column> | ||
| <column title="vars">vars = (\d+)</column> | ||
| <column title="evals">evals = (\d+)</column> | ||
| <column title="live">live: (\d+)</column> | ||
| </result> | ||
|
|
||
| </table> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| <?xml version="1.0"?> | ||
| <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd"> | ||
| <benchmark tool="cpachecker" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1"> | ||
|
|
||
| <option name="-heap">10000M</option> | ||
| <option name="-timelimit">900s</option> | ||
|
|
||
| <resultfiles>**/invariantWitnesses/*</resultfiles> | ||
| <!-- <resultfiles>**</resultfiles> --> | ||
| <option name="-witness2invariant"/> | ||
| <option name="-skipRecursion"/> | ||
|
|
||
| <rundefinition name="ourtool"> | ||
| <requiredfiles>RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml</requiredfiles> | ||
| <option name="-setprop">invariantStore.witness=RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml</option> | ||
| </rundefinition> | ||
|
|
||
| <tasks> | ||
| <include>../plain/*.yml</include> | ||
| <propertyfile expectedverdict="true">../properties/unreach-call.prp</propertyfile> | ||
| </tasks> | ||
|
|
||
| </benchmark> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| <?xml version="1.0"?> | ||
| <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd"> | ||
| <benchmark tool="goblint" timelimit="900 s" hardtimelimit="960 s" memlimit="6 GB" cpuCores="1"> | ||
|
|
||
| <resultfiles></resultfiles> | ||
|
|
||
| <option name="--conf">conf/svcomp-yaml-validate.json</option> | ||
| <option name="--enable">dbg.timing.enabled</option> | ||
| <option name="--set">ana.activated[+]</option><option>apron</option> | ||
| <option name="--set">ana.apron.domain</option><option>polyhedra</option> | ||
|
|
||
| <tasks> | ||
| <include>../plain/*.yml</include> | ||
| <propertyfile expectedverdict="true">../properties/unreach-call.prp</propertyfile> | ||
| </tasks> | ||
|
|
||
| <rundefinition name="ourtool-yaml"> | ||
| <requiredfiles>RESULTSDIR/LOGDIR/ourtool/${taskdef_name}/witness.yml</requiredfiles> | ||
| <option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR/ourtool/${taskdef_name}/witness.yml</option> | ||
| <option name="--witness.yaml.validate">RESULTSDIR/LOGDIR/ourtool/${taskdef_name}/witness.yml</option> | ||
| </rundefinition> | ||
|
|
||
| <rundefinition name="ourtool-graphml"> | ||
| <requiredfiles>RESULTSDIR/LOGDIR3/ourtool/${taskdef_name}/witness.yml</requiredfiles> | ||
| <option name="--witness.yaml.unassume">RESULTSDIR/LOGDIR3/ourtool/${taskdef_name}/witness.yml</option> | ||
| <option name="--witness.yaml.validate">RESULTSDIR/LOGDIR3/ourtool/${taskdef_name}/witness.yml</option> | ||
| </rundefinition> | ||
|
|
||
| </benchmark> |
Oops, something went wrong.