In January 2021 we will introduce a 10 GB quota for project repositories. Higher limits for individual projects will be available on request. Please see https://doku.lrz.de/display/PUBLIC/GitLab for more information.

Commit 20146560 authored by Philipp Meyer's avatar Philipp Meyer

Refined run-benchmarks script

parent e1b46850
#!/bin/bash
#benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' )
benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' )
#benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' 'cav-benchmarks/bug_tracking' 'cav-benchmarks/bug_tracking' )
#benchmarks=( 'cav-benchmarks/bug_tracking' )
#benchmarks=( 'cav-benchmarks/medical' )
benchmarks=( 'cav-benchmarks/mist' )
extensions=( 'pnet' 'tpn' 'lola' 'spec' )
executable='../slapnet'
#2 minutes
time_soft=$(expr 2 \* 60)
time_hard=$(expr $time_soft + 60)
# 2 GB
mem_soft=$(expr 2 \* 1048576)
mem_hard=$(expr $mem_soft + 1024)
properties=( 'safety' 'safe' 'deadlock-free' 'terminating' )
property_options=( ''
'--no-given-properties --safe'
'--no-given-properties --deadlock-free'
'--no-given-properties --terminating'
)
# TODO: separate input, output and result files
for benchmark in ${benchmarks[@]}; do
benchmark_dir="$benchmark"
>$benchmark_dir/positive-slapnet.list
>$benchmark_dir/dontknow-slapnet.list
>$benchmark_dir/timeout-slapnet.list
>$benchmark_dir/error-slapnet.list
for ext in ${extensions[@]}; do
for file in `find $benchmark_dir -name "*.$ext"`; do
T="$(date +%s%N)"
(
set -o pipefail;
timeout 60 $executable --no-given-properties --terminating --$ext $file 2>&1 | tee $file.out
)
result=$?
T=$(($(date +%s%N)-T))
if [[ result -eq 0 ]]; then
list='positive'
elif [[ result -eq 2 ]]; then
list='dontknow'
elif [[ result -eq 124 || result -eq 137 ]]; then
list='timeout'
else
list='error'
fi
echo $T $file >>$benchmark_dir/$list-slapnet.list
benchmark_dir="$benchmark"
for (( propi=0;propi<${#properties[@]};propi++)); do
prop=${properties[$propi]}
prop_options=${property_options[$propi]}
>$benchmark_dir/$prop-positive-slapnet.list
>$benchmark_dir/$prop-dontknow-slapnet.list
>$benchmark_dir/$prop-timeout-slapnet.list
>$benchmark_dir/$prop-error-slapnet.list
for ext in ${extensions[@]}; do
for file in $(find $benchmark_dir -name "*.$ext"); do
# TODO: use /usr/bin/time to measure resources
timing="$(date +%s%N)"
(
ulimit -S -t $time_soft
ulimit -H -t $time_hard
ulimit -S -v $mem_soft
ulimit -H -v $mem_hard
set -o pipefail
$executable $prop_options --$ext $file 2>&1 | tee $file.$prop.out
)
result=$?
timing=$(($(date +%s%N)-timing))
if [[ result -eq 0 ]]; then
list='positive'
elif [[ result -eq 2 ]]; then
list='dontknow'
elif [[ result -gt 127 ]]; then
list='timeout'
timing=$result
else
list='error'
timing=$result
fi
echo $timing $file >>$benchmark_dir/$prop-$list-slapnet.list
done
done
done
done
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