[PATCH 02/18] adds barrier manager model
Andrew.Butterfield at scss.tcd.ie
Andrew.Butterfield at scss.tcd.ie
Thu Dec 22 11:32:21 UTC 2022
---
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)
More information about the devel
mailing list