[herd] report timeouts when running tests

catalogue/aarch64-VMSA/shelf.py

@@ -10,10 +10,10 @@
 
 illustrative_tests = [
     "tests/A031.litmus",
-    "tests/2+2WNExpExp+NExpExp+DMBST+DMBST+SHOW.litmus",
-    "tests/2+2WNExpExp+NExpExp+DMBST+DMBST.litmus",
-    "tests/2+2WNExpExp+NExpExp+SHOW.litmus",
-    "tests/2+2WNExpExp+NExpExp.litmus",
+    "tests/2+2WNExpExp+NExpNExp+DMBST+DMBST+SHOW.litmus",
+    "tests/2+2WNExpExp+NExpNExp+DMBST+DMBST.litmus",
+    "tests/2+2WNExpExp+NExpNExp+SHOW.litmus",
+    "tests/2+2WNExpExp+NExpNExp.litmus",
     "tests/Artem2+TLBIx-HDy+dsb.ish.litmus",
     "tests/Artem2+TLBIx-TLBIy+dmb2.litmus",
     "tests/Artem2+TLBIx-UCy+dsb.ish.litmus",

doc/Makefile

@@ -247,10 +247,9 @@ clean::
 	/bin/rm -f version.tex
 
 #HTML
-HEVEABIN=/usr/local/bin
-HEVEA=$(HEVEABIN)/hevea
+HEVEA=hevea
 HEVEAOPTS=-fix -exec xxdate.exe -O
-HACHA=$(HEVEABIN)/hacha
+HACHA=hacha
 HACHAOPTS=-tocter
 
 dochtml: html/index.html

doc/herd.tex

@@ -481,7 +481,7 @@ \subsection{Computing \label{sec:cos}coherence orders}
 \end{verbatim}
 Where the pre-defined sets \texttt{IW} and~\texttt{FW} are the sets
 of all initial and final writes respectively.
-%TODO exemple of co0 on 2+2W
+%TODO example of co0 on 2+2W
 
 Then, assuming that $W_x$ is the set of all writes to location~$x$, one
 can compute the set of all possible coherence orders for~$x$ with
@@ -855,7 +855,7 @@ \subsection{\label{overview}Overview}
 There are two structured values: tuples of values and sets of values.
 One should notice that primitive set of events and structured set of events are not the same
 thing. In fact, the language prevents the construction of structured set of events.
-Similarily, there are no structured sets of elements of relations, there are only relations.
+Similarly, there are no structured sets of elements of relations, there are only relations.
 
 \item There is a distinction between expressions that evaluate
 to some value, and instructions that are executed for their effect.
@@ -1308,7 +1308,7 @@ \subsubsection*{\label{sec:check}Checks}
 evaluates \nt{expr} and applies the check \nt{check}.
 There are six checks: the three basic acyclicity (keyword~\T{acyclic}),
 irreflexivity (keyword~\T{irreflexive})
-and emptyness (keyword~\T{empty}); and their
+and emptiness (keyword~\T{empty}); and their
 negations.
 If the check succeeds, execution goes on. Otherwise, execution stops.
 
@@ -1902,7 +1902,7 @@ \subsection{Options}
 \item[{\tt -texmacros <bool>}] Use latex commands in some text of pictures.
 If activated (\opt{-showthread true}), thread numbers are shown as
 \verb+\myth{+$n$\verb+}+. Assembler instructions are locations in nodes
-are argument to an \verb+\asm+ command. It user responsability to define
+are argument to an \verb+\asm+ command. It user responsibility to define
 those commands in their \LaTeX{} documents that include the pictures.
 Possible definitions are \verb+\newcommand{\myth}[1]{Thread~#1}+
 and \verb+\newcommand{\asm}[1]{\texttt{#1}}+.
@@ -1935,7 +1935,7 @@ \subsection{Options}
 \item[{\tt -squished <bool>}] The setting \opt{-squished true} drastically
 limits the information displayed in graph nodes. This is usually what
 is wanted in modes \opt{free} and~\opt{columns}. Default is~\opt{false}.
-\item[{\tt -fixedsize <bool>}] This setting is meaningfull in
+\item[{\tt -fixedsize <bool>}] This setting is meaningful in
 \opt{columns} graph mode and for squished nodes. When set by
 \opt{-fixedsize true} it forces node width to be $65\%$ of the space
 between columns. This may sometime yield a nice edge routing. Default is~\opt{false}
@@ -2095,6 +2095,16 @@ \subsection{\label{herd:searchpath}File searching}
 and then in herd installation directory, which is defined
 while compiling~\herd.
 
+
+\subsection{\label{herd:exitstatus}Exit Status}
+\herd{} exits with different status depending on the errors it encounters while running:
+\begin{description}
+\item[{\tt 0}] All test executions were successful.
+\item[{\tt 1}] A test execution encountered an unexpected internal error (bug).
+\item[{\tt 2}] A test execution encountered a fatal or a user error.
+\item[{\tt 154}] A test execution was interrupted because of a timeout.
+\end{description}
+
 %\section{Extensions to Herd}
 %
 %\begin{quote}\it

herd/herd.ml

@@ -27,6 +27,7 @@ open OptNames
 
 let exit_code_of_exn = function
   | Misc.Exit | Misc.UserError _ | Misc.Fatal _ -> 2
+  | Misc.Timeout -> 128 + 26 (* SIGVTALRM *)
   | _ -> 1
 
 (* Command line arguments *)
@@ -808,10 +809,13 @@ let () =
       (fun _ -> raise Misc.Timeout)
       !debug.Debug_herd.timeout;
     Misc.fold_argv_or_stdin
-      (fun name ((exit_code, seen) as r) ->
+      (fun name (exit_code, seen) ->
         try exit_code, from_file name seen
         with
-        | Misc.Timeout -> r
+        | Misc.Timeout as e ->
+           if dbg_exc then raise e ;
+           Warn.warn_always "%a: timed out" Pos.pp_pos0 name ;
+           check_exit e seen
         | Misc.Exit as e ->
            if dbg_exc then raise e ;
            check_exit e seen

herd/itimer.ml

@@ -32,7 +32,7 @@ let set_signal timeout f dbg =
            f s
        else f in
      Sys.set_signal
-       26 (* SIGVTALARM *)
+       26 (* SIGVTALRM *)
        (Sys.Signal_handle g)
 
 let start n timeout =

herd/tests/other/timeout-report.t/Armv8-ext-forbidden000018.litmus

@@ -0,0 +1,25 @@
+AArch64 Armv8-ext-forbidden000018
+"TLBI-sync.ISHdWWPteAF0P Rfe DpAddrdR LxSx PosWRPA FreAPteAF0"
+Cycle=Rfe DpAddrdR LxSx PosWRPA FreAPteAF0 TLBI-sync.ISHdWWPteAF0P
+Relax=[Fre,PteAF0,TLBI-sync.ISHdWW]
+Safe=Rfe DpAddrdR [LxSx,PosWR,A]
+Generator=diy7 (version 7.58+1)
+Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
+Com=Rf Fr
+Orig=TLBI-sync.ISHdWWPteAF0P Rfe DpAddrdR LxSx PosWRPA FreAPteAF0
+{ int y=0x4;
+0:X0=PTE(x); 0:X1=(oa:PA(x), af:0); 0:X3=y; 0:X4=x;
+1:X3=y; 1:X4=x;
+}
+ P0              | P1                ;
+ STR X1,[X0]     | LDR W2,[X3]       ;
+ DSB ISH         | MOV W8,#1         ;
+ LSR X5,X4,#12   | EOR W5,W2,W2      ;
+ TLBI VAAE1IS,X5 | ADD X6,X4,W5,SXTW ;
+ DSB ISH         | Loop00:           ;
+ MOV W2,#5       | L00:              ;
+ STR W2,[X3]     | LDXR W7,[X6]      ;
+                 | STXR W9,W8,[X6]   ;
+                 | CBNZ W9,Loop00    ;
+                 | LDAR W10,[X4]     ;
+exists (1:X2=0x5 /\ 1:X7=0x0 /\ 1:X10=0x1 /\ ~Fault(P1:L00,x))

herd/tests/other/timeout-report.t/run.t

@@ -0,0 +1,11 @@
+Force test timeouts by picking an expensive test and setting the timeout to a
+single millisecondand observe the timeout is applied for every litmus test
+
+  $ herd7 -set-libdir ../libdir -timeout 0.001 Armv8-ext-forbidden000018.litmus Armv8-ext-forbidden000018.litmus Armv8-ext-forbidden000018.litmus
+  Warning: File "Armv8-ext-forbidden000018.litmus": timed out
+  Warning: File "Armv8-ext-forbidden000018.litmus": timed out
+  Warning: File "Armv8-ext-forbidden000018.litmus": timed out
+  [154]
+
+Note that 154 is generated by adding SIGVTALRM 26, and 128, because the
+execution got interrupted by a signal.

internal/diy_regression_test.ml

@@ -42,8 +42,10 @@ let do_run flags =
     |> Fun.flip List.nth 1
     |> String.trim in
     cycles := cycle :: !cycles in
-  (* ignore the output to stderr *)
-  Command.NonBlock.run ~stdout:read_line ~stderr:(fun _ -> ()) flags.diy (diy_argument flags);
+  let ignore _ = () in
+  let raise_e e = failwith (Command.string_of_error e) in
+  Command.NonBlock.run ~stdout:read_line ~stderr:ignore flags.diy (diy_argument flags)
+  |> Result.fold ~ok:ignore ~error:raise_e ;
   StringSet.of_list !cycles
 
 let run_tests flags =

internal/diyone_test.ml

@@ -57,9 +57,12 @@ let run_diyone flags command =
     "/bin/sh" ["-c";shell_command] in
   let comment =
     match status,!stderr with
-    | 0,stderr -> stderr
-    | status,"" -> Printf.sprintf "[%d]" status
-    | status,stderr -> Printf.sprintf "[%d]\n%s" status stderr in
+    | Ok 0,stderr -> stderr
+    | Ok status,"" -> Printf.sprintf "[%d]" status
+    | Ok status,stderr -> Printf.sprintf "[%d]\n%s" status stderr
+    | Error err, stderr ->
+        Printf.sprintf "[%s]\n%s" (Command.string_of_error err) stderr
+  in
   match comment,!stdout with
   | "",stdout -> stdout
   | comment,"" -> Printf.sprintf "(*\n%s\n*)" comment

internal/herd_assumptions_test.ml

@@ -111,12 +111,14 @@ let run flags =
       (fun remaining_flags (dir, conf) ->
         Printf.printf "Checking assumptions against %s ...\n%!" dir;
         let litmuses = get_each_litmus_in_dir dir in
+        let raise_e e = failwith (Command.string_of_error e) in
         let remaining_flags =
           List.fold_left
             (fun remaining_flags litmus ->
               let _, stdout, stderr =
                 TestHerd.run_herd ~bell:None ~cat:(Some flags.assumptions_file)
                   ~conf ~variants:[] ~libdir:flags.libdir flags.herd [ litmus ]
+                |> Result.fold ~ok:Fun.id ~error:raise_e
               in
               let stdout = String.concat "\n" stdout in
               let stderr = String.concat "\n" stderr in

internal/herd_catalogue_regression_test.ml

@@ -69,6 +69,9 @@ let (>>=) o1 o2 = match o1 with
 | "" -> o2
 | _ -> Some o1
 
+type herd_kinds =
+  | Kinds of (string * ConstrGen.kind) list
+  | Timeout of string list
 
 let herd_kinds_of_permutation ?j ?timeout flags shelf_dir litmuses p =
   let prepend path = Filename.concat shelf_dir path in
@@ -84,13 +87,18 @@ let herd_kinds_of_permutation ?j ?timeout flags shelf_dir litmuses p =
       flags.herd ?j ?timeout
   in
   match cmd litmuses with
-  | 0,stdout, [] ->
+  | Ok (0, stdout, []) ->
       let kind_of_log l = Log.(l.name, Option.get l.kind) in
-      List.map kind_of_log (Log.of_string_list stdout)
-  | _, _, stderr ->
+      Kinds (List.map kind_of_log (Log.of_string_list stdout))
+  | Ok (ec, _, _) when ec = 128 + 26 -> (* SIGVTALRM *)
+      Timeout litmuses
+  | Ok (_, _, stderr) ->
       let lines = String.concat "\n" stderr in
       let msg = Printf.sprintf "Herd returned stderr:\n%s" lines in
       raise (Error msg)
+  | Result.Error e ->
+      let msg = Printf.sprintf "Herd returned error: %s" (Command.string_of_error e) in
+      raise (Error msg)
 
 
 (* Shelves. *)
@@ -115,6 +123,8 @@ let exit_1_if_any_files_missing ~description paths =
       List.iter (Printf.printf "Missing %s: %s\n" description) missing ;
       raise (Error "Some files are missing")
 
+let short_test_name path = Misc.filebase path
+
 (* Commands. *)
 
 let show_tests ?j ?timeout flags =
@@ -143,53 +153,72 @@ let show_tests ?j ?timeout flags =
 let run_tests ?j ?timeout flags =
   let cat, shelf_dir, tests =
     first_of_shelf flags.shelf_path flags.index_path in
+  let catalogue = Filename.basename shelf_dir in
 
   exit_1_if_any_files_missing ~description:"test" tests ;
   exit_1_if_any_files_missing ~description:"kinds.txt file" [flags.kinds_path] ;
 
   let result_of_permutation kinds_path p =
     let expected = Kinds.of_file kinds_path in
-    let actual =
-      herd_kinds_of_permutation ?j ?timeout flags shelf_dir tests p in
-    let diff,miss,excess = Kinds.check ~expected ~actual in
-    if Misc.consp miss then begin
-      let pf =
-        match miss with
-        | [_] -> Printf.eprintf "Warning: test %s is not in reference kind file %s\n"
-        | _ -> Printf.eprintf "Warning: tests %s are not in reference kind file %s\n" in
-      pf (String.concat "," miss) kinds_path
-      end ;
-     if Misc.consp excess then begin
-      let pf =
-        match excess with
-        | [_] -> Printf.eprintf "Warning: test %s is not in test base\n"
-        | _ -> Printf.eprintf "Warning: tests %s are not in test base\n" in
-      pf (String.concat "," excess) 
-      end ;
-    match diff with
-    | [] -> true
-    | rs ->
-        let pp =
-          List.map
-            (fun (n,ke,ka) ->
-              Printf.sprintf "%s: expected=%s, actual=%s"
-                n (ConstrGen.pp_kind ke) (ConstrGen.pp_kind ka))
-            rs in
-        Printf.printf "Kinds differs: kinds file = %s ; %s\n"
-          kinds_path (string_of_permutation p) ;
-        List.iter (Printf.printf "%s\n") pp ;
-        false in
+    match herd_kinds_of_permutation ?j ?timeout flags shelf_dir tests p with
+    | Timeout litmuses ->
+        let pf =
+          ( match litmuses with
+          | [_] -> Printf.eprintf "Warning: a test timed out in catalogue %s: %s\n"
+          | _ -> Printf.eprintf "Warning: tests timed out in catalogue %s: %s\n"
+          )
+        in
+        pf catalogue
+          (String.concat ", "
+             (List.map short_test_name litmuses)) ;
+        Result.Error ()
+    | Kinds actual ->
+        let diff,miss,excess = Kinds.check ~expected ~actual in
+        if Misc.consp miss then begin
+          let pf =
+            match miss with
+            | [_] -> Printf.eprintf "Warning: test %s is not in reference kind file %s\n"
+            | _ -> Printf.eprintf "Warning: tests %s are not in reference kind file %s\n" in
+          pf (String.concat "," miss) kinds_path
+          end ;
+         if Misc.consp excess then begin
+          let pf =
+            match excess with
+            | [_] -> Printf.eprintf "Warning: test %s is not in test base\n"
+            | _ -> Printf.eprintf "Warning: tests %s are not in test base\n" in
+          pf (String.concat "," excess)
+          end ;
+        match diff with
+        | [] -> Ok ()
+        | rs ->
+            let pp =
+              List.map
+                (fun (n,ke,ka) ->
+                  Printf.sprintf "%s: expected=%s, actual=%s"
+                    n (ConstrGen.pp_kind ke) (ConstrGen.pp_kind ka))
+                rs in
+            Printf.printf "Kinds differs: kinds file = %s ; %s\n"
+              kinds_path (string_of_permutation p) ;
+            List.iter (Printf.printf "%s\n") pp ;
+            Result.Error () in
   let passed = result_of_permutation flags.kinds_path cat in
-  if not passed then exit 1
+  if passed <> Ok () then exit 1
 
 
 let promote_tests ?j flags =
   let cat, shelf_dir, tests =
     first_of_shelf flags.shelf_path flags.index_path in
+  let catalogue = Filename.basename shelf_dir in
   exit_1_if_any_files_missing ~description:"tests" tests ;
 
   let kinds =
-    herd_kinds_of_permutation ?j flags shelf_dir tests cat
+    match herd_kinds_of_permutation ?j flags shelf_dir tests cat with
+    | Kinds kinds -> kinds
+    | Timeout litmuses ->
+        Printf.eprintf "Warning: timeout for tests in catalogue %s: %s\n"
+          catalogue (String.concat "; "
+             (List.map short_test_name litmuses)) ;
+        []
   in
   Filesystem.write_file flags.kinds_path
     (fun o -> output_string o (Kinds.to_string kinds))