On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote:
[...]

quoted

- 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.

quoted

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!

quoted

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