source: rtems-central/formal/promela/models/barriers/barrier-mgr-model-run.h @ 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: 2.4 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3static void RtemsModelBarrierMgr_Setup{0}( void *arg )
4{{
5  RtemsModelBarrierMgr_Context *ctx;
6  ctx = arg;
7
8  rtems_status_code   sc;
9  rtems_task_priority prio;
10
11  T_log( T_NORMAL, "Runner Setup" );
12  memset( ctx, 0, sizeof( *ctx ) );
13  ctx->runner_thread = _Thread_Get_executing();
14  ctx->runner_id = ctx->runner_thread->Object.id;
15
16  T_log( T_NORMAL, "Creating Runner Semaphore" );
17  ctx->runner_sema = CreateSema("RUNR");
18
19  T_log( T_NORMAL, "Creating Worker0 Semaphore" );
20  ctx->worker0_sema = CreateSema("WRS0");
21
22  T_log( T_NORMAL, "Creating Worker1 Semaphore" );
23  ctx->worker1_sema = CreateSema("WRS1");
24
25  sc = rtems_task_get_scheduler( RTEMS_SELF, &ctx->runner_sched );
26  T_rsc_success( sc );
27
28  #if defined(RTEMS_SMP)
29  sc = rtems_scheduler_ident_by_processor( 1, &ctx->other_sched );
30  T_rsc_success( sc );
31  T_ne_u32( ctx->runner_sched, ctx->other_sched );
32  #endif
33
34  prio = 0;
35  sc = rtems_task_set_priority( RTEMS_SELF, BM_PRIO_NORMAL, &prio );
36  T_rsc_success( sc );
37  T_eq_u32( prio, BM_PRIO_HIGH );
38
39  ctx->worker0_id = CreateTask( "WRK0", BM_PRIO_NORMAL );
40  T_log( T_NORMAL, "Created Worker 0");
41  StartTask( ctx->worker0_id, Worker0, ctx );
42  T_log( T_NORMAL, "Started Worker 0");
43
44  ctx->worker1_id = CreateTask( "WRK1", BM_PRIO_NORMAL );
45  T_log( T_NORMAL, "Created Worker 1");
46  StartTask( ctx->worker1_id, Worker1, ctx );
47  T_log( T_NORMAL, "Started Worker 1");
48}}
49
50static RtemsModelBarrierMgr_Context RtemsModelBarrierMgr_Instance{0};
51
52static T_fixture RtemsModelBarrierMgr_Fixture{0} = {{
53  .setup = RtemsModelBarrierMgr_Setup{0},
54  .stop = NULL,
55  .teardown = RtemsModelBarrierMgr_Teardown,
56  .scope = RtemsModelBarrierMgr_Scope,
57  .initial_context = &RtemsModelBarrierMgr_Instance{0}
58}};
59
60static T_fixture_node RtemsModelBarrierMgr_Node{0};
61
62void RtemsModelBarrierMgr_Run{0}()
63{{
64  RtemsModelBarrierMgr_Context *ctx;
65
66  T_set_verbosity( T_NORMAL );
67  T_log( T_NORMAL, "Pushing Test Fixture..." );
68
69  ctx = T_push_fixture(
70    &RtemsModelBarrierMgr_Node{0},
71    &RtemsModelBarrierMgr_Fixture{0}
72  );
73  // This runs RtemsModelBarrierMgr_Fixture
74  T_log( T_NORMAL, "Test Fixture Pushed" );
75
76  ctx->this_test_number = {0};
77
78  memset( &ctx->thread_switch_log, 0, sizeof( ctx->thread_switch_log ) );
79  _Thread_Wait_flags_set( ctx->runner_thread, THREAD_WAIT_CLASS_PERIOD );
80
81  TestSegment0( ctx );
82
83  Runner( ctx );
84
85  RtemsModelBarrierMgr_Cleanup( ctx );
86
87  T_log( T_NORMAL, "Run Pop Fixture" );
88  T_pop_fixture();
89}}
90
91/** @}} */
Note: See TracBrowser for help on using the repository browser.