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;
Date:   Thu, 23 Mar 2023 02:42:08 +0100
From:   Andrea Parri <parri.andrea@gmail.com>
To:     "Paul E. McKenney" <paulmck@kernel.org>
Cc:     linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        kernel-team@meta.com, mingo@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
Subject: Re: [PATCH memory-model scripts 01/31] tools/memory-model:  Document
 locking corner cases
Message-ID: <ZBuucIhuVuoJHljI@andrea>
References: <4e5839bb-e980-4931-a550-3548d025a32a@paulmck-laptop>
 <20230321010549.51296-1-paulmck@kernel.org>
 <ZBrDeoCIs1wmNBeF@andrea>
 <5a32a825-70b3-49d2-9a17-9e5be38e4b72@paulmck-laptop>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <5a32a825-70b3-49d2-9a17-9e5be38e4b72@paulmck-laptop>
Precedence: bulk

> I was surprised by the need to change the "locations" clauses, but
> applied that change anyway.  Ah, I take it that klitmus prints that,
> but doesn't know how to print out a spinlock_t?

Yep, this aligns with my understanding.

  Andrea