Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Paul E. McKenney]

On Thu, Feb 15, 2018 at 07:20:35AM +0900, Akira Yokosawa wrote:
> On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote:
> > On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
> >> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
> >> From: Akira Yokosawa <akiyks@xxxxxxxxx>
> >> Date: Fri, 9 Feb 2018 04:51:05 -0800
> >> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
> >>
> >> As of herd7 7.47, these '-'s are not permitted and end up in
> >> errors such as:
> >>
> >>     File "./linux-kernel.def", line 44, characters 29-30:
> >>     unexpected '-' (in macros)
> >>
> >> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
> >> identifiers match ASPLOS paper") in the repository at
> >> https://github.com/aparri/memory-model can restore the compatibility
> >> with herd7 7.47.
> >>
> >> Reported-by: Patrick Bellasi <patrick.bellasi@xxxxxxx>
> >> Suggested-by: Andrea Parri <parri.andrea@xxxxxxxxx>
> >> Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> >> ---
> >> Paul,
> >>
> >> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> > 
> > Thank you, Akira!
> > 
> > I am going to hold off on this for a bit to see if we can instead get
> > a new release of herd7, but if we can't. this might well be a very good
> > way to go.
> 
> So, herdtools7.7.48 is now available by "opam update; opam upgrade".
> Maybe mentioning the required version of herdtools7 in README would help.

Or have some way for the memory model's .cat files to state what version
they need, but in the meantime please see the patch below.  But even with
such version specification, we probably want to have the version in the
README...

> One glitch I'm aware of is one of the output of klitmus7 fails to
> compile on kernels prior to 4.14, because of smp_mb__after_spinlock()
> used in Z6.0+pooncelock+poonceLock+pombonce.litmus.

This is one advantage of having the memory model in the kernel source
itself -- the versions match.  And people can always fire up a different
kernel version (for example, within a VM) to run the output of klitmus7.

> And there is a question I want to ask.
> 
> Z6.0+pooncelock+pooncelock+pombonce.litmus, which doesn't have
> smp_mb__after_spinlock(), has a comment of:
> 
> (*
>  * Result: Never
>  *
>  * This example demonstrates that a pair of accesses made by different
>  * processes each while holding a given lock will not necessarily be
>  * seen as ordered by a third process not holding that lock.
>  *)
> 
> The result was changed from "Sometimes" to "Never" in response to
> Alan's feedback the other day, but the following comment indicates
> the result should be "Sometimes". And the current model gives the
> result of "Sometimes".
> 
> As I have no idea of the pending patches, I'd like to know once
> the pending patches are applied, would 
> Z6.0+pooncelock+pooncelock+pombonce.litmus and
> Z6.0+pooncelock+poonceLock+pombonce.litmus become identical?

Let's see, examining the Z6 litmus tests and running on herd7 version 7.48:

Z6.0+pooncelock+pooncelock+pombonce Sometimes 1 7
Z6.0+pooncelock+poonceLock+pombonce Never 0 7
Z6.0+pooncerelease+poacquirerelease+mbonceonce Sometimes 1 7

But Alan stated that the result of the test would be changed by one of
the patches in our "pending" list.  I ran with all the patches currently
applied, so I am guessing that Alan was refering to one of the changes
that we have discussed but not yet created.

Alan, enlightenment?

							Thanx, Paul

------------------------------------------------------------------------

commit dad94d8dc78e50bab91b313a67232e85ee22a733
Author: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
Date:   Wed Feb 14 14:37:22 2018 -0800

    tools/memory-model: Add required herd7 version to README file
    
    LKMM and the herd7 tool are co-evolving, and out-of-date herd7 tools
    produce inaccurate results, often with no obvious error messages.  This
    commit therefore adds the required herd7 version to the LKMM README file.
    
    Longer term, it would be good if .cat files could specify the required
    version in a manner allowing herd7 to produce clear diagnostics.
    
    Suggested-by: Akira Yokosawa <akiyks@xxxxxxxxx>
    Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>

diff --git a/tools/memory-model/README b/tools/memory-model/README
index 91414a49fac5..ea950c566ffd 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -20,7 +20,8 @@ that litmus test to be exercised within the Linux kernel.
 REQUIREMENTS
 ============
 
-The "herd7" and "klitmus7" tools must be downloaded separately:
+Version 7.48 of the "herd7" and "klitmus7" tools must be downloaded
+separately:
 
   https://github.com/herd/herdtools7