diff options
Diffstat (limited to 'spec/score/tq/req/enqueue-ceiling.yml')
| -rw-r--r-- | spec/score/tq/req/enqueue-ceiling.yml | 429 |
1 files changed, 429 insertions, 0 deletions
diff --git a/spec/score/tq/req/enqueue-ceiling.yml b/spec/score/tq/req/enqueue-ceiling.yml new file mode 100644 index 00000000..6b136894 --- /dev/null +++ b/spec/score/tq/req/enqueue-ceiling.yml @@ -0,0 +1,429 @@ +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: InitialFirst + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + A priority queue associated with the scheduler which contains exactly the + enqueueing thread shall be created as the first priority queue of the + thread queue. + - name: First + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_B ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The enqueueing thread shall be enqueued in the priority queue associated + with the scheduler. + - name: Second + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_B ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The enqueueing thread shall be enqueued in the priority queue associated + with the scheduler. + - name: FirstFirst + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_B ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The enqueueing thread shall be enqueued in the priority queue associated + with the scheduler. + + The position of the priority queue in the thread queue shall not change. + - name: SecondFirst + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_B ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The enqueueing thread shall be enqueued in the priority queue associated + with the scheduler. + + The position of the priority queue in the thread queue shall not change. + - name: SecondQueue + test-code: | + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_B ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), NULL ); + text: | + The enqueueing thread shall be enqueued in the priority queue associated + with the scheduler. + + The position of the priority queue in the thread queue shall not change. + test-epilogue: null + test-prologue: | + size_t i; + + i = 0; + + /* Event receives */ + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_C ) ); + T_eq_ptr( GetUnblock( ctx, &i ), GetTCB( ctx, TQ_BLOCKER_A ) ); +pre-conditions: +- name: EligibleScheduler + states: + - name: Home + test-code: | + ctx->helping = false; + text: | + While the enqueueing thread has no helping scheduler. + - name: Helping + test-code: | + ctx->helping = true; + text: | + While the enqueueing thread has at least one helping scheduler. + test-epilogue: null + test-prologue: null +- name: QueueEligible + states: + - name: None + test-code: | + /* This is the default */ + text: | + While the priority queue of the thread queue associated with an eligible + scheduler of the enqueueing thread is empty. + - name: EQ + test-code: | + ctx->priority = PRIO_VERY_HIGH; + text: | + While the priority queue of the thread queue associated with an eligible + scheduler of the enqueueing thread is non-empty, while at least one + thread of this priority queue has a priority equal to the priority of the + enqueueing thread with respect to this scheduler. + - name: GT + test-code: | + ctx->priority = PRIO_HIGH; + text: | + While the priority queue of the thread queue associated with an eligible + scheduler of the enqueueing thread is non-empty, while at least one + thread of this priority queue has a priority greater than the priority of + the enqueueing thread with respect to this scheduler. + test-epilogue: null + test-prologue: null +- name: QueueIneligible + states: + - name: None + test-code: | + /* This is the default */ + text: | + While no priority queue of the thread queue exists which is not + associated with an eligible scheduler of the enqueueing thread. + - name: Before + test-code: | + ctx->other_before = true; + text: | + While a priority queue of the thread queue exists which is not + associated with an eligible scheduler of the enqueueing thread, while + this priority queue is positioned before all priority queues which are + associated with eligible schedulers of the enqueueing thread. + - name: After + test-code: | + ctx->other_after = true; + text: | + While a priority queue of the thread queue exists which is not associated + with an eligible scheduler of the enqueueing thread, while this priority + queue is positioned after all priority queues which are associated with + eligible schedulers of the enqueueing thread. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: + Invalid: | + These variants are invalid due to two independent reasons. Firstly, + where the system was built with SMP support disabled, no other scheduler + can exist. Secondly, a priority queue must be present to have another + priority queue positioned before or after the priority queue. +test-action: | + Status_Control status; + + if ( ctx->priority == PRIO_PSEUDO_ISR ) { + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE ); + } else { + TQSetPriority( ctx->tq_ctx, TQ_BLOCKER_B , ctx->priority ); + + if ( ctx->other_before || ctx->other_after ) { + TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_B_OBTAIN ); + TQSendAndWaitForExecutionStop( + ctx->tq_ctx, + TQ_BLOCKER_D, + TQ_EVENT_MUTEX_B_OBTAIN | TQ_EVENT_MUTEX_B_RELEASE | + TQ_EVENT_RUNNER_SYNC + ); + + if ( ctx->other_before ) { + TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_ENQUEUE ); + } + + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE ); + TQSend( + ctx->tq_ctx, + TQ_BLOCKER_B, + TQ_EVENT_ENQUEUE | TQ_EVENT_SURRENDER + ); + + if ( ctx->other_before ) { + TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_SURRENDER ); + } + } else { + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE ); + TQSend( + ctx->tq_ctx, + TQ_BLOCKER_B, + TQ_EVENT_ENQUEUE | TQ_EVENT_SURRENDER + ); + } + } + + if ( ctx->helping ) { + if ( ctx->other_before || ctx->other_after ) { + if ( rtems_scheduler_get_processor_maximum() > 2 ) { + AddHelper( ctx->tq_ctx, ctx->tq_ctx->third_scheduler_id ); + } + } else { + AddHelper( ctx->tq_ctx, ctx->tq_ctx->other_scheduler_id ); + } + } + + TQSchedulerRecordStart( ctx->tq_ctx ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_ENQUEUE | TQ_EVENT_SURRENDER ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_SURRENDER ); + status = TQEnqueue( ctx->tq_ctx, TQ_WAIT_FOREVER ); + T_eq_int( status, TQConvertStatus( ctx->tq_ctx, STATUS_SUCCESSFUL ) ); + TQSchedulerRecordStop( ctx->tq_ctx ); + TQSurrender( ctx->tq_ctx ); + + if ( ctx->other_before || ctx->other_after ) { + TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_MUTEX_B_RELEASE ); + TQSynchronizeRunner(); + } + + if ( ctx->helping ) { + if ( ctx->other_before || ctx->other_after ) { + if ( rtems_scheduler_get_processor_maximum() > 2 ) { + RemoveHelper( ctx->tq_ctx ); + } + } else { + RemoveHelper( ctx->tq_ctx ); + } + } +test-brief: null +test-cleanup: null +test-context: +- brief: | + This this member is true, then the enqueueing thread shall have at least + one helping scheduler. + description: null + member: | + bool helping +- brief: | + This member specifies the priority of a thread with an eligible scheduler + equal to an eligible scheduler of the enqueueing thread. + description: null + member: | + rtems_task_priority priority; +- brief: | + If this member is true, then a thread those eligible schedulers are + ineligible scheduler to the enqueueing task should be enqueued before a + thread with an eligible scheduler equal to an eligible scheduler of the + enqueueing thread. + description: null + member: | + size_t other_before; +- brief: | + If this member is true, then a thread those eligible schedulers are + ineligible scheduler to the enqueueing task should be enqueued after a + thread with an eligible scheduler equal to an eligible scheduler of the + enqueueing thread. + description: null + member: | + size_t other_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} + target: testsuites/validation/tr-tq-enqueue-ceiling.h +test-includes: [] +test-local-includes: +- tr-tq-enqueue-ceiling.h +test-prepare: + ctx->priority = PRIO_PSEUDO_ISR; + ctx->other_before = false; + ctx->other_after = false; +test-setup: + brief: null + code: | + rtems_id scheduler_id; + + scheduler_id = ctx->tq_ctx->runner_scheduler_id; + TQSetScheduler( ctx->tq_ctx, TQ_BLOCKER_A, scheduler_id, PRIO_VERY_HIGH ); + TQSetScheduler( ctx->tq_ctx, TQ_BLOCKER_B, scheduler_id, PRIO_VERY_HIGH ); + TQSetScheduler( ctx->tq_ctx, TQ_BLOCKER_C, scheduler_id, PRIO_VERY_HIGH ); + #if defined( RTEMS_SMP ) + TQSetScheduler( + ctx->tq_ctx, + TQ_BLOCKER_D, + ctx->tq_ctx->other_scheduler_id, + PRIO_LOW + ); + #endif + description: null +test-stop: null +test-support: | + typedef ScoreTqReqEnqueueCeiling_Context Context; + + static const rtems_tcb *GetUnblock( Context *ctx, size_t *index ) + { + const rtems_tcb *thread; + + do { + thread = TQGetNextUnblock( ctx->tq_ctx, index )->thread; + } while ( thread == ctx->tq_ctx->runner_tcb ); + + return thread; + } + + static const rtems_tcb *GetTCB( Context *ctx, TQWorkerKind worker ) + { + return ctx->tq_ctx->worker_tcb[ worker ]; + } + + static void AddHelper( TQContext *tq_ctx, rtems_id scheduler_id ) + { + TQSend( tq_ctx, TQ_BLOCKER_C, TQ_EVENT_MUTEX_A_OBTAIN ); + TQSetScheduler( tq_ctx, TQ_BLOCKER_E, scheduler_id, PRIO_LOW ); + TQSendAndWaitForExecutionStop( + tq_ctx, + TQ_BLOCKER_E, + TQ_EVENT_MUTEX_A_OBTAIN | TQ_EVENT_MUTEX_A_RELEASE + ); + } + + static void RemoveHelper( TQContext *tq_ctx ) + { + TQSend( tq_ctx, TQ_BLOCKER_C, TQ_EVENT_MUTEX_A_RELEASE ); + TQMutexObtain( tq_ctx, TQ_MUTEX_A ); + TQMutexRelease( tq_ctx, TQ_MUTEX_A ); + } +test-target: testsuites/validation/tr-tq-enqueue-ceiling.c +test-teardown: + brief: null + code: | + TQReset( ctx->tq_ctx ); + description: null +text: | + When the calling thread is enqueued on the thread queue. +transition-map: +- enabled-by: true + post-conditions: + Position: InitialFirst + pre-conditions: + EligibleScheduler: + - Home + QueueEligible: + - None + QueueIneligible: + - None +- enabled-by: true + post-conditions: + Position: First + pre-conditions: + EligibleScheduler: + - Home + QueueEligible: + - GT + QueueIneligible: + - None +- enabled-by: true + post-conditions: + Position: Second + pre-conditions: + EligibleScheduler: + - Home + QueueEligible: + - EQ + QueueIneligible: + - None +- enabled-by: true + post-conditions: Invalid + pre-conditions: default +- enabled-by: RTEMS_SMP + post-conditions: + Position: InitialFirst + pre-conditions: + EligibleScheduler: + - Helping + QueueEligible: + - None + QueueIneligible: + - None +- enabled-by: RTEMS_SMP + post-conditions: + Position: First + pre-conditions: + EligibleScheduler: + - Helping + QueueEligible: + - GT + QueueIneligible: + - None +- enabled-by: RTEMS_SMP + post-conditions: + Position: Second + pre-conditions: + EligibleScheduler: + - Helping + QueueEligible: + - EQ + QueueIneligible: + - None +- enabled-by: RTEMS_SMP + post-conditions: + Position: SecondQueue + pre-conditions: + EligibleScheduler: all + QueueEligible: + - EQ + - GT + QueueIneligible: + - Before +- enabled-by: RTEMS_SMP + post-conditions: + Position: FirstFirst + pre-conditions: + EligibleScheduler: all + QueueEligible: + - GT + QueueIneligible: + - After +- enabled-by: RTEMS_SMP + post-conditions: + Position: SecondFirst + pre-conditions: + EligibleScheduler: all + QueueEligible: + - EQ + QueueIneligible: + - After +type: requirement |