spec: Improve mutex seize specification

4 files changed, 605 insertions, 206 deletions

diff --git a/spec/rtems/sem/req/obtain.yml b/spec/rtems/sem/req/obtain.yml
index a48fe071..6fed26f5 100644
--- a/spec/rtems/sem/req/obtain.yml
+++ b/spec/rtems/sem/req/obtain.yml
@@ -35,7 +35,8 @@ post-conditions:
   - name: MtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_YES;
+      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_ALLOWED;
+      ctx->tq_mtx_ctx.deadlock = TQ_MTX_DEADLOCK_STATUS;
       ctx->tq_mtx_ctx.priority_ceiling = PRIO_INVALID;
       ${/score/mtx/req/seize-try:/test-run}( &ctx->tq_mtx_ctx );
     text: |
@@ -45,7 +46,8 @@ post-conditions:
   - name: MtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_YES;
+      ctx->tq_mtx_ctx.deadlock = TQ_MTX_DEADLOCK_STATUS;
+      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: |
@@ -55,7 +57,8 @@ post-conditions:
   - name: CeilingMtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_YES;
+      ctx->tq_mtx_ctx.deadlock = TQ_MTX_DEADLOCK_STATUS;
+      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 );
     text: |
@@ -65,7 +68,8 @@ post-conditions:
   - name: CeilingMtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_YES;
+      ctx->tq_mtx_ctx.deadlock = TQ_MTX_DEADLOCK_STATUS;
+      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 );
     text: |
@@ -75,7 +79,8 @@ post-conditions:
   - name: MrsPMtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_STICKY;
-      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_NO_STATUS;
+      ctx->tq_mtx_ctx.deadlock = TQ_MTX_DEADLOCK_STATUS;
+      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 );
     text: |
@@ -85,7 +90,8 @@ post-conditions:
   - name: MrsPMtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_STICKY;
-      ctx->tq_mtx_ctx.recursive = TQ_MTX_RECURSIVE_NO_STATUS;
+      ctx->tq_mtx_ctx.deadlock = TQ_MTX_DEADLOCK_STATUS;
+      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 );
     text: |
@@ -210,6 +216,18 @@ test-action: |
     &ctx->tq_ctx.thread_queue_id
   );
   T_rsc_success( sc );
+
+  if ( ( ctx->attribute_set & RTEMS_MULTIPROCESSOR_RESOURCE_SHARING ) != 0 ) {
+    rtems_task_priority prio;
+
+    sc = rtems_semaphore_set_priority(
+      ctx->tq_ctx.thread_queue_id,
+      ctx->tq_ctx.other_scheduler_id,
+      PRIO_VERY_HIGH,
+      &prio
+    );
+    T_rsc_success( sc );
+  }
 test-brief: null
 test-cleanup:
   rtems_status_code sc;
diff --git a/spec/score/mtx/req/seize-try.yml b/spec/score/mtx/req/seize-try.yml
index f9bab387..fb7ad6ff 100644
--- a/spec/score/mtx/req/seize-try.yml
+++ b/spec/score/mtx/req/seize-try.yml
@@ -35,32 +35,24 @@ post-conditions:
   - name: Recursive
     test-code: |
       switch ( ctx->tq_ctx->recursive ) {
-        case TQ_MTX_RECURSIVE_YES:
+        case TQ_MTX_RECURSIVE_ALLOWED:
           T_eq_int( ctx->status, Status( ctx, STATUS_SUCCESSFUL ) );
           TQSurrender( &ctx->tq_ctx->base );
           break;
-        case TQ_MTX_RECURSIVE_NO_STATUS:
+        case TQ_MTX_RECURSIVE_DEADLOCK:
           T_eq_int( ctx->status, Status( ctx, STATUS_DEADLOCK ) );
           break;
-        case TQ_MTX_RECURSIVE_NO_FATAL:
-          /* TODO */
-          T_unreachable();
-          break;
         default:
           T_unreachable();
           break;
       }
     text: |
