[litmus] add new tests that record the programs' output by psafont · Pull Request #1926 · herd/herdtools7

psafont · 2026-07-22T14:20:55Z

These tests capture the output of the resulting programs to detect
regressions and are meant to run in native architecture that the litmus
tests test. They are also run along the rest of unit tests driven by
dune.

Currently a few tests have been added to demonstrate how these can be
developed into a full suite.

The pre-commit hooks had to be changed to avoid modifying the output
present in the cram test, in both the endline and whitespace checks

Further enhancements for the tests include, adding more parameters to
test, more target architectures.

There's also the addition of cross-architecture tests, using cross-compilers and qemu-user package. These allow running litmus tests on arbitrary architectures, but the dependency setup is more complex. This is why they are not run by default. I've prepared an opam metapackage to submit upstream if we decide to proceed with the approach: ocaml/opam-repository@master...psafont:opam-repository:dev/pau/qemu

The first two commits are code changes I made while inspecting the codebase, and may be dropped if they are too disruptive, I thought there were worthwhile since they show a style I like: they remove code by increasing shared code, and adds unit-tests for the newly shared code to ensure it behaves as expected and won't regress.

psafont · 2026-07-22T14:27:04Z

I need to control better the output of the programs:

--- a/_build/.sandbox/1e71485e728b3185aca35345f52c5b7e/default/litmus/tests/X86_64/A009.t
+++ b/_build/.sandbox/1e71485e728b3185aca35345f52c5b7e/default/litmus/tests/X86_64/A009.t.corrected
@@ -12,12 +12,12 @@ stable
   $ "./$TEST.exe" | sed '$d'
   Test A009 Required
   Histogram (1 states)
-  12000000:>0:rcx=-1;
+  4000000:>0:rcx=-1;
   Ok
   
   Witnesses
-  Positive: 12000000, Negative: 0
+  Positive: 4000000, Negative: 0
   Condition forall (0:rcx=-1) is validated
   Hash=7ca3c35015d75a877ccf509d75062e79
-  Observation A009 Always 12000000 0
+  Observation A009 Always 4000000 0

The lower bounds for alcotest also needs to be set correclty, it can now pick an incompatible version

fsestini

I'm still looking through the PR, but here's some early comments.

fsestini · 2026-07-31T11:07:48Z

+  let destroy () = Filesystem.remove_recursive root in
+  Fun.protect ~finally:destroy (fun () -> f root)
+
+let ( let@ ) f x = f x


Nice trick, I've used it quite a lot as well, in the past.

fsestini · 2026-07-31T11:19:54Z

