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