source: rtems-central/formal/promela/models/messages/msg-mgr-model-rfn.yml @ 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: 5.3 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3LANGUAGE: C
4
5SEGNAMEPFX: TestSegment{} # segnumber
6SEGARG: Context* ctx
7SEGDECL: static void {}( {} )  # segnamepf{segnumber}, segarg,
8SEGBEGIN: " {"
9SEGEND: "}"
10
11NAME: |
12  /* Test Name is defined in the Test Case code (tc-model-msg-mgr.c) */
13
14semaphore_DCL: rtems_id {0}[SEMA_MAX];
15
16sendrc_DCL: rtems_status_code
17
18recrc_DCL: rtems_status_code
19
20qrc_DCL: rtems_status_code
21
22queue_buffer_DCL: RTEMS_MESSAGE_QUEUE_BUFFER( MAX_MESSAGE_SIZE ) {0} [MAX_PENDING_MESSAGES];
23
24receive_buffer_DCL: uint8_t {0} [ MAX_MESSAGE_SIZE ];
25
26send_buffer_DCL: uint8_t {0} [ MAX_MESSAGE_SIZE ];
27
28send_counter_DCL: uint8_t
29
30INIT: |
31  initialise_semaphore( ctx, semaphore );
32
33Runner: |
34  checkTaskIs( ctx->runner_id );
35
36Worker1: |
37  checkTaskIs( ctx->worker1_id );
38
39Worker2: |
40  checkTaskIs( ctx->worker2_id );
41
42SIGNAL: |
43  Wakeup( semaphore[{}] );
44
45WAIT: |
46  Wait( semaphore[{}] );
47
48message_queue_construct: |
49  T_log( T_NORMAL, "Calling construct(%d,%d,%d,%d,%d)");
50
51  rtems_message_queue_config config;
52  config.name = {3};
53  config.maximum_pending_messages = MAX_PENDING_MESSAGES;
54  config.maximum_message_size = MAX_MESSAGE_SIZE;
55  config.storage_area = queue_buffer;
56  config.storage_size = sizeof( queue_buffer );
57  config.storage_free = NULL;
58  config.attributes = RTEMS_DEFAULT_ATTRIBUTES;
59 
60  {5} = rtems_message_queue_construct(
61    &config,
62    &ctx->queue_id
63  );
64  T_log(T_NORMAL, "Queue id 0x%x", ctx->queue_id);
65  T_log( T_NORMAL, "Returned 0x%x from construct", {5} );
66
67 
68
69message_queue_send: |
70  T_log( T_NORMAL, "Calling Send(%d,%d)");
71
72  memset( send_buffer, {2}, {3} );
73 
74  {4} = rtems_message_queue_send(
75    idNull(ctx, {1}),
76    {2} ? send_buffer : NULL,
77    {3}
78  );
79
80  T_log( T_NORMAL, "Returned 0x%x from send", {4} );
81
82message_queue_receive: |
83  T_log( T_NORMAL, "Calling Receive(%d,%d)");
84  size_t receive_size;
85  {4} = rtems_message_queue_receive(
86  idNull(ctx, {1}),
87  receive_buffer,
88  &receive_size,
89  mergeopts({2}),
90  getTimeout({3})
91  );
92  T_log( T_NORMAL, "Returned 0x%x from receive", {4} );
93
94sendrc:
95  T_rsc( sendrc, {0} );
96
97recrc:
98  T_rsc( recrc, {0} );
99
100qrc:
101  T_rsc( qrc, {0} );
102
103recout:
104  T_eq_int( recout[{0}], {1} );
105
106Ready: |
107   /* We (Task {0}) must have been recently ready because we are running */
108
109Zombie:
110  /* Code to check that Task {0} has terminated */
111
112EventWait:
113  /* Code to check that Task {0} is waiting on events */
114
115TimeWait:
116  /* Code to check that Task {0} is waiting on a timer */
117
118OtherWait:
119  /* Code to check that Task {0} is waiting (after pre-emption) */
120
121SUSPEND:
122  /* SWITCH[{0}] Suspension of proc{1} in favour of proc{2} */
123
124WAKEUP:
125  /* SWITCH[{0}] Wakeup of proc{1} (sometime) after proc{2} */
126 
127LowerPriority: |
128  SetSelfPriority( PRIO_LOW );
129  rtems_task_priority prio;
130  rtems_status_code sc;
131  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
132  T_rsc_success( sc );
133  T_eq_u32( prio, PRIO_LOW );
134
135EqualPriority: |
136  SetSelfPriority( PRIO_NORMAL );
137  rtems_task_priority prio;
138  rtems_status_code sc;
139  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
140  T_rsc_success( sc );
141  T_eq_u32( prio, PRIO_NORMAL );
142
143HigherPriority: |
144  SetSelfPriority( PRIO_HIGH );
145  rtems_task_priority prio;
146  rtems_status_code sc;
147  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
148  T_rsc_success( sc );
149  T_eq_u32( prio, PRIO_HIGH );
150
151  StartLog: |
152  T_thread_switch_log *log;
153  log = T_thread_switch_record_4( &ctx->thread_switch_log );
154
155CheckPreemption: |
156  log = &ctx->thread_switch_log;
157  T_eq_sz( log->header.recorded, 2 );
158  T_eq_u32( log->events[ 0 ].heir, ctx->runner_id );
159  T_eq_u32( log->events[ 1 ].heir, ctx->worker_id );
160
161CheckNoPreemption: |
162  log = &ctx->thread_switch_log;
163  T_le_sz( log->header.recorded, 1 );
164  for ( size_t i = 0; i < log->header.recorded; ++i ) {
165    T_ne_u32( log->events[ i ].executing, ctx->worker_id );
166    T_eq_u32( log->events[ i ].heir, ctx->runner_id );
167  }
168
169RunnerScheduler: |
170  uint32_t processor = {};
171  rtems_status_code sc1;
172  rtems_id current_sched;
173  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
174  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
175  sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->runner_sched );
176  T_rsc_success( sc1 );
177  T_log( T_NORMAL, "runner scheduler id: %d", &ctx->runner_sched);
178  sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->runner_sched, RTEMS_CURRENT_PRIORITY);
179  T_rsc_success( sc1 );
180  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
181  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
182
183OtherScheduler: |
184  uint32_t processor = {};
185  rtems_status_code sc1;
186  rtems_id current_sched;
187  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
188  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
189  sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->other_sched );
190  T_rsc_success( sc1 );
191  T_log( T_NORMAL, "other scheduler id: %d", &ctx->other_sched);
192  sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->other_sched, RTEMS_CURRENT_PRIORITY);
193  T_rsc_success( sc1 );
194  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
195  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
196
197SetProcessor: |
198  T_eq_u32( rtems_scheduler_get_processor_maximum(), 2 );
199  uint32_t processor = {};
200  cpu_set_t cpuset;
201  CPU_ZERO(&cpuset);
202  CPU_SET(processor, &cpuset);
Note: See TracBrowser for help on using the repository browser.