-      Where the mutex supports a recursive seize, the return status of the
+      Where recursive seize of the mutex is allowed, the return status of the
       directive call shall be derived from ${../../status/if/successful:/name}.
 
-      Where the mutex does not support a recursive seize, where a deadlock is
-      indicated by a status code, the return status of the directive call shall
-      be derived from ${../../status/if/deadlock:/name}.
-
-      Where the mutex does not support a recursive seize, where a deadlock is
-      indicated by a fatal error, the thread queue deadlock internal error
-      shall occur.
+      Where recursive seize of the mutex results in a deadlock, the return
+      status of the directive call shall be derived from
+      ${../../status/if/deadlock:/name}.
   - name: Unsat
     test-code: |
       T_eq_int( ctx->status, Status( ctx, STATUS_UNSATISFIED ) );
diff --git a/spec/score/mtx/req/seize-wait.yml b/spec/score/mtx/req/seize-wait.yml
index 8bf08aac..ae7dbbde 100644
--- a/spec/score/mtx/req/seize-wait.yml
+++ b/spec/score/mtx/req/seize-wait.yml
@@ -11,90 +11,61 @@ 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
-    test-code: |
-      switch ( ctx->tq_ctx->recursive ) {
-        case TQ_MTX_RECURSIVE_YES:
-          T_eq_int( ctx->status, Status( ctx, STATUS_SUCCESSFUL ) );
-          TQSurrender( &ctx->tq_ctx->base );
-          break;
-        case TQ_MTX_RECURSIVE_NO_STATUS:
-          T_eq_int( ctx->status, Status( ctx, STATUS_DEADLOCK ) );
-          break;
-        case TQ_MTX_RECURSIVE_NO_FATAL:
-          /* TODO */
-          T_unreachable();
-          break;
-        default:
-          T_unreachable();
-          break;
-      }
-    text: |
-      Where the mutex supports a recursive seize, the return status of the
-      directive call shall be derived from ${../../status/if/successful:/name}.
-
-      Where the mutex does not support a recursive seize, where a deadlock is
-      indicated by a status code, the return status of the directive call shall
-      be derived from ${../../status/if/deadlock:/name}.
-
-      Where the mutex does not support a recursive seize, where a deadlock is
-      indicated by a fatal error, the thread queue deadlock internal error
-      shall occur.
-  - name: Deadlock
+  - name: DeadlockStatus
     test-code: |
+      T_true( IsEnqueueStatus( ctx, STATUS_DEADLOCK ) );
       ${../../tq/req/enqueue-deadlock:/test-run}( &ctx->tq_ctx->base );
     text: |
       The return status of the directive call shall be derived from
-      ${../../status/if/deadlock:/name} for deadlock scenarios specified by
-      ${../../tq/req/enqueue-deadlock}.
-  - name: Enqueued
+      ${../../status/if/deadlock:/name}.
+  - name: DeadlockFatal
     test-code: |
-      switch ( ctx->tq_ctx->base.discipline ) {
-        case TQ_FIFO:
-          ${../../tq/req/enqueue-fifo:/test-run}( &ctx->tq_ctx->base );
-          break;
-        case TQ_PRIORITY:
-          if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
-            if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
-              ${../../tq/req/enqueue-mrsp:/test-run}( &ctx->tq_ctx->base );
-            } else {
-              ${../../tq/req/enqueue-ceiling:/test-run}( &ctx->tq_ctx->base );
-            }
-          } else {
-            ${../../tq/req/enqueue-priority:/test-run}( &ctx->tq_ctx->base );
-          }
-          break;
-        default:
-          T_unreachable();
-          break;
-      }
+      T_unreachable();
     text: |
