Mon Apr 26 09:07:19 UTC 2021
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for PPOCA.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
C PPOCA

{}

P0(volatile int* y, volatile int* x) {

  atomic_store(x,1);
  atomic_store(y,1);

}

P1(volatile int* z, volatile int* y, volatile int* x) {

  int r1=-1; int r2=-1;
  int r0 = atomic_load_explicit(y,memory_order_relaxed);
  if (r0) {
    atomic_store_explicit(z,1,memory_order_relaxed);
    r1 = atomic_load_explicit(z,memory_order_relaxed);
    r2 = atomic_load_explicit(x+(r1 & 128),memory_order_relaxed);
  }

}


exists (1:r0=1 /\ 1:r1=1 /\ 1:r2=0)

Histogram (3 states)
11057696:>1:r0=0; 1:r1=-1; 1:r2=-1;
2     *>1:r0=1; 1:r1=1; 1:r2=0;
8942302:>1:r0=1; 1:r1=1; 1:r2=1;
Ok

Witnesses
Positive: 2, Negative: 19999998
Condition exists (1:r0=1 /\ 1:r1=1 /\ 1:r2=0) is validated
Hash=bb2426936c19f1555410d1483dd31452
Observation PPOCA Sometimes 2 19999998
Time PPOCA 3.30
Revision 45690d9d0f7a956a6d3dbaf9e912efb22835756e, version 7.56+02~dev
Command line: litmus7 -mach vougeot -c11 true -o R.tar PPOCA.litmus
Parameters
#define SIZE_OF_TEST 10000
#define NUMBER_OF_RUN 100
#define AVAIL 4
#define STRIDE 1
#define MAX_LOOP 0
/* gcc options: -Wall -std=gnu11 -O2 -pthread */
/* barrier: userfence */
/* launch: changing */
/* affinity: none */
/* alloc: dynamic */
/* memory: direct */
/* stride: 1 */
/* safer: write */
/* preload: random */
/* speedcheck: no */
/* proc used: 4 */
GCC=gcc
LITMUSOPTS=-s 5k -r 2k -st 1
Mon Apr 26 09:07:23 UTC 2021