spec: Specify priority ceiling violation

2 files changed, 125 insertions, 26 deletions

diff --git a/spec/score/mtx/req/seize-try.yml b/spec/score/mtx/req/seize-try.yml
index aaee66a3..4ef805fa 100644
--- a/spec/score/mtx/req/seize-try.yml
+++ b/spec/score/mtx/req/seize-try.yml
@@ -16,6 +16,22 @@ post-conditions:
     text: |
       The return status of the directive call shall be derived from
       ${../../status/if/successful:/name}.
+  - name: OkOrMutexCeilingViolated
+    test-code: |
+      if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
+        T_eq_int( ctx->status, Status( ctx, STATUS_MUTEX_CEILING_VIOLATED ) );
+      } else {
+        T_eq_int( ctx->status, Status( ctx, STATUS_SUCCESSFUL ) );
+        TQSurrender( &ctx->tq_ctx->base );
+      }
+    text: |
+      Where the mutex provides a priority ceiling, the return status of the
+      directive call shall be derived from
+      ${../../status/if/mutex-ceiling-violated:/name}.
+
+      Where the mutex does not provide a priority ceiling, the return status of
+      the directive call shall be derived from
+      ${../../status/if/successful:/name}.
   - name: Recursive
     test-code: |
       switch ( ctx->tq_ctx->recursive ) {
@@ -55,25 +71,36 @@ post-conditions:
   test-prologue: null
 - name: Owner
   states:
-  - name: Nop
+  - name: Other
     test-code: |
-      if ( ctx->owner_self ) {
-        T_eq_ptr( ctx->owner_after, ctx->tq_ctx->base.runner_tcb );
-      } else if ( ctx->owner_other ) {
-        T_eq_ptr(
-          ctx->owner_after,
-          ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
-        );
-      } else {
-        T_null( ctx->owner_after );
-      }
+      T_eq_ptr(
+        ctx->owner_after,
+        ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
+      );
+    text: |
+      The owner of the mutex shall not be modified.
+  - name: Caller
+    test-code: |
+      T_eq_ptr( ctx->owner_after, ctx->tq_ctx->base.runner_tcb );
     text: |
-      The owner of the semaphore shall not be modified.
-  - name: New
+      The owner of the mutex shall be the calling thread.
+  - name: CallerOrNoOwner
     test-code: |
       T_eq_ptr( ctx->owner_after, ctx->tq_ctx->base.runner_tcb );
     text: |
-      The owner of the semaphore shall be the calling thread.
+      The owner of the mutex shall be the calling thread.
+    test-code: |
+      if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
+        T_null( ctx->owner_after );
+      } else {
+        T_eq_ptr( ctx->owner_after, ctx->tq_ctx->base.runner_tcb );
+      }
+    text: |
+      Where the mutex provides a priority ceiling, the mutex shall have no
+      owner.
+
+      Where the mutex does not provide a priority ceiling, the owner of the
+      mutex shall be the calling thread.
   test-epilogue: null
   test-prologue: null
 - name: Priority
@@ -106,9 +133,9 @@ pre-conditions:
       /* This is the default */
     text: |
       While the mutex has no owner.
-  - name: Self
+  - name: Caller
     test-code: |
-      ctx->owner_self = true;
+      ctx->owner_caller = true;
     text: |
       While the owner of the mutex is the calling thread.
   - name: Other
@@ -118,12 +145,41 @@ pre-conditions:
       While the owner of the mutex is a thread other than the calling thread.
   test-epilogue: null
   test-prologue: null
+- name: Priority
+  states:
+  - name: Higher
+    test-code: |
+      ctx->priority_before = ctx->tq_ctx->priority_ceiling - 1;
+    text: |
+      Where the mutex provides a priority ceiling, while the calling thread has
+      a ${/glossary/priority-current:/term} greater than the priority ceiling.
+  - name: Equal
+    test-code: |
+      ctx->priority_before = ctx->tq_ctx->priority_ceiling;
+    text: |
+      Where the mutex provides a priority ceiling, while the calling thread has
+      a ${/glossary/priority-current:/term} equal to the priority ceiling.
+  - name: Lower
+    test-code: |
+      ctx->priority_before = ctx->tq_ctx->priority_ceiling + 1;
+    text: |
+      Where the mutex provides a priority ceiling, while the calling thread has
+      a ${/glossary/priority-current:/term} lower than the priority ceiling.
+  test-epilogue: null
+  test-prologue: null
 rationale: null
 references: []
 requirement-type: functional
-skip-reasons: {}
+skip-reasons:
+  CeilingOwner: |
+    Where the mutex provides a priority ceiling, the owner of the mutex cannot
+    have a ${/glossary/priority-current:/term} lower than the priority ceiling.
 test-action: |
-  if ( ctx->owner_self ) {
+  rtems_task_priority priority;
+
+  priority = GetSelfPriority();
+
+  if ( ctx->owner_caller ) {
     Status_Control status;
 
     status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
@@ -147,12 +203,17 @@ test-action: |
     }
   }
 
-  ctx->priority_before = GetSelfPriority();
+  if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
+    SetSelfPriority( ctx->priority_before );
+  } else {
+    ctx->priority_before = GetSelfPriority();
+  }
+
   ctx->status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
   ctx->owner_after = TQMtxGetOwner( ctx->tq_ctx );
   ctx->priority_after = GetSelfPriority();
 
-  if ( ctx->owner_self ) {
+  if ( ctx->owner_caller ) {
     TQSurrender( &ctx->tq_ctx->base );
   } else if ( ctx->owner_other ) {
     if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
@@ -172,6 +233,8 @@ test-action: |
       TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
     }
   }
+
+  SetSelfPriority( priority );
 test-brief: null
 test-cleanup: null
 test-context:
@@ -180,7 +243,7 @@ test-context:
     mutex.
   description: null
   member: |
-    bool owner_self;
+    bool owner_caller;
 - brief: |
     If this member is true, then a thread other than the calling thread shall
     be the owner of the mutex.
@@ -228,7 +291,7 @@ test-includes: []
 test-local-includes:
 - tr-mtx-seize-try.h
 test-prepare: |
-  ctx->owner_self = false;
+  ctx->owner_caller = false;
   ctx->owner_other = false;
 test-setup: null
 test-stop: null
@@ -247,25 +310,49 @@ transition-map:
 - enabled-by: true
   post-conditions:
     Status: Ok
-    Owner: New
+    Owner: Caller
     Priority: Ceiling
   pre-conditions:
     Owner:
     - 'No'
+    Priority:
+    - Equal
+    - Lower
+- enabled-by: true
+  post-conditions:
+    Status: OkOrMutexCeilingViolated
+    Owner: CallerOrNoOwner
+    Priority: Nop
+  pre-conditions:
+    Owner:
+    - 'No'
+    Priority:
+    - Higher
 - enabled-by: true
   post-conditions:
     Status: Recursive
-    Owner: Nop
+    Owner: Caller
     Priority: Nop
   pre-conditions:
     Owner:
-    - Self
+    - Caller
+    Priority:
+    - Higher
+    - Equal
 - enabled-by: true
   post-conditions:
     Status: Unsat
-    Owner: Nop
+    Owner: Other
     Priority: Nop
   pre-conditions:
     Owner:
     - Other
+    Priority: all
+- enabled-by: true
+  post-conditions: CeilingOwner
+  pre-conditions:
+    Owner:
+    - Caller
+    Priority:
+    - Lower
 type: requirement
diff --git a/spec/score/status/if/mutex-ceiling-violated.yml b/spec/score/status/if/mutex-ceiling-violated.yml
new file mode 100644
index 00000000..2b4a2e8f
--- /dev/null
+++ b/spec/score/status/if/mutex-ceiling-violated.yml
@@ -0,0 +1,12 @@
+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
+links:
+- role: interface-placement
+  uid: header
+name: STATUS_MUTEX_CEILING_VIOLATED
+references: {}
+type: interface