Re: [GIT PULL tools] Linux kernel memory model

[Boqun Feng]

On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote:
[...]
> > - A long term question: have you considered and would it make sense to generate a
> >   memory-barriers.txt like file directly into Documentation/locking/, using the
> >   formal description? That way any changes/extensions/fixes to the model could be
> >   tracked on a high level, without readers having to understand the formal
> >   representation.
> 
> I hadn't considered this at all, actually.  ;-)
> 
> The sections of memory-barriers.txt dealing with MMIO ordering would need
> to stay hand-generated, but they are a very small fraction of the total.
> The herd7 tool is capable of generating cool diagrams sort of like
> this one: https://static.lwn.net/images/2017/mm-model/rmo-acyclic.png,
> which might replace at least some of the hand-generated ASCII-art
> diagrams.
> 

Which reminds me, one thing we could start with is to try to convert all
the examples with litmus tests. Has this been done somewhere (e.g. in
your litmus github repo)? If not, I can try if you think that's a good
idea.

Regards,
Boqun

> Although I do confess harboring some skepticism about being able to
> generated high-quality text, there is no denying that it would be
> valuable to be able to do so.
> 
> > In any case, the base commit is certainly nice and clean and I've pulled it into 
> > tip:locking/core for a v4.17 merge.
> 
> Very good!
> 
> > I believe these additional improvements (to the extent you agree with doing them!) 
> > could/should be done as add-on commits on top of this existing commit.
> 
> Sounds good!
> 
> Would you prefer a pull request or a patch series for these?
> 
> 							Thanx, Paul
>

Attachment: signature.asc
Description: PGP signature