On Tue, Nov 19, 2019 at 10:11:48PM +0800, laokz wrote:
> Hello Paul,
>
> With your perfbook help, now I can understand base memory-model issue. Such
> as tools/memory-model/litmus/LB+fencembonceonce+ctrlonceonce.litmus :
>
> P0(int *x, int *y)
> {
> int r0;
>
> r0 = READ_ONCE(*x);
> if (r0)
> WRITE_ONCE(*y, 1);
> }
>
> P1(int *x, int *y)
> {
> int r0;
>
> r0 = READ_ONCE(*y);
> smp_mb();
> WRITE_ONCE(*x, 1);
> }
>
> exists (0:r0=1 /\ 1:r0=1)
>
> But wonder how about cpu in-order commit. So I removed smp_mb(), the litmus
> test showed the result exist! This confused me. In my understanding, cpu in-
> order commit means out-of-order-execution results commit to register/memory
> in compiled program order. That is cpu P1 must retire r0=y first then x=1,
> thus P0 can see P1's update of x. So P1's r0 should never be 1.
>
> Is this caused by LKMM's compatibility with out-of-order commit
> architectures? Or what's wrong with me?
Nothing is wrong with you. You are just going through a common phase
in learning about memory models. ;-)
So you modified P1() as follows, correct?
P1(int *x, int *y)
{
int r0;
r0 = READ_ONCE(*y);
WRITE_ONCE(*x, 1);
}
The compiler is free to rearrange this code as follows:
P1(int *x, int *y)
{
int r0;
WRITE_ONCE(*x, 1);
r0 = READ_ONCE(*y);
}
This can clearly satisfy the exists clause: P1() does its write,
P0() does its read and its write, and finally P1() does its read.
But suppose we prevented the compiler from moving the code:
P1(int *x, int *y)
{
int r0;
r0 = READ_ONCE(*y);
barrier();
WRITE_ONCE(*x, 1);
}
Then, as you say, weakly ordered CPUs might still reorder P1()'s
read and write. So LKMM must still say that the exists clause is
satisfied.
Thanx, Paul
