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+polockmbonce+poacquiresilsil.litmus (745B)

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