+      is empty. Calling this function evaluates the first [k] elements of
+      [seq]. *)
+
+  val for_every_element : ('a -> bool) -> 'a Seq.t -> bool


Why not Stdlib.Seq.for_all?

That's because for_all doesn't guarantee that the p is evaluated for every element, i.e it stops evaluating elements as soon as p does not hold.

Got it, makes sense. Maybe just a personal preference, but I'd probably call it something like fold_with_predicate or similar. I feel like seeing the term "fold" would make it unambiguously clear in my head that this function is fully traversing the structure. Not a big deal though.

fsestini · 2026-07-31T11:25:07Z

+  let mapply = Filename.concat (Filename.dirname herd) "mapply7" in
+  mapply, args
+
+let parallelize ?j ~s ~p args = match j with None -> s args | Some j -> p j args


Nit: could we use slightly more informative names for ~s and ~p? E.g. ~para for ~p.

fsestini · 2026-07-31T14:55:21Z


 (ocamllex lexState)
+
+(tests


Note that I think this means dune build @default becomes dependent on alcotest being installed, which is not what we advertise in INSTALL.md and probably also not desirable. Could we make this test stanza optional based on whether alcotest is installed?

The commit changes both INSTALL.md and the opam file.

I can make the tests optional on the presence of alcotest, but I think that removes quite a bit of value from having tests in the first place.

My point was that in INSTALL.md we don't require users to install test dependencies in order to run make all. However, I was wrong about alcotest being needed for make all. I though the chain of calls would be make all -> dune build -> dune build @default, and indeed dune build @default does require alcotest now.
But actually, dune build only resolves to @@default, not @default, so no issues there...

Ah, I see. The names of those rules are not confusing at all...

fsestini · 2026-07-31T16:26:45Z


+For testing, additional dependencies are needed, this can be installed using opam:
+
+    % opam install --deps-only -with-test .


Suggested change

% opam install --deps-only -with-test .

% opam install --deps-only --with-test .

I think this is still unresolved.

These were added years ago to the standard library and is available in all supported versions of OCaml. Signed-off-by: Pau Ruiz Safont <pau.ruizsafont@arm.com>

…ystem; and test them These will be used to share code and simplify existing one for driving regression tests. The unit tests use Alcotest, which has been added as a testing dependency

Now these executables use the same tested code from the Base and Filesystem modules.

The new function does not have to fork into a new process and is faster as a result. Signed-off-by: Pau Ruiz Safont <pau.ruizsafont@arm.com>

This allows future tests for litmus to use the files in them, for example, while excluding them from dune to evaluate rules in them.

These tests allow to tests litmus both the native architecture and use qemu for cross-compilation in linux systems. Currently a few tests have been added to demonstrate how these can be developed into a full suite. The pre-commit hooks had to be changed to avoid modifying the output present in the cram test, in both the endline and whitespace checks These tests have one main advantage over the current tests, they observe the output of running the litmus tests, which makes them better at detecting changes in the output. They also run along the rest of the other unit tests. Further enhancements for the tests include, adding more parameters to test, more target architectures.

Add a smoke test for litmus that uses a cross-compiler and qemu to run a test, similar to the native tests. The current AArch64 test is gated behind the alias `runtest-cross-aarch64`. This is because of the cross-compiler and qemu user-mode requirements. The qemu user-mode can be expressed using an opam package, but the cross-compilers need one package per architecture, which makes it awkward as it will need a conf package per architecture. Furthermore, depending on the distribution the cross-compilers have different names. This means it might need a more robust setup that works on several distributions, maybe zig's cross compilation here can help?

These have steep dependencies, and shouldn't be run when the rest of tests run.

fsestini · 2026-08-07T14:55:25Z

+
+  val for_every_element : ('a -> bool) -> 'a list -> bool
+  (** [for_every_element p lst] returns whether all elements in [lst] hold the
+      property [p]. Every element in the list is evaluated. *)


Maybe we should reword this now that the container is a list rather than a Seq.t:

Suggested change

property [p]. Every element in the list is evaluated. *)

property [p]. [p x] is evaluated for every element [x] in the list. *)

fsestini · 2026-08-07T15:01:54Z

 (* "http://www.cecill.info". We also give a copy in LICENSE.txt.            *)
 (****************************************************************************)

+open! Base.Fun.Syntax


Can we move this to be a let open Base.Fun.Syntax local to get_each_litmus_in_dir, since it's only used there anyway?

fsestini · 2026-08-07T15:48:17Z

+      let entry = Unix.readdir handle in
+      k entry ;
+      read ()
+    with End_of_file -> ()


On a second look, I think this try/with should only be around the call to Unix.readdir. Right now it wraps k entry and read () too, which makes read non-tail-recursive, and silently swallows EOF exceptions raised by k.

I recall the idiom match ... with | exception Foo -> ... being useful in these cases:

let rec read () = match Unix.readdir handle with | entry -> k entry; read () | exception End_of_file -> ()

fsestini · 2026-08-07T16:17:34Z

-      (fun litmus -> litmuses :=  litmus :: !litmuses) in
-  List.rev !litmuses
-
+  (* append in not tail-recursive in 4.14, rev_append forces the reverse sort*)


But then again, List.map is also not tail recursive (modulo cons) in 4.14.

I general it looks to me like this function might potentially allocate quite a bit more compared to the previous version (e.g. it materialises the whole output in a list and does a List.map on it). I would consider implementing litmuses_in as an iterator-returning function to avoid list allocations and preserve the memory behaviour of the previous implementation.

fsestini · 2026-08-07T16:25:50Z


+For testing, additional dependencies are needed, this can be installed using opam:
+
+    % opam install --deps-only -with-test .


I think this is still unresolved.

fsestini · 2026-08-07T16:26:50Z

+  $ mkdir "$TEST"
+  $ litmus7 -set-libdir ../../../libdir -gcc="$GCC" -o "$TEST" \
+  > "../../../../herd/tests/instructions/AArch64/$TEST.litmus" \
+  > -mode std -a 4 -s 1k -r 100


Should there be a trailing \ here?

fsestini · 2026-08-07T16:35:54Z

+  Fun.protect ~finally:close read
+
+let temp_name root =
+  let name = Random.bits64 () in


How does this generator get seeded? Perhaps we need a Random.self_init () somewhere?

fsestini · 2026-08-07T16:47:59Z

Added a few more comments. I think the cram tests look fine, but the changes to internal/ need more work/discussion I think. In light of that, I would consider pulling either the cram tests or the changes to internal/ into a separate PR to be reviewed and merged independently.

psafont force-pushed the dev/pau/litmus-tests branch from 16c504b to f566ac2 Compare July 22, 2026 14:23

psafont force-pushed the dev/pau/litmus-tests branch 7 times, most recently from 54b3ef6 to db3fc3e Compare July 23, 2026 10:25

psafont force-pushed the dev/pau/litmus-tests branch from db3fc3e to b28fad0 Compare July 30, 2026 14:27

fsestini reviewed Jul 31, 2026

View reviewed changes

psafont force-pushed the dev/pau/litmus-tests branch from b28fad0 to 0d6d8f4 Compare July 31, 2026 15:14

fsestini reviewed Jul 31, 2026

View reviewed changes

Comment thread internal/lib/base.mli Outdated

psafont force-pushed the dev/pau/litmus-tests branch from 58f35bb to eac0a09 Compare July 31, 2026 16:19

fsestini reviewed Jul 31, 2026

View reviewed changes

Comment thread internal/lib/filesystem.ml Outdated

fsestini reviewed Jul 31, 2026

View reviewed changes

psafont force-pushed the dev/pau/litmus-tests branch 5 times, most recently from d4a1fc5 to 8d3bcec Compare August 5, 2026 13:10

psafont added 8 commits August 7, 2026 17:12

[internal] remove protect and negate from Fun

98a6339

These were added years ago to the standard library and is available in all supported versions of OCaml. Signed-off-by: Pau Ruiz Safont <pau.ruizsafont@arm.com>

[internal/lib]: Add for_every_element to Base.List, list_dir to Files…

8a43269

…ystem; and test them These will be used to share code and simplify existing one for driving regression tests. The unit tests use Alcotest, which has been added as a testing dependency

[internal] Reuse litmus-gathering code for herd tests

895ba63

Now these executables use the same tested code from the Base and Filesystem modules.

[internal] replace new_temp_dir

e28978b

The new function does not have to fork into a new process and is faster as a result. Signed-off-by: Pau Ruiz Safont <pau.ruizsafont@arm.com>

[herd] allow rules to include libdir and tests/instructions

4d2028b

This allows future tests for litmus to use the files in them, for example, while excluding them from dune to evaluate rules in them.

[litmus] exclude cross-compilation tests from @runtest alias

49d2d7d

These have steep dependencies, and shouldn't be run when the rest of tests run.

psafont force-pushed the dev/pau/litmus-tests branch from 8d3bcec to 49d2d7d Compare August 7, 2026 16:14

fsestini reviewed Aug 7, 2026

View reviewed changes


		For testing, additional dependencies are needed, this can be installed using opam:

		% opam install --deps-only -with-test .

	% opam install --deps-only -with-test .
	% opam install --deps-only --with-test .

	property [p]. Every element in the list is evaluated. *)
	property [p]. [p x] is evaluated for every element [x] in the list. *)

Uh oh!

Conversation

psafont commented Jul 22, 2026

Uh oh!

psafont commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fsestini left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fsestini commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

psafont commented Jul 22, 2026 •

edited

Loading