Messages in this thread | | | From | Alan Huang <> | Subject | Question about ISA2+pooncelock+pooncelock+pombonce litmus | Date | Mon, 18 Mar 2024 01:47:43 +0800 |
| |
Hi,
I’m playing with the LKMM, then I saw the ISA2+pooncelock+pooncelock+pombonce.
The original litmus is as follows: ------------------------------------------------------ P0(int *x, int *y, spinlock_t *mylock) { spin_lock(mylock); WRITE_ONCE(*x, 1); WRITE_ONCE(*y, 1); spin_unlock(mylock); }
P1(int *y, int *z, spinlock_t *mylock) { int r0;
spin_lock(mylock); r0 = READ_ONCE(*y); WRITE_ONCE(*z, 1); spin_unlock(mylock); }
P2(int *x, int *z) { int r1; int r2;
r2 = READ_ONCE(*z); smp_mb(); r1 = READ_ONCE(*x); }
exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0) ------------------------------------------------------ Of course, the result is Never.
But when I delete P0’s spin_lock and P1’s spin_unlock: ------------------------------------------------------- P0(int *x, int *y, spinlock_t *mylock) { WRITE_ONCE(*x, 1); WRITE_ONCE(*y, 1); spin_unlock(mylock); }
P1(int *y, int *z, spinlock_t *mylock) { int r0;
spin_lock(mylock); r0 = READ_ONCE(*y); WRITE_ONCE(*z, 1); }
P2(int *x, int *z) { int r1; int r2;
r2 = READ_ONCE(*z); smp_mb(); r1 = READ_ONCE(*x); }
exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0) ------------------------------------------------------ Then herd told me the result is Sometimes.
Is this expected?
| |