spec: Improve mutex try seize specification

2 files changed, 353 insertions, 151 deletions

diff --git a/spec/score/mtx/req/seize-try.yml b/spec/score/mtx/req/seize-try.yml
index fb7ad6ff..b8776566 100644
--- a/spec/score/mtx/req/seize-try.yml
+++ b/spec/score/mtx/req/seize-try.yml
@@ -11,54 +11,28 @@ post-conditions:
   states:
   - name: Ok
     test-code: |
-      T_eq_int( ctx->status, Status( ctx, STATUS_SUCCESSFUL ) );
-      TQSurrender( &ctx->tq_ctx->base );
+      T_true( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) );
     text: |
       The return status of the directive call shall be derived from
       ${../../status/if/successful:/name}.
-  - name: OkOrMutexCeilingViolated
+  - name: MutexCeilingViolated
     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 );
-      }
+      T_true( IsEnqueueStatus( ctx, STATUS_MUTEX_CEILING_VIOLATED ) );
     text: |
-      Where the mutex provides a priority ceiling, the return status of the
-      directive call shall be derived from
+      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
+  - name: Deadlock
     test-code: |
-      switch ( ctx->tq_ctx->recursive ) {
-        case TQ_MTX_RECURSIVE_ALLOWED:
-          T_eq_int( ctx->status, Status( ctx, STATUS_SUCCESSFUL ) );
-          TQSurrender( &ctx->tq_ctx->base );
-          break;
-        case TQ_MTX_RECURSIVE_DEADLOCK:
-          T_eq_int( ctx->status, Status( ctx, STATUS_DEADLOCK ) );
-          break;
-        default:
-          T_unreachable();
-          break;
-      }
+      T_true( IsEnqueueStatus( ctx, STATUS_DEADLOCK ) );
     text: |
-      Where recursive seize of the mutex is allowed, the return status of the
-      directive call shall be derived from ${../../status/if/successful:/name}.
-
-      Where recursive seize of the mutex results in a deadlock, the return
-      status of the directive call shall be derived from
+      The return status of the directive call shall be derived from
       ${../../status/if/deadlock:/name}.
-  - name: Unsat
+  - name: Unavailable
     test-code: |
-      T_eq_int( ctx->status, Status( ctx, STATUS_UNSATISFIED ) );
+      T_true( IsEnqueueStatus( ctx, STATUS_UNAVAILABLE ) );
     text: |
       The return status of the directive call shall be derived from
-      ${../../status/if/unsatisfied:/name}.
+      ${../../status/if/unavailable:/name}.
   test-epilogue: null
   test-prologue: null
 - name: Owner
@@ -67,32 +41,23 @@ post-conditions:
     test-code: |
       T_eq_ptr(
         ctx->owner_after,
-        ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
+        ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_B ]
       );
     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 mutex shall be the calling thread.
-  - name: CallerOrNoOwner
-    test-code: |
-      T_eq_ptr( ctx->owner_after, ctx->tq_ctx->base.runner_tcb );
+      T_eq_ptr(
+        ctx->owner_after,
+        ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
+      );
     text: |
       The owner of the mutex shall be the calling thread.
+  - name: None
     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 );
-      }
+      T_null( ctx->owner_after );
     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.
+      The mutex shall have no owner.
   test-epilogue: null
   test-prologue: null
 - name: Priority
@@ -101,26 +66,93 @@ post-conditions:
     test-code: |
       T_eq_u32( ctx->priority_after, ctx->priority_before );
     text: |
-      The current priority of the calling thread shall not be modified.
+      The priorities of the calling thread shall not be modified.
+  - name: Ceiling
+    test-code: |
+      T_eq_u32( ctx->priority_after, ctx->tq_ctx->priority_ceiling );
+    text: |
+      The calling thread shall use the priority ceiling of the mutex.
+  test-epilogue: null
+  test-prologue: null
+pre-conditions:
+- name: Protocol
+  states:
   - name: Ceiling
     test-code: |
