spec: Improve deadlock specification

3 files changed, 87 insertions, 57 deletions

diff --git a/spec/rtems/sem/req/obtain.yml b/spec/rtems/sem/req/obtain.yml
index 2086c561..b14eb669 100644
--- a/spec/rtems/sem/req/obtain.yml
+++ b/spec/rtems/sem/req/obtain.yml
@@ -36,7 +36,6 @@ post-conditions:
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
       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: |
@@ -46,7 +45,6 @@ post-conditions:
   - name: MtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      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 );
@@ -57,7 +55,6 @@ post-conditions:
   - name: CeilingMtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      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 );
@@ -68,7 +65,6 @@ post-conditions:
   - name: CeilingMtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_BLOCKS;
-      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 );
@@ -79,7 +75,6 @@ post-conditions:
   - name: MrsPMtxSeizeTry
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_STICKY;
-      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 );
@@ -90,7 +85,6 @@ post-conditions:
   - name: MrsPMtxSeizeWait
     test-code: |
       ctx->tq_mtx_ctx.base.enqueue_variant = TQ_ENQUEUE_STICKY;
-      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 );
@@ -268,6 +262,7 @@ test-setup:
   brief: null
   code: |
     memset( ctx, 0, sizeof( *ctx ) );
+    ctx->tq_ctx.deadlock = TQ_DEADLOCK_STATUS;
     ctx->tq_ctx.enqueue_prepare = TQEnqueuePrepareDefault;
     ctx->tq_ctx.enqueue_done = TQEnqueueDoneDefault;
     ctx->tq_ctx.enqueue = TQEnqueueClassicSem;
diff --git a/spec/score/mtx/req/seize-wait.yml b/spec/score/mtx/req/seize-wait.yml
index 84394417..1174a35d 100644
--- a/spec/score/mtx/req/seize-wait.yml
+++ b/spec/score/mtx/req/seize-wait.yml
@@ -30,7 +30,8 @@ post-conditions:
       ${../../status/if/deadlock:/name}.
   - name: DeadlockFatal
     test-code: |
-      T_unreachable();
+      T_eq_int( ctx->tq_ctx->base.status[ TQ_BLOCKER_A ], STATUS_DEADLOCK );
+      ${../../tq/req/enqueue-deadlock:/test-run}( &ctx->tq_ctx->base );
     text: |
       The system shall terminate with the
       ${/score/interr/if/internal-error-core:/name} fatal source and the
@@ -162,14 +163,14 @@ pre-conditions:
   states:
   - name: Status
     test-code: |
-      if ( ctx->tq_ctx->deadlock != TQ_MTX_DEADLOCK_STATUS ) {
+      if ( ctx->tq_ctx->base.deadlock != TQ_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 ) {
+      if ( ctx->tq_ctx->base.deadlock != TQ_DEADLOCK_FATAL ) {
         ${.:skip}
       }
     text: |
@@ -196,7 +197,7 @@ pre-conditions:
   test-prologue: null
 - name: Owner
   states:
-  - name: 'No'
+  - name: None
     test-code: |
       /* This is the default */
     text: |
@@ -255,7 +256,7 @@ test-action: |
   TQSetScheduler(
     &ctx->tq_ctx->base,
     TQ_BLOCKER_B,
-    ctx->tq_ctx->base.runner_scheduler_id,
+    SCHEDULER_A_ID,
     PRIO_VERY_HIGH
   );
 
@@ -346,10 +347,12 @@ test-support: |
 
   static void Action( Context *ctx )
   {
+    TQEvent enqueue;
+
     TQSetScheduler(
       &ctx->tq_ctx->base,
       TQ_BLOCKER_A,
-      ctx->tq_ctx->base.runner_scheduler_id,
+      SCHEDULER_A_ID,
       PRIO_VERY_HIGH
     );
 
@@ -376,7 +379,14 @@ test-support: |
     }
 
     TQSetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A, ctx->priority_before );
-    TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
+
+    if ( ctx->tq_ctx->base.deadlock == TQ_DEADLOCK_FATAL ) {
+      enqueue = TQ_EVENT_ENQUEUE_FATAL;
+    } else {
+      enqueue = TQ_EVENT_ENQUEUE;
+    }
+
+    TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, enqueue );
     ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
     ctx->priority_after = TQGetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A );
 
