cbmc/regression/goto-instrument-wmm-core/ppc_aclwsrr002_TSO_ALL/aclwsrr002.c at 7d44a79e687dde6e6d12660e81578e42f1dd6ab1 · diffblue/cbmc · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
void fence()
{
  asm("sync");
}
void lwfence()
{
  asm("lwsync");
}
void isync()
{
  asm("isync");
}

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;

void *P0(void *arg)
{
  __unbuffered_p0_r1 = 1;
  x = __unbuffered_p0_r1;
  fence();
  __unbuffered_p0_r3 = 1;
  y = __unbuffered_p0_r3;
  // Instrumentation for CPROVER
  fence();
  __unbuffered_cnt++;
}

void *P1(void *arg)
{
  __unbuffered_p1_r1 = y;
  lwfence();
  __unbuffered_p1_r3 = y;
  __unbuffered_p1_r4 = __unbuffered_p1_r3 ^ __unbuffered_p1_r3;
  __unbuffered_p1_r5 = *(&x + __unbuffered_p1_r4);
  // Instrumentation for CPROVER
  fence();
  __unbuffered_cnt++;
}

int main()
{
__CPROVER_ASYNC_0:
  P0(0);
__CPROVER_ASYNC_1:
  P1(0);
  __CPROVER_assume(__unbuffered_cnt == 2);
  fence();
  // EXPECT:exists
  __CPROVER_assert(
    !(__unbuffered_p1_r1 == 1 && __unbuffered_p1_r5 == 0),
    "Program proven to be relaxed for PPC, model checker says YES.");
  return 0;
}