Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20;
Message-ID: <4a917e54-d029-9341-aef4-a447746b7743@huaweicloud.com>
Date:   Wed, 18 Jan 2023 23:02:40 +0100
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.6.1
Subject: Re: [PATCH] tools/memory-model: Make ppo a subrelation of po
To:     Andrea Parri <parri.andrea@gmail.com>
Cc:     paulmck@kernel.org, stern@rowland.harvard.edu, will@kernel.org,
        peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
        dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
        akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
        urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
        linux-kernel@vger.kernel.org
References: <20230117193159.22816-1-jonas.oberhauser@huaweicloud.com>
 <Y8hk6JrUXei6ZInI@andrea>
From:   Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <Y8hk6JrUXei6ZInI@andrea>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Precedence: bulk

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