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+poonceonces+OnceOnce.litmus (655B)


      1C IRIW+poonceonces+OnceOnce
      2
      3(*
      4 * Result: Sometimes
      5 *
      6 * Test of independent reads from independent writes with nothing
      7 * between each pairs of reads.  In other words, is anything at all
      8 * needed to cause two different reading processes to agree on the order
      9 * of a pair of writes, where each write is to a different variable by a
     10 * different process?
     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	r1 = READ_ONCE(*y);
     27}
     28
     29P2(int *y)
     30{
     31	WRITE_ONCE(*y, 1);
     32}
     33
     34P3(int *x, int *y)
     35{
     36	int r0;
     37	int r1;
     38
     39	r0 = READ_ONCE(*y);
     40	r1 = READ_ONCE(*x);
     41}
     42
     43exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)