@@ -412,7 +422,7 @@ test-support: |
     TQSetScheduler(
       &ctx->tq_ctx->base,
       TQ_BLOCKER_A,
-      ctx->tq_ctx->base.other_scheduler_id,
+      SCHEDULER_B_ID,
       PRIO_VERY_HIGH
     );
 
@@ -431,10 +441,7 @@ test-support: |
         );
       }
 
-      SetSelfScheduler(
-        ctx->tq_ctx->base.other_scheduler_id,
-        PRIO_ULTRA_HIGH
-      );
+      SetSelfScheduler( SCHEDULER_B_ID, PRIO_ULTRA_HIGH );
       TQSendAndSynchronizeRunner(
         &ctx->tq_ctx->base,
         TQ_BLOCKER_B,
@@ -449,10 +456,7 @@ test-support: |
         );
       }
 
-      SetSelfScheduler(
-        ctx->tq_ctx->base.runner_scheduler_id,
-        PRIO_ULTRA_HIGH
-      );
+      SetSelfScheduler( SCHEDULER_A_ID, PRIO_ULTRA_HIGH );
     }
 
     TQSetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A, ctx->priority_before );
@@ -480,10 +484,7 @@ test-support: |
         );
       }
 
-      SetSelfScheduler(
-        ctx->tq_ctx->base.other_scheduler_id,
-        PRIO_ULTRA_HIGH
-      );
+      SetSelfScheduler( SCHEDULER_B_ID, PRIO_ULTRA_HIGH );
       TQSendAndSynchronizeRunner(
         &ctx->tq_ctx->base,
         TQ_BLOCKER_B,
@@ -498,10 +499,7 @@ test-support: |
         );
       }
 
-      SetSelfScheduler(
-        ctx->tq_ctx->base.runner_scheduler_id,
-        PRIO_NORMAL
-      );
+      SetSelfScheduler( SCHEDULER_A_ID, PRIO_NORMAL );
     }
 
     TQWaitForDone( &ctx->tq_ctx->base, TQ_BLOCKER_A );
@@ -532,7 +530,7 @@ transition-map:
     DeadlockResult: all
     Recursive: all
     Owner:
-    - 'No'
+    - None
     Priority: N/A
 - enabled-by: true
   post-conditions:
@@ -690,7 +688,7 @@ transition-map:
     DeadlockResult: all
     Recursive: all
     Owner:
-    - 'No'
+    - None
     Priority:
     - Low
     - Equal
@@ -756,7 +754,7 @@ transition-map:
     Owner:
     - if:
         pre-conditions:
-          Owner: 'No'
+          Owner: None
       then: None
     - else: Other
     Priority: Nop
@@ -768,7 +766,7 @@ transition-map:
     DeadlockResult: all
     Recursive: all
     Owner:
-    - 'No'
+    - None
     Priority:
     - High
 - enabled-by: true
@@ -778,7 +776,7 @@ transition-map:
     Owner:
     - if:
         pre-conditions:
-          Owner: 'No'
+          Owner: None
       then: None
     - else: Other
     Priority: Nop
@@ -790,7 +788,7 @@ transition-map:
     DeadlockResult: all
     Recursive: all
     Owner:
-    - 'No'
+    - None
     - Other
     - Deadlock
     Priority:
diff --git a/spec/score/tq/req/enqueue-deadlock.yml b/spec/score/tq/req/enqueue-deadlock.yml
index 2b441657..1b89528a 100644
--- a/spec/score/tq/req/enqueue-deadlock.yml
+++ b/spec/score/tq/req/enqueue-deadlock.yml
@@ -7,17 +7,42 @@ links:
 - role: requirement-refinement
   uid: ../if/group
 post-conditions:
-- name: Status
+- name: Result
   states:
-  - name: Deadlock
+  - name: Status
     test-code: |
       /* Checked by action */
     text: |
       The return status of the directive call shall be derived from
       ${../../status/if/deadlock:/name}.
+  - name: Fatal
+    test-code: |
+      /* Checked by action */
+    text: |
+      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
 pre-conditions:
+- name: Notification
+  states:
+  - name: Status
+    test-code: |
+      if ( ctx->tq_ctx->deadlock != TQ_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_DEADLOCK_FATAL ) {
+        ${.:skip}
+      }
+    text: |
+      Where a detected deadlock results in a fatal error.
+  test-epilogue: null
+  test-prologue: null
 - name: Deadlock
   states:
   - name: One
@@ -43,53 +68,63 @@ skip-reasons: {}
 test-action: |
   Status_Control status;
 
-  TQMutexObtain( ctx->tq_ctx, TQ_MUTEX_A );
-
   if ( ctx->tq_ctx->enqueue_variant == TQ_ENQUEUE_STICKY ) {
-    TQSetScheduler(
-      ctx->tq_ctx,
-      TQ_BLOCKER_A,
-      ctx->tq_ctx->other_scheduler_id,
-      PRIO_HIGH
-    );
+    TQSetScheduler( ctx->tq_ctx, TQ_BLOCKER_A, SCHEDULER_B_ID, PRIO_NORMAL );
   } else {
     TQSetScheduler(
       ctx->tq_ctx,
       TQ_BLOCKER_A,
-      ctx->tq_ctx->runner_scheduler_id,
-      PRIO_HIGH
+      SCHEDULER_A_ID,
+      PRIO_VERY_HIGH
     );
   }
 
+  TQSetScheduler( ctx->tq_ctx, TQ_BLOCKER_B, SCHEDULER_A_ID, PRIO_HIGH );
+  TQSetScheduler( ctx->tq_ctx, TQ_BLOCKER_C, SCHEDULER_A_ID, PRIO_HIGH );
+
+  TQSortMutexesByID( ctx->tq_ctx );
+  TQMutexObtain( ctx->tq_ctx, TQ_MUTEX_C );
   TQSendAndWaitForExecutionStop( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
 
   if ( ctx->more ) {
-    TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_B_OBTAIN );
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_A_OBTAIN );
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_C_OBTAIN );
+    Yield();
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_MUTEX_B_OBTAIN );
+    Yield();
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_MUTEX_A_OBTAIN );
+    Yield();
     TQSendAndWaitForExecutionStop(
       ctx->tq_ctx,
       TQ_BLOCKER_A,
       TQ_EVENT_MUTEX_B_OBTAIN
     );
-    TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_A_OBTAIN );
   } else {
     TQSendAndWaitForExecutionStop(
       ctx->tq_ctx,
       TQ_BLOCKER_A,
-      TQ_EVENT_MUTEX_A_OBTAIN
+      TQ_EVENT_MUTEX_C_OBTAIN
     );
   }
 
-  status = TQEnqueue( ctx->tq_ctx, TQ_WAIT_FOREVER );
-  T_eq_int( status, TQConvertStatus( ctx->tq_ctx, STATUS_DEADLOCK ) );
+  if ( ctx->tq_ctx->deadlock == TQ_DEADLOCK_FATAL ) {
+    status = TQEnqueueFatal( ctx->tq_ctx );
+    T_eq_int( status, STATUS_DEADLOCK );
+  } else {
+    status = TQEnqueue( ctx->tq_ctx, TQ_WAIT_FOREVER );
+    T_eq_int( status, TQConvertStatus( ctx->tq_ctx, STATUS_DEADLOCK ) );
+  }
 
-  TQMutexRelease( ctx->tq_ctx, TQ_MUTEX_A );
+  TQMutexRelease( ctx->tq_ctx, TQ_MUTEX_C );
 
   if ( ctx->more ) {
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_C_RELEASE );
     TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_A_RELEASE );
-    TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_B_RELEASE );
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_MUTEX_A_RELEASE );
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_MUTEX_B_RELEASE );
     TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_MUTEX_B_RELEASE );
   } else {
-    TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_MUTEX_A_RELEASE );
+    TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_MUTEX_C_RELEASE );
   }
 
   if ( ctx->tq_ctx->enqueue_variant == TQ_ENQUEUE_STICKY ) {
@@ -146,7 +181,9 @@ text: |
 transition-map:
 - enabled-by: true
   post-conditions:
-    Status: Deadlock
+    Result:
+    - specified-by: Notification
   pre-conditions:
+    Notification: all
     Deadlock: all
 type: requirement