Commit 06641dfe authored by Etienne Renault's avatar Etienne Renault

bench: report time and memory

* benchs/run-benchmark.sh: Here.
parent 0eb9eb63
Pipeline #18449 passed with stage
in 1 minute and 36 seconds
......@@ -90,6 +90,7 @@ for model in $FILES; do
done
echo file : $(pwd)/$OUTPUT contains the CSV of all previous values
echo
#######################
# Blackbox evaluation
......@@ -101,29 +102,47 @@ echo "###########################"
echo "==> Benchmark for BlackBox."
echo "###########################"
echo
echo "/!\ Note that some of these tests require huge amount of memory /!\ "
echo
echo "bb-percent,states,transitions" > $OUTPUT_BB
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 | head -n $HOW_MANY| tr '\n' ';' | sed 's/\t*//g' | sed 's/([^)]*)//g' )
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=$(./go2pins-mc -kripke-size| sed "s/kripke/$PERCENT/g" | grep "^#")
ST=$(echo $RESULT | awk -F',' '{print $2}')
TR=$(echo $RESULT | awk -F',' '{print $3}')
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
echo -e " - Time: $U_TIME seconds"
echo -e " - Memory: $MEM kbytes"
cd ..
echo $RESULT >> $OUTPUT_BB
RESULT2=$RESULT2","$U_TIME","$MEM
echo $RESULT2 >> $OUTPUT_BB
done
echo
......
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