[herd] Include some linux tests in the regression testing procedure by maranget · Pull Request #1942 · herd/herdtools7

maranget · 2026-07-31T12:20:21Z

This PR add a few linux kernel memory model tests to our regression suite. The model, configuration files and most tests are taken from Linux sources. A few tests are authored by @akiyks.

relokin · 2026-07-31T12:34:06Z

Thanks for this Luc, this is very useful!

Just one question. Should we move the tests to the catalogue? I see two arguments for doing so:

herd/test should focus on unit tests that are focused on the semantics we implement in herd. Arguably, this is not universally true but I think this would be a good principle to follow.
if we had a catalogue C-lkmm or LKMM we could expose these tests through the web interface.

If you want to maintain the expected files, see here for what I did with a similar requirement https://github.com/herd/herdtools7/pull/1864/changes#diff-76ed074a9305c04054cdebb9e9aad2d818052b07091de1f20cad0bbac34ffb52

maranget · 2026-07-31T12:58:31Z

Exposing some LKMM tests in the web interface looks like a great idea. Nevertheless, I'd realy like to also have some LKMM testing to be part of systematic testing, given the often unforseen impact of some changes on LKMM we experienced in the past. Your solution from PR #1864 can apparently give us both. Should we wait for PR #1864 to be merged?

maranget · 2026-08-10T16:09:17Z

Hi @relokin. I have moved all tests to the now serious "linux" book of the web interface and used your Makefile entry "test.herd.cata-extended.%" to include the tests of the book into the standard test suite (make test).

Web interface: https://diy.inria.fr/TST/www/index.html?record=linux&bell=linux-kernel&cat=linux-kernel&litmus=MP%2Brelacq&cfg=linux-kernel

fsestini · 2026-08-11T08:43:10Z

Could you help me understand the motivation for the new include $dirname? How come other catalogues do not seem to need it?

maranget · 2026-08-11T09:10:46Z

Could you help me understand the motivation for the new include $dirname? How come other catalogues do not seem to need it?

For the linux arch, herd7 loads three files in addition to the configuration file (.cfg): model (.cat), bell file (.bell) and macros (.def). For running herd7 as make test.herd.cata-extended.linux does, I found it convenient to group all these files in the same directory (catalogue/linux/cats) and to specify them in the configuration file. The $dirname trick avoids ising explicit paths. Additionnaly one can invoke the installed herd7 directly on the tests as simply as:

