Re: [PATCH] tools/memory-model: Document herd7 (internal) representation

[Andrea Parri]

> > +    |                smp_store_mb | W[once] ->po F[mb]                        |
> 
> I expect this one to be hard-coded in herd7 source code, but I cannot find
> it. Can you give me a pointer?

smp_store_mb() is currently mapped to { __store{once}(X,V); __fence{mb}; } in
the .def file, so it's semantically equivalent to "WRITE_ONCE(); smp_mb();".


> What about spin_unlock?

spin_unlock() is listed among the non-RMW ops/macros in the current table: it
is represented by a single UL or "Unlock" event (a special type of Store event
with (some special) Release semantics).


> I found the extra spaces in the failure case very hard to read. Any
> particular reason why you went with this format?

The extra spaces were simply to convey something like "belong to the previous
row/entry", but I'm open to remove them or other suggestions if preferred.

  Andrea