Lines Matching refs:P1

78 11 P1(int *x, int *y)
114 The name of the first process is "P0" and that of the second "P1".
118 for example, a .litmus file matching "^P1(" but not matching "^P2("
123 names are significant.  The fact that both P0() and P1() have a formal
126 and P1() mean that both processes are working with two shared global
130 P0() has no local variables, but P1() has two of them named "r0" and "r1".
151 The P1() process declares two local variables on lines 13 and 14.
155 variable "r1".  Both "x" and "y" are in P1()'s parameter list, so both
175 flag ("y") set but the buffer ("x") as not yet filled in, that is, if P1()
221 both of P1()'s loads returned the value "0".  As expected, given the
268 14 P1(int *x, int *y)
317 P1() is the other side completing its update.
332 14 P1(int *x, int *y)
343 P1()'s "if" statement on line 10 works as expected, so that line 11 is
344 executed only if line 9 loads a non-zero value from "x".  Because P1()'s
345 write of "1" to "x" happens only after P1()'s read from "y", one would
400 15 P1(int *x, int *y)
453 15 P1(int *x, int *y)
528 17 P1(int *sl, int *x0, int *x1)
553 having the value "1"), respectively.  P1() operates in a similar manner.
616 of P1() reads that variable into "1:r2" to force an early mismatch with
639 18 P1(int *sl, int *x0, int *x1, int *x2)
700 14 P1(int *x, int **y)
720 The "exists" clause works the same way, with the "1:r0=x" comparing P1()'s
728 P1()'s line 20 loads a pointer from "y", and line 21 dereferences that
750 The only possible outcomes feature P1() loading a pointer to "z"
751 (which contains zero) on the one hand and P1() loading a pointer to "x"
755 scenario is flagged by the "exists" clause, and would occur if P1()
791 20 P1(int *x, int **y)
839 20 P1(int *z, int **y, int *c)
858 "x".  In addition, "z" is pre-initialized to prepare for P1(), which
865 P1() on lines 20-24 updates the list header to instead reference "z",