+      if (
+        ctx->tq_ctx->priority_ceiling == PRIO_INVALID ||
+        ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY
+      ) {
+        ${.:skip}
+      }
+    text: |
+      Where the mutex uses the priority ceiling locking protocol.
+  - name: MrsP
+    test-code: |
+      if (
+        ctx->tq_ctx->priority_ceiling == PRIO_INVALID ||
+        ctx->tq_ctx->base.enqueue_variant != TQ_ENQUEUE_STICKY
+      ) {
+        ${.:skip}
+      }
+    text: |
+      Where the mutex uses the MrsP locking protocol.
+  - name: Other
+    test-code: |
       if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
-        T_eq_u32( ctx->priority_after, ctx->tq_ctx->priority_ceiling );
-      } else {
-        T_eq_u32( ctx->priority_after, ctx->priority_before );
+        ${.:skip}
       }
     text: |
-      Where the mutex provides a priority ceiling, the calling thread shall use
-      the priority ceiling of the mutex.
-
-      Where the mutex does not provide a priority ceiling, the current priority
-      of the calling thread shall not be modified.
+      Where the mutex does not use the priority ceiling or MrsP locking
+      protocol.
+  test-epilogue: null
+  test-prologue: null
+- name: Discipline
+  states:
+  - name: FIFO
+    test-code: |
+      if ( ctx->tq_ctx->base.discipline != TQ_FIFO ) {
+        ${.:skip}
+      }
+    text: |
+      Where the thread queue of the mutex uses the FIFO discipline.
+  - name: Priority
+    test-code: |
+      if ( ctx->tq_ctx->base.discipline != TQ_PRIORITY ) {
+        ${.:skip}
+      }
+    text: |
+      Where the thread queue of the mutex uses the priority discipline.
+  test-epilogue: null
+  test-prologue: null
+- name: Recursive
+  states:
+  - name: Allowed
+    test-code: |
+      if ( ctx->tq_ctx->recursive != TQ_MTX_RECURSIVE_ALLOWED ) {
+        ${.:skip}
+      }
+    text: |
+      Where a recursive seize of the mutex is allowed.
+  - name: Unavailable
+    test-code: |
+      if ( ctx->tq_ctx->recursive != TQ_MTX_RECURSIVE_UNAVAILABLE ) {
+        ${.:skip}
+      }
+    text: |
+      Where a recursive seize of the mutex results in an unavailable status.
+  - name: Deadlock
+    test-code: |
+      if ( ctx->tq_ctx->recursive != TQ_MTX_RECURSIVE_DEADLOCK ) {
+        ${.:skip}
+      }
+    text: |
+      Where a recursive seize of the mutex results in a deadlock status.
   test-epilogue: null
   test-prologue: null
-pre-conditions:
 - name: Owner
   states:
-  - name: 'No'
+  - name: None
     test-code: |
       /* This is the default */
     text: |
@@ -139,24 +171,24 @@ pre-conditions:
   test-prologue: null
 - name: Priority
   states:
-  - name: LT
+  - name: High
     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
+      While the calling thread has a ${/glossary/priority-current:/term} higher
+      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: GT
+      While the calling thread has a ${/glossary/priority-current:/term} equal
+      to the priority ceiling.
+  - name: Low
     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.
+      While the calling thread has a ${/glossary/priority-current:/term} lower
+      than the priority ceiling.
   test-epilogue: null
   test-prologue: null
 rationale: null
@@ -165,68 +197,23 @@ 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} greater than the priority ceiling.
+    have a ${/glossary/priority-current:/term} lower than the priority ceiling.
+  PriorityDisciplineByProtocol: |
+    The priority ceiling and MrsP locking protocol requires a priority
+    discipline.
 test-action: |
