Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
From: Jonas Oberhauser
Date: Mon Jan 23 2023 - 14:41:06 EST
On 1/23/2023 4:55 PM, Alan Stern wrote:
On Mon, Jan 23, 2023 at 12:48:42PM +0100, Jonas Oberhauser wrote:
On 1/21/2023 6:36 PM, Alan Stern wrote:
On Fri, Jan 20, 2023 at 10:41:14PM +0100, Jonas Oberhauser wrote:
On 1/20/2023 5:18 PM, Alan Stern wrote:
On Fri, Jan 20, 2023 at 11:13:00AM +0100, Jonas Oberhauser wrote:
Perhaps we could say that reading an index without using it later is
forbidden?
flag ~empty [Srcu-lock];data;rf;[~ domain(data;[Srcu-unlock])] as
thrown-srcu-cookie-on-floor
We already flag locks that don't have a matching unlock.
Of course, but as you know this is completely orthogonal.
Yeah, okay. It doesn't hurt to add this check, but the check isn't
complete. For example, it won't catch the invalid usage here:
P0(srcu_struct *ss)
{
int r1, r2;
r1 = srcu_read_lock(ss);
srcu_read_unlock(&ss, r1);
r2 = srcu_read_lock(ss);
srcu_read_unlock(&ss, r2);
}
exists (~0:r1=0:r2)
On the other hand, how often will people make this sort of mistake in
their litmus tests? My guess is not very.
I currently don't care too much about the incorrect usage of herd (by
inspecting some final state incorrectly), only incorrect usage in the code.
I'm inclined to add this check to the memory model. Would you prefer to
submit it yourself as a separate patch? Or are you happy to have it
merged with my patch, and if so, do you have a final, preferred form for
the check?
After clearing my confusion, I'm no longer sure if it should be added.
If you're still inclined to have it, I would prefer to submit the patch,
but I'd like to define the use-cookie relation (=
(data|[~Srcu-unlock];rfe)+) and use it also to clarify the srcu match
definition (I almost would like to do that anyways :D).
Is that ok?
jonas