[rtems-central commit] spec: Improve deadlock specification
Sebastian Huber
sebh at rtems.org
Fri Sep 24 11:32:07 UTC 2021
Module: rtems-central
Branch: master
Commit: 8c4f3fc4eec3dc027941eb42fa970673ae2026df
Changeset: http://git.rtems.org/rtems-central/commit/?id=8c4f3fc4eec3dc027941eb42fa970673ae2026df
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Mon Sep 20 12:35:10 2021 +0200
spec: Improve deadlock specification
---
spec/rtems/sem/req/obtain.yml | 7 +--
spec/score/mtx/req/seize-wait.yml | 58 ++++++++++++-------------
spec/score/tq/req/enqueue-deadlock.yml | 79 +++++++++++++++++++++++++---------
3 files changed, 87 insertions(+), 57 deletions(-)
diff --git a/spec/rtems/sem/req/obtain.yml b/spec/rtems/sem/req/obtain.yml
index 2086c56..b14eb66 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 8439441..1174a35 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 2b44165..1b89528 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
More information about the vc
mailing list