1: p(0):[(((lck_initialize==0)&&empty(req_cll_initialize)))]
2: p(0):[req_cll_initialize!_pid]
3: initialize(6):[((nempty(req_cll_initialize)&&!(lck_initialize)))]
4: initialize(6):[req_cll_initialize?lck_id]
5: p(0):[exc_cll_initialize!_pid]
6: initialize(6):[exc_cll_initialize?eval(lck_id)]
7: initialize(6):[(((lck_dcas_malloc==0)&&empty(req_cll_dcas_malloc)))]
8: initialize(6):[req_cll_dcas_malloc!_pid]
9: initialize(6):[ now.par0_dcas_malloc = sizeof(Node ); ]
10: dcas_malloc(5):[((nempty(req_cll_dcas_malloc)&&!(lck_dcas_malloc)))]
11: dcas_malloc(5):[req_cll_dcas_malloc?lck_id]
12: initialize(6):[exc_cll_dcas_malloc!_pid]
13: dcas_malloc(5):[exc_cll_dcas_malloc?eval(lck_id)]
14: dcas_malloc(5):[ Pdcas_malloc->n = now.par0_dcas_malloc; ]
15: dcas_malloc(5):[lck_dcas_malloc = 0]
16: dcas_malloc(5):[ Pdcas_malloc->p=(char *)0; ]
17: dcas_malloc(5):[( ((now.dcas_cnt+Pdcas_malloc->n)<=sizeof(now.dcas_heap)) )]
18: dcas_malloc(5):[ Pdcas_malloc->p=&(now.dcas_heap[now.dcas_cnt]); ]
19: dcas_malloc(5):[ now.dcas_cnt+=Pdcas_malloc->n; ]
20: dcas_malloc(5):[(!(lck_dcas_malloc_ret))]
21: dcas_malloc(5):[ now.res_dcas_malloc = (long) Pdcas_malloc->p; ]
22: dcas_malloc(5):[(1)]
23: dcas_malloc(5):[ret_dcas_malloc!lck_id]
24: initialize(6):[ret_dcas_malloc?eval(_pid)]
25: initialize(6):[ now.Dummy=(Node *) now.res_dcas_malloc; now.lck_dcas_malloc_ret = 0; ]
26: initialize(6):[ now.Dummy->L=now.Dummy->R=now.Dummy; ]
27: initialize(6):[ now.LeftHat=now.Dummy; ]
28: initialize(6):[ now.RightHat=now.Dummy; ]
29: initialize(6):[(1)]
30: initialize(6):[ret_initialize!lck_id]
31: p1(4):[else]
32: p1(4):[(((lck_popLeft==0)&&empty(req_cll_popLeft)))]
33: p1(4):[req_cll_popLeft!_pid]
34: popLeft(8):[((nempty(req_cll_popLeft)&&!(lck_popLeft)))]
35: popLeft(8):[req_cll_popLeft?lck_id]
36: p(0):[ret_initialize?eval(_pid)]
37: p(0):[ ; now.lck_initialize_ret = 0; ]
38: p(0):[ Pp->i=0; ]
39: p2(2):[else]
40: p(0):[( (Pp->i<3) )]
41: p(0):[(((lck_pushLeft==0)&&empty(req_cll_pushLeft)))]
42: p(0):[req_cll_pushLeft!_pid]
43: p(0):[ now.par0_pushLeft = Pp->i; ]
44: pushLeft(11):[((nempty(req_cll_pushLeft)&&!(lck_pushLeft)))]
45: pushLeft(11):[req_cll_pushLeft?lck_id]
46: p1(3):[else]
47: p2(2):[(((lck_popRight==0)&&empty(req_cll_popRight)))]
48: p2(2):[req_cll_popRight!_pid]
49: popRight(10):[((nempty(req_cll_popRight)&&!(lck_popRight)))]
50: popRight(10):[req_cll_popRight?lck_id]
51: p(0):[exc_cll_pushLeft!_pid]
52: pushLeft(11):[exc_cll_pushLeft?eval(lck_id)]
53: pushLeft(11):[ PpushLeft->v = now.par0_pushLeft; ]
54: pushLeft(11):[lck_pushLeft = 0]
55: pushLeft(11):[(((lck_dcas_malloc==0)&&empty(req_cll_dcas_malloc)))]
56: pushLeft(11):[req_cll_dcas_malloc!_pid]
57: pushLeft(11):[ now.par0_dcas_malloc = sizeof(Node ); ]
58: dcas_malloc(5):[((nempty(req_cll_dcas_malloc)&&!(lck_dcas_malloc)))]
59: dcas_malloc(5):[req_cll_dcas_malloc?lck_id]
60: p1(4):[exc_cll_popLeft!_pid]
61: popLeft(8):[exc_cll_popLeft?eval(lck_id)]
62: popLeft(8):[(1)]
63: pushLeft(11):[exc_cll_dcas_malloc!_pid]
64: dcas_malloc(5):[exc_cll_dcas_malloc?eval(lck_id)]
65: dcas_malloc(5):[ Pdcas_malloc->n = now.par0_dcas_malloc; ]
66: dcas_malloc(5):[lck_dcas_malloc = 0]
67: dcas_malloc(5):[ Pdcas_malloc->p=(char *)0; ]
68: dcas_malloc(5):[( ((now.dcas_cnt+Pdcas_malloc->n)<=sizeof(now.dcas_heap)) )]
69: dcas_malloc(5):[ Pdcas_malloc->p=&(now.dcas_heap[now.dcas_cnt]); ]
70: dcas_malloc(5):[ now.dcas_cnt+=Pdcas_malloc->n; ]
71: p2(1):[else]
72: dcas_malloc(5):[(!(lck_dcas_malloc_ret))]
73: dcas_malloc(5):[ now.res_dcas_malloc = (long) Pdcas_malloc->p; ]
74: dcas_malloc(5):[(1)]
75: dcas_malloc(5):[ret_dcas_malloc!lck_id]
76: p2(2):[exc_cll_popRight!_pid]
77: popRight(10):[exc_cll_popRight?eval(lck_id)]
78: popRight(10):[(1)]
79: p2(1):[(((lck_popRight==0)&&empty(req_cll_popRight)))]
80: p2(1):[req_cll_popRight!_pid]
81: pushLeft(11):[ret_dcas_malloc?eval(_pid)]
82: popRight(9):[((nempty(req_cll_popRight)&&!(lck_popRight)))]
83: popRight(9):[req_cll_popRight?lck_id]
84: p1(3):[(((lck_popLeft==0)&&empty(req_cll_popLeft)))]
85: p1(3):[req_cll_popLeft!_pid]
86: pushLeft(11):[ PpushLeft->nd=(Node *) now.res_dcas_malloc; now.lck_dcas_malloc_ret = 0; ]
87: pushLeft(11):[else]
88: pushLeft(11):[ PpushLeft->nd->L=now.Dummy; ]
89: pushLeft(11):[ PpushLeft->nd->V=PpushLeft->v; ]
90: pushLeft(11):[(1)]
91: pushLeft(11):[ PpushLeft->lh=now.LeftHat; ]
92: pushLeft(11):[ PpushLeft->lhL=PpushLeft->lh->L; ]
93: popLeft(7):[((nempty(req_cll_popLeft)&&!(lck_popLeft)))]
94: popLeft(7):[req_cll_popLeft?lck_id]
95: pushLeft(11):[( (PpushLeft->lhL==PpushLeft->lh) )]
96: pushLeft(11):[ PpushLeft->nd->R=now.Dummy; ]
97: pushLeft(11):[ PpushLeft->rh=now.RightHat; ]
98: p2(1):[exc_cll_popRight!_pid]
99: popRight(9):[exc_cll_popRight?eval(lck_id)]
100: popRight(9):[(1)]
101: pushLeft(11):[ PpushLeft->tmp=DCAS(&(now.LeftHat),&(now.RightHat),PpushLeft->lh,PpushLeft->rh,PpushLeft->nd,PpushLeft->nd); ]
102: pushLeft(11):[( PpushLeft->tmp )]
103: pushLeft(11):[(!(lck_pushLeft_ret))]
104: pushLeft(11):[ now.res_pushLeft = (long) 0; ]
105: pushLeft(11):[(1)]
106: popRight(10):[ PpopRight->rh=now.RightHat; ]
107: pushLeft(11):[ret_pushLeft!lck_id]
108: popRight(10):[ PpopRight->lh=now.LeftHat; ]
109: p(0):[ret_pushLeft?eval(_pid)]
110: p(0):[ Pp->v= now.res_pushLeft; now.lck_pushLeft_ret = 0; ]
111: p1(3):[exc_cll_popLeft!_pid]
112: popLeft(7):[exc_cll_popLeft?eval(lck_id)]
113: popLeft(7):[(1)]
114: p(0):[else]
115: p(0):[ Pp->i++; ]
116: popLeft(8):[ PpopLeft->lh=now.LeftHat; ]
117: popLeft(7):[ PpopLeft->lh=now.LeftHat; ]
118: p(0):[( (Pp->i<3) )]
119: p(0):[(((lck_pushLeft==0)&&empty(req_cll_pushLeft)))]
120: p(0):[req_cll_pushLeft!_pid]
121: p(0):[ now.par0_pushLeft = Pp->i; ]
122: pushLeft(11):[((nempty(req_cll_pushLeft)&&!(lck_pushLeft)))]
123: pushLeft(11):[req_cll_pushLeft?lck_id]
124: p(0):[exc_cll_pushLeft!_pid]
125: pushLeft(11):[exc_cll_pushLeft?eval(lck_id)]
126: pushLeft(11):[ PpushLeft->v = now.par0_pushLeft; ]
127: pushLeft(11):[lck_pushLeft = 0]
128: pushLeft(11):[(((lck_dcas_malloc==0)&&empty(req_cll_dcas_malloc)))]
129: pushLeft(11):[req_cll_dcas_malloc!_pid]
130: pushLeft(11):[ now.par0_dcas_malloc = sizeof(Node ); ]
131: dcas_malloc(5):[((nempty(req_cll_dcas_malloc)&&!(lck_dcas_malloc)))]
132: dcas_malloc(5):[req_cll_dcas_malloc?lck_id]
133: pushLeft(11):[exc_cll_dcas_malloc!_pid]
134: dcas_malloc(5):[exc_cll_dcas_malloc?eval(lck_id)]
135: dcas_malloc(5):[ Pdcas_malloc->n = now.par0_dcas_malloc; ]
136: dcas_malloc(5):[lck_dcas_malloc = 0]
137: popLeft(7):[ PpopLeft->rh=now.RightHat; ]
138: dcas_malloc(5):[ Pdcas_malloc->p=(char *)0; ]
139: dcas_malloc(5):[( ((now.dcas_cnt+Pdcas_malloc->n)<=sizeof(now.dcas_heap)) )]
140: dcas_malloc(5):[ Pdcas_malloc->p=&(now.dcas_heap[now.dcas_cnt]); ]
141: dcas_malloc(5):[ now.dcas_cnt+=Pdcas_malloc->n; ]
142: dcas_malloc(5):[(!(lck_dcas_malloc_ret))]
143: popRight(10):[else]
144: popRight(10):[( (PpopRight->rh==PpopRight->lh) )]
145: dcas_malloc(5):[ now.res_dcas_malloc = (long) Pdcas_malloc->p; ]
146: dcas_malloc(5):[(1)]
147: dcas_malloc(5):[ret_dcas_malloc!lck_id]
148: pushLeft(11):[ret_dcas_malloc?eval(_pid)]
149: pushLeft(11):[ PpushLeft->nd=(Node *) now.res_dcas_malloc; now.lck_dcas_malloc_ret = 0; ]
150: pushLeft(11):[else]
151: pushLeft(11):[ PpushLeft->nd->L=now.Dummy; ]
152: pushLeft(11):[ PpushLeft->nd->V=PpushLeft->v; ]
153: pushLeft(11):[(1)]
154: popRight(9):[ PpopRight->rh=now.RightHat; ]
155: popRight(9):[ PpopRight->lh=now.LeftHat; ]
156: pushLeft(11):[ PpushLeft->lh=now.LeftHat; ]
157: pushLeft(11):[ PpushLeft->lhL=PpushLeft->lh->L; ]
158: pushLeft(11):[else]
159: pushLeft(11):[ PpushLeft->nd->R=PpushLeft->lh; ]
160: popLeft(7):[else]
161: pushLeft(11):[ PpushLeft->tmp=DCAS(&(now.LeftHat),&(PpushLeft->lh->L),PpushLeft->lh,PpushLeft->lhL,PpushLeft->nd,PpushLeft->nd); ]
162: pushLeft(11):[( PpushLeft->tmp )]
163: pushLeft(11):[(!(lck_pushLeft_ret))]
164: pushLeft(11):[ now.res_pushLeft = (long) 0; ]
165: pushLeft(11):[(1)]
166: popRight(10):[ PpopRight->tmp=DCAS(&(now.RightHat),&(now.LeftHat),PpopRight->rh,PpopRight->lh,now.Dummy,now.Dummy); ]
167: popRight(10):[else]
168: popRight(10):[(1)]
169: pushLeft(11):[ret_pushLeft!lck_id]
170: popRight(10):[ PpopRight->rh=now.RightHat; ]
171: popRight(9):[else]
172: popRight(10):[ PpopRight->lh=now.LeftHat; ]
173: popRight(10):[else]
174: popRight(9):[( (PpopRight->rh==PpopRight->lh) )]
175: popRight(9):[ PpopRight->tmp=DCAS(&(now.RightHat),&(now.LeftHat),PpopRight->rh,PpopRight->lh,now.Dummy,now.Dummy); ]
176: popRight(9):[else]
177: popRight(9):[(1)]
178: p(0):[ret_pushLeft?eval(_pid)]
179: p(0):[ Pp->v= now.res_pushLeft; now.lck_pushLeft_ret = 0; ]
180: popRight(9):[ PpopRight->rh=now.RightHat; ]
181: popLeft(7):[( (PpopLeft->lh==PpopLeft->rh) )]
182: p(0):[else]
183: p(0):[ Pp->i++; ]
184: popLeft(7):[ PpopLeft->tmp=DCAS(&(now.LeftHat),&(now.RightHat),PpopLeft->lh,PpopLeft->rh,now.Dummy,now.Dummy); ]
185: popLeft(7):[else]
186: popLeft(7):[(1)]
187: popLeft(7):[ PpopLeft->lh=now.LeftHat; ]
188: popLeft(8):[ PpopLeft->rh=now.RightHat; ]
189: popLeft(8):[else]
190: popLeft(8):[( (PpopLeft->lh==PpopLeft->rh) )]
191: popLeft(7):[ PpopLeft->rh=now.RightHat; ]
192: popRight(10):[else]
193: popRight(10):[ PpopRight->rhL=PpopRight->rh->L; ]
194: popRight(9):[ PpopRight->lh=now.LeftHat; ]
195: popLeft(8):[ PpopLeft->tmp=DCAS(&(now.LeftHat),&(now.RightHat),PpopLeft->lh,PpopLeft->rh,now.Dummy,now.Dummy); ]
196: popLeft(8):[else]
197: popLeft(8):[(1)]
198: popLeft(8):[ PpopLeft->lh=now.LeftHat; ]
199: popRight(9):[else]
200: popLeft(8):[ PpopLeft->rh=now.RightHat; ]
201: popRight(9):[else]
202: popRight(9):[ PpopRight->rhL=PpopRight->rh->L; ]
203: p(0):[( (Pp->i<3) )]
204: p(0):[(((lck_pushLeft==0)&&empty(req_cll_pushLeft)))]
205: p(0):[req_cll_pushLeft!_pid]
206: p(0):[ now.par0_pushLeft = Pp->i; ]
207: pushLeft(11):[((nempty(req_cll_pushLeft)&&!(lck_pushLeft)))]
208: pushLeft(11):[req_cll_pushLeft?lck_id]
209: p(0):[exc_cll_pushLeft!_pid]
210: pushLeft(11):[exc_cll_pushLeft?eval(lck_id)]
211: pushLeft(11):[ PpushLeft->v = now.par0_pushLeft; ]
212: pushLeft(11):[lck_pushLeft = 0]
213: pushLeft(11):[(((lck_dcas_malloc==0)&&empty(req_cll_dcas_malloc)))]
214: pushLeft(11):[req_cll_dcas_malloc!_pid]
215: pushLeft(11):[ now.par0_dcas_malloc = sizeof(Node ); ]
216: dcas_malloc(5):[((nempty(req_cll_dcas_malloc)&&!(lck_dcas_malloc)))]
217: dcas_malloc(5):[req_cll_dcas_malloc?lck_id]
218: pushLeft(11):[exc_cll_dcas_malloc!_pid]
219: dcas_malloc(5):[exc_cll_dcas_malloc?eval(lck_id)]
220: dcas_malloc(5):[ Pdcas_malloc->n = now.par0_dcas_malloc; ]
221: dcas_malloc(5):[lck_dcas_malloc = 0]
222: popLeft(8):[else]
223: dcas_malloc(5):[ Pdcas_malloc->p=(char *)0; ]
224: dcas_malloc(5):[( ((now.dcas_cnt+Pdcas_malloc->n)<=sizeof(now.dcas_heap)) )]
225: dcas_malloc(5):[ Pdcas_malloc->p=&(now.dcas_heap[now.dcas_cnt]); ]
226: dcas_malloc(5):[ now.dcas_cnt+=Pdcas_malloc->n; ]
227: popRight(9):[ PpopRight->tmp=DCAS(&(now.RightHat),&(PpopRight->rh->L),PpopRight->rh,PpopRight->rhL,PpopRight->rhL,PpopRight->rh); ]
228: popRight(9):[( PpopRight->tmp )]
229: popRight(9):[ PpopRight->result=PpopRight->rh->V; ]
230: dcas_malloc(5):[(!(lck_dcas_malloc_ret))]
231: popRight(9):[ PpopRight->rh->R=now.Dummy; ]
232: dcas_malloc(5):[ now.res_dcas_malloc = (long) Pdcas_malloc->p; ]
233: dcas_malloc(5):[(1)]
234: popRight(10):[ PpopRight->tmp=DCAS(&(now.RightHat),&(PpopRight->rh->L),PpopRight->rh,PpopRight->rhL,PpopRight->rhL,PpopRight->rh); ]
235: popRight(10):[else]
236: popRight(10):[(1)]
237: popRight(9):[ PpopRight->rh->V=(-1); ]
238: dcas_malloc(5):[ret_dcas_malloc!lck_id]
239: pushLeft(11):[ret_dcas_malloc?eval(_pid)]
240: pushLeft(11):[ PpushLeft->nd=(Node *) now.res_dcas_malloc; now.lck_dcas_malloc_ret = 0; ]
241: pushLeft(11):[else]
242: popLeft(8):[else]
243: popLeft(8):[ PpopLeft->lhR=PpopLeft->lh->R; ]
244: pushLeft(11):[ PpushLeft->nd->L=now.Dummy; ]
245: pushLeft(11):[ PpushLeft->nd->V=PpushLeft->v; ]
246: pushLeft(11):[(1)]
247: pushLeft(11):[ PpushLeft->lh=now.LeftHat; ]
248: pushLeft(11):[ PpushLeft->lhL=PpushLeft->lh->L; ]
249: popLeft(7):[else]
250: popRight(9):[(!(lck_popRight_ret))]
251: pushLeft(11):[else]
252: pushLeft(11):[ PpushLeft->nd->R=PpushLeft->lh; ]
253: popLeft(7):[else]
254: popLeft(7):[ PpopLeft->lhR=PpopLeft->lh->R; ]
255: pushLeft(11):[ PpushLeft->tmp=DCAS(&(now.LeftHat),&(PpushLeft->lh->L),PpushLeft->lh,PpushLeft->lhL,PpushLeft->nd,PpushLeft->nd); ]
256: pushLeft(11):[( PpushLeft->tmp )]
257: popLeft(7):[ PpopLeft->tmp=DCAS(&(now.LeftHat),&(PpopLeft->lh->R),PpopLeft->lh,PpopLeft->lhR,PpopLeft->lhR,PpopLeft->lh); ]
258: popLeft(7):[else]
259: popLeft(7):[(1)]
260: popRight(9):[ now.res_popRight = (long) PpopRight->result; ]
261: popRight(9):[(1)]
262: popRight(9):[ret_popRight!lck_id]
263: popLeft(7):[ PpopLeft->lh=now.LeftHat; ]
264: p2(1):[ret_popRight?eval(_pid)]
265: popRight(10):[ PpopRight->rh=now.RightHat; ]
266: popLeft(7):[ PpopLeft->rh=now.RightHat; ]
267: popLeft(7):[else]
268: popRight(10):[ PpopRight->lh=now.LeftHat; ]
269: popLeft(7):[else]
270: popLeft(7):[ PpopLeft->lhR=PpopLeft->lh->R; ]
271: popRight(10):[else]
272: popLeft(7):[ PpopLeft->tmp=DCAS(&(now.LeftHat),&(PpopLeft->lh->R),PpopLeft->lh,PpopLeft->lhR,PpopLeft->lhR,PpopLeft->lh); ]
273: popLeft(7):[( PpopLeft->tmp )]
274: popLeft(7):[ PpopLeft->result=PpopLeft->lh->V; ]
275: popLeft(7):[ PpopLeft->lh->L=now.Dummy; ]
276: popLeft(7):[ PpopLeft->lh->V=(-1); ]
277: popLeft(7):[(!(lck_popLeft_ret))]
278: popLeft(8):[ PpopLeft->tmp=DCAS(&(now.LeftHat),&(PpopLeft->lh->R),PpopLeft->lh,PpopLeft->lhR,PpopLeft->lhR,PpopLeft->lh); ]
279: popLeft(8):[( PpopLeft->tmp )]
280: popLeft(8):[ PpopLeft->result=PpopLeft->lh->V; ]
281: popLeft(8):[ PpopLeft->lh->L=now.Dummy; ]
282: pushLeft(11):[(!(lck_pushLeft_ret))]
283: p2(1):[ Pp2->rv= now.res_popRight; now.lck_popRight_ret = 0; ]
284: popLeft(7):[ now.res_popLeft = (long) PpopLeft->result; ]
285: popLeft(7):[(1)]
286: p2(1):[( (Pp2->rv!=(-1)) )]
287: popLeft(7):[ret_popLeft!lck_id]
288: p1(3):[ret_popLeft?eval(_pid)]
289: pushLeft(11):[ now.res_pushLeft = (long) 0; ]
290: pushLeft(11):[(1)]
291: popRight(10):[else]
292: popRight(10):[ PpopRight->rhL=PpopRight->rh->L; ]
293: pushLeft(11):[ret_pushLeft!lck_id]
294: p1(3):[ Pp1->rv= now.res_popLeft; now.lck_popLeft_ret = 0; ]
295: popRight(10):[ PpopRight->tmp=DCAS(&(now.RightHat),&(PpopRight->rh->L),PpopRight->rh,PpopRight->rhL,PpopRight->rhL,PpopRight->rh); ]
296: popRight(10):[( PpopRight->tmp )]
297: popRight(10):[ PpopRight->result=PpopRight->rh->V; ]
298: popRight(10):[ PpopRight->rh->R=now.Dummy; ]
299: popRight(10):[ PpopRight->rh->V=(-1); ]
300: popRight(10):[(!(lck_popRight_ret))]
301: popRight(10):[ now.res_popRight = (long) PpopRight->result; ]
302: popRight(10):[(1)]
303: popLeft(8):[ PpopLeft->lh->V=(-1); ]
304: popRight(10):[ret_popRight!lck_id]
305: p2(2):[ret_popRight?eval(_pid)]
306: popLeft(8):[(!(lck_popLeft_ret))]
307: p2(2):[ Pp2->rv= now.res_popRight; now.lck_popRight_ret = 0; ]
308: popLeft(8):[ now.res_popLeft = (long) PpopLeft->result; ]
309: popLeft(8):[(1)]
310: popLeft(8):[ret_popLeft!lck_id]
311: p(0):[ret_pushLeft?eval(_pid)]
312: p1(4):[ret_popLeft?eval(_pid)]
313: p1(4):[ Pp1->rv= now.res_popLeft; now.lck_popLeft_ret = 0; ]
314: p1(4):[( (Pp1->rv!=(-1)) )]
315: p1(3):[( (Pp1->rv!=(-1)) )]
p1_rv=1
316: p1(4):[ Printf("p1_rv=%d
",Pp1->rv); ]
317: p1(4):[ ; ]
318: p(0):[ Pp->v= now.res_pushLeft; now.lck_pushLeft_ret = 0; ]
319: p1(4):[ now.received[Pp1->rv]=1; ]
p1_rv=2
320: p1(3):[ Printf("p1_rv=%d
",Pp1->rv); ]
321: p1(3):[ ; ]
322: p1(3):[ now.received[Pp1->rv]=1; ]
323: p2(2):[( (Pp2->rv!=(-1)) )]
p2_rv=1
324: p2(2):[ Printf("p2_rv=%d
",Pp2->rv); ]
pan: precondition false: (((Pp2->rv>=0)&&(Pp2->rv<3))&&(now.received[Pp2->rv]==0))
325: p2(2):[ ; ]
spin: trail ends after 325 steps
#processes 12:
325: proc 0 (p) model:82 (state 19) (invalid end state)
( (Pp->v!=0) )
else
325: proc 1 (p2) model:105 (state 14) (invalid end state)
Printf("p2_rv=%d\n",Pp2->rv);
325: proc 2 (p2) model:107 (state 16) (invalid end state)
now.received[Pp2->rv]=1;
325: proc 3 (p1) model:131 (state 20)
-end-
325: proc 4 (p1) model:131 (state 20)
-end-
325: proc 5 (dcas_malloc) model:138 (state 7)
((nempty(req_cll_dcas_malloc)&&!(lck_dcas_malloc)))
325: proc 6 (initialize) model:161 (state 6)
((nempty(req_cll_initialize)&&!(lck_initialize)))
325: proc 7 (popLeft) model:185 (state 6)
((nempty(req_cll_popLeft)&&!(lck_popLeft)))
325: proc 8 (popLeft) model:185 (state 6)
((nempty(req_cll_popLeft)&&!(lck_popLeft)))
325: proc 9 (popRight) model:235 (state 6)
((nempty(req_cll_popRight)&&!(lck_popRight)))
325: proc 10 (popRight) model:235 (state 6)
((nempty(req_cll_popRight)&&!(lck_popRight)))
325: proc 11 (pushLeft) model:285 (state 7)
((nempty(req_cll_pushLeft)&&!(lck_pushLeft)))
global vars:
int par0_dcas_malloc: 24
bit lck_dcas_malloc_ret: 0
bit lck_dcas_malloc: 0
bit lck_initialize_ret: 0
bit lck_initialize: 0
bit lck_popLeft_ret: 0
bit lck_popLeft: 0
bit lck_popRight_ret: 0
bit lck_popRight: 0
int dcas_cnt: 96
int par0_pushLeft: 2
bit lck_pushLeft_ret: 0
bit lck_pushLeft: 0
chan ret_dcas_malloc (=1): len 0:
chan exc_cll_dcas_malloc (=2): len 0:
chan req_cll_dcas_malloc (=3): len 0:
chan ret_initialize (=4): len 0:
chan exc_cll_initialize (=5): len 0:
chan req_cll_initialize (=6): len 0:
chan ret_popLeft (=7): len 0:
chan exc_cll_popLeft (=8): len 0:
chan req_cll_popLeft (=9): len 0:
chan ret_popRight (=10): len 0:
chan exc_cll_popRight (=11): len 0:
chan req_cll_popRight (=12): len 0:
chan ret_pushLeft (=13): len 0:
chan exc_cll_pushLeft (=14): len 0:
chan req_cll_pushLeft (=15): len 0:
local vars proc 0 (p):
int i: 2
int v: 0
local vars proc 1 (p2):
int rv: 0
local vars proc 2 (p2):
int rv: 1
local vars proc 3 (p1):
int rv: 2
local vars proc 4 (p1):
int rv: 1
local vars proc 5 (dcas_malloc):
byte lck_id: 11
int n: 24
local vars proc 6 (initialize):
byte lck_id: 0
local vars proc 7 (popLeft):
byte lck_id: 3
int tmp: 1
int result: 2
local vars proc 8 (popLeft):
byte lck_id: 4
int tmp: 1
int result: 1
local vars proc 9 (popRight):
byte lck_id: 1
int tmp: 1
int result: 0
local vars proc 10 (popRight):
byte lck_id: 2
int tmp: 1
int result: 1
local vars proc 11 (pushLeft):
int tmp: 1
byte lck_id: 0
int v: 2