source: rtems-central/formal/promela/models/events/event-mgr-model-rfn.yml @ 285cae9

Last change on this file since 285cae9 was 285cae9, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/10/23 at 19:49:26

Memory Manager model and test gen material

  • Property mode set to 100644
File size: 5.8 KB
Line 
1# SPDX-License-Identifier: BSD-2-Clause
2# Event Manager: Promela to RTEMS Refinement
3
4# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
5#
6# Redistribution and use in source and binary forms, with or without
7# modification, are permitted provided that the following conditions
8# are met:
9# 1. Redistributions of source code must retain the above copyright
10#    notice, this list of conditions and the following disclaimer.
11# 2. Redistributions in binary form must reproduce the above copyright
12#    notice, this list of conditions and the following disclaimer in the
13#    documentation and/or other materials provided with the distribution.
14#
15# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25# POSSIBILITY OF SUCH DAMAGE.
26LANGUAGE: C
27
28SEGNAMEPFX: TestSegment{} # segnumber
29SEGARG: Context* ctx
30SEGDECL: static void {}( {} )  # segnamepf{segnumber}, segarg,
31SEGBEGIN: " {"
32SEGEND: "}"
33
34NAME: |
35  /* Test Name is defined in the Test Case code (tc-model-events-mgr.c) */
36
37pending_DCL: rtems_event_set {0}[TASK_MAX];
38
39semaphore_DCL: rtems_id {0}[SEMA_MAX];
40
41sendrc_DCL: rtems_status_code
42
43recrc_DCL: rtems_status_code
44
45recout_DCL: rtems_event_set {0}[TASK_MAX];
46
47INIT: |
48  initialise_pending( pending, TASK_MAX );
49  initialise_semaphore( ctx, semaphore );
50
51Runner: |
52  checkTaskIs( ctx->runner_id );
53
54Worker: |
55  checkTaskIs( ctx->worker_id );
56
57SIGNAL: |
58  Wakeup( semaphore[{}] );
59
60WAIT: |
61  Wait( semaphore[{}] );
62
63event_send: |
64  T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, {1}), {2} );
65  {3} = ( *ctx->send )( mapid( ctx, {1} ), {2} );
66  T_log( T_NORMAL, "Returned 0x%x from Send", {3} );
67
68event_receive: |
69  T_log( T_NORMAL, "Calling Receive(%d,%d,%d,%d)", {0}, mergeopts( {1}, {2} ) ,{3} , {4} ? &recout[{4}] : NULL );
70  {5} = ( *ctx->receive )( {0}, mergeopts( {1}, {2} ), {3}, {4} ? &recout[{4}] : NULL );
71  T_log( T_NORMAL, "Returned 0x%x from Receive", {5} );
72
73sendrc:
74  T_rsc( sendrc, {0} );
75
76recrc:
77  T_rsc( recrc, {0} );
78
79pending: |
80  pending[{0}] = GetPending( ctx );
81  T_eq_int( pending[{0}], {1} );
82
83recout:
84  T_eq_int( recout[{0}], {1} );
85
86Ready: |
87   /* We (Task {0}) must have been recently ready because we are running */
88
89Zombie:
90  /* Code to check that Task {0} has terminated */
91
92EventWait:
93  /* Code to check that Task {0} is waiting on events */
94
95TimeWait:
96  /* Code to check that Task {0} is waiting on a timer */
97
98OtherWait:
99  /* Code to check that Task {0} is waiting (after pre-emption) */
100
101SUSPEND:
102  /* SWITCH[{0}] Suspension of proc{1} in favour of proc{2} */
103
104WAKEUP:
105  /* SWITCH[{0}] Wakeup of proc{1} (sometime) after proc{2} */
106
107LowerPriority: |
108  SetSelfPriority( PRIO_LOW );
109  rtems_task_priority prio;
110  rtems_status_code sc;
111  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
112  T_rsc_success( sc );
113  T_eq_u32( prio, PRIO_LOW );
114
115EqualPriority: |
116  SetSelfPriority( PRIO_NORMAL );
117  rtems_task_priority prio;
118  rtems_status_code sc;
119  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
120  T_rsc_success( sc );
121  T_eq_u32( prio, PRIO_NORMAL );
122
123HigherPriority: |
124  SetSelfPriority( PRIO_HIGH );
125  rtems_task_priority prio;
126  rtems_status_code sc;
127  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
128  T_rsc_success( sc );
129  T_eq_u32( prio, PRIO_HIGH );
130
131StartLog: |
132  T_thread_switch_log *log;
133  log = T_thread_switch_record_4( &ctx->thread_switch_log );
134
135CheckPreemption: |
136  log = &ctx->thread_switch_log;
137  T_eq_sz( log->header.recorded, 2 );
138  T_eq_u32( log->events[ 0 ].heir, ctx->runner_id );
139  T_eq_u32( log->events[ 1 ].heir, ctx->worker_id );
140
141CheckNoPreemption: |
142  log = &ctx->thread_switch_log;
143  T_le_sz( log->header.recorded, 1 );
144  for ( size_t i = 0; i < log->header.recorded; ++i ) {
145    T_ne_u32( log->events[ i ].executing, ctx->worker_id );
146    T_eq_u32( log->events[ i ].heir, ctx->runner_id );
147  }
148
149RunnerScheduler: |
150  uint32_t processor = {};
151  rtems_status_code sc1;
152  rtems_id current_sched;
153  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
154  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
155  sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->runner_sched );
156  T_rsc_success( sc1 );
157  T_log( T_NORMAL, "runner scheduler id: %d", &ctx->runner_sched);
158  sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->runner_sched, RTEMS_CURRENT_PRIORITY);
159  T_rsc_success( sc1 );
160  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
161  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
162
163OtherScheduler: |
164  uint32_t processor = {};
165  rtems_status_code sc1;
166  rtems_id current_sched;
167  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
168  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
169  sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->other_sched );
170  T_rsc_success( sc1 );
171  T_log( T_NORMAL, "other scheduler id: %d", &ctx->other_sched);
172  sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->other_sched, RTEMS_CURRENT_PRIORITY);
173  T_rsc_success( sc1 );
174  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
175  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
176
177SetProcessor: |
178  T_ge_u32( rtems_scheduler_get_processor_maximum(), 2 );
179  uint32_t processor = {};
180  cpu_set_t cpuset;
181  CPU_ZERO(&cpuset);
182  CPU_SET(processor, &cpuset);
Note: See TracBrowser for help on using the repository browser.