[rtems-central commit] spec: Specify parts of rtems_semaphore_obtain()
Sebastian Huber
sebh at rtems.org
Mon Apr 12 06:11:11 UTC 2021
Module: rtems-central
Branch: master
Commit: 7e71a8c0c35b47b1d6ebdb9a59a2d234c87261ba
Changeset: http://git.rtems.org/rtems-central/commit/?id=7e71a8c0c35b47b1d6ebdb9a59a2d234c87261ba
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Wed Apr 7 14:12:19 2021 +0200
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(+)
diff --git a/spec/rtems/sem/req/obtain.yml b/spec/rtems/sem/req/obtain.yml
new file mode 100644
index 0000000..94ec985
--- /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 0000000..724a000
--- /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 0000000..0b5aba3
--- /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 0000000..62322a1
--- /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 0000000..50ad478
--- /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 0000000..ba10068
--- /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
More information about the vc
mailing list