Received-SPF: pass (google.com: domain of linux-kernel+bounces-190750-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.48.161 as permitted sender) client-ip=147.75.48.161;
Message-ID: <7f5a586f-f4b6-4d70-b121-3d82daf54865@huaweicloud.com>
Date: Mon, 27 May 2024 15:47:20 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
 representation
To: Alan Stern <stern@rowland.harvard.edu>,
 Andrea Parri <parri.andrea@gmail.com>
Cc: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>,
 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, paulmck@kernel.org, akiyks@gmail.com,
 dlustig@nvidia.com, joel@joelfernandes.org, linux-kernel@vger.kernel.org,
 linux-arch@vger.kernel.org
References: <20240524151356.236071-1-parri.andrea@gmail.com>
 <1a3c892c-903e-8fd3-24a6-2454c2a55302@huaweicloud.com>
 <ZlSKYA/Y/daiXzfy@andrea>
 <79b55c10-dd06-4947-8545-20ffeb324bc6@rowland.harvard.edu>
From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
In-Reply-To: <79b55c10-dd06-4947-8545-20ffeb324bc6@rowland.harvard.edu>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit


Am 5/27/2024 um 3:37 PM schrieb Alan Stern:
> On Mon, May 27, 2024 at 03:28:00PM +0200, Andrea Parri wrote:
>>>> +    |                smp_store_mb | W[once] ->po F[mb]                        |
>>>
>>> I expect this one to be hard-coded in herd7 source code, but I cannot find
>>> it. Can you give me a pointer?
>>
>> smp_store_mb() is currently mapped to { __store{once}(X,V); __fence{mb}; } in
>> the .def file, so it's semantically equivalent to "WRITE_ONCE(); smp_mb();".
> 
> Why don't we use this approach for all the value-returning full-barrier
> RMW operations?  That would immediately solve the issue of the
> special-purpose code in herd7, leaving only the matter of how to
> annotate failed RMW operations.


I experimented with that the other day. My idea was to use a new 
__fence{mb-successful-rmw} which would have

   Mb = Mb | Mb-successful-rmw & (domain((po\(po;po));rmw) | 
range(rmw;(po\(po;po)))

to turn only the ordering effect of fences around cmpxchg off (and the 
existance of these fences around unsuccessful cmpxchg would be the only 
difference to the current representation).

Unfortunately I didn't manage to get my changes to the .def file to 
compile (FWIW I'm on herd 7.56+03).

Maybe someone wiser with herd can figure out how to work the .def file.

Best wishes,
    jonas