Messages in this thread |  | | Date | Sat, 21 Jan 2023 15:49:27 -0800 | From | "Paul E. McKenney" <> | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) |
| |
On Sat, Jan 21, 2023 at 04:03:38PM -0500, Alan Stern wrote: > On Sat, Jan 21, 2023 at 12:10:26PM -0800, Paul E. McKenney wrote: > > On Sat, Jan 21, 2023 at 02:56:57PM -0500, Alan Stern wrote: > > > > > Anyway, the operational model says the litmus test can succeed as > > > > > follows: > > > > > > > > > > P0 P1 P2 > > > > > --------------------- ---------------------- ------------------------- > > > > > Widx2=srcu_down_read() > > > > > Wrel p2=1 > > > > > Ry=0 > > > > > Wy=1 > > > > > synchronize_srcu() starts > > > > > ... idx2, p2, and y propagate to all CPUs ... > > > > > Time t1 > > > > > Widx1=srcu_down_read() > > > > > Wrel p1=1 > > > > > ,,, idx1 and p1 propagate to all CPUs ... > > > > > Racq p1=1 > > > > > srcu_up_read(idx2) > > > > > synchronize_srcu() ends > > > > > Wx=1 > > > > > Rx=1 > > > > > Racq p2=1 > > > > > Ridx2=idx1 > > > > > srcu_up_read(idx1) > > > > > > > > > > (The final equality in P0 is allowed because idx1 and idx2 are both > > > > > random numbers, so they might be equal.) > > > > > > > > This all makes sense to me. > > > > > > > > > Incidentally, it's worth pointing out that the algorithm Paul described > > > > > will forbid this litmus test even if you remove the while loop and the > > > > > read of idx2 from P0. > > > > Sorry, what I said may not have been clear. I meant that even if you > > > remove the while loop and read of idx2 from P0, your algorithm will > > > still not allow idx1 = idx2 provided everything else is as written. > > > > If synchronize_srcu() has flipped ->srcu_idx by the time that P0's > > srcu_down_read() executes, agreed. Otherwise, Widx1 and Widx2 might > > well be equal. > > But idx1 and idx2 are equal, we can't have both P0 reads x=1 and P1 > reads y=0 -- not even if P0 doesn't wait until it reads p2=1. If you > don't see why, I'll send an explanation.
Ah, synchronize_srcu() does unlocks *then* locks. I was getting it backwards, apologies for my confusion!
Thanx, Paul
|  |