% herd7 -conf catalogue/linux/cfgs/ci.cfg catalogue/linux/tests/*.litmus

Hence the new feature has more to do with herd7 than with the web interface. However it may be necessary to load the `macro file. I am not so sure about the bell file...

Another option would have been to add the -I option to the test driver for it to pass the search path to herd7. This would have been slightl;y more complex.

relokin

Thanks for this Luc, I've got two comments.

relokin · 2026-08-11T11:11:13Z

@@ -0,0 +1,40 @@
+C Z6.0+pooncelock+pooncelock+pombonce


This catalogue has two tests with almost identical names:

Z6.0+pooncelock+pooncelock+pombonce

Z6.0+pooncelock+poonceLock+pombonce

In case-insensitive filesystems (for example, by default APFS on MacOS), this creates problems. Can we change the name of one of the tests?

Nice catch, I am fixing this as you suggest.

relokin · 2026-08-11T11:12:37Z

@@ -0,0 +1,3 @@
+include $dirname/../cats


isn't this very fragile? Is it hard to create a full libdir inside this catalogue?

I do not see what you mean by "full libdir inside this catalogue".

AFAICT, the issue is that the Makefile sets libdir to herd/libdir, while you want herd7 to be able to find linux-kernel.bell, linux-kernel.cat, linux-kernel.def, and lock.cat, which currently live in catalogue/linux/cats.

I can see three possible ways to fix this:

Your approach: extend the list of paths in which herd7 looks for files.

Copy these files into herd/libdir.

Create a complete libdir under catalogue/linux/libdir containing all the .cat, .bell, and .def files needed to run this catalogue.

I think the second and third options are less fragile. More generally, independently of this particular catalogue, I would expect us to want all the files needed to run herd7 with the LKMM model to be available in one place, as that would also make things easier for users.

I would also be in favour of solving this problem with (2) or (3), or other "internal" solution, before considering working around it by changing the public configuration language of herd. I do see the utility in what $dirname proposes, however, user-facing changes come with a maintenance commitment to keep that interface stable, and I think that warrants its own PR and discussion.

The four files linux-kernel.bell, linux-kernel.cat, linux-kernel.def, and lock.cat are from the linux sources and I'd rather have them in the catalogue (with README) than in herd7 standard libdir. Hence I'd rather have solution (3). However, lock.cat includes the files cross.cat and cos-opt.cat. Hence those files would have to be copied into catalogue/linux/libdir. Additionally a stdlib.cat would also have to be copied there. I do not find this that elegant.

fsestini · 2026-08-11T13:12:46Z

Could you help me understand the motivation for the new include $dirname? How come other catalogues do not seem to need it?

For the linux arch, herd7 loads three files in addition to the configuration file (.cfg): model (.cat), bell file (.bell) and macros (.def). For running herd7 as make test.herd.cata-extended.linux does, I found it convenient to group all these files in the same directory (catalogue/linux/cats) and to specify them in the configuration file. The $dirname trick avoids ising explicit paths. Additionnaly one can invoke the installed herd7 directly on the tests as simply as:
% herd7 -conf catalogue/linux/cfgs/ci.cfg catalogue/linux/tests/*.litmus

Thanks for the additional context. As a data point, for the mere purpose of make test and/or CI, I believe it would be enough to write this in ci.cfg:

include catalogue/linux/cats
local-conf linux-kernel.cfg

I realise this only works if herd7 is executed in a working directory that corresponds to the repository root. Such assumption holds for CI, but not necessarily so if a user is running these tests independently from a non-root cwd. @relokin 's suggestions seem to offer more flexibility in that regard.

maranget · 2026-08-11T14:07:37Z

Thanks for the additional context. As a data point, for the mere purpose of make test and/or CI, I believe it would be enough to write this in ci.cfg:
include catalogue/linux/cats
local-conf linux-kernel.cfg
I realise this only works if herd7 is executed in a working directory that corresponds to the repository root. Such assumption holds for CI, but not necessarily so if a user is running these tests independently from a non-root cwd. @relokin 's suggestions seem to offer more flexibility in that regard.

I follow your suggestion, which provides a simple and workable solution.

The regression consists in not marking some effects as being a data port, resulting in less dependencies. However, by contrast with C11 models, the LKMM sometimes relies on dependencies.

maranget · 2026-08-11T14:31:48Z

Hi @relokin abd @fsestini. I have followed @fsestini's simple suggestion for configuring the CI testing of LKMM and removed the "$dirname" feature. I have also fixed a long-standing bug that the new test set unveiled, see commit 3867397.

fsestini

Thanks for the changes @maranget .

relokin

LGTM, thanks Luc!

The new book includes: - Linux Kernel Memory Model at date, copied from linux sources (https://github.com/torvalds/linux/tree/master/tools/memory-model) - Some litmus tests taken from linux sources (see above) and from the "perfbook" (https://kernel.googlesource.com/pub/scm/linux/kernel/git/paulmck/perfbook/+/refs/heads/master/CodeSamples/formal/herd/) by "Paul E. McKenney" <paulmck@kernel.org>. Those tests were suggested to us by "Akira Yokosawa" <akiyks@gmail.com>.

To that aim we use the extension introduced by PR #1864.

maranget · 2026-08-11T15:39:31Z

Merged thanks a lot @relokin and @fsestini for your suggestions.

maranget changed the title ~~[herd] Include some linux tests in the regression testing proceddure~~ [herd] Include some linux tests in the regression testing procedure Jul 31, 2026

maranget force-pushed the test-lkmm branch 2 times, most recently from 633a4d5 to 0efa116 Compare August 10, 2026 15:50

maranget force-pushed the test-lkmm branch from 0efa116 to 2364244 Compare August 10, 2026 16:14

HadrienRenaud reviewed Aug 10, 2026

View reviewed changes

Comment thread herd/lexConf_herd.mll Outdated

maranget force-pushed the test-lkmm branch 2 times, most recently from 2ff3c33 to cad0a90 Compare August 11, 2026 09:04

relokin reviewed Aug 11, 2026

View reviewed changes

maranget force-pushed the test-lkmm branch from cad0a90 to 9eb3a62 Compare August 11, 2026 11:46

[herd] Fix regression introduced by PR #1179

3867397

The regression consists in not marking some effects as being a data port, resulting in less dependencies. However, by contrast with C11 models, the LKMM sometimes relies on dependencies.

maranget force-pushed the test-lkmm branch from 9eb3a62 to dc659b5 Compare August 11, 2026 14:28

fsestini approved these changes Aug 11, 2026

View reviewed changes

relokin approved these changes Aug 11, 2026

View reviewed changes

maranget added 2 commits August 11, 2026 17:21

[test] Include the linux book from the catalogue in standard test suite.

dd7783f

To that aim we use the extension introduced by PR #1864.

maranget force-pushed the test-lkmm branch from dc659b5 to dd7783f Compare August 11, 2026 15:21

maranget merged commit 4fb4cab into master Aug 11, 2026
5 checks passed

maranget deleted the test-lkmm branch August 11, 2026 15:39

maranget mentioned this pull request Aug 11, 2026

[herd] Add special clause include $dirname... in configuration file #1961

Draft

Uh oh!

Conversation

maranget commented Jul 31, 2026

Uh oh!

relokin commented Jul 31, 2026

Uh oh!

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

Uh oh!

Uh oh!

maranget commented Aug 10, 2026

Uh oh!

Uh oh!

fsestini commented Aug 11, 2026

Uh oh!

maranget commented Aug 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

relokin left a comment

Choose a reason for hiding this comment

Uh oh!

relokin Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

maranget Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

relokin Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

relokin Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

maranget Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

relokin Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

fsestini Aug 11, 2026

Choose a reason for hiding this comment

Uh oh!

maranget Aug 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fsestini commented Aug 11, 2026

Uh oh!

maranget commented Aug 11, 2026

Uh oh!

maranget commented Aug 11, 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!

relokin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

maranget commented Aug 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

maranget commented Jul 31, 2026 •

edited

Loading

maranget commented Aug 11, 2026 •

edited

Loading

maranget Aug 11, 2026 •

edited

Loading

maranget commented Aug 11, 2026 •

edited

Loading