On Sat, 9 Nov 2019, Linus Torvalds wrote:
> On Sat, Nov 9, 2019, 15:08 Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> wrote:
>
> > On Fri, 8 Nov 2019, Linus Torvalds wrote:
> > >
> > > Two writes to normal memory are *not* idempotent if they write
> > > different values. The ordering very much matters, and it's racy and a
> > > tool should complain.
> >
> > What you have written strongly indicates that either you think the word
> > "idempotent" means something different from its actual meaning or else
> > you are misusing the word in a very confusing way.
> >
>
> "Idempotence is the property of certain operations in mathematics and
> computer science whereby they can be applied multiple times without
> changing the result beyond the initial application. "
>
> This is (for example) commonly used when talking about nfs operations,
> where you can re-send the same nfs operation, and it's ok (even if it has
> side effects) because the server remembers that it already did the
> operation. If it's already been done, nothing changes.
>
> It may not match your definition in some other area, but this is very much
> the accepted meaning of the word in computer science and operating systems.
Agreed. My point was that you were using the word in a way which did
not match this definition.
Never mind that. You did not respond to the question at the end of my
previous email: Should the LKMM be changed so that two writes are not
considered to race with each other if they store the same value?
That change would take care of the original issue of this email thread,
wouldn't it? And it would render WRITE_IDEMPOTENT unnecessary.
Making that change would amount to formalizing your requirement that
the compiler should not invent stores to shared variables. In C11 such
invented stores are allowed. Given something like this:
<A complex computation which does not involve x but does
require a register spill>
x = 1234;
C11 allows the compiler to store an intermediate value in x rather than
allocating a slot on the stack for the register spill. After all, x is
going to be overwritten anyway, and if any other thread accessed x
during the complex computation then it would race with the final store
and so the behavior would be undefined in any case.
If you want to specifically forbid the compiler from doing this, it
makes sense to change the memory model accordingly.
For those used to thinking in terms of litmus tests, consider this one:
C equivalent-writes
{}
P0(int *x)
{
*x = 1;
}
P1(int *x)
{
*x = 1;
}
exists (~x=1)
Should the LKMM say that this litmus test contains a race?
This suggests that we might also want to relax the notion of a write
racing with a read, although in that case I'm not at all sure what the
appropriate change to the memory model would be. Something along the
lines of: If a write W races with a read R, but W stores the same value
that R would have read if W were not present, then it's not really a
race. But of course this is far too vague to be useful.
Alan Stern
