[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