-      Where the thread queue uses the FIFO discipline, the calling thread shall
-      be enqueued in FIFO order.
-
-      Where the thread queue uses the priority discipline, the calling thread
-      shall be enqueued in priority order.
+      The system shall terminate with the
+      ${/score/interr/if/internal-error-core:/name} fatal source and the
+      ${/score/interr/if/thread-queue-deadlock:/name} fatal code.
+  test-epilogue: null
+  test-prologue: null
+- name: Enqueued
+  states:
+  - name: 'No'
+    test-code: |
+      /* The test runner would block if the worker is enqueued */
+    text: |
+      The calling thread shall not be enqueued on the thread queue of the mutex.
+  - name: FIFO
+    test-code: |
+      ${../../tq/req/enqueue-fifo:/test-run}( &ctx->tq_ctx->base );
+    text: |
+      The calling thread shall be enqueued in FIFO order.
+  - name: Priority
+    test-code: |
+      ${../../tq/req/enqueue-priority:/test-run}( &ctx->tq_ctx->base );
+    text: |
+      The calling thread shall be enqueued in priority order.
+  - name: PriorityCeiling
+    test-code: |
+      ${../../tq/req/enqueue-ceiling:/test-run}( &ctx->tq_ctx->base );
+    text: |
+      The calling thread shall be enqueued in priority order according to the
+      priority ceiling locking protocol.
+  - name: PriorityMrsP
+    test-code: |
+      ${../../tq/req/enqueue-mrsp:/test-run}( &ctx->tq_ctx->base );
+    text: |
+      The calling thread shall be enqueued in priority order according to the
+      MrsP locking protocol.
   test-epilogue: null
   test-prologue: null
 - name: Owner
@@ -103,32 +74,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
@@ -137,23 +99,101 @@ 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: DeadlockResult
+  states:
+  - name: Status
+    test-code: |
+      if ( ctx->tq_ctx->deadlock != TQ_MTX_DEADLOCK_STATUS ) {
+        ${.:skip}
+      }
+    text: |
+      Where a detected deadlock results in a return with a status code.
+  - name: Fatal
+    test-code: |
+      if ( ctx->tq_ctx->deadlock != TQ_MTX_DEADLOCK_FATAL ) {
+        ${.:skip}
+      }
+    text: |
+      Where a detected deadlock results in a fatal error.
+  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: 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.
   test-epilogue: null
   test-prologue: null
-pre-conditions:
 - name: Owner
   states:
   - name: 'No'
@@ -173,6 +213,7 @@ pre-conditions:
       While the owner of the mutex is a thread other than the calling thread.
   - name: Deadlock
     test-code: |
+      ctx->owner_other = true;
       ctx->deadlock = true;
     text: |
       While the attempt to seize the mutex results in a deadlock.
@@ -180,24 +221,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
@@ -206,10 +247,22 @@ 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: |
-  if ( !ctx->deadlock ) {
-    NonDeadlockAction( ctx );
+  TQSetScheduler(
+    &ctx->tq_ctx->base,
+    TQ_BLOCKER_B,
+    ctx->tq_ctx->base.runner_scheduler_id,
+    PRIO_VERY_HIGH
+  );
+
+  if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
+    ActionSticky( ctx );
+  } else {
+    Action( ctx );
   }
 test-brief: null
 test-cleanup: null
@@ -238,11 +291,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: |
@@ -268,8 +316,7 @@ test-header:
     name: tq_ctx
     specifier: TQMtxContext *${.:name}
   target: testsuites/validation/tr-mtx-seize-wait.h
-test-includes:
-- rtems/score/statesimpl.h
+test-includes: []
 test-local-includes:
 - tr-mtx-seize-wait.h
 - tr-tq-enqueue-ceiling.h
@@ -280,10 +327,10 @@ test-local-includes:
 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_caller = false;
   ctx->owner_other = false;
   ctx->deadlock = false;
+  ctx->priority_before = PRIO_VERY_HIGH;
 test-setup: null
 test-stop: null
 test-support: |
@@ -294,90 +341,180 @@ test-support: |
     return TQConvertStatus( &ctx->tq_ctx->base, status );
   }
 
-  static void GetProperties( TQContext *base, TQWorkerKind enqueued_worker )
+  static bool IsEnqueueStatus( const Context *ctx, Status_Control expected )
   {
-    TQMtxContext        *ctx;
-    T_thread_timer_state timer_state;
+    return ctx->tq_ctx->base.status[ TQ_BLOCKER_A ] == Status( ctx, expected );
+  }
 
