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