cachepc-linux

Fork of AMDESE/linux with modifications for CachePC side-channel attack
git clone https://git.sinitax.com/sinitax/cachepc-linux
Log | Files | Refs | README | LICENSE | sfeed.txt

Z6.0+pooncelock+pooncelock+pombonce.litmus (658B)


      1C Z6.0+pooncelock+pooncelock+pombonce
      2
      3(*
      4 * Result: Sometimes
      5 *
      6 * This example demonstrates that a pair of accesses made by different
      7 * processes each while holding a given lock will not necessarily be
      8 * seen as ordered by a third process not holding that lock.
      9 *)
     10
     11{}
     12
     13P0(int *x, int *y, spinlock_t *mylock)
     14{
     15	spin_lock(mylock);
     16	WRITE_ONCE(*x, 1);
     17	WRITE_ONCE(*y, 1);
     18	spin_unlock(mylock);
     19}
     20
     21P1(int *y, int *z, spinlock_t *mylock)
     22{
     23	int r0;
     24
     25	spin_lock(mylock);
     26	r0 = READ_ONCE(*y);
     27	WRITE_ONCE(*z, 1);
     28	spin_unlock(mylock);
     29}
     30
     31P2(int *x, int *z)
     32{
     33	int r1;
     34
     35	WRITE_ONCE(*z, 2);
     36	smp_mb();
     37	r1 = READ_ONCE(*x);
     38}
     39
     40exists (1:r0=1 /\ z=2 /\ 2:r1=0)