diff --git a/salut/test/gen-salut-batch.sh b/salut/test/gen-salut-batch.sh new file mode 100755 index 0000000000000000000000000000000000000000..5b94c197663b1df1cdafec2f93f0722bb6d3fbc8 --- /dev/null +++ b/salut/test/gen-salut-batch.sh @@ -0,0 +1,108 @@ +#!/bin/bash +#set -x + +GITROOT=$(git rev-parse --show-toplevel) +LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/sas.lus" +daemon_lustre_file=${GITROOT}/salut/lib/daemon.lus + +help=" Generate a (standalone) lustre program that runs salut with a lustre daemon + +It is useful to perform batch simulations. + +usage: + $0 daemon topology n [an] + +where: + - daemon is the name of one the node in ${daemon_lustre_file} + - topology is one of graph supported by gg (ring, diring, grid, etc.) + - n is the size of the topology [*] + - an is the action number of the algorithm (1 by default) + +nb: only work for algorithms which node state is made of an integer + +[*] except for grids, where the size of the topology would be n*n + +" + +# 3 or 4 arguments only + if [[ $# < 3 ]] + then + printf "$help" + exit 2 + elif [[ $# = 3 ]] + then + an=1 + else + an=$4 +fi +daemon=$1 +topology=$2 +n=$3 + + if [[ $topology == "grid" ]] + then + size=$(($n * $n)) + else + size=$n + fi + + + +# work in a tmp dir to ease the cleaning +TMP=.tmp +[ -d ${TMP} ] || mkdir ${TMP} +cp Makefile ${TMP} +cp ${GITROOT}/salut/test/Makefile.inc ${TMP} +cp ${GITROOT}/salut/test/Makefile.dot ${TMP} +cp *.ml *.lus ${TMP} + +# to measure the perf, we don't want the algo to stop too soon. +echo "let legitimate = None" >> ${TMP}/config.ml +cd ${TMP} + +main_node=${daemon}_${topology}${n} +outfile=${main_node}.lus +dotfile=${topology}${n}.dot +lusfile=${topology}${n}.lus +lusconstfile=${topology}${n}_const.lus + +make ${dotfile} || (echo "Beware: Makefile.dot should be in the scope of make!"; exit 2) + +salut ${dotfile} + +# XXX state should me made of an integer +config_init=`printf "["; for ((a=1; a < $size ; a++)) do printf "%d," $RANDOM; done; printf "%d]" $RANDOM` + +timestamp=`date +"%d/%m/%Y- %H:%M:%S"` +printf "(* Automatically generated ($timestamp) by '$0 $*' *) + +include \"${daemon_lustre_file}\" +include \"${lusfile}\" +include \"${lusconstfile}\" + +node ${main_node}(any:int)\n\ + returns (p_c : state^${size}; Enab_p : bool^${an}^${size});\n\ +var\n\ + round:bool; round_nb:int;\n\ + initials : state^${size};\n\ +let\n\ + initials = ${config_init};\n\ + p_c, Enab_p, round, round_nb = ${topology}${n}([false] ^ ${size} -> ${daemon}<<$an,$size>>(any, pre Enab_p), initials);\n\ +tel" > $outfile + +echo " +The file '$outfile' has been generated. +To run simulations, you can generate an executable: + + lv6 -2c -cc $outfile -n ${main_node} ${LIB_LUS} -dir ${main_node} + +and run it: + + ./${main_node}.exec + +or, to avoid the need to provide the dummy input: + + (for i in {1..10}; do echo $((((1<<15)| RANDOM))); done ; echo q) | ./${main_node}.exec + (for i in {1..10}; do echo $((((1<<15)| RANDOM))); done ; echo q) | time ./${main_node}.exec > /dev/null +" + diff --git a/salut/test/run-kind2.sh b/salut/test/run-kind2.sh new file mode 100755 index 0000000000000000000000000000000000000000..51e3f70b7e47ffeb5964221ea35796cea0529830 --- /dev/null +++ b/salut/test/run-kind2.sh @@ -0,0 +1,85 @@ +#!/bin/bash +set -x + +GITROOT=$(git rev-parse --show-toplevel) +LIB_LUS="${GITROOT}/test/lustre/round.lus ${GITROOT}/salut/lib/sas.lus" + +help=" +usage: + $0 topology n [property] + +where: + - topology is one of graph supported by gg (ring, diring, grid, etc.) + - n is the size of the topology [*] + - property is one of the verify node (in verify.lus) variable (ok by default) + +[*] except for grids, where the size of the topology would be n*n + +" + +# 2 arguments only + if [[ $# < 2 ]] + then + printf "$help" + exit 2 + elif [[ $# == 2 ]] + then + prop=ok + else + prop=$3 +fi +topology=$1 +n=$2 +main=$1$2 + +if [[ $topology == "grid" ]] + then + size=$(($n * $n)) +else + size=$n +fi + + +kind2_opt="--enable BMC --enable IND --enable INVGEN --timeout 36000" + + +# work in a tmp dir to ease the cleaning +TMP=.tmp-`uname -n` +[ -d ${TMP} ] || mkdir ${TMP} +cp Makefile ${TMP} +cp ${GITROOT}/salut/test/Makefile.inc ${TMP} +cp ${GITROOT}/salut/test/Makefile.dot ${TMP} +cp *.lus ${TMP} +cp ${LIB_LUS} ${TMP} +cd ${TMP} + + +make $main.dot || (echo "Beware: Makefile.dot should be in the scope of make!"; exit 2) + +make ${main}_const.lus + + +#make $main.verify.int8.lv4 +lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -o $main.verify.lv4 + +sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY $prop;\ntel/" $main.verify.lv4 + +cat $main.verify.lv4 | \ + sed -r "s/[ =]((-)?[[:digit:]]+)/ (int8 \1)/g" | \ + sed -r "s/\(((-)?[[:digit:]]+)\)/(int8 \1)/g" | \ + sed -r "s/:int/:int8/g" \ + > $main.verify.int8.lv4 + +start=`date +%s.%N` +time kind2 --color true ${kind2_opt} $main.verify.int8.lv4 +end=`time date +%s.%N` +wallclock=$( echo "$end - $start" | bc -l ) + +timestamp=`date +"%d/%m/%Y-%H:%M:%S"` +algodir=$(dirname $PWD) +algo=$(basename $algodir) + +LC_NUMERIC="en_US.UTF-8" + +printf "| %s | %s | %s | %s | %.2f | %s | %s |\n" $algo ${topology} ${size} \ + $prop $wallclock $timestamp `kind2 --version | cut -d ' ' -f2` >> ../../kind2-result-`uname -n`.org diff --git a/salut/test/salut-vs-sasa.sh b/salut/test/salut-vs-sasa.sh new file mode 100755 index 0000000000000000000000000000000000000000..9250f2c2ae06fb1b38e1d9d385337d2d71ef1132 --- /dev/null +++ b/salut/test/salut-vs-sasa.sh @@ -0,0 +1,63 @@ +#!/bin/bash + set -x + +MY_DIR=$(dirname $(readlink -f $0)) + +source $MY_DIR/gen-salut-batch.sh + +LENGTH=$5 + +################################################################ +lv6 -2c -cc $outfile -n ${main_node} ${LIB_LUS} -dir ${main_node} > lv6_${main_node}.log + +start=`date +%s.%N` + +[ -f ./${main_node}.exec ] && (for (( c=1; c<=$LENGTH; c++ )) ; do echo $((((1<<15)| RANDOM))); done ; echo q) | time ./${main_node}.exec | tail + +end=`date +%s.%N` + +runtime_salut=$( echo "$end - $start" | bc -l ) + +################################################################ +case $daemon in + synchronous) + sasad="-sd" + ;; + central) + sasad="-cd" + ;; + *) + sasas="" + ;; +esac + +make ${topology}${n}.dot +make ${topology}${n}.cmxs + +# set -x +start=`date +%s.%N` +time sasa ${sasad} ${topology}${n}.dot -l ${LENGTH} > sasa_${main_node}.log +end=`time date +%s.%N` + +runtime_sasa=$( echo "$end - $start" | bc -l ) + +################################################################ + +ratio1=$( echo "${runtime_salut} / ${runtime_sasa} * 100 " | bc -l ) +ratio2=$( echo "$runtime_sasa / $runtime_salut * 100 " | bc -l ) + +LC_NUMERIC="en_US.UTF-8" + +printf " ===> speedup = %.2f (%.2f)\n" $ratio1 $ratio2 + +echo "* $0 $* " `date +"%d/%m/%Y- %H:%M:%S"` >> ../result.org +echo " ===> salut a mis $runtime_salut secondes" >> ../result.org +echo " ===> sasa a mis $runtime_sasa secondes" >> ../result.org +printf " ===> speedup = %.2f (%.2f)\n" $ratio1 $ratio2 >> ../result.org + +DATE=`date +"%d/%m/%Y-%H:%M:%S"` +algodir=$(dirname $PWD) +algo=$(basename $algodir) +printf "| %s | %s | %s | %s | %s | %.2f | %.2f | %.2f | %s | %s |\n" \ + ${topology} ${size} $algo $daemon \ + ${LENGTH} $runtime_salut $runtime_sasa $ratio1 $DATE `uname -n` >> ../../result-tab.org \ No newline at end of file