Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

[Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>]

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 can imagine models that allow this but they aren't pretty. Maybe you have
>> a better operational model?
> The operational model is not very detailed as far as SRCU is concerned.
> It merely says that synchronize_srcu() executing on CPU C waits until:
>
> 	[...]
>
> 	For every srcu_down_read() that executed prior to t1, the
> 	matching srcu_up_read() [...].
> [...]
>
> Does this answer your question satisfactorily?

The reason I originally didn't consider this type of model (which 
requires defining 'matching') pretty is that the most natural way to 
define matching is probably using the whole dependency stuff at the 
operational level. This isn't necessary for rcu or srcu lock/unlock, so 
I thought this will add a new amount of tediousness to the model.
But I now realized that mechanisms for tracking dependencies are pretty 
much already there (to define when stores can be executed), so I'm not 
that unhappy about it anymore.


>>>> So if there is an srcu_down() that produces a cookie that is read by some
>>>> read R, and R doesn't then pass that value into an srcu_up(), the
>>>> srcu-warranty is voided.
>>> No, it isn't.
>> I quote Paul:
>> "If you do anything else at all with it, anything at all, you just voided
>> your SRCU warranty. For that matter, if you just throw that value on the
>> floor and don't pass it to an srcu_up_read() execution, you also just voided
>> your SRCU warranty."
> I suspect Paul did not express himself very precisely, and what he
> really meant was more like this:
>
> 	If you don't pass the value to exactly one srcu_up_read() call,
> 	you void the SRCU warranty.  In addition, if you do anything
> 	else with the value that might affect the outcome of the litmus
> 	test, you incur the risk that herd7 might compute an incorrect
> 	result [as in the litmus test I gave near the start of this
> 	email].
>
> Merely storing the value in a shared variable which then doesn't get
> used or is used only for something inconsequential would not cause any
> problems.
>
> Alan
Ah, I understand now.
Thanks, jonas