[rtems-central commit] spec: Specify rtems_semaphore_set_priority()
Sebastian Huber
sebh at rtems.org
Tue Mar 23 15:35:44 UTC 2021
Module: rtems-central
Branch: master
Commit: 3772505f6558c05eee9e79ad1db63006f741561d
Changeset: http://git.rtems.org/rtems-central/commit/?id=3772505f6558c05eee9e79ad1db63006f741561d
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Mon Mar 22 16:44:41 2021 +0100
spec: Specify rtems_semaphore_set_priority()
---
spec/rtems/sem/req/set-priority.yml | 703 ++++++++++++++++++++++++++++++++++++
1 file changed, 703 insertions(+)
diff --git a/spec/rtems/sem/req/set-priority.yml b/spec/rtems/sem/req/set-priority.yml
new file mode 100644
index 0000000..2a0f00c
--- /dev/null
+++ b/spec/rtems/sem/req/set-priority.yml
@@ -0,0 +1,703 @@
+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
+functional-type: action
+links:
+- role: interface-function
+ uid: ../if/set-priority
+post-conditions:
+- name: Status
+ states:
+ - name: Ok
+ test-code: |
+ T_rsc_success( ctx->status );
+ text: |
+ The return status of ${../if/set-priority:/name} shall be
+ ${../../status/if/successful:/name}.
+ - name: InvAddr
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ADDRESS );
+ text: |
+ The return status of ${../if/set-priority:/name} shall be
+ ${../../status/if/invalid-address:/name}.
+ - name: InvId
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ID );
+ text: |
+ The return status of ${../if/set-priority:/name} shall be
+ ${../../status/if/invalid-id:/name}.
+ - name: InvPrio
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_PRIORITY );
+ text: |
+ The return status of ${../if/set-priority:/name} shall be
+ ${../../status/if/invalid-priority:/name}.
+ - name: NotDef
+ test-code: |
+ T_rsc( ctx->status, RTEMS_NOT_DEFINED );
+ text: |
+ The return status of ${../if/set-priority:/name} shall be
+ ${../../status/if/not-defined:/name}.
+ test-epilogue: null
+ test-prologue: null
+- name: CallerPrio
+ states:
+ - name: Nop
+ test-code: |
+ if ( ctx->count == 0 ) {
+ T_eq_u32( GetSelfPriority(), PRIO_HIGH );
+ ReleaseSemaphore( ctx );
+ } else {
+ T_eq_u32( GetSelfPriority(), PRIO_NORMAL );
+ }
+ text: |
+ The current priority of the task which called ${../if/set-priority:/name}
+ shall not be modified by the ${../if/set-priority:/name} call.
+ - name: New
+ test-code: |
+ T_eq_u32( GetSelfPriority(), PRIO_VERY_HIGH );
+ ReleaseSemaphore( ctx );
+ text: |
+ The current priority of the task which called ${../if/set-priority:/name}
+ shall be equal to the value of the ${../if/set-priority:/params[2]/name}
+ parameter.
+ test-epilogue: null
+ test-prologue: null
+- name: SemPrio
+ states:
+ - name: Set
+ test-code: |
+ if ( ( ctx->attribute_set & RTEMS_MULTIPROCESSOR_RESOURCE_SHARING ) != 0 ) {
+ if ( ctx->scheduler_id == ctx->other_scheduler_id ) {
+ CheckPriority( ctx, ctx->runner_scheduler_id, PRIO_HIGH );
+ CheckPriority( ctx, ctx->other_scheduler_id, PRIO_VERY_HIGH );
+ } else {
+ CheckPriority( ctx, ctx->runner_scheduler_id, PRIO_VERY_HIGH );
+ CheckPriority( ctx, ctx->other_scheduler_id, 0 );
+ }
+ } else if ( ( ctx->attribute_set & RTEMS_PRIORITY_CEILING ) != 0 ) {
+ CheckPriority( ctx, ctx->runner_scheduler_id, PRIO_VERY_HIGH );
+ CheckNotDefined( ctx, ctx->other_scheduler_id );
+ }
+ text: |
+ The priority used for the scheduler specified by the
+ ${../if/set-priority:/params[1]/name} parameter of the semaphore
+ associated with the identifier specified by the
+ ${../if/set-priority:/params[0]/name} parameter shall be set to the
+ prioriy specified by the ${../if/set-priority:/params[2]/name} parameter
+ during the ${../if/set-priority:/name} call.
+ - name: Nop
+ test-code: |
+ if ( ( ctx->attribute_set & RTEMS_MULTIPROCESSOR_RESOURCE_SHARING ) != 0 ) {
+ CheckPriority( ctx, ctx->runner_scheduler_id, PRIO_HIGH );
+ CheckPriority( ctx, ctx->other_scheduler_id, 0 );
+ } else if ( ( ctx->attribute_set & RTEMS_PRIORITY_CEILING ) != 0 ) {
+ CheckPriority( ctx, ctx->runner_scheduler_id, PRIO_HIGH );
+ CheckNotDefined( ctx, ctx->other_scheduler_id );
+ }
+ text: |
+ Priorities used by semaphores shall not be modified by the
+ ${../if/set-priority:/name} call.
+ test-epilogue: null
+ test-prologue: null
+- name: OldPrioVar
+ states:
+ - name: Set
+ test-code: |
+ T_eq_ptr( ctx->old_priority, &ctx->old_priority_value );
+
+ if ( ctx->scheduler_id == ctx->other_scheduler_id ) {
+ T_eq_u32( ctx->old_priority_value, 0 );
+ } else {
+ T_eq_u32( ctx->old_priority_value, PRIO_HIGH );
+ }
+ text: |
+ The value of the object referenced by the
+ ${../if/set-priority:/params[3]/name} parameter shall be set to the
+ priority used for the scheduler specified by the
+ ${../if/set-priority:/params[1]/name} parameter of the semaphore
+ associated with the identifier specified by the
+ ${../if/set-priority:/params[0]/name} parameter right before the priority
+ is set by the ${../if/set-priority:/name} call.
+ - name: Nop
+ test-code: |
+ T_eq_u32( ctx->old_priority_value, INVALID_PRIO );
+ text: |
+ Objects referenced by the ${../if/set-priority:/params[3]/name} parameter in
+ past calls to ${../if/set-priority:/name} shall not be accessed by the
+ ${../if/set-priority:/name} call.
+ test-epilogue: null
+ test-prologue: null
+pre-conditions:
+- name: OldPrio
+ states:
+ - name: Valid
+ test-code: |
+ ctx->old_priority = &ctx->old_priority_value;
+ text: |
+ While the ${../if/set-priority:/params[3]/name} parameter references an
+ object of type ${../../type/if/priority:/name}.
+ - name: 'Null'
+ test-code: |
+ ctx->old_priority = NULL;
+ text: |
+ While the ${../if/set-priority:/params[3]/name} parameter is
+ ${/c/if/null:/name}.
+ test-epilogue: null
+ test-prologue: null
+- name: SchedId
+ states:
+ - name: Invalid
+ test-code: |
+ ctx->scheduler_id = INVALID_ID;
+ text: |
+ While the ${../if/set-priority:/params[1]/name} parameter is not associated
+ with a scheduler.
+ - name: Create
+ test-code: |
+ ctx->scheduler_id = ctx->runner_scheduler_id;
+ text: |
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ the scheduler used to create the semaphore.
+ - name: Other
+ test-code: |
+ ctx->scheduler_id = ctx->other_scheduler_id;
+ text: |
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated
+ with a scheduler other than the one used to create the semaphore.
+ test-epilogue: null
+ test-prologue: null
+- name: SemId
+ states:
+ - name: NoObj
+ test-code: |
+ ctx->valid_id = false;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is not associated
+ with a semaphore.
+ - name: Counting
+ test-code: |
+ ctx->attribute_set |= RTEMS_COUNTING_SEMAPHORE;
+ text: |
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a counting semaphore.
+ - name: Simple
+ test-code: |
+ ctx->attribute_set |= RTEMS_SIMPLE_BINARY_SEMAPHORE;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a simple binary semaphore.
+ - name: Binary
+ test-code: |
+ ctx->attribute_set |= RTEMS_BINARY_SEMAPHORE;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a binary semaphore.
+ - name: PrioCeilingNoOwner
+ test-code: |
+ ctx->attribute_set |= RTEMS_BINARY_SEMAPHORE | RTEMS_PRIORITY_CEILING;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a priority ceiling semaphore, while the semaphore is has no owner.
+ - name: PrioCeilingOwner
+ test-code: |
+ ctx->attribute_set |= RTEMS_BINARY_SEMAPHORE | RTEMS_PRIORITY_CEILING;
+ ctx->count = 0;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a priority ceiling semaphore, while the semaphore has an owner.
+ - name: PrioInherit
+ test-code: |
+ ctx->attribute_set |= RTEMS_BINARY_SEMAPHORE | RTEMS_INHERIT_PRIORITY;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a priority inheritance semaphore.
+ - name: MrsP
+ test-code: |
+ ctx->attribute_set |= RTEMS_BINARY_SEMAPHORE |
+ RTEMS_MULTIPROCESSOR_RESOURCE_SHARING;
+ text: |
+ While the ${../if/set-priority:/params[0]/name} parameter is associated with
+ a MrsP semaphore.
+ test-epilogue: null
+ test-prologue: null
+- name: NewPrio
+ states:
+ - name: Current
+ test-code: |
+ ctx->new_priority = RTEMS_CURRENT_PRIORITY;
+ text: |
+ While the ${../if/set-priority:/params[2]/name} parameter is equal to
+ ${../../task/if/current-priority:/name}.
+ - name: Valid
+ test-code: |
+ ctx->new_priority = PRIO_VERY_HIGH;
+ text: |
+ While the ${../if/set-priority:/params[2]/name} parameter is not equal to
+ ${../../task/if/current-priority:/name} and valid with respect to the
+ scheduler specified by the ${../if/set-priority:/params[1]/name}
+ parameter.
+ - name: Invalid
+ test-code: |
+ ctx->new_priority = INVALID_PRIO;
+ text: |
+ While the ${../if/set-priority:/params[2]/name} parameter is invalid with
+ respect to the scheduler specified by the
+ ${../if/set-priority:/params[1]/name} parameter.
+ test-epilogue: null
+ test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons:
+ NoOtherScheduler: |
+ Where the system was built with SMP support disabled, exactly one scheduler
+ is present in an application.
+test-action: |
+ rtems_status_code sc;
+
+ sc = rtems_semaphore_create(
+ NAME,
+ ctx->count,
+ ctx->attribute_set,
+ PRIO_HIGH,
+ &ctx->the_semaphore_id
+ );
+ T_rsc_success( sc );
+
+ if ( ctx->valid_id ) {
+ ctx->semaphore_id = ctx->the_semaphore_id;
+ } else {
+ ctx->semaphore_id = INVALID_ID;
+ }
+
+ ctx->status = rtems_semaphore_set_priority(
+ ctx->semaphore_id,
+ ctx->scheduler_id,
+ ctx->new_priority,
+ ctx->old_priority
+ );
+test-brief: null
+test-cleanup: |
+ rtems_status_code sc;
+
+ sc = rtems_semaphore_delete( ctx->the_semaphore_id );
+ T_rsc_success( sc );
+test-context:
+- brief: |
+ This member contains the scheduler identifier of the runner task.
+ description: null
+ member: |
+ rtems_id runner_scheduler_id
+- brief: |
+ This member contains the scheduler identifier of a scheduler not used by
+ the runner task.
+ description: null
+ member: |
+ rtems_id other_scheduler_id
+- brief: |
+ This member specifies the initial count of the semaphore.
+ description: null
+ member: |
+ uint32_t count
+- brief: |
+ This member specifies the attribute set of the semaphore.
+ description: null
+ member: |
+ rtems_attribute attribute_set
+- brief: |
+ This member contains the semaphore identifier.
+ description: null
+ member: |
+ rtems_id the_semaphore_id
+- brief: |
+ If this member is true, then the ${../if/set-priority:/params[0]/name}
+ parameter shall be valid, otherwise it shall be ${/c/if/null:/name}.
+ description: null
+ member: |
+ bool valid_id
+- brief: |
+ This member may contain the task priority returned by
+ ${../if/set-priority:/name}.
+ description: null
+ member: |
+ rtems_task_priority old_priority_value
+- brief: |
+ This member specifies the ${../if/set-priority:/params[0]/name} parameter
+ for the ${../if/set-priority:/name} call.
+ description: null
+ member: |
+ rtems_id semaphore_id
+- brief: |
+ This member specifies the ${../if/set-priority:/params[1]/name} parameter
+ for the ${../if/set-priority:/name} call.
+ description: null
+ member: |
+ rtems_id scheduler_id
+- brief: |
+ This member specifies the ${../if/set-priority:/params[2]/name} parameter
+ for the ${../if/set-priority:/name} call.
+ description: null
+ member: |
+ rtems_task_priority new_priority
+- brief: |
+ This member specifies the ${../if/set-priority:/params[3]/name} parameter
+ for the ${../if/set-priority:/name} call.
+ description: null
+ member: |
+ rtems_task_priority *old_priority
+- brief: |
+ This member contains the status of the ${../if/set-priority:/name} call.
+ description: null
+ member: |
+ rtems_status_code status
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+- string.h
+test-local-includes:
+- tc-support.h
+- ts-config.h
+test-prepare: |
+ ctx->old_priority_value = INVALID_PRIO;
+ ctx->count = 1;
+ ctx->attribute_set = RTEMS_PRIORITY;
+ ctx->valid_id = true;
+test-setup:
+ brief: null
+ code: |
+ rtems_status_code sc;
+
+ memset( ctx, 0, sizeof( *ctx ) );
+ SetSelfPriority( PRIO_NORMAL );
+
+ sc = rtems_task_get_scheduler( RTEMS_SELF, &ctx->runner_scheduler_id );
+ T_rsc_success( sc );
+
+ #if defined(RTEMS_SMP)
+ sc = rtems_scheduler_ident(
+ CONFIG_SCHEDULER_B_NAME,
+ &ctx->other_scheduler_id
+ );
+ T_rsc_success( sc );
+ #else
+ ctx->other_scheduler_id = INVALID_ID;
+ #endif
+ description: null
+test-stop: null
+test-support: |
+ #define NAME rtems_build_name( 'T', 'E', 'S', 'T' )
+
+ #define INVALID_ID 0xffffffff
+
+ #define INVALID_PRIO 0xffffffff
+
+ typedef RtemsSemReqSetPriority_Context Context;
+
+ static void ReleaseSemaphore( const Context *ctx )
+ {
+ rtems_status_code sc;
+
+ sc = rtems_semaphore_release( ctx->the_semaphore_id );
+ T_rsc_success( sc );
+ }
+
+ static void SetScheduler( rtems_id scheduler_id )
+ {
+ #if defined(RTEMS_SMP)
+ rtems_status_code sc;
+
+ sc = rtems_task_set_scheduler( RTEMS_SELF, scheduler_id, PRIO_NORMAL );
+ T_rsc_success( sc );
+ #else
+ (void) scheduler_id;
+ #endif
+ }
+
+ static void CheckPriority(
+ const Context *ctx,
+ rtems_id scheduler_id,
+ rtems_task_priority priority
+ )
+ {
+ rtems_status_code sc;
+
+ SetScheduler( scheduler_id );
+
+ sc = rtems_semaphore_obtain(
+ ctx->the_semaphore_id,
+ RTEMS_WAIT,
+ RTEMS_NO_TIMEOUT
+ );
+ T_rsc_success( sc );
+
+ T_eq_u32( GetSelfPriority(), priority );
+
+ ReleaseSemaphore( ctx );
+ SetScheduler( ctx->runner_scheduler_id );
+ }
+
+ static void CheckNotDefined(
+ const Context *ctx,
+ rtems_id scheduler_id
+ )
+ {
+ #if defined(RTEMS_SMP)
+ rtems_status_code sc;
+
+ SetScheduler( scheduler_id );
+
+ sc = rtems_semaphore_obtain(
+ ctx->the_semaphore_id,
+ RTEMS_WAIT,
+ RTEMS_NO_TIMEOUT
+ );
+ T_rsc( sc, RTEMS_NOT_DEFINED );
+
+ SetScheduler( ctx->runner_scheduler_id );
+ #else
+ (void) ctx;
+ (void) scheduler_id;
+ #endif
+ }
+test-target: testsuites/validation/tc-sem-set-priority.c
+test-teardown:
+ brief: null
+ code: |
+ RestoreRunnerPriority();
+ description: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: InvAddr
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - 'Null'
+ SchedId:
+ SchedId:
+ - Invalid
+ - Create
+ SemId: all
+ NewPrio: all
+- enabled-by: true
+ post-conditions:
+ Status: InvId
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Invalid
+ SemId: all
+ NewPrio: all
+- enabled-by: true
+ post-conditions:
+ Status: InvId
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Create
+ SemId:
+ - NoObj
+ NewPrio: all
+- enabled-by: true
+ post-conditions:
+ Status: InvPrio
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Create
+ SemId:
+ - Counting
+ - Simple
+ - Binary
+ - PrioCeilingNoOwner
+ - PrioCeilingOwner
+ - PrioInherit
+ - MrsP
+ NewPrio:
+ - Invalid
+- enabled-by: true
+ post-conditions:
+ Status: NotDef
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Create
+ SemId:
+ - Counting
+ - Simple
+ - Binary
+ - PrioInherit
+ NewPrio:
+ - Current
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: Ok
+ CallerPrio:
+ - if:
+ pre-conditions:
+ SemId: PrioCeilingOwner
+ NewPrio: Valid
+ then: New
+ - else: Nop
+ SemPrio:
+ - if:
+ pre-conditions:
+ NewPrio: Current
+ then: Nop
+ - else: Set
+ OldPrioVar: Set
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Create
+ SemId:
+ - PrioCeilingNoOwner
+ - PrioCeilingOwner
+ - MrsP
+ NewPrio:
+ - Current
+ - Valid
+- enabled-by: true
+ post-conditions: NoOtherScheduler
+ pre-conditions:
+ OldPrio: all
+ SchedId:
+ - Other
+ SemId: all
+ NewPrio: all
+- enabled-by: RTEMS_SMP
+ post-conditions:
+ Status: InvAddr
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - 'Null'
+ SchedId:
+ SchedId:
+ - Other
+ SemId: all
+ NewPrio: all
+- enabled-by: RTEMS_SMP
+ post-conditions:
+ Status: InvId
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Create
+ - Other
+ SemId:
+ - NoObj
+ NewPrio: all
+- enabled-by: RTEMS_SMP
+ post-conditions:
+ Status: InvPrio
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Other
+ SemId:
+ - Counting
+ - Simple
+ - Binary
+ - PrioCeilingNoOwner
+ - PrioCeilingOwner
+ - PrioInherit
+ - MrsP
+ NewPrio:
+ - Invalid
+- enabled-by: RTEMS_SMP
+ post-conditions:
+ Status: NotDef
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Other
+ SemId:
+ - Counting
+ - Simple
+ - Binary
+ - PrioInherit
+ NewPrio:
+ - Current
+ - Valid
+- enabled-by: RTEMS_SMP
+ post-conditions:
+ Status: NotDef
+ CallerPrio: Nop
+ SemPrio: Nop
+ OldPrioVar: Nop
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Other
+ SemId:
+ - PrioCeilingNoOwner
+ - PrioCeilingOwner
+ NewPrio:
+ - Current
+ - Valid
+- enabled-by: RTEMS_SMP
+ post-conditions:
+ Status: Ok
+ CallerPrio: Nop
+ SemPrio:
+ - if:
+ pre-conditions:
+ NewPrio: Current
+ then: Nop
+ - else: Set
+ OldPrioVar: Set
+ pre-conditions:
+ OldPrio:
+ - Valid
+ SchedId:
+ - Other
+ SemId:
+ - MrsP
+ NewPrio:
+ - Current
+ - Valid
+type: requirement
More information about the vc
mailing list