lkml.org 
[lkml]   [2023]   [Jan]   [18]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
SubjectRe: [PATCH] tools/memory-model: Make ppo a subrelation of po
From
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

\
 
 \ /
  Last update: 2023-03-26 23:46    [W:0.134 / U:0.140 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site