run_tests: Create and fetch timing/timeout info.

misc/regression/run_tests.py

@@ -300,6 +300,8 @@ def run_test(test, status_queue, kill_switch, verbose=False, stuck_timeout=None,
 
     if output is None:
         output = ""
+    if test_status[0] in [STUCK, TIMEOUT, CPU_TIMEOUT]:
+        output = output + extra_timeout_output(test.name)
     output = output.decode(encoding='utf8', errors='replace')
 
     status_queue.put({'name': test.name,
@@ -309,6 +311,17 @@ def run_test(test, status_queue, kill_switch, verbose=False, stuck_timeout=None,
                       'cpu_time': cpu_usage,
                       'mem_usage': peak_mem_usage})
 
+# run a heuristic script for getting some output on a timeout
+def extra_timeout_output(test_name):
+    command = [os.path.join('misc', 'regression', 'timeout_output'), test_name]
+    try:
+        process = subprocess.Popen(command,
+                stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+        (output, _) = process.communicate()
+    except Exception, e:
+        output = "Exception launching timeout_output: %s" % str(e)
+    return output
+
 # Print a status line.
 def print_test_line_start(test_name):
     if sys.stdout.isatty():
@@ -406,6 +419,9 @@ def main():
     if args.list:
         for t in tests:
             print(t.name)
+            if args.verbose:
+                print('  #> cd ' + t.cwd)
+                print('  #> ' + t.command)
         sys.exit(0)
 
     args.exclude = set(args.exclude)

misc/regression/timeout_output

@@ -0,0 +1,29 @@
+#! /bin/bash
+#
+#
+# Copyright 2017, Data61, CSIRO
+#
+# This software may be distributed and modified according to the terms of
+# the BSD 2-Clause license. Note that NO WARRANTY is provided.
+# See "LICENSE_BSD2.txt" for details.
+#
+# @TAG(DATA61_BSD)
+#
+#
+
+OUTDIR=$(./isabelle/bin/isabelle env bash -c 'echo "$ISABELLE_OUTPUT"')
+FILE="$OUTDIR/log/$1_times.txt"
+
+if [[ -e $FILE ]]
+then
+  echo Long running tasks for "$1":
+  grep '^Long' $FILE | tail -n 10
+  echo
+  echo final timing log:
+  tail -n 10 $FILE
+  echo
+  echo "  (more information might be found in $FILE)"
+else
+  echo No timing log for "$1" was found.
+  echo "  (in $FILE)"
+fi

run_tests

@@ -42,6 +42,9 @@ if L4V_ARCH not in L4V_ARCH_LIST:
 
 print "Testing for L4V_ARCH=%s:" % L4V_ARCH
 
+# enable timing logs in isabelle builds and set report interval to 3 seconds
+os.environ["ISABELLE_TIMING_LOG"]="3.0s"
+
 # Enable quick_and_dirty mode for various images
 if os.environ.has_key("QUICK_AND_DIRTY"):
     os.environ["AINVS_QUICK_AND_DIRTY"]=1