On Wed, Mar 03, 2021 at 06:39:14PM +0100, maranget wrote: > > > > On 3 Mar 2021, at 18:37, maranget <luc.maranget@xxxxxxxx> wrote: > > > > I have made a PR to herd7 that performs the change. The commit message states the new definition. > > For those who are interested > <https://github.com/herd/herdtools7/pull/183> And I just confirmed that with this change, Björn's original litmus test behaves as desired. Merci beaucoup, Luc! The new herd7 also passes the in-kernel regression test, and also all of the github "litmus" archive's tests up to six processes that are flagged with expected outcomes except for these five tests, which are expected failures: litmus/manual/deps/LB-addr-equals.litmus litmus/manual/deps/LB-ctls-bothvals-a.litmus litmus/manual/deps/LB-ctls-diffvals-det.litmus litmus/manual/deps/LB-ctls-sameval-barrier.litmus litmus/manual/deps/LB-ctls-sameval.litmus This situation is a bit silly, so I changed the "Results" clause and added a comment noting that LKMM does not yet know about these corner cases. I just started a longer regression test, but this will take some time. Thanx, Paul