source: rtems-central/formal/promela/models/barriers/barrier-mgr-model.pml @ 44fca64

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

Barrier Manager model and test gen material

  • Property mode set to 100644
File size: 35.6 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3/*
4 * barrier-mgr-model.pml
5 *
6 * Copyright (C) 2022 Trinity College Dublin (www.tcd.ie)
7 *
8 * All rights reserved.
9 *
10 * Redistribution and use in source and binary forms, with or without
11 * modification, are permitted provided that the following conditions are
12 * met:
13 *
14 *     * Redistributions of source code must retain the above copyright
15 *       notice, this list of conditions and the following disclaimer.
16 *
17 *     * Redistributions in binary form must reproduce the above
18 *       copyright notice, this list of conditions and the following
19 *       disclaimer in the documentation and/or other materials provided
20 *       with the distribution.
21 *
22 *     * Neither the name of the copyright holders nor the names of its
23 *       contributors may be used to endorse or promote products derived
24 *       from this software without specific prior written permission.
25 *
26 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
27 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
28 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
29 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
30 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
31 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
32 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
33 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
34 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
35 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
36 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
37 */
38
39/*
40 * The model presented here is designed to work with the following files:
41 *   Refinement:   barrier-events-mgr-rfn.yml
42 *   Test Preamble: barrier-events-mgr-pre.h
43 *   Test Postamble: barrier-events-mgr-post.h
44 *   Test Runner: barrier-events-mgr-run.h
45 */
46
47/*
48 * We need to output annotations for any #define we use.
49 * It is simplest to keep them all together,
50 * and use an inline to output them.
51 */
52
53// Barriers - we will test Automatic and Manual Barriers
54#define MAX_BARRIERS 2 // Max amount of barriers available to be created
55                       // 0 reserved for NULL pointers
56// Barrier Configurations
57#define BARRIER_MAN 0
58#define BARRIER_AUTO 1
59#define MAX_WAITERS 3
60#define NO_TIMEOUT 0
61
62// We envisage three RTEMS tasks involved.
63#define TASK_MAX 4 // These are the "RTEMS" tasks only, numbered 1, 2 & 3
64                   // We reserve 0 to model NULL pointers
65
66// We use semaphores to synchronise the tasks
67#define SEMA_MAX 3
68
69// Return Values
70// Defined in cpukit/include/rtems/rtems/status.h
71#define RC_OK      0  // RTEMS_SUCCESSFUL
72#define RC_InvName 3  // RTEMS_INVALID_NAME
73#define RC_InvId   4  // RTEMS_INVALID_ID
74#define RC_TooMany 5  // RTEMS_TOO_MANY
75#define RC_Timeout 6  // RTEMS_TIMEOUT
76#define RC_Deleted 7  // RTEMS_OBJECT_WAS_DELETED
77#define RC_InvAddr 9  // RTEMS_INVALID_ADDRESS
78#define RC_InvNum  10 // RTEMS_INVALID_NUMBER
79
80// Output configuration
81inline outputDefines () {
82   printf("@@@ %d DEF MAX_BARRIERS %d\n",_pid,MAX_BARRIERS);
83   printf("@@@ %d DEF BARRIER_MAN %d\n",_pid,BARRIER_MAN);
84   printf("@@@ %d DEF BARRIER_AUTO %d\n",_pid,BARRIER_AUTO);
85   printf("@@@ %d DEF MAX_WAITERS %d\n",_pid,MAX_WAITERS);
86   printf("@@@ %d DEF TASK_MAX %d\n",_pid,TASK_MAX);
87   printf("@@@ %d DEF SEMA_MAX %d\n",_pid,SEMA_MAX);
88}
89
90// Special values: task states, options, return codes
91mtype = {
92  // Task states, BarrierWait is same as TimeWait but with no timeout
93  Zombie, Ready, BarrierWait, TimeWait, OtherWait,
94};
95
96// Tasks
97typedef Task {
98  byte nodeid; // So we can spot remote calls
99  byte pmlid; // Promela process id
100  mtype state ; // {Ready,BarrierWait,TimeWait,OtherWait}
101  bool preemptable;
102  byte prio; // lower number is higher priority
103  int ticks; // clock ticks to keep track of timeout
104  bool tout; // true if woken by a timeout
105};
106
107// Barriers
108typedef Barrier {
109  byte b_name; // barrier name
110  bool isAutomatic; // true for automatic, false for manual barrier
111  int maxWaiters; // maximum count of waiters for automatic barrier
112  int waiterCount; // current amount of tasks waiting on the barrier
113  bool waiters[TASK_MAX]; // waiters on the barrier
114  bool isInitialised; // indicated whenever this barrier was created
115}
116
117Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference
118Barrier barriers[MAX_BARRIERS]; // barriers[0] models a NULL dereference
119
120/*
121 * Running Orders (maintained by simple global sync counter):
122 *  Create;;Ident = Barrier Identified only after creating
123 *  Acquire;;Release = Manual barrier is acquired and then released
124 *  Acquire;;Delete = Manual barrier is acquired and then deleted
125 * Here ;; is "sequential" composition of *different* threads.
126 * Additionally task 1 will always create a barrier before operations
127 */
128bool semaphore[SEMA_MAX]; // Semaphore
129
130inline outputDeclarations () {
131  printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid);
132}
133
134/*
135 * Synchronisation Mechanisms
136 *
137 *  Obtained(sem_id) - call that waits if semaphore
138 *   `sem_id` is aquired by someone.
139 *  Obtain(sem_id) - obttains semaphore `sem_id`
140 *  Release(sem_id)  - call that releases semaphore `sem_id`
141 *
142 * Binary semaphores:  True means available, False means in use.
143 */
144
145inline Obtain(sem_id){
146  atomic{
147    printf("@@@ %d WAIT %d\n",_pid,sem_id);
148    semaphore[sem_id] ;        // wait until available
149    semaphore[sem_id] = false; // set as in use
150    printf("@@@ %d LOG WAIT %d Over\n",_pid,sem_id);
151  }
152}
153
154inline Release(sem_id){
155  atomic{
156    printf("@@@ %d SIGNAL %d\n",_pid,sem_id);
157    semaphore[sem_id] = true ; // release
158  }
159}
160
161/* The following inlines are not given here as atomic,
162 * but are intended to be used in an atomic context.
163*/
164
165inline nl() { printf("\n") } // Useful shorthand
166
167/*
168 * waitUntilReady(id) logs that task[id] is waiting,
169 * and then attempts to execute a statement that blocks,
170 * until some other process changes task[id]'s state to Ready.
171 * It relies on the fact that if a statement blocks inside an atomic block,
172 * the block loses its atomic behaviour and yields to other Promela processes
173 *
174 * It is used to model a task that has been suspended for any reason.
175 */
176inline waitUntilReady(id){
177  atomic{
178    printf("@@@ %d LOG Task %d waiting, state = ",_pid,id);
179    printm(tasks[id].state); nl()
180  }
181  tasks[id].state == Ready; // breaks out of atomics if false
182  printf("@@@ %d STATE %d Ready\n",_pid,id)
183}
184
185/*
186 * satisfied(bid, sat) checks if a barrier reached enough
187 * waiters to be released. Relevant only for automatic barriers.
188 */
189inline satisfied(bid,sat) {
190  if
191  ::  barriers[bid].waiterCount >= barriers[bid].maxWaiters ->
192      printf("@@@ %d LOG Auto Barrier satisfied(<bid:%d wt:%d max:%d>)\n",
193              _pid,bid,barriers[bid].waiterCount,barriers[bid].maxWaiters);
194      sat = true
195  ::  else -> sat = false
196  fi
197}
198
199/*
200 * preemptIfRequired(callerid) is executed,
201 * when the tasks waiting on the barrier are released.
202 *
203 * It checks if task[callerid] should be preempted, and makes it so.
204 * This is achieved here by setting the calling task state to OtherWait.
205 * Task goes over all of the released processes and chooses one with
206 * highest priority.
207 */
208inline preemptIfRequired(callerid) {
209  int t_index = 1;
210  do
211  ::  t_index < TASK_MAX && t_index != callerid ->
212      if
213      ::  tasks[callerid].preemptable  &&
214          // we use the (usual?) convention that higher priority is a lower
215          // number
216          tasks[t_index].prio < tasks[callerid].prio &&
217          tasks[t_index].state == Ready
218          ->  tasks[callerid].state = OtherWait;
219          printf("@@@ %d STATE %d OtherWait\n",_pid,callerid)
220          callerid = t_index;
221      ::  (!tasks[callerid].preemptable  ||
222          tasks[t_index].prio > tasks[callerid].prio) &&
223          tasks[t_index].state == Ready ->
224          tasks[t_index].state = OtherWait;
225          printf("@@@ %d STATE %d OtherWait\n",_pid,t_index)
226      ::  else -> skip
227      fi
228      t_index++
229  ::  else -> break
230  od
231}
232
233/*
234 * waitAtBarrier(tid, bid, rc) holds the task at the barrier.
235 *
236 * It utilises the same principle as the waitUntilReady to hold the task.
237 * However, here when the task is released it is checked why it was released.
238 * This allows to model us correct return codes, whenever the task was released
239 * due to barrier release, barrier deletion or timeout of the waiting task.
240 */
241inline waitAtBarrier(tid,bid,rc){
242  atomic{
243    printf("@@@ %d LOG Task %d waiting, state = ",_pid,tid);
244    printm(tasks[tid].state); nl()
245  }
246  tasks[tid].state == Ready; // breaks out of atomics if false
247  if
248  ::  tasks[tid].tout ->
249      barriers[bid].waiters[tid] = false; // remove self from waiters
250      rc = RC_Timeout
251      tasks[tid].tout = false; // reset timeout in case we reaquire
252      barriers[bid].waiterCount--;
253      preemptIfRequired(tid);
254      waitUntilReady(tid) // if we were higher prio, need to pre-empt others
255  ::  !barriers[bid].isInitialised ->
256      rc = RC_Deleted
257  ::  else -> // normally released
258      rc = RC_OK   
259  fi
260  printf("@@@ %d STATE %d Ready\n",_pid,tid)
261}
262
263/*
264 * barrierRelease(self,bid) is executed, when the tasks waiting on the barrier
265 * are released.
266 *
267 * It can be invoked by release or delete directives in this model.
268 *
269 * It checks if calling task should be preempted, and makes it so.
270 */
271inline barrierRelease(self,bid) {
272  atomic{
273    int tid = 1;
274    do
275    :: tid < TASK_MAX ->
276       if
277       ::  barriers[bid].waiters[tid] ->
278           barriers[bid].waiters[tid] = false;
279           tasks[tid].state = Ready
280       ::  else -> skip
281       fi
282       tid++
283    :: else -> break
284    od
285    barriers[bid].waiterCount = 0;
286    preemptIfRequired(self);
287    waitUntilReady(self) // Of all the tasks released only one should have
288                         // Ready state and the rest is in OtherWait State.
289  }
290}
291
292/*
293 * barrier_create(name,attribs,max_waiters,id,rc)
294 *
295 * Simulates a call to rtems_barrier_create
296 *   name : name of the barrier
297 *   arrtibs : attribute set of the barrier
298 *   max_waiters : (automatic only, optional) amount of max waiters
299 *                  on the barrier
300 *   id : id of the barrier if created successfully
301 *   rc : updated with the return code when directive completes
302 *
303 * Corresponding RTEMS call:
304 *   rc = rtems_barrier_create(name,attribs,max_waiters,id);
305 *     `name` models `rtems_name name`
306 *     `attribs` models `rtems_attribute attribute_set`
307 *     `max_waiters` models `uint32_t maximum_waiters`
308 *     `id` models `rtems_event_set *id`
309 *
310 *  This directive does not preempt the task, so it's relatively
311 *  straightforward.
312 */
313inline barrier_create(name,attribs,max_waiters,id,rc) {
314  atomic{
315    int new_bid = 1;
316    if
317    ::  id == 0 -> rc = RC_InvAddr;
318    ::  name <= 0 -> rc = RC_InvName;
319    ::  else ->
320        do
321          ::  new_bid < MAX_BARRIERS ->
322              if
323              ::  !barriers[new_bid].isInitialised ->
324                  if
325                  ::  attribs == BARRIER_AUTO ->
326                      if
327                      ::  max_waiters > 0 ->
328                            barriers[new_bid].maxWaiters = max_waiters;
329                      ::  else ->
330                            rc = RC_InvNum;
331                            break;
332                      fi
333                      barriers[new_bid].b_name = name;
334                      barriers[new_bid].isAutomatic =
335                        barriers[new_bid].isAutomatic | attribs;
336                      barriers[new_bid].waiterCount = 0;
337                      barriers[new_bid].isInitialised = true;
338                      id = new_bid;
339                      rc = RC_OK;
340                      printf("@@@ %d LOG %d Created {n: %d, auto: true, mw: %d}\n"
341                              ,_pid, new_bid, name, max_waiters);
342                      break
343                  ::  else -> // attribs == BARRIER_MAN
344                      barriers[new_bid].b_name = name;
345                      barriers[new_bid].isAutomatic =
346                        barriers[new_bid].isAutomatic | attribs;
347                      barriers[new_bid].waiterCount = 0;
348                      barriers[new_bid].isInitialised = true;
349                      id = new_bid;
350                      rc = RC_OK;
351                      printf("@@@ %d LOG %d Created {n: %d, auto: false}\n"
352                              ,_pid, new_bid, name);
353                      break
354                  fi
355              ::  else /* barriers[id].isInitialised */ -> new_bid++;
356              fi
357          ::  else -> // new_bid >= MAX_BARRIERS
358              rc = RC_TooMany;
359              break
360          od
361    fi
362  }
363}
364
365
366/*
367 * barrier_ident(name,id,rc)
368 *
369 * Simulates a call to rtems_barrier_ident
370 *   name : name of the barrier
371 *   id : id of the barrier if created successfully
372 *   rc : updated with the return code when the directive completes
373 *
374 * Corresponding RTEMS call:
375 *   rc = rtems_barrier_ident(name,id);
376 *     `name` models `rtems_name name`
377 *     `id` models `rtems_event_set *id`
378 *
379 * Here we assuming that the node where the barrier was created
380 * is searched.
381 */
382inline barrier_ident(name,id,rc) {
383  atomic{
384    int b_index = 1; // 0 is NULL deref
385    if
386    ::  id == 0 -> rc = RC_InvAddr;
387    ::  name <= 0 ->
388        rc = RC_InvName;
389        id = 0;
390    ::  else -> // name > 0
391        do
392        ::  b_index < MAX_BARRIERS ->
393            if
394            ::  barriers[b_index ].isInitialised &&
395                barriers[b_index ].b_name == name ->
396                  id = b_index ;
397                  printf("@@@ %d LOG Barrier %d Identified by name %d\n",
398                          _pid, b_index, name);
399                  rc = RC_OK;
400                  break;
401            ::  else -> /* !barriers[id].isInitialised ||
402                           barriers[b_index ].b_name!=name */
403                  b_index ++;
404            fi
405        ::  else -> // b_index  >= MAX_BARRIERS
406              rc = RC_InvName;
407              break;
408        od
409    fi
410  }
411}
412
413/*
414 * barrier_wait(self,bid,interval,rc)
415 *
416 * Simulates a call to rtems_barrier_wait
417 *   self : task id making the call
418 *   bid : id of the barrier
419 *   interval : wait time on the barrier (0 waits forever)
420 *   rc : updated with the return code when the wait completes
421 *
422 * Corresponding RTEMS call:
423 *   rc = rtems_barrier_wait(bid, interval;
424 *     `bid` models `rtems_id id`
425 *     `interval` models `rtems_interval timeout`
426 *
427 * This directive almost always blocks the calling taks, unless it
428 * releases automatic barrier and the task still has the priority.
429 * It's hard to model automatic release therefore in this model the
430 * task is calling for release of the barriers if it was going to be the
431 * waiter that triggers the release.
432 *
433 */
434inline barrier_wait(self,bid,interval,rc) {
435  atomic{
436    if
437    ::  bid >= MAX_BARRIERS || bid <= 0 || !barriers[bid].isInitialised ->
438        rc = RC_InvId
439    ::  else -> // id is correct
440        barriers[bid].waiterCount++;
441        if
442        ::  barriers[bid].isAutomatic ->
443            bool sat;
444            satisfied(bid, sat) // check if enough waiters to release barrier
445            if
446            ::  sat ->
447                barrierRelease(self,bid);
448                rc = RC_OK
449            ::  else -> // !sat
450                barriers[bid].waiters[self] = true;
451                if
452                ::  interval > NO_TIMEOUT ->
453                    tasks[self].tout = false;
454                    tasks[self].ticks = interval;
455                    tasks[self].state = TimeWait;
456                    printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval);
457                ::  else ->
458                    tasks[self].state = BarrierWait;
459                    printf("@@@ %d STATE %d BarrierWait\n",_pid,self)
460                fi
461                waitAtBarrier(self,bid,rc)
462            fi
463        ::  else -> // !barriers[bid].isAutomatic
464            barriers[bid].waiters[self] = true;
465            if
466            ::  interval > NO_TIMEOUT ->
467                tasks[self].tout = false;
468                tasks[self].ticks = interval;
469                tasks[self].state = TimeWait
470                printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval);
471            ::  else ->
472                tasks[self].state = BarrierWait;
473                printf("@@@ %d STATE %d BarrierWait\n",_pid,self)
474            fi
475            waitAtBarrier(self,bid,rc)
476        fi
477    fi
478  }
479}
480
481/*
482 * barrier_release(self,bid,nreleased,rc)
483 *
484 * Simulates a call to rtems_barrier_release
485 *   self: if of the calling task
486 *   bid : id of the barrier
487 *   nrelease : contains number of released tasks if successful
488 *   rc : updated with the return code when the directive completes
489 *
490 * Corresponding RTEMS call:
491 *   rc = rtems_barrier_release(bid, nreleased);
492 *     `bid` models `rtems_id id`
493 *     `nreleased models `uint32_t` *released`
494 *
495 */
496inline barrier_release(self,bid,nreleased,rc) {
497  atomic{
498    if
499    ::  nreleased == 0 -> rc = RC_InvAddr;
500    ::  bid >= MAX_BARRIERS || bid <= 0 || !barriers[bid].isInitialised ->
501        rc = RC_InvId
502    ::  else ->
503        nreleased = barriers[bid].waiterCount;
504        barrierRelease(self,bid);
505        printf("@@@ %d LOG Barrier %d manually released\n", _pid, bid)
506        rc = RC_OK
507    fi
508  }
509}
510
511/*
512 * barrier_delete(self,bid,rc)
513 *
514 * Simulates a call to rtems_barrier_delete
515 *   bid : id of the barrier
516 *   rc : updated with the return code when the directive completes
517 *
518 * Corresponding RTEMS call:
519 *   rc = rtems_barrier_delete(bid);
520 *     `bid`  models `rtems_id id`
521 *
522 * All tasks waiting on deleted barrier are released
523 */
524inline barrier_delete(self,bid,rc) {
525  atomic{
526    if
527    ::  bid >= MAX_BARRIERS || bid <= 0 || !barriers[bid].isInitialised ->
528        rc = RC_InvId
529    ::  else ->
530        barriers[bid].isInitialised = false;
531        barrierRelease(self,bid);
532        printf("@@@ %d LOG Barrier %d deleted\n", _pid, bid)
533        rc = RC_OK
534    fi
535  }
536}
537
538/*
539 * Model Processes
540 * We shall use five processes in this model.
541 *  Three will represent the RTEMS tasks that will make use of the
542 *    barrier directives.
543 *  One will model a timer.
544 *  One will model scheduling and other task management behaviour.
545 */
546
547// These are not output to test generation
548#define TASK1_ID 1
549#define TASK2_ID 2
550#define TASK3_ID 3
551#define BARRIER1_NAME 1
552#define BARRIER2_NAME 2
553// In SMP setting there are different cores, but all are settled on same node.
554#define THIS_CORE 0
555#define THAT_CORE 1
556
557/*
558 * Scenario Generation
559 */
560
561 /*
562 * Task variants:
563 *   Task objectives - Barrier {Create, Acquire, Release, Delete}
564 *   timeout_length in {0,1,2...}
565 *   
566 * Task Scenarios:
567 *   vary: priority, preemptable, timeout interval, barrier options
568 */
569typedef TaskInputs {
570  bool doCreate; // will task create a barrier
571  bool isAutomatic; // if doCreate is true, specifies barrier type
572  int maxWaiters; // if isAutomatic is true, specifies max barrier waiters
573  byte bName; // Name of barrier to create or identify
574  bool doAcquire; // will task aquire the barrier
575  byte timeoutLength; // only relevant if doAcquire is true, gives wait time
576  bool doDelete; // will task delete the barrier
577  bool doRelease; // will task release the barrier
578
579  byte taskPrio;
580  bool taskPreempt;
581
582  bool idNull; // indicates whenever passed id is null
583  bool releasedNull // indicates whenever nreleased param is null
584};
585TaskInputs task_in[TASK_MAX];
586
587 /*
588 * Convenience function that assigns default options to a given `TaskInputs`
589 * structure.
590 */
591inline assignDefaults(defaults, opts) {
592  opts.doCreate = defaults.doCreate;
593  opts.isAutomatic = defaults.isAutomatic;
594  opts.maxWaiters = defaults.maxWaiters;
595  opts.doAcquire = defaults.doAcquire;
596  opts.timeoutLength = defaults.timeoutLength;
597  opts.doRelease = defaults.doRelease;
598  opts.doDelete = defaults.doDelete;
599  opts.taskPrio = defaults.taskPrio;
600  opts.taskPreempt = defaults.taskPreempt;
601  opts.bName = defaults.bName;
602  opts.idNull = defaults.idNull;
603  opts.releasedNull = defaults.releasedNull;
604}
605
606/*
607 * Semaphore Setup
608 */
609int task1Sema
610int task2Sema;
611int task3Sema;
612
613/*
614 * Multicore setup
615 */
616bool multicore;
617int task1Core;
618int task2Core;
619int task3Core;
620
621/*
622 * Generating Scenarios
623 *
624 * We consider the following broad scenario classes:
625 *
626 *   Manual Barrier - Check for barrier creation and manual release with delete
627 *   Automatic Barrier - Check for barrier creation and automatic release
628 *   Acquire ; Timeout ; Delete - check correct timeout and delete behaviour
629 *
630 */
631mtype = {ManAcqRel,AutoAcq,AutoToutDel};
632mtype scenario;
633
634inline chooseScenario() {
635  // Common Defaults
636  TaskInputs defaults;
637  defaults.doCreate = false;
638  defaults.isAutomatic = false;
639  defaults.maxWaiters = 0;
640  defaults.doAcquire = true;
641  defaults.timeoutLength = NO_TIMEOUT;
642  defaults.doRelease= false;
643  defaults.doDelete = false;
644  defaults.taskPrio = 2;
645  defaults.taskPreempt = false;
646  defaults.idNull = false;
647  defaults.releasedNull = false;
648  defaults.bName = BARRIER1_NAME;
649  // Set the defaults
650  assignDefaults(defaults, task_in[TASK1_ID]);
651  task_in[TASK1_ID].doCreate = true; // Task 1 is always the creator
652  assignDefaults(defaults, task_in[TASK2_ID]);
653  assignDefaults(defaults, task_in[TASK3_ID]);
654
655  // Semaphore initialization
656  semaphore[0] = false;
657  task1Sema = 0;
658  semaphore[1] = false;
659  task2Sema = 1;
660  semaphore[2] = false;
661  task3Sema = 2;
662
663  tasks[TASK1_ID].state = Ready;
664  tasks[TASK2_ID].state = Ready;
665  tasks[TASK3_ID].state = Ready;
666
667  multicore = false;
668  task1Core = THIS_CORE;
669  task2Core = THIS_CORE;
670  task3Core = THIS_CORE;
671
672  if
673  ::  scenario = ManAcqRel;
674  ::  scenario = AutoAcq;
675  ::  scenario = AutoToutDel;
676  fi
677  atomic{printf("@@@ %d LOG scenario ",_pid); printm(scenario); nl()} ;
678
679  if
680  ::  scenario == ManAcqRel ->
681        task_in[TASK1_ID].doAcquire = false;
682        task_in[TASK1_ID].doRelease = true;
683        task_in[TASK1_ID].doDelete = true;
684        if
685        ::  task_in[TASK1_ID].bName = 0;
686            printf( "@@@ %d LOG sub-senario bad create, invalid name\n", _pid);
687        ::  task_in[TASK1_ID].idNull = true;
688            printf( "@@@ %d LOG sub-senario bad create, passed id null\n",
689                      _pid);
690        ::  task_in[TASK2_ID].doAcquire = false;
691            task_in[TASK3_ID].doAcquire = false;
692            printf( "@@@ %d LOG sub-senario barrier not acquired\n", _pid);
693        ::  task_in[TASK2_ID].bName = 0;
694            printf( "@@@ %d LOG sub-senario Worker0 ident barrier name is 0\n",
695                      _pid);
696        ::  task_in[TASK1_ID].releasedNull = true;
697            printf( "@@@ %d LOG sub-senario realesed passed is null\n", _pid);
698        ::  task_in[TASK2_ID].idNull = true;
699            printf( "@@@ %d LOG sub-senario Worker0 ident passed id null\n",
700                      _pid);
701        /* ::  task_in[TASK2_ID].doAcquire = false;
702            task_in[TASK2_ID].doCreate = true;
703            task_in[TASK2_ID].bName = BARRIER2_NAME;
704            printf( "@@@ %d LOG sub-senario TooMany barriers created\n", _pid); */
705        ::  skip
706        fi
707  ::  scenario == AutoAcq ->
708        task_in[TASK1_ID].isAutomatic = true;
709        task_in[TASK1_ID].maxWaiters = MAX_WAITERS;
710        if
711        ::  task_in[TASK1_ID].maxWaiters = 0;
712            printf( "@@@ %d LOG sub-senario bad create, max_waiters is 0\n",
713                      _pid);
714        ::  skip
715        fi
716  ::  scenario == AutoToutDel ->
717        task_in[TASK1_ID].doAcquire = false;
718        task_in[TASK1_ID].isAutomatic = true;
719        task_in[TASK1_ID].maxWaiters = MAX_WAITERS;
720        task_in[TASK3_ID].timeoutLength = 4;
721        task_in[TASK3_ID].doDelete = true;
722  fi
723
724  // Multicore subscenario
725  if
726  ::  multicore = true;
727      // Its enough for the main creator task to be on another core to test
728      // everything
729      task1Core = THAT_CORE;
730      printf( "@@@ %d LOG sub-senario multicore enabled, cores:(%d,%d,%d)\n",
731                _pid, task1Core, task2Core, task3Core );
732  ::  skip
733  fi
734}
735
736proctype Runner (byte nid, taskid; TaskInputs opts) {
737  tasks[taskid].nodeid = nid;
738  tasks[taskid].pmlid = _pid;
739  tasks[taskid].prio = opts.taskPrio;
740
741  printf("@@@ %d TASK Runner\n",_pid);
742  if
743  :: tasks[taskid].prio == 1 -> printf("@@@ %d CALL HighPriority\n", _pid);
744  :: tasks[taskid].prio == 2 -> printf("@@@ %d CALL NormalPriority\n", _pid);
745  :: tasks[taskid].prio == 3 -> printf("@@@ %d CALL LowPriority\n", _pid);
746  fi
747  // Preemption check setup, uncomment if necessary
748  //printf("@@@ %d CALL StartLog\n",_pid);
749  byte rc;
750  byte bid;
751  if
752  :: opts.idNull -> bid = 0;
753  :: else -> bid = 1;
754  fi
755
756  if
757  :: multicore ->
758       printf("@@@ %d CALL SetProcessor %d\n", _pid, tasks[taskid].nodeid);
759  :: else -> skip
760  fi
761
762  if
763  ::  opts.doCreate ->
764        printf("@@@ %d CALL barrier_create %d %d %d %d\n"
765                ,_pid, opts.bName, opts.isAutomatic, opts.maxWaiters, bid);
766                  /*  (name,       attribs,          max_waiters,     id, rc) */
767        barrier_create(opts.bName, opts.isAutomatic, opts.maxWaiters, bid, rc);
768        if
769        :: rc == RC_OK ->
770            printf("@@@ %d SCALAR created %d\n", _pid, bid);
771        :: else -> skip;
772        fi
773        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
774  ::  else ->
775        printf("@@@ %d CALL barrier_ident %d %d\n", _pid, opts.bName, bid);
776                  /* (name,      id, rc) */
777        barrier_ident(opts.bName,bid,rc);
778        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
779  fi
780  Release(task2Sema);
781
782  if
783  ::  opts.doAcquire ->
784        printf("@@@ %d CALL barrier_wait %d %d\n",
785                _pid, bid, opts.timeoutLength);
786                 /* (self,   bid, timeout,            rc) */
787        barrier_wait(taskid, bid, opts.timeoutLength, rc);
788        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
789  ::  else -> skip
790  fi
791
792  if
793  ::  opts.doRelease ->
794        Obtain(task1Sema);
795        int nreleased;
796        if
797        :: opts.releasedNull -> nreleased = 0;
798        :: else -> nreleased = 1;
799        fi
800        int toRelease = barriers[bid].waiterCount;
801        printf("@@@ %d CALL barrier_release %d %d\n", _pid, bid, nreleased);
802                    /* (self,   bid, nreleased, rc) */
803        barrier_release(taskid, bid, nreleased, rc);
804        if
805        :: rc == RC_OK ->
806            printf("@@@ %d SCALAR released %d\n", _pid, toRelease);
807        :: else -> skip;
808        fi
809        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
810        Release(task1Sema);
811  ::  else -> skip
812  fi
813
814  if
815  ::  opts.doDelete ->
816        Obtain(task1Sema);
817        printf("@@@ %d CALL barrier_delete %d\n",_pid, bid);
818                  /*  (self,   bid, rc) */
819        barrier_delete(taskid, bid, rc);
820        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
821        Release(task1Sema);
822  ::  else -> skip
823  fi
824
825  // Make sure everyone ran
826  Obtain(task1Sema);
827  // Wait for other tasks to finish
828  Obtain(task2Sema);
829  Obtain(task3Sema);
830
831  printf("@@@ %d LOG Task %d finished\n",_pid,taskid);
832  tasks[taskid].state = Zombie;
833  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
834}
835
836proctype Worker0 (byte nid, taskid; TaskInputs opts) {
837  tasks[taskid].nodeid = nid;
838  tasks[taskid].pmlid = _pid;
839  tasks[taskid].prio = opts.taskPrio;
840
841  printf("@@@ %d TASK Worker0\n",_pid);
842  if
843  :: tasks[taskid].prio == 1 -> printf("@@@ %d CALL HighPriority\n", _pid);
844  :: tasks[taskid].prio == 2 -> printf("@@@ %d CALL NormalPriority\n", _pid);
845  :: tasks[taskid].prio == 3 -> printf("@@@ %d CALL LowPriority\n", _pid);
846  fi
847  // Preemption check setup, uncomment if necessary
848  //printf("@@@ %d CALL StartLog\n",_pid);
849  byte rc;
850  byte bid;
851  if
852  :: opts.idNull -> bid = 0;
853  :: else -> bid = 1;
854  fi
855
856  if
857  :: multicore ->
858       printf("@@@ %d CALL SetProcessor %d\n", _pid, tasks[taskid].nodeid);
859  :: else -> skip
860  fi
861
862  Obtain(task2Sema);
863  if
864  ::  opts.doCreate ->
865        printf("@@@ %d CALL barrier_create %d %d %d %d\n"
866                ,_pid, opts.bName, opts.isAutomatic, opts.maxWaiters, bid);
867                  /*  (name,       attribs,          max_waiters,     id, rc) */
868        barrier_create(opts.bName, opts.isAutomatic, opts.maxWaiters, bid, rc);
869        if
870        :: rc == RC_OK ->
871            printf("@@@ %d SCALAR created %d\n", _pid, bid);
872        :: else -> skip;
873        fi
874        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
875  ::  else ->
876        printf("@@@ %d CALL barrier_ident %d %d\n", _pid, opts.bName, bid);
877                  /* (name,      id, rc) */
878        barrier_ident(opts.bName,bid,rc);
879        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
880  fi
881
882  if
883  ::  opts.doAcquire ->
884        atomic{
885          Release(task3Sema);
886          printf("@@@ %d CALL barrier_wait %d %d\n",
887                    _pid, bid, opts.timeoutLength);         
888                   /* (self,   bid, timeout,            rc) */
889          barrier_wait(taskid, bid, opts.timeoutLength, rc);
890        }
891        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
892  ::  else -> Release(task3Sema);
893  fi
894
895  if
896  ::  opts.doRelease ->
897        int nreleased;
898        if
899        :: opts.releasedNull -> nreleased = 0;
900        :: else -> nreleased = 1;
901        fi
902        int toRelease = barriers[bid].waiterCount;
903        printf("@@@ %d CALL barrier_release %d %d\n", _pid, bid, nreleased);
904                    /* (self,   bid, nreleased, rc) */
905        barrier_release(taskid, bid, nreleased, rc);
906        if
907        :: rc == RC_OK ->
908            printf("@@@ %d SCALAR released %d\n", _pid, toRelease);
909        :: else -> skip;
910        fi
911        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
912  ::  else -> skip
913  fi
914
915  if
916  ::  opts.doDelete ->
917        printf("@@@ %d CALL barrier_delete %d\n",_pid, bid);
918                  /*  (self,   bid, rc) */
919        barrier_delete(taskid, bid, rc);
920        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
921  ::  else -> skip
922  fi
923  atomic{
924    Release(task2Sema);
925    printf("@@@ %d LOG Task %d finished\n",_pid,taskid);
926    tasks[taskid].state = Zombie;
927    printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
928  }
929}
930
931proctype Worker1 (byte nid, taskid; TaskInputs opts) {
932  tasks[taskid].nodeid = nid;
933  tasks[taskid].pmlid = _pid;
934  tasks[taskid].prio = opts.taskPrio;
935
936  printf("@@@ %d TASK Worker1\n",_pid);
937  if
938  :: tasks[taskid].prio == 1 -> printf("@@@ %d CALL HighPriority\n", _pid);
939  :: tasks[taskid].prio == 2 -> printf("@@@ %d CALL NormalPriority\n", _pid);
940  :: tasks[taskid].prio == 3 -> printf("@@@ %d CALL LowPriority\n", _pid);
941  fi
942  // Preemption check setup, uncomment if necessary
943  //printf("@@@ %d CALL StartLog\n",_pid);
944  byte rc;
945  byte bid;
946  if
947  :: opts.idNull -> bid = 0;
948  :: else -> bid = 1;
949  fi
950
951  if
952  :: multicore ->
953       printf("@@@ %d CALL SetProcessor %d\n", _pid, tasks[taskid].nodeid);
954  :: else -> skip
955  fi
956  Obtain(task3Sema);
957
958  if
959  ::  opts.doCreate ->
960        printf("@@@ %d CALL barrier_create %d %d %d %d\n"
961                ,_pid, opts.bName, opts.isAutomatic, opts.maxWaiters, bid);
962                  /*  (name,       attribs,          max_waiters,     id, rc) */
963        barrier_create(opts.bName, opts.isAutomatic, opts.maxWaiters, bid, rc);
964        if
965        :: rc == RC_OK ->
966            printf("@@@ %d SCALAR created %d\n", _pid, bid);
967        :: else -> skip;
968        fi
969        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
970  ::  else ->
971        printf("@@@ %d CALL barrier_ident %d %d\n", _pid, opts.bName, bid);
972                  /* (name,      id, rc) */
973        barrier_ident(opts.bName,bid,rc);
974        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
975  fi
976
977  if
978  ::  opts.doAcquire ->
979        atomic{
980          Release(task1Sema);
981          printf("@@@ %d CALL barrier_wait %d %d\n",
982                    _pid, bid, opts.timeoutLength);         
983                   /* (self,   bid, timeout,            rc) */
984          barrier_wait(taskid, bid, opts.timeoutLength, rc);
985        }
986        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
987  ::  else -> Release(task1Sema);
988  fi
989
990  if
991  ::  opts.doRelease ->
992        int nreleased;
993        if
994        :: opts.releasedNull -> nreleased = 0;
995        :: else -> nreleased = 1;
996        fi
997        int toRelease = barriers[bid].waiterCount;
998        printf("@@@ %d CALL barrier_release %d %d\n", _pid, bid, nreleased);
999                    /* (self,   bid, nreleased, rc) */
1000        barrier_release(taskid, bid, nreleased, rc);
1001        if
1002        :: rc == RC_OK ->
1003            printf("@@@ %d SCALAR released %d\n", _pid, toRelease);
1004        :: else -> skip;
1005        fi
1006        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
1007  ::  else -> skip
1008  fi
1009
1010  if
1011  ::  opts.doDelete ->
1012        printf("@@@ %d CALL barrier_delete %d\n",_pid, bid);
1013                  /*  (self,   bid, rc) */
1014        barrier_delete(taskid, bid, rc);
1015        printf("@@@ %d SCALAR rc %d\n",_pid, rc);
1016  ::  else -> skip
1017  fi
1018  atomic {
1019    Release(task3Sema);
1020    printf("@@@ %d LOG Task %d finished\n",_pid,taskid);
1021    tasks[taskid].state = Zombie;
1022    printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
1023  }
1024}
1025
1026bool stopclock = false;
1027
1028/*
1029 * We need a process that periodically wakes up blocked processes.
1030 * This is modelling background behaviour of the system,
1031 * such as ISRs and scheduling.
1032 * We visit all tasks in round-robin order (to prevent starvation)
1033 * and make them ready if waiting on "other" things.
1034 * Tasks waiting for events or timeouts are not touched
1035 * This terminates when all tasks are zombies.
1036 */
1037proctype System () {
1038  byte taskid ;
1039  bool liveSeen;
1040
1041  printf("@@@ %d LOG System running...\n",_pid);
1042
1043  loop:
1044  taskid = 1;
1045  liveSeen = false;
1046
1047  printf("@@@ %d LOG Loop through tasks...\n",_pid);
1048  atomic {
1049    printf("@@@ %d LOG Scenario is ",_pid);
1050    printm(scenario); nl();
1051  }
1052  do   // while taskid < TASK_MAX ....
1053  ::  taskid == TASK_MAX -> break;
1054  ::  else ->
1055      atomic {
1056        printf("@@@ %d LOG Task %d state is ",_pid,taskid);
1057        printm(tasks[taskid].state); nl()
1058      }
1059      if
1060      :: tasks[taskid].state == Zombie -> taskid++
1061      :: else ->
1062         if
1063         ::  tasks[taskid].state == OtherWait
1064             -> tasks[taskid].state = Ready
1065                printf("@@@ %d LOG %d Ready\n",_pid,taskid)
1066         ::  else -> skip
1067         fi
1068         liveSeen = true;
1069         taskid++
1070      fi
1071  od
1072
1073  printf("@@@ %d LOG ...all visited, live:%d\n",_pid,liveSeen);
1074
1075  if
1076  ::  liveSeen -> goto loop
1077  ::  else
1078  fi
1079  printf("@@@ %d LOG All are Zombies, game over.\n",_pid);
1080  stopclock = true;
1081}
1082
1083
1084/*
1085 * We need a process that handles a clock tick,
1086 * by decrementing the tick count for tasks waiting on a timeout.
1087 * Such a task whose ticks become zero is then made Ready,
1088 * and its timer status is flagged as a timeout
1089 * This terminates when all tasks are zombies
1090 * (as signalled by System via `stopclock`).
1091 */
1092proctype Clock () {
1093  int tid, tix;
1094  printf("@@@ %d LOG Clock Started\n",_pid)
1095  do
1096  ::  stopclock  -> goto stopped
1097  ::  !stopclock ->
1098      printf(" (tick) \n");
1099      tid = 1;
1100      do
1101      ::  tid == TASK_MAX -> break
1102      ::  else ->
1103          atomic{
1104            printf("Clock: tid=%d, state=",tid); printm(tasks[tid].state); nl()
1105          };
1106          if
1107          ::  tasks[tid].state == TimeWait ->
1108              tix = tasks[tid].ticks - 1;
1109              // printf("Clock: ticks=%d, tix=%d\n",tasks[tid].ticks,tix);
1110              if
1111              ::  tix == 0
1112                  tasks[tid].tout = true
1113                  tasks[tid].state = Ready
1114                  printf("@@@ %d LOG %d Ready\n",_pid,tid)
1115              ::  else
1116                  tasks[tid].ticks = tix
1117              fi
1118          ::  else // state != TimeWait
1119          fi
1120          tid = tid + 1
1121      od
1122  od
1123stopped:
1124  printf("@@@ %d LOG Clock Stopped\n",_pid);
1125}
1126
1127
1128init {
1129  pid nr;
1130
1131  printf("Barrier Manager Model running.\n");
1132  printf("Setup...\n");
1133
1134  printf("@@@ %d LOG TestName: Barrier_Manager_TestGen\n",_pid)
1135  outputDefines();
1136  outputDeclarations();
1137
1138  printf("@@@ %d INIT\n",_pid);
1139  chooseScenario();
1140
1141
1142  printf("Run...\n");
1143
1144  run System();
1145  run Clock();
1146
1147  run Runner(task1Core,TASK1_ID,task_in[TASK1_ID]);
1148  run Worker0(task2Core,TASK2_ID,task_in[TASK2_ID]);
1149  run Worker1(task3Core,TASK3_ID,task_in[TASK3_ID]);
1150
1151  _nr_pr == 1;
1152
1153//#ifdef TEST_GEN
1154  assert(false);
1155//#endif
1156
1157  printf("Barrier Manager Model finished !\n")
1158}
Note: See TracBrowser for help on using the repository browser.