source: rtems-central/formal/promela/models/barriers/tr-barrier-mgr-model.c @ 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: 6.0 KB
Line 
1/* SPDX-License-Identifier: BSD-2-Clause */
2
3/**
4 * @file
5 *
6 * @ingroup RTEMSTestCaseRtemsModelBarrierMgr
7 */
8
9/*
10 * Copyright (C) 2020-2022 embedded brains GmbH (http://www.embedded-brains.de)
11 *                         Trinity College Dublin (http://www.tcd.ie)
12 *
13 * Redistribution and use in source and binary forms, with or without
14 * modification, are permitted provided that the following conditions
15 * are met:
16 * 1. Redistributions of source code must retain the above copyright
17 *    notice, this list of conditions and the following disclaimer.
18 * 2. Redistributions in binary form must reproduce the above copyright
19 *    notice, this list of conditions and the following disclaimer in the
20 *    documentation and/or other materials provided with the distribution.
21 *
22 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
23 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
24 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
25 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
26 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
27 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
28 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
29 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
30 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
31 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
32 * POSSIBILITY OF SUCH DAMAGE.
33 */
34
35/*
36 * This file was automatically generated.  Do not edit it manually.
37 * Please have a look at
38 *
39 * https://docs.rtems.org/branches/master/eng/req/howto.html
40 *
41 * for information how to maintain and re-generate this file.
42 */
43
44#ifdef HAVE_CONFIG_H
45#include "config.h"
46#endif
47
48#include <rtems/score/threadimpl.h>
49
50#include "tr-barrier-mgr-model.h"
51#include "tx-support.h"
52
53static const char PromelaModelBarrierMgr[] = "/PML-BarrierMgr";
54
55rtems_id CreateSema( char * name )
56{
57  rtems_status_code sc;
58  rtems_id id;
59
60  sc = rtems_semaphore_create(
61    rtems_build_name( name[ 0 ], name[ 1 ], name[ 2 ], name[ 3 ] ),
62    0,
63    RTEMS_SIMPLE_BINARY_SEMAPHORE,
64    0,
65    &id
66  );
67  T_assert_rsc_success( sc );
68
69  return id;
70}
71
72void DeleteSema( rtems_id id )
73{
74  if ( id != 0 ) {
75    rtems_status_code sc;
76
77    sc = rtems_semaphore_delete( id );
78    T_rsc_success( sc );
79  }
80}
81
82void ObtainSema( rtems_id id )
83{
84  rtems_status_code sc;
85  sc = rtems_semaphore_obtain( id, RTEMS_WAIT, RTEMS_NO_TIMEOUT );
86  T_quiet_rsc_success( sc );
87}
88
89void ReleaseSema( rtems_id id )
90{
91  rtems_status_code sc;
92
93  sc = rtems_semaphore_release( id );
94  T_quiet_rsc_success( sc );
95}
96
97// rtems_task_priority SetPriority( rtems_id id, rtems_task_priority priority )
98// {
99//   rtems_status_code   sc;
100//   rtems_task_priority previous;
101//
102//   sc = rtems_task_set_priority( id, priority, &previous );
103//   T_rsc_success( sc );
104//
105//   return previous;
106// }
107
108// rtems_task_priority SetSelfPriority( rtems_task_priority priority )
109// {
110//   return SetPriority( RTEMS_SELF, priority );
111// }
112
113// rtems_id DoCreateTask( rtems_name name, rtems_task_priority priority )
114// {
115//   rtems_status_code sc;
116//   rtems_id          id;
117//
118//   sc = rtems_task_create(
119//     name,
120//     priority,
121//     RTEMS_MINIMUM_STACK_SIZE,
122//     RTEMS_DEFAULT_MODES,
123//     RTEMS_DEFAULT_ATTRIBUTES,
124//     &id
125//   );
126//   T_assert_rsc_success( sc );
127//
128//   return id;
129// }
130
131// void StartTask( rtems_id id, rtems_task_entry entry, void *arg )
132// {
133//   rtems_status_code sc;
134//
135//   sc = rtems_task_start( id, entry, (rtems_task_argument) arg);
136//   T_assert_rsc_success( sc );
137// }
138
139// void DeleteTask( rtems_id id )
140// {
141//   if ( id != 0 ) {
142//     rtems_status_code sc;
143//     T_printf( "L:Deleting Task id : %d\n", id );
144//     sc = rtems_task_delete( id );
145//     T_rsc_success( sc );
146//   }
147// }
148
149rtems_attribute mergeattribs( bool automatic )
150{
151  rtems_attribute attribs;
152
153  if ( automatic ) { attribs = RTEMS_BARRIER_AUTOMATIC_RELEASE; }
154  else { attribs = RTEMS_BARRIER_MANUAL_RELEASE; }
155
156  return attribs;
157}
158
159void checkTaskIs( rtems_id expected_id )
160{
161  rtems_id own_id;
162
163  own_id = _Thread_Get_executing()->Object.id;
164  T_eq_u32( own_id, expected_id );
165}
166
167void initialise_semaphore( Context *ctx, rtems_id semaphore[] ) {
168  semaphore[0] = ctx->runner_sema;
169  semaphore[1] = ctx->worker0_sema;
170  semaphore[2] = ctx->worker1_sema;
171}
172
173void ShowSemaId( Context *ctx ) {
174  T_printf( "L:ctx->runner_sema = %d\n", ctx->runner_sema );
175  T_printf( "L:ctx->worker0_sema = %d\n", ctx->worker0_sema );
176  T_printf( "L:ctx->worker1_sema = %d\n", ctx->worker1_sema );
177}
178
179void initialise_id ( rtems_id * id ) {
180  *id = 0;
181}
182
183void RtemsModelBarrierMgr_Teardown( void *arg )
184{
185  RtemsModelBarrierMgr_Context *ctx;
186
187  ctx = arg;
188
189  rtems_status_code   sc;
190  rtems_task_priority prio;
191
192  T_log( T_NORMAL, "Teardown" );
193
194  prio = 0;
195  sc = rtems_task_set_priority( RTEMS_SELF, BM_PRIO_HIGH, &prio );
196  T_rsc_success( sc );
197  T_eq_u32( prio, BM_PRIO_NORMAL );
198
199  DeleteTask(ctx->worker0_id);
200  DeleteTask(ctx->worker1_id);
201
202  T_log( T_NORMAL, "Deleting Runner Semaphore" );
203  DeleteSema( ctx->runner_sema );
204  T_log( T_NORMAL, "Deleting Worker0 Semaphore" );
205  DeleteSema( ctx->worker0_sema );
206  T_log( T_NORMAL, "Deleting Worker1 Semaphore" );
207  DeleteSema( ctx->worker1_sema );
208}
209
210
211size_t RtemsModelBarrierMgr_Scope( void *arg, char *buf, size_t n )
212{
213  RtemsModelBarrierMgr_Context *ctx;
214  size_t m;
215  int p10;
216  int tnum ;
217  char digit;
218
219  ctx = arg;
220  p10 = POWER_OF_10;
221
222  m = T_str_copy(buf, PromelaModelBarrierMgr, n);
223  buf += m;
224  tnum = ctx->this_test_number;
225  while( p10 > 0 && m < n )
226  {
227    digit = (char) ( (int) '0' + tnum / p10 );
228    buf[0] = digit;
229    ++buf;
230    ++m;
231    tnum = tnum % p10;
232    p10 /= 10;
233  }
234  return m;
235}
236
237void RtemsModelBarrierMgr_Cleanup(
238  RtemsModelBarrierMgr_Context *ctx
239)
240{
241  rtems_status_code sc;
242
243  if (ctx->barrier_id != 0) {
244    sc = rtems_barrier_delete(ctx->barrier_id);
245    if ( sc != RTEMS_SUCCESSFUL ) {
246      T_quiet_rsc( sc, RTEMS_INVALID_ID );
247    }
248  }
249}
Note: See TracBrowser for help on using the repository browser.