diff options
author | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2021-09-28 16:09:40 +0200 |
---|---|---|
committer | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2021-09-29 08:01:06 +0200 |
commit | 512a4a2ce9ae663f7c2d843351ba3184e8697535 (patch) | |
tree | 2339b87053c01d7f345a23c5dd29c54edf9bf191 | |
parent | spec: Specify scheduler helping detail (diff) | |
download | rtems-central-512a4a2ce9ae663f7c2d843351ba3184e8697535.tar.bz2 |
spec: Improve semaphore surrender
-rw-r--r-- | spec/rtems/sem/req/release.yml | 14 | ||||
-rw-r--r-- | spec/score/sem/req/surrender.yml | 25 |
2 files changed, 22 insertions, 17 deletions
diff --git a/spec/rtems/sem/req/release.yml b/spec/rtems/sem/req/release.yml index 2f30836c..9e432256 100644 --- a/spec/rtems/sem/req/release.yml +++ b/spec/rtems/sem/req/release.yml @@ -53,8 +53,8 @@ post-conditions: ${/score/mtx/req/surrender:/test-run}( &ctx->tq_mtx_ctx ); text: | The calling task shall surrender the mutex as specified by - ${/score/mtx/req/surrender} where an enqueue blocks and a recursive seize - is allowed. + ${/score/mtx/req/surrender} where an enqueue blocks, a recursive seize is + allowed, the owner is checked, and no locking protocol is used. - name: InheritMtxSurrender test-code: | ctx->tq_ctx.enqueue_variant = TQ_ENQUEUE_BLOCKS; @@ -66,8 +66,9 @@ post-conditions: ${/score/mtx/req/surrender:/test-run}( &ctx->tq_mtx_ctx ); text: | The calling task shall surrender the mutex as specified by - ${/score/mtx/req/surrender} where an enqueue blocks and a recursive seize - is allowed. + ${/score/mtx/req/surrender} where an enqueue blocks, a recursive seize is + allowed, the owner is checked, and a priority inheritance protocol is + used. - name: CeilingMtxSurrender test-code: | ctx->tq_ctx.enqueue_variant = TQ_ENQUEUE_BLOCKS; @@ -80,7 +81,7 @@ post-conditions: text: | The calling task shall surrender the mutex as specified by ${/score/mtx/req/surrender} where an enqueue blocks, a recursive seize is - allowed, and a priority ceiling is used. + allowed, the owner is checked, and a priority ceiling is used. - name: MrsPMtxSurrender test-code: | ctx->tq_ctx.enqueue_variant = TQ_ENQUEUE_STICKY; @@ -93,7 +94,8 @@ post-conditions: text: | The calling task shall surrender the mutex as specified by ${/score/mtx/req/surrender} where an enqueue is sticky, a recursive seize - returns an error status, and a priority ceiling is used. + returns an error status, the owner is checked, and a priority ceiling is + used. test-epilogue: null test-prologue: | rtems_status_code sc; diff --git a/spec/score/sem/req/surrender.yml b/spec/score/sem/req/surrender.yml index fc767941..e2b83da0 100644 --- a/spec/score/sem/req/surrender.yml +++ b/spec/score/sem/req/surrender.yml @@ -4,6 +4,8 @@ copyrights: enabled-by: true functional-type: action links: +- role: function-implementation + uid: /score/tq/req/surrender - role: requirement-refinement uid: ../if/group post-conditions: @@ -23,19 +25,18 @@ post-conditions: ${../../status/if/maximum-count-exceeded:/name}. test-epilogue: null test-prologue: null -- name: Dequeue +- name: Surrender states: - name: FIFO test-code: | - /* TODO */ + ${../../tq/req/surrender:/test-run}( &ctx->tq_ctx->base ); text: | - The first thread in FIFO order shall be dequeued from the thread queue. + The thread queue of the semaphore shall be surrendered in FIFO order. - name: Priority test-code: | - /* TODO */ + ${../../tq/req/surrender:/test-run}( &ctx->tq_ctx->base ); text: | - The first thread in priority order shall be dequeued from the thread - queue. + The thread queue of the semaphore shall be surrendered in priority order. test-epilogue: null test-prologue: null - name: Count @@ -144,6 +145,7 @@ test-action: | ctx->status = TQSurrender( &ctx->tq_ctx->base ); ctx->count_after = TQSemGetCount( ctx->tq_ctx ); + TQSemSetCount( ctx->tq_ctx, 1 ); test-brief: null test-cleanup: null test-context: @@ -186,6 +188,7 @@ test-header: test-includes: [] test-local-includes: - tr-sem-surrender.h +- tr-tq-surrender.h test-prepare: null test-setup: brief: null @@ -209,7 +212,7 @@ transition-map: - enabled-by: true post-conditions: Status: Ok - Dequeue: N/A + Surrender: N/A Count: One pre-conditions: Variant: @@ -221,7 +224,7 @@ transition-map: - enabled-by: true post-conditions: Status: Ok - Dequeue: + Surrender: - specified-by: Discipline Count: Zero pre-conditions: @@ -233,7 +236,7 @@ transition-map: - enabled-by: true post-conditions: Status: Ok - Dequeue: N/A + Surrender: N/A Count: PlusOne pre-conditions: Variant: @@ -244,7 +247,7 @@ transition-map: - enabled-by: true post-conditions: Status: MaxCountExceeded - Dequeue: N/A + Surrender: N/A Count: Nop pre-conditions: Variant: @@ -255,7 +258,7 @@ transition-map: - enabled-by: true post-conditions: Status: Ok - Dequeue: + Surrender: - specified-by: Discipline Count: Zero pre-conditions: |