Re: [PATCH] tools/memory-model: Make ppo a subrelation of po

[Jonas Oberhauser]

Thanks for reviewing the documentation.
You made me realize that the patch is already doing two things -- trying 
to fix the incorrectness of the documentation where it claims that 
fences like strong-fence only relate po-earlier to po-later events, and 
trying to make ppo a subrelation of po.

Perhaps it would be better to do this in two steps. First like you 
suggest only do the ppo fix, and then in a second step (after agreeing 
with Alan on terminology) fix the documentation in a unified way 
(instead of only for strong-fence like in this patch).
Of course you're free to re-state your disagreement about such a change 
then :D

Either way, the specific comments are helpful.

On 1/18/2023 10:30 PM, Andrea Parri wrote:

> > +	Whenever any CPU C' executes an unlock operation U such that
> > +	CPU C executes a lock operation L followed by a po-later
> > +	smp_mb__after_unlock_lock() fence, and L is either a later lock
> > +	operation on the lock released by U or is po-after U, then any
> > +	store that propagates to C' before U must propagate to all other
> > +	CPUs before any instructions po-after the fence are executed on C.
> The barrier is never mentioned in this document.  This is a relatively
> oddball/rare barrier.  Also, IMO, this description doesn't add much to
> the notions of execution and propagation being introduced.  I'd rather
> move it (or parts of it) to ODDS AND ENDS where smp_mb__after_spinlock()
> and other smp_mb__*() are currently briefly described.

I understand your concern.
However, I think the extended strong-order relation needs to be 
mentioned for defining pb. Having a strong ordering operation at this 
point of the manual also helps introducing rcu-fence later which works 
similarly.
I'm hoping if we can make a single renaming patch, we can essentially 
kill most of the explanation of how rcu-fence links events by different 
threads by just pointing to how strong-order is doing the same thing.


> > +While smp_wmb() and release fences only force certain earlier stores
> > +to propagate to another CPU C' before certain later stores propagate
> > +to the same CPU C',
> If "earlier" means po-earlier, this statement is wrong, cf. the comment
> about A-cumulativity.  IAC, it should be clarified.
Indeed I don't mean po-earlier, and agree it should be clarified.
But I'm not sure yet how to clarify "earlier" and "later" considering 
that the precise definition of earlier and later depends on the barrier.

> > strong fences and smp_mb__after_unlock_lock()
> > +force those stores to propagate to all other CPUs before any later
> > +instruction is executed.  We collectively refer to the latter
> > +operations as strong ordering operations, as they provide much
> > +stronger ordering in two ways:
> > +
> > +	Firstly, strong ordering operations also create order between
> > +	earlier stores and later reads.
> Switching back to "execution order" I guess; need clarification.
(Same as above)
> > +
> > +	Secondly, strong ordering operations create a form of global
> > +	ordering: When an earlier store W propagates to CPU C and is
> > +	ordered by a strong ordering operation with a store W' of C,
> > +	and another CPU C' observes W' and in response issues yet
> > +	another store W'', then W'' also can not propagate to any CPU
> > +	before W.  By contrast, a release fence or smp_wmb() would only
> > +	order W and W', but not force any ordering between W and W''.
> > +	To summarize, the ordering forced by strong ordering operations
> > +	extends to later stores of all CPUs, while other fences only
> > +	force ordering with relation to stores on the CPU that executes
> > +	the fence.
> > +
> > +The propagation ordering enforced by release fences and strong ordering
> > +operations affects stores from other CPUs that propagate to CPU C before
> > +the fence is executed, as well as stores that are executed on C before
> > +the fence.  We describe this property by saying that release fences and
> > +strong ordering operations are A-cumulative.  By contrast, smp_wmb()
> > +fences are not A-cumulative; they only affect the propagation of stores
> > +that are executed on C before the fence (i.e., those which precede the
> > +fence in program order).
> [lots of renaming unless I missed something]

The second paragraph is just renaming, but the first part is new.

Best wishes and let me know if you agree on rearranging the submission 
like that,
jonas