Testing Weak Memory Consistency Models

The examples below can be used to demonstrate the difference of various weak memory consistency models.

thread P w1: write(x,1) thread Q w2: write(x,2) r0: write(y,1) r1: read(x,1) r2: read(x,2) constraints w1 -> r1 w2 -> r2

thread P p1: write(x,1) p2: read(x,2) thread Q q1: write(x,2) q2: read(x,1) constraints p1 -> q2 q1 -> p2

thread P p1: write(x,1) thread Q q1: read(x,1) q2: write(x,2) thread R r1: read(x,1) r2: read(x,2) thread S s1: read(x,2) s2: read(x,1) constraints p1 -> q1 p1 -> r1 p1 -> s2 q2 -> r2 q2 -> s1

thread P p1: write(x,1) p2: write(y,2) thread Q q1: read(y,2) q2: read(x,0) constraints p2 -> q1

thread P p1: write(x,1) p2: read(y,0) thread Q q1: write(y,2) q2: read(x,0) constraints

thread P p1: write(x,1) p2: write(z,2) p3: read(y,0) thread Q q1: write(y,3) q2: write(z,4) q3: read(x,0) constraints

thread P p1: write(x,1) p2: read(y,3) p3: read(x,1) thread Q q1: read(x,1) q2: write(x,2) q3: write(y,3) constraints q3->p2 p1->p3 p1->q1

thread P p1: write(x,1) p2: write(x,3) thread Q q1: read(x,1) q2: write(x,2) thread R r1: read(x,1) r2: read(x,3) r3: read(x,2) thread S s1: read(x,1) s2: read(x,2) s3: read(x,3) constraints p1->q1 p1->r1 p1->s1 p2->r2 p2->s3 q2->r3 q2->s2

thread P p1: write(x,1) p2: read(y,3) p3: read(x,1) thread Q q1: read(x,1) q2: write(x,2) q3: write(y,3) constraints p1->q1 q3->p2 p1->p3

thread P p1: read(x,0) p2: write(x,1) p3: read(x,2) p4: write(x,3) thread Q q1: write(y,1) q2: read(x,1) q3: write(x,2) thread R r1: read(x,3) r2: read(y,0) constraints p2->q2 p4->r1 q3->p3

thread P p1: write(x,1) p2: write(y,2) thread Q q1: read(y,2) q2: write(x,3) thread R r1: read(x,3) r2: read(x,1) constraints p1 -> r2 p2 -> q1 q2 -> r1

thread P p1: write(x,1) p2: read(y,0) p3: read(y,2) thread Q q1: write(y,2) q2: read(x,0) q3: read(x,1) constraints p1 -> q3 q1 -> p3

thread P p1: write(x,1) p2: write(y,2) thread Q q1: read(y,2) q2: write(x,3) q3: read(x,1) constraints p1 -> q3 p2 -> q1

thread P p1: read(x,2) p2: write(y,1) thread Q q1: read(y,1) q2: write(x,2) constraints p2 -> q1 q2 -> p1

thread P p1: write(x,1) p2: write(x,3) p3: write(y,1) p4: read(x,2) thread Q q1: write(x,2) q2: read(y,1) q3: read(x,1) constraints p1 -> q3 p3 -> q2 q1 -> p4

thread P p1: write(x,1) p2: write(y,2) thread Q q1: read(y,2) q2: read(x,0) thread R r1: read(u,2) r2: write(v,1) thread S s1: read(v,1) s2: write(u,2) constraints p2 -> q1 r2 -> s1 s2 -> r1

thread P p1: write(x,0) p2: write(x,1) thread Q q1: read(x,1) q2: write(y,1) thread R r1: read(y,1) r2: read(x,0) constraints

thread P p1: write(x,1) p2: write(x,2) thread Q q1: read(x,2) q2: read(x,1) constraints p1 -> q2 p2 -> q1