Messages in this thread | ![/](/images/icornerl.gif) | | Date | Wed, 18 Jan 2023 23:02:40 +0100 | Subject | Re: [PATCH] tools/memory-model: Make ppo a subrelation of po | From | 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
| ![\](/images/icornerr.gif) |