-  rtems_task_priority priority;
-
-  priority = GetSelfPriority();
-
-  if ( ctx->owner_caller ) {
-    Status_Control status;
+  TQSetScheduler(
+    &ctx->tq_ctx->base,
+    TQ_BLOCKER_B,
+    SCHEDULER_A_ID,
+    PRIO_VERY_HIGH
+  );
 
-    status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
-    T_eq_int( status, Status( ctx, STATUS_SUCCESSFUL ) );
-  } else if ( ctx->owner_other ) {
-    if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
-      TQSetScheduler(
-        &ctx->tq_ctx->base,
-        TQ_BLOCKER_A,
-        ctx->tq_ctx->base.other_scheduler_id,
-        PRIO_HIGH
-      );
-      TQSend(
-        &ctx->tq_ctx->base,
-        TQ_BLOCKER_A,
-        TQ_EVENT_ENQUEUE | TQ_EVENT_RUNNER_SYNC
-      );
-      TQSynchronizeRunner();
-    } else {
-      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
-    }
-  }
-
-  if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
-    SetSelfPriority( ctx->priority_before );
+  if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
+    ActionSticky( ctx );
   } else {
-    ctx->priority_before = GetSelfPriority();
-  }
-
-  ctx->status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
-  ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
-  ctx->priority_after = GetSelfPriority();
-
-  if ( ctx->owner_caller ) {
-    TQSurrender( &ctx->tq_ctx->base );
-  } else if ( ctx->owner_other ) {
-    if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
-      TQSend(
-        &ctx->tq_ctx->base,
-        TQ_BLOCKER_A,
-        TQ_EVENT_SURRENDER | TQ_EVENT_RUNNER_SYNC
-      );
-      TQSynchronizeRunner();
-      TQSetScheduler(
-        &ctx->tq_ctx->base,
-        TQ_BLOCKER_A,
-        ctx->tq_ctx->base.runner_scheduler_id,
-        PRIO_HIGH
-      );
-    } else {
-      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
-    }
+    Action( ctx );
   }
-
-  SetSelfPriority( priority );
 test-brief: null
 test-cleanup: null
 test-context:
@@ -249,11 +236,6 @@ test-context:
   member: |
     rtems_task_priority priority_before;
 - brief: |
-    This member contains the return status of the directive call.
-  description: null
-  member: |
-    Status_Control status
-- brief: |
     This member contains the owner of the mutex after the directive call.
   description: null
   member: |
@@ -282,9 +264,14 @@ test-header:
 test-includes: []
 test-local-includes:
 - tr-mtx-seize-try.h
+- tr-tq-enqueue-ceiling.h
+- tr-tq-enqueue-fifo.h
+- tr-tq-enqueue-mrsp.h
+- tr-tq-enqueue-priority.h
 test-prepare: |
   ctx->owner_caller = false;
   ctx->owner_other = false;
+  ctx->priority_before = PRIO_VERY_HIGH;
 test-setup: null
 test-stop: null
 test-support: |
@@ -294,6 +281,104 @@ test-support: |
   {
     return TQConvertStatus( &ctx->tq_ctx->base, status );
   }
+
+  static bool IsEnqueueStatus( const Context *ctx, Status_Control expected )
+  {
+    return ctx->tq_ctx->base.status[ TQ_BLOCKER_A ] == Status( ctx, expected );
+  }
+
+  static void Action( Context *ctx )
+  {
+    TQSetScheduler(
+      &ctx->tq_ctx->base,
+      TQ_BLOCKER_A,
+      SCHEDULER_A_ID,
+      PRIO_VERY_HIGH
+    );
+
+    if ( ctx->owner_caller ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
+    } else if ( ctx->owner_other ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_B, TQ_EVENT_ENQUEUE );
+    }
+
+    TQSetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A, ctx->priority_before );
+    TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
+    ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
+    ctx->priority_after = TQGetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A );
+
+    if ( ctx->owner_caller ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
+    } else if ( ctx->owner_other ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_B, TQ_EVENT_SURRENDER );
+    }
+
+    if ( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
+    }
+  }
+
+  static void ActionSticky( Context *ctx )
+  {
+    TQSetScheduler(
+      &ctx->tq_ctx->base,
+      TQ_BLOCKER_A,
+      SCHEDULER_B_ID,
+      PRIO_VERY_HIGH
+    );
+
+    if ( ctx->owner_caller ) {
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_A,
+        TQ_EVENT_ENQUEUE
+      );
+    } else if ( ctx->owner_other ) {
+      SetSelfScheduler( SCHEDULER_B_ID, PRIO_ULTRA_HIGH );
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_B,
+        TQ_EVENT_ENQUEUE
+      );
+      SetSelfScheduler( SCHEDULER_A_ID, PRIO_ULTRA_HIGH );
+    }
+
+    TQSetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A, ctx->priority_before );
+    TQClearDone( &ctx->tq_ctx->base, TQ_BLOCKER_A );
+    TQSendAndWaitForExecutionStopOrIntendToBlock(
+      &ctx->tq_ctx->base,
+      TQ_BLOCKER_A,
+      TQ_EVENT_ENQUEUE
+    );
+    ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
+    ctx->priority_after = TQGetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A );
+
+    if ( ctx->owner_caller ) {
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_A,
+        TQ_EVENT_SURRENDER
+      );
+    } else if ( ctx->owner_other ) {
+      SetSelfScheduler( SCHEDULER_B_ID, PRIO_ULTRA_HIGH );
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_B,
+        TQ_EVENT_SURRENDER
+      );
+      SetSelfScheduler( SCHEDULER_A_ID, PRIO_NORMAL );
+    }
+
+    TQWaitForDone( &ctx->tq_ctx->base, TQ_BLOCKER_A );
+
+    if ( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) ) {
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_A,
+        TQ_EVENT_SURRENDER
+      );
+    }
+  }
 test-target: testsuites/validation/tr-mtx-seize-try.c
 test-teardown: null
 text: |