-    ctx = (TQMtxContext *) base;
-    T_eq_u32(
-      ctx->base.worker_tcb[ enqueued_worker ]->current_state,
-      STATES_WAITING_FOR_MUTEX
+  static void Action( Context *ctx )
+  {
+    TQSetScheduler(
+      &ctx->tq_ctx->base,
+      TQ_BLOCKER_A,
+      ctx->tq_ctx->base.runner_scheduler_id,
+      PRIO_VERY_HIGH
     );
 
-    timer_state = T_get_thread_timer_state(
-      ctx->base.worker_id[ enqueued_worker ]
-    );
+    if ( ctx->owner_caller ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
+    } else if ( ctx->owner_other ) {
+      if ( ctx->deadlock ) {
+        TQSend(
+          &ctx->tq_ctx->base,
+          TQ_BLOCKER_A,
+          TQ_EVENT_MUTEX_NO_PROTOCOL_OBTAIN
+        );
+      }
 
-    if ( base->wait == TQ_WAIT_TICKS ) {
-      T_eq_int( timer_state, T_THREAD_TIMER_SCHEDULED );
-    } else {
-      T_eq_int( timer_state, T_THREAD_TIMER_INACTIVE );
-    }
-  }
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_B, TQ_EVENT_ENQUEUE );
 
-  static void NonDeadlockAction( Context *ctx )
-  {
-    rtems_task_priority priority;
+      if ( ctx->deadlock ) {
+        TQSend(
+          &ctx->tq_ctx->base,
+          TQ_BLOCKER_B,
+          TQ_EVENT_MUTEX_NO_PROTOCOL_OBTAIN
+        );
+      }
+    }
 
-    priority = GetSelfPriority();
+    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 ) {
-      Status_Control status;
-
-      status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
-      T_eq_int( status, Status( ctx, STATUS_SUCCESSFUL ) );
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
     } else if ( ctx->owner_other ) {
-      if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
-        TQSetScheduler(
+      if ( ctx->deadlock ) {
+        TQSend(
           &ctx->tq_ctx->base,
           TQ_BLOCKER_A,
-          ctx->tq_ctx->base.other_scheduler_id,
-          PRIO_HIGH
+          TQ_EVENT_MUTEX_NO_PROTOCOL_RELEASE
         );
+      }
+
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_B, TQ_EVENT_SURRENDER );
+
+      if ( ctx->deadlock ) {
         TQSend(
           &ctx->tq_ctx->base,
-          TQ_BLOCKER_A,
-          TQ_EVENT_ENQUEUE | TQ_EVENT_RUNNER_SYNC
+          TQ_BLOCKER_B,
+          TQ_EVENT_MUTEX_NO_PROTOCOL_RELEASE
         );
-        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 );
-    } else {
-      ctx->priority_before = GetSelfPriority();
+    if ( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) ) {
+      TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
     }
+  }
 
