Message-ID: <4a917e54-d029-9341-aef4-a447746b7743@huaweicloud.com>
Date:   Wed, 18 Jan 2023 23:02:40 +0100
From:   Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To:     Andrea Parri <parri.andrea@...il.com>
Cc:     paulmck@...nel.org, stern@...land.harvard.edu, will@...nel.org,
        peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
        dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
        akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
        urezki@...il.com, quic_neeraju@...cinc.com, frederic@...nel.org,
        linux-kernel@...r.kernel.org
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po

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

Powered by blists - more mailing lists