@@ -303,48 +388,153 @@ transition-map:
   post-conditions:
     Status: Ok
     Owner: Caller
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    Recursive: all
+    Owner:
+    - None
+    Priority: N/A
+- enabled-by: true
+  post-conditions:
+    Status: Ok
+    Owner: Caller
     Priority: Ceiling
   pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    Recursive: all
     Owner:
-    - 'No'
+    - None
     Priority:
-    - EQ
-    - GT
+    - Low
+    - Equal
 - enabled-by: true
   post-conditions:
-    Status: OkOrMutexCeilingViolated
-    Owner: CallerOrNoOwner
+    Status: Unavailable
+    Owner: Other
     Priority: Nop
   pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    Recursive: all
     Owner:
-    - 'No'
+    - Other
+    Priority: N/A
+- enabled-by: true
+  post-conditions:
+    Status: Unavailable
+    Owner: Other
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline: all
+    Recursive: all
+    Owner:
+    - Other
+    Priority: all
+- enabled-by: true
+  post-conditions:
+    Status:
+    - if:
+        pre-conditions:
+          Recursive: Allowed
+      then: Ok
+    - specified-by: Recursive
+    Owner: Caller
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    Recursive: all
+    Owner:
+    - Caller
+    Priority: N/A
+- enabled-by: true
+  post-conditions:
+    Status: Ok
+    Owner: Caller
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    Recursive:
+    - Allowed
+    Owner:
+    - Caller
     Priority:
-    - LT
+    - High
+    - Equal
 - enabled-by: true
   post-conditions:
-    Status: Recursive
+    Status:
+    - specified-by: Recursive
     Owner: Caller
     Priority: Nop
   pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    Recursive:
+    - Deadlock
+    - Unavailable
     Owner:
     - Caller
     Priority:
-    - LT
-    - EQ
+    - High
+    - Equal
 - enabled-by: true
   post-conditions:
-    Status: Unsat
-    Owner: Other
+    Status: MutexCeilingViolated
+    Owner: None
     Priority: Nop
   pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    Recursive: all
     Owner:
-    - Other
-    Priority: all
+    - None
+    Priority:
+    - High
 - enabled-by: true
   post-conditions: CeilingOwner
   pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    Recursive: all
     Owner:
     - Caller
     Priority:
-    - GT
+    - Low
+- enabled-by: true
+  post-conditions: PriorityDisciplineByProtocol
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - FIFO
+    Recursive: all
+    Owner: all
+    Priority: all
 type: requirement
diff --git a/spec/score/status/if/unavailable.yml b/spec/score/status/if/unavailable.yml
new file mode 100644
index 00000000..b7d76bdc
--- /dev/null
+++ b/spec/score/status/if/unavailable.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_UNAVAILABLE
+references: []
+type: interface