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