source: rtems-central/formal/promela/models/messages/msg-mgr-model-run.h @ 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: 4.8 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3/*
4static void Worker{0}( rtems_task_argument arg )
5{{
6  Context *ctx;
7
8  ctx = (Context *) arg;
9  rtems_event_set events;
10
11  T_log( T_NORMAL, "Worker Running" );
12  TestSegment4( ctx );
13  T_log( T_NORMAL, "Worker finished" );
14
15  rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
16}}
17
18
19RTEMS_ALIGNED( RTEMS_TASK_STORAGE_ALIGNMENT ) static char WorkerStorage{0}[
20  RTEMS_TASK_STORAGE_SIZE(
21    MAX_TLS_SIZE + RTEMS_MINIMUM_STACK_SIZE,
22    WORKER_ATTRIBUTES
23  )
24];
25
26static const rtems_task_config WorkerConfig{0} = {{
27  .name = rtems_build_name( 'W', 'O', 'R', 'K' ),
28  .initial_priority = PRIO_LOW,
29  .storage_area = WorkerStorage{0},
30  .storage_size = sizeof( WorkerStorage{0} ),
31  .maximum_thread_local_storage_size = MAX_TLS_SIZE,
32  .initial_modes = RTEMS_DEFAULT_MODES,
33  .attributes = WORKER_ATTRIBUTES
34}};
35
36*/
37static void Worker1( rtems_task_argument arg )
38{{
39  Context *ctx;
40
41  ctx = (Context *) arg;
42  rtems_event_set events;
43
44  T_log( T_NORMAL, "Worker1 Running" );
45  TestSegment4( ctx );
46  T_log( T_NORMAL, "Worker1 finished" );
47
48  rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
49}}
50
51static void Worker2( rtems_task_argument arg )
52{{
53  Context *ctx;
54
55  ctx = (Context *) arg;
56  rtems_event_set events;
57
58  T_log( T_NORMAL, "Worker2 Running" );
59  TestSegment5( ctx );
60  T_log( T_NORMAL, "Worker2 finished" );
61
62  rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
63}}
64
65static void RtemsModelMessageMgr_Setup{0}(
66  RtemsModelMessageMgr_Context *ctx
67)
68{{
69  rtems_status_code   sc;
70  rtems_task_priority prio;
71
72  T_log( T_NORMAL, "Runner Setup" );
73
74  memset( ctx, 0, sizeof( *ctx ) );
75  ctx->runner_thread = _Thread_Get_executing();
76  ctx->runner_id = ctx->runner_thread->Object.id;
77  ctx->worker1_wakeup = CreateWakeupSema();
78  ctx->worker2_wakeup = CreateWakeupSema();
79  ctx->runner_wakeup = CreateWakeupSema();
80
81  sc = rtems_task_get_scheduler( RTEMS_SELF, &ctx->runner_sched );
82  T_rsc_success( sc );
83
84  #if defined(RTEMS_SMP)
85  sc = rtems_scheduler_ident_by_processor( 1, &ctx->other_sched );
86  T_rsc_success( sc );
87  T_ne_u32( ctx->runner_sched, ctx->other_sched );
88  #endif
89
90  prio = 0;
91  sc = rtems_task_set_priority( RTEMS_SELF, PRIO_NORMAL, &prio );
92  T_rsc_success( sc );
93  T_eq_u32( prio, PRIO_HIGH );
94
95  //sc = rtems_task_construct( &WorkerConfig{0}, &ctx->worker_id );
96  //T_log( T_NORMAL, "Construct Worker, sc = %x", sc );
97  //T_assert_rsc_success( sc );
98
99  //T_log( T_NORMAL, "Starting Worker..." );
100  //sc = rtems_task_start( ctx->worker_id, Worker{0}, (rtems_task_argument) ctx );
101  //T_log( T_NORMAL, "Started Worker, sc = %x", sc );
102  //T_assert_rsc_success( sc );
103
104  sc = rtems_task_create("WRKR",
105                          PRIO_NORMAL,
106                          RTEMS_MINIMUM_STACK_SIZE,
107                          RTEMS_DEFAULT_MODES,
108                          RTEMS_DEFAULT_ATTRIBUTES,
109                          &ctx->worker1_id);
110  T_assert_rsc_success( sc );
111
112  T_log( T_NORMAL, "Starting Worker1..." );
113  sc = rtems_task_start( ctx->worker1_id, Worker1,ctx );
114  T_log( T_NORMAL, "Started Worker1, sc = %x", sc );
115  T_assert_rsc_success( sc );
116
117  sc = rtems_task_create("WRKR",
118                          PRIO_NORMAL,
119                          RTEMS_MINIMUM_STACK_SIZE,
120                          RTEMS_DEFAULT_MODES,
121                          RTEMS_DEFAULT_ATTRIBUTES,
122                          &ctx->worker2_id);
123  T_assert_rsc_success( sc );
124
125  T_log( T_NORMAL, "Starting Worker2..." );
126  sc = rtems_task_start( ctx->worker2_id, Worker2,ctx );
127  T_log( T_NORMAL, "Started Worker2, sc = %x", sc );
128  T_assert_rsc_success( sc );
129
130}}
131
132
133static void RtemsModelMessageMgr_Setup_Wrap{0}( void *arg )
134{{
135  RtemsModelMessageMgr_Context *ctx;
136
137  ctx = arg;
138  RtemsModelMessageMgr_Setup{0}( ctx );
139}}
140
141
142static RtemsModelMessageMgr_Context RtemsModelMessageMgr_Instance{0};
143
144static T_fixture RtemsModelMessageMgr_Fixture{0} = {{
145  .setup = RtemsModelMessageMgr_Setup_Wrap{0},
146  .stop = NULL,
147  .teardown = RtemsModelMessageMgr_Teardown_Wrap,
148  .scope = RtemsModelMessageMgr_Scope,
149  .initial_context = &RtemsModelMessageMgr_Instance{0}
150}};
151
152static T_fixture_node RtemsModelMessageMgr_Node{0};
153
154void RtemsModelMessageMgr_Run{0}()
155{{
156  RtemsModelMessageMgr_Context *ctx;
157
158  T_set_verbosity( T_NORMAL );
159
160  T_log( T_NORMAL, "Runner Invoked" );
161  T_log( T_NORMAL, "Pushing Test Fixture..." );
162
163
164  ctx = T_push_fixture(
165    &RtemsModelMessageMgr_Node{0},
166    &RtemsModelMessageMgr_Fixture{0}
167  );
168
169  T_log( T_NORMAL, "Test Fixture Pushed" );
170
171
172
173  ctx->this_test_number = {0};
174
175
176  ctx->send_status = RTEMS_INCORRECT_STATE;
177  ctx->receive_option_set = 0;
178  ctx->receive_timeout = RTEMS_NO_TIMEOUT;
179  _Thread_Wait_flags_set( ctx->runner_thread, THREAD_WAIT_CLASS_PERIOD );
180
181  TestSegment0( ctx );
182
183  Runner( ctx );
184
185  RtemsModelMessageMgr_Cleanup( ctx );
186
187  T_log( T_NORMAL, "Run Pop Fixture" );
188  T_pop_fixture();
189}}
190
191/** @}} */
Note: See TracBrowser for help on using the repository browser.