[rtems-central commit] spec: Improve mutex try seize specification
Sebastian Huber
sebh at rtems.org
Fri Sep 24 11:32:07 UTC 2021
Module: rtems-central
Branch: master
Commit: b3f558d74759f030f493fba5bace8e26c27835f4
Changeset: http://git.rtems.org/rtems-central/commit/?id=b3f558d74759f030f493fba5bace8e26c27835f4
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Mon Sep 20 12:37:23 2021 +0200
spec: Improve mutex try seize specification
---
spec/score/mtx/req/seize-try.yml | 492 ++++++++++++++++++++++++-----------
spec/score/status/if/unavailable.yml | 12 +
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 fb7ad6f..b877656 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 0000000..b7d76bd
--- /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
More information about the vc
mailing list