Messages in this thread | | | Date | Mon, 27 Feb 2023 20:40:00 +0100 | From | Andrea Parri <> | Subject | Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po |
| |
> 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?
(Unpopular opinion I know,) it should drop dependencies ordering, not add/promote it.
Andrea
| |