lkml.org 
[lkml]   [2023]   [Feb]   [27]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: [PATCH v3] tools/memory-model: Make ppo a subrelation of po
    On Mon, Feb 27, 2023 at 05:50:15PM +0100, Jonas Oberhauser wrote:
    > > So I don't see this as a valid argument for not using rw-xbstar in
    > > rw-race. Even theoretically.
    >
    > There's nothing wrong with using rw-xbstar in rw-race, especially in current
    > LKMM, and I'm not arguing against that.
    >
    > I'm saying that the argument
    > "if rw-xbstar links a read R to a plain write W, and that plain write is
    > replaced by a read R', and in case R' reads a value different from W,
    > followed by a store W' (with some dependency from R' to W')  by the
    > compiler, then the fact that R and R' can't have a data race means that it's
    > safe to use rw-xbstar in rw-race"
    > is incomplete. (Of course that doesn't mean the claim is wrong.)
    > To make the argument complete, you also need that W' is generated if
    > necessary, and more crucially that W' is still ordered behind R!
    > Otherwise you would now have a data race between R and W', like in the
    > hypothetical example I mentioned, even though R and R' don't race.
    >
    > And if you do that second step in LKMM (even with the change of
    > w-pre-bounded we are discussing) you quickly find that W' is indeed still
    > ordered, so rw-xbstar is perfectly fine.
    >
    > Perhaps that step is so trivial to you that you don't feel it needs
    > mentioning : ) But speaking about LKMM-like models in general, some might
    > have some subtle case where rw-xbstar links R and W but would not R and W'.

    Ah, okay. Yes, it is a subtle point. And by the reasoning I just used,
    if such a case did exist then one could conclude it would be an example
    demonstrating that rw-xbstar should not have linked R and W in the first
    place.

    And it looks like I should write up and submit a patch allowing more
    dependencies in the definition of w-pre-bounded.

    Alan

    \
     
     \ /
      Last update: 2023-03-27 00:37    [W:2.211 / U:0.108 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site