[internal] Fix parallel promotion for herd tests

[psafont]

When running or promoting litmus tests in parallel, the parallelizer
runs a wrapper, which runs herd7, each of the stages has its own
parameters. Early 2025 some parameters were added to the wrapper that
runs herd7, but these were not added to the promoter, and since then
parameters have accumulated. Unfortunately the handling of these
parameters was not added to the promoter, causing failures to the
promotion when these parameters are present. We therefore have to find a
way to allow this parameters to be present for the runner while the
promoter can ignore these easily.

This commit solves this by using the common practice of separating the
arguments for the launcher and the launched programs using "--" with a
shared function.

Further work may include changing the wrapper's handling of its own
parameters use Arg, or make the promoter be aware of the arguments.

Opening as a draft to allow @Roman-Manevich to test the promotion of ASL tests

[hrutvik]

Adding @HadrienRenaud to review ASL+herd tests - @psafont said he will provide details on how to run

[psafont]

The fix can be verified by running make test-all-asl REGRESSION_TEST_MODE=promote

[HadrienRenaud]

Hi @psafont, this looks very nice to me, but I'd like to understand a little bit more before approving. Could you please share a before/after of a command that you changed? Thanks

[psafont]

I'd like to understand a little bit more before approving.

Of course, let's run the command for promoting on a branch without the fix:

% make test-all-asl REGRESSION_TEST_MODE=promote
Fatal error: exception Unix.Unix_error(Unix.ENOENT, "create_process", "-nohash")
Fatal error: exception Unix.Unix_error(Unix.ENOENT, "create_process", "-nohash")
[...]
Fatal error: exception Unix.Unix_error(Unix.ENOENT, "create_process", "-nohash")
Fatal error: exception Unix.Unix_error(Unix.ENOENT, "create_process", "-nohash")
Some tests had errors
make: *** [test.herd.inst.ASL] Error 1

With make -n, the command that produces these errors can be seen:

_build/default/internal/herd_regression_test.exe \
                -j 15 \
                -nohash \
                -herd-path _build/install/default/bin/herd7 \
                -libdir-path ./herd/libdir \
                -litmus-dir ./herd/tests/instructions/ASL \
                -conf ./herd/tests/instructions/ASL/ci.cfg \
                promote

Then we modify the internal/herd_promote.ml to print the cli arguments it receives, there's already a guarded expression to print to do this.

The arguments it got called with it is:

_build/default/internal/herd_promote.exe -nohash _build/install/default/bin/herd7 -exit true -set-libdir ./herd/libdir -conf ./herd/tests/instructions/ASL/ci.cfg ./herd/tests/instructions/ASL/write_mem.litmus

We can see that the -no-hash argument snuck up before the location of the herd executable. The code is quite clear here, the command (com) to launch is supposed to be the first argument. This means there has been a breakdown in the interface between the caller and the callee. Similarly, this also happens when adding a -verbose argument.

To fix this, we change the interface that herd_promote.exe and herd_test.exe expose so they can be used in the same way by herd_regression_test.exe.

After the fix the arguments are:

_build/default/internal/herd_promote.exe -nohash -- _build/install/default/bin/herd7 -exit true -set-libdir ./herd/libdir -conf ./herd/tests/instructions/ASL/ci.cfg ./herd/tests/instructions/ASL/globals.litmus

The new code, however uses a different output format to show the semantic meaning that it gives to the argument:

_build/default/internal/herd_promote.exe called with com: _build/install/default/bin/herd7 and args: [-exit; true; -set-libdir; ./herd/libdir; -conf; ./herd/tests/instructions/ASL/ci.cfg; ./herd/tests/instructions/ASL/records.litmus]

Similarly, when test is invoked we can see these arguments with the previous code:

_build/default/internal/herd_test.exe -nohash _build/install/default/bin/herd7 -exit true -set-libdir ./herd/libdir -conf ./herd/tests/instructions/ASL/ci.cfg ./herd/tests/instructions/ASL/records.litmus

and with the new code:

_build/default/internal/herd_test.exe -nohash -- _build/install/default/bin/herd7 -exit true -set-libdir ./herd/libdir -conf ./herd/tests/instructions/ASL/ci.cfg ./herd/tests/instructions/ASL/unknown.litmus

[HadrienRenaud]

Thanks a lot for the explanation, this looks very good to me.

[psafont]

I've added unit-tests for List.split_at. I've noticed that I'm not too fond of the existing pretty printers, they allocate for each stage of the conversion, which can become quite costly for serializing datastructures. In general I would prefer something based on Format.asprintf, which allows to defer the conversion to be done all at once using Format.asprintf "%a" pretty_printer_for_a a. A good library that allows this is https://ocaml.org/p/fmt/latest.

Alcotest combines this with equality tests to have quite succint code, for exmaple, to define a pair of lists of characters, like in the code I added:

let split_at_result_pp = Fmt.Dump.(pair (list char) (list char))
let split_at_result_equal = Pair.equal (List.equal Char.equal) (List.equal Char.equal) 
let split_at_result = Alcotest.testable split_at_result_pp split_at_result_equal

[...]

Alcotest.check split_at_result "split_at must split correctly" expected actual

[fsestini]

In general I'm very much in favour of improving our testing infrastructure, but I also think different code paths warrant different degrees of testing. split_at's implementation seems straightforward, and being a general operation on lists it's very unlikely to ever change. Therefore I wonder whether it adds value to have a test such as this one checked in and run at every make test.

[psafont]

I've found that for long-running project, encoding function behaviours in unit tests is worth it. These are generally very cheap to run, in the order of milliseconds, and they end up being read, or excercised because someone wants to change them because there are curious or there are better that don't need that function. This also helps catching silly mistakes.

One such example is when I replaced several chop functions with split_at: xapi-project/xen-api#6733

Maybe I should rename this function to split_when, as the at seems to indicate a position.

[fsestini]

Maybe I should rename this function to split_when, as the at seems to indicate a position.

I agree. I was thinking split_with but split_when also works.

[fsestini]

I won't approve this yet as I believe @psafont is still working on some parts of this.

[psafont]

I believe that the commit [internal] Recognise the different wrappers for herd (promote and test) Should fix the issue, but I'm still seeing warnings regardings some promotions not having any output.

The last two commits change interfaces for cli tools, and might not be worth merging:

• The first has the issue that the wrapper (herd_test / herd_promote) doesn't drop the last parameter (the litmus test) when launching herd
• The second has the issue that it changes mapply, which is not internal only.

For this reasons I'm leaving this as draft for the time being.