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

IRIW+fencembonceonces+OnceOnce.litmus (731B)

      1C IRIW+fencembonceonces+OnceOnce
      2
      3(*
      4 * Result: Never
      5 *
      6 * Test of independent reads from independent writes with smp_mb()
      7 * between each pairs of reads.  In other words, is smp_mb() sufficient to
      8 * cause two different reading processes to agree on the order of a pair
      9 * of writes, where each write is to a different variable by a different
     10 * process?  This litmus test exercises LKMM's "propagation" rule.
     11 *)
     12
     13{}
     14
     15P0(int *x)
     16{
     17	WRITE_ONCE(*x, 1);
     18}
     19
     20P1(int *x, int *y)
     21{
     22	int r0;
     23	int r1;
     24
     25	r0 = READ_ONCE(*x);
     26	smp_mb();
     27	r1 = READ_ONCE(*y);
     28}
     29
     30P2(int *y)
     31{
     32	WRITE_ONCE(*y, 1);
     33}
     34
     35P3(int *x, int *y)
     36{
     37	int r0;
     38	int r1;
     39
     40	r0 = READ_ONCE(*y);
     41	smp_mb();
     42	r1 = READ_ONCE(*x);
     43}
     44
     45exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)