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

RCU+sync+free.litmus (892B)

      1C RCU+sync+free
      2
      3(*
      4 * Result: Never
      5 *
      6 * This litmus test demonstrates that an RCU reader can never see a write that
      7 * follows a grace period, if it did not see writes that precede that grace
      8 * period.
      9 *
     10 * This is a typical pattern of RCU usage, where the write before the grace
     11 * period assigns a pointer, and the writes following the grace period destroy
     12 * the object that the pointer used to point to.
     13 *
     14 * This is one implication of the RCU grace-period guarantee, which says (among
     15 * other things) that an RCU read-side critical section cannot span a grace period.
     16 *)
     17
     18{
     19int x = 1;
     20int *y = &x;
     21int z = 1;
     22}
     23
     24P0(int *x, int *z, int **y)
     25{
     26	int *r0;
     27	int r1;
     28
     29	rcu_read_lock();
     30	r0 = rcu_dereference(*y);
     31	r1 = READ_ONCE(*r0);
     32	rcu_read_unlock();
     33}
     34
     35P1(int *x, int *z, int **y)
     36{
     37	rcu_assign_pointer(*y, z);
     38	synchronize_rcu();
     39	WRITE_ONCE(*x, 0);
     40}
     41
     42exists (0:r0=x /\ 0:r1=0)