[PATCH 08/18] adds message manager model
Andrew.Butterfield at scss.tcd.ie
Andrew.Butterfield at scss.tcd.ie
Thu Dec 22 11:40:32 UTC 2022
From 4364f65705b387697c33181cb8a9a7b772ea7f58 Mon Sep 17 00:00:00 2001
From: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>
Date: Wed, 21 Dec 2022 16:31:40 +0000
Subject: [PATCH 08/18] adds message manager model
---
formal/promela/models/messages/README.md | 10 +
formal/promela/models/messages/STATUS.md | 14 +
.../models/messages/msg-mgr-model-post.h | 8 +
.../models/messages/msg-mgr-model-pre.h | 51 ++
.../models/messages/msg-mgr-model-rfn.yml | 202 +++++
.../models/messages/msg-mgr-model-run.h | 191 ++++
.../promela/models/messages/msg-mgr-model.pml | 842 ++++++++++++++++++
.../models/messages/tc-msg-mgr-model.c | 211 +++++
.../models/messages/tr-msg-mgr-model.c | 240 +++++
.../models/messages/tr-msg-mgr-model.h | 132 +++
10 files changed, 1901 insertions(+)
create mode 100644 formal/promela/models/messages/README.md
create mode 100644 formal/promela/models/messages/STATUS.md
create mode 100644 formal/promela/models/messages/msg-mgr-model-post.h
create mode 100644 formal/promela/models/messages/msg-mgr-model-pre.h
create mode 100644 formal/promela/models/messages/msg-mgr-model-rfn.yml
create mode 100644 formal/promela/models/messages/msg-mgr-model-run.h
create mode 100644 formal/promela/models/messages/msg-mgr-model.pml
create mode 100644 formal/promela/models/messages/tc-msg-mgr-model.c
create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.c
create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.h
diff --git a/formal/promela/models/messages/README.md b/formal/promela/models/messages/README.md
new file mode 100644
index 00000000..2eb723b5
--- /dev/null
+++ b/formal/promela/models/messages/README.md
@@ -0,0 +1,10 @@
+# Message Manager model
+
+Developer: Eoin Lynch
+
+This directory contains the code for the generation/running of tests for the [RTEMS Message Manager](https://docs.rtems.org/branches/master/c-user/message/index.html)
+
+It is a subset of the material available at [Eoin Lynch's project repository](https://github.com/lynche12/SPIN-PromelaTestGeneration).
+
+This project is research work done for his dissertation as part of the MAI in Computer Engineering program at Trinity College Dublin
+
diff --git a/formal/promela/models/messages/STATUS.md b/formal/promela/models/messages/STATUS.md
new file mode 100644
index 00000000..361984c6
--- /dev/null
+++ b/formal/promela/models/messages/STATUS.md
@@ -0,0 +1,14 @@
+# MESSAGE MANAGER status
+
+## 3rd Nov 2022 TEST FAIL
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: NO, 1 failure
+```
+F:0.17:0:"x/PML-MessageMgr022:tr-msg-mgr-model-22.c:192:RTEMS_SUCCESSFUL == RTEMS_TIMEOUT
+```
+
+See `events/archive/20221103-170322`
diff --git a/formal/promela/models/messages/msg-mgr-model-post.h b/formal/promela/models/messages/msg-mgr-model-post.h
new file mode 100644
index 00000000..9a9606d3
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelMessageMgr_Context *ctx )
+{
+ T_log( T_NORMAL, "Runner running" );
+ TestSegment3( ctx );
+ T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/messages/msg-mgr-model-pre.h b/formal/promela/models/messages/msg-mgr-model-pre.h
new file mode 100644
index 00000000..f3986267
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelMessageMgr
+ */
+
+/*
+ * Copyright (C) 2020 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-msg-mgr-model.h"
\ No newline at end of file
diff --git a/formal/promela/models/messages/msg-mgr-model-rfn.yml b/formal/promela/models/messages/msg-mgr-model-rfn.yml
new file mode 100644
index 00000000..f5fc8120
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-rfn.yml
@@ -0,0 +1,202 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+LANGUAGE: C
+
+SEGNAMEPFX: TestSegment{} # segnumber
+SEGARG: Context* ctx
+SEGDECL: static void {}( {} ) # segnamepf{segnumber}, segarg,
+SEGBEGIN: " {"
+SEGEND: "}"
+
+NAME: |
+ /* Test Name is defined in the Test Case code (tc-model-msg-mgr.c) */
+
+semaphore_DCL: rtems_id {0}[SEMA_MAX];
+
+sendrc_DCL: rtems_status_code
+
+recrc_DCL: rtems_status_code
+
+qrc_DCL: rtems_status_code
+
+queue_buffer_DCL: RTEMS_MESSAGE_QUEUE_BUFFER( MAX_MESSAGE_SIZE ) {0} [MAX_PENDING_MESSAGES];
+
+receive_buffer_DCL: uint8_t {0} [ MAX_MESSAGE_SIZE ];
+
+send_buffer_DCL: uint8_t {0} [ MAX_MESSAGE_SIZE ];
+
+send_counter_DCL: uint8_t
+
+INIT: |
+ initialise_semaphore( ctx, semaphore );
+
+Runner: |
+ checkTaskIs( ctx->runner_id );
+
+Worker1: |
+ checkTaskIs( ctx->worker1_id );
+
+Worker2: |
+ checkTaskIs( ctx->worker2_id );
+
+SIGNAL: |
+ Wakeup( semaphore[{}] );
+
+WAIT: |
+ Wait( semaphore[{}] );
+
+message_queue_construct: |
+ T_log( T_NORMAL, "Calling construct(%d,%d,%d,%d,%d)");
+
+ rtems_message_queue_config config;
+ config.name = {3};
+ config.maximum_pending_messages = MAX_PENDING_MESSAGES;
+ config.maximum_message_size = MAX_MESSAGE_SIZE;
+ config.storage_area = queue_buffer;
+ config.storage_size = sizeof( queue_buffer );
+ config.storage_free = NULL;
+ config.attributes = RTEMS_DEFAULT_ATTRIBUTES;
+
+ {5} = rtems_message_queue_construct(
+ &config,
+ &ctx->queue_id
+ );
+ T_log(T_NORMAL, "Queue id 0x%x", ctx->queue_id);
+ T_log( T_NORMAL, "Returned 0x%x from construct", {5} );
+
+
+
+message_queue_send: |
+ T_log( T_NORMAL, "Calling Send(%d,%d)");
+
+ memset( send_buffer, {2}, {3} );
+
+ {4} = rtems_message_queue_send(
+ idNull(ctx, {1}),
+ {2} ? send_buffer : NULL,
+ {3}
+ );
+
+ T_log( T_NORMAL, "Returned 0x%x from send", {4} );
+
+message_queue_receive: |
+ T_log( T_NORMAL, "Calling Receive(%d,%d)");
+ size_t receive_size;
+ {4} = rtems_message_queue_receive(
+ idNull(ctx, {1}),
+ receive_buffer,
+ &receive_size,
+ mergeopts({2}),
+ getTimeout({3})
+ );
+ T_log( T_NORMAL, "Returned 0x%x from receive", {4} );
+
+sendrc:
+ T_rsc( sendrc, {0} );
+
+recrc:
+ T_rsc( recrc, {0} );
+
+qrc:
+ T_rsc( qrc, {0} );
+
+recout:
+ T_eq_int( recout[{0}], {1} );
+
+Ready: |
+ /* We (Task {0}) must have been recently ready because we are running */
+
+Zombie:
+ /* Code to check that Task {0} has terminated */
+
+EventWait:
+ /* Code to check that Task {0} is waiting on events */
+
+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} */
+
+LowerPriority: |
+ SetSelfPriority( 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, PRIO_LOW );
+
+EqualPriority: |
+ SetSelfPriority( 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, PRIO_NORMAL );
+
+HigherPriority: |
+ SetSelfPriority( 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, 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 );
+ }
+
+RunnerScheduler: |
+ uint32_t processor = {};
+ rtems_status_code sc1;
+ rtems_id current_sched;
+ sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+ T_log( T_NORMAL, "current scheduler id: %d", ¤t_sched);
+ sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->runner_sched );
+ T_rsc_success( sc1 );
+ T_log( T_NORMAL, "runner scheduler id: %d", &ctx->runner_sched);
+ sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->runner_sched, RTEMS_CURRENT_PRIORITY);
+ T_rsc_success( sc1 );
+ sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+ T_log( T_NORMAL, "current scheduler id: %d", ¤t_sched);
+
+OtherScheduler: |
+ uint32_t processor = {};
+ rtems_status_code sc1;
+ rtems_id current_sched;
+ sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+ T_log( T_NORMAL, "current scheduler id: %d", ¤t_sched);
+ sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->other_sched );
+ T_rsc_success( sc1 );
+ T_log( T_NORMAL, "other scheduler id: %d", &ctx->other_sched);
+ sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->other_sched, RTEMS_CURRENT_PRIORITY);
+ T_rsc_success( sc1 );
+ sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+ T_log( T_NORMAL, "current scheduler id: %d", ¤t_sched);
+
+SetProcessor: |
+ T_eq_u32( rtems_scheduler_get_processor_maximum(), 2 );
+ uint32_t processor = {};
+ cpu_set_t cpuset;
+ CPU_ZERO(&cpuset);
+ CPU_SET(processor, &cpuset);
diff --git a/formal/promela/models/messages/msg-mgr-model-run.h b/formal/promela/models/messages/msg-mgr-model-run.h
new file mode 100644
index 00000000..e9430df1
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-run.h
@@ -0,0 +1,191 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/*
+static void Worker{0}( rtems_task_argument arg )
+{{
+ Context *ctx;
+
+ ctx = (Context *) arg;
+ rtems_event_set events;
+
+ T_log( T_NORMAL, "Worker Running" );
+ TestSegment4( ctx );
+ T_log( T_NORMAL, "Worker finished" );
+
+ rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
+}}
+
+
+RTEMS_ALIGNED( RTEMS_TASK_STORAGE_ALIGNMENT ) static char WorkerStorage{0}[
+ RTEMS_TASK_STORAGE_SIZE(
+ MAX_TLS_SIZE + RTEMS_MINIMUM_STACK_SIZE,
+ WORKER_ATTRIBUTES
+ )
+];
+
+static const rtems_task_config WorkerConfig{0} = {{
+ .name = rtems_build_name( 'W', 'O', 'R', 'K' ),
+ .initial_priority = PRIO_LOW,
+ .storage_area = WorkerStorage{0},
+ .storage_size = sizeof( WorkerStorage{0} ),
+ .maximum_thread_local_storage_size = MAX_TLS_SIZE,
+ .initial_modes = RTEMS_DEFAULT_MODES,
+ .attributes = WORKER_ATTRIBUTES
+}};
+
+*/
+static void Worker1( rtems_task_argument arg )
+{{
+ Context *ctx;
+
+ ctx = (Context *) arg;
+ rtems_event_set events;
+
+ T_log( T_NORMAL, "Worker1 Running" );
+ TestSegment4( ctx );
+ T_log( T_NORMAL, "Worker1 finished" );
+
+ rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
+}}
+
+static void Worker2( rtems_task_argument arg )
+{{
+ Context *ctx;
+
+ ctx = (Context *) arg;
+ rtems_event_set events;
+
+ T_log( T_NORMAL, "Worker2 Running" );
+ TestSegment5( ctx );
+ T_log( T_NORMAL, "Worker2 finished" );
+
+ rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
+}}
+
+static void RtemsModelMessageMgr_Setup{0}(
+ RtemsModelMessageMgr_Context *ctx
+)
+{{
+ 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;
+ ctx->worker1_wakeup = CreateWakeupSema();
+ ctx->worker2_wakeup = CreateWakeupSema();
+ ctx->runner_wakeup = CreateWakeupSema();
+
+ 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, PRIO_NORMAL, &prio );
+ T_rsc_success( sc );
+ T_eq_u32( prio, PRIO_HIGH );
+
+ //sc = rtems_task_construct( &WorkerConfig{0}, &ctx->worker_id );
+ //T_log( T_NORMAL, "Construct Worker, sc = %x", sc );
+ //T_assert_rsc_success( sc );
+
+ //T_log( T_NORMAL, "Starting Worker..." );
+ //sc = rtems_task_start( ctx->worker_id, Worker{0}, (rtems_task_argument) ctx );
+ //T_log( T_NORMAL, "Started Worker, sc = %x", sc );
+ //T_assert_rsc_success( sc );
+
+ sc = rtems_task_create("WRKR",
+ PRIO_NORMAL,
+ RTEMS_MINIMUM_STACK_SIZE,
+ RTEMS_DEFAULT_MODES,
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &ctx->worker1_id);
+ T_assert_rsc_success( sc );
+
+ T_log( T_NORMAL, "Starting Worker1..." );
+ sc = rtems_task_start( ctx->worker1_id, Worker1,ctx );
+ T_log( T_NORMAL, "Started Worker1, sc = %x", sc );
+ T_assert_rsc_success( sc );
+
+ sc = rtems_task_create("WRKR",
+ PRIO_NORMAL,
+ RTEMS_MINIMUM_STACK_SIZE,
+ RTEMS_DEFAULT_MODES,
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &ctx->worker2_id);
+ T_assert_rsc_success( sc );
+
+ T_log( T_NORMAL, "Starting Worker2..." );
+ sc = rtems_task_start( ctx->worker2_id, Worker2,ctx );
+ T_log( T_NORMAL, "Started Worker2, sc = %x", sc );
+ T_assert_rsc_success( sc );
+
+}}
+
+
+static void RtemsModelMessageMgr_Setup_Wrap{0}( void *arg )
+{{
+ RtemsModelMessageMgr_Context *ctx;
+
+ ctx = arg;
+ RtemsModelMessageMgr_Setup{0}( ctx );
+}}
+
+
+static RtemsModelMessageMgr_Context RtemsModelMessageMgr_Instance{0};
+
+static T_fixture RtemsModelMessageMgr_Fixture{0} = {{
+ .setup = RtemsModelMessageMgr_Setup_Wrap{0},
+ .stop = NULL,
+ .teardown = RtemsModelMessageMgr_Teardown_Wrap,
+ .scope = RtemsModelMessageMgr_Scope,
+ .initial_context = &RtemsModelMessageMgr_Instance{0}
+}};
+
+static T_fixture_node RtemsModelMessageMgr_Node{0};
+
+void RtemsModelMessageMgr_Run{0}()
+{{
+ RtemsModelMessageMgr_Context *ctx;
+
+ T_set_verbosity( T_NORMAL );
+
+ T_log( T_NORMAL, "Runner Invoked" );
+ T_log( T_NORMAL, "Pushing Test Fixture..." );
+
+
+ ctx = T_push_fixture(
+ &RtemsModelMessageMgr_Node{0},
+ &RtemsModelMessageMgr_Fixture{0}
+ );
+
+ T_log( T_NORMAL, "Test Fixture Pushed" );
+
+
+
+ ctx->this_test_number = {0};
+
+
+ ctx->send_status = RTEMS_INCORRECT_STATE;
+ ctx->receive_option_set = 0;
+ ctx->receive_timeout = RTEMS_NO_TIMEOUT;
+ _Thread_Wait_flags_set( ctx->runner_thread, THREAD_WAIT_CLASS_PERIOD );
+
+ TestSegment0( ctx );
+
+ Runner( ctx );
+
+ RtemsModelMessageMgr_Cleanup( ctx );
+
+ T_log( T_NORMAL, "Run Pop Fixture" );
+ T_pop_fixture();
+}}
+
+/** @}} */
diff --git a/formal/promela/models/messages/msg-mgr-model.pml b/formal/promela/models/messages/msg-mgr-model.pml
new file mode 100644
index 00000000..36c54571
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model.pml
@@ -0,0 +1,842 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+// Message queue attributes
+
+#define TASK_MAX 4 //three rtems tasks
+#define NULL 0
+
+#define SEMA_MAX 3
+
+#define BAD_ID TASK_MAX
+
+#define MAX_MESSAGE_QUEUES 3
+#define MAX_PENDING_MESSAGES 4
+#define MAX_MESSAGE_SIZE 1
+#define QUEUE_NAME 1
+
+//define 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_InvAddr 9 // RTEMS_INVALID_ADDRESS
+#define RC_Unsat 13 // RTEMS_UNSATISFIED
+#define RC_Timeout 6 // RTEMS_TIMEOUT
+#define RC_InvSize 8 // RTEMS_INVALID_SIZE
+#define RC_InvNum 10 // RTEMS_INVALID_NUMBER
+#define RC_TooMany 5 // RTEMS_TOO_MANY
+
+inline outputDefines() {
+ printf("@@@ %d DEF TASK_MAX %d\n",_pid,TASK_MAX);
+ printf("@@@ %d DEF BAD_ID %d\n",_pid,BAD_ID);
+ printf("@@@ %d DEF SEMA_MAX %d\n",_pid,SEMA_MAX);
+ printf("@@@ %d DEF MAX_MESSAGE_SIZE %d\n",_pid, MAX_MESSAGE_SIZE);
+ printf("@@@ %d DEF MAX_MESSAGE_QUEUES %d\n",_pid, MAX_MESSAGE_QUEUES);
+ printf("@@@ %d DEF MAX_PENDING_MESSAGES %d\n",_pid, MAX_PENDING_MESSAGES);
+}
+
+
+mtype = {
+ Zombie, Ready, MsgWait, TimeWait, OtherWait, // Task states
+ Wait, NoWait // Option Set values
+};
+
+
+// Tasks
+typedef Task {
+ byte nodeid; // So we can spot remote calls
+ byte pmlid; // Promela process id
+ mtype state ; // {Ready,EventWait,TickWait,OtherWait}
+ bool preemptable ;
+ byte prio ; // lower number is higher priority
+ int ticks; //
+ bool tout; // true if woken by a timeout
+ bool doCreate; // whether to create a queue
+ bool doSend; //whether task should send
+ bool doReceive; //whether task should receive
+ bool doWait; //whether task should wait message
+ int rcvInterval; //how many ticks to wait
+ int rcvMsg; //hold value of message received, modelling receive buffer
+ int sndMsg; //hold value of message to send, modelling send buffer
+ int targetQueue; //queue id for task to interact with
+ int numSends; //number of message send calls to make
+ int msgSize; //size of message to send
+};
+
+Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference
+
+
+byte sendrc; // Sender global variable
+byte recrc; // Receiver global variable
+byte qrc // creation variable
+byte recout[TASK_MAX] ; // models receive 'out' location.
+
+
+bool semaphore[SEMA_MAX]; // Semaphore
+
+mtype = {
+ FIFO, PRIORITY
+};
+
+typedef Config {
+ int name; //An integer is used to represent valid RTEMS_NAME
+ int count; //Max messages for a queue
+ int maxSize; //Max message size
+ mtype attrSet; // RTEMS_ATTRIBUTE_SET, FIFO||priority
+};
+
+typedef MessageQueue {
+ Config config;
+ int messages [MAX_PENDING_MESSAGES] //message circular buffer
+ int head; //top of message queue
+ int tail; //end of message queue
+ bool queueFull; //used to determine full or empty state
+ int waitingTasks [TASK_MAX]; //task circular buffer
+ int nextTask; //top of task queue
+ int lastTask; //end of task queue
+ bool taskFull;
+};
+
+MessageQueue queueList[MAX_MESSAGE_QUEUES]; //queueList[0] is null
+
+/*
+* Helper functions for task
+* and message queue operations
+*/
+
+inline enqueueTask(id, qid) {
+ atomic{
+ queueList[qid].waitingTasks[queueList[qid].lastTask] = id;
+ if
+ :: queueList[qid].lastTask == TASK_MAX-1 -> queueList[qid].lastTask = 0;
+ :: else -> queueList[qid].lastTask++;
+ fi
+ if
+ :: queueList[qid].lastTask == queueList[qid].nextTask -> queueList[qid].taskFull = true;
+ :: else -> skip;
+ fi
+ }
+}
+
+inline dequeueTask(id,qid) {
+ atomic{
+ id = queueList[qid].waitingTasks[queueList[qid].nextTask];
+ if
+ :: queueList[qid].nextTask == TASK_MAX-1 -> queueList[qid].nextTask = 0;
+ :: else -> queueList[qid].nextTask++;
+ fi
+ if
+ :: queueList[qid].lastTask == queueList[qid].nextTask -> queueList[qid].taskFull = false;
+ :: else -> skip;
+ fi
+ }
+}
+
+
+
+inline enqueueMessage(id,msg) {
+ atomic{
+ queueList[id].messages[queueList[id].head] = msg;
+ //printf("enqueue message %d", msg);
+ if
+ :: queueList[id].head == MAX_PENDING_MESSAGES-1 -> queueList[id].head = 0;
+ :: else -> queueList[id].head++;
+ fi
+ if
+ :: queueList[id].head == queueList[id].tail -> queueList[id].queueFull = true;
+ :: else -> skip;
+ fi
+ }
+}
+
+inline dequeueMessage(id,msg) {
+ atomic{
+ msg = queueList[id].messages[queueList[id].tail];
+ //printf("dequeue message %d", msg);
+ if
+ :: msg == 0 -> skip;
+ :: queueList[id].tail == MAX_PENDING_MESSAGES-1 -> queueList[id].tail = 0;
+ :: else -> queueList[id].tail++;
+ fi
+ if
+ :: queueList[id].head == queueList[id].tail -> queueList[id].queueFull = false;
+ :: else -> skip;
+ fi
+ }
+}
+
+
+inline sizeOfQueue(id, qsize) {
+ atomic{
+ if
+ :: queueList[id].head == queueList[id].tail ->
+ if
+ :: -> qsize = MAX_PENDING_MESSAGES;
+ :: else -> qsize = 0;
+ fi
+ :: queueList[id].head > queueList[id].tail -> qsize = queueList[id].head - queueList[id].tail;
+ :: queueList[id].head < queueList[id].tail -> qsize = MAX_PENDING_MESSAGES + queueList[id].head - queueList[id].tail;
+ fi
+ return qsize;
+ }
+}
+
+//Declare needed arrays, variables
+inline outputDeclarations () {
+ printf("@@@ %d DECL byte sendrc 0\n",_pid);
+ printf("@@@ %d DECL byte recrc 0\n",_pid);
+ printf("@@@ %d DECL byte qrc 0\n",_pid);
+ printf("@@@ %d DECL uint8_t send_counter 0\n",_pid);
+ printf("@@@ %d DCLARRAY uint8_t receive_buffer MAX_MESSAGE_SIZE\n",_pid);
+ printf("@@@ %d DCLARRAY uint8_t send_buffer MAX_MESSAGE_SIZE\n",_pid);
+ printf("@@@ %d DCLARRAY RTEMS_MESSAGE_QUEUE_BUFFER queue_buffer MAX_PENDING_MESSAGES\n",_pid);
+ // Rather than refine an entire Task array, we refine array 'slices'
+ printf("@@@ %d DCLARRAY byte recout TASK_MAX\n",_pid);
+ printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid);
+}
+
+inline nl() { printf("\n") }
+/*
+ * Synchronisation Mechanisms
+ * Obtain(sem_id) - call that waits to obtain semaphore `sem_id`
+ * Release(sem_id) - call that releases semaphore `sem_id`
+ * Released(sem_id) - simulates ecosystem behaviour releases `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
+ }
+}
+
+inline Released(sem_id)
+{
+ semaphore[sem_id] = true ;
+}
+
+
+/*
+ * 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)
+}
+
+
+/* message_queue_create()
+* creates a message queue object from passed parameters
+* queue_name -rtems object name
+* msg_count - max messages in queue
+* max_size - max message size
+* rc - return flag
+*/
+
+inline message_queue_create(queue_name, msg_count, max_size, rc) {
+ atomic{
+ //only one queue created
+ int qid = 1;
+ if
+ :: queue_name == 0 -> rc = RC_InvName;
+ :: max_size == 0 -> rc = RC_InvSize;
+ :: msg_count == 0 -> rc = RC_InvNum;
+ :: else ->
+ queueList[qid].config.count = msg_count;
+ queueList[qid].config.maxSize = max_size;
+ queueList[qid].queueFull = false;
+ queueList[qid].config.name = queue_name;
+ rc = RC_OK;
+ fi
+ ;
+ }
+}
+
+
+/*
+* message_queue_send
+* self: id of calling task
+* qid: id of queue
+* msg : message
+* size : size of the message
+* rc: return code
+*
+* This directive will send a message to the to the specficied
+* message queue.
+* If there is a task waiting it will copy the message to that tasks
+* buffer and unblock it
+* If there is no task waiting it will ad the message to the message queue
+*/
+
+inline message_queue_send(self,qid,msg,size,rc) {
+ atomic{
+ int queuedTask = queueList[qid].waitingTasks[queueList[qid].nextTask];
+ if
+ :: qid == 0 -> rc = RC_InvId;
+ :: else ->
+ if
+ :: msg == NULL -> rc = RC_InvAddr;
+ :: size > queueList[qid].config.maxSize -> rc = RC_InvSize;
+ :: queueList[qid].queueFull -> rc = RC_TooMany;
+ :: else ->
+ if
+ :: queuedTask == 0 -> //no task waiting, add to buffer
+ enqueueMessage(qid,msg);
+ printf("@@@ %d LOG Send queueing message\n",_pid)
+ rc = RC_OK;
+ :: else -> //task waiting
+ dequeueTask(queuedTask,qid);
+ enqueueMessage(qid,msg);
+ printf("@@@ %d LOG Send to task %d\n",_pid, queuedTask)
+ //tasks[queuedTask].rcvMsg = msg;
+ //printf("%d rcv msg %d",_pid,tasks[queuedTask].rcvMsg)
+ tasks[queuedTask].state = Ready
+ printf("@@@ %d STATE %d Ready\n",_pid, queuedTask)
+ rc = RC_OK;
+ fi
+ fi
+ fi
+ }
+}
+
+inline message_queue_receive(self,qid,msg,rc) {
+ int rcvmsg;
+ atomic{
+ if
+ :: qid == 0 -> rc = RC_InvId;
+ //:: msg == 0 -> rc = RC_InvAddr
+ //:: size >= config.maxSize -> RC_InvSize
+ :: else ->
+ dequeueMessage(qid,msg);
+ if
+ :: msg == 0 && !tasks[self].doWait ->
+ rc = RC_Unsat; printf("@@@ %d LOG Receive Not Satisfied (no wait)\n",_pid)
+ :: msg == 0 && tasks[self].doWait ->
+ printf("@@@ %d LOG Receive Not Satisfied (timeout %d)\n",
+ _pid,
+ tasks[self].rcvInterval);
+ tasks[self].ticks = tasks[self].rcvInterval;
+ tasks[self].tout = false;
+ printf("@@@ %d STATE %d TimeWait %d\n",
+ _pid,
+ self,
+ tasks[self].rcvInterval);
+ tasks[self].state = TimeWait;
+ enqueueTask(self,qid);
+ waitUntilReady(self);
+
+ if
+ :: tasks[self].tout -> dequeueTask(self,qid); rc = RC_Timeout;
+ :: else -> dequeueMessage(qid,msg);
+ fi
+
+ :: else -> rc = RC_OK;
+ fi
+ fi
+ }
+}
+
+
+/*
+ * Model Processes
+ * We shall use four processes in this model.
+ * One will represent the RTEMS send task
+ * Two will represent the RTEMS receive tasks
+ * One will model a timer
+ */
+
+// These are not output to test generation
+#define SEND_ID 1
+#define RCV1_ID 2
+#define RCV2_ID 3
+
+/*
+ * Sender Scenario
+ */
+byte sendTarget;
+byte msize;
+bool sendAgain
+int totalSendCount
+int currSendCount
+/*
+ * Receiver Scenario
+ */
+
+/*
+ * Semaphore Setup
+ */
+int sendSema;
+int rcvSema1;
+int startSema;
+int rcvSema2;
+
+/*
+* Queue setup
+*
+*/
+bool queueCreated;
+int queueId;
+
+
+
+
+mtype = {Send,Receive,SndRcv, RcvSnd};
+mtype scenario;
+
+inline chooseScenario() {
+
+ sendAgain = false;
+ semaphore[0] = false;
+ semaphore[1] = false;
+ semaphore[2] = false;
+ sendSema = 0;
+ rcvSema1 = 1;
+ rcvSema2 = 2;
+ startSema = sendSema;
+ tasks[SEND_ID].doCreate = true;
+
+ //Queue parameters
+ queueCreated = false;
+ queueId = 1;
+
+ msize = MAX_MESSAGE_SIZE;
+ //set up defaults
+ tasks[SEND_ID].numSends = 1;
+ tasks[SEND_ID].sndMsg = 1;
+ tasks[SEND_ID].targetQueue = queueId;
+ tasks[RCV1_ID].targetQueue = queueId;
+ tasks[RCV2_ID].targetQueue = queueId;
+ tasks[SEND_ID].sndMsg = 1;
+ tasks[SEND_ID].msgSize = MAX_MESSAGE_SIZE;
+
+
+ //select scenario
+ if
+ :: scenario = Send;
+ :: scenario = Receive;
+ :: scenario = SndRcv;
+ :: scenario = RcvSnd;
+ fi
+
+ atomic{printf("@@@ %d LOG scenario ",_pid);
+ printm(scenario);
+ nl()};
+
+
+ if
+ :: scenario == Send ->
+ tasks[RCV1_ID].doReceive = false;
+ tasks[RCV2_ID].doReceive = false;
+ tasks[SEND_ID].doSend = true;
+ if
+ :: tasks[SEND_ID].targetQueue = 0;
+ printf("@@@ %d LOG sub-scenario Send Bad ID\n", _pid)
+ :: tasks[SEND_ID].targetQueue = queueId;
+ printf("@@@ %d LOG sub-scenario Send Success\n", _pid)
+ :: tasks[SEND_ID].msgSize = MAX_MESSAGE_SIZE + 1;
+ printf("@@@ %d LOG sub-scenario Send Size Error\n", _pid)
+ :: tasks[SEND_ID].sndMsg = 0;
+ printf("@@@ %d LOG sub-scenario Buffer Address Error\n", _pid)
+ :: tasks[SEND_ID].numSends = MAX_PENDING_MESSAGES + 1;
+ printf("@@@ %d LOG sub-scenario Too Many messages Error\n", _pid)
+ fi
+
+ :: scenario == Receive ->
+ tasks[SEND_ID].doSend = false;
+ tasks[RCV1_ID].doReceive = true;
+ tasks[RCV2_ID].doReceive = false;
+ startSema = rcvSema1;
+
+ if
+ :: tasks[RCV1_ID].doWait = false;
+ if
+ :: tasks[RCV1_ID].targetQueue = 0;
+ printf("@@@ %d LOG sub-scenario Rcv Bad ID No Wait\n", _pid)
+ :: tasks[SEND_ID].targetQueue = queueId;
+ printf("@@@ %d LOG sub-scenario Rcv Success No Wait\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+ fi
+ :: tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 5;
+ printf("@@@ %d LOG sub-scenario Rcv Success wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+ fi
+
+ /*
+ if
+ :: tasks[RCV2_ID].doWait = false;
+ :: tasks[RCV2_ID].doWait = true; tasks[RCV2_ID].rcvInterval = 5;
+ fi
+ printf("@@@ %d LOG sub-scenario Receive2 wait:%d interval:%d\n", _pid, tasks[RCV2_ID].doWait, tasks[RCV2_ID].rcvInterval)
+ */
+
+ :: scenario == SndRcv ->
+
+ if
+ :: tasks[SEND_ID].numSends = 2;
+ :: tasks[SEND_ID].numSends = 1;
+ fi
+ printf("@@@ %d LOG sub-scenario SndRcv numSends:%d\n",
+ _pid,
+ tasks[SEND_ID].numSends
+ )
+ /*
+ if
+ :: tasks[RCV1_ID].doWait = false;
+ :: tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 5;
+ fi
+ printf("@@@ %d LOG sub-scenario Receive1 wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+ if
+ :: tasks[RCV2_ID].doWait = false;
+ :: tasks[RCV2_ID].doWait = true; tasks[RCV2_ID].rcvInterval = 5;
+ fi
+ printf("@@@ %d LOG sub-scenario Receive2 wait:%d interval:%d\n", _pid, tasks[RCV2_ID].doWait, tasks[RCV2_ID].rcvInterval)
+ */
+
+ tasks[SEND_ID].doSend = true;
+ tasks[RCV1_ID].doReceive = true;
+ tasks[RCV2_ID].doReceive = true;
+
+ :: scenario == RcvSnd ->
+ startSema = rcvSema1;
+ tasks[SEND_ID].doSend = true;
+ tasks[RCV1_ID].doReceive = true;
+ tasks[RCV2_ID].doReceive = false;
+ tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 10;
+ //tasks[SEND_ID].numSends = 2
+ /*
+ if
+ :: tasks[RCV1_ID].doWait = false; tasks[RCV2_ID].doWait = false;
+ :: tasks[RCV1_ID].doWait = true; tasks[RCV2_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 10; tasks[RCV2_ID].rcvInterval = 10;
+ fi
+ printf("@@@ %d LOG sub-scenario RcvSnd wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+ */
+
+ fi
+}
+
+
+proctype Sender (byte taskid) {
+
+ tasks[taskid].pmlid = _pid;
+ tasks[taskid].state = Ready;
+ printf("@@@ %d TASK Runner\n",_pid,taskid);
+
+ if
+ :: (tasks[taskid].doCreate && !queueCreated) ->
+ printf("@@@ %d CALL message_queue_construct %d %d %d %d %d qrc\n", _pid,
+ taskid,
+ QUEUE_NAME,
+ MAX_PENDING_MESSAGES,
+ MAX_MESSAGE_SIZE,
+ queueId);
+ message_queue_create(QUEUE_NAME,
+ MAX_PENDING_MESSAGES,
+ MAX_MESSAGE_SIZE,
+ qrc);
+ printf("@@@ %d SCALAR qrc %d\n",_pid,qrc);
+ queueCreated = true;
+ Release(startSema);
+ fi
+
+ if
+ :: tasks[taskid].doSend ->
+ Obtain(sendSema);
+ repeat:
+ atomic{
+ printf("@@@ %d CALL message_queue_send %d %d %d %d sendrc\n",
+ _pid,
+ taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].sndMsg,
+ tasks[taskid].msgSize);
+ message_queue_send(taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].sndMsg,
+ tasks[taskid].msgSize,
+ sendrc);
+ printf("@@@ %d SCALAR sendrc %d\n",_pid,sendrc);
+ tasks[taskid].numSends-- ;
+ if
+ :: tasks[taskid].numSends != 0 -> tasks[SEND_ID].sndMsg++; goto repeat;
+ :: scenario == RcvSnd -> skip;
+ :: else -> Release(rcvSema1);
+ fi
+ }
+ :: else -> skip;
+ fi
+
+
+ //adjust semaphore behaviour for RcvSnd as Receive1 starts
+ if
+ :: scenario == RcvSnd ->
+ Obtain(rcvSema1);
+ Obtain(rcvSema2);
+ :: else ->
+ Obtain(sendSema);
+ Obtain(rcvSema2);
+ Obtain(rcvSema1);
+ fi
+
+ printf("@@@ %d LOG Sender %d finished\n",_pid,taskid);
+ tasks[taskid].state = Zombie;
+ printf("@@@ %d STATE %d Zombie\n",_pid,taskid);
+}
+
+proctype Receiver1 (byte taskid) {
+
+ tasks[taskid].pmlid = _pid;
+ tasks[taskid].state = Ready;
+ printf("@@@ %d TASK Worker1\n",_pid);
+
+
+ Obtain(rcvSema1);
+
+ if
+ :: tasks[taskid].doReceive && scenario != RcvSnd->
+ atomic{
+ printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+ _pid,taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].doWait,
+ tasks[taskid].rcvInterval);
+ message_queue_receive(taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].rcvMsg,
+ recrc);
+ printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+ printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+ Release(rcvSema2);
+ }
+ :: tasks[taskid].doReceive && scenario == RcvSnd->
+ atomic{
+ Release(sendSema);
+ printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+ _pid,
+ taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].doWait,
+ tasks[taskid].rcvInterval);
+ message_queue_receive(taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].rcvMsg,
+ recrc);
+ printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+ printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+ }
+ :: else -> Release(rcvSema2);
+ fi
+
+
+
+ atomic{
+ Release(rcvSema1);
+ printf("@@@ %d LOG Receiver1 %d finished\n",_pid,taskid);
+ tasks[taskid].state = Zombie;
+ printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+ }
+}
+
+proctype Receiver2 (byte taskid) {
+
+ tasks[taskid].pmlid = _pid;
+ tasks[taskid].state = Ready;
+ printf("@@@ %d TASK Worker2\n",_pid);
+
+ if
+ :: scenario == RcvSnd ->
+ goto rcvSkip;
+ :: else -> Obtain(rcvSema2);
+ fi
+
+
+ if
+ :: tasks[taskid].doReceive && scenario != RcvSnd->
+ atomic{
+ printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+ _pid,
+ taskid,
+ tasks[taskid].targetQueue,
+ tasks[taskid].doWait,
+ tasks[taskid].rcvInterval);
+ message_queue_receive(taskid,tasks[taskid].targetQueue,tasks[taskid].rcvMsg,recrc);
+ printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+ printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+ Release(sendSema);
+ }
+ :: tasks[taskid].doReceive && scenario == RcvSnd->
+ atomic{
+ printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+ _pid,
+ taskid,tasks[taskid].targetQueue,
+ tasks[taskid].doWait,
+ tasks[taskid].rcvInterval);
+ Release(sendSema);
+ message_queue_receive(taskid,tasks[taskid].targetQueue,tasks[taskid].rcvMsg,recrc);
+ printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+ printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+ }
+ :: else -> Release(sendSema);
+ fi
+
+ rcvSkip:
+ atomic{
+ Release(rcvSema2);
+ printf("@@@ %d LOG Receiver2 %d finished\n",_pid,taskid);
+ tasks[taskid].state = Zombie;
+ printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+ }
+}
+
+
+/*
+ * 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.
+ */
+
+bool stopclock = false;
+
+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 STATE %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 STATE %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("Message Manager Model running.\n");
+ printf("Setup...\n");
+
+ printf("@@@ %d NAME Message_Manager_TestGen\n",_pid)
+ //#define required in test file
+ outputDefines();
+ //Structures and data types required in test file
+ outputDeclarations();
+
+ printf("@@@ %d INIT\n",_pid);
+ chooseScenario();
+
+ printf("Run...\n");
+ //start nececssary processes
+ run System();
+ run Clock();
+
+ run Sender(SEND_ID);
+ run Receiver1(RCV1_ID);
+ run Receiver2(RCV2_ID);
+
+ _nr_pr == 1;
+
+#ifdef TEST_GEN
+ assert(false);
+#endif
+
+
+printf("Message Manager Model finished !\n")
+}
\ No newline at end of file
diff --git a/formal/promela/models/messages/tc-msg-mgr-model.c b/formal/promela/models/messages/tc-msg-mgr-model.c
new file mode 100644
index 00000000..cb3176f1
--- /dev/null
+++ b/formal/promela/models/messages/tc-msg-mgr-model.c
@@ -0,0 +1,211 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsMessageVal
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *
+ * 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/eventimpl.h>
+#include <rtems/rtems/tasksdata.h>
+#include <rtems/score/statesimpl.h>
+#include <rtems/score/threadimpl.h>
+
+#include "tr-msg-mgr-model.h"
+
+#include <rtems/test.h>
+
+
+
+/**
+ * @defgroup RTEMSTestCaseRtemsMessageVal
+ *
+ * @ingroup RTEMSTestSuiteTestsuitesValidation0
+ *
+ * @brief Tests the rtems_message_queue_create, rtems_message_queue_send,
+ * rtems_message_queue_recieve, rtems_message_queue_delete, rtems_message_queue_ident
+ *
+ * This test case performs the following actions:
+ *
+ * - Runs tests for message manager
+ *
+ * @{
+ */
+
+/**
+ * @fn void T_case_body_RtemsMessageVal( void )
+ */
+
+T_TEST_CASE( RtemsModelMessageMgr0 )
+{
+ RtemsModelMessageMgr_Run0();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr1 )
+{
+ RtemsModelMessageMgr_Run1();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr2 )
+{
+ RtemsModelMessageMgr_Run2();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr3 )
+{
+ RtemsModelMessageMgr_Run3();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr4 )
+{
+ RtemsModelMessageMgr_Run4();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr5 )
+{
+ RtemsModelMessageMgr_Run5();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr6 )
+{
+ RtemsModelMessageMgr_Run6();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr7 )
+{
+ RtemsModelMessageMgr_Run7();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr8 )
+{
+ RtemsModelMessageMgr_Run8();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr9 )
+{
+ RtemsModelMessageMgr_Run9();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr10 )
+{
+ RtemsModelMessageMgr_Run10();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr11 )
+{
+ RtemsModelMessageMgr_Run11();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr12 )
+{
+ RtemsModelMessageMgr_Run12();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr13 )
+{
+ RtemsModelMessageMgr_Run13();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr14 )
+{
+ RtemsModelMessageMgr_Run14();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr15 )
+{
+ RtemsModelMessageMgr_Run15();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr16 )
+{
+ RtemsModelMessageMgr_Run16();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr17 )
+{
+ RtemsModelMessageMgr_Run17();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr18 )
+{
+ RtemsModelMessageMgr_Run18();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr19 )
+{
+ RtemsModelMessageMgr_Run19();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr20 )
+{
+ RtemsModelMessageMgr_Run20();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr21 )
+{
+ RtemsModelMessageMgr_Run21();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr22 )
+{
+ RtemsModelMessageMgr_Run22();
+}
+/*
+T_TEST_CASE( RtemsModelMessageMgr23 )
+{
+ RtemsModelMessageMgr_Run23();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr24 )
+{
+ RtemsModelMessageMgr_Run24();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr25 )
+{
+ RtemsModelMessageMgr_Run25();
+}
+*/
\ No newline at end of file
diff --git a/formal/promela/models/messages/tr-msg-mgr-model.c b/formal/promela/models/messages/tr-msg-mgr-model.c
new file mode 100644
index 00000000..79562e9b
--- /dev/null
+++ b/formal/promela/models/messages/tr-msg-mgr-model.c
@@ -0,0 +1,240 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelMsgMgr
+ */
+
+/*
+ * Copyright (C) 2020 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-msg-mgr-model.h"
+
+static const char PromelaModelMessageMgr[] = "/PML-MessageMgr";
+
+rtems_id CreateWakeupSema( void )
+{
+ rtems_status_code sc;
+ rtems_id id;
+
+ sc = rtems_semaphore_create(
+ rtems_build_name( 'W', 'K', 'U', 'P' ),
+ 0,
+ RTEMS_SIMPLE_BINARY_SEMAPHORE,
+ 0,
+ &id
+ );
+ T_assert_rsc_success( sc );
+
+ return id;
+}
+
+void DeleteWakeupSema( rtems_id id )
+{
+ if ( id != 0 ) {
+ rtems_status_code sc;
+
+ sc = rtems_semaphore_delete( id );
+ T_rsc_success( sc );
+ }
+}
+
+void Wait( rtems_id id )
+{
+ rtems_status_code sc;
+
+ sc = rtems_semaphore_obtain( id, RTEMS_WAIT, RTEMS_NO_TIMEOUT );
+ T_quiet_rsc_success( sc );
+}
+
+void Wakeup( rtems_id id )
+{
+ rtems_status_code sc;
+
+ sc = rtems_semaphore_release( id );
+ T_quiet_rsc_success( sc );
+}
+
+rtems_option mergeopts( bool wait )
+{
+ rtems_option opts;
+
+ if ( wait ) { opts = RTEMS_WAIT; }
+ else { opts = RTEMS_NO_WAIT; } ;
+ return opts;
+}
+
+rtems_interval getTimeout( int timeout )
+{
+ rtems_interval tout;
+
+ if ( timeout == 0 ) { tout = RTEMS_NO_TIMEOUT; }
+ else { tout = timeout; } ;
+ return tout;
+}
+
+rtems_id idNull( Context *ctx, bool passedid )
+{
+ rtems_id id;
+
+ if ( passedid ) { return ctx->queue_id; }
+ else { return NULL; }
+}
+
+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_pending( rtems_event_set pending[], int max )
+{
+ int i;
+
+ for( i=0; i < max; i++ ) {
+ pending[i] = 0;
+ }
+}
+
+void initialise_semaphore( Context *ctx, rtems_id semaphore[] )
+{
+ semaphore[0] = ctx->runner_wakeup;
+ semaphore[1] = ctx->worker1_wakeup;
+ semaphore[2] = ctx->worker2_wakeup;
+}
+
+void ShowWorkerSemaId( Context *ctx ) {
+ T_printf( "L:ctx->worker1_wakeup = %d\n", ctx->worker1_wakeup );
+ T_printf( "L:ctx->worker2_wakeup = %d\n", ctx->worker2_wakeup );
+}
+
+void ShowRunnerSemaId( Context *ctx ) {
+ T_printf( "L:ctx->runner_wakeup = %d\n", ctx->runner_wakeup );
+}
+
+static void RtemsModelMessageMgr_Teardown(
+ RtemsModelMessageMgr_Context *ctx
+)
+{
+ rtems_status_code sc;
+ rtems_task_priority prio;
+
+ T_log( T_NORMAL, "Runner Teardown" );
+
+ prio = 0;
+ sc = rtems_task_set_priority( RTEMS_SELF, PRIO_HIGH, &prio );
+ T_rsc_success( sc );
+ T_eq_u32( prio, PRIO_NORMAL );
+
+ if ( ctx->worker1_id != 0 ) {
+ T_printf( "L:Deleting Task id : %d\n", ctx->worker1_id );
+ sc = rtems_task_delete( ctx->worker1_id );
+ T_rsc_success( sc );
+ }
+
+ T_log( T_NORMAL, "Deleting Worker1 Wakeup Semaphore" );
+ DeleteWakeupSema( ctx->worker1_wakeup );
+
+
+ if ( ctx->worker2_id != 0 ) {
+ T_printf( "L:Deleting Task id : %d\n", ctx->worker2_id );
+ sc = rtems_task_delete( ctx->worker2_id );
+ T_rsc_success( sc );
+ }
+
+ T_log( T_NORMAL, "Deleting Worker2 Wakeup Semaphore" );
+ DeleteWakeupSema( ctx->worker2_wakeup );
+
+ T_log( T_NORMAL, "Deleting Runner Wakeup Semaphore" );
+ DeleteWakeupSema( ctx->runner_wakeup );
+}
+
+void RtemsModelMessageMgr_Teardown_Wrap( void *arg )
+{
+ RtemsModelMessageMgr_Context *ctx;
+
+ ctx = arg;
+ RtemsModelMessageMgr_Teardown( ctx );
+}
+
+
+size_t RtemsModelMessageMgr_Scope( void *arg, char *buf, size_t n )
+{
+ RtemsModelMessageMgr_Context *ctx;
+ size_t m;
+ int p10;
+ int tnum ;
+ char digit;
+
+ ctx = arg;
+ p10 = POWER_OF_10;
+
+ m = T_str_copy(buf, PromelaModelMessageMgr, 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 RtemsModelMessageMgr_Cleanup(
+ RtemsModelMessageMgr_Context *ctx
+)
+{
+ rtems_status_code status;
+
+ if (ctx->queue_id != 0){
+ status = rtems_message_queue_delete(ctx->queue_id);
+ if (status != RTEMS_SUCCESSFUL) { T_quiet_rsc( status, RTEMS_INVALID_ID ); }
+ else { T_rsc_success( status ); }
+ ctx->queue_id = RTEMS_ID_NONE;
+ }
+}
diff --git a/formal/promela/models/messages/tr-msg-mgr-model.h b/formal/promela/models/messages/tr-msg-mgr-model.h
new file mode 100644
index 00000000..9af14bd8
--- /dev/null
+++ b/formal/promela/models/messages/tr-msg-mgr-model.h
@@ -0,0 +1,132 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+#ifndef _TR_MODEL_EVENTS_MGR_H
+#define _TR_MODEL_EVENTS_MGR_H
+
+#include <rtems.h>
+#include <rtems/score/thread.h>
+
+#include <rtems/test.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
+ rtems_id receiver_id; // receiver ID used for the event send action.
+ rtems_status_code send_status; // status of the message send action.
+ rtems_option receive_option_set; // option set used for the message receive action
+ rtems_interval receive_timeout; // timeout used for the message receive action
+ rtems_status_code receive_status; // status of the message receive action
+ rtems_status_code create; //status of the messsge queue create action
+ rtems_attribute msg_queue_attr;
+
+ rtems_id queue_id;
+ uint8_t send_msg_counter;
+ size_t receive_size; //size of messages recieved by receive
+
+ Thread_Control *runner_thread; // TCB of the runner task
+ rtems_id runner_id; // ID of the runner task
+ rtems_id worker1_id; // task ID of the worker task
+ rtems_id worker2_id;
+ rtems_id worker1_wakeup; // ID of the semaphore used to wake up the worker task
+ rtems_id worker2_wakeup;
+ rtems_id runner_wakeup; // ID of the semaphore used to wake up the runner task
+ 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
+} RtemsModelMessageMgr_Context;
+
+typedef enum {
+ PRIO_HIGH = 1,
+ PRIO_NORMAL,
+ PRIO_LOW,
+ PRIO_OTHER
+} Priorities;
+
+#define POWER_OF_10 100
+
+#define WORKER_ATTRIBUTES RTEMS_DEFAULT_ATTRIBUTES
+
+#define MAX_TLS_SIZE RTEMS_ALIGN_UP( 64, RTEMS_TASK_STORAGE_ALIGNMENT )
+
+typedef RtemsModelMessageMgr_Context Context;
+
+rtems_id CreateWakeupSema( void );
+
+void DeleteWakeupSema( rtems_id id );
+
+void Wait( rtems_id id );
+
+void Wakeup( rtems_id id ) ;
+
+rtems_event_set GetPending( Context *ctx );
+
+rtems_option mergeopts( bool wait );
+
+rtems_interval getTimeout( int timeout ) ;
+
+rtems_id idNull( Context *ctx, bool passedid ) ;
+
+rtems_id mapid( Context *ctx, int pid ) ;
+
+void checkTaskIs( rtems_id expected_id ) ;
+
+void ShowWorkerSemaId( Context *ctx ) ;
+
+void ShowRunnerSemaId( Context *ctx ) ;
+
+void initialise_semaphore( Context *ctx, rtems_id semaphore[] );
+
+void RtemsModelMessageMgr_Setup_Wrap( void *arg ) ;
+
+
+void RtemsModelMessageMgr_Teardown_Wrap( void *arg ) ;
+
+size_t RtemsModelMessageMgr_Scope( void *arg, char *buf, size_t n ) ;
+
+void RtemsModelMessageMgr_Cleanup( RtemsModelMessageMgr_Context *ctx );
+
+
+/**
+ * @addtogroup RTEMSTestCaseRtemsModelMessageMgr_Run
+ *
+ * @{
+ */
+
+/**
+ * @brief Runs the parameterized test case.
+ *
+ */
+
+void RtemsModelMessageMgr_Run0(void);
+
+void RtemsModelMessageMgr_Run1(void);
+
+void RtemsModelMessageMgr_Run2(void);
+
+void RtemsModelMessageMgr_Run3(void);
+
+void RtemsModelMessageMgr_Run4(void);
+
+void RtemsModelMessageMgr_Run5(void);
+
+void RtemsModelMessageMgr_Run6(void);
+
+void RtemsModelMessageMgr_Run7(void);
+
+void RtemsModelMessageMgr_Run8(void);
+
+/** @} */
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* _TR_EVENT_SEND_RECEIVE_H */
--
2.37.1 (Apple Git-137.1)
More information about the devel
mailing list