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

[Jonas Oberhauser]

On 1/18/2023 5:50 PM, Alan Stern wrote:
> On Tue, Jan 17, 2023 at 07:50:41PM -0800, Paul E. McKenney wrote:
> > On Tue, Jan 17, 2023 at 03:15:06PM -0500, Alan Stern wrote:
> > > On Tue, Jan 17, 2023 at 09
> > > > Given an Srcu-down and an Srcu-up:
> > > >
> > > > let srcu-rscs = ( return_value(Srcu-lock) ; (dep | rfi)* ;
> > > > 		  parameter(Srcu-unlock, 2) ) |
> > > > 		( return_value(Srcu-down) ; (dep | rf)* ;
> > > > 		  parameter(Srcu-up, 2) )
> > > >
> > > > Seem reasonable, or am I missing yet something else?
> > > Not at all reasonable.
> > >
> > > For one thing, consider this question: Which statements lie inside a
> > > read-side critical section?
> > Here srcu_down_read() and srcu_up_read() are to srcu_read_lock() and
> > srcu_read_unlock() as down_read() and up_read() are to mutex_lock()
> > and mutex_unlock().  Not that this should be all that much comfort
> > given that I have no idea how one would go about modeling down_read()
> > and up_read() in LKMM.
> It might make sense to work on that first, before trying to do
> srcu_down_read() and srcu_up_read().
>
> > > With srcu_read_lock() and a matching srcu_read_unlock(), the answer is
> > > clear: All statements po-between the two.  With srcu_down_read() and
> > > srcu_up_read(), the answer is cloudy in the extreme.
> > And I agree that it must be clearly specified, and my that previous try
> > was completely lacking.  Here is a second attempt:
> >
> > let srcu-rscs = (([Srcu-lock] ; data ; [Srcu-unlock]) & loc) |
> > 		(([Srcu-down] ; (data | rf)* ; [Srcu-up]) & loc)
> >
> > (And I see your proposal and will try it.)
> >
> > > Also, bear in mind that the Fundamental Law of RCU is formulated in
> > > terms of stores propagating to a critical section's CPU.  What are we to
> > > make of this when a single critical section can belong to more than one
> > > CPU?
> > One way of answering this question is by analogy with down() and up()
> > when used as a cross-task mutex.  Another is by mechanically applying
> > some of current LKMM.  Let's start with this second option.
> >
> > LKMM works mostly with critical sections, but we also discussed ordering
> > based on the set of events po-after an srcu_read_lock() on the one hand
> > and the set of events po-before an srcu_read_unlock() on the other.
> > Starting here, the critical section is the intersection of these two sets.
> >
> > In the case of srcu_down_read() and srcu_up_read(), as you say, whatever
> > might be a critical section must span processes.  So what if instead of
> > po, we used (say) xbstar?  Then given a set of A such that ([Srcu-down ;
> > xbstar ; A) and B such that (B ; xbstar ; [Srcu-up]), then the critical
> > section is the intersection of A and B.
> >
> > One objection to this approach is that a bunch of unrelated events could
> > end up being defined as part of the critical section.  Except that this
> > happens already anyway in real critical sections in the Linux kernel.
> >
> > So what about down() and up() when used as cross-task mutexes?
> > These often do have conceptual critical sections that protect some
> > combination of resource, but these critical sections might span tasks
> > and/or workqueue handlers.  And any reasonable definition of these
> > critical sections would be just as likely to pull in unrelated accesses as
> > the above intersection approach for srcu_down_read() and srcu_up_read().
> >
> > But I am just now making all this up, so thoughts?
> Maybe we don't really need to talk about read-side critical sections at
> all.  Once again, here's what explanation.txt currently says:
>
> 	For any critical section C and any grace period G, at least
> 	one of the following statements must hold:
>
> (1)	C ends before G does, and in addition, every store that
> 	propagates to C's CPU before the end of C must propagate to
> 	every CPU before G ends.
>
> (2)	G starts before C does, and in addition, every store that
> 	propagates to G's CPU before the start of G must propagate
> 	to every CPU before C starts.
>
> Suppose we change this to:
>
> 	For any RCU lock operation L and matching unlock operation U,
> 	and any matching grace period G, at least one of the following
> 	statements must hold:
>
> (1)	U executes before G ends, and in addition, every store that
> 	propagates to U's CPU before U executes must propagate to
> 	every CPU before G ends.
>
> (2)	G starts before L executes, and in addition, every store that
> 	propagates to G's CPU before the start of G must propagate
> 	to every CPU before L executes.
>
> (For SRCU, G matches L and U if it operates on the same srcu structure.)

I think for the formalization, the definition of "critical section" is 
hidden inside the word "matching" here.
You will still need to define what matching means for up and down.
Can I understand down and up to create a large read-side critical 
section that is shared between multiple threads, analogously to a 
semaphore? With the restriction that for srcu, there are really multiple 
(two) such critical sections that can be open in parallel, which are 
indexed by the return value of down/the input of up?

If so I suspect that every down matches with every up within a "critical 
section"?
maybe you can define balancing along the co analous to the balancing 
along po currently used for matching rcu_lock() and rcu_unlock(). I.e.,

down ------------- up
   \down--------up/
       \down-up/
          \_/
where diagonal links are co links and the straight links are "balanced 
match" links.

Then everything that is enclosed within a pair of "balanced match" is 
linked:

match-down-up = co^-1?; balanced-srcu-updown ; co^-1?

Since multiple critical sections can be in-flight, maybe you can use co 
& same-value (or whatever the relation is) to define this?


let balanced-srcu-updown = let rec
        unmatched-locks = Srcu-down \ domain(matched)
    and unmatched-unlocks = Srcu-up \ range(matched)
    and unmatched = unmatched-locks | unmatched-unlocks
    and unmatched-co = [unmatched] ; co & same-value ; [unmatched]
    and unmatched-locks-to-unlocks =
        [unmatched-locks] ;  co & same-value ; [unmatched-unlocks]
    and matched = matched | (unmatched-locks-to-unlocks \
        (unmatched-co ; unmatched-co))
    in matched
let match-down-up = (co & same-value)^-1?; balanced-srcu-updown ; (co & 
same-value)^-1?



> > > Indeed, given:
> > >
> > > 	P0(int *x) {
> > > 		srcu_down_read(x);
> > > 	}
> > >
> > > 	P1(int *x) {
> > > 		srcu_up_read(x);
> > > 	}
> > >
> > > what are we to make of executions in which P1 executes before P0?
> > Indeed, there had better be something else forbidding such executions, or
> > this is an invalid use of srcu_down_read() and srcu_up_read().

Would it be sufficient to flag executions in which an up is not matched 
with any down event?

> >    This might
> > become more clear if the example is expanded to include the index returned
> > from srcu_down_read() that is to be passed to srcu_up_read():
> >
> > 	P0(int *x, int *i) {
> > 		WRITE_ONCE(i, srcu_down_read(x));
> > 	}
> >
> > 	P1(int *x, int *i) {
> > 		srcu_up_read(x, READ_ONCE(i));
> > 	}
> Hmmm.  What happens if you write:
>
> 	r1 = srcu_down_read(x);
> 	r2 = srcu_down_read(x);
> 	srcu_up_read(x, r1);
> 	srcu_up_read(x, r2);
>
> ?  I can't even tell what that would be _intended_ to do.

Is it correct that it creates one or two read-side critical sections 
depending on whether the two down() happen to return the same value, 
which either spans at least all four lines (plus perhaps more if other 
threads also do down()) or the first spans lines 1-3 and the second 
spans 2-4?

Is the implementation of srcu-lock and srcu-unlock still anything like 
the implementation in the 2009 paper?

best wishes and thanks for your patient explanations, jonas