Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

Commit 6f0c6f0a authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Configured benchmark scripts to either reproduce PODC results or complete results

parent 5f542a3d
all: main.pdf
all: results-complete.pdf
program: pp-print
podc: results-podc.pdf
program: pp-print
@echo 'Compiling pp-print'
@$(MAKE) -C pp-print
......@@ -11,17 +13,26 @@ peregrine:
protocols: program
@./generate_protocols.sh
results/results.csv: protocols peregrine
@./run_benchmarks.sh
results-podc.csv: protocols peregrine
@./run_benchmarks.sh $@ termination consensus
results-complete.csv: protocols peregrine
@./run_benchmarks.sh $@ termination consensus correctness
table-podc.tex: results-podc.csv
python3 make_table.py $< >$@
table-complete.tex: results-complete.csv
python3 make_table.py $< >$@
table.tex: results/results.csv
python3 make_table.py >table.tex
results-podc.pdf: results-podc.tex table-podc.tex
pdflatex $<
main.pdf: table.tex
pdflatex main.tex
results-complete.pdf: results-complete.tex table-complete.tex
pdflatex $<
clean:
@rm -f *.aux *.log *.pdf
@rm -rf results protocols out
@rm -f table.tex
@rm -rf results-podc.csv results-complete.csv protocols out
@rm -f table.tex table-podc.tex table-complete.tex
@$(MAKE) clean -C pp-print
import sys
import pandas as pd
benchmark_dir='.'
results_dir='results'
properties = [ 'termination', 'consensus', 'correctness' ]
prop_steps = [ '$|\mathcal{P}|$', '$|R|$', '$|R|$' ]
prop_steps = {}
prop_steps['termination'] = '$|\mathcal{P}|$'
prop_steps['consensus'] = '$|R|$'
prop_steps['correctness'] = '$|R|$'
max_params = 2
long_table = True
short_table = False
results_file = 'results/results.csv'
if len(sys.argv) >= 2:
long_table = False
short_table = False
for arg in sys.argv[1:]:
if arg == '-s':
short_table = True
elif arg == '-l':
long_table = True
if arg[0] == '-':
if arg == '-s':
long_table = False
short_table = True
elif arg == '-l':
long_table = True
short_table = False
else:
print("unknown argument: %s" % arg, file=sys.stderr)
sys.exit(-1)
else:
print("unknown argument: %s" % arg, file=sys.stderr)
sys.exit(-1)
results_file = sys.argv[1]
# long table
if long_table:
results_file='results.csv'
results = pd.read_csv(benchmark_dir + '/' + results_dir + '/' + results_file)
results = pd.read_csv(results_file)
properties = list(map(lambda s: s[:-7], filter(lambda s: s[-7:] == "_result", results.columns.values, )))
alignrow = "\\begin{longtable}{l"
for i in range(max_params):
......@@ -42,8 +47,8 @@ if long_table:
print("\\toprule")
headerrow = "protocol & \\multicolumn{%d}{c}{params} & $|Q|$ & $|T|$" % max_params
for prop, prop_step in zip(properties, prop_steps):
headerrow += " & %s & %s" % (prop, prop_step)
for prop in properties:
headerrow += " & %s & %s" % (prop, prop_steps[prop])
headerrow += " & total \\\\"
print(headerrow)
......@@ -133,7 +138,9 @@ if long_table:
if short_table:
results_file='results.csv'
results = pd.read_csv(benchmark_dir + '/' + results_dir + '/' + results_file)
results = pd.read_csv(results_file)
properties = list(map(lambda s: s[:-7], filter(lambda s: s[-7:] == "_result", results.columns.values, )))
last_protocol = ''
last_params = []
......
\documentclass{scrartcl}
\usepackage[a4paper, top=1cm, bottom=1cm, left=1cm, right=1cm]{geometry}
\usepackage[table]{xcolor}
\usepackage{booktabs}
\usepackage{longtable}
\usepackage{multirow}
\begin{document}
\input{table-complete.tex}
\begin{tabular}{ll}
$|Q|$ & Number of states. \\
$|T|$ & Number of non-silent transitions. \\
termination & Time in seconds to prove layered termination. \\
$|\mathcal{P}|$ & Number of layers in the partition for layered termination. \\
consensus & Time in seconds to prove strong consensus. \\
correctness & Time in seconds to prove strong consensus with correctness. \\
$|\mathcal{R}|$ & Number of refinement steps (i.e.\ number of traps or siphons) for strong consensus and correctness. \\
total & Time in seconds to prove layered termination, strong consensus and strong consensus with correctness. \\
\end{tabular}
\end{document}
......@@ -8,7 +8,7 @@
\begin{document}
\input{table.tex}
\input{table-podc.tex}
\begin{tabular}{ll}
$|Q|$ & Number of states. \\
......
#!/bin/bash
benchmark_dir='.'
protocols_dir='protocols'
out_dir='out'
results_dir='results'
extension='pp'
executable_dir='../dist/build/peregrine'
......@@ -13,82 +11,83 @@ options='-i -v'
#1 hour
timelimit=$((1 * 3600))
properties=( 'termination' 'consensus' 'correctness' )
prop_options=( '--layered-termination' '--strong-consensus' '--correctness' )
prop_refinements=( 'Checking SAT of layered termination' 'Checking SAT of trap' 'Checking SAT of trap' )
structure_option='--structure'
results_file="$1"
properties="${@:2}"
declare -A prop_options
prop_options['termination']='--layered-termination'
prop_options['consensus']='--strong-consensus'
prop_options['correctness']='--correctness'
mkdir -p $benchmark_dir/$out_dir
mkdir -p $benchmark_dir/$results_dir
declare -A prop_refinements
prop_refinements['termination']='Checking SAT of layered termination'
prop_refinements['consensus']='Checking SAT of trap'
prop_refinements['correctness']='Checking SAT of trap'
>$benchmark_dir/$results_dir/results.csv
echo -n "protocol,file,states,transitions" >>$benchmark_dir/$results_dir/results.csv
structure_option='--structure'
for (( propi=0;propi<${#properties[@]};propi++)); do
prop=${properties[$propi]}
echo -n ",${prop}_result,${prop}_time,${prop}_refinements" >>$benchmark_dir/$results_dir/results.csv
>$benchmark_dir/$results_dir/$prop.positive.list
>$benchmark_dir/$results_dir/$prop.dontknow.list
>$benchmark_dir/$results_dir/$prop.timeout.list
>$benchmark_dir/$results_dir/$prop.error.list
mkdir -p $out_dir
>$results_file
echo -n "protocol,file,states,transitions" >>$results_file
for prop in $properties; do
echo -n ",${prop}_result,${prop}_time,${prop}_refinements" >>$results_file
done
echo >>$benchmark_dir/$results_dir/results.csv
echo >>$results_file
for protocol_dir in $(find $benchmark_dir/$protocols_dir -mindepth 1 -maxdepth 1 -type d); do
for protocol_dir in $(find $protocols_dir -mindepth 1 -maxdepth 1 -type d); do
protocol=$(basename $protocol_dir)
echo
echo "Benchmarking $protocol protocol"
echo
mkdir -p $benchmark_dir/$out_dir/$protocol
mkdir -p $out_dir/$protocol
timeout_reached='false'
for param in $(seq 1 1000); do
if [ $timeout_reached == 'false' ]; then
for filename in $(find $protocol_dir -mindepth 1 -maxdepth 1 -name "${protocol}_?${param}_*.$extension"); do
file=$(basename $filename)
echo -n "$protocol,$file" >>$benchmark_dir/$results_dir/results.csv
echo -n "$protocol,$file" >>$results_file
(
$executable_dir/$executable $options $structure_option $filename 2>&1 | tee $benchmark_dir/$out_dir/$protocol/$file.out
$executable_dir/$executable $options $structure_option $filename 2>&1 | tee $out_dir/$protocol/$file.out
)
n_states=$(grep -e '^States *: ' "$benchmark_dir/$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
n_transitions=$(grep -e '^Transitions *: ' "$benchmark_dir/$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
echo -n ",$n_states,$n_transitions" >>$benchmark_dir/$results_dir/results.csv
for (( propi=0;propi<${#properties[@]};propi++)); do
prop=${properties[$propi]}
prop_option=${prop_options[$propi]}
prop_refinement=${prop_refinements[$propi]}
n_states=$(grep -e '^States *: ' "$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
n_transitions=$(grep -e '^Transitions *: ' "$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
echo -n ",$n_states,$n_transitions" >>$results_file
for prop in $properties; do
prop_option=${prop_options[$prop]}
prop_refinement=${prop_refinements[$prop]}
echo "Benchmarking $file with property $prop"
timing="$(date +%s%N)"
(
set -o pipefail
echo timeout $timelimit $executable_dir/$executable $options $prop_option $filename
timeout $timelimit $executable_dir/$executable $options $prop_option $filename 2>&1 | tee $benchmark_dir/$out_dir/$protocol/$file.$prop.out
timeout $timelimit $executable_dir/$executable $options $prop_option $filename 2>&1 | tee $out_dir/$protocol/$file.$prop.out
)
result=$?
timing=$(($(date +%s%N)-timing))
if [[ result -eq 0 ]]; then
list='positive'
res='positive'
elif [[ result -eq 2 ]]; then
list='dontknow'
res='dontknow'
elif [[ result -eq 124 || result -eq 137 ]]; then
list='timeout'
res='timeout'
else
list='error'
res='error'
fi
# get number of refinement steps
n_refinements=$(grep -c -e "$prop_refinement" "$benchmark_dir/$out_dir/$protocol/$file.$prop.out")
echo "$file,$timing" >>$benchmark_dir/$results_dir/$prop.$list.list
echo -n ",$list,$timing,$n_refinements" >>$benchmark_dir/$results_dir/results.csv
if [ $list == 'timeout' ]; then
n_refinements=$(grep -c -e "$prop_refinement" "$out_dir/$protocol/$file.$prop.out")
echo -n ",$res,$timing,$n_refinements" >>$results_file
if [ $res == 'timeout' ]; then
timeout_reached='true'
fi
done
echo >>$benchmark_dir/$results_dir/results.csv
echo >>$results_file
done
fi
done
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment