[rtems-central commit] spec: Specify priority ceiling violation

Sebastian Huber sebh at rtems.org
Thu Aug 12 14:14:28 UTC 2021


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

Author:    Sebastian Huber <sebastian.huber at embedded-brains.de>
Date:      Thu Aug 12 15:17:00 2021 +0200

spec: Specify priority ceiling violation

---

 spec/score/mtx/req/seize-try.yml  |  24 +++----
 spec/score/mtx/req/seize-wait.yml | 140 +++++++++++++++++++++++++++++++-------
 2 files changed, 126 insertions(+), 38 deletions(-)

diff --git a/spec/score/mtx/req/seize-try.yml b/spec/score/mtx/req/seize-try.yml
index 4ef805f..7e1f04f 100644
--- a/spec/score/mtx/req/seize-try.yml
+++ b/spec/score/mtx/req/seize-try.yml
@@ -147,24 +147,24 @@ pre-conditions:
   test-prologue: null
 - name: Priority
   states:
-  - name: Higher
+  - name: LT
     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
+      a ${/glossary/priority-current:/term} less than the priority ceiling.
+  - name: EQ
     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
+  - name: GT
     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.
+      a ${/glossary/priority-current:/term} greater than the priority ceiling.
   test-epilogue: null
   test-prologue: null
 rationale: null
@@ -173,7 +173,7 @@ requirement-type: functional
 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.
+    have a ${/glossary/priority-current:/term} greater than the priority ceiling.
 test-action: |
   rtems_task_priority priority;
 
@@ -316,8 +316,8 @@ transition-map:
     Owner:
     - 'No'
     Priority:
-    - Equal
-    - Lower
+    - EQ
+    - GT
 - enabled-by: true
   post-conditions:
     Status: OkOrMutexCeilingViolated
@@ -327,7 +327,7 @@ transition-map:
     Owner:
     - 'No'
     Priority:
-    - Higher
+    - LT
 - enabled-by: true
   post-conditions:
     Status: Recursive
@@ -337,8 +337,8 @@ transition-map:
     Owner:
     - Caller
     Priority:
-    - Higher
-    - Equal
+    - LT
+    - EQ
 - enabled-by: true
   post-conditions:
     Status: Unsat
@@ -354,5 +354,5 @@ transition-map:
     Owner:
     - Caller
     Priority:
-    - Lower
+    - GT
 type: requirement
diff --git a/spec/score/mtx/req/seize-wait.yml b/spec/score/mtx/req/seize-wait.yml
index 8de6df6..53dd245 100644
--- a/spec/score/mtx/req/seize-wait.yml
+++ b/spec/score/mtx/req/seize-wait.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 ) {
@@ -83,25 +99,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
@@ -134,9 +161,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
@@ -151,10 +178,35 @@ pre-conditions:
       While the attempt to seize the mutex results in a deadlock.
   test-epilogue: null
   test-prologue: null
+- name: Priority
+  states:
+  - name: LT
+    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} less than the priority ceiling.
+  - name: EQ
+    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: GT
+    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.
+  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} greater than the priority ceiling.
 test-action: |
   if ( !ctx->deadlock ) {
     NonDeadlockAction( ctx );
@@ -167,7 +219,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.
@@ -229,7 +281,7 @@ test-prepare: |
   ctx->tq_ctx->base.enqueue_prepare = TQEnqueuePrepareClassicSem;
   ctx->tq_ctx->base.enqueue_done = TQSurrenderClassicSem;
   ctx->tq_ctx->base.get_properties = GetProperties;
-  ctx->owner_self = false;
+  ctx->owner_caller = false;
   ctx->owner_other = false;
   ctx->deadlock = false;
 test-setup: null
@@ -266,7 +318,11 @@ test-support: |
 
   static void NonDeadlockAction( Context *ctx )
   {
-    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 );
@@ -290,12 +346,17 @@ test-support: |
       }
     }
 
-    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 ) {
@@ -315,6 +376,8 @@ test-support: |
         TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
       }
     }
+
+    SetSelfPriority( priority );
   }
 test-target: testsuites/validation/tr-mtx-seize-wait.c
 test-teardown: null
@@ -324,27 +387,44 @@ transition-map:
 - enabled-by: true
   post-conditions:
     Status: Ok
-    Owner: New
+    Owner: Caller
     Priority: Ceiling
   pre-conditions:
     Owner:
     - 'No'
+    Priority:
+    - EQ
+    - GT
+- enabled-by: true
+  post-conditions:
+    Status: OkOrMutexCeilingViolated
+    Owner: CallerOrNoOwner
+    Priority: Nop
+  pre-conditions:
+    Owner:
+    - 'No'
+    Priority:
+    - LT
 - enabled-by: true
   post-conditions:
     Status: Recursive
-    Owner: Nop
+    Owner: Caller
     Priority: Nop
   pre-conditions:
     Owner:
-    - Self
+    - Caller
+    Priority:
+    - LT
+    - EQ
 - enabled-by: true
   post-conditions:
     Status: Enqueued
-    Owner: Nop
+    Owner: Other
     Priority: Nop
   pre-conditions:
     Owner:
     - Other
+    Priority: all
 - enabled-by: true
   post-conditions:
     Status: Deadlock
@@ -353,4 +433,12 @@ transition-map:
   pre-conditions:
     Owner:
     - Deadlock
+    Priority: all
+- enabled-by: true
+  post-conditions: CeilingOwner
+  pre-conditions:
+    Owner:
+    - Caller
+    Priority:
+    - GT
 type: requirement



More information about the vc mailing list