source: rtems-central/formal/promela/models/messages/msg-mgr-model.pml @ d59895a

Last change on this file since d59895a was d59895a, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/10/23 at 19:51:42

Message Manager model and test gen material

  • Property mode set to 100644
File size: 23.5 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3// Message queue attributes
4
5#define TASK_MAX 4 //three rtems tasks
6#define NULL 0
7
8#define SEMA_MAX 3
9
10#define BAD_ID TASK_MAX
11
12#define MAX_MESSAGE_QUEUES 3
13#define MAX_PENDING_MESSAGES 4
14#define MAX_MESSAGE_SIZE 1
15#define QUEUE_NAME 1
16
17//define in cpukit/include/rtems/rtems/status.h
18#define RC_OK      0  // RTEMS_SUCCESSFUL
19#define RC_InvName 3  // RTEMS_INVALID_NAME
20#define RC_InvId   4  // RTEMS_INVALID_ID
21#define RC_InvAddr 9  // RTEMS_INVALID_ADDRESS
22#define RC_Unsat   13 // RTEMS_UNSATISFIED
23#define RC_Timeout 6  // RTEMS_TIMEOUT
24#define RC_InvSize 8 // RTEMS_INVALID_SIZE
25#define RC_InvNum 10 // RTEMS_INVALID_NUMBER
26#define RC_TooMany 5 // RTEMS_TOO_MANY
27
28inline outputDefines() {
29    printf("@@@ %d DEF TASK_MAX %d\n",_pid,TASK_MAX);
30    printf("@@@ %d DEF BAD_ID %d\n",_pid,BAD_ID);
31    printf("@@@ %d DEF SEMA_MAX %d\n",_pid,SEMA_MAX);
32    printf("@@@ %d DEF MAX_MESSAGE_SIZE %d\n",_pid, MAX_MESSAGE_SIZE);
33    printf("@@@ %d DEF MAX_MESSAGE_QUEUES %d\n",_pid, MAX_MESSAGE_QUEUES);
34    printf("@@@ %d DEF MAX_PENDING_MESSAGES %d\n",_pid, MAX_PENDING_MESSAGES);
35}
36
37
38mtype = {
39  Zombie, Ready, MsgWait, TimeWait, OtherWait, // Task states
40  Wait, NoWait // Option Set values
41};
42
43
44// Tasks
45typedef Task {
46  byte nodeid; // So we can spot remote calls
47  byte pmlid; // Promela process id
48  mtype state ; // {Ready,EventWait,TickWait,OtherWait}
49  bool preemptable ;
50  byte prio ; // lower number is higher priority
51  int ticks; //
52  bool tout; // true if woken by a timeout
53  bool doCreate; // whether to create a queue
54  bool doSend; //whether task should send
55  bool doReceive; //whether task should receive
56  bool doWait; //whether task should wait message
57  int rcvInterval; //how many ticks to wait
58  int rcvMsg; //hold value of message received, modelling receive buffer
59  int sndMsg; //hold value of message to send, modelling send buffer
60  int targetQueue; //queue id for task to interact with
61  int numSends; //number of message send calls to make
62  int msgSize; //size of message to send
63};
64
65Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference
66
67
68byte sendrc;            // Sender global variable
69byte recrc;             // Receiver global variable
70byte qrc              // creation variable
71byte recout[TASK_MAX] ; // models receive 'out' location.
72
73
74bool semaphore[SEMA_MAX]; // Semaphore
75
76mtype = {
77  FIFO, PRIORITY
78};
79
80typedef Config {
81    int name; //An integer is used to represent valid RTEMS_NAME
82    int count; //Max messages for a queue
83    int maxSize; //Max message size
84    mtype attrSet; // RTEMS_ATTRIBUTE_SET, FIFO||priority
85};
86
87typedef MessageQueue {
88  Config config;
89  int messages [MAX_PENDING_MESSAGES] //message circular buffer
90  int head; //top of message queue
91  int tail; //end of message queue
92  bool queueFull; //used to determine full or empty state
93  int waitingTasks [TASK_MAX]; //task circular buffer
94  int nextTask; //top of task queue
95  int lastTask; //end of task queue
96  bool taskFull;
97};
98
99MessageQueue queueList[MAX_MESSAGE_QUEUES]; //queueList[0] is null
100
101/*
102* Helper functions for task
103* and message queue operations
104*/
105
106inline enqueueTask(id, qid) {
107  atomic{
108    queueList[qid].waitingTasks[queueList[qid].lastTask] = id;
109    if
110    :: queueList[qid].lastTask == TASK_MAX-1 -> queueList[qid].lastTask = 0;
111    :: else -> queueList[qid].lastTask++;
112    fi
113    if
114    :: queueList[qid].lastTask == queueList[qid].nextTask -> queueList[qid].taskFull = true;
115    :: else -> skip;
116    fi
117  }
118}
119
120inline dequeueTask(id,qid) {
121  atomic{
122    id = queueList[qid].waitingTasks[queueList[qid].nextTask];
123    if
124    :: queueList[qid].nextTask == TASK_MAX-1 -> queueList[qid].nextTask = 0;
125    :: else -> queueList[qid].nextTask++;
126    fi
127    if
128    :: queueList[qid].lastTask == queueList[qid].nextTask -> queueList[qid].taskFull = false;
129    :: else -> skip;
130    fi
131  }
132}
133
134
135
136inline enqueueMessage(id,msg) {
137  atomic{
138    queueList[id].messages[queueList[id].head] = msg;
139   //printf("enqueue message %d", msg);
140    if
141    :: queueList[id].head == MAX_PENDING_MESSAGES-1 -> queueList[id].head = 0;
142    :: else -> queueList[id].head++;
143    fi
144    if
145    :: queueList[id].head == queueList[id].tail -> queueList[id].queueFull = true;
146    :: else -> skip;
147    fi
148  }
149}
150
151inline dequeueMessage(id,msg) {
152  atomic{
153    msg = queueList[id].messages[queueList[id].tail];
154    //printf("dequeue message %d", msg);
155    if
156    :: msg == 0 -> skip;
157    :: queueList[id].tail == MAX_PENDING_MESSAGES-1 -> queueList[id].tail = 0;
158    :: else -> queueList[id].tail++;
159    fi
160    if
161    :: queueList[id].head == queueList[id].tail -> queueList[id].queueFull = false;
162    :: else -> skip;
163    fi
164  }
165}
166
167
168inline sizeOfQueue(id, qsize) {
169  atomic{
170  if
171  :: queueList[id].head == queueList[id].tail ->
172      if
173      ::  -> qsize = MAX_PENDING_MESSAGES;
174      :: else -> qsize = 0;
175      fi
176  :: queueList[id].head > queueList[id].tail -> qsize = queueList[id].head - queueList[id].tail;
177  :: queueList[id].head < queueList[id].tail -> qsize = MAX_PENDING_MESSAGES + queueList[id].head - queueList[id].tail;
178  fi
179  return qsize;
180  }
181}
182
183//Declare needed arrays, variables
184inline outputDeclarations () {
185  printf("@@@ %d DECL byte sendrc 0\n",_pid);
186  printf("@@@ %d DECL byte recrc 0\n",_pid);
187  printf("@@@ %d DECL byte qrc 0\n",_pid);
188  printf("@@@ %d DECL uint8_t send_counter 0\n",_pid);
189  printf("@@@ %d DCLARRAY uint8_t receive_buffer MAX_MESSAGE_SIZE\n",_pid);
190  printf("@@@ %d DCLARRAY uint8_t send_buffer MAX_MESSAGE_SIZE\n",_pid);
191  printf("@@@ %d DCLARRAY RTEMS_MESSAGE_QUEUE_BUFFER queue_buffer MAX_PENDING_MESSAGES\n",_pid);
192  // Rather than refine an entire Task array, we refine array 'slices'
193  printf("@@@ %d DCLARRAY byte recout TASK_MAX\n",_pid);
194  printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid);
195}
196
197inline nl() { printf("\n") }
198/*
199 * Synchronisation Mechanisms
200 *  Obtain(sem_id)   - call that waits to obtain semaphore `sem_id`
201 *  Release(sem_id)  - call that releases semaphore `sem_id`
202 *  Released(sem_id) - simulates ecosystem behaviour releases `sem_id`
203 *
204 * Binary semaphores:  True means available, False means in use.
205 */
206inline Obtain(sem_id){
207  atomic{
208    printf("@@@ %d WAIT %d\n",_pid,sem_id);
209    semaphore[sem_id] ;        // wait until available
210    semaphore[sem_id] = false; // set as in use
211    printf("@@@ %d LOG WAIT %d Over\n",_pid,sem_id);
212  }
213}
214
215inline Release(sem_id){
216  atomic{
217    printf("@@@ %d SIGNAL %d\n",_pid,sem_id);
218    semaphore[sem_id] = true ; // release
219  }
220}
221
222inline Released(sem_id)
223{
224  semaphore[sem_id] = true ;
225}
226
227
228/*
229 * waitUntilReady(id) logs that task[id] is waiting,
230 * and then attempts to execute a statement that blocks,
231 * until some other process changes task[id]'s state to Ready.
232 * It relies on the fact that if a statement blocks inside an atomic block,
233 * the block loses its atomic behaviour and yields to other Promela processes
234 *
235 * It is used to model a task that has been suspended for any reason.
236 */
237inline waitUntilReady(id){
238  atomic{
239    printf("@@@ %d LOG Task %d waiting, state = ",_pid,id);
240    printm(tasks[id].state); nl()
241  }
242  tasks[id].state == Ready; // breaks out of atomics if false
243  printf("@@@ %d STATE %d Ready\n",_pid,id)
244}
245
246
247/* message_queue_create()
248* creates a message queue object from passed parameters
249* queue_name -rtems object name
250* msg_count - max messages in queue
251* max_size - max message size
252* rc - return flag
253*/
254
255inline message_queue_create(queue_name, msg_count, max_size, rc) {
256    atomic{
257      //only one queue created
258      int qid = 1;
259      if
260      ::  queue_name == 0 -> rc = RC_InvName;
261      ::  max_size == 0 -> rc = RC_InvSize;
262      ::  msg_count == 0 -> rc = RC_InvNum;
263      ::  else ->
264            queueList[qid].config.count = msg_count;
265            queueList[qid].config.maxSize = max_size;
266            queueList[qid].queueFull = false;
267            queueList[qid].config.name = queue_name;
268            rc = RC_OK;
269      fi
270      ;
271  }
272}
273
274
275/*
276* message_queue_send
277*    self: id of calling task
278*    qid: id of queue
279*    msg : message
280*    size : size of the message
281*    rc: return code
282*
283* This directive will send a message to the to the specficied
284* message queue.
285*  If there is a task waiting it will copy the message to that tasks
286*  buffer and unblock it
287*  If there is no task waiting it will ad the message to the message queue
288*/
289
290inline message_queue_send(self,qid,msg,size,rc) {
291    atomic{
292      int queuedTask = queueList[qid].waitingTasks[queueList[qid].nextTask];
293      if
294      ::  qid == 0 -> rc = RC_InvId;
295      ::  else ->
296          if
297          ::  msg == NULL -> rc = RC_InvAddr;
298          ::  size > queueList[qid].config.maxSize -> rc = RC_InvSize;
299          ::  queueList[qid].queueFull -> rc = RC_TooMany;
300          ::  else ->
301              if
302              ::  queuedTask == 0 -> //no task waiting, add to buffer
303                  enqueueMessage(qid,msg);
304                  printf("@@@ %d LOG Send queueing message\n",_pid)
305                  rc = RC_OK;
306              ::  else -> //task waiting
307                  dequeueTask(queuedTask,qid);
308                  enqueueMessage(qid,msg);
309                  printf("@@@ %d LOG Send to task %d\n",_pid, queuedTask)
310                  //tasks[queuedTask].rcvMsg = msg;
311                  //printf("%d rcv msg %d",_pid,tasks[queuedTask].rcvMsg)
312                  tasks[queuedTask].state = Ready
313                  printf("@@@ %d STATE %d Ready\n",_pid, queuedTask)
314                  rc = RC_OK;
315              fi
316          fi
317      fi
318    }
319}
320
321inline message_queue_receive(self,qid,msg,rc) {
322  int rcvmsg;
323  atomic{
324    if
325    :: qid == 0 -> rc = RC_InvId;
326    //:: msg == 0 -> rc = RC_InvAddr
327    //:: size >= config.maxSize -> RC_InvSize
328    :: else ->
329      dequeueMessage(qid,msg);
330      if
331      :: msg == 0 && !tasks[self].doWait ->
332        rc = RC_Unsat; printf("@@@ %d LOG Receive Not Satisfied (no wait)\n",_pid)
333      :: msg == 0 && tasks[self].doWait ->
334        printf("@@@ %d LOG Receive Not Satisfied (timeout %d)\n",
335                _pid,
336                tasks[self].rcvInterval);
337        tasks[self].ticks = tasks[self].rcvInterval;
338        tasks[self].tout = false;
339        printf("@@@ %d STATE %d TimeWait %d\n",
340                _pid,
341                self,
342                tasks[self].rcvInterval);
343        tasks[self].state = TimeWait;
344        enqueueTask(self,qid);
345        waitUntilReady(self);
346       
347        if
348        ::  tasks[self].tout  ->  dequeueTask(self,qid); rc = RC_Timeout;
349        ::  else              -> dequeueMessage(qid,msg);
350        fi
351
352      :: else -> rc = RC_OK;
353      fi
354    fi   
355  }
356}
357
358
359/*
360 * Model Processes
361 * We shall use four processes in this model.
362 *  One will represent the RTEMS send task
363 *  Two will represent the RTEMS receive tasks
364 *  One will model a timer
365 */
366
367// These are not output to test generation
368#define SEND_ID 1
369#define RCV1_ID 2
370#define RCV2_ID 3
371
372/*
373 * Sender Scenario
374 */
375byte sendTarget;
376byte msize;
377bool sendAgain
378int totalSendCount
379int currSendCount
380/*
381 * Receiver Scenario
382 */
383
384/*
385 * Semaphore Setup
386 */
387int sendSema;
388int rcvSema1;
389int startSema;
390int rcvSema2;
391
392/*
393* Queue setup
394*
395*/
396bool queueCreated;
397int queueId;
398
399
400
401
402mtype = {Send,Receive,SndRcv, RcvSnd};
403mtype scenario;
404
405inline chooseScenario() {
406
407  sendAgain = false;
408  semaphore[0] = false;
409  semaphore[1] = false;
410  semaphore[2] = false;
411  sendSema = 0;
412  rcvSema1 = 1;
413  rcvSema2 = 2;
414  startSema = sendSema;
415  tasks[SEND_ID].doCreate = true;
416
417  //Queue parameters
418  queueCreated = false;
419  queueId = 1;
420
421  msize = MAX_MESSAGE_SIZE;
422  //set up defaults
423  tasks[SEND_ID].numSends = 1;
424  tasks[SEND_ID].sndMsg = 1;
425  tasks[SEND_ID].targetQueue = queueId;
426  tasks[RCV1_ID].targetQueue = queueId;
427  tasks[RCV2_ID].targetQueue = queueId;
428  tasks[SEND_ID].sndMsg = 1;
429  tasks[SEND_ID].msgSize = MAX_MESSAGE_SIZE;
430
431
432  //select scenario
433  if
434  ::  scenario = Send;
435  ::  scenario = Receive;
436  ::  scenario = SndRcv;
437  ::  scenario = RcvSnd;
438  fi
439
440  atomic{printf("@@@ %d LOG scenario ",_pid);
441  printm(scenario);
442  nl()};
443
444
445  if
446  :: scenario == Send ->
447        tasks[RCV1_ID].doReceive = false;
448        tasks[RCV2_ID].doReceive = false;
449        tasks[SEND_ID].doSend = true;
450        if
451        ::  tasks[SEND_ID].targetQueue = 0;
452            printf("@@@ %d LOG sub-scenario Send Bad ID\n", _pid)
453        ::  tasks[SEND_ID].targetQueue = queueId;
454            printf("@@@ %d LOG sub-scenario Send Success\n", _pid)
455        ::  tasks[SEND_ID].msgSize = MAX_MESSAGE_SIZE + 1;
456            printf("@@@ %d LOG sub-scenario Send Size Error\n", _pid)
457        ::  tasks[SEND_ID].sndMsg = 0;
458            printf("@@@ %d LOG sub-scenario Buffer Address Error\n", _pid)
459        ::  tasks[SEND_ID].numSends = MAX_PENDING_MESSAGES + 1;
460            printf("@@@ %d LOG sub-scenario Too Many messages Error\n", _pid)         
461        fi
462
463  :: scenario == Receive ->
464        tasks[SEND_ID].doSend = false;
465        tasks[RCV1_ID].doReceive = true;
466        tasks[RCV2_ID].doReceive = false;
467        startSema = rcvSema1;
468       
469        if
470        ::  tasks[RCV1_ID].doWait = false;
471            if
472            ::  tasks[RCV1_ID].targetQueue = 0;
473                printf("@@@ %d LOG sub-scenario Rcv Bad ID No Wait\n", _pid)
474            ::  tasks[SEND_ID].targetQueue = queueId;
475                printf("@@@ %d LOG sub-scenario Rcv Success No Wait\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
476            fi
477        ::  tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 5;
478            printf("@@@ %d LOG sub-scenario Rcv Success wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
479        fi
480       
481        /*
482        if
483        ::  tasks[RCV2_ID].doWait = false; 
484        ::  tasks[RCV2_ID].doWait = true; tasks[RCV2_ID].rcvInterval = 5;
485        fi
486        printf("@@@ %d LOG sub-scenario Receive2 wait:%d interval:%d\n", _pid, tasks[RCV2_ID].doWait, tasks[RCV2_ID].rcvInterval)
487        */
488
489  :: scenario == SndRcv ->
490
491        if
492        ::  tasks[SEND_ID].numSends = 2;     
493        ::  tasks[SEND_ID].numSends = 1;
494        fi
495        printf("@@@ %d LOG sub-scenario SndRcv numSends:%d\n",
496                _pid,
497                tasks[SEND_ID].numSends
498                )
499        /*
500        if
501        ::  tasks[RCV1_ID].doWait = false;     
502        ::  tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 5;
503        fi
504        printf("@@@ %d LOG sub-scenario Receive1 wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
505        if
506        ::  tasks[RCV2_ID].doWait = false;     
507        ::  tasks[RCV2_ID].doWait = true; tasks[RCV2_ID].rcvInterval = 5;
508        fi
509        printf("@@@ %d LOG sub-scenario Receive2 wait:%d interval:%d\n", _pid, tasks[RCV2_ID].doWait, tasks[RCV2_ID].rcvInterval)
510        */
511       
512        tasks[SEND_ID].doSend = true;
513        tasks[RCV1_ID].doReceive = true;
514        tasks[RCV2_ID].doReceive = true;
515
516  :: scenario == RcvSnd ->
517        startSema = rcvSema1;
518        tasks[SEND_ID].doSend = true;
519        tasks[RCV1_ID].doReceive = true;
520        tasks[RCV2_ID].doReceive = false;
521        tasks[RCV1_ID].doWait = true;  tasks[RCV1_ID].rcvInterval = 10;
522        //tasks[SEND_ID].numSends = 2
523        /*
524        if
525        :: tasks[RCV1_ID].doWait = false; tasks[RCV2_ID].doWait = false;
526        :: tasks[RCV1_ID].doWait = true;  tasks[RCV2_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 10; tasks[RCV2_ID].rcvInterval = 10;
527        fi
528        printf("@@@ %d LOG sub-scenario RcvSnd wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
529        */
530
531  fi
532}
533
534
535proctype Sender (byte taskid) {
536
537  tasks[taskid].pmlid = _pid;
538  tasks[taskid].state = Ready;
539  printf("@@@ %d TASK Runner\n",_pid,taskid);
540 
541  if
542  ::  (tasks[taskid].doCreate && !queueCreated) ->
543      printf("@@@ %d CALL message_queue_construct %d %d %d %d %d qrc\n", _pid,
544              taskid,
545              QUEUE_NAME,
546              MAX_PENDING_MESSAGES,
547              MAX_MESSAGE_SIZE,
548              queueId);
549      message_queue_create(QUEUE_NAME,
550                            MAX_PENDING_MESSAGES,
551                            MAX_MESSAGE_SIZE,
552                            qrc);
553      printf("@@@ %d SCALAR qrc %d\n",_pid,qrc);
554      queueCreated = true;
555      Release(startSema);
556  fi
557 
558  if
559  :: tasks[taskid].doSend ->
560      Obtain(sendSema);
561      repeat:
562      atomic{
563      printf("@@@ %d CALL message_queue_send %d %d %d %d sendrc\n",
564              _pid,
565              taskid,
566              tasks[taskid].targetQueue,
567              tasks[taskid].sndMsg,
568              tasks[taskid].msgSize);
569      message_queue_send(taskid,
570                          tasks[taskid].targetQueue,
571                          tasks[taskid].sndMsg,
572                          tasks[taskid].msgSize,
573                          sendrc);
574      printf("@@@ %d SCALAR sendrc %d\n",_pid,sendrc);
575      tasks[taskid].numSends-- ;
576      if
577      :: tasks[taskid].numSends != 0 -> tasks[SEND_ID].sndMsg++; goto repeat;
578      :: scenario == RcvSnd -> skip;
579      :: else -> Release(rcvSema1);
580      fi
581      }
582  :: else -> skip;
583  fi
584
585
586  //adjust semaphore behaviour for RcvSnd as Receive1 starts
587  if
588  :: scenario == RcvSnd ->
589        Obtain(rcvSema1);
590        Obtain(rcvSema2);
591  :: else ->         
592        Obtain(sendSema);
593        Obtain(rcvSema2);
594        Obtain(rcvSema1);
595  fi
596 
597  printf("@@@ %d LOG Sender %d finished\n",_pid,taskid);
598  tasks[taskid].state = Zombie;
599  printf("@@@ %d STATE %d Zombie\n",_pid,taskid);
600}
601
602proctype Receiver1 (byte taskid) {
603
604  tasks[taskid].pmlid = _pid;
605  tasks[taskid].state = Ready;
606  printf("@@@ %d TASK Worker1\n",_pid);
607
608 
609  Obtain(rcvSema1);
610
611  if
612  :: tasks[taskid].doReceive && scenario != RcvSnd->
613      atomic{
614      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
615              _pid,taskid,
616              tasks[taskid].targetQueue,
617              tasks[taskid].doWait,
618              tasks[taskid].rcvInterval);
619      message_queue_receive(taskid,
620                              tasks[taskid].targetQueue,
621                              tasks[taskid].rcvMsg,
622                              recrc);
623      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
624      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
625      Release(rcvSema2);
626      }   
627  :: tasks[taskid].doReceive && scenario == RcvSnd->
628      atomic{
629      Release(sendSema);
630      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
631                _pid,
632                taskid,
633                tasks[taskid].targetQueue,
634                tasks[taskid].doWait,
635                tasks[taskid].rcvInterval);
636      message_queue_receive(taskid,
637                              tasks[taskid].targetQueue,
638                              tasks[taskid].rcvMsg,
639                              recrc);
640      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
641      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
642      }
643  :: else -> Release(rcvSema2);
644  fi
645
646 
647
648  atomic{
649  Release(rcvSema1);
650  printf("@@@ %d LOG Receiver1 %d finished\n",_pid,taskid);
651  tasks[taskid].state = Zombie;
652  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
653  }
654}
655
656proctype Receiver2 (byte taskid) {
657
658  tasks[taskid].pmlid = _pid;
659  tasks[taskid].state = Ready;
660  printf("@@@ %d TASK Worker2\n",_pid);
661 
662  if
663  :: scenario == RcvSnd ->
664      goto rcvSkip;
665  :: else -> Obtain(rcvSema2);
666  fi
667 
668 
669  if
670  :: tasks[taskid].doReceive && scenario != RcvSnd->
671      atomic{
672      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
673              _pid,
674              taskid,
675              tasks[taskid].targetQueue,
676              tasks[taskid].doWait,
677              tasks[taskid].rcvInterval);
678      message_queue_receive(taskid,tasks[taskid].targetQueue,tasks[taskid].rcvMsg,recrc);
679      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
680      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
681      Release(sendSema);
682      }
683  :: tasks[taskid].doReceive && scenario == RcvSnd->
684      atomic{
685      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
686              _pid,
687              taskid,tasks[taskid].targetQueue,
688              tasks[taskid].doWait,
689              tasks[taskid].rcvInterval);
690      Release(sendSema);
691      message_queue_receive(taskid,tasks[taskid].targetQueue,tasks[taskid].rcvMsg,recrc);
692      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
693      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
694      }
695  :: else -> Release(sendSema);
696  fi
697
698  rcvSkip:
699  atomic{
700  Release(rcvSema2);
701  printf("@@@ %d LOG Receiver2 %d finished\n",_pid,taskid);
702  tasks[taskid].state = Zombie;
703  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
704  }
705}
706
707
708/*
709 * We need a process that periodically wakes up blocked processes.
710 * This is modelling background behaviour of the system,
711 * such as ISRs and scheduling.
712 * We visit all tasks in round-robin order (to prevent starvation)
713 * and make them ready if waiting on "other" things.
714 * Tasks waiting for events or timeouts are not touched
715 * This terminates when all tasks are zombies.
716 */
717
718bool stopclock = false;
719
720proctype System () {
721  byte taskid ;
722  bool liveSeen;
723
724  printf("@@@ %d LOG System running...\n",_pid);
725
726  loop:
727  taskid = 1;
728  liveSeen = false;
729
730  printf("@@@ %d LOG Loop through tasks...\n",_pid);
731  atomic {
732    printf("@@@ %d LOG Scenario is ",_pid);
733    printm(scenario); nl();
734  }
735  do   // while taskid < TASK_MAX ....
736  ::  taskid == TASK_MAX -> break;
737  ::  else ->
738      atomic {
739        printf("@@@ %d LOG Task %d state is ",_pid,taskid);
740        printm(tasks[taskid].state); nl()
741      }
742      if
743      :: tasks[taskid].state == Zombie -> taskid++
744      :: else ->
745         if
746         ::  tasks[taskid].state == OtherWait
747             -> tasks[taskid].state = Ready
748                printf("@@@ %d STATE %d Ready\n",_pid,taskid)
749         ::  else -> skip
750         fi
751         liveSeen = true;
752         taskid++
753      fi
754  od
755
756  printf("@@@ %d LOG ...all visited, live:%d\n",_pid,liveSeen);
757
758  if
759  ::  liveSeen -> goto loop
760  ::  else
761  fi
762  printf("@@@ %d LOG All are Zombies, game over.\n",_pid);
763  stopclock = true;
764}
765
766
767/*
768 * We need a process that handles a clock tick,
769 * by decrementing the tick count for tasks waiting on a timeout.
770 * Such a task whose ticks become zero is then made Ready,
771 * and its timer status is flagged as a timeout
772 * This terminates when all tasks are zombies
773 * (as signalled by System via `stopclock`).
774 */
775proctype Clock () {
776  int tid, tix;
777  printf("@@@ %d LOG Clock Started\n",_pid)
778  do
779  ::  stopclock  -> goto stopped
780  ::  !stopclock ->
781      printf(" (tick) \n");
782      tid = 1;
783      do
784      ::  tid == TASK_MAX -> break
785      ::  else ->
786          atomic{printf("Clock: tid=%d, state=",tid); printm(tasks[tid].state); nl()};
787          if
788          ::  tasks[tid].state == TimeWait ->
789              tix = tasks[tid].ticks - 1;
790              // printf("Clock: ticks=%d, tix=%d\n",tasks[tid].ticks,tix);
791              if
792              ::  tix == 0
793                  tasks[tid].tout = true
794                  tasks[tid].state = Ready
795                  printf("@@@ %d STATE %d Ready\n",_pid,tid)
796              ::  else
797                  tasks[tid].ticks = tix
798              fi
799          ::  else // state != TimeWait
800          fi
801          tid = tid + 1
802      od
803  od
804stopped:
805  printf("@@@ %d LOG Clock Stopped\n",_pid);
806}
807
808
809
810init {
811  pid nr;
812
813  printf("Message Manager Model running.\n");
814  printf("Setup...\n");
815 
816  printf("@@@ %d NAME Message_Manager_TestGen\n",_pid)
817  //#define required in test file
818  outputDefines();
819  //Structures and data types required in test file
820  outputDeclarations();
821
822  printf("@@@ %d INIT\n",_pid);
823  chooseScenario();
824
825  printf("Run...\n");
826  //start nececssary processes
827  run System();
828  run Clock();
829 
830  run Sender(SEND_ID);
831  run Receiver1(RCV1_ID);
832  run Receiver2(RCV2_ID);
833 
834  _nr_pr == 1;
835
836#ifdef TEST_GEN
837  assert(false);
838#endif
839
840
841printf("Message Manager Model finished !\n")
842}
Note: See TracBrowser for help on using the repository browser.