Received-SPF: pass (google.com: domain of linux-kernel+bounces-191204-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45d1:ec00::1 as permitted sender) client-ip=2604:1380:45d1:ec00::1;
Date: Mon, 27 May 2024 12:06:43 -0400
From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: paulmck@kernel.org, parri.andrea@gmail.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,
  akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
  urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
  linux-kernel@vger.kernel.org
Subject: Re: [RFC][PATCH 4/4] tools/memory-model: Distinguish between
 syntactic and semantic tags
Message-ID: <5ce0c8a3-bd9c-475a-9427-7edef47a90f2@rowland.harvard.edu>
References: <20240527152253.195956-1-jonas.oberhauser@huaweicloud.com>
 <20240527152253.195956-5-jonas.oberhauser@huaweicloud.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20240527152253.195956-5-jonas.oberhauser@huaweicloud.com>

On Mon, May 27, 2024 at 05:22:53PM +0200, Jonas Oberhauser wrote:
> Not all tags that are always there syntactically also provide semantic
> membership in the corresponding set. For example, an 'acquire tag on a
> write does not imply that the write is finally in the Acquire set and
> provides acquire ordering.
> 
> To distinguish in those cases between the syntactic tags and actual
> sets, we capitalize the former, so 'ACQUIRE tags may be present on both
> reads and writes, but only reads will appear in the Acquire set.
> 
> For tags where the two concepts are the same we do not use specific
> capitalization to make this distinction.
> 
> Reported-by: Boqun Feng <boqun.feng@gmail.com>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> ---
>  tools/memory-model/linux-kernel.bell |  22 ++--
>  tools/memory-model/linux-kernel.def  | 176 +++++++++++++--------------
>  2 files changed, 99 insertions(+), 99 deletions(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 08fa1ccb1328..045d94a8eabf 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -13,18 +13,18 @@
>  
>  "Linux-kernel memory consistency model"
>  
> -enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
> -		'release (*smp_store_release*) ||
> -		'acquire (*smp_load_acquire*) ||
> -		'noreturn (* R of non-return RMW *) ||
> -		'mb (*xchg(),compare_exchange(),...*)
> +enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) ||
> +		'RELEASE (*smp_store_release*) ||
> +		'ACQUIRE (*smp_load_acquire*) ||
> +		'NORETURN (* R of non-return RMW *) ||
> +		'MB (*xchg(),compare_exchange(),...*)
>  instructions R[Accesses]
>  instructions W[Accesses]
>  instructions RMW[Accesses]
>  
>  enum Barriers = 'wmb (*smp_wmb*) ||
>  		'rmb (*smp_rmb*) ||
> -		'mb (*smp_mb*) ||
> +		'MB (*smp_mb*) ||
>  		'barrier (*barrier*) ||
>  		'rcu-lock (*rcu_read_lock*)  ||
>  		'rcu-unlock (*rcu_read_unlock*) ||
> @@ -38,10 +38,10 @@ instructions F[Barriers]
>  
>  (* Remove impossible tags, such as Acquire on a store or failed RMW *)
>  let FailedRMW = RMW \ (domain(rmw) | range(rmw))
> -let Acquire = Acquire \ W \ FailedRMW
> -let Release = Release \ R \ FailedRMW
> -let Mb = Mb \ FailedRMW
> -let Noreturn = Noreturn \ W
> +let Acquire = ACQUIRE \ W \ FailedRMW
> +let Release = RELEASE \ R \ FailedRMW
> +let Mb = MB \ FailedRMW
> +let Noreturn = NORETURN \ W
>  
>  (* SRCU *)
>  enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
> @@ -81,7 +81,7 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
>  flag ~empty different-values(srcu-rscs) as srcu-bad-value-match
>  
>  (* Compute marked and plain memory accesses *)
> -let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
> +let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | domain(rmw) | range(rmw) |

The new MB term isn't needed, because MB tags on memory accesses are 
filtered out unless the access also belongs to domain(rmw) | range(rmw).

Alan