From d86a5d68a37c2014b87f84a13c794b60df8bcd8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20K=C3=BChndel?= Date: Wed, 30 Jun 2021 17:27:30 +0200 Subject: spec: Specify rate monotonic manager directives --- spec/rtems/ratemon/glossary/active.yml | 28 + spec/rtems/ratemon/glossary/consumed.yml | 15 + spec/rtems/ratemon/glossary/cputime.yml | 13 + spec/rtems/ratemon/glossary/deadline.yml | 34 + spec/rtems/ratemon/glossary/elapsed.yml | 16 + spec/rtems/ratemon/glossary/expired.yml | 24 + spec/rtems/ratemon/glossary/inactive.yml | 17 + spec/rtems/ratemon/glossary/interval.yml | 37 + spec/rtems/ratemon/glossary/job.yml | 17 + spec/rtems/ratemon/glossary/nop.yml | 14 + spec/rtems/ratemon/glossary/ownertask.yml | 17 + spec/rtems/ratemon/glossary/postponedjob.yml | 35 + spec/rtems/ratemon/glossary/scheduleroperation.yml | 19 + spec/rtems/ratemon/glossary/state.yml | 20 + spec/rtems/ratemon/glossary/time.yml | 12 + spec/rtems/ratemon/req/cancel.yml | 537 ++++++++++++ spec/rtems/ratemon/req/get-status.yml | 655 +++++++++++++++ spec/rtems/ratemon/req/period.yml | 932 +++++++++++++++++++++ 18 files changed, 2442 insertions(+) create mode 100644 spec/rtems/ratemon/glossary/active.yml create mode 100644 spec/rtems/ratemon/glossary/consumed.yml create mode 100644 spec/rtems/ratemon/glossary/cputime.yml create mode 100644 spec/rtems/ratemon/glossary/deadline.yml create mode 100644 spec/rtems/ratemon/glossary/elapsed.yml create mode 100644 spec/rtems/ratemon/glossary/expired.yml create mode 100644 spec/rtems/ratemon/glossary/inactive.yml create mode 100644 spec/rtems/ratemon/glossary/interval.yml create mode 100644 spec/rtems/ratemon/glossary/job.yml create mode 100644 spec/rtems/ratemon/glossary/nop.yml create mode 100644 spec/rtems/ratemon/glossary/ownertask.yml create mode 100644 spec/rtems/ratemon/glossary/postponedjob.yml create mode 100644 spec/rtems/ratemon/glossary/scheduleroperation.yml create mode 100644 spec/rtems/ratemon/glossary/state.yml create mode 100644 spec/rtems/ratemon/glossary/time.yml create mode 100644 spec/rtems/ratemon/req/cancel.yml create mode 100644 spec/rtems/ratemon/req/get-status.yml create mode 100644 spec/rtems/ratemon/req/period.yml diff --git a/spec/rtems/ratemon/glossary/active.yml b/spec/rtems/ratemon/glossary/active.yml new file mode 100644 index 00000000..036d7bbe --- /dev/null +++ b/spec/rtems/ratemon/glossary/active.yml @@ -0,0 +1,28 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: active +text: | + A period is in active ${../glossary/state:/term} if a time + ${../glossary/interval:/term} is set and the end + ${../glossary/deadline:/term} has not yet been reached. In active + ${../glossary/state:/term} either the ${../glossary/ownertask:/term} + executes the current ${../glossary/job:/term} or the + ${../glossary/ownertask:/term} is waiting for the end of the current + ${../glossary/interval:/term} inside the ${../if/period:/name} directive. + + A period enters active ${../glossary/state:/term} by a call to + ${../if/period:/name} if it was before in ${../glossary/inactive:/term} + or ${../glossary/expired:/term} ${../glossary/state:/term}. + + A period leaves active ${../glossary/state:/term} when the execution of the + current ${../glossary/job:/term} passes over the next + ${../glossary/deadline:/term} (no matter whether this + ${../glossary/deadline:/term} belongs to the current + ${../glossary/interval:/term} or not) or by a call to ${../if/cancel:/name}. +type: glossary diff --git a/spec/rtems/ratemon/glossary/consumed.yml b/spec/rtems/ratemon/glossary/consumed.yml new file mode 100644 index 00000000..9c0c1c4f --- /dev/null +++ b/spec/rtems/ratemon/glossary/consumed.yml @@ -0,0 +1,15 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: consumed +text: | + Consumed denotes the processor ${../glossary/cputime:/term} consumed by the + owner task since the last successful invocation of ${../if/period:/name} + (excluding the case where ${../if/period-status-define:/name} is used for + parameter ${../if/period:/params[1]/name}). +type: glossary diff --git a/spec/rtems/ratemon/glossary/cputime.yml b/spec/rtems/ratemon/glossary/cputime.yml new file mode 100644 index 00000000..5687b49d --- /dev/null +++ b/spec/rtems/ratemon/glossary/cputime.yml @@ -0,0 +1,13 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: CPU time +text: | + An amount of time during which a processor executed the + ${../glossary/ownertask:/term}. +type: glossary diff --git a/spec/rtems/ratemon/glossary/deadline.yml b/spec/rtems/ratemon/glossary/deadline.yml new file mode 100644 index 00000000..29bae547 --- /dev/null +++ b/spec/rtems/ratemon/glossary/deadline.yml @@ -0,0 +1,34 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: deadline +text: | + A deadline is a point in time. A sequence of deadlines each separated + from the next by the exact period length (i.e. parameter + ${../if/period:/params[1]/name}) form a theoretical ideal execution + sequence of ${../glossary/interval:/plural} of a rate monotonic period. + The return of the first call to ${../if/period:/name} which changes the + ${../glossary/state:/term} from ${../glossary/inactive:/term} to + ${../glossary/active:/term} defines the first deadline in this sequence. + + Ideally each ${../glossary/interval:/term} takes place between + a start and an end deadline whereby the N-th + ${../glossary/interval:/term} starts with the N-th deadline and ends + with the (N+1)-th deadline. Due to ${../glossary/postponedjob:/plural} + and ${../glossary/expired:/term} ${../glossary/state:/plural} + an ${../glossary/interval:/term} can be out-of-sync from this ideal + deadline sequence. In such a case it may start sometime after its + start deadline or even start after its end deadline has passed. + + If the period is in ${../glossary/active:/term} ${../glossary/state:/term} + and there are no ${../glossary/postponedjob:/plural}, the + ${../glossary/interval:/term} end is synchronized with the ideal end + deadline of the ${../glossary/interval:/term} by the + ${../if/period:/name} directive not returning before that end deadline + has passed. +type: glossary diff --git a/spec/rtems/ratemon/glossary/elapsed.yml b/spec/rtems/ratemon/glossary/elapsed.yml new file mode 100644 index 00000000..47c454e3 --- /dev/null +++ b/spec/rtems/ratemon/glossary/elapsed.yml @@ -0,0 +1,16 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: elapsed +text: | + Elapsed denotes the real ${../glossary/time:/term} passed since the last + successful invocation of ${../if/period:/name} (excluding the case where + ${../if/period-status-define:/name} is used for parameter + ${../if/period:/params[1]/name}). The elapsed time is measured using + ${/glossary/clock-monotonic:/term}. +type: glossary diff --git a/spec/rtems/ratemon/glossary/expired.yml b/spec/rtems/ratemon/glossary/expired.yml new file mode 100644 index 00000000..9b6db30b --- /dev/null +++ b/spec/rtems/ratemon/glossary/expired.yml @@ -0,0 +1,24 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: expired +text: | + A period is in expired ${../glossary/state:/term} if an + ${../glossary/interval:/term} is set and a + ${../glossary/deadline:/term} has passed while the current + ${../glossary/job:/term} is still executing. + + A period enters expired ${../glossary/state:/term} when the execution of the + current ${../glossary/job:/term} passes over the next + ${../glossary/deadline:/term} -- no matter whether this is the ideal end + ${../glossary/deadline:/term} of the current or any other + ${../glossary/interval:/term}. A period + leaves expired ${../glossary/state:/term} whenever the ${../if/period:/name} + directive (not using ${../if/period-status-define:/name} as value for + parameter ${../if/period:/params[1]/name}) is called. +type: glossary diff --git a/spec/rtems/ratemon/glossary/inactive.yml b/spec/rtems/ratemon/glossary/inactive.yml new file mode 100644 index 00000000..3ec97eed --- /dev/null +++ b/spec/rtems/ratemon/glossary/inactive.yml @@ -0,0 +1,17 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: inactive +text: | + A period is in inactive ${../glossary/state:/term} if no current + ${../glossary/interval:/term} is set. A period enters inactive + ${../glossary/state:/term} by a call to ${../if/create:/name} or + ${../if/cancel:/name}. A period leaves inactive state by a call to + ${../if/period:/name} (not using ${../if/period-status-define:/name} as value + for parameter ${../if/period:/params[1]/name}). +type: glossary diff --git a/spec/rtems/ratemon/glossary/interval.yml b/spec/rtems/ratemon/glossary/interval.yml new file mode 100644 index 00000000..711f5f69 --- /dev/null +++ b/spec/rtems/ratemon/glossary/interval.yml @@ -0,0 +1,37 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: interval +text: | + The current interval starts with the last return from a successful call to + ${../if/period:/name} which does not use ${../if/period-status-define:/name} + as value for parameter ${../if/period:/params[1]/name}. The current + interval ends with the return from the next successful call to + ${../if/period:/name} which does not use ${../if/period-status-define:/name} + as value for parameter ${../if/period:/params[1]/name}. See also + start/end ${../glossary/deadline:/term}. + + The parameter ${../if/period:/params[1]/name} of that call specifies the + interval length of the period. + + **Warning**: All calls to ${../if/period:/name} for the same period must + provide the same value for parameter ${../if/period:/params[1]/name}. That + is, the intervals of a period must have a strictly regular length. If that + is not the case and the period enters ${../glossary/expired:/term} + ${../glossary/state:/term}, future period ${../glossary/deadline:/term} are + set arbitrarily because the use of ${../glossary/postponedjob:/plural} + implicitly assumes a fixed time length for future + ${../glossary/job:/plural}. + + Note, an interval denotes a time while ${../glossary/job:/term} denotes code. + Note also, if a first call to ${../if/period:/name} which does not use + ${../if/period-status-define:/name} returned and a second + ${../if/period:/name} which does not use ${../if/period-status-define:/name} + is invoked but did not yet return, the current interval is still the one of + the first call. +type: glossary diff --git a/spec/rtems/ratemon/glossary/job.yml b/spec/rtems/ratemon/glossary/job.yml new file mode 100644 index 00000000..cdff78f6 --- /dev/null +++ b/spec/rtems/ratemon/glossary/job.yml @@ -0,0 +1,17 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: job +text: | + A job denotes the code which the ${../glossary/ownertask:/term} executes + between two successive calls to ${../if/period:/name} (excluding those using + ${../if/period-status-define:/name}). A job starts when the first + of these two ${../if/period:/name} calls returns. A job ends with the next + call to ${../if/period:/name} or a call to ${../if/cancel:/name} or + ${../if/delete:/name}. +type: glossary diff --git a/spec/rtems/ratemon/glossary/nop.yml b/spec/rtems/ratemon/glossary/nop.yml new file mode 100644 index 00000000..372e356b --- /dev/null +++ b/spec/rtems/ratemon/glossary/nop.yml @@ -0,0 +1,14 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: Nop +text: | + Nop means *no operation*. This term is used when directives do not return + ${../../status/if/successful:/name} as result. Nop indicates that the call of + a directive has no observable effect on any ${/glossary/rtems:/term} state. +type: glossary diff --git a/spec/rtems/ratemon/glossary/ownertask.yml b/spec/rtems/ratemon/glossary/ownertask.yml new file mode 100644 index 00000000..6419087e --- /dev/null +++ b/spec/rtems/ratemon/glossary/ownertask.yml @@ -0,0 +1,17 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: owner task +text: | + The owner ${/glossary/task:/term} of a period is the ${/glossary/task:/term} + which created it by successfully invoking ${../if/create:/name}. The + ${/glossary/task:/term} looses the ownership when the period is deleted + by a call to ${../if/delete:/name}. The ${../req/group:/name} permits + only the ${/glossary/task:/term} owning a period to invoke + ${../if/period:/name}. +type: glossary diff --git a/spec/rtems/ratemon/glossary/postponedjob.yml b/spec/rtems/ratemon/glossary/postponedjob.yml new file mode 100644 index 00000000..b16e32f3 --- /dev/null +++ b/spec/rtems/ratemon/glossary/postponedjob.yml @@ -0,0 +1,35 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: postponed job +text: | + A postponed job is a ${../glossary/job:/term} which should already have been + started but which has not yet been started because an earlier + ${../glossary/job:/term} is still executed. Postponed jobs exist in + ${../glossary/active:/term} and ${../glossary/expired:/term} + ${../glossary/state:/term}. + + Note that the ${../if/cancel:/name} + directive does not change the number of postponed jobs, + ${../glossary/elapsed:/term} or ${../glossary/consumed:/term} + ${../glossary/time:/term}. Moreover, the ${../if/create:/name} + directive does not set these values 0. + + The period has a counter for the number of currently postponed jobs (with a + maximum of 0xffffffff). The number of postponed jobs is increased whenever + the execution of the current ${../glossary/job:/term} exceeds the time + ${../glossary/interval:/term} length allotted for the current job (with the + ${../glossary/interval:/term} starting over again). This assumes and in + effect works only correct when all future jobs have the same + ${../glossary/interval:/term} length as the current one. + + If one or more postponed jobs are present when ${../if/period:/name} is + called, ${../if/period:/name} returns immediately without waiting for the + end of an ${../glossary/interval:/term} in an attempt to reduce the number + of postponed jobs. +type: glossary diff --git a/spec/rtems/ratemon/glossary/scheduleroperation.yml b/spec/rtems/ratemon/glossary/scheduleroperation.yml new file mode 100644 index 00000000..6d5d7602 --- /dev/null +++ b/spec/rtems/ratemon/glossary/scheduleroperation.yml @@ -0,0 +1,19 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: scheduler operation +text: | + When the ${../glossary/ownertask:/term} executes a ${../glossary/job:/term} of + a rate monotonic period, it often competes with other + ${/glossary/task:/plural} for CPU time. What exactly happens depends on the + ${/glossary/scheduler-home:/term} of the ${/glossary/task:/term}. Directives + like ${../if/period:/name} or ${../if/cancel:/name} invoke + ${/glossary/scheduler:/term} operations like ``release_job`` or ``cancel_job``. + The ${/glossary/scheduler-home:/term} often changes the + ${/glossary/priority-task:/term}. +type: glossary diff --git a/spec/rtems/ratemon/glossary/state.yml b/spec/rtems/ratemon/glossary/state.yml new file mode 100644 index 00000000..b7ee8235 --- /dev/null +++ b/spec/rtems/ratemon/glossary/state.yml @@ -0,0 +1,20 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: state +text: | + The rate monotonic state indicates whether the period is currently used to + execute ${../glossary/job:/plural} or not. In the former case it also + indicates whether the current ${../glossary/job:/term} is still within the + planed time ${../glossary/interval:/term} or not. A rate monotonic period can + be in one of these three states: + + * ${../glossary/inactive:/term} + * ${../glossary/active:/term} + * ${../glossary/expired:/term} +type: glossary diff --git a/spec/rtems/ratemon/glossary/time.yml b/spec/rtems/ratemon/glossary/time.yml new file mode 100644 index 00000000..bb47b0ae --- /dev/null +++ b/spec/rtems/ratemon/glossary/time.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: time +text: | + An amount of real time which passed. +type: glossary diff --git a/spec/rtems/ratemon/req/cancel.yml b/spec/rtems/ratemon/req/cancel.yml new file mode 100644 index 00000000..26aafd21 --- /dev/null +++ b/spec/rtems/ratemon/req/cancel.yml @@ -0,0 +1,537 @@ +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/cancel +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_rsc_success( ctx->status ); + text: | + The return status of ${../if/cancel:/name} shall be + ${../../status/if/successful:/name} + - name: InvId + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ID ); + text: | + The return status of ${../if/cancel:/name} shall be + ${../../status/if/invalid-id:/name}. + - name: NotOwn + test-code: | + T_rsc( ctx->status, RTEMS_NOT_OWNER_OF_RESOURCE ); + text: | + The return status of ${../if/cancel:/name} shall be + ${../../status/if/not-owner-of-resource:/name}. + test-epilogue: null + test-prologue: null +- name: State + states: + - name: Inactive + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_INACTIVE ); + text: | + The ${../glossary/state:/term} of the period shall be + ${../glossary/inactive:/term} after the return of the + ${../if/cancel:/name} call. + - name: Nop + test-code: | + T_eq_u32( ctx->period_status.state, ctx->previous_state ); + text: | + Objects referenced by the ${../if/cancel:/params[0]/name} + parameter in past calls to ${../if/cancel:/name} shall not be + accessed by the ${../if/cancel:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Postponed + states: + - name: Zero + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, 0 ); + text: | + There shall be no ${../glossary/postponedjob:/plural} + after the return of the ${../if/cancel:/name} call. + - name: One + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, 1 ); + text: | + The number of ${../glossary/postponedjob:/plural} shall not be + changed by the past call to ${../if/cancel:/name}. + - name: Several + test-code: | + T_eq_u32( + ctx->period_status.postponed_jobs_count, + ctx->postponed_jobs_count + ); + text: | + The number of ${../glossary/postponedjob:/plural} shall not be + changed by the past call to ${../if/cancel:/name}. + - name: Nop + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, + ctx->postponed_jobs_count ); + text: | + Objects referenced by the ${../if/cancel:/params[0]/name} + parameter in past calls to ${../if/cancel:/name} shall not be + accessed by the ${../if/cancel:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Scheduler + states: + - name: Called + test-code: | + /* Cannot be tested as the effect is unknown. */ + text: | + The last call of the ${../if/cancel:/name} function shall execute + the ``cancel_job`` ${../glossary/scheduleroperation:/term} of the + ${/glossary/scheduler-home:/term}. + - name: Nop + test-code: | + /* Cannot be tested as the effect is unknown. */ + text: | + The last call of the ${../if/cancel:/name} function shall not execute + any ${../glossary/scheduleroperation:/term}. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: Id + states: + - name: Valid + test-code: | + ctx->id_param = ctx->period_id; + text: | + While the ${../if/cancel:/params[0]/name} parameter is valid. + - name: Invalid + test-code: | + ctx->id_param = RTEMS_ID_NONE; + text: | + While the ${../if/cancel:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: Caller + states: + - name: OwnerTask + test-code: | + ctx->do_action = Action; + text: | + While the ${/glossary/task:/term} invoking ${../if/cancel:/name} is + the ${/glossary/task:/term} which created the period - + the ${../glossary/ownertask:/term}. + - name: OtherTask + test-code: | + ctx->do_action = WorkerTaskAction; + text: | + While the ${/glossary/task:/term} invoking ${../if/cancel:/name} is not + the ${../glossary/ownertask:/term}. + test-epilogue: null + test-prologue: null +- name: State + states: + - name: Inactive + test-code: | + /* Nothing to do here as the period is newly created. */ + ctx->previous_state = RATE_MONOTONIC_INACTIVE; + text: | + While the ${../if/cancel:/params[0]/name} parameter references an + period object in ${../glossary/inactive:/term} + ${../glossary/state:/term}. + - name: Active + test-code: | + rtems_status_code status; + status = rtems_rate_monotonic_period( ctx->period_id, period_length ); + T_rsc_success( status ); + ctx->previous_state = RATE_MONOTONIC_ACTIVE; + text: | + While the ${../if/cancel:/params[0]/name} parameter references an + period object in ${../glossary/active:/term} ${../glossary/state:/term}. + - name: Expired + test-code: | + rtems_status_code status; + status = rtems_rate_monotonic_period( ctx->period_id, period_length ); + T_rsc_success( status ); + ctx->previous_state = RATE_MONOTONIC_EXPIRED; + text: | + While the ${../if/cancel:/params[0]/name} parameter references an + period object in ${../glossary/expired:/term} + ${../glossary/state:/term}. + test-epilogue: null + test-prologue: null +- name: Postponed + states: + - name: Zero + test-code: | + ctx->postponed_jobs_count = 0; + text: | + While the period is not in ${../glossary/expired:/term} + ${../glossary/state:/term}. + - name: One + test-code: | + CreatePostponedJobs( ctx, 1 ); + text: | + While there is one ${../glossary/postponedjob:/term}. + - name: Several + test-code: | + CreatePostponedJobs( ctx, 5 ); + text: | + While there are two or more ${../glossary/postponedjob:/plural}. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: + NotInInactiveState: | + ${../glossary/postponedjob:/plural} do not exist in + ${../glossary/inactive:/term} ${../glossary/state:/term}. + NeverInExpiredState: | + There must be ${../glossary/postponedjob:/plural} in + ${../glossary/expired:/term} ${../glossary/state:/term}. +test-action: | + rtems_status_code status; + + ctx->do_action( ctx ); + + status = rtems_rate_monotonic_get_status( + ctx->period_id, + &ctx->period_status + ); + T_rsc_success( status ); +test-brief: null +test-cleanup: | + T_rsc_success( rtems_rate_monotonic_delete( ctx->period_id ) ); +test-context: +- brief: | + This member contains a valid identifier of a period. + description: null + member: | + rtems_id period_id +- brief: | + This member is used to receive the ${../if/period-status:/name} + after the action. + description: null + member: | + rtems_rate_monotonic_period_status period_status +- brief: | + This member specifies the ${../if/cancel:/params[0]/name} parameter + for the action. + description: null + member: | + rtems_id id_param +- brief: | + This member contains the returned ${/glossary/statuscode:/term} + of the action. + description: null + member: | + rtems_status_code status +- brief: | + This member contains the pointer to the function which executes the action. + description: | + The action is either executed by the ${../glossary/ownertask:/term} + or by the worker ${/glossary/task:/term} depending on the function pointer + used here. ``argument`` is a pointer to this context structure. + member: | + void ( *do_action )( void *ctx ) +- brief: | + This member contains the ${/glossary/task:/term} identifier of the + ${../glossary/ownertask:/term}. + description: null + member: | + rtems_id task_id +- brief: | + This member contains the ${/glossary/task:/term} identifier of the + worker ${/glossary/task:/term} (which is not the + ${../glossary/ownertask:/term}). + description: null + member: | + rtems_id worker_id +- brief: | + This member contains a backup of the ${/glossary/priority-task:/term} + before the execution of this test. + description: null + member: | + rtems_id original_priority +- brief: | + This member contains the number of ${../glossary/postponedjob:/plural} + before the action. + description: null + member: | + uint32_t postponed_jobs_count +- brief: | + This member contains the ${../glossary/state:/term} + before the action. + description: null + member: | + rtems_rate_monotonic_period_states previous_state +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +test-local-includes: +- tx-support.h +test-prepare: | + rtems_status_code status; + status = rtems_rate_monotonic_create( + rtems_build_name( 'R', 'M', 'O', 'N' ), + &ctx->period_id + ); + T_rsc_success( status ); + + ctx->postponed_jobs_count = 0; +test-setup: + brief: null + code: | + rtems_status_code status; + rtems_task_priority priority; + rtems_event_set event_set; + ctx->worker_id = RTEMS_INVALID_ID; + + status = rtems_task_ident( + RTEMS_SELF, + RTEMS_SEARCH_ALL_NODES, + &ctx->task_id + ); + T_rsc_success( status ); + + status = rtems_task_set_priority( + RTEMS_SELF, + RTEMS_CURRENT_PRIORITY, + &ctx->original_priority + ); + T_rsc_success( status ); + + status = rtems_task_set_priority( + RTEMS_SELF, + background_task_priority, + &priority + ); + T_rsc_success( status ); + + status = rtems_task_create( + rtems_build_name( 'W', 'O', 'R', 'K' ), + foreground_task_priority, + RTEMS_MINIMUM_STACK_SIZE, + RTEMS_DEFAULT_MODES, + RTEMS_DEFAULT_ATTRIBUTES, + &ctx->worker_id + ); + T_rsc_success( status ); + + /* Defensive programming: clean away any pending events */ + status = rtems_event_receive( + RTEMS_ALL_EVENTS, + RTEMS_NO_WAIT | RTEMS_EVENT_ANY, + RTEMS_NO_TIMEOUT, + &event_set + ); + T_true( status == RTEMS_SUCCESSFUL || status == RTEMS_UNSATISFIED ); + + status = rtems_task_start( + ctx->worker_id, + WorkerTask, + (rtems_task_argument) NULL + ); + T_rsc_success( status ); + description: null +test-stop: null +test-support: | + static const rtems_interval period_length = 5; + static const rtems_task_priority background_task_priority = 100; + static const rtems_task_priority foreground_task_priority = 10; + static const rtems_event_set wake_main_task_event = RTEMS_EVENT_17; + + static void TickTheClock( + RtemsRatemonReqCancel_Context *ctx, + uint32_t ticks + ) + { + uint32_t i; + for ( i = 0; i < ticks; ++i ) { + TimecounterTick(); + } + } + + static void Action( void *ctx_in ) + { + RtemsRatemonReqCancel_Context *ctx = ctx_in; + ctx->status = rtems_rate_monotonic_cancel( ctx->id_param ); + } + + RTEMS_INLINE_ROUTINE void WorkerTask( unsigned int argument ) + { + RtemsRatemonReqCancel_Context *ctx = + (RtemsRatemonReqCancel_Context *) argument; + + if ( ctx != NULL ) { + Action( ctx ); + T_rsc_success( rtems_event_send( ctx->task_id, wake_main_task_event ) ); + } + + T_rsc_success( rtems_task_suspend( RTEMS_SELF ) ); + } + + RTEMS_INLINE_ROUTINE void WorkerTaskAction( void *ctx_in ) + { + rtems_status_code status; + rtems_event_set event_set; + RtemsRatemonReqCancel_Context *ctx = ctx_in; + + status = rtems_task_restart( ctx->worker_id, (rtems_task_argument) ctx ); + T_rsc_success( status ); + + /* Wait till the worker task finishes */ + status = rtems_event_receive( + wake_main_task_event, + RTEMS_DEFAULT_OPTIONS, + RTEMS_NO_TIMEOUT, + &event_set + ); + T_rsc_success( status ); + } + + static void CreatePostponedJobs( + RtemsRatemonReqCancel_Context *ctx, + uint32_t jobs_count + ) + { + rtems_status_code status; + ctx->postponed_jobs_count = jobs_count; + if ( ctx->previous_state == RATE_MONOTONIC_ACTIVE ) { + TickTheClock( ctx, ( jobs_count + 1 ) * period_length ); + status = rtems_rate_monotonic_period( ctx->period_id, period_length ); + T_rsc( status, RTEMS_TIMEOUT ); + } else { + /* ctx->previous_state == RATE_MONOTONIC_INACTIVE || _EXPIRED */ + TickTheClock( ctx, jobs_count * period_length ); + } + } +test-target: testsuites/validation/tc-ratemon-cancel.c +test-teardown: + brief: null + code: | + rtems_status_code status; + rtems_task_priority priority; + + T_rsc_success( rtems_task_delete( ctx->worker_id ) ); + + status = rtems_task_set_priority( + RTEMS_SELF, + ctx->original_priority, + &priority + ); + T_rsc_success( status ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: Ok + State: Inactive + Postponed: N/A + Scheduler: Called + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + State: + - Inactive + Postponed: N/A +- enabled-by: true + post-conditions: + Status: Ok + State: Inactive + Postponed: + - specified-by: Postponed + Scheduler: Called + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + State: + - Active + - Expired + Postponed: all +- enabled-by: true + post-conditions: + Status: InvId + State: Nop + Postponed: Nop + Scheduler: Nop + pre-conditions: + Id: + - Invalid + Caller: all + State: + - Inactive + Postponed: N/A +- enabled-by: true + post-conditions: + Status: InvId + State: Nop + Postponed: Nop + Scheduler: Nop + pre-conditions: + Id: + - Invalid + Caller: all + State: + - Active + - Expired + Postponed: all +- enabled-by: true + post-conditions: + Status: NotOwn + State: Nop + Postponed: Nop + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OtherTask + State: + - Inactive + Postponed: N/A +- enabled-by: true + post-conditions: + Status: NotOwn + State: Nop + Postponed: Nop + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OtherTask + State: + - Active + - Expired + Postponed: all +- enabled-by: true + post-conditions: NotInInactiveState + pre-conditions: + Id: all + Caller: all + State: + - Inactive + Postponed: + - One + - Several +- enabled-by: true + post-conditions: NeverInExpiredState + pre-conditions: + Id: all + Caller: all + State: + - Expired + Postponed: + - Zero +type: requirement diff --git a/spec/rtems/ratemon/req/get-status.yml b/spec/rtems/ratemon/req/get-status.yml new file mode 100644 index 00000000..ea04c9ea --- /dev/null +++ b/spec/rtems/ratemon/req/get-status.yml @@ -0,0 +1,655 @@ +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/get-status +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_rsc_success( ctx->status ); + text: | + The return status of ${../if/get-status:/name} shall be + ${../../status/if/successful:/name} + - name: InvAddr + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); + text: | + The return status of ${../if/get-status:/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/get-status:/name} shall be + ${../../status/if/invalid-id:/name}. + test-epilogue: null + test-prologue: null +- name: Owner + states: + - name: OwnerTask + test-code: | + T_eq_u32( ctx->period_status.owner, ctx->task_id ); + text: | + The value of the member + ${../if/period-status:/definition[0]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to the object identifier of the + ${../glossary/ownertask:/term} of the period after the return of + the ${../if/get-status:/name} call. + - name: Nop + test-code: | + T_eq_u32( ctx->period_status.owner, initial_owner ); + text: | + Objects referenced by the ${../if/get-status:/params[1]/name} + parameter in past call to ${../if/get-status:/name} shall not be + accessed by the ${../if/get-status:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: State + states: + - name: Inactive + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_INACTIVE ); + text: | + The value of the member + ${../if/period-status:/definition[1]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} parameter + shall be set to ${../if/inactive:/name} after the return of the + ${../if/get-status:/name} call. (See also ${../glossary/inactive:/term}) + - name: Active + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_ACTIVE ); + text: | + The value of the member + ${../if/period-status:/definition[1]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} parameter + shall be set to ${../if/active:/name} after the return of the + ${../if/get-status:/name} call. (See also ${../glossary/active:/term}) + - name: Expired + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_EXPIRED ); + text: | + The value of the member + ${../if/period-status:/definition[1]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to ${../if/expired:/name} after the + return of the ${../if/get-status:/name} call. + (See also ${../glossary/expired:/term}) + - name: Nop + test-code: | + T_eq_u32( ctx->period_status.state, initial_state ); + text: | + Objects referenced by the ${../if/get-status:/params[1]/name} + parameter in past calls to ${../if/get-status:/name} shall not be + accessed by the ${../if/get-status:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Elapsed + states: + - name: Time + test-code: | + T_log( T_VERBOSE, "Elapsed: %lld.%ld (expected: %lld.%ld)", + ctx->period_status.since_last_period.tv_sec, + ctx->period_status.since_last_period.tv_nsec, + ctx->elapsed.tv_sec, + ctx->elapsed.tv_nsec + ); + T_eq_u64( + ctx->period_status.since_last_period.tv_sec, + ctx->elapsed.tv_sec + ); + /* period_status integer arithmetic is plagued by a rounding error. */ + T_le_long( + ctx->period_status.since_last_period.tv_nsec, + ctx->elapsed.tv_nsec + 1 + ); + T_ge_long( + ctx->period_status.since_last_period.tv_nsec, + ctx->elapsed.tv_nsec - 1 + ); + text: | + The value of the member + ${../if/period-status:/definition[2]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to the ${../glossary/time:/term} + ${../glossary/elapsed:/term}. + - name: Zero + test-code: | + T_eq_u64( ctx->period_status.since_last_period.tv_sec, 0 ); + T_eq_long( ctx->period_status.since_last_period.tv_nsec, 0 ); + text: | + The value of the member + ${../if/period-status:/definition[2]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to 0. + - name: Nop + test-code: | + T_eq_mem( + &ctx->period_status.since_last_period, + &initial_period, + sizeof( ctx->elapsed ) + ); + text: | + Objects referenced by the ${../if/get-status:/params[1]/name} + parameter in past calls to ${../if/get-status:/name} shall not be + accessed by the ${../if/get-status:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Consumed + states: + - name: CpuTime + test-code: | + T_log( T_VERBOSE, "CPU elapsed: %lld.%ld (expected: %lld.%ld)", + ctx->period_status.executed_since_last_period.tv_sec, + ctx->period_status.executed_since_last_period.tv_nsec, + ctx->consumed.tv_sec, + ctx->consumed.tv_nsec + ); + T_eq_u64( + ctx->period_status.executed_since_last_period.tv_sec, + ctx->consumed.tv_sec + ); + /* period_status integer arithmetic is plagued by a rounding error. */ + T_le_long( + ctx->period_status.executed_since_last_period.tv_nsec, + ctx->consumed.tv_nsec + 1 + ); + T_ge_long( + ctx->period_status.executed_since_last_period.tv_nsec, + ctx->consumed.tv_nsec - 1 + ); + text: | + The value of the member + ${../if/period-status:/definition[3]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to the ${../glossary/cputime:/term} + ${../glossary/consumed:/term} by the ${../glossary/ownertask:/term}. + - name: Zero + test-code: | + T_eq_u64( ctx->period_status.executed_since_last_period.tv_sec, 0 ); + T_eq_long( ctx->period_status.executed_since_last_period.tv_nsec, 0 ); + text: | + The value of the member + ${../if/period-status:/definition[2]/default/name} of the object + referenced by the ${../if/get-status:/params[1]/name} parameter + shall be set to 0. + - name: Nop + test-code: | + T_eq_mem( + &ctx->period_status.executed_since_last_period, + &initial_period, + sizeof( ctx->consumed ) + ); + text: | + Objects referenced by the ${../if/get-status:/params[1]/name} + parameter in past calls to ${../if/get-status:/name} shall not be + accessed by the ${../if/get-status:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Postponed + states: + - name: Zero + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, 0 ); + text: | + The value of the member + ${../if/period-status:/definition[4]/default/name} + of the object referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to 0 after the return of the + ${../if/get-status:/name} call. + - name: One + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, 1 ); + text: | + The value of the member + ${../if/period-status:/definition[4]/default/name} + of the object referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to the number of + ${../glossary/postponedjob:/plural} (here 1) after the return of + the ${../if/get-status:/name} call. + - name: Several + test-code: | + T_eq_u32( + ctx->period_status.postponed_jobs_count, + ctx->postponed_jobs_count + ); + text: | + The value of the member + ${../if/period-status:/definition[4]/default/name} + of the object referenced by the ${../if/get-status:/params[1]/name} + parameter shall be set to the number of + ${../glossary/postponedjob:/plural} after the return of the + ${../if/get-status:/name} call. + - name: Nop + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, + initial_postponed_jobs_count ); + text: | + Objects referenced by the ${../if/get-status:/params[1]/name} + parameter in past calls to ${../if/get-status:/name} shall not be + accessed by the ${../if/get-status:/name} call (see also + ${../glossary/nop:/term}). + + Note: A newly created period has an arbitrary the number of + ${../glossary/postponedjob:/plural} because ${../if/create:/name} + does not set this value 0. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: StatusAddr + states: + - name: Valid + test-code: | + ctx->status_param = &ctx->period_status; + text: | + While the ${../if/get-status:/params[1]/name} parameter references + an object of type ${../if/period-status:/name}. + - name: 'Null' + test-code: | + ctx->status_param = NULL; + text: | + While the ${../if/get-status:/params[1]/name} parameter is + ${/c/if/null:/name}. + test-epilogue: null + test-prologue: null +- name: Id + states: + - name: Valid + test-code: | + ctx->id_param = ctx->period_id; + text: | + While the ${../if/get-status:/params[0]/name} parameter is valid. + - name: Invalid + test-code: | + ctx->id_param = RTEMS_ID_NONE; + text: | + While the ${../if/get-status:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: State + states: + - name: Inactive + test-code: | + /* Nothing to do here as the period is newly created. */ + ctx->previous_state = RATE_MONOTONIC_INACTIVE; + text: | + While the ${../if/get-status:/params[0]/name} parameter references an + period object in ${../glossary/inactive:/term} + ${../glossary/state:/term}. + - name: Active + test-code: | + rtems_status_code status; + status = rtems_rate_monotonic_period( ctx->period_id, period_length ); + T_rsc_success( status ); + ctx->previous_state = RATE_MONOTONIC_ACTIVE; + text: | + While the ${../if/get-status:/params[0]/name} parameter references an + period object in ${../glossary/active:/term} ${../glossary/state:/term}. + - name: Expired + test-code: | + rtems_status_code status; + status = rtems_rate_monotonic_period( ctx->period_id, period_length ); + T_rsc_success( status ); + ctx->previous_state = RATE_MONOTONIC_EXPIRED; + text: | + While the ${../if/get-status:/params[0]/name} parameter references an + period object in ${../glossary/expired:/term} + ${../glossary/state:/term}. + test-epilogue: null + test-prologue: null +- name: Elapsed + states: + - name: Time + test-code: | + /* Time elapsed while having a CPU is added below in "CpuTime". */ + text: | + While a certain ${../glossary/time:/term} of the + ${/glossary/clock-monotonic:/term} has ${../glossary/elapsed:/term}. + test-epilogue: null + test-prologue: null +- name: Consumed + states: + - name: CpuTime + test-code: | + TickTheClock( ctx, elapsed_cpu_ticks ); + ctx->consumed.tv_nsec += + rtems_configuration_get_nanoseconds_per_tick() * elapsed_cpu_ticks; + text: | + While the owner ${/glossary/task:/term} has ${../glossary/consumed:/term} + a certain amount of ${../glossary/cputime:/term}. + test-epilogue: null + test-prologue: null +- name: Postponed + states: + - name: Zero + test-code: | + ctx->postponed_jobs_count = 0; + text: | + While the period is not in ${../glossary/expired:/term} + ${../glossary/state:/term}. + - name: One + test-code: | + CreatePostponedJobs( ctx, 1 ); + text: | + While there is one ${../glossary/postponedjob:/term}. + - name: Several + test-code: | + CreatePostponedJobs( ctx, 5 ); + text: | + While there are two or more ${../glossary/postponedjob:/term}. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: + NotInInactiveState: | + ${../glossary/postponedjob:/plural} do not exist in + ${../glossary/inactive:/term} ${../glossary/state:/term}. + NeverInExpiredState: | + There must be ${../glossary/postponedjob:/plural} in + ${../glossary/expired:/term} ${../glossary/state:/term}. +test-action: | + ctx->status = rtems_rate_monotonic_get_status( + ctx->id_param, + ctx->status_param + ); +test-brief: null +test-cleanup: | + T_rsc_success( rtems_rate_monotonic_delete( ctx->period_id ) ); +test-context: +- brief: | + This member contains a valid identifier of a period. + description: null + member: | + rtems_id period_id +- brief: | + This member contains the previous timecounter handler to restore. + description: null + member: | + GetTimecountHandler previous_timecounter_handler +- brief: | + This member is used to receive the ${../if/period-status:/name} + from the action. + description: null + member: | + rtems_rate_monotonic_period_status period_status +- brief: | + This member specifies the ${../if/get-status:/params[0]/name} parameter + for the action. + description: null + member: | + rtems_id id_param +- brief: | + This member specifies the ${../if/get-status:/params[1]/name} parameter + for the action. + description: null + member: | + rtems_rate_monotonic_period_status *status_param +- brief: | + This member contains the returned ${/glossary/statuscode:/term} + of the action. + description: null + member: | + rtems_status_code status +- brief: | + This member contains the ${/glossary/task:/term} identifier of the + ${../glossary/ownertask:/term}. + description: null + member: | + rtems_id task_id +- brief: | + This member contains the ${../glossary/state:/term} + before the action. + description: null + member: | + rtems_rate_monotonic_period_states previous_state +- brief: | + This member contains the ${/glossary/clock-monotonic:/term} + ${../glossary/time:/term} ${../glossary/elapsed:/term}. + description: null + member: | + struct timespec elapsed +- brief: | + This member contains the ${../glossary/cputime:/term} + ${../glossary/consumed:/term} by the ${../glossary/ownertask:/term}. + description: null + member: | + struct timespec consumed +- brief: | + This member contains the number of ${../glossary/postponedjob:/plural}. + description: null + member: | + uint32_t postponed_jobs_count +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +test-local-includes: +- tx-support.h +test-prepare: | + rtems_status_code status; + status = rtems_rate_monotonic_create( + rtems_build_name( 'R', 'M', 'O', 'N' ), + &ctx->period_id + ); + T_rsc_success( status ); + + ctx->period_status = (rtems_rate_monotonic_period_status) { + .owner = initial_owner, + .state = initial_state, + .since_last_period = initial_period, + .executed_since_last_period = initial_period, + .postponed_jobs_count = initial_postponed_jobs_count + }; + + ctx->elapsed.tv_sec = 0; + ctx->elapsed.tv_nsec = 0; + ctx->consumed.tv_sec = 0; + ctx->consumed.tv_nsec = 0; + ctx->postponed_jobs_count = 0; +test-setup: + brief: null + code: | + ctx->previous_timecounter_handler = SetGetTimecountHandler( FreezeTime ); + ctx->task_id = rtems_task_self(); + description: null +test-stop: null +test-support: | + static const rtems_id initial_owner = 0xFFFFFFFF; + static const rtems_rate_monotonic_period_states initial_state = + (rtems_rate_monotonic_period_states) 0xFFFFFFFF; + static const struct timespec initial_period = { 0xFFFFFFFF, 0xFFFFFFFF }; + static const uint32_t initial_postponed_jobs_count = 0xFFFFFFFF; + static const rtems_interval period_length = 5; + static const uint32_t elapsed_cpu_ticks = 3; + + static uint32_t FreezeTime( void ) + { + return GetTimecountCounter() - 1; + } + + static void TickTheClock( + RtemsRatemonReqGetStatus_Context *ctx, + uint32_t ticks + ) + { + uint32_t i; + for ( i = 0; i < ticks; ++i ) { + TimecounterTick(); + } + ctx->elapsed.tv_nsec += + rtems_configuration_get_nanoseconds_per_tick() * ticks; + } + + static void CreatePostponedJobs( + RtemsRatemonReqGetStatus_Context *ctx, + uint32_t jobs_count + ) + { + rtems_status_code status; + ctx->postponed_jobs_count = jobs_count; + if ( ctx->previous_state == RATE_MONOTONIC_ACTIVE ) { + jobs_count++; + TickTheClock( ctx, jobs_count * period_length ); + status = rtems_rate_monotonic_period( ctx->period_id, period_length ); + T_rsc( status, RTEMS_TIMEOUT ); + } else { + /* ctx->previous_state == RATE_MONOTONIC_INACTIVE || _EXPIRED */ + TickTheClock( ctx, jobs_count * period_length ); + } + ctx->consumed.tv_nsec += + rtems_configuration_get_nanoseconds_per_tick() * + jobs_count * period_length; + } +test-target: testsuites/validation/tc-ratemon-get-status.c +test-teardown: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: Ok + Owner: OwnerTask + State: Inactive + Elapsed: N/A + Consumed: N/A + Postponed: N/A + pre-conditions: + StatusAddr: + - Valid + Id: + - Valid + State: + - Inactive + Elapsed: N/A + Consumed: N/A + Postponed: N/A +- enabled-by: true + post-conditions: + Status: Ok + Owner: OwnerTask + State: + - specified-by: State + Elapsed: Time + Consumed: CpuTime + Postponed: + - specified-by: Postponed + pre-conditions: + StatusAddr: + - Valid + Id: + - Valid + State: + - Active + - Expired + Elapsed: + - Time + Consumed: + - CpuTime + Postponed: all +- enabled-by: true + post-conditions: + Status: InvAddr + Owner: Nop + State: Nop + Elapsed: Nop + Consumed: Nop + Postponed: Nop + pre-conditions: + StatusAddr: + - 'Null' + Id: all + State: + - Inactive + Elapsed: all + Consumed: all + Postponed: N/A +- enabled-by: true + post-conditions: + Status: InvAddr + Owner: Nop + State: Nop + Elapsed: Nop + Consumed: Nop + Postponed: Nop + pre-conditions: + StatusAddr: + - 'Null' + Id: all + State: + - Active + - Expired + Elapsed: all + Consumed: all + Postponed: all +- enabled-by: true + post-conditions: + Status: InvId + Owner: Nop + State: Nop + Elapsed: Nop + Consumed: Nop + Postponed: Nop + pre-conditions: + StatusAddr: + - Valid + Id: + - Invalid + State: + - Inactive + Elapsed: all + Consumed: all + Postponed: N/A +- enabled-by: true + post-conditions: + Status: InvId + Owner: Nop + State: Nop + Elapsed: Nop + Consumed: Nop + Postponed: Nop + pre-conditions: + StatusAddr: + - Valid + Id: + - Invalid + State: + - Active + - Expired + Elapsed: all + Consumed: all + Postponed: all +- enabled-by: true + post-conditions: NotInInactiveState + pre-conditions: + StatusAddr: all + Id: all + State: + - Inactive + Elapsed: all + Consumed: all + Postponed: + - One + - Several +- enabled-by: true + post-conditions: NeverInExpiredState + pre-conditions: + StatusAddr: all + Id: all + State: + - Expired + Elapsed: all + Consumed: all + Postponed: + - Zero +type: requirement diff --git a/spec/rtems/ratemon/req/period.yml b/spec/rtems/ratemon/req/period.yml new file mode 100644 index 00000000..7d5674f3 --- /dev/null +++ b/spec/rtems/ratemon/req/period.yml @@ -0,0 +1,932 @@ +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/period +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_rsc_success( ctx->status ); + text: | + The return status of ${../if/period:/name} shall be + ${../../status/if/successful:/name} + - name: InvId + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ID ); + text: | + The return status of ${../if/period:/name} shall be + ${../../status/if/invalid-id:/name}. + - name: NotOwn + test-code: | + T_rsc( ctx->status, RTEMS_NOT_OWNER_OF_RESOURCE ); + text: | + The return status of ${../if/period:/name} shall be + ${../../status/if/not-owner-of-resource:/name}. + - name: NotDef + test-code: | + T_rsc( ctx->status, RTEMS_NOT_DEFINED ); + text: | + The return status of ${../if/period:/name} shall be + ${../../status/if/not-defined:/name}. + - name: TimeOut + test-code: | + T_rsc( ctx->status, RTEMS_TIMEOUT ); + text: | + The return status of ${../if/period:/name} shall be + ${../../status/if/timeout:/name}. + test-epilogue: null + test-prologue: null +- name: State + states: + - name: Inactive + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_INACTIVE ); + text: | + The ${../glossary/state:/term} of the period shall be + ${../glossary/inactive:/term} after the return of the + ${../if/period:/name} call. + - name: Active + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_ACTIVE ); + text: | + The ${../glossary/state:/term} of the period shall be + ${../if/active:/name} after the return of the + ${../if/period:/name} call. + - name: Expired + test-code: | + T_eq_int( ctx->period_status.state, RATE_MONOTONIC_EXPIRED ); + text: | + The ${../glossary/state:/term} of the period shall be + ${../if/expired:/name} after the return of the + ${../if/period:/name} call. + - name: Nop + test-code: | + T_eq_u32( ctx->period_status.state, ctx->previous_state ); + text: | + Objects referenced by the ${../if/period:/params[0]/name} + parameter in past calls to ${../if/period:/name} shall not be + accessed by the ${../if/period:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Postponed + states: + - name: Zero + test-code: | + T_eq_u32( ctx->period_status.postponed_jobs_count, 0 ); + text: | + There shall be no ${../glossary/postponedjob:/plural} + after the return of the ${../if/period:/name} call. + - name: OneOrMore + test-code: | + T_eq_u32( + ctx->period_status.postponed_jobs_count, + ( ctx->test_duration / period_length + 1 ) - ctx->period_calls + ); + text: | + The number of ${../glossary/postponedjob:/plural} shall be + the number of ${../glossary/deadline:/plural} passed + minus the number of returned calls to ${../if/period:/name}. + + The last call to ${../if/period:/name} where the + ${../glossary/state:/term} changes from ${../glossary/inactive:/term} + to ${../if/active:/name} is counted as the first returned call. + The first deadline occurred at a point in time during that call + to ${../if/period:/name}. + - name: Nop + test-code: | + T_eq_u32( + ctx->period_status.postponed_jobs_count, + ctx->postponed_jobs_count + ); + text: | + Objects referenced by the ${../if/period:/params[0]/name} + parameter in past calls to ${../if/period:/name} shall not be + accessed by the ${../if/period:/name} call (see also + ${../glossary/nop:/term}). + + Note: A newly created period has an arbitrary the number of + ${../glossary/postponedjob:/plural} because ${../if/create:/name} + does not set this value 0. + test-epilogue: null + test-prologue: null +- name: Delay + states: + - name: None + test-code: | + T_eq_u32( ctx->action_duration, 0 ); + text: | + The last call to ${../if/period:/name} shall return without delay. + - name: TillDeadline + test-code: | + T_eq_u32( + ctx->action_duration, + ( ctx->test_duration_till_action % period_length + 1 ) * period_length - + ctx->test_duration_till_action + ); + text: | + The last call to ${../if/period:/name} shall block the + ${../glossary/ownertask:/term} till the next ${../glossary/deadline:/term} + and return afterwards. + test-epilogue: null + test-prologue: null +- name: Scheduler + states: + - name: Called + test-code: | + /* Cannot be tested as the effect is unknown. */ + text: | + The last call of the ${../if/period:/name} function shall execute + the ``release_job`` ${../glossary/scheduleroperation:/term} of the + ${/glossary/scheduler-home:/term}. + - name: Nop + test-code: | + /* Cannot be tested as the effect is unknown. */ + text: | + The last call of the ${../if/period:/name} function shall not execute + any ${../glossary/scheduleroperation:/term}. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: Id + states: + - name: Valid + test-code: | + ctx->id_param = ctx->period_id; + text: | + While the ${../if/period:/params[0]/name} parameter is valid. + - name: Invalid + test-code: | + ctx->id_param = RTEMS_ID_NONE; + text: | + While the ${../if/period:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: Caller + states: + - name: OwnerTask + test-code: | + ctx->do_action = OwnerDoWork; + text: | + While the ${/glossary/task:/term} invoking ${../if/period:/name} is the + ${/glossary/task:/term} which created the period + - the ${../glossary/ownertask:/term}. + - name: OtherTask + test-code: | + ctx->do_action = OtherDoWork; + text: | + While the ${/glossary/task:/term} invoking ${../if/period:/name} is not + the ${../glossary/ownertask:/term}. + test-epilogue: null + test-prologue: null +- name: Length + states: + - name: Ticks + test-code: | + ctx->length_param = period_length; + text: | + While the ${../if/period:/params[1]/name} parameter is a number larger + than 0. + + Note: + + * ${../if/period-status-define:/name} == 0 + + * The ${../if/period:/params[1]/name} parameter of all calls to + ${../if/period:/name} must have the same value (see + ${../glossary/interval:/term}). + - name: Status + test-code: | + ctx->length_param = RTEMS_PERIOD_STATUS; + text: | + While the ${../if/period:/params[1]/name} parameter is + ${../if/period-status-define:/name}. + test-epilogue: null + test-prologue: null +- name: State + states: + - name: Inactive + test-code: | + /* Nothing to do here as the period is newly created. */ + ctx->previous_state = RATE_MONOTONIC_INACTIVE; + text: | + While the ${../if/period:/params[0]/name} parameter references an + period object in ${../glossary/inactive:/term} + ${../glossary/state:/term}. + - name: Active + test-code: | + OwnerDoWork( ctx, CallPeriod ); + ctx->previous_state = RATE_MONOTONIC_ACTIVE; + text: | + While the ${../if/period:/params[0]/name} parameter references an + period object in ${../glossary/active:/term} ${../glossary/state:/term}. + - name: Expired + test-code: | + OwnerDoWork( ctx, CallPeriod ); + ctx->previous_state = RATE_MONOTONIC_EXPIRED; + text: | + While the ${../if/period:/params[0]/name} parameter references an + period object in ${../glossary/expired:/term} + ${../glossary/state:/term}. + test-epilogue: null + test-prologue: null +- name: Postponed + states: + - name: Zero + test-code: | + ctx->postponed_jobs_count = 0; + text: | + While there is no ${../glossary/postponedjob:/term}. + - name: One + test-code: | + CreatePostponedJobs( ctx, 1 ); + text: | + While there is one ${../glossary/postponedjob:/term}. + - name: Several + test-code: | + CreatePostponedJobs( ctx, 5 ); + text: | + While there are two or more ${../glossary/postponedjob:/plural}. + test-epilogue: null + test-prologue: null +- name: InactiveCause + states: + - name: New + test-code: | + /* Nothing to do here as the period is newly created. */ + text: | + While ${../if/period:/name} has never been invoked with result + ${../../status/if/successful:/name} on the period object referenced + by the ${../if/period:/params[0]/name} parameter since that + period object has been created. + - name: Canceled + test-code: | + if ( ctx->period_calls == 0 ) { + OwnerDoWork( ctx, CallPeriod ); + TickTheClock( ctx, ctx->postponed_jobs_count * period_length ); + } + OwnerDoWork( ctx, CancelPeriod ); + text: | + While ${../if/period:/name} has never been invoked with result + ${../../status/if/successful:/name} on the period object referenced + by the ${../if/period:/params[0]/name} parameter since that + period object has been canceled using ${../if/cancel:/name}. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: + NeverInExpiredState: | + There must be ${../glossary/postponedjob:/plural} in + ${../glossary/expired:/term} ${../glossary/state:/term}. +test-action: | + rtems_status_code status; + + ctx->test_duration_till_action = ctx->test_duration; + ctx->action_duration = ctx->do_action( ctx, DoAction ); + + status = rtems_rate_monotonic_get_status( + ctx->period_id, + &ctx->period_status + ); + T_rsc_success( status ); +test-brief: null +test-cleanup: | + OwnerDoWork( ctx, DeletePeriod ); +test-context: +- brief: | + This member contains a valid identifier of a period. + description: null + member: | + rtems_id period_id +- brief: | + This member is used to receive the ${../if/period-status:/name} + after the action. + description: null + member: | + rtems_rate_monotonic_period_status period_status +- brief: | + This member specifies the ${../if/period:/params[0]/name} parameter + for the action. + description: null + member: | + rtems_id id_param +- brief: | + This member specifies the ${../if/period:/params[1]/name} parameter + for the action. + description: null + member: | + rtems_interval length_param +- brief: | + This member contains the returned ${/glossary/statuscode:/term} + of the action. + description: null + member: | + rtems_status_code status +- brief: | + This member contains the pointer to the function which executes the action. + description: | + The action is either executed by the ${../glossary/ownertask:/term} + or by the worker ${/glossary/task:/term} depending on the function + pointer used here. ``ctx_arg`` must be a pointer to this context + structure. + member: | + uint32_t ( *do_action )( void *ctx, void (*todo)( void *ctx_arg ) ) +- brief: | + This member serves to pass the pointer to the function + which the work ${../glossary/ownertask:/term} shall execute from + function ``OwnerDoWork`` to function ``WorkerTask``. + description: null + member: | + void (*worker_todo)( void *ctx ) +- brief: | + This member contains the ${../glossary/ownertask:/term} identifier of the + ${../glossary/ownertask:/term}. + description: null + member: | + rtems_id task_id +- brief: | + This member contains the ${../glossary/ownertask:/term} identifier of the + worker task (which is not the ${../glossary/ownertask:/term}). + description: null + member: | + rtems_id worker_id +- brief: | + This member contains a backup of the ${/glossary/priority-task:/term} + before the execution of this test. + description: null + member: | + rtems_id original_priority +- brief: | + This member contains the number of ${../glossary/postponedjob:/plural} + before the action. + description: null + member: | + uint32_t postponed_jobs_count +- brief: | + This member contains the ${../glossary/state:/term} + before the action. + description: null + member: | + rtems_rate_monotonic_period_states previous_state +- brief: | + This member contains the number of ${/glossary/clock-tick:/plural} passed + since the test started. + description: null + member: | + uint32_t test_duration +- brief: | + This member contains the number of ${/glossary/clock-tick:/plural} passed + since the test started till (before) the ${../if/period:/name} action + is invoked. + description: null + member: | + uint32_t test_duration_till_action +- brief: | + This member contains the number of times the ${../if/period:/name} + function returned since the test started. + description: null + member: | + uint32_t period_calls +- brief: | + This member contains the number of ${/glossary/clock-tick:/plural} + which passed in the action till the ${../if/period:/name} + function returned. + description: null + member: | + uint32_t action_duration +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +test-local-includes: +- tx-support.h +test-prepare: | + rtems_status_code status; + rtems_rate_monotonic_period_status period_status; + ctx->test_duration = 0; + ctx->period_calls = 0; + OwnerDoWork( ctx, CreatePeriod ); + + /* + * In case of a new period the postponed jobs count is arbitrary + * (what ever value happens to be stored in that field of the internal data + * structure) until period() is called. + */ + status = rtems_rate_monotonic_get_status( + ctx->period_id, + &period_status + ); + T_rsc_success( status ); + ctx->postponed_jobs_count = period_status.postponed_jobs_count; +test-setup: + brief: null + code: | + rtems_status_code status; + rtems_task_priority priority; + rtems_event_set event_set; + ctx->worker_id = RTEMS_INVALID_ID; + + status = rtems_task_ident( + RTEMS_SELF, + RTEMS_SEARCH_ALL_NODES, + &ctx->task_id + ); + T_rsc_success( status ); + + status = rtems_task_set_priority( + RTEMS_SELF, + RTEMS_CURRENT_PRIORITY, + &ctx->original_priority + ); + T_rsc_success( status ); + + status = rtems_task_set_priority( + RTEMS_SELF, + background_task_priority, + &priority + ); + T_rsc_success( status ); + + status = rtems_task_create( + rtems_build_name( 'W', 'O', 'R', 'K' ), + foreground_task_priority, + RTEMS_MINIMUM_STACK_SIZE, + RTEMS_DEFAULT_MODES, + RTEMS_DEFAULT_ATTRIBUTES, + &ctx->worker_id + ); + T_rsc_success( status ); + + /* Defensive programming: clean away any pending events */ + status = rtems_event_receive( + RTEMS_ALL_EVENTS, + RTEMS_NO_WAIT | RTEMS_EVENT_ANY, + RTEMS_NO_TIMEOUT, + &event_set + ); + T_true( status == RTEMS_SUCCESSFUL || status == RTEMS_UNSATISFIED ); + + status = rtems_task_start( + ctx->worker_id, + WorkerTask, + (rtems_task_argument) NULL + ); + T_rsc_success( status ); + description: null +test-stop: null +test-support: | + static const rtems_interval period_length = 5; + static const rtems_task_priority background_task_priority = 100; + static const rtems_task_priority foreground_task_priority = 10; + static const rtems_event_set wake_main_task_event = RTEMS_EVENT_17; + + static void TickTheClock( + RtemsRatemonReqPeriod_Context *ctx, + uint32_t ticks + ) + { + uint32_t i; + for ( i = 0; i < ticks; ++i ) { + TimecounterTick(); + ctx->test_duration++; + } + } + + static rtems_status_code CallPeriodFunction( + RtemsRatemonReqPeriod_Context *ctx, + rtems_id id, + rtems_interval length + ) + { + rtems_status_code status; + status = rtems_rate_monotonic_period( id, length ); + ctx->period_calls++; + return status; + } + + RTEMS_INLINE_ROUTINE void CreatePeriod( void *ctx_in ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + rtems_status_code status; + status = rtems_rate_monotonic_create( + rtems_build_name( 'R', 'M', 'O', 'N' ), + &ctx->period_id + ); + T_rsc_success( status ); + } + + RTEMS_INLINE_ROUTINE void DeletePeriod( void *ctx_in ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + T_rsc_success( rtems_rate_monotonic_delete( ctx->period_id ) ); + } + + RTEMS_INLINE_ROUTINE void CancelPeriod( void *ctx_in ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + T_rsc_success( rtems_rate_monotonic_cancel( ctx->period_id ) ); + } + + RTEMS_INLINE_ROUTINE void CallPeriod( void *ctx_in ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + T_rsc_success( CallPeriodFunction( ctx, ctx->period_id, period_length ) ); + } + + RTEMS_INLINE_ROUTINE void CallPeriodTimeout( void *ctx_in ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + rtems_status_code status; + status = CallPeriodFunction( ctx, ctx->period_id, period_length ); + T_rsc( status, RTEMS_TIMEOUT ); + } + + RTEMS_INLINE_ROUTINE void DoAction( void *ctx_in ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + ctx->status = CallPeriodFunction( ctx, ctx->id_param, ctx->length_param ); + } + + RTEMS_INLINE_ROUTINE void WorkerTask( unsigned int argument ) + { + RtemsRatemonReqPeriod_Context *ctx = + (RtemsRatemonReqPeriod_Context *) argument; + if ( ctx != NULL ) { + ctx->worker_todo( ctx ); + T_rsc_success( rtems_event_send( ctx->task_id, wake_main_task_event ) ); + } + T_rsc_success( rtems_task_suspend( RTEMS_SELF ) ); + } + + static uint32_t OwnerDoWork( void *ctx_in, void (*todo)( void *ctx_arg ) ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + uint32_t ticks_to_wait = period_length + 1; + rtems_status_code status; + rtems_event_set event_set; + + ctx->worker_todo = todo; + status = rtems_task_restart( ctx->worker_id, (rtems_task_argument) ctx ); + T_rsc_success( status ); + + for ( ; ticks_to_wait > 0; --ticks_to_wait ) { + /* Check whether the worker finished executing the action */ + status = rtems_event_receive( + RTEMS_PENDING_EVENTS, + RTEMS_NO_WAIT | RTEMS_EVENT_ANY, + RTEMS_NO_TIMEOUT, + &event_set + ); + T_rsc_success( status ); + + if ( ( event_set & wake_main_task_event ) == wake_main_task_event ) { + break; + } + TickTheClock( ctx, 1 ); + } + + /* Wait till the worker task finishes */ + status = rtems_event_receive( + wake_main_task_event, + RTEMS_DEFAULT_OPTIONS, + RTEMS_NO_TIMEOUT, + &event_set + ); + T_rsc_success( status ); + + return period_length + 1 - ticks_to_wait; + } + + static uint32_t OtherDoWork( void *ctx_in, void (*todo)( void *ctx_arg ) ) + { + RtemsRatemonReqPeriod_Context *ctx = ctx_in; + todo( ctx ); + /* Duration = 0 ticks as DoAction() does not call TickTheClock() */ + return 0; + } + + static void CreatePostponedJobs( + RtemsRatemonReqPeriod_Context *ctx, + uint32_t jobs_count + ) + { + ctx->postponed_jobs_count = jobs_count; + if ( ctx->previous_state == RATE_MONOTONIC_ACTIVE ) { + TickTheClock( ctx, ( jobs_count + 1 ) * period_length ); + OwnerDoWork( ctx, CallPeriodTimeout ); + } else { + /* ctx->previous_state == RATE_MONOTONIC_INACTIVE || _EXPIRED */ + TickTheClock( ctx, jobs_count * period_length ); + } + } +test-target: testsuites/validation/tc-ratemon-period.c +test-teardown: + brief: null + code: | + rtems_status_code status; + rtems_task_priority priority; + + T_rsc_success( rtems_task_delete( ctx->worker_id ) ); + + status = rtems_task_set_priority( + RTEMS_SELF, + ctx->original_priority, + &priority + ); + T_rsc_success( status ); + description: null +text: ${.:text-template} +transition-map: +# ---- RTEMS_PERIOD_STATUS - OK ---- +- enabled-by: true + post-conditions: + Status: Ok + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Status + State: + - Active + Postponed: all + InactiveCause: 'N/A' +# ---- RTEMS_PERIOD_STATUS - NotDef ---- +- enabled-by: true + post-conditions: + Status: NotDef + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Status + State: + - Inactive + Postponed: all + InactiveCause: + - Canceled +- enabled-by: true + post-conditions: + Status: NotDef + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Status + State: + - Inactive + Postponed: 'N/A' + InactiveCause: + - New +# ---- RTEMS_PERIOD_STATUS - TimeOut ---- +- enabled-by: true + post-conditions: + Status: TimeOut + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Status + State: + - Expired + Postponed: + - One + - Several + InactiveCause: 'N/A' +# ---- Period: Inactive->Active - OK ---- +- enabled-by: true + post-conditions: + Status: Ok + State: Active + Postponed: Zero + Delay: None + Scheduler: Called + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Ticks + State: + - Inactive + Postponed: all + InactiveCause: + - Canceled +- enabled-by: true + post-conditions: + Status: Ok + State: Active + Postponed: Zero + Delay: None + Scheduler: Called + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Ticks + State: + - Inactive + Postponed: 'N/A' + InactiveCause: + - New +# ---- Period: Active->Active - OK ---- +- enabled-by: true + post-conditions: + Status: Ok + State: Active + Postponed: Zero + Delay: TillDeadline + Scheduler: Called + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Ticks + State: + - Active + Postponed: + - Zero + InactiveCause: 'N/A' +# ---- Period: Active/Expired->Active - TimeOut ---- +- enabled-by: true + post-conditions: + Status: TimeOut + State: Active + Postponed: + - if: + pre-conditions: + Postponed: One + then: Zero + - else: OneOrMore + Delay: None + Scheduler: Called + pre-conditions: + Id: + - Valid + Caller: + - OwnerTask + Length: + - Ticks + State: + - Active + - Expired + Postponed: + - One + - Several + InactiveCause: 'N/A' +# ---- Error Case - InvId ---- +- enabled-by: true + post-conditions: + Status: InvId + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Invalid + Caller: all + Length: all + State: + - Inactive + Postponed: all + InactiveCause: + - Canceled +- enabled-by: true + post-conditions: + Status: InvId + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Invalid + Caller: all + Length: all + State: + - Inactive + Postponed: 'N/A' + InactiveCause: + - New +- enabled-by: true + post-conditions: + Status: InvId + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Invalid + Caller: all + Length: all + State: + - Active + - Expired + Postponed: all + InactiveCause: 'N/A' +# ---- Error Case - NotOwn ---- +- enabled-by: true + post-conditions: + Status: NotOwn + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OtherTask + Length: all + State: + - Inactive + Postponed: all + InactiveCause: + - Canceled +- enabled-by: true + post-conditions: + Status: NotOwn + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OtherTask + Length: all + State: + - Inactive + Postponed: 'N/A' + InactiveCause: + - New +- enabled-by: true + post-conditions: + Status: NotOwn + State: Nop + Postponed: Nop + Delay: None + Scheduler: Nop + pre-conditions: + Id: + - Valid + Caller: + - OtherTask + Length: all + State: + - Active + - Expired + Postponed: all + InactiveCause: 'N/A' +# ---- NA ---- +- enabled-by: true + post-conditions: NeverInExpiredState + pre-conditions: + Id: all + Caller: all + Length: all + State: + - Expired + Postponed: + - Zero + InactiveCause: 'N/A' +type: requirement -- cgit v1.2.3