[rtems-central commit] spec: Improve mutex seize wait

Sebastian Huber sebh at rtems.org
Wed Sep 29 12:18:09 UTC 2021


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

Author:    Sebastian Huber <sebastian.huber at embedded-brains.de>
Date:      Tue Sep 28 18:09:50 2021 +0200

spec: Improve mutex seize wait

---

 spec/rtems/sem/req/obtain.yml     | 40 ++++++++++++++++++++++----
 spec/score/mtx/req/seize-wait.yml | 59 +++++++++++++++++++++++++--------------
 2 files changed, 72 insertions(+), 27 deletions(-)

diff --git a/spec/rtems/sem/req/obtain.yml b/spec/rtems/sem/req/obtain.yml
index c01ae3c..8828d17 100644
--- a/spec/rtems/sem/req/obtain.yml
+++ b/spec/rtems/sem/req/obtain.yml
@@ -43,26 +43,51 @@ post-conditions:
   - name: MtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_NO_PROTOCOL;
       ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_INVALID;
       ${/score/mtx/req/seize-try:/test-run}( &ctx->tq_mtx_ctx );
     text: |
       The calling task shall try to seize the mutex as specified by
-      ${/score/mtx/req/seize-try} where an enqueue blocks and a recursive seize
-      is allowed.
+      ${/score/mtx/req/seize-try} where an enqueue blocks, a recursive seize is
+      allowed, and no locking protocol is used.
   - name: MtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_NO_PROTOCOL;
+      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
+      ctx->tq_mtx_ctx.priority_ceiling = PRIO_INVALID;
+      ${/score/mtx/req/seize-wait:/test-run}( &ctx->tq_mtx_ctx );
+    text: |
+      The calling task shall wait to seize the mutex as specified by
+      ${/score/mtx/req/seize-wait} where an enqueue blocks, a recursive seize
+      is allowed, and no locking protocol is used.
+  - name: InheritMtxSeizeTry
+    test-code: |
+      ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_NO_PROTOCOL;
+      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
+      ctx->tq_mtx_ctx.priority_ceiling = PRIO_INVALID;
+      ${/score/mtx/req/seize-try:/test-run}( &ctx->tq_mtx_ctx );
+    text: |
+      The calling task shall try to seize the mutex as specified by
+      ${/score/mtx/req/seize-try} where an enqueue blocks, a recursive seize is
+      allowed, and a priority inheritance protocol is used.
+  - name: InheritMtxSeizeWait
+    test-code: |
+      ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_NO_PROTOCOL;
       ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_INVALID;
       ${/score/mtx/req/seize-wait:/test-run}( &ctx->tq_mtx_ctx );
     text: |
       The calling task shall wait to seize the mutex as specified by
-      ${/score/mtx/req/seize-wait} where an enqueue blocks and a recursive
-      seize is allowed.
+      ${/score/mtx/req/seize-wait} where an enqueue blocks, a recursive seize
+      is allowed, and a priority inheritance protocol is used.
   - name: CeilingMtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_PRIORITY_CEILING;
       ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_VERY_HIGH;
       ${/score/mtx/req/seize-try:/test-run}( &ctx->tq_mtx_ctx );
@@ -73,6 +98,7 @@ post-conditions:
   - name: CeilingMtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_PRIORITY_CEILING;
       ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_VERY_HIGH;
       ${/score/mtx/req/seize-wait:/test-run}( &ctx->tq_mtx_ctx );
@@ -83,6 +109,7 @@ post-conditions:
   - name: MrsPMtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_STICKY;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_MRSP;
       ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_DEADLOCK;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_VERY_HIGH;
       ${/score/mtx/req/seize-try:/test-run}( &ctx->tq_mtx_ctx );
@@ -93,6 +120,7 @@ post-conditions:
   - name: MrsPMtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_STICKY;
+      ctx->tq_mtx_ctx.protocol = TQ_MTX_MRSP;
       ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_DEADLOCK;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_VERY_HIGH;
       ${/score/mtx/req/seize-wait:/test-run}( &ctx->tq_mtx_ctx );
@@ -391,7 +419,7 @@ transition-map:
     - Forever
 - enabled-by: true
   post-conditions:
-    Action: MtxSeizeTry
+    Action: InheritMtxSeizeTry
   pre-conditions:
     Class:
     - PrioInherit
@@ -403,7 +431,7 @@ transition-map:
     - 'No'
 - enabled-by: true
   post-conditions:
-    Action: MtxSeizeWait
+    Action: InheritMtxSeizeWait
   pre-conditions:
     Class:
     - PrioInherit
diff --git a/spec/score/mtx/req/seize-wait.yml b/spec/score/mtx/req/seize-wait.yml
index 3cf6a7e..99d90db 100644
--- a/spec/score/mtx/req/seize-wait.yml
+++ b/spec/score/mtx/req/seize-wait.yml
@@ -65,6 +65,12 @@ post-conditions:
       ${../../tq/req/enqueue-priority:/test-run}( &ctx->tq_ctx->base );
     text: |
       The calling thread shall be enqueued in priority order.
+  - name: PriorityInherit
+    test-code: |
+      ${../../tq/req/enqueue-priority:/test-run}( &ctx->tq_ctx->base );
+    text: |
+      The calling thread shall be enqueued in priority order with priorit
+      inheritance.
   - name: PriorityCeiling
     test-code: |
       ${../../tq/req/enqueue-ceiling:/test-run}( &ctx->tq_ctx->base );
@@ -121,34 +127,35 @@ post-conditions:
 pre-conditions:
 - name: Protocol
   states:
-  - name: Ceiling
+  states:
+  - name: None
     test-code: |
-      if (
-        ctx->tq_ctx->priority_ceiling == PRIO_INVALID ||
-        ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY
-      ) {
+      if ( ctx->tq_ctx->protocol != TQ_MTX_NO_PROTOCOL ) {
         ${.:skip}
       }
     text: |
-      Where the mutex uses the priority ceiling locking protocol.
-  - name: MrsP
+      Where the mutex does not use a locking protocol.
+  - name: Inherit
     test-code: |
-      if (
-        ctx->tq_ctx->priority_ceiling == PRIO_INVALID ||
-        ctx->tq_ctx->base.enqueue_variant != TQ_ENQUEUE_STICKY
-      ) {
+      if ( ctx->tq_ctx->protocol != TQ_MTX_PRIORITY_INHERIT ) {
         ${.:skip}
       }
     text: |
-      Where the mutex uses the MrsP locking protocol.
-  - name: Other
+      Where the mutex uses the priority inheritance locking protocol.
+  - name: Ceiling
+    test-code: |
+      if ( ctx->tq_ctx->protocol != TQ_MTX_PRIORITY_CEILING ) {
+        ${.:skip}
+      }
+    text: |
+      Where the mutex uses the priority ceiling locking protocol.
+  - name: MrsP
     test-code: |
-      if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
+      if ( ctx->tq_ctx->protocol != TQ_MTX_MRSP ) {
         ${.:skip}
       }
     text: |
-      Where the mutex does not use the priority ceiling or MrsP locking
-      protocol.
+      Where the mutex uses the MrsP locking protocol.
   test-epilogue: null
   test-prologue: null
 - name: Discipline
@@ -535,7 +542,8 @@ transition-map:
     Priority: Nop
   pre-conditions:
     Protocol:
-    - Other
+    - None
+    - Inherit
     Discipline: all
     DeadlockResult: all
     Recursive: all
@@ -546,12 +554,17 @@ transition-map:
   post-conditions:
     Status: N/A
     Enqueued:
+    - if:
+        pre-conditions:
+          Protocol: Inherit
+      then: PriorityInherit
     - specified-by: Discipline
     Owner: Other
     Priority: Nop
   pre-conditions:
     Protocol:
-    - Other
+    - None
+    - Inherit
     Discipline: all
     DeadlockResult: all
     Recursive: all
@@ -566,7 +579,8 @@ transition-map:
     Priority: Nop
   pre-conditions:
     Protocol:
-    - Other
+    - None
+    - Inherit
     Discipline: all
     DeadlockResult: all
     Recursive:
@@ -607,7 +621,8 @@ transition-map:
     Priority: Nop
   pre-conditions:
     Protocol:
-    - Other
+    - None
+    - Inherit
     Discipline: all
     DeadlockResult: all
     Recursive:
@@ -653,7 +668,8 @@ transition-map:
     Priority: Nop
   pre-conditions:
     Protocol:
-    - Other
+    - None
+    - Inherit
     Discipline: all
     DeadlockResult: all
     Recursive: all
@@ -821,6 +837,7 @@ transition-map:
   post-conditions: PriorityDisciplineByProtocol
   pre-conditions:
     Protocol:
+    - Inherit
     - Ceiling
     - MrsP
     Discipline:



More information about the vc mailing list