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

Jonas Oberhauser
2023-01-18T21:06:34Z

On 1/18/2023 9:54 PM, Alan Stern wrote:
> On Wed, Jan 18, 2023 at 12:06:01PM -0800, Paul E. McKenney wrote:
>> On Wed, Jan 18, 2023 at 11:50:24AM -0500, Alan Stern wrote:
>> Boqun mentioned off-list this morning that this is still the case,
>> and that each execution of srcu_read_lock() will return a unique value.
>> Assuming that I understood him correctly, anyway.
> That will no longer be true with the patch I posted yesterday. Every
> execution of srcu_read_lock() will return 0 (or whatever the initial
> value of the lock variable is).
>
> But with a small change to the .def file, each execution of
> srcu_read_unlock() can be made to increment the lock's value, and then
> the next srcu_read_lock() would naturally return the new value.

That's one of the reasons I'd prefer to see some way to define arbitrary
events and constrain their values axiomatically in cat/bell, rather than
having to rely on loads and stores.

>
>>>> 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().
>> The thing is that it is easy to associate an srcu_down_read() with the
>> corresponding srcu_up_read(). With down() and up(), although in the
>> Linux kernel this might be represented by a data structure tracking
>> (say) an I/O request, LKMM is going to be hard pressed to figure that out.
> It would help (or at least, it would help _me_) if you gave a short
> explanation of how srcu_down_read() and srcu_up_read() are meant to
> work. With regular r/w semaphores, the initial lock value is 0, each
> down() operation decrements the value, each up() operation increments
> the value -- or vice versa if you don't like negative values -- and a
> write_lock() will wait until the value is >= 0. In that setting, it
> makes sense to say that a down() which changes the value from n to n-1
> matches the next up() which changes the value from n-1 to n.
>
> I presume that srcu semaphores do not work this way. Particularly since
> the down() operation returns a value which must be passed to the
> corresponding up() operation. So how _do_ they work?

Coming from the lense of how it probably works (that you get an index
computed from the number of completed rcu_sync(), and down() on a
semaphore in an array indexed by that index, where any concurrent
rcu_sync waits until the semaphore is 0 again), I suspect that each
value defines its own semaphore.
That's why I proposed

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?

Which would match every down on the same value with every up that
happens between two times that the value of the semaphore is 0, without
having to keep track of the actual value of the semaphore.

Since the semaphore starts from zero, it's really just a matter of
having balanced down() and up(), and if you are enclosed between
balanced down() and up(), you are in a critical section.

Then any GP that ends after any down() must also end after all "later"
up() on the same semaphore (same srcu_struct, same idx) until the value
reaches zero again. (Here "later" is encoded through co. Might be you
want fr instead.)
And any GP that starts before any up() must also start before all
"earlier" down() on the same semaphore.

This is the sense of matching I'm trying to encode above.
Let me know if my understanding of down() and up() is wrong.

have fun, jonas