From 7e71a8c0c35b47b1d6ebdb9a59a2d234c87261ba Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Wed, 7 Apr 2021 14:12:19 +0200 Subject: spec: Specify parts of rtems_semaphore_obtain() --- spec/rtems/sem/req/obtain.yml | 159 +++++++++++++++++++++++++++++++++++ spec/score/sem/req/seize-try.yml | 134 +++++++++++++++++++++++++++++ spec/score/status/if/header.yml | 14 +++ spec/score/status/if/successful.yml | 12 +++ spec/score/status/if/unsatisfied.yml | 12 +++ spec/score/tq/req/enqueue-fifo.yml | 105 +++++++++++++++++++++++ 6 files changed, 436 insertions(+) create mode 100644 spec/rtems/sem/req/obtain.yml create mode 100644 spec/score/sem/req/seize-try.yml create mode 100644 spec/score/status/if/header.yml create mode 100644 spec/score/status/if/successful.yml create mode 100644 spec/score/status/if/unsatisfied.yml create mode 100644 spec/score/tq/req/enqueue-fifo.yml diff --git a/spec/rtems/sem/req/obtain.yml b/spec/rtems/sem/req/obtain.yml new file mode 100644 index 00000000..94ec9858 --- /dev/null +++ b/spec/rtems/sem/req/obtain.yml @@ -0,0 +1,159 @@ +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/obtain +post-conditions: +- name: Action + states: + - name: InvId + test-code: | + sc = rtems_semaphore_obtain( 0xffffffff, RTEMS_WAIT, RTEMS_NO_TIMEOUT ); + T_rsc( sc, RTEMS_INVALID_ID ); + text: | + The return status of ${../if/obtain:/name} shall be + ${../../status/if/invalid-id:/name}. + - name: SemSeizeTry + test-code: | + ${/score/sem/req/seize-try:/test-run}( + &ctx->tq_ctx, + TQClassicSemGetCount, + TQClassicSemSetCount + ); + text: | + The calling task shall try to seize the semaphore as specified by + ${/score/sem/req/seize-try}. + test-epilogue: null + test-prologue: | + rtems_status_code sc; +pre-conditions: +- name: Class + states: + - name: Counting + test-code: | + ctx->attribute_set |= RTEMS_COUNTING_SEMAPHORE; + text: | + While the semaphore object is a counting semaphore. + - name: Simple + test-code: | + ctx->attribute_set |= RTEMS_SIMPLE_BINARY_SEMAPHORE; + text: | + While the semaphore object is a simple binary semaphore. + test-epilogue: null + test-prologue: null +- name: Discipline + states: + - name: FIFO + test-code: | + ctx->attribute_set |= RTEMS_FIFO; + text: | + While the semaphore uses the FIFO task wait queue discipline. + - name: Priority + test-code: | + ctx->attribute_set |= RTEMS_PRIORITY; + text: | + While the semaphore uses the priority task wait queue discipline. + test-epilogue: null + test-prologue: null +- name: Id + states: + - name: Valid + test-code: | + /* Nothing to prepare */ + text: | + While the ${../if/obtain:/params[0]/name} parameter is associated with + the semaphore. + - name: Invalid + test-code: | + /* Nothing to prepare */ + text: | + While the ${../if/obtain:/params[0]/name} parameter is not associated + with a semaphore. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + rtems_status_code sc; + + sc = rtems_semaphore_create( + NAME, + 1, + ctx->attribute_set, + PRIO_ULTRA_HIGH, + &ctx->tq_ctx.thread_queue_id + ); + T_rsc_success( sc ); +test-brief: null +test-cleanup: + rtems_status_code sc; + + sc = rtems_semaphore_delete( ctx->tq_ctx.thread_queue_id ); + T_rsc_success( sc ); +test-context: +- brief: | + This member contains the thread queue test context. + description: null + member: | + TQContext tq_ctx +- brief: | + This member specifies if the attribute set of the semaphore. + description: null + member: | + rtems_attribute attribute_set +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +- string.h +test-local-includes: +- tc-support.h +- tr-sem-seize-try.h +- tx-thread-queue.h +test-prepare: null +test-setup: + brief: null + code: | + memset( ctx, 0, sizeof( *ctx ) ); + ctx->tq_ctx.enqueue = TQClassicSemEnqueue; + ctx->tq_ctx.dequeue_one = TQClassicSemDequeue; + ctx->tq_ctx.dequeue_all = TQClassicSemDequeue; + ctx->tq_ctx.convert_status = TQClassicConvertStatus; + TQInitialize( &ctx->tq_ctx ); + description: null +test-stop: null +test-support: | + #define NAME rtems_build_name( 'T', 'E', 'S', 'T' ) + + typedef RtemsSemReqObtain_Context Context; +test-target: testsuites/validation/tc-sem-obtain.c +test-teardown: + brief: null + code: | + TQDestory( &ctx->tq_ctx ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Action: InvId + pre-conditions: + Class: all + Discipline: all + Id: + - Invalid +- enabled-by: true + post-conditions: + Action: SemSeizeTry + pre-conditions: + Class: all + Discipline: all + Id: + - Valid +type: requirement diff --git a/spec/score/sem/req/seize-try.yml b/spec/score/sem/req/seize-try.yml new file mode 100644 index 00000000..724a0003 --- /dev/null +++ b/spec/score/sem/req/seize-try.yml @@ -0,0 +1,134 @@ +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: [] +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_eq_int( ctx->status, Status( ctx, STATUS_SUCCESSFUL ) ); + text: | + The return status of the directive call shall be derived from + ${../../status/if/successful:/name}. + - name: Unsat + test-code: | + T_eq_int( ctx->status, Status( ctx, STATUS_UNSATISFIED ) ); + text: | + The return status of the directive call shall be derived from + ${../../status/if/unsatisfied:/name}. + test-epilogue: null + test-prologue: null +- name: Count + states: + - name: Nop + test-code: | + T_eq_u32( ctx->count_after, ctx->count_before ); + text: | + The count of the semaphore shall not be modified. + - name: MinusOne + test-code: | + T_eq_u32( ctx->count_after, ctx->count_before - 1 ); + text: | + The count of the semaphore shall be decremented by one. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: Count + states: + - name: Zero + test-code: | + ctx->count_before = 0; + text: | + The count of the semaphore shall be zero. + - name: Positive + test-code: | + ctx->count_before = 1; + text: | + The count of the semaphore shall be greater than zero. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ( *ctx->set_count )( ctx->tq_ctx, ctx->count_before ); + ctx->status = TQEnqueue( ctx->tq_ctx, TQ_NO_WAIT ); + ctx->count_after = ( *ctx->get_count )( ctx->tq_ctx ); +test-brief: null +test-cleanup: null +test-context: +- brief: | + This member specifies the semaphore count before the directive call. + description: null + member: | + uint32_t count_before +- brief: | + This member contains the return status of the directive call. + description: null + member: | + Status_Control status +- brief: | + This member contains the semaphore count after the directive call. + description: null + member: | + uint32_t count_after +test-context-support: null +test-description: null +test-header: + code: null + includes: [] + local-includes: + - tx-thread-queue.h + run-params: + - description: | + is the thread queue context. + dir: inout + name: tq_ctx + specifier: TQContext *${.:name} + - description: | + is the semaphore get count handler. + dir: null + name: get_count + specifier: uint32_t ( *${.:name} )( TQContext * ) + - description: | + is the semaphore set count handler. + dir: null + name: set_count + specifier: void ( *${.:name} )( TQContext *, uint32_t ) + target: testsuites/validation/tr-sem-seize-try.h +test-includes: [] +test-local-includes: +- tr-sem-seize-try.h +test-prepare: null +test-setup: null +test-stop: null +test-support: | + typedef ScoreSemReqSeizeTry_Context Context; + + static Status_Control Status( const Context *ctx, Status_Control status ) + { + return TQConvertStatus( ctx->tq_ctx, status ); + } +test-target: testsuites/validation/tr-sem-seize-try.c +test-teardown: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: Ok + Count: MinusOne + pre-conditions: + Count: + - Positive +- enabled-by: true + post-conditions: + Status: Unsat + Count: Nop + pre-conditions: + Count: + - Zero +type: requirement diff --git a/spec/score/status/if/header.yml b/spec/score/status/if/header.yml new file mode 100644 index 00000000..0b5aba3f --- /dev/null +++ b/spec/score/status/if/header.yml @@ -0,0 +1,14 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: | + This header file defines interfaces of the Operation Status Support. +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: header-file +links: +- role: interface-placement + uid: ../../if/domain +path: rtems/score/status.h +prefix: cpukit/include +type: interface diff --git a/spec/score/status/if/successful.yml b/spec/score/status/if/successful.yml new file mode 100644 index 00000000..62322a1a --- /dev/null +++ b/spec/score/status/if/successful.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified +links: +- role: interface-placement + uid: header +name: STATUS_SUCCESSFUL +reference: null +type: interface diff --git a/spec/score/status/if/unsatisfied.yml b/spec/score/status/if/unsatisfied.yml new file mode 100644 index 00000000..50ad478e --- /dev/null +++ b/spec/score/status/if/unsatisfied.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: unspecified +links: +- role: interface-placement + uid: header +name: STATUS_UNSATISFIED +reference: null +type: interface diff --git a/spec/score/tq/req/enqueue-fifo.yml b/spec/score/tq/req/enqueue-fifo.yml new file mode 100644 index 00000000..ba100681 --- /dev/null +++ b/spec/score/tq/req/enqueue-fifo.yml @@ -0,0 +1,105 @@ +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: [] +post-conditions: +- name: Position + states: + - name: First + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_A ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The thread shall be the first thread in the queue. + - name: Last + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_B ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_A ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The thread shall be the last thread in the queue. + test-epilogue: null + test-prologue: | + size_t i; + + i = 0; +pre-conditions: +- name: Empty + states: + - name: 'Yes' + test-code: | + /* This is the default */ + text: | + While the queue is empty. + - name: 'No' + test-code: | + TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_ENQUEUE ); + text: | + While the queue is non-empty. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + TQPrepare( ctx->tq_ctx ); + TQSchedulerRecordStart( ctx->tq_ctx ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE ); + TQDequeueAll( ctx->tq_ctx ); + TQSchedulerRecordStop( ctx->tq_ctx ); + TQCleanup( ctx->tq_ctx ); +test-brief: null +test-cleanup: null +test-context: [] +test-context-support: null +test-description: null +test-header: + code: null + includes: [] + local-includes: + - tx-thread-queue.h + run-params: + - description: | + is the thread queue context. + dir: inout + name: tq_ctx + specifier: TQContext *${.:name} + target: testsuites/validation/tr-tq-enqueue-fifo.h +test-includes: [] +test-local-includes: +- tr-tq-enqueue-fifo.h +test-prepare: null +test-setup: null +test-stop: null +test-support: | + typedef ScoreTqReqEnqueueFifo_Context Context; + + static const T_scheduler_event *GetUnblock( Context *ctx, size_t *index ) + { + return TQGetNextUnblock( ctx->tq_ctx, index ); + } + + static const rtems_tcb *GetTCB( Context *ctx, TQWorkerKind worker ) + { + return ctx->tq_ctx->worker_tcb[ TQ_BLOCKER_A ]; + } +test-target: testsuites/validation/tr-tq-enqueue-fifo.c +test-teardown: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Position: First + pre-conditions: + Empty: + - 'Yes' +- enabled-by: true + post-conditions: + Position: Last + pre-conditions: + Empty: + - 'No' +type: requirement -- cgit v1.2.3