Commit e575bdb8 authored by Etienne Renault's avatar Etienne Renault
Browse files

bench: update according to new benchmark

* Makefile, benchs/run-benchmark.sh: Here.
parent 27d28b18
......@@ -39,7 +39,7 @@ check: go2pins
@cd tests && ./run.sh
benchmark:
@make clean release && cd benchs && ./run-benchmark.sh $(nbthreads)
@make clean release && cd benchs && make $(nbthreads)
clean:
go clean
......
# Copyright (C) 2020 Laboratoire de Recherche et Developpement
# de l'EPITA (LRDE).
#
# This file is part of Go2Pins, a tool for Golang model-checking
#
# Go2Pins is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Go2Pins is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
# /bin/zsh
# This script runs the benchmark as presented in the paper
# Files from RERSchallenge, category "Sequential Reachability Problems"
# Note that we exclude from this benchmark all files that fall in the
# category "Sequential Reachability Problems/data structures, hard" since
# they require complex array manipulation that are not yet supported by
# the Go2Pins tool.
LTLFILES="RERS/2016-Problem1-ltl.go \
RERS/2016-Problem2-ltl.go \
RERS/2016-Problem4-ltl.go \
RERS/2016-Problem5-ltl.go \
RERS/2016-Problem7-ltl.go \
RERS/2017-Problem1-ltl.go \
RERS/2017-Problem2-ltl.go \
RERS/2017-Problem4-ltl.go \
RERS/2017-Problem5-ltl.go \
RERS/2017-Problem7-ltl.go \
RERS/2018-Problem1-ltl.go \
RERS/2018-Problem2-ltl.go \
RERS/2018-Problem4-ltl.go \
RERS/2018-Problem5-ltl.go \
RERS/2018-Problem7-ltl.go \
RERS/2019-Problem1-ltl.go \
RERS/2019-Problem2-ltl.go \
RERS/2019-Problem4-ltl.go \
RERS/2019-Problem5-ltl.go \
RERS/2019-Problem7-ltl.go \
RERS/2020-Problem1-ltl.go \
RERS/2020-Problem2-ltl.go \
RERS/2020-Problem4-ltl.go \
RERS/2020-Problem5-ltl.go \
RERS/2020-Problem7-ltl.go "
FILES="RERS/2016-Problem10-reach.go \
RERS/2016-Problem11-reach.go \
RERS/2016-Problem12-reach.go \
RERS/2016-Problem14-reach.go \
RERS/2016-Problem15-reach.go \
RERS/2017-Problem10-reach.go \
RERS/2017-Problem11-reach.go \
RERS/2017-Problem12-reach.go \
RERS/2017-Problem14-reach.go \
RERS/2017-Problem15-reach.go \
RERS/2018-Problem10-reach.go \
RERS/2018-Problem11-reach.go \
RERS/2019-Problem11-reach.go \
RERS/2019-Problem12-reach.go \
RERS/2019-Problem14-reach.go \
RERS/2019-Problem15-reach.go "
NBTHREADS=1
if [ $# -eq 1 ]; then
NBTHREADS=$1
fi
OUTPUT="benchs-$NBTHREADS.csv"
OUTPUT_BB="benchs-bb-$NBTHREADS.csv"
OUTPUT_REACH="benchs-reach-$NBTHREADS.csv"
OUTPUT_LTL="benchs-ltl-$NBTHREADS.csv"
echo "##################################"
echo "==> Benchmark for LTL evaluation"
echo "##################################"
echo
if [ ! -f "$OUTPUT_LTL" ]; then
echo "model,isempty,spottime,ltsmintime,formulae" > $OUTPUT_LTL
fi
echo First, we transpile only once every model. This may take some time.
i=0
for model in $LTLFILES; do
echo -e "==> Processing $model"
rers_inputs=$(cat $model | grep 'var inputs \[\]int' | \
sed 's/var inputs \[\]int = \[\]int{//g' | \
sed 's/}//g' | sed 's/ *//g' | sed 's/,/;/g')
filename=$(basename -- "$model")
filename="${filename%.*}"
if [ -d "$filename" ]; then
echo " $filename already exists, skip transpilation"
continue
fi
../go2pins -f -o $filename -rers "$rers_inputs" $model > /dev/null 2>&1
done
i=0
for model in $LTLFILES; do
echo -e "==> Processing $model"
while read -r formulae
do
# Detect the number of lines and skip already computed formulae
LOC=$(wc -l $OUTPUT_LTL | awk '{print $1}' )
tmp=$((i+2))
if [ "$tmp" -lt "$LOC" ]; then
echo " [SKIP] formulae $i"
i=$((i+1))
continue
fi;
rers_inputs=$(cat $model | grep 'var inputs \[\]int' | \
sed 's/var inputs \[\]int = \[\]int{//g' | \
sed 's/}//g' | sed 's/ *//g' | sed 's/,/;/g')
filename=$(basename -- "$model")
filename="${filename%.*}"
# Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time"
echo "$model,$status,$spot_time,$ltsmin_time,$formulae">> $OUTPUT_LTL
i=$((i+1))
done < $model.formulae.txt
done
echo
echo file : $(pwd)/$OUTPUT_LTL contains the CSV of LTL evaluation
echo "##################################"
echo "==> Benchmark for Reachability / Correctness"
echo "##################################"
echo
if [ ! -f "$OUTPUT_REACH" ]; then
echo "model,isempty,spottime,ltsmintime,formulae" > $OUTPUT_REACH
fi;
i=0
for model in $FILES; do
if [ ! -f "$model.formulae.txt" ]; then
# No full specification for this model
continue
fi
rers_inputs=$(cat $model | grep 'var inputs \[\]int' | \
sed 's/var inputs \[\]int = \[\]int{//g' | \
sed 's/}//g' | sed 's/ *//g' | sed 's/,/;/g')
filename=$(basename -- "$model")
filename="${filename%.*}"
../go2pins -f -o $filename -rers "$rers_inputs" $model > /dev/null 2>&1
echo -e "==> Processing $model"
while read -r status formulae
do
# Detect the number of lines and skip already computed formulae
LOC=$(wc -l $OUTPUT_REACH | awk '{print $1}' )
tmp=$((i+2))
if [ "$tmp" -lt "$LOC" ]; then
echo " [SKIP] formulae $i"
i=$((i+1))
continue
fi;
# Compute LTSmin and Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time"
if [ "$status" == "EMPTY" ]; then
TMP=$(echo $RESS | grep "no accepting run found")
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $formulae
exit 1
fi
else
TMP=$(echo $RESS | grep "an accepting run exists")
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $formulae
exit 1
fi
fi
echo "$model,$status,$spot_time,$ltsmin_time,$formulae">> $OUTPUT_REACH
i=$((i+1))
done < $model.formulae.txt
done
echo
echo file : $(pwd)/$OUTPUT_REACH contains the CSV of reachability evaluation
echo "##################################"
echo "==> Benchmark for Compilation time"
echo "##################################"
echo
if [ ! -f "$OUTPUT" ]; then
echo "#filename,loc,transpile_time,compile_time,total_time,final_num_var,final_loc" > $OUTPUT
fi
# Clean cache to have relevant times.
go clean -cache
for model in $FILES; do
echo -e "==> Processing $model"
loc=$(wc -l $model| awk '{print $1}')
echo -e " - Line of code (original file):\t$loc"
filename=$(basename -- "$model")
filename="${filename%.*}"
tmp=(grep $filename $OUTPUT)
if [ ! -z "$tmp" ]; then
continue
fi
rers_inputs=$(cat $model | grep 'var inputs \[\]int' | \
sed 's/var inputs \[\]int = \[\]int{//g' | \
sed 's/}//g' | sed 's/ *//g' | sed 's/,/;/g')
start=$(date +%s.%N)
../go2pins -f -o $filename -rers "$rers_inputs" $model > /dev/null 2>&1
end=$(date +%s.%N)
transpile_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo -e " - Go2Pins processing:\t\t$transpile_time seconds"
rm -Rf $COCACHE
start=$(date +%s.%N)
make -C $filename > /dev/null 2>&1
end=$(date +%s.%N)
compile_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo -e " - Compiling output:\t\t\t$compile_time seconds"
total_time=`echo -e "$compile_time + $transpile_time"| bc`
echo -e " - Total Time:\t\t\t$total_time seconds"
final_num_var=$($filename/go2pins-mc --list-variables | grep '\-' | wc -l)
echo -e " - Number of variables:\t\t$final_num_var"
loc2=$(wc -l $filename/$filename.go| tail -n1|awk '{print $1}')
echo -e " - Line of code generated:\t\t$loc2"
echo
echo "$filename,$loc,$transpile_time,$compile_time,$total_time,$final_num_var,$loc2" >> $OUTPUT
done
echo file : $(pwd)/$OUTPUT contains the CSV of all previous values
echo
#######################
# Blackbox evaluation
######################
NB_FUN=$(cat sqrt_prime_fibo.go | grep compute_main | grep -v func | wc -l)
echo "###########################"
echo "==> Benchmark for BlackBox."
echo "###########################"
echo
echo "#######################################################################"
echo "# /!\ Note that some of these tests require huge amount of memory /!\ #"
echo "# - 90% BlackBox: 1.31 sec / 115168 kbytes # "
echo "# - 80% BlackBox: 2.49 sec / 202044 kbytes # "
echo "# - 70% BlackBox: 4.58 sec / 349352 kbytes # "
echo "# - 60% BlackBox: 6.89 sec / 562036 kbytes # "
echo "# - 50% BlackBox: 11.13 sec / 928384 kbytes # "
echo "# - 40% BlackBox: 26.86 sec / 2301496 kbytes # "
echo "# - 30% BlackBox: 45.48 sec / 3700572 kbytes # "
echo "# - 20% BlackBox: 75.08 sec / 6037908 kbytes # "
echo "# - 10% BlackBox: 114.12 sec / 9825980 kbytes # "
echo "# - 0% BlackBox: 298.32 sec / 26478164 kbytes # "
echo "#######################################################################"
echo "bb-percent,states,transitions,time,mem" > $OUTPUT_BB
PAGE_SIZE=$(getconf PAGE_SIZE)
for i in 90 80 70 60 50 40 30 20 10 0; do
PERCENT=$i
model=sqrt_prime_fibo.go
echo "==> Processing file 'sqrt_prime_fibo.go' with $PERCENT% BlackBox"
HOW_MANY=$((NB_FUN*PERCENT/100))
BB=$(cat sqrt_prime_fibo.go | grep compute_main | grep -v func | tail -n $HOW_MANY| tr '\n' ';' | sed 's/\t*//g' | sed 's/([^)]*)//g' )
BB=$(echo "${BB%?}") # remove last semicolumn
../go2pins -f -o "sqrt_prime_fibo_$PERCENT" -blackbox-fn "$BB" $model > /dev/null 2>&1
cd sqrt_prime_fibo_$PERCENT
make > /dev/null 2>&1
RESULT=$( /usr/bin/time -v ./go2pins-mc -kripke-size 2>&1 | sed "s/kripke/$PERCENT/g" >/tmp/go2pins.tmp.1)
RESULT2=$(cat /tmp/go2pins.tmp.1 | grep "^#" | sed 's/#//g')
ST=$(echo $RESULT2 | awk -F',' '{print $2}')
TR=$(echo $RESULT2 | awk -F',' '{print $3}')
U_TIME=$(cat /tmp/go2pins.tmp.1 | grep "User time" | awk '{print $4}')
MEM=$(cat /tmp/go2pins.tmp.1 | grep "Maximum resident" | awk '{print $6}')
echo -e " - States: $ST states"
echo -e " - Transitions: $TR transitions"
echo -e " - Time: $U_TIME seconds"
echo -e " - Memory: $MEM kbytes"
cd ..
RESULT2=$RESULT2","$U_TIME","$MEM
echo $RESULT2 >> $OUTPUT_BB
done
echo
echo file : $(pwd)/$OUTPUT_BB contains the CSV of blackbox evaluation
Supports Markdown
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