[rtems-central commit] spec: Specify priority ceiling violation
Sebastian Huber
sebh at rtems.org
Thu Aug 12 06:30:36 UTC 2021
Module: rtems-central
Branch: master
Commit: 34701f8bdd21cabcff907953adebaa1b17c0a59c
Changeset: http://git.rtems.org/rtems-central/commit/?id=34701f8bdd21cabcff907953adebaa1b17c0a59c
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Wed Aug 11 15:47:04 2021 +0200
spec: Specify priority ceiling violation
---
spec/score/mtx/req/seize-try.yml | 139 +++++++++++++++++++-----
spec/score/status/if/mutex-ceiling-violated.yml | 12 ++
2 files changed, 125 insertions(+), 26 deletions(-)
diff --git a/spec/score/mtx/req/seize-try.yml b/spec/score/mtx/req/seize-try.yml
index aaee66a..4ef805f 100644
--- a/spec/score/mtx/req/seize-try.yml
+++ b/spec/score/mtx/req/seize-try.yml
@@ -16,6 +16,22 @@ post-conditions:
text: |
The return status of the directive call shall be derived from
${../../status/if/successful:/name}.
+ - name: OkOrMutexCeilingViolated
+ 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 );
+ }
+ text: |
+ Where the mutex provides a priority ceiling, 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 ) {
@@ -55,25 +71,36 @@ post-conditions:
test-prologue: null
- name: Owner
states:
- - name: Nop
+ - name: Other
test-code: |
- if ( ctx->owner_self ) {
- T_eq_ptr( ctx->owner_after, ctx->tq_ctx->base.runner_tcb );
- } else if ( ctx->owner_other ) {
- T_eq_ptr(
- ctx->owner_after,
- ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
- );
- } else {
- T_null( ctx->owner_after );
- }
+ T_eq_ptr(
+ ctx->owner_after,
+ ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
+ );
+ 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 semaphore shall not be modified.
- - name: New
+ 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 );
text: |
- The owner of the semaphore shall be the calling thread.
+ The owner of the mutex shall be the calling thread.
+ 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 );
+ }
+ 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.
test-epilogue: null
test-prologue: null
- name: Priority
@@ -106,9 +133,9 @@ pre-conditions:
/* This is the default */
text: |
While the mutex has no owner.
- - name: Self
+ - name: Caller
test-code: |
- ctx->owner_self = true;
+ ctx->owner_caller = true;
text: |
While the owner of the mutex is the calling thread.
- name: Other
@@ -118,12 +145,41 @@ pre-conditions:
While the owner of the mutex is a thread other than the calling thread.
test-epilogue: null
test-prologue: null
+- name: Priority
+ states:
+ - name: Higher
+ 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.
+ - 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: Lower
+ 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} lower than the priority ceiling.
+ test-epilogue: null
+ test-prologue: null
rationale: null
references: []
requirement-type: functional
-skip-reasons: {}
+skip-reasons:
+ CeilingOwner: |
+ Where the mutex provides a priority ceiling, the owner of the mutex cannot
+ have a ${/glossary/priority-current:/term} lower than the priority ceiling.
test-action: |
- if ( ctx->owner_self ) {
+ rtems_task_priority priority;
+
+ priority = GetSelfPriority();
+
+ if ( ctx->owner_caller ) {
Status_Control status;
status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
@@ -147,12 +203,17 @@ test-action: |
}
}
- ctx->priority_before = GetSelfPriority();
+ if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
+ SetSelfPriority( ctx->priority_before );
+ } else {
+ ctx->priority_before = GetSelfPriority();
+ }
+
ctx->status = TQEnqueue( &ctx->tq_ctx->base, TQ_NO_WAIT );
ctx->owner_after = TQMtxGetOwner( ctx->tq_ctx );
ctx->priority_after = GetSelfPriority();
- if ( ctx->owner_self ) {
+ if ( ctx->owner_caller ) {
TQSurrender( &ctx->tq_ctx->base );
} else if ( ctx->owner_other ) {
if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
@@ -172,6 +233,8 @@ test-action: |
TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
}
}
+
+ SetSelfPriority( priority );
test-brief: null
test-cleanup: null
test-context:
@@ -180,7 +243,7 @@ test-context:
mutex.
description: null
member: |
- bool owner_self;
+ bool owner_caller;
- brief: |
If this member is true, then a thread other than the calling thread shall
be the owner of the mutex.
@@ -228,7 +291,7 @@ test-includes: []
test-local-includes:
- tr-mtx-seize-try.h
test-prepare: |
- ctx->owner_self = false;
+ ctx->owner_caller = false;
ctx->owner_other = false;
test-setup: null
test-stop: null
@@ -247,25 +310,49 @@ transition-map:
- enabled-by: true
post-conditions:
Status: Ok
- Owner: New
+ Owner: Caller
Priority: Ceiling
pre-conditions:
Owner:
- 'No'
+ Priority:
+ - Equal
+ - Lower
+- enabled-by: true
+ post-conditions:
+ Status: OkOrMutexCeilingViolated
+ Owner: CallerOrNoOwner
+ Priority: Nop
+ pre-conditions:
+ Owner:
+ - 'No'
+ Priority:
+ - Higher
- enabled-by: true
post-conditions:
Status: Recursive
- Owner: Nop
+ Owner: Caller
Priority: Nop
pre-conditions:
Owner:
- - Self
+ - Caller
+ Priority:
+ - Higher
+ - Equal
- enabled-by: true
post-conditions:
Status: Unsat
- Owner: Nop
+ Owner: Other
Priority: Nop
pre-conditions:
Owner:
- Other
+ Priority: all
+- enabled-by: true
+ post-conditions: CeilingOwner
+ pre-conditions:
+ Owner:
+ - Caller
+ Priority:
+ - Lower
type: requirement
diff --git a/spec/score/status/if/mutex-ceiling-violated.yml b/spec/score/status/if/mutex-ceiling-violated.yml
new file mode 100644
index 0000000..2b4a2e8
--- /dev/null
+++ b/spec/score/status/if/mutex-ceiling-violated.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_MUTEX_CEILING_VIOLATED
+references: {}
+type: interface
More information about the vc
mailing list