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

MP+polockonce+poacquiresilsil.litmus (681B)

      1C MP+polockonce+poacquiresilsil
      2
      3(*
      4 * Result: Sometimes
      5 *
      6 * Do spinlocks provide order to outside observers using spin_is_locked()
      7 * to sense the lock-held state, ordered by acquire?  Note that when the
      8 * first spin_is_locked() returns false and the second true, we know that
      9 * the smp_load_acquire() executed before the lock was acquired (loosely
     10 * speaking).
     11 *)
     12
     13{}
     14
     15P0(spinlock_t *lo, int *x) // Producer
     16{
     17	spin_lock(lo);
     18	WRITE_ONCE(*x, 1);
     19	spin_unlock(lo);
     20}
     21
     22P1(spinlock_t *lo, int *x) // Consumer
     23{
     24	int r1;
     25	int r2;
     26	int r3;
     27
     28	r1 = smp_load_acquire(x);
     29	r2 = spin_is_locked(lo);
     30	r3 = spin_is_locked(lo);
     31}
     32
     33exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)