Messages in this thread | | | Date | Sun, 26 Feb 2023 10:49:26 -0800 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po |
| |
On Sat, Feb 25, 2023 at 07:03:11PM -0800, Paul E. McKenney wrote: > On Sat, Feb 25, 2023 at 09:29:51PM -0500, Alan Stern wrote: > > On Sat, Feb 25, 2023 at 05:01:10PM -0800, Paul E. McKenney wrote: > > > A few other oddities: > > > > > > litmus/auto/C-LB-Lww+R-OC.litmus > > > > > > Both versions flag a data race, which I am not seeing. It appears > > > to me that P1's store to u0 cannot happen unless P0's store > > > has completed. So what am I missing here? > > > > The LKMM doesn't believe that a control or data dependency orders a > > plain write after a marked read. Hence in this test it thinks that P1's > > store to u0 can happen before the load of x1. I don't remember why we > > did it this way -- probably we just wanted to minimize the restrictions > > on when plain accesses can execute. (I do remember the reason for > > making address dependencies induce order; it was so RCU would work.) > > > > The patch below will change what the LKMM believes. It eliminates the > > positive outcome of the litmus test and the data race. Should it be > > adopted into the memory model? > > Excellent question! > > As noted separately, I was conflating the C++ memory model and LKMM. > > > > litmus/auto/C-LB-Lrw+R-OC.litmus > > > litmus/auto/C-LB-Lww+R-Oc.litmus > > > litmus/auto/C-LB-Lrw+R-Oc.litmus > > > litmus/auto/C-LB-Lrw+R-A+R-Oc.litmus > > > litmus/auto/C-LB-Lww+R-A+R-OC.litmus > > > > > > Ditto. (There are likely more.) > > > > I haven't looked at these but they're probably similar. > > Let me give this patch a go and see what it does.
And it operates as expected, converting Sometimes/data-race results into Never.
Leaving the question of whether that is what we need. ;-)
Thanx, Paul
| |