-    ctx->status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
-    ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
-    ctx->priority_after = GetSelfPriority();
+  static void ActionSticky( Context *ctx )
+  {
+    TQSetScheduler(
+      &ctx->tq_ctx->base,
+      TQ_BLOCKER_A,
+      ctx->tq_ctx->base.other_scheduler_id,
+      PRIO_VERY_HIGH
+    );
 
     if ( ctx->owner_caller ) {
-      TQSurrender( &ctx->tq_ctx->base );
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_A,
+        TQ_EVENT_ENQUEUE
+      );
     } else if ( ctx->owner_other ) {
-      if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
-        TQSend(
+      if ( ctx->deadlock ) {
+        TQSendAndSynchronizeRunner(
           &ctx->tq_ctx->base,
           TQ_BLOCKER_A,
-          TQ_EVENT_SURRENDER | TQ_EVENT_RUNNER_SYNC
+          TQ_EVENT_MUTEX_NO_PROTOCOL_OBTAIN
         );
-        TQSynchronizeRunner();
-        TQSetScheduler(
+      }
+
+      SetSelfScheduler(
+        ctx->tq_ctx->base.other_scheduler_id,
+        PRIO_ULTRA_HIGH
+      );
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_B,
+        TQ_EVENT_ENQUEUE
+      );
+
+      if ( ctx->deadlock ) {
+        TQSendAndWaitForExecutionStop(
+          &ctx->tq_ctx->base,
+          TQ_BLOCKER_B,
+          TQ_EVENT_MUTEX_NO_PROTOCOL_OBTAIN
+        );
+      }
+
+      SetSelfScheduler(
+        ctx->tq_ctx->base.runner_scheduler_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 ) {
+      if ( ctx->deadlock ) {
+        TQSendAndSynchronizeRunner(
           &ctx->tq_ctx->base,
           TQ_BLOCKER_A,
-          ctx->tq_ctx->base.runner_scheduler_id,
-          PRIO_HIGH
+          TQ_EVENT_MUTEX_NO_PROTOCOL_RELEASE
         );
-      } else {
-        TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
       }
+
+      SetSelfScheduler(
+        ctx->tq_ctx->base.other_scheduler_id,
+        PRIO_ULTRA_HIGH
+      );
+      TQSendAndSynchronizeRunner(
+        &ctx->tq_ctx->base,
+        TQ_BLOCKER_B,
+        TQ_EVENT_SURRENDER
+      );
+
+      if ( ctx->deadlock ) {
+        TQSendAndSynchronizeRunner(
+          &ctx->tq_ctx->base,
+          TQ_BLOCKER_B,
+          TQ_EVENT_MUTEX_NO_PROTOCOL_RELEASE
+        );
+      }
+
+      SetSelfScheduler(
+        ctx->tq_ctx->base.runner_scheduler_id,
+        PRIO_NORMAL
+      );
     }
 
-    SetSelfPriority( priority );
+    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-wait.c
 test-teardown: null
@@ -387,58 +524,303 @@ transition-map:
 - enabled-by: true
   post-conditions:
     Status: Ok
+    Enqueued: 'No'
     Owner: Caller
-    Priority: Ceiling
+    Priority: Nop
   pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    DeadlockResult: all
+    Recursive: all
     Owner:
     - 'No'
-    Priority:
-    - EQ
-    - GT
+    Priority: N/A
 - enabled-by: true
   post-conditions:
-    Status: OkOrMutexCeilingViolated
-    Owner: CallerOrNoOwner
+    Status: N/A
+    Enqueued:
+    - specified-by: Discipline
+    Owner: Other
     Priority: Nop
   pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    DeadlockResult: all
+    Recursive: all
     Owner:
-    - 'No'
+    - Other
+    Priority: N/A
+- enabled-by: true
+  post-conditions:
+    Status: Ok
+    Enqueued: 'No'
+    Owner: Caller
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    DeadlockResult: all
+    Recursive:
+    - Allowed
+    Owner:
+    - Caller
+    Priority: N/A
+- enabled-by: true
+  post-conditions:
+    Status: Ok
+    Enqueued: 'No'
+    Owner: Caller
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive:
+    - Allowed
+    Owner:
+    - Caller
     Priority:
-    - LT
+    - High
+    - Equal
+- enabled-by: true
+  post-conditions:
+    Status:
+    - if:
+        pre-conditions:
+           DeadlockResult: Fatal
+      then: DeadlockFatal
+    - else: DeadlockStatus
+    Enqueued: 'No'
+    Owner: Caller
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    DeadlockResult: all
+    Recursive:
+    - Deadlock
+    Owner:
+    - Caller
+    Priority: N/A
 - enabled-by: true
   post-conditions:
-    Status: Recursive
+    Status:
+    - if:
+        pre-conditions:
+           DeadlockResult: Fatal
+      then: DeadlockFatal
+    - else: DeadlockStatus
+    Enqueued: 'No'
     Owner: Caller
     Priority: Nop
   pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive:
+    - Deadlock
     Owner:
     - Caller
     Priority:
-    - LT
-    - EQ
+    - High
+    - Equal
+- enabled-by: true
+  post-conditions:
+    Status:
+    - if:
+        pre-conditions:
+           DeadlockResult: Fatal
+      then: DeadlockFatal
+    - else: DeadlockStatus
+    Enqueued: 'No'
+    Owner: Other
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Other
+    Discipline: all
+    DeadlockResult: all
+    Recursive: all
+    Owner:
+    - Deadlock
+    Priority: N/A
 - enabled-by: true
   post-conditions:
-    Status: Enqueued
+    Status:
+    - if:
+        pre-conditions:
+           DeadlockResult: Fatal
+      then: DeadlockFatal
+    - else: DeadlockStatus
+    Enqueued: 'No'
     Owner: Other
     Priority: Nop
   pre-conditions:
+    Protocol:
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
+    Owner:
+    - Deadlock
+    Priority:
+    - Low
+    - Equal
+- enabled-by: true
+  post-conditions:
+    Status: Ok
+    Enqueued: 'No'
+    Owner: Caller
+    Priority: Ceiling
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
+    Owner:
+    - 'No'
+    Priority:
+    - Low
+    - Equal
+- enabled-by: true
+  post-conditions:
+    Status: N/A
+    Enqueued: PriorityCeiling
+    Owner: Other
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
     Owner:
     - Other
     Priority: all
 - enabled-by: true
   post-conditions:
-    Status: Deadlock
-    Owner: N/A
-    Priority: N/A
+    Status:
+    - if:
+        pre-conditions:
+           DeadlockResult: Fatal
+      then: DeadlockFatal
+    - else: DeadlockStatus
+    Enqueued: 'No'
+    Owner: Other
+    Priority: Nop
   pre-conditions:
+    Protocol:
+    - Ceiling
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
     Owner:
     - Deadlock
     Priority: all
 - enabled-by: true
+  post-conditions:
+    Status: N/A
+    Enqueued: PriorityMrsP
+    Owner: Other
+    Priority: Ceiling
+  pre-conditions:
+    Protocol:
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
+    Owner:
+    - Other
+    Priority:
+    - Low
+    - Equal
+- enabled-by: true
+  post-conditions:
+    Status: MutexCeilingViolated
+    Enqueued: 'No'
+    Owner:
+    - if:
+        pre-conditions:
+          Owner: 'No'
+      then: None
+    - else: Other
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
+    Owner:
+    - 'No'
+    Priority:
+    - High
+- enabled-by: true
+  post-conditions:
+    Status: MutexCeilingViolated
+    Enqueued: 'No'
+    Owner:
+    - if:
+        pre-conditions:
+          Owner: 'No'
+      then: None
+    - else: Other
+    Priority: Nop
+  pre-conditions:
+    Protocol:
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
+    Owner:
+    - 'No'
+    - Other
+    - Deadlock
+    Priority:
+    - High
+- enabled-by: true
   post-conditions: CeilingOwner
   pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - Priority
+    DeadlockResult: all
+    Recursive: all
     Owner:
     - Caller
     Priority:
-    - GT
+    - Low
+- enabled-by: true
+  post-conditions: PriorityDisciplineByProtocol
+  pre-conditions:
+    Protocol:
+    - Ceiling
+    - MrsP
+    Discipline:
+    - FIFO
+    DeadlockResult: all
+    Recursive: all
+    Owner: all
+    Priority: all
 type: requirement
diff --git a/spec/score/tq/req/enqueue-deadlock.yml b/spec/score/tq/req/enqueue-deadlock.yml
index f2a96006..2b441657 100644
--- a/spec/score/tq/req/enqueue-deadlock.yml
+++ b/spec/score/tq/req/enqueue-deadlock.yml
@@ -52,6 +52,13 @@ test-action: |
       ctx->tq_ctx->other_scheduler_id,
       PRIO_HIGH
     );
+  } else {
+    TQSetScheduler(
+      ctx->tq_ctx,
+      TQ_BLOCKER_A,
+      ctx->tq_ctx->runner_scheduler_id,
+      PRIO_HIGH
+    );
   }
 
   TQSendAndWaitForExecutionStop( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );