[rtems-central commit] spec: Specify bad sticky thread queue enqueue

[Sebastian Huber]

Module:    rtems-central
Branch:    master
Commit:    e7c122cc25df3629f8c1f35d07cc343f206ee6ac
Changeset: http://git.rtems.org/rtems-central/commit/?id=e7c122cc25df3629f8c1f35d07cc343f206ee6ac

Author:    Sebastian Huber <sebastian.huber at embedded-brains.de>
Date:      Wed Sep  8 08:27:37 2021 +0200

spec: Specify bad sticky thread queue enqueue

---

 spec/rtems/sem/val/smp.yml                         | 120 +++++++++++++++++++++
 .../thread-queue-enqueue-sticky-from-bad-state.yml |  13 +++
 .../tq/req/fatal-enqueue-sticky-from-bad-state.yml |  18 ++++
 3 files changed, 151 insertions(+)

diff --git a/spec/rtems/sem/val/smp.yml b/spec/rtems/sem/val/smp.yml
new file mode 100644
index 0000000..a23f850
--- /dev/null
+++ b/spec/rtems/sem/val/smp.yml
@@ -0,0 +1,120 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: RTEMS_SMP
+links: []
+test-actions:
+- action-brief: |
+    Create a worker thread and a MrsP mutex.  Use the mutex and the worker to
+    perform a bad sticky thread queue enqueue.
+  action-code: |
+    rtems_status_code sc;
+    rtems_id          worker_id;
+    rtems_id          scheduler_b_id;
+
+    ctx->done = false;
+
+    sc = rtems_scheduler_ident( TEST_SCHEDULER_B_NAME, &scheduler_b_id );
+    T_rsc_success( sc );
+
+    sc = rtems_semaphore_create(
+      rtems_build_name( 'M', 'U', 'T', 'X' ),
+      1,
+      RTEMS_BINARY_SEMAPHORE | RTEMS_PRIORITY |
+        RTEMS_MULTIPROCESSOR_RESOURCE_SHARING,
+      PRIO_HIGH,
+      &ctx->mutex_id
+    );
+    T_rsc_success( sc );
+
+    worker_id = CreateTask( "WORK", PRIO_NORMAL );
+    SetScheduler( worker_id, scheduler_b_id, PRIO_NORMAL );
+
+    ObtainMutex( ctx->mutex_id );
+    SetFatalExtension( BadEnqueueFatal );
+    StartTask( worker_id, BadEnqueueTask, ctx );
+
+    while ( !ctx->done ) {
+      /* Wait */
+    }
+
+    DeleteTask( worker_id );
+    ReleaseMutex( ctx->mutex_id );
+    DeleteMutex( ctx->mutex_id );
+  checks: []
+  links:
+  - role: validation
+    uid: /score/tq/req/fatal-enqueue-sticky-from-bad-state
+test-brief: |
+  Tests SMP-specific semaphore behaviour.
+test-context:
+- brief: |
+    This member contains the mutex identifier.
+  description: null
+  member: |
+    rtems_id mutex_id;
+- brief: |
+    If this member is true, then the worker is done.
+  description: null
+  member: |
+    volatile bool done
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+- rtems/score/threaddispatch.h
+test-local-includes:
+- ts-config.h
+- tx-support.h
+test-setup:
+  brief: null
+  code: |
+    SetSelfPriority( PRIO_NORMAL );
+  description: null
+test-stop: null
+test-support: |
+  typedef ${.:/test-context-type} Context;
+
+  static void BadEnqueueFatal(
+    rtems_fatal_source source,
+    bool               always_set_to_false,
+    rtems_fatal_code   code
+  )
+  {
+    Per_CPU_Control *cpu_self;
+    Context         *ctx;
+
+    T_eq_int( source, INTERNAL_ERROR_CORE );
+    T_false( always_set_to_false );
+    T_eq_ulong(
+      code,
+      INTERNAL_ERROR_THREAD_QUEUE_ENQUEUE_STICKY_FROM_BAD_STATE
+    );
+
+    SetFatalExtension( NULL );
+
+    cpu_self = _Per_CPU_Get();
+    _Thread_Dispatch_unnest( cpu_self );
+    _Thread_Dispatch_unnest( cpu_self );
+
+    ctx = T_fixture_context();
+    ctx->done = true;
+    SuspendSelf();
+  }
+
+  static void BadEnqueueTask( rtems_task_argument arg )
+  {
+    Context *ctx;
+
+    ctx = (Context *) arg;
+    (void) _Thread_Dispatch_disable();
+    ObtainMutex( ctx->mutex_id );
+  }
+test-target: testsuites/validation/tc-sem-smp.c
+test-teardown:
+  brief: null
+  code: |
+    RestoreRunnerPriority();
+  description: null
+type: test-case
diff --git a/spec/score/interr/if/thread-queue-enqueue-sticky-from-bad-state.yml b/spec/score/interr/if/thread-queue-enqueue-sticky-from-bad-state.yml
new file mode 100644
index 0000000..9ffe116
--- /dev/null
+++ b/spec/score/interr/if/thread-queue-enqueue-sticky-from-bad-state.yml
@@ -0,0 +1,13 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+index-entries: []
+interface-type: unspecified-define
+links:
+- role: interface-placement
+  uid: header
+name: INTERNAL_ERROR_THREAD_QUEUE_ENQUEUE_STICKY_FROM_BAD_STATE
+references:
+  c-user: internal_errors
+type: interface
diff --git a/spec/score/tq/req/fatal-enqueue-sticky-from-bad-state.yml b/spec/score/tq/req/fatal-enqueue-sticky-from-bad-state.yml
new file mode 100644
index 0000000..2154ece
--- /dev/null
+++ b/spec/score/tq/req/fatal-enqueue-sticky-from-bad-state.yml
@@ -0,0 +1,18 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: RTEMS_SMP
+links:
+- role: requirement-refinement
+  uid: /req/fatal-error
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  While no deadlock was detected in a sticky thread queue enqueue, while the
+  thread dispatch disable level is not equal to one, if the sticky thread queue
+  enqueue is performed, then the system shall terminate with the
+  ${/score/interr/if/internal-error-core:/name} fatal source and the
+  ${/score/interr/if/thread-queue-enqueue-sticky-from-bad-state} fatal code.
+type: requirement