Lines Matching +full:3 +full:p0
70 3 {}
72 5 P0(int *x, int *y)
105 Line 3 is the initialization section. Because the default initialization
114 The name of the first process is "P0" and that of the second "P1".
123 names are significant. The fact that both P0() and P1() have a formal
125 same global variable, also named "x". So the "int *x, int *y" on P0()
128 by reference, hence "P0(int *x, int *y)", but *never* "P0(int x, int y)".
130 P0() has no local variables, but P1() has two of them named "r0" and "r1".
145 The P0() process does "WRITE_ONCE(*x, 1)" on line 7. Because "x" is a
146 pointer in P0()'s parameter list, this does an unordered store to global
148 is also in P0()'s parameter list, this does a release store to global
156 reference the same global variables that are used by P0().
189 2 States 3
190 3 1:r0=0; 1:r1=0;
195 8 Positive: 0 Negative: 3
197 10 Observation MP+pooncerelease+poacquireonce Never 0 3
201 The most pertinent line is line 10, which contains "Never 0 3", which
208 clause's condition and run the test.) The numbers ("0 3") at the end
210 clause (0) and the number not not satisfying that clause (3).
214 2 States 3
215 3 1:r0=0; 1:r1=0;
219 Line 2 gives the total number of end states, and each of lines 3-5 list
234 lead-in to line 8's "Positive: 0 Negative: 3", which lists the number
257 3 {
262 8 P0(int *x, int *y)
279 Lines 3-6 now initialize both "x" and "y" to the value 42. This also
287 2 States 3
288 3 1:r0=1; 1:r1=1;
293 8 Positive: 0 Negative: 3
295 10 Observation MP+pooncerelease+poacquireonce Never 0 3
316 below, P0() is one side checking to see if an operation may proceed and
321 3 {}
323 5 P0(int *x, int *y)
350 3 0:r0=0; 1:r0=0;
388 3 {}
390 5 P0(int *x, int *y)
416 3 0:r2=0; 1:r4=0;
422 9 Positive: 1 Negative: 3
424 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
441 3 {}
443 5 P0(int *x, int *y)
470 3 0:r1=1; 0:r2=0; 1:r3=1; 1:r4=0; x=1; y=1;
476 9 Positive: 1 Negative: 3
478 11 Observation SB+rfionceonce-poonceonces Sometimes 1 3
514 3 {
517 6 P0(int *sl, int *x0, int *x1)
549 that process sets "sl" back to "0". P0()'s lock acquisition is emulated
574 3 0:r1=0; 1:r1=1;
624 3 {
628 7 P0(int *sl, int *x0, int *x1)
662 3 x1=1;
671 Line 3 shows that there is one execution that did not get filtered out,
689 3 {
694 8 P0(int *x, int **y)
725 P0()'s line 10 initializes "x" to the value 1 then line 11 links to "x"
740 3 1:r0=x; 1:r1=1;
774 3 (* B *)
783 12 P0(int *x, int **y) // F
822 3 {
828 9 P0(int *x, int *z, int **y)
861 P0() on lines 9-18 enters an RCU read-side critical section, loads the
986 3. Exceptions and interrupts are not modeled. In some cases,
1044 3. The Pn() functions' formal parameters must be pointers to the