Check parallel (#488)

* Split test in two scripts * Parallel regression done * Code formatting * Build system update to use static libpoly for all builds when configured * Added GNU parallel support * Fixed GNU parallel escaping * Fixed some missing quotes in bash scripts * use full path in output log instead of PID * fixed whitespace * Fixed result printing with hidden error files * Fix path escape * Revert "Build system update to use static libpoly for all builds when configured" This reverts commit 337025a. * Include support for GNU make jobserver * Fixed for newer make versions * Added cleanupto check.sh --------- Co-authored-by: Thomas Hader <[email protected]> Co-authored-by: Thomas Hader <[email protected]> Co-authored-by: Thomas Hader <[email protected]>
SRI-CSL · Feb 21, 2024 · d84ee0a · d84ee0a
1 parent 2f30a0a
commit d84ee0a
Show file tree

Hide file tree

Showing 4 changed files with 298 additions and 142 deletions.
diff --git a/Makefile.build b/Makefile.build
@@ -309,14 +309,14 @@ regress: build_subdirs version
 	@ echo "=== Building binaries ==="
 	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
 	@ echo "=== Running regressions ==="
-	@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
+	+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
 
 
 static-regress: static_build_subdirs version
 	@ echo "=== Building binaries ==="
 	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin
 	@ echo "=== Running regressions ==="
-	@ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin
+	@ $(regressdir)/check.sh -j $(regressdir) $(build_dir)/static_bin
 
 
 .PHONY: all obj static-obj lib static-lib bin static-bin test static-test \

diff --git a/configure.ac b/configure.ac
@@ -578,7 +578,7 @@ if test -z "$1"; then
        if test -f $ldir/libgmp.a; then
           AC_MSG_RESULT(found)
           testlib=$ldir/libgmp.a
-	  CSL_CHECK_GMP($testlib,$testincludedir)
+          CSL_CHECK_GMP($testlib,$testincludedir)
           if test $run_ok = yes; then
             STATIC_GMP=$testlib
             STATIC_GMP_INCLUDE_DIR=$testincludedir

diff --git a/tests/regress/check.sh b/tests/regress/check.sh
@@ -38,17 +38,25 @@ usage() {
    echo "Usage: $0 <test-directory> <bin-directory> [test1] [test2] ..."
    exit
 }
-
+
+cleanup() {
+    [[ -n "$logdir" ]] && rm -rf "$logdir"
+}
+
 smt2_options=
+j_option=
 
-while getopts "s:" o; do
+while getopts "js:" o; do
     case "$o" in
-	s)
-	    smt2_options=${OPTARG}
-	    ;;
-	*)
-	    usage
-	    ;;
+    s)
+      smt2_options=${OPTARG}
+      ;;
+    j)
+      j_option=yes
+      ;;
+    *)
+      usage
+      ;;
     esac
 done
 shift $((OPTIND-1))
@@ -62,13 +70,10 @@ bin_dir=$2
 shift 2
 all_tests="$@"
 
-# Make sure fatal errors go to stderr
-export LIBC_FATAL_STDERR_=1
-
 #
 # System-dependent configuration
 #
-os_name=`uname 2>/dev/null` || os_name=unknown
+os_name=$(uname 2>/dev/null) || os_name=unknown
 
 case "$os_name" in
   *Darwin* )
@@ -81,165 +86,121 @@ case "$os_name" in
 
 esac
 
-#
-# We try bash's builtin time command
-#
-TIMEFORMAT="%U"
-
-
-#
-# Output colors
-#
-red=
-green=
-black=
-if test -t 1 ; then
-  red=`tput setaf 1`
-  green=`tput setaf 2`
-  black=`tput sgr0`
+parallel_tool=
+if command -v parallel &> /dev/null ; then
+    if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then
+        parallel_tool="gnu"
+    else
+        parallel_tool="more"
+    fi
 fi
 
 #
 # The temp file for output
 #
-outfile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; }
-timefile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; }
-
-fail=0
-pass=0
-
-failed_tests=()
+trap cleanup EXIT
+logdir=$($mktemp_cmd -d) || { echo "Can't create temp folder" ; exit 1 ; }
 
 if [[ -z "$REGRESS_FILTER" ]];
 then
-	REGRESS_FILTER="."
+    REGRESS_FILTER="."
 fi
 
-if [[ -z "$TIME_LIMIT" ]];
-then
-  TIME_LIMIT=60
-fi
-
-
 #
 # Check if MCSAT is supported
 #
-./$bin_dir/yices_smt2 --mcsat >& /dev/null < /dev/null
+./"$bin_dir"/yices_smt2 --mcsat >& /dev/null < /dev/null
 if [ $? -ne 0 ]
 then
     MCSAT_FILTER="-v mcsat"
 else
     MCSAT_FILTER="."
 fi
 
-if test -z "$all_tests"; then
+if [ -z "$all_tests" ] ; then
     all_tests=$(
-	find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
-	    grep $REGRESS_FILTER | grep $MCSAT_FILTER |
-	    sort
+    find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
+      grep $REGRESS_FILTER | grep $MCSAT_FILTER |
+      sort
     )
 fi
 
-for file in $all_tests; do
-
-    echo -n $file
-
-    # Get the binary based on the filename
-    filename=`basename "$file"`
-
-    options=
-
-    case $filename in
-        *.smt2)
-            binary=yices_smt2
-	    options=$smt2_options
-            ;;
-        *.smt)
-            binary=yices_smtcomp
-            ;;
-        *.ys)
-            binary=yices
-            ;;
-        *)
-            echo FAIL: unknown extension for $filename
-            fail=`expr $fail + 1`
-            continue
-    esac
+if [ -t 1 ] ; then
+  color_flag="-c"
+fi
 
-    # Get the options
-    if [ -e "$file.options" ]
-    then
-        options="$options `cat $file.options`"
-        echo " [ $options ]"
-    	test_string="$file [ $options ]"
-    else
-        test_string="$file"
-        echo
-    fi
+# job_count 1: serial execution, 0: unrestricted parallel, n>1: n processes
+job_count=1
+
+#check if we are in a make run with -j N
+if [[ -n "$j_option" ]]; then
+    job_count=0
+elif [[ "$MAKEFLAGS" =~ --jobserver-(fds|auth)=([0-9]+),([0-9]+) ]]; then
+    # greedy get as many tokens as possible
+    fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|")
+    fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|")
+    while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do
+      job_count=$((job_count+1))
+    done
+elif [[ "$MAKEFLAGS" =~ --jobserver-auth=fifo:([^ ]+) ]]; then
+    fifo=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-auth=fifo:([^ ]+).*|\1|")
+    while IFS= read -r -d '' -t 1 -n 1 <"$fifo"; do
+      job_count=$((job_count+1))
+    done
+elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then
+    job_count=0
+fi
 
-    # Get the expected result
-    if [ -e "$file.gold" ]
-    then
-        gold=$file.gold
-    else
-        echo -n $red
-        echo FAIL: missing file: $file.gold
-        echo -n $black
-        fail=`expr $fail + 1`
-        failed_tests+=("$test_string")
-        continue
-    fi
+if [[ $job_count != 1 ]] && [[ -z "$parallel_tool" ]]; then
+    echo "**********************************************************"
+    echo "Install moreutils or GNU parallel to run tests in parallel"
+    echo "**********************************************************"
+else
+    case $job_count in
+        0) echo "Running in parallel";;
+        1) echo "Running sequentially";;
+        *) echo "Running with $job_count parallel jobs";;
+    esac
+fi
 
-    # Run the binary
-    (
-      ulimit -S -t $TIME_LIMIT &> /dev/null
-      ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null
-      (time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile
-    )
-    status=$?
-    thetime=`cat $timefile`
-
-    # Do the diff
-    DIFF=`diff -w $outfile $gold`
-
-    if [ $? -eq 0 ] && [ $status -eq 0 ]
-    then
-        echo -n $green
-    	echo PASS [${thetime} s]
-        echo -n $black
-        pass=`expr $pass + 1`
-    else
-        echo -n $red
-        echo FAIL
-        echo -n $black
-        fail=`expr $fail + 1`
-        failed_tests+=("$test_string"$'\n'"$DIFF")
-    fi
+j_param="-j$job_count"
+if [[ $job_count == 0 ]]; then j_param=""; fi
+
+case "$parallel_tool" in
+    more)
+        parallel -i $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests
+        ;;
+    gnu)
+        parallel -q $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests
+        ;;
+    *)
+        for file in $all_tests; do
+            bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir"
+        done
+        ;;
+esac
 
+# give back tokens
+while [[ $job_count -gt 1 ]]; do
+    [[ -n $fdW ]] && echo -n '+' >&"$fdW"
+    [[ -n $fifo ]] && echo -n '+' >"$fifo"
+    job_count=$((job_count-1))
 done
 
-rm $outfile
-rm $timefile
+pass=$(find "$logdir" -type f -name "*.pass" | wc -l)
+fail=$(find "$logdir" -type f -name "*.error" | wc -l)
 
-if [ $fail -eq 0 ]
-then
-    echo -n $green
-    echo Pass: $pass
-    echo Fail: $fail
-    echo -n $black
-else
-    echo -n $red
-    echo Pass: $pass
-    echo Fail: $fail
-    echo -n $black
-fi
+echo "Pass: $pass"
+echo "Fail: $fail"
 
-if [ $fail -eq 0 ]
-then
-    exit 0
+if [ "$fail" -eq 0 ] ; then
+    code=0
 else
-    for i in "${!failed_tests[@]}"; do echo "$((i+1)). ${failed_tests[$i]}"; done
-    exit 1
+    for f in "$logdir"/*.error ; do
+      cat "$f"
+      echo
+    done
+    code=1
 fi
 
-echo -n $black
+exit $code