Received-SPF: pass (google.com: domain of linux-kernel+bounces-191308-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:4601:e00::3 as permitted sender) client-ip=2604:1380:4601:e00::3;
Message-ID: <5a9bc579-01ad-0b0f-bcba-c8f0bd932331@huaweicloud.com>
Date: Mon, 27 May 2024 19:57:41 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.13.0
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
 representation
Content-Language: en-US
To: Andrea Parri <parri.andrea@gmail.com>
Cc: 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, paulmck@kernel.org,
 akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
 linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
 jonas.oberhauser@huaweicloud.com
References: <20240524151356.236071-1-parri.andrea@gmail.com>
 <1a3c892c-903e-8fd3-24a6-2454c2a55302@huaweicloud.com>
 <ZlSKYA/Y/daiXzfy@andrea>
From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
In-Reply-To: <ZlSKYA/Y/daiXzfy@andrea>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit

On 5/27/2024 3:28 PM, 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();".

Ok, so some fences where added in the .def file (this) while other 
programmatically (e.g., xchg). We should at least be consistent about 
how this is done. Based on previous comments, it seems most of us agree 
this should go the the .def file.

> 
> 
>> What about spin_unlock?
> 
> spin_unlock() is listed among the non-RMW ops/macros in the current table: it
> is represented by a single UL or "Unlock" event (a special type of Store event
> with (some special) Release semantics).

I was blind. Sorry for the noise.

> 
> 
>> I found the extra spaces in the failure case very hard to read. Any
>> particular reason why you went with this format?
> 
> The extra spaces were simply to convey something like "belong to the previous
> row/entry", but I'm open to remove them or other suggestions if preferred.

I find it easier to read without the extra spaces. The empty column on 
the left already tells me this is a continuation of the previous row.
But I don't see this as a blocker.

> 
>    Andrea