--- formal/promela/models/barriers/README.md | 11 + formal/promela/models/barriers/STATUS.md | 95 ++ .../models/barriers/barrier-mgr-model-post.h | 44 + .../models/barriers/barrier-mgr-model-pre.h | 51 + .../models/barriers/barrier-mgr-model-rfn.yml | 169 +++ .../models/barriers/barrier-mgr-model-run.h | 91 ++ .../models/barriers/barrier-mgr-model.pml | 1158 +++++++++++++++++ .../models/barriers/tc-barrier-mgr-model.c | 180 +++ .../models/barriers/tr-barrier-mgr-model.c | 249 ++++ .../models/barriers/tr-barrier-mgr-model.h | 197 +++ 10 files changed, 2245 insertions(+) create mode 100644 formal/promela/models/barriers/README.md create mode 100644 formal/promela/models/barriers/STATUS.md create mode 100644 formal/promela/models/barriers/barrier-mgr-model-post.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model-pre.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model-rfn.yml create mode 100644 formal/promela/models/barriers/barrier-mgr-model-run.h create mode 100644 formal/promela/models/barriers/barrier-mgr-model.pml create mode 100644 formal/promela/models/barriers/tc-barrier-mgr-model.c create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.c create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.h
diff --git a/formal/promela/models/barriers/README.md b/formal/promela/models/barriers/README.md new file mode 100644 index 00000000..5ed32946 --- /dev/null +++ b/formal/promela/models/barriers/README.md @@ -0,0 +1,11 @@ +# Barrier Manager model + +Developer: Jerzy Jaśkuć + +SPIN/Promela based test generation framework for RTEMS Barrier Manager + +This directory contains all of the necessary files needed to perform test generation for [RTEMS](https://www.rtems.org/ "RTEMS Homepage") [Barrier Manager](https://docs.rtems.org/branches/master/c-user/barrier/background.html "Barrier Manager") using SPIN/Promela framework. + +It is a subset of the material available at [Jerzy Jaśkuć's project repository](https://github.com/EZCodes/SPIN-PromelaRTEMSTestGen). + +These files were produced as a part of his research work done in Trinity College Dublin in partial fulfilment of the requirements for the degree of MCS in Integrated Computer Science. diff --git a/formal/promela/models/barriers/STATUS.md b/formal/promela/models/barriers/STATUS.md new file mode 100644 index 00000000..5e8f52de --- /dev/null +++ b/formal/promela/models/barriers/STATUS.md @@ -0,0 +1,95 @@ +# BARRIER MANAGER status + +## 7th Nov 2022 COMPLETE + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: OK + +See `barriers/archive/20221107-131233` + +## 7th Nov 2022 DIAGNOSIS + +Test cases 12 and 13 fail because there is a misinterpretation of how the +maximum number of barriers is determined. The actual configuration is set statically +in `ts-config.h` to be 7, as `TEST_MAXIMUM_BARRIERS`. In `ts-default.h`, this is used to set the +value of `CONFIGURE_MAXIMUM_BARRIERS`. This is not easily changed. + +The current Promela model only allows 2 barriers. + +## 5th Nov 2022 TEST FAIL + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: No, 4 fail + +Log extract showing all four fails: + +``` +:0.19:0:WRK0/PML-BarrierMgr013:tr-barrier-mgr-model-13.c:185:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +E:RtemsModelBarrierMgr13:N:33:F:2:D:0.011053 + +F:0.21:0:WRK0/PML-BarrierMgr012:tr-barrier-mgr-model-12.c:203:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +E:RtemsModelBarrierMgr12:N:36:F:2:D:0.011254 +``` + +# 4th Nov 2022 TEST FAIL + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: OK +* Runs: OK +* All Tests Pass: No, 27 fail + +Log extract showing representative sample: + +``` +F:0.7:0:RUN/PML-BarrierMgr000:tr-barrier-mgr-model-9.c:332:1 == 4 +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr9:N:33:F:2:D:0.012084 + +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr8:N:36:F:1:D:0.012003 + +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr14:N:37:F:1:D:0.012264 + +F:0.19:0:WRK0/PML-BarrierMgr013:tr-barrier-mgr-model-13.c:185:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr13:N:33:F:3:D:0.011301 + +F:0.21:0:WRK0/PML-BarrierMgr012:tr-barrier-mgr-model-12.c:203:RTEMS_SUCCESSFUL == RTEMS_TOO_MANY +F:*:0:RUN:*:*:RTEMS barrier leak (1) +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr12:N:36:F:3:D:0.011563 + +F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4 +E:RtemsModelBarrierMgr0:N:36:F:1:D:0.009776 +Z:Model0:C:22:N:757:F:27:D:0.246403 +Y:ReportHash:SHA256:H_j2zroRO1RaYJR3cZx9Bn68EfP5EBnpXZej6By5tIU= +cpu 0 in error mode (tt = 0x80) + 12687650 00015ba0: 91d02000 ta 0x0 +``` +See `events/archive/20221103-170752` + +## 3rd Nov 2022 BUILD FAIL + +* Platform: Dell G5, Ubuntu 20.04.5 LTS +* Generated: OK +* Compiles: No + ``` + Build failed + -> task in 'testsuites/validation/ts-model-0.exe' failed with exit status 1 (run with -v to display more information) +``` +It's the `tx-support` issue. +* Runs: n/a +* All Tests Pass: n/a + +See `events/archive/20221103-171724` diff --git a/formal/promela/models/barriers/barrier-mgr-model-post.h b/formal/promela/models/barriers/barrier-mgr-model-post.h new file mode 100644 index 00000000..b1b02bc9 --- /dev/null +++ b/formal/promela/models/barriers/barrier-mgr-model-post.h @@ -0,0 +1,44 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +// Task 0 +static void Runner( RtemsModelBarrierMgr_Context *ctx ) +{ + T_log( T_NORMAL, "Runner(Task 0) running" ); + TestSegment3( ctx ); + T_log( T_NORMAL, "Runner(Task 0) finished" ); + + // Ensure we hold no semaphores + ReleaseSema( ctx->runner_sema ); + ReleaseSema( ctx->worker0_sema ); + ReleaseSema( ctx->worker1_sema ); +} + +// Task 1 +static void Worker0( rtems_task_argument arg ) +{ + Context *ctx; + ctx = (Context *) arg; + rtems_event_set events; + + T_log( T_NORMAL, "Worker0(Task 1) running" ); + TestSegment4( ctx ); + T_log( T_NORMAL, "Worker0(Task 1) finished" ); + + // Wait for events so that we don't terminate + rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events ); +} + +// Task 2 +static void Worker1( rtems_task_argument arg ) +{ + Context *ctx; + ctx = (Context *) arg; + rtems_event_set events; + + T_log( T_NORMAL, "Worker1(Task 2) running" ); + TestSegment5( ctx ); + T_log( T_NORMAL, "Worker1(Task 2) finished" ); + + // Wait for events so that we don't terminate + rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events ); +} \ No newline at end of file diff --git a/formal/promela/models/barriers/barrier-mgr-model-pre.h b/formal/promela/models/barriers/barrier-mgr-model-pre.h new file mode 100644 index 00000000..7c176bfb --- /dev/null +++ b/formal/promela/models/barriers/barrier-mgr-model-pre.h @@ -0,0 +1,51 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * @file + * + * @ingroup RTEMSTestCaseRtemsModelBarrierMgr + */ + +/* + * Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de) + * Trinity College Dublin (http://www.tcd.ie) + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +/* + * This file was automatically generated. Do not edit it manually. + * Please have a look at + * + * https://docs.rtems.org/branches/master/eng/req/howto.html + * + * for information how to maintain and re-generate this file. + */ + +#ifndef HAVE_CONFIG_H +#include "config.h" +#endif + +#include <rtems/score/threadimpl.h> + + +#include "tr-barrier-mgr-model.h" diff --git a/formal/promela/models/barriers/barrier-mgr-model-rfn.yml b/formal/promela/models/barriers/barrier-mgr-model-rfn.yml new file mode 100644 index 00000000..34bb4d74 --- /dev/null +++ b/formal/promela/models/barriers/barrier-mgr-model-rfn.yml @@ -0,0 +1,169 @@ +# SPDX-License-Identifier: BSD-2-Clause +# Barrier Manager: Promela to RTEMS Refinement + +# Copyright (C) 2019-2022 Trinity College Dublin (www.tcd.ie) +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +# ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE +# LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +# CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +# SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +# CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +# ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +# POSSIBILITY OF SUCH DAMAGE. +LANGUAGE: C + +SEGNAMEPFX: TestSegment{} # segnumber + + +NAME: | + /* Test Name is defined in the Test Case code (tc-model-barrier-mgr.c) */ + +semaphore_DCL: rtems_id {0}[{1}]; + +INIT: | + initialise_semaphore( ctx, semaphore ); + +Runner: | + checkTaskIs( ctx->runner_id ); + +Worker0: | + checkTaskIs( ctx->worker0_id ); + +Worker1: | + checkTaskIs( ctx->worker1_id ); + +SIGNAL: | + ReleaseSema( semaphore[{}] ); + +WAIT: | + ObtainSema( semaphore[{}] ); + +barrier_create: | + T_log(T_NORMAL, "Calling BarrierCreate(%d,%d,%d,%d)", {0}, {1}, {2}, {3} ); + rtems_id bid; + initialise_id(&bid); + rtems_status_code rc; + rtems_attribute attribs; + attribs = mergeattribs({1}); + rc = rtems_barrier_create({0}, attribs, {2}, {3} ? &bid : NULL); + T_log(T_NORMAL, "Returned 0x%x from Create", rc ); + +barrier_ident: | + T_log(T_NORMAL, "Calling BarrierIdent(%d,%d)", {0}, {1} ); + rtems_id bid; + initialise_id(&bid); + rtems_status_code rc; + rc = rtems_barrier_ident({0} , {1} ? &bid : NULL); + T_log(T_NORMAL, "Returned 0x%x from Ident", rc ); + +barrier_wait: | + rtems_interval timeout = {1}; + T_log(T_NORMAL, "Calling BarrierWait(%d,%d)", bid, timeout ); + rc = rtems_barrier_wait(bid, timeout); + T_log(T_NORMAL, "Returned 0x%x from Wait", rc ); + +barrier_delete: | + T_log(T_NORMAL, "Calling BarrierDelete(%d)", bid); + rc = rtems_barrier_delete(bid); + T_log(T_NORMAL, "Returned 0x%x from Delete", rc ); + +barrier_release: | + T_log(T_NORMAL, "Calling BarrierRelease(%d,%d)", bid, {1}); + uint32_t released; + rc = rtems_barrier_release(bid, {1} ? &released : NULL); + T_log(T_NORMAL, "Returned 0x%x from Release", rc ); + +rc: + T_rsc( rc, {0} ); + +released: + T_eq_u32( released, {0} ); + +created: + /* This is used later for cleanup */ + ctx->barrier_id = bid; + +Ready: | + /* We (Task {0}) must have been recently ready because we are running */ + +Zombie: + /* Code to check that Task {0} has terminated */ + +BarrierWait: + /* Code to check that Task {0} is waiting on the barrier */ + +TimeWait: + /* Code to check that Task {0} is waiting on a timer */ + +OtherWait: + /* Code to check that Task {0} is waiting (after pre-emption) */ + +SUSPEND: + /* SWITCH[{0}] Suspension of proc{1} in favour of proc{2} */ + +WAKEUP: + /* SWITCH[{0}] Wakeup of proc{1} (sometime) after proc{2} */ + +LowPriority: | + SetSelfPriority( BM_PRIO_LOW ); + rtems_task_priority prio; + rtems_status_code sc; + sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio ); + T_rsc_success( sc ); + T_eq_u32( prio, BM_PRIO_LOW ); + +NormalPriority: | + SetSelfPriority( BM_PRIO_NORMAL ); + rtems_task_priority prio; + rtems_status_code sc; + sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio ); + T_rsc_success( sc ); + T_eq_u32( prio, BM_PRIO_NORMAL ); + +HighPriority: | + SetSelfPriority( BM_PRIO_HIGH ); + rtems_task_priority prio; + rtems_status_code sc; + sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio ); + T_rsc_success( sc ); + T_eq_u32( prio, BM_PRIO_HIGH ); + +StartLog: | + T_thread_switch_log *log; + log = T_thread_switch_record_4( &ctx->thread_switch_log ); + +CheckPreemption: | + log = &ctx->thread_switch_log; + T_eq_sz( log->header.recorded, 2 ); + T_eq_u32( log->events[ 0 ].heir, ctx->runner_id ); + T_eq_u32( log->events[ 1 ].heir, ctx->worker_id ); + +CheckNoPreemption: | + log = &ctx->thread_switch_log; + T_le_sz( log->header.recorded, 1 ); + for ( size_t i = 0; i < log->header.recorded; ++i ) { + T_ne_u32( log->events[ i ].executing, ctx->worker_id ); + T_eq_u32( log->events[ i ].heir, ctx->runner_id ); + } + +SetProcessor: | + #if defined(RTEMS_SMP) + T_eq_u32( rtems_scheduler_get_processor_maximum(), 4 ); + uint32_t processor = {}; + cpu_set_t cpuset; + CPU_ZERO(&cpuset); + CPU_SET(processor, &cpuset); + #endif diff --git a/formal/promela/models/barriers/barrier-mgr-model-run.h b/formal/promela/models/barriers/barrier-mgr-model-run.h new file mode 100644 index 00000000..03a498bd --- /dev/null +++ b/formal/promela/models/barriers/barrier-mgr-model-run.h @@ -0,0 +1,91 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +static void RtemsModelBarrierMgr_Setup{0}( void *arg ) +{{ + RtemsModelBarrierMgr_Context *ctx; + ctx = arg; + + rtems_status_code sc; + rtems_task_priority prio; + + T_log( T_NORMAL, "Runner Setup" ); + memset( ctx, 0, sizeof( *ctx ) ); + ctx->runner_thread = _Thread_Get_executing(); + ctx->runner_id = ctx->runner_thread->Object.id; + + T_log( T_NORMAL, "Creating Runner Semaphore" ); + ctx->runner_sema = CreateSema("RUNR"); + + T_log( T_NORMAL, "Creating Worker0 Semaphore" ); + ctx->worker0_sema = CreateSema("WRS0"); + + T_log( T_NORMAL, "Creating Worker1 Semaphore" ); + ctx->worker1_sema = CreateSema("WRS1"); + + sc = rtems_task_get_scheduler( RTEMS_SELF, &ctx->runner_sched ); + T_rsc_success( sc ); + + #if defined(RTEMS_SMP) + sc = rtems_scheduler_ident_by_processor( 1, &ctx->other_sched ); + T_rsc_success( sc ); + T_ne_u32( ctx->runner_sched, ctx->other_sched ); + #endif + + prio = 0; + sc = rtems_task_set_priority( RTEMS_SELF, BM_PRIO_NORMAL, &prio ); + T_rsc_success( sc ); + T_eq_u32( prio, BM_PRIO_HIGH ); + + ctx->worker0_id = CreateTask( "WRK0", BM_PRIO_NORMAL ); + T_log( T_NORMAL, "Created Worker 0"); + StartTask( ctx->worker0_id, Worker0, ctx ); + T_log( T_NORMAL, "Started Worker 0"); + + ctx->worker1_id = CreateTask( "WRK1", BM_PRIO_NORMAL ); + T_log( T_NORMAL, "Created Worker 1"); + StartTask( ctx->worker1_id, Worker1, ctx ); + T_log( T_NORMAL, "Started Worker 1"); +}} + +static RtemsModelBarrierMgr_Context RtemsModelBarrierMgr_Instance{0}; + +static T_fixture RtemsModelBarrierMgr_Fixture{0} = {{ + .setup = RtemsModelBarrierMgr_Setup{0}, + .stop = NULL, + .teardown = RtemsModelBarrierMgr_Teardown, + .scope = RtemsModelBarrierMgr_Scope, + .initial_context = &RtemsModelBarrierMgr_Instance{0} +}}; + +static T_fixture_node RtemsModelBarrierMgr_Node{0}; + +void RtemsModelBarrierMgr_Run{0}() +{{ + RtemsModelBarrierMgr_Context *ctx; + + T_set_verbosity( T_NORMAL ); + T_log( T_NORMAL, "Pushing Test Fixture..." ); + + ctx = T_push_fixture( + &RtemsModelBarrierMgr_Node{0}, + &RtemsModelBarrierMgr_Fixture{0} + ); + // This runs RtemsModelBarrierMgr_Fixture + T_log( T_NORMAL, "Test Fixture Pushed" ); + + ctx->this_test_number = {0}; + + memset( &ctx->thread_switch_log, 0, sizeof( ctx->thread_switch_log ) ); + _Thread_Wait_flags_set( ctx->runner_thread, THREAD_WAIT_CLASS_PERIOD ); + + TestSegment0( ctx ); + + Runner( ctx ); + + RtemsModelBarrierMgr_Cleanup( ctx ); + + T_log( T_NORMAL, "Run Pop Fixture" ); + T_pop_fixture(); +}} + +/** @}} */ diff --git a/formal/promela/models/barriers/barrier-mgr-model.pml b/formal/promela/models/barriers/barrier-mgr-model.pml new file mode 100644 index 00000000..85c2aef8 --- /dev/null +++ b/formal/promela/models/barriers/barrier-mgr-model.pml @@ -0,0 +1,1158 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/* + * barrier-mgr-model.pml + * + * Copyright (C) 2022 Trinity College Dublin (www.tcd.ie) + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above + * copyright notice, this list of conditions and the following + * disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * * Neither the name of the copyright holders nor the names of its + * contributors may be used to endorse or promote products derived + * from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/* + * The model presented here is designed to work with the following files: + * Refinement: barrier-events-mgr-rfn.yml + * Test Preamble: barrier-events-mgr-pre.h + * Test Postamble: barrier-events-mgr-post.h + * Test Runner: barrier-events-mgr-run.h + */ + +/* + * We need to output annotations for any #define we use. + * It is simplest to keep them all together, + * and use an inline to output them. + */ + +// Barriers - we will test Automatic and Manual Barriers +#define MAX_BARRIERS 2 // Max amount of barriers available to be created + // 0 reserved for NULL pointers +// Barrier Configurations +#define BARRIER_MAN 0 +#define BARRIER_AUTO 1 +#define MAX_WAITERS 3 +#define NO_TIMEOUT 0 + +// We envisage three RTEMS tasks involved. +#define TASK_MAX 4 // These are the "RTEMS" tasks only, numbered 1, 2 & 3 + // We reserve 0 to model NULL pointers + +// We use semaphores to synchronise the tasks +#define SEMA_MAX 3 + +// Return Values +// Defined in cpukit/include/rtems/rtems/status.h +#define RC_OK 0 // RTEMS_SUCCESSFUL +#define RC_InvName 3 // RTEMS_INVALID_NAME +#define RC_InvId 4 // RTEMS_INVALID_ID +#define RC_TooMany 5 // RTEMS_TOO_MANY +#define RC_Timeout 6 // RTEMS_TIMEOUT +#define RC_Deleted 7 // RTEMS_OBJECT_WAS_DELETED +#define RC_InvAddr 9 // RTEMS_INVALID_ADDRESS +#define RC_InvNum 10 // RTEMS_INVALID_NUMBER + +// Output configuration +inline outputDefines () { + printf("@@@ %d DEF MAX_BARRIERS %d\n",_pid,MAX_BARRIERS); + printf("@@@ %d DEF BARRIER_MAN %d\n",_pid,BARRIER_MAN); + printf("@@@ %d DEF BARRIER_AUTO %d\n",_pid,BARRIER_AUTO); + printf("@@@ %d DEF MAX_WAITERS %d\n",_pid,MAX_WAITERS); + printf("@@@ %d DEF TASK_MAX %d\n",_pid,TASK_MAX); + printf("@@@ %d DEF SEMA_MAX %d\n",_pid,SEMA_MAX); +} + +// Special values: task states, options, return codes +mtype = { + // Task states, BarrierWait is same as TimeWait but with no timeout + Zombie, Ready, BarrierWait, TimeWait, OtherWait, +}; + +// Tasks +typedef Task { + byte nodeid; // So we can spot remote calls + byte pmlid; // Promela process id + mtype state ; // {Ready,BarrierWait,TimeWait,OtherWait} + bool preemptable; + byte prio; // lower number is higher priority + int ticks; // clock ticks to keep track of timeout + bool tout; // true if woken by a timeout +}; + +// Barriers +typedef Barrier { + byte b_name; // barrier name + bool isAutomatic; // true for automatic, false for manual barrier + int maxWaiters; // maximum count of waiters for automatic barrier + int waiterCount; // current amount of tasks waiting on the barrier + bool waiters[TASK_MAX]; // waiters on the barrier + bool isInitialised; // indicated whenever this barrier was created +} + +Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference +Barrier barriers[MAX_BARRIERS]; // barriers[0] models a NULL dereference + +/* + * Running Orders (maintained by simple global sync counter): + * Create;;Ident = Barrier Identified only after creating + * Acquire;;Release = Manual barrier is acquired and then released + * Acquire;;Delete = Manual barrier is acquired and then deleted + * Here ;; is "sequential" composition of *different* threads. + * Additionally task 1 will always create a barrier before operations + */ +bool semaphore[SEMA_MAX]; // Semaphore + +inline outputDeclarations () { + printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid); +} + +/* + * Synchronisation Mechanisms + * + * Obtained(sem_id) - call that waits if semaphore + * `sem_id` is aquired by someone. + * Obtain(sem_id) - obttains semaphore `sem_id` + * Release(sem_id) - call that releases semaphore `sem_id` + * + * Binary semaphores: True means available, False means in use. + */ + +inline Obtain(sem_id){ + atomic{ + printf("@@@ %d WAIT %d\n",_pid,sem_id); + semaphore[sem_id] ; // wait until available + semaphore[sem_id] = false; // set as in use + printf("@@@ %d LOG WAIT %d Over\n",_pid,sem_id); + } +} + +inline Release(sem_id){ + atomic{ + printf("@@@ %d SIGNAL %d\n",_pid,sem_id); + semaphore[sem_id] = true ; // release + } +} + +/* The following inlines are not given here as atomic, + * but are intended to be used in an atomic context. +*/ + +inline nl() { printf("\n") } // Useful shorthand + +/* + * waitUntilReady(id) logs that task[id] is waiting, + * and then attempts to execute a statement that blocks, + * until some other process changes task[id]'s state to Ready. + * It relies on the fact that if a statement blocks inside an atomic block, + * the block loses its atomic behaviour and yields to other Promela processes + * + * It is used to model a task that has been suspended for any reason. + */ +inline waitUntilReady(id){ + atomic{ + printf("@@@ %d LOG Task %d waiting, state = ",_pid,id); + printm(tasks[id].state); nl() + } + tasks[id].state == Ready; // breaks out of atomics if false + printf("@@@ %d STATE %d Ready\n",_pid,id) +} + +/* + * satisfied(bid, sat) checks if a barrier reached enough + * waiters to be released. Relevant only for automatic barriers. + */ +inline satisfied(bid,sat) { + if + :: barriers[bid].waiterCount >= barriers[bid].maxWaiters -> + printf("@@@ %d LOG Auto Barrier satisfied(<bid:%d wt:%d max:%d>)\n", + _pid,bid,barriers[bid].waiterCount,barriers[bid].maxWaiters); + sat = true + :: else -> sat = false + fi +} + +/* + * preemptIfRequired(callerid) is executed, + * when the tasks waiting on the barrier are released. + * + * It checks if task[callerid] should be preempted, and makes it so. + * This is achieved here by setting the calling task state to OtherWait. + * Task goes over all of the released processes and chooses one with + * highest priority. + */ +inline preemptIfRequired(callerid) { + int t_index = 1; + do + :: t_index < TASK_MAX && t_index != callerid -> + if + :: tasks[callerid].preemptable && + // we use the (usual?) convention that higher priority is a lower + // number + tasks[t_index].prio < tasks[callerid].prio && + tasks[t_index].state == Ready + -> tasks[callerid].state = OtherWait; + printf("@@@ %d STATE %d OtherWait\n",_pid,callerid) + callerid = t_index; + :: (!tasks[callerid].preemptable || + tasks[t_index].prio > tasks[callerid].prio) && + tasks[t_index].state == Ready -> + tasks[t_index].state = OtherWait; + printf("@@@ %d STATE %d OtherWait\n",_pid,t_index) + :: else -> skip + fi + t_index++ + :: else -> break + od +} + +/* + * waitAtBarrier(tid, bid, rc) holds the task at the barrier. + * + * It utilises the same principle as the waitUntilReady to hold the task. + * However, here when the task is released it is checked why it was released. + * This allows to model us correct return codes, whenever the task was released + * due to barrier release, barrier deletion or timeout of the waiting task. + */ +inline waitAtBarrier(tid,bid,rc){ + atomic{ + printf("@@@ %d LOG Task %d waiting, state = ",_pid,tid); + printm(tasks[tid].state); nl() + } + tasks[tid].state == Ready; // breaks out of atomics if false + if + :: tasks[tid].tout -> + barriers[bid].waiters[tid] = false; // remove self from waiters + rc = RC_Timeout + tasks[tid].tout = false; // reset timeout in case we reaquire + barriers[bid].waiterCount--; + preemptIfRequired(tid); + waitUntilReady(tid) // if we were higher prio, need to pre-empt others + :: !barriers[bid].isInitialised -> + rc = RC_Deleted + :: else -> // normally released + rc = RC_OK + fi + printf("@@@ %d STATE %d Ready\n",_pid,tid) +} + +/* + * barrierRelease(self,bid) is executed, when the tasks waiting on the barrier + * are released. + * + * It can be invoked by release or delete directives in this model. + * + * It checks if calling task should be preempted, and makes it so. + */ +inline barrierRelease(self,bid) { + atomic{ + int tid = 1; + do + :: tid < TASK_MAX -> + if + :: barriers[bid].waiters[tid] -> + barriers[bid].waiters[tid] = false; + tasks[tid].state = Ready + :: else -> skip + fi + tid++ + :: else -> break + od + barriers[bid].waiterCount = 0; + preemptIfRequired(self); + waitUntilReady(self) // Of all the tasks released only one should have + // Ready state and the rest is in OtherWait State. + } +} + +/* + * barrier_create(name,attribs,max_waiters,id,rc) + * + * Simulates a call to rtems_barrier_create + * name : name of the barrier + * arrtibs : attribute set of the barrier + * max_waiters : (automatic only, optional) amount of max waiters + * on the barrier + * id : id of the barrier if created successfully + * rc : updated with the return code when directive completes + * + * Corresponding RTEMS call: + * rc = rtems_barrier_create(name,attribs,max_waiters,id); + * `name` models `rtems_name name` + * `attribs` models `rtems_attribute attribute_set` + * `max_waiters` models `uint32_t maximum_waiters` + * `id` models `rtems_event_set *id` + * + * This directive does not preempt the task, so it's relatively + * straightforward. + */ +inline barrier_create(name,attribs,max_waiters,id,rc) { + atomic{ + int new_bid = 1; + if + :: id == 0 -> rc = RC_InvAddr; + :: name <= 0 -> rc = RC_InvName; + :: else -> + do + :: new_bid < MAX_BARRIERS -> + if + :: !barriers[new_bid].isInitialised -> + if + :: attribs == BARRIER_AUTO -> + if + :: max_waiters > 0 -> + barriers[new_bid].maxWaiters = max_waiters; + :: else -> + rc = RC_InvNum; + break; + fi + barriers[new_bid].b_name = name; + barriers[new_bid].isAutomatic = + barriers[new_bid].isAutomatic | attribs; + barriers[new_bid].waiterCount = 0; + barriers[new_bid].isInitialised = true; + id = new_bid; + rc = RC_OK; + printf("@@@ %d LOG %d Created {n: %d, auto: true, mw: %d}\n" + ,_pid, new_bid, name, max_waiters); + break + :: else -> // attribs == BARRIER_MAN + barriers[new_bid].b_name = name; + barriers[new_bid].isAutomatic = + barriers[new_bid].isAutomatic | attribs; + barriers[new_bid].waiterCount = 0; + barriers[new_bid].isInitialised = true; + id = new_bid; + rc = RC_OK; + printf("@@@ %d LOG %d Created {n: %d, auto: false}\n" + ,_pid, new_bid, name); + break + fi + :: else /* barriers[id].isInitialised */ -> new_bid++; + fi + :: else -> // new_bid >= MAX_BARRIERS + rc = RC_TooMany; + break + od + fi + } +} + + +/* + * barrier_ident(name,id,rc) + * + * Simulates a call to rtems_barrier_ident + * name : name of the barrier + * id : id of the barrier if created successfully + * rc : updated with the return code when the directive completes + * + * Corresponding RTEMS call: + * rc = rtems_barrier_ident(name,id); + * `name` models `rtems_name name` + * `id` models `rtems_event_set *id` + * + * Here we assuming that the node where the barrier was created + * is searched. + */ +inline barrier_ident(name,id,rc) { + atomic{ + int b_index = 1; // 0 is NULL deref + if + :: id == 0 -> rc = RC_InvAddr; + :: name <= 0 -> + rc = RC_InvName; + id = 0; + :: else -> // name > 0 + do + :: b_index < MAX_BARRIERS -> + if + :: barriers[b_index ].isInitialised && + barriers[b_index ].b_name == name -> + id = b_index ; + printf("@@@ %d LOG Barrier %d Identified by name %d\n", + _pid, b_index, name); + rc = RC_OK; + break; + :: else -> /* !barriers[id].isInitialised || + barriers[b_index ].b_name!=name */ + b_index ++; + fi + :: else -> // b_index >= MAX_BARRIERS + rc = RC_InvName; + break; + od + fi + } +} + +/* + * barrier_wait(self,bid,interval,rc) + * + * Simulates a call to rtems_barrier_wait + * self : task id making the call + * bid : id of the barrier + * interval : wait time on the barrier (0 waits forever) + * rc : updated with the return code when the wait completes + * + * Corresponding RTEMS call: + * rc = rtems_barrier_wait(bid, interval; + * `bid` models `rtems_id id` + * `interval` models `rtems_interval timeout` + * + * This directive almost always blocks the calling taks, unless it + * releases automatic barrier and the task still has the priority. + * It's hard to model automatic release therefore in this model the + * task is calling for release of the barriers if it was going to be the + * waiter that triggers the release. + * + */ +inline barrier_wait(self,bid,interval,rc) { + atomic{ + if + :: bid >= MAX_BARRIERS || bid <= 0 || !barriers[bid].isInitialised -> + rc = RC_InvId + :: else -> // id is correct + barriers[bid].waiterCount++; + if + :: barriers[bid].isAutomatic -> + bool sat; + satisfied(bid, sat) // check if enough waiters to release barrier + if + :: sat -> + barrierRelease(self,bid); + rc = RC_OK + :: else -> // !sat + barriers[bid].waiters[self] = true; + if + :: interval > NO_TIMEOUT -> + tasks[self].tout = false; + tasks[self].ticks = interval; + tasks[self].state = TimeWait; + printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval); + :: else -> + tasks[self].state = BarrierWait; + printf("@@@ %d STATE %d BarrierWait\n",_pid,self) + fi + waitAtBarrier(self,bid,rc) + fi + :: else -> // !barriers[bid].isAutomatic + barriers[bid].waiters[self] = true; + if + :: interval > NO_TIMEOUT -> + tasks[self].tout = false; + tasks[self].ticks = interval; + tasks[self].state = TimeWait + printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval); + :: else -> + tasks[self].state = BarrierWait; + printf("@@@ %d STATE %d BarrierWait\n",_pid,self) + fi + waitAtBarrier(self,bid,rc) + fi + fi + } +} + +/* + * barrier_release(self,bid,nreleased,rc) + * + * Simulates a call to rtems_barrier_release + * self: if of the calling task + * bid : id of the barrier + * nrelease : contains number of released tasks if successful + * rc : updated with the return code when the directive completes + * + * Corresponding RTEMS call: + * rc = rtems_barrier_release(bid, nreleased); + * `bid` models `rtems_id id` + * `nreleased models `uint32_t` *released` + * + */ +inline barrier_release(self,bid,nreleased,rc) { + atomic{ + if + :: nreleased == 0 -> rc = RC_InvAddr; + :: bid >= MAX_BARRIERS || bid <= 0 || !barriers[bid].isInitialised -> + rc = RC_InvId + :: else -> + nreleased = barriers[bid].waiterCount; + barrierRelease(self,bid); + printf("@@@ %d LOG Barrier %d manually released\n", _pid, bid) + rc = RC_OK + fi + } +} + +/* + * barrier_delete(self,bid,rc) + * + * Simulates a call to rtems_barrier_delete + * bid : id of the barrier + * rc : updated with the return code when the directive completes + * + * Corresponding RTEMS call: + * rc = rtems_barrier_delete(bid); + * `bid` models `rtems_id id` + * + * All tasks waiting on deleted barrier are released + */ +inline barrier_delete(self,bid,rc) { + atomic{ + if + :: bid >= MAX_BARRIERS || bid <= 0 || !barriers[bid].isInitialised -> + rc = RC_InvId + :: else -> + barriers[bid].isInitialised = false; + barrierRelease(self,bid); + printf("@@@ %d LOG Barrier %d deleted\n", _pid, bid) + rc = RC_OK + fi + } +} + +/* + * Model Processes + * We shall use five processes in this model. + * Three will represent the RTEMS tasks that will make use of the + * barrier directives. + * One will model a timer. + * One will model scheduling and other task management behaviour. + */ + +// These are not output to test generation +#define TASK1_ID 1 +#define TASK2_ID 2 +#define TASK3_ID 3 +#define BARRIER1_NAME 1 +#define BARRIER2_NAME 2 +// In SMP setting there are different cores, but all are settled on same node. +#define THIS_CORE 0 +#define THAT_CORE 1 + +/* + * Scenario Generation + */ + + /* + * Task variants: + * Task objectives - Barrier {Create, Acquire, Release, Delete} + * timeout_length in {0,1,2...} + * + * Task Scenarios: + * vary: priority, preemptable, timeout interval, barrier options + */ +typedef TaskInputs { + bool doCreate; // will task create a barrier + bool isAutomatic; // if doCreate is true, specifies barrier type + int maxWaiters; // if isAutomatic is true, specifies max barrier waiters + byte bName; // Name of barrier to create or identify + bool doAcquire; // will task aquire the barrier + byte timeoutLength; // only relevant if doAcquire is true, gives wait time + bool doDelete; // will task delete the barrier + bool doRelease; // will task release the barrier + + byte taskPrio; + bool taskPreempt; + + bool idNull; // indicates whenever passed id is null + bool releasedNull // indicates whenever nreleased param is null +}; +TaskInputs task_in[TASK_MAX]; + + /* + * Convenience function that assigns default options to a given `TaskInputs` + * structure. + */ +inline assignDefaults(defaults, opts) { + opts.doCreate = defaults.doCreate; + opts.isAutomatic = defaults.isAutomatic; + opts.maxWaiters = defaults.maxWaiters; + opts.doAcquire = defaults.doAcquire; + opts.timeoutLength = defaults.timeoutLength; + opts.doRelease = defaults.doRelease; + opts.doDelete = defaults.doDelete; + opts.taskPrio = defaults.taskPrio; + opts.taskPreempt = defaults.taskPreempt; + opts.bName = defaults.bName; + opts.idNull = defaults.idNull; + opts.releasedNull = defaults.releasedNull; +} + +/* + * Semaphore Setup + */ +int task1Sema +int task2Sema; +int task3Sema; + +/* + * Multicore setup + */ +bool multicore; +int task1Core; +int task2Core; +int task3Core; + +/* + * Generating Scenarios + * + * We consider the following broad scenario classes: + * + * Manual Barrier - Check for barrier creation and manual release with delete + * Automatic Barrier - Check for barrier creation and automatic release + * Acquire ; Timeout ; Delete - check correct timeout and delete behaviour + * + */ +mtype = {ManAcqRel,AutoAcq,AutoToutDel}; +mtype scenario; + +inline chooseScenario() { + // Common Defaults + TaskInputs defaults; + defaults.doCreate = false; + defaults.isAutomatic = false; + defaults.maxWaiters = 0; + defaults.doAcquire = true; + defaults.timeoutLength = NO_TIMEOUT; + defaults.doRelease= false; + defaults.doDelete = false; + defaults.taskPrio = 2; + defaults.taskPreempt = false; + defaults.idNull = false; + defaults.releasedNull = false; + defaults.bName = BARRIER1_NAME; + // Set the defaults + assignDefaults(defaults, task_in[TASK1_ID]); + task_in[TASK1_ID].doCreate = true; // Task 1 is always the creator + assignDefaults(defaults, task_in[TASK2_ID]); + assignDefaults(defaults, task_in[TASK3_ID]); + + // Semaphore initialization + semaphore[0] = false; + task1Sema = 0; + semaphore[1] = false; + task2Sema = 1; + semaphore[2] = false; + task3Sema = 2; + + tasks[TASK1_ID].state = Ready; + tasks[TASK2_ID].state = Ready; + tasks[TASK3_ID].state = Ready; + + multicore = false; + task1Core = THIS_CORE; + task2Core = THIS_CORE; + task3Core = THIS_CORE; + + if + :: scenario = ManAcqRel; + :: scenario = AutoAcq; + :: scenario = AutoToutDel; + fi + atomic{printf("@@@ %d LOG scenario ",_pid); printm(scenario); nl()} ; + + if + :: scenario == ManAcqRel -> + task_in[TASK1_ID].doAcquire = false; + task_in[TASK1_ID].doRelease = true; + task_in[TASK1_ID].doDelete = true; + if + :: task_in[TASK1_ID].bName = 0; + printf( "@@@ %d LOG sub-senario bad create, invalid name\n", _pid); + :: task_in[TASK1_ID].idNull = true; + printf( "@@@ %d LOG sub-senario bad create, passed id null\n", + _pid); + :: task_in[TASK2_ID].doAcquire = false; + task_in[TASK3_ID].doAcquire = false; + printf( "@@@ %d LOG sub-senario barrier not acquired\n", _pid); + :: task_in[TASK2_ID].bName = 0; + printf( "@@@ %d LOG sub-senario Worker0 ident barrier name is 0\n", + _pid); + :: task_in[TASK1_ID].releasedNull = true; + printf( "@@@ %d LOG sub-senario realesed passed is null\n", _pid); + :: task_in[TASK2_ID].idNull = true; + printf( "@@@ %d LOG sub-senario Worker0 ident passed id null\n", + _pid); + /* :: task_in[TASK2_ID].doAcquire = false; + task_in[TASK2_ID].doCreate = true; + task_in[TASK2_ID].bName = BARRIER2_NAME; + printf( "@@@ %d LOG sub-senario TooMany barriers created\n", _pid); */ + :: skip + fi + :: scenario == AutoAcq -> + task_in[TASK1_ID].isAutomatic = true; + task_in[TASK1_ID].maxWaiters = MAX_WAITERS; + if + :: task_in[TASK1_ID].maxWaiters = 0; + printf( "@@@ %d LOG sub-senario bad create, max_waiters is 0\n", + _pid); + :: skip + fi + :: scenario == AutoToutDel -> + task_in[TASK1_ID].doAcquire = false; + task_in[TASK1_ID].isAutomatic = true; + task_in[TASK1_ID].maxWaiters = MAX_WAITERS; + task_in[TASK3_ID].timeoutLength = 4; + task_in[TASK3_ID].doDelete = true; + fi + + // Multicore subscenario + if + :: multicore = true; + // Its enough for the main creator task to be on another core to test + // everything + task1Core = THAT_CORE; + printf( "@@@ %d LOG sub-senario multicore enabled, cores:(%d,%d,%d)\n", + _pid, task1Core, task2Core, task3Core ); + :: skip + fi +} + +proctype Runner (byte nid, taskid; TaskInputs opts) { + tasks[taskid].nodeid = nid; + tasks[taskid].pmlid = _pid; + tasks[taskid].prio = opts.taskPrio; + + printf("@@@ %d TASK Runner\n",_pid); + if + :: tasks[taskid].prio == 1 -> printf("@@@ %d CALL HighPriority\n", _pid); + :: tasks[taskid].prio == 2 -> printf("@@@ %d CALL NormalPriority\n", _pid); + :: tasks[taskid].prio == 3 -> printf("@@@ %d CALL LowPriority\n", _pid); + fi + // Preemption check setup, uncomment if necessary + //printf("@@@ %d CALL StartLog\n",_pid); + byte rc; + byte bid; + if + :: opts.idNull -> bid = 0; + :: else -> bid = 1; + fi + + if + :: multicore -> + printf("@@@ %d CALL SetProcessor %d\n", _pid, tasks[taskid].nodeid); + :: else -> skip + fi + + if + :: opts.doCreate -> + printf("@@@ %d CALL barrier_create %d %d %d %d\n" + ,_pid, opts.bName, opts.isAutomatic, opts.maxWaiters, bid); + /* (name, attribs, max_waiters, id, rc) */ + barrier_create(opts.bName, opts.isAutomatic, opts.maxWaiters, bid, rc); + if + :: rc == RC_OK -> + printf("@@@ %d SCALAR created %d\n", _pid, bid); + :: else -> skip; + fi + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> + printf("@@@ %d CALL barrier_ident %d %d\n", _pid, opts.bName, bid); + /* (name, id, rc) */ + barrier_ident(opts.bName,bid,rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + fi + Release(task2Sema); + + if + :: opts.doAcquire -> + printf("@@@ %d CALL barrier_wait %d %d\n", + _pid, bid, opts.timeoutLength); + /* (self, bid, timeout, rc) */ + barrier_wait(taskid, bid, opts.timeoutLength, rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> skip + fi + + if + :: opts.doRelease -> + Obtain(task1Sema); + int nreleased; + if + :: opts.releasedNull -> nreleased = 0; + :: else -> nreleased = 1; + fi + int toRelease = barriers[bid].waiterCount; + printf("@@@ %d CALL barrier_release %d %d\n", _pid, bid, nreleased); + /* (self, bid, nreleased, rc) */ + barrier_release(taskid, bid, nreleased, rc); + if + :: rc == RC_OK -> + printf("@@@ %d SCALAR released %d\n", _pid, toRelease); + :: else -> skip; + fi + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + Release(task1Sema); + :: else -> skip + fi + + if + :: opts.doDelete -> + Obtain(task1Sema); + printf("@@@ %d CALL barrier_delete %d\n",_pid, bid); + /* (self, bid, rc) */ + barrier_delete(taskid, bid, rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + Release(task1Sema); + :: else -> skip + fi + + // Make sure everyone ran + Obtain(task1Sema); + // Wait for other tasks to finish + Obtain(task2Sema); + Obtain(task3Sema); + + printf("@@@ %d LOG Task %d finished\n",_pid,taskid); + tasks[taskid].state = Zombie; + printf("@@@ %d STATE %d Zombie\n",_pid,taskid) +} + +proctype Worker0 (byte nid, taskid; TaskInputs opts) { + tasks[taskid].nodeid = nid; + tasks[taskid].pmlid = _pid; + tasks[taskid].prio = opts.taskPrio; + + printf("@@@ %d TASK Worker0\n",_pid); + if + :: tasks[taskid].prio == 1 -> printf("@@@ %d CALL HighPriority\n", _pid); + :: tasks[taskid].prio == 2 -> printf("@@@ %d CALL NormalPriority\n", _pid); + :: tasks[taskid].prio == 3 -> printf("@@@ %d CALL LowPriority\n", _pid); + fi + // Preemption check setup, uncomment if necessary + //printf("@@@ %d CALL StartLog\n",_pid); + byte rc; + byte bid; + if + :: opts.idNull -> bid = 0; + :: else -> bid = 1; + fi + + if + :: multicore -> + printf("@@@ %d CALL SetProcessor %d\n", _pid, tasks[taskid].nodeid); + :: else -> skip + fi + + Obtain(task2Sema); + if + :: opts.doCreate -> + printf("@@@ %d CALL barrier_create %d %d %d %d\n" + ,_pid, opts.bName, opts.isAutomatic, opts.maxWaiters, bid); + /* (name, attribs, max_waiters, id, rc) */ + barrier_create(opts.bName, opts.isAutomatic, opts.maxWaiters, bid, rc); + if + :: rc == RC_OK -> + printf("@@@ %d SCALAR created %d\n", _pid, bid); + :: else -> skip; + fi + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> + printf("@@@ %d CALL barrier_ident %d %d\n", _pid, opts.bName, bid); + /* (name, id, rc) */ + barrier_ident(opts.bName,bid,rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + fi + + if + :: opts.doAcquire -> + atomic{ + Release(task3Sema); + printf("@@@ %d CALL barrier_wait %d %d\n", + _pid, bid, opts.timeoutLength); + /* (self, bid, timeout, rc) */ + barrier_wait(taskid, bid, opts.timeoutLength, rc); + } + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> Release(task3Sema); + fi + + if + :: opts.doRelease -> + int nreleased; + if + :: opts.releasedNull -> nreleased = 0; + :: else -> nreleased = 1; + fi + int toRelease = barriers[bid].waiterCount; + printf("@@@ %d CALL barrier_release %d %d\n", _pid, bid, nreleased); + /* (self, bid, nreleased, rc) */ + barrier_release(taskid, bid, nreleased, rc); + if + :: rc == RC_OK -> + printf("@@@ %d SCALAR released %d\n", _pid, toRelease); + :: else -> skip; + fi + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> skip + fi + + if + :: opts.doDelete -> + printf("@@@ %d CALL barrier_delete %d\n",_pid, bid); + /* (self, bid, rc) */ + barrier_delete(taskid, bid, rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> skip + fi + atomic{ + Release(task2Sema); + printf("@@@ %d LOG Task %d finished\n",_pid,taskid); + tasks[taskid].state = Zombie; + printf("@@@ %d STATE %d Zombie\n",_pid,taskid) + } +} + +proctype Worker1 (byte nid, taskid; TaskInputs opts) { + tasks[taskid].nodeid = nid; + tasks[taskid].pmlid = _pid; + tasks[taskid].prio = opts.taskPrio; + + printf("@@@ %d TASK Worker1\n",_pid); + if + :: tasks[taskid].prio == 1 -> printf("@@@ %d CALL HighPriority\n", _pid); + :: tasks[taskid].prio == 2 -> printf("@@@ %d CALL NormalPriority\n", _pid); + :: tasks[taskid].prio == 3 -> printf("@@@ %d CALL LowPriority\n", _pid); + fi + // Preemption check setup, uncomment if necessary + //printf("@@@ %d CALL StartLog\n",_pid); + byte rc; + byte bid; + if + :: opts.idNull -> bid = 0; + :: else -> bid = 1; + fi + + if + :: multicore -> + printf("@@@ %d CALL SetProcessor %d\n", _pid, tasks[taskid].nodeid); + :: else -> skip + fi + Obtain(task3Sema); + + if + :: opts.doCreate -> + printf("@@@ %d CALL barrier_create %d %d %d %d\n" + ,_pid, opts.bName, opts.isAutomatic, opts.maxWaiters, bid); + /* (name, attribs, max_waiters, id, rc) */ + barrier_create(opts.bName, opts.isAutomatic, opts.maxWaiters, bid, rc); + if + :: rc == RC_OK -> + printf("@@@ %d SCALAR created %d\n", _pid, bid); + :: else -> skip; + fi + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> + printf("@@@ %d CALL barrier_ident %d %d\n", _pid, opts.bName, bid); + /* (name, id, rc) */ + barrier_ident(opts.bName,bid,rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + fi + + if + :: opts.doAcquire -> + atomic{ + Release(task1Sema); + printf("@@@ %d CALL barrier_wait %d %d\n", + _pid, bid, opts.timeoutLength); + /* (self, bid, timeout, rc) */ + barrier_wait(taskid, bid, opts.timeoutLength, rc); + } + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> Release(task1Sema); + fi + + if + :: opts.doRelease -> + int nreleased; + if + :: opts.releasedNull -> nreleased = 0; + :: else -> nreleased = 1; + fi + int toRelease = barriers[bid].waiterCount; + printf("@@@ %d CALL barrier_release %d %d\n", _pid, bid, nreleased); + /* (self, bid, nreleased, rc) */ + barrier_release(taskid, bid, nreleased, rc); + if + :: rc == RC_OK -> + printf("@@@ %d SCALAR released %d\n", _pid, toRelease); + :: else -> skip; + fi + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> skip + fi + + if + :: opts.doDelete -> + printf("@@@ %d CALL barrier_delete %d\n",_pid, bid); + /* (self, bid, rc) */ + barrier_delete(taskid, bid, rc); + printf("@@@ %d SCALAR rc %d\n",_pid, rc); + :: else -> skip + fi + atomic { + Release(task3Sema); + printf("@@@ %d LOG Task %d finished\n",_pid,taskid); + tasks[taskid].state = Zombie; + printf("@@@ %d STATE %d Zombie\n",_pid,taskid) + } +} + +bool stopclock = false; + +/* + * We need a process that periodically wakes up blocked processes. + * This is modelling background behaviour of the system, + * such as ISRs and scheduling. + * We visit all tasks in round-robin order (to prevent starvation) + * and make them ready if waiting on "other" things. + * Tasks waiting for events or timeouts are not touched + * This terminates when all tasks are zombies. + */ +proctype System () { + byte taskid ; + bool liveSeen; + + printf("@@@ %d LOG System running...\n",_pid); + + loop: + taskid = 1; + liveSeen = false; + + printf("@@@ %d LOG Loop through tasks...\n",_pid); + atomic { + printf("@@@ %d LOG Scenario is ",_pid); + printm(scenario); nl(); + } + do // while taskid < TASK_MAX .... + :: taskid == TASK_MAX -> break; + :: else -> + atomic { + printf("@@@ %d LOG Task %d state is ",_pid,taskid); + printm(tasks[taskid].state); nl() + } + if + :: tasks[taskid].state == Zombie -> taskid++ + :: else -> + if + :: tasks[taskid].state == OtherWait + -> tasks[taskid].state = Ready + printf("@@@ %d LOG %d Ready\n",_pid,taskid) + :: else -> skip + fi + liveSeen = true; + taskid++ + fi + od + + printf("@@@ %d LOG ...all visited, live:%d\n",_pid,liveSeen); + + if + :: liveSeen -> goto loop + :: else + fi + printf("@@@ %d LOG All are Zombies, game over.\n",_pid); + stopclock = true; +} + + +/* + * We need a process that handles a clock tick, + * by decrementing the tick count for tasks waiting on a timeout. + * Such a task whose ticks become zero is then made Ready, + * and its timer status is flagged as a timeout + * This terminates when all tasks are zombies + * (as signalled by System via `stopclock`). + */ +proctype Clock () { + int tid, tix; + printf("@@@ %d LOG Clock Started\n",_pid) + do + :: stopclock -> goto stopped + :: !stopclock -> + printf(" (tick) \n"); + tid = 1; + do + :: tid == TASK_MAX -> break + :: else -> + atomic{ + printf("Clock: tid=%d, state=",tid); printm(tasks[tid].state); nl() + }; + if + :: tasks[tid].state == TimeWait -> + tix = tasks[tid].ticks - 1; + // printf("Clock: ticks=%d, tix=%d\n",tasks[tid].ticks,tix); + if + :: tix == 0 + tasks[tid].tout = true + tasks[tid].state = Ready + printf("@@@ %d LOG %d Ready\n",_pid,tid) + :: else + tasks[tid].ticks = tix + fi + :: else // state != TimeWait + fi + tid = tid + 1 + od + od +stopped: + printf("@@@ %d LOG Clock Stopped\n",_pid); +} + + +init { + pid nr; + + printf("Barrier Manager Model running.\n"); + printf("Setup...\n"); + + printf("@@@ %d LOG TestName: Barrier_Manager_TestGen\n",_pid) + outputDefines(); + outputDeclarations(); + + printf("@@@ %d INIT\n",_pid); + chooseScenario(); + + + printf("Run...\n"); + + run System(); + run Clock(); + + run Runner(task1Core,TASK1_ID,task_in[TASK1_ID]); + run Worker0(task2Core,TASK2_ID,task_in[TASK2_ID]); + run Worker1(task3Core,TASK3_ID,task_in[TASK3_ID]); + + _nr_pr == 1; + +//#ifdef TEST_GEN + assert(false); +//#endif + + printf("Barrier Manager Model finished !\n") +} \ No newline at end of file diff --git a/formal/promela/models/barriers/tc-barrier-mgr-model.c b/formal/promela/models/barriers/tc-barrier-mgr-model.c new file mode 100644 index 00000000..82fb29ff --- /dev/null +++ b/formal/promela/models/barriers/tc-barrier-mgr-model.c @@ -0,0 +1,180 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * @file + * + * @ingroup RTEMSTestCaseRtemsBarrierVal + */ + +/* + * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + * 2022 Trinity College Dublin (http://www.tcd.ie) + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +/* + * Do not manually edit this file. It is part of the RTEMS quality process + * and was automatically generated. + * + * If you find something that needs to be fixed or worded better please + * post a report to an RTEMS mailing list or raise a bug report: + * + * https://docs.rtems.org/branches/master/user/support/bugs.html + * + * For information on updating and regenerating please refer to: + * + * https://docs.rtems.org/branches/master/eng/req/howto.html + */ + +#ifdef HAVE_CONFIG_H +#include "config.h" +#endif + +#include <rtems/rtems/tasksdata.h> +#include <rtems/score/statesimpl.h> +#include <rtems/score/threadimpl.h> + +#include "tr-barrier-mgr-model.h" + +#include <rtems/test.h> + +/** + * @defgroup RTEMSTestCaseRtemsBarrierVal + * + * @ingroup RTEMSTestSuiteTestsuitesValidation0 + * + * @brief Tests the rtems_barrier_create, rtems_barrier_ident, + * rtems_barrier_wait, rtems_barrier_release and rtems_barrier_delete + * directives. + * + * This test case performs the following actions: + * + * - Runs tests for Barrier Manager + * + * @{ + */ + +/** + * @fn void T_case_body_RtemsBarrierVal void ) + */ +T_TEST_CASE( RtemsModelBarrierMgr0 ) +{ + RtemsModelBarrierMgr_Run0(); +} + +T_TEST_CASE( RtemsModelBarrierMgr1 ) +{ + RtemsModelBarrierMgr_Run1(); +} + +T_TEST_CASE( RtemsModelBarrierMgr2 ) +{ + RtemsModelBarrierMgr_Run2(); +} + +T_TEST_CASE( RtemsModelBarrierMgr3 ) +{ + RtemsModelBarrierMgr_Run3(); +} + +T_TEST_CASE( RtemsModelBarrierMgr4 ) +{ + RtemsModelBarrierMgr_Run4(); +} + +T_TEST_CASE( RtemsModelBarrierMgr5 ) +{ + RtemsModelBarrierMgr_Run5(); +} + +T_TEST_CASE( RtemsModelBarrierMgr6 ) +{ + RtemsModelBarrierMgr_Run6(); +} + +T_TEST_CASE( RtemsModelBarrierMgr7 ) +{ + RtemsModelBarrierMgr_Run7(); +} + +T_TEST_CASE( RtemsModelBarrierMgr8 ) +{ + RtemsModelBarrierMgr_Run8(); +} + +T_TEST_CASE( RtemsModelBarrierMgr9 ) +{ + RtemsModelBarrierMgr_Run9(); +} + +T_TEST_CASE( RtemsModelBarrierMgr10 ) +{ + RtemsModelBarrierMgr_Run10(); +} + +T_TEST_CASE( RtemsModelBarrierMgr11 ) +{ + RtemsModelBarrierMgr_Run11(); +} + +T_TEST_CASE( RtemsModelBarrierMgr12 ) +{ + RtemsModelBarrierMgr_Run12(); +} + +T_TEST_CASE( RtemsModelBarrierMgr13 ) +{ + RtemsModelBarrierMgr_Run13(); +} + +T_TEST_CASE( RtemsModelBarrierMgr14 ) +{ + RtemsModelBarrierMgr_Run14(); +} + +T_TEST_CASE( RtemsModelBarrierMgr15 ) +{ + RtemsModelBarrierMgr_Run15(); +} + +T_TEST_CASE( RtemsModelBarrierMgr16 ) +{ + RtemsModelBarrierMgr_Run16(); +} + +T_TEST_CASE( RtemsModelBarrierMgr17 ) +{ + RtemsModelBarrierMgr_Run17(); +} + +T_TEST_CASE( RtemsModelBarrierMgr18 ) +{ + RtemsModelBarrierMgr_Run18(); +} + +T_TEST_CASE( RtemsModelBarrierMgr19 ) +{ + RtemsModelBarrierMgr_Run19(); +} + +/** @} */ diff --git a/formal/promela/models/barriers/tr-barrier-mgr-model.c b/formal/promela/models/barriers/tr-barrier-mgr-model.c new file mode 100644 index 00000000..18b949e6 --- /dev/null +++ b/formal/promela/models/barriers/tr-barrier-mgr-model.c @@ -0,0 +1,249 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * @file + * + * @ingroup RTEMSTestCaseRtemsModelBarrierMgr + */ + +/* + * Copyright (C) 2020-2022 embedded brains GmbH (http://www.embedded-brains.de) + * Trinity College Dublin (http://www.tcd.ie) + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +/* + * This file was automatically generated. Do not edit it manually. + * Please have a look at + * + * https://docs.rtems.org/branches/master/eng/req/howto.html + * + * for information how to maintain and re-generate this file. + */ + +#ifdef HAVE_CONFIG_H +#include "config.h" +#endif + +#include <rtems/score/threadimpl.h> + +#include "tr-barrier-mgr-model.h" +#include "tx-support.h" + +static const char PromelaModelBarrierMgr[] = "/PML-BarrierMgr"; + +rtems_id CreateSema( char * name ) +{ + rtems_status_code sc; + rtems_id id; + + sc = rtems_semaphore_create( + rtems_build_name( name[ 0 ], name[ 1 ], name[ 2 ], name[ 3 ] ), + 0, + RTEMS_SIMPLE_BINARY_SEMAPHORE, + 0, + &id + ); + T_assert_rsc_success( sc ); + + return id; +} + +void DeleteSema( rtems_id id ) +{ + if ( id != 0 ) { + rtems_status_code sc; + + sc = rtems_semaphore_delete( id ); + T_rsc_success( sc ); + } +} + +void ObtainSema( rtems_id id ) +{ + rtems_status_code sc; + sc = rtems_semaphore_obtain( id, RTEMS_WAIT, RTEMS_NO_TIMEOUT ); + T_quiet_rsc_success( sc ); +} + +void ReleaseSema( rtems_id id ) +{ + rtems_status_code sc; + + sc = rtems_semaphore_release( id ); + T_quiet_rsc_success( sc ); +} + +// rtems_task_priority SetPriority( rtems_id id, rtems_task_priority priority ) +// { +// rtems_status_code sc; +// rtems_task_priority previous; +// +// sc = rtems_task_set_priority( id, priority, &previous ); +// T_rsc_success( sc ); +// +// return previous; +// } + +// rtems_task_priority SetSelfPriority( rtems_task_priority priority ) +// { +// return SetPriority( RTEMS_SELF, priority ); +// } + +// rtems_id DoCreateTask( rtems_name name, rtems_task_priority priority ) +// { +// rtems_status_code sc; +// rtems_id id; +// +// sc = rtems_task_create( +// name, +// priority, +// RTEMS_MINIMUM_STACK_SIZE, +// RTEMS_DEFAULT_MODES, +// RTEMS_DEFAULT_ATTRIBUTES, +// &id +// ); +// T_assert_rsc_success( sc ); +// +// return id; +// } + +// void StartTask( rtems_id id, rtems_task_entry entry, void *arg ) +// { +// rtems_status_code sc; +// +// sc = rtems_task_start( id, entry, (rtems_task_argument) arg); +// T_assert_rsc_success( sc ); +// } + +// void DeleteTask( rtems_id id ) +// { +// if ( id != 0 ) { +// rtems_status_code sc; +// T_printf( "L:Deleting Task id : %d\n", id ); +// sc = rtems_task_delete( id ); +// T_rsc_success( sc ); +// } +// } + +rtems_attribute mergeattribs( bool automatic ) +{ + rtems_attribute attribs; + + if ( automatic ) { attribs = RTEMS_BARRIER_AUTOMATIC_RELEASE; } + else { attribs = RTEMS_BARRIER_MANUAL_RELEASE; } + + return attribs; +} + +void checkTaskIs( rtems_id expected_id ) +{ + rtems_id own_id; + + own_id = _Thread_Get_executing()->Object.id; + T_eq_u32( own_id, expected_id ); +} + +void initialise_semaphore( Context *ctx, rtems_id semaphore[] ) { + semaphore[0] = ctx->runner_sema; + semaphore[1] = ctx->worker0_sema; + semaphore[2] = ctx->worker1_sema; +} + +void ShowSemaId( Context *ctx ) { + T_printf( "L:ctx->runner_sema = %d\n", ctx->runner_sema ); + T_printf( "L:ctx->worker0_sema = %d\n", ctx->worker0_sema ); + T_printf( "L:ctx->worker1_sema = %d\n", ctx->worker1_sema ); +} + +void initialise_id ( rtems_id * id ) { + *id = 0; +} + +void RtemsModelBarrierMgr_Teardown( void *arg ) +{ + RtemsModelBarrierMgr_Context *ctx; + + ctx = arg; + + rtems_status_code sc; + rtems_task_priority prio; + + T_log( T_NORMAL, "Teardown" ); + + prio = 0; + sc = rtems_task_set_priority( RTEMS_SELF, BM_PRIO_HIGH, &prio ); + T_rsc_success( sc ); + T_eq_u32( prio, BM_PRIO_NORMAL ); + + DeleteTask(ctx->worker0_id); + DeleteTask(ctx->worker1_id); + + T_log( T_NORMAL, "Deleting Runner Semaphore" ); + DeleteSema( ctx->runner_sema ); + T_log( T_NORMAL, "Deleting Worker0 Semaphore" ); + DeleteSema( ctx->worker0_sema ); + T_log( T_NORMAL, "Deleting Worker1 Semaphore" ); + DeleteSema( ctx->worker1_sema ); +} + + +size_t RtemsModelBarrierMgr_Scope( void *arg, char *buf, size_t n ) +{ + RtemsModelBarrierMgr_Context *ctx; + size_t m; + int p10; + int tnum ; + char digit; + + ctx = arg; + p10 = POWER_OF_10; + + m = T_str_copy(buf, PromelaModelBarrierMgr, n); + buf += m; + tnum = ctx->this_test_number; + while( p10 > 0 && m < n ) + { + digit = (char) ( (int) '0' + tnum / p10 ); + buf[0] = digit; + ++buf; + ++m; + tnum = tnum % p10; + p10 /= 10; + } + return m; +} + +void RtemsModelBarrierMgr_Cleanup( + RtemsModelBarrierMgr_Context *ctx +) +{ + rtems_status_code sc; + + if (ctx->barrier_id != 0) { + sc = rtems_barrier_delete(ctx->barrier_id); + if ( sc != RTEMS_SUCCESSFUL ) { + T_quiet_rsc( sc, RTEMS_INVALID_ID ); + } + } +} diff --git a/formal/promela/models/barriers/tr-barrier-mgr-model.h b/formal/promela/models/barriers/tr-barrier-mgr-model.h new file mode 100644 index 00000000..2f8ae19d --- /dev/null +++ b/formal/promela/models/barriers/tr-barrier-mgr-model.h @@ -0,0 +1,197 @@ +/* SPDX-License-Identifier: BSD-2-Clause */ + +/** + * @file + * + * @ingroup RTEMSTestCaseRtemsModelBarrierMgr_Run + */ + +/* + * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + * 2022 Trinity College Dublin (http://www.tcd.ie) + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +/* + * Do not manually edit this file. It is part of the RTEMS quality process + * and was automatically generated. + * + * If you find something that needs to be fixed or worded better please + * post a report to an RTEMS mailing list or raise a bug report: + * + * https://docs.rtems.org/branches/master/user/support/bugs.html + * + * For information on updating and regenerating please refer to: + * + * https://docs.rtems.org/branches/master/eng/req/howto.html + */ + +#ifndef _TR_MODEL_BARRIER_MGR_H +#define _TR_MODEL_BARRIER_MGR_H + +#include <rtems.h> +#include <rtems/score/thread.h> + +#include <rtems/test.h> +#include "tx-support.h" + +#ifdef __cplusplus +extern "C" { +#endif + +/* + * Run Setup/Cleanup structs/functions + */ +typedef struct { + int this_test_number; // test number used to identify a test runner instance + + Thread_Control *runner_thread; // TCB of the runner task + rtems_id runner_id; // ID of the tasks + rtems_id worker0_id; + rtems_id worker1_id; + + rtems_id runner_sema; // ID of the Runner semaphore + rtems_id worker0_sema; // ID of the Worker0 semaphore + rtems_id worker1_sema; // ID of the Worker1 semaphore + rtems_id barrier_id; // ID of the created barrier + + rtems_id runner_sched; // scheduler ID of scheduler used by the runner task + rtems_id other_sched; // scheduler ID of another scheduler + // which is not used by the runner task + T_thread_switch_log_4 thread_switch_log; // thread switch log +} RtemsModelBarrierMgr_Context; + +typedef enum { + BM_PRIO_HIGH = 1, + BM_PRIO_NORMAL, + BM_PRIO_LOW, + BM_PRIO_OTHER +} Priorities; + +#define POWER_OF_10 100 + +#define CreateTask( name, priority ) \ + DoCreateTask( \ + rtems_build_name( name[ 0 ], name[ 1 ], name[ 2 ], name[ 3 ] ), \ + priority \ + ) + +typedef RtemsModelBarrierMgr_Context Context; + +rtems_id DoCreateTask( rtems_name name, rtems_task_priority priority ); + +void StartTask( rtems_id id, rtems_task_entry entry, void *arg ); + +void DeleteTask( rtems_id id ); + +rtems_id CreateSema( char * name); + +void DeleteSema( rtems_id id ); + +void ObtainSema( rtems_id id ); + +void ReleaseSema( rtems_id id ); + +rtems_task_priority SetPriority( rtems_id id, rtems_task_priority priority ); + +rtems_task_priority SetSelfPriority( rtems_task_priority priority ); + +rtems_option mergeattribs( bool automatic ); + +void checkTaskIs( rtems_id expected_id ) ; + +void ShowSemaId( Context *ctx ) ; + +void initialise_id ( rtems_id * id ); + +void initialise_semaphore( Context *ctx, rtems_id semaphore[] ); + +void RtemsModelBarrierMgr_Setup( void *arg ) ; + +void RtemsModelBarrierMgr_Teardown( void *arg ) ; + +size_t RtemsModelBarrierMgr_Scope( void *arg, char *buf, size_t n ) ; + +void RtemsModelBarrierMgr_Cleanup( RtemsModelBarrierMgr_Context *ctx ); + +/** + * @addtogroup RTEMSTestCaseRtemsModelBarrierMgr_Run + * + * @{ + */ + +/** + * @brief Runs the test case. + */ + +void RtemsModelBarrierMgr_Run0(void); + +void RtemsModelBarrierMgr_Run1(void); + +void RtemsModelBarrierMgr_Run2(void); + +void RtemsModelBarrierMgr_Run3(void); + +void RtemsModelBarrierMgr_Run4(void); + +void RtemsModelBarrierMgr_Run5(void); + +void RtemsModelBarrierMgr_Run6(void); + +void RtemsModelBarrierMgr_Run7(void); + +void RtemsModelBarrierMgr_Run8(void); + +void RtemsModelBarrierMgr_Run9(void); + +void RtemsModelBarrierMgr_Run10(void); + +void RtemsModelBarrierMgr_Run11(void); + +void RtemsModelBarrierMgr_Run12(void); + +void RtemsModelBarrierMgr_Run13(void); + +void RtemsModelBarrierMgr_Run14(void); + +void RtemsModelBarrierMgr_Run15(void); + +void RtemsModelBarrierMgr_Run16(void); + +void RtemsModelBarrierMgr_Run17(void); + +void RtemsModelBarrierMgr_Run18(void); + +void RtemsModelBarrierMgr_Run19(void); + +void RtemsModelBarrierMgr_Run20(void); + +void RtemsModelBarrierMgr_Run21(void); + +/** @} */ + +#ifdef __cplusplus +} +#endif + +#endif /* _TR_BARRIER_H */ -- 2.37.1 (Apple Git-137.1) _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
