Add 2+2W litmus test

[cbeuw]

Add 2+2W litmus tests with the strongest ordering that still allows observing x==y==1

Equivalent cppmem code:

int main() {
  atomic_int x=0; atomic_int y=0;
  {{{ { x.store(1,memory_order_seq_cst); 
        y.store(2,memory_order_seq_cst);
        r1=y.load(memory_order_relaxed);
      }
  ||| { y.store(1,memory_order_release);
        x.store(2,memory_order_seq_cst);
        r2=x.load(memory_order_relaxed);
      }  
  }}}

  return 0;
}

[rustbot]

Thank you for contributing to Miri!
Please remember to not force-push to the PR branch except when you need to rebase due to a conflict or when the reviewer asks you for it.

[RalfJung]

This only checks y, and it checks that that is always 1...?

The slice here is the set of all outcomes, so [1, 1] is equivalent to [1].

[RalfJung]

Your code doesn't match the cppmem code. It should be:

Suggested change

	x.load(Relaxed)
	});
	let t2 = spawn(move || {
	y.store(1, Release);
	x.store(2, SeqCst);
	y.load(Relaxed)
	y.load(Relaxed)
	});
	let t2 = spawn(move || {
	y.store(1, Release);
	x.store(2, SeqCst);
	x.load(Relaxed)

[RalfJung]

As noted on Zulip, the test is wrong: the y.load and x.load need to be swapped. With the correct version, Miri can't produce the (1, 1) outcome any more.

@rustbot author

[rustbot]

Reminder, once the PR becomes ready for a review, use @rustbot ready.