From cc2b4aa32d82a360454aea3840f91e054e1529e7 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Tue, 31 Aug 2021 15:18:31 +0200 Subject: spec: Specify futex operations --- spec/c/if/eagain.yml | 12 ++ spec/score/futex/if/group.yml | 15 +++ spec/score/futex/if/wait.yml | 12 ++ spec/score/futex/if/wake.yml | 12 ++ spec/score/futex/req/wait.yml | 167 ++++++++++++++++++++++++++++ spec/score/futex/req/wake.yml | 185 +++++++++++++++++++++++++++++++ spec/score/tq/req/flush-fifo.yml | 177 +++++++++++++++++++++++++++++ spec/score/tq/req/flush-filter-stop.yml | 16 +++ spec/score/tq/req/flush-filter.yml | 15 +++ spec/score/tq/req/flush-remove-timer.yml | 15 +++ spec/score/tq/req/flush-unblock.yml | 15 +++ 11 files changed, 641 insertions(+) create mode 100644 spec/c/if/eagain.yml create mode 100644 spec/score/futex/if/group.yml create mode 100644 spec/score/futex/if/wait.yml create mode 100644 spec/score/futex/if/wake.yml create mode 100644 spec/score/futex/req/wait.yml create mode 100644 spec/score/futex/req/wake.yml create mode 100644 spec/score/tq/req/flush-fifo.yml create mode 100644 spec/score/tq/req/flush-filter-stop.yml create mode 100644 spec/score/tq/req/flush-filter.yml create mode 100644 spec/score/tq/req/flush-remove-timer.yml create mode 100644 spec/score/tq/req/flush-unblock.yml diff --git a/spec/c/if/eagain.yml b/spec/c/if/eagain.yml new file mode 100644 index 00000000..907cb1a8 --- /dev/null +++ b/spec/c/if/eagain.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-define +links: +- role: interface-placement + uid: errno-header +name: EAGAIN +references: {} +type: interface diff --git a/spec/score/futex/if/group.yml b/spec/score/futex/if/group.yml new file mode 100644 index 00000000..b5037de5 --- /dev/null +++ b/spec/score/futex/if/group.yml @@ -0,0 +1,15 @@ +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 +identifier: RTEMSScoreFutex +links: +- role: interface-ingroup + uid: ../../if/group +non-functional-type: design-group +rationale: null +references: [] +requirement-type: non-functional +text: | + The super core shall have a component containing the futex implementation. +type: requirement diff --git a/spec/score/futex/if/wait.yml b/spec/score/futex/if/wait.yml new file mode 100644 index 00000000..77123799 --- /dev/null +++ b/spec/score/futex/if/wait.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-function +links: +- role: interface-ingroup + uid: group +name: _Futex_Wait +references: {} +type: interface diff --git a/spec/score/futex/if/wake.yml b/spec/score/futex/if/wake.yml new file mode 100644 index 00000000..74c5b321 --- /dev/null +++ b/spec/score/futex/if/wake.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-function +links: +- role: interface-ingroup + uid: group +name: _Futex_Wake +references: {} +type: interface diff --git a/spec/score/futex/req/wait.yml b/spec/score/futex/req/wait.yml new file mode 100644 index 00000000..190e134b --- /dev/null +++ b/spec/score/futex/req/wait.yml @@ -0,0 +1,167 @@ +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/wake +post-conditions: +- name: Result + states: + - name: Zero + test-code: | + /* This result is checked by Enqueue() */ + text: | + The return status of ${../if/wait:/name} shall be zero. + - name: EAGAIN + test-code: | + eno = _Futex_Wait( &ctx->futex, &ctx->state, ctx->expected_value ); + T_eq_int( eno, EAGAIN ); + text: | + The return status of ${../if/wait:/name} shall be ${/c/if/eagain:/name}. + test-epilogue: null + test-prologue: | + int eno; +- name: Enqueue + states: + - name: 'No' + test-code: | + /* The runner would block forever */ + text: | + The calling thread shall not be enqueued on the thread queue of the futex + object. + - name: 'Yes' + test-code: | + ${../../tq/req/enqueue-fifo:/test-run}( &ctx->tq_ctx ); + text: | + The calling thread shall be enqueued in FIFO order on the thread queue of + the futex object. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: State + states: + - name: Equal + test-code: | + ctx->expected_value = 0; + text: | + While the expected futex state value is equal to the actual futex state + value. + - name: NotEqual + test-code: | + ctx->expected_value = 1; + text: | + While the expected futex state value is not equal to the actual futex + state value. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + /* The action is performed in the post-conditions. */ +test-brief: null +test-cleanup: + _Futex_Destroy( &ctx->futex ); +test-context: +- brief: | + This member contains the thread queue test context. + description: null + member: | + TQContext tq_ctx; +- brief: | + This member specifies the expected futex state value. + description: null + member: | + int expected_value +- brief: | + This member provides the futex object. + description: null + member: | + struct _Futex_Control futex +- brief: | + This member provides the futex state. + description: null + member: | + int state +test-context-support: null +test-description: null +test-header: null +test-includes: +- sys/lock.h +- limits.h +- rtems.h +test-local-includes: +- tx-thread-queue.h +- tr-tq-enqueue-fifo.h +test-prepare: | + _Futex_Initialize( &ctx->futex ); + ctx->state = 0; +test-setup: + brief: null + code: | + memset( ctx, 0, sizeof( *ctx ) ); + ctx->tq_ctx.discipline = TQ_FIFO; + ctx->tq_ctx.wait = TQ_WAIT_FOREVER; + ctx->tq_ctx.enqueue_prepare = TQDoNothing; + ctx->tq_ctx.enqueue = Enqueue; + ctx->tq_ctx.enqueue_done = EnqueueDone; + ctx->tq_ctx.surrender = TQDoNothing; + ctx->tq_ctx.convert_status = TQConvertStatusPOSIX; + TQInitialize( &ctx->tq_ctx ); + description: null +test-stop: null +test-support: | + typedef ${.:/test-context-type} Context; + + static Context *ToContext( TQContext *tq_ctx ) + { + return RTEMS_CONTAINER_OF( tq_ctx, Context, tq_ctx ); + } + + static Status_Control Enqueue( TQContext *tq_ctx, TQWait wait ) + { + Context *ctx; + int eno; + + ctx = ToContext( tq_ctx ); + eno = _Futex_Wait( &ctx->futex, &ctx->state, ctx->expected_value ); + T_eq_int( eno, 0 ); + + return STATUS_BUILD( 0, eno ); + } + + static void EnqueueDone( TQContext *tq_ctx ) + { + Context *ctx; + int count; + + ctx = ToContext( tq_ctx ); + count = _Futex_Wake( &ctx->futex, INT_MAX ); + T_eq_int( count, (int) ctx->tq_ctx.how_many ); + } +test-target: testsuites/validation/tc-futex-wait.c +test-teardown: + brief: null + code: | + TQDestroy( &ctx->tq_ctx ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Result: EAGAIN + Enqueue: 'No' + pre-conditions: + State: + - NotEqual +- enabled-by: true + post-conditions: + Result: Zero + Enqueue: 'Yes' + pre-conditions: + State: + - Equal +type: requirement diff --git a/spec/score/futex/req/wake.yml b/spec/score/futex/req/wake.yml new file mode 100644 index 00000000..87604775 --- /dev/null +++ b/spec/score/futex/req/wake.yml @@ -0,0 +1,185 @@ +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/wake +post-conditions: +- name: Result + states: + - name: Count + test-code: | + /* This result is checked by Flush() */ + text: | + The return status of ${../if/wake:/name} shall be the count of threads + extracted from the thread queue of the futex object. + test-epilogue: null + test-prologue: null +- name: Flush + states: + - name: 'No' + test-code: | + /* This state is checked by Enqueue() */ + text: | + No thread shall be extracted from the thread queue of the futex object. + - name: Partial + test-code: | + /* This state is checked by Flush() */ + text: | + The first count threads specified by the ``count`` parameter shall be + extracted from the thread queue of the futex object in + ${/glossary/fifo:/term} order. + - name: All + test-code: | + ${../../tq/req/flush-fifo:/test-run}( &ctx->tq_ctx ); + text: | + All threads shall be extracted from the thread queue of the futex object + in ${/glossary/fifo:/term} order. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: Count + states: + - name: Negative + test-code: | + /* This state is prepared by Enqueue() */ + text: | + While the ``count`` parameter is less than zero. + - name: Partial + test-code: | + /* This state is prepared by Flush() */ + text: | + While the ``count`` parameter is greater than or equal to zero, + while the ``count`` parameter is less than the count of threads enqueued + on the thread queue of the futex object. + - name: All + test-code: | + /* This state is prepared by Flush() */ + text: | + While the ``count`` parameter is greater than or equal to zero, + while the ``count`` parameter is greater than or equal to the count of + threads enqueued on the thread queue of the futex object. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + /* The action is performed in the ``Flush`` post-condition ``All`` state. */ +test-brief: null +test-cleanup: + _Futex_Destroy( &ctx->futex ); +test-context: +- brief: | + This member contains the thread queue test context. + description: null + member: | + TQContext tq_ctx; +- brief: | + This member provides the futex object. + description: null + member: | + struct _Futex_Control futex +- brief: | + This member provides the futex state. + description: null + member: | + int state +test-context-support: null +test-description: null +test-header: null +test-includes: +- sys/lock.h +- limits.h +- rtems.h +test-local-includes: +- tx-thread-queue.h +- tr-tq-flush-fifo.h +test-prepare: | + _Futex_Initialize( &ctx->futex ); +test-setup: + brief: null + code: | + memset( ctx, 0, sizeof( *ctx ) ); + ctx->tq_ctx.discipline = TQ_FIFO; + ctx->tq_ctx.wait = TQ_WAIT_FOREVER; + ctx->tq_ctx.enqueue_prepare = TQDoNothing; + ctx->tq_ctx.enqueue = Enqueue; + ctx->tq_ctx.enqueue_done = TQDoNothing; + ctx->tq_ctx.flush = Flush; + ctx->tq_ctx.surrender = TQDoNothing; + ctx->tq_ctx.convert_status = TQConvertStatusPOSIX; + TQInitialize( &ctx->tq_ctx ); + description: null +test-stop: null +test-support: | + typedef ${.:/test-context-type} Context; + + static Context *ToContext( TQContext *tq_ctx ) + { + return RTEMS_CONTAINER_OF( tq_ctx, Context, tq_ctx ); + } + + static Status_Control Enqueue( TQContext *tq_ctx, TQWait wait ) + { + Context *ctx; + int count; + int eno; + + ctx = ToContext( tq_ctx ); + + count = _Futex_Wake( &ctx->futex, -1 ); + T_eq_int( count, 0 ); + + count = _Futex_Wake( &ctx->futex, 0 ); + T_eq_int( count, 0 ); + + eno = _Futex_Wait( &ctx->futex, &ctx->state, 0 ); + T_eq_int( eno, 0 ); + + return STATUS_BUILD( 0, eno ); + } + + static void Flush( TQContext *tq_ctx ) + { + Context *ctx; + int count; + int how_many; + + ctx = ToContext( tq_ctx ); + how_many = (int) ctx->tq_ctx.how_many; + + count = _Futex_Wake( &ctx->futex, 1 ); + T_eq_int( count, how_many > 0 ? 1 : 0 ); + + count = _Futex_Wake( &ctx->futex, INT_MAX ); + T_eq_int( count, how_many > 1 ? how_many - 1 : 0 ); + } +test-target: testsuites/validation/tc-futex-wake.c +test-teardown: + brief: null + code: | + TQDestroy( &ctx->tq_ctx ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Result: Count + Flush: 'No' + pre-conditions: + Count: + - Negative +- enabled-by: true + post-conditions: + Result: Count + Flush: + - specified-by: Count + pre-conditions: + Count: + - Partial + - All +type: requirement diff --git a/spec/score/tq/req/flush-fifo.yml b/spec/score/tq/req/flush-fifo.yml new file mode 100644 index 00000000..636288bc --- /dev/null +++ b/spec/score/tq/req/flush-fifo.yml @@ -0,0 +1,177 @@ +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: requirement-refinement + uid: ../if/group +- role: validation + uid: flush-filter +- role: validation + uid: flush-remove-timer +- role: validation + uid: flush-unblock +post-conditions: +- name: Operation + states: + - name: Nop + test-code: | + /* Event receive */ + T_eq_ptr( GetUnblock( ctx, &i )->thread, GetTCB( ctx, TQ_BLOCKER_A ) ); + T_eq_ptr( GetUnblock( ctx, &i ), &T_scheduler_event_null ); + text: | + No operation shall be performed. + - name: TryExtract + test-code: | + event = GetUnblock( ctx, &i ); + T_eq_ptr( event->executing, NULL ); + T_eq_ptr( event->thread, GetTCB( ctx, TQ_BLOCKER_B ) ); + + event = GetUnblock( ctx, &i ); + T_eq_ptr( event->executing, NULL ); + T_eq_ptr( event->thread, GetTCB( ctx, TQ_BLOCKER_C ) ); + + event = GetUnblock( ctx, &i ); + T_eq_ptr( event->executing, GetTCB( ctx, TQ_BLOCKER_D ) ); + T_eq_ptr( event->thread, GetTCB( ctx, TQ_BLOCKER_D ) ); + + T_eq_ptr( GetUnblock( ctx, &i ), &T_scheduler_event_null ); + text: | + The enqueued threads of the thread queue may be extracted in + ${/glossary/fifo:/term} order. + test-epilogue: | + test-prologue: | + size_t i; + const T_scheduler_event *event; + + i = 0; +pre-conditions: +- name: Queue + states: + - name: Empty + test-code: | + ctx->tq_ctx->how_many = 0; + text: | + While the thread queue is empty. + - name: NonEmpty + test-code: | + ctx->tq_ctx->how_many = 3; + text: | + While the thread queue has at least one enqueued thread. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE_PREPARE ); + + if ( ctx->tq_ctx->how_many > 0 ) { + TQSend( ctx->tq_ctx, TQ_BLOCKER_B, TQ_EVENT_ENQUEUE | TQ_EVENT_SURRENDER ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_C, TQ_EVENT_ENQUEUE | TQ_EVENT_SURRENDER ); + T_scheduler_set_event_handler( SchedulerEvent, ctx ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_D, TQ_EVENT_ENQUEUE | TQ_EVENT_SURRENDER ); + } else { + TQSchedulerRecordStart( ctx->tq_ctx ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_FLUSH ); + } + + TQSchedulerRecordStop( ctx->tq_ctx ); + TQSend( ctx->tq_ctx, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE_DONE ); +test-brief: null +test-cleanup: null +test-context: +- brief: | + This member contains the call within ISR request. + description: null + member: | + CallWithinISRRequest request; +test-context-support: null +test-description: null +test-header: + code: null + freestanding: false + includes: [] + local-includes: + - tx-thread-queue.h + run-params: + - description: | + is the thread queue test context. + dir: inout + name: tq_ctx + specifier: TQContext *${.:name} + target: testsuites/validation/tr-tq-flush-fifo.h +test-includes: [] +test-local-includes: +- tx-support.h +- tr-tq-flush-fifo.h +test-prepare: null +test-setup: + brief: null + code: | + TQReset( ctx->tq_ctx ); + TQSetPriority( ctx->tq_ctx, TQ_BLOCKER_A, PRIO_ULTRA_HIGH ); + TQSetPriority( ctx->tq_ctx, TQ_BLOCKER_B, PRIO_VERY_HIGH ); + TQSetPriority( ctx->tq_ctx, TQ_BLOCKER_C, PRIO_HIGH ); + TQSetPriority( ctx->tq_ctx, TQ_BLOCKER_D, PRIO_HIGH ); + description: null +test-stop: null +test-support: | + typedef ${.:/test-context-type} 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[ worker ]; + } + + static void Flush( void *arg ) + { + Context *ctx; + + ctx = arg; + TQSchedulerRecordStart( ctx->tq_ctx ); + TQFlush( ctx->tq_ctx ); + } + + static void SchedulerEvent( void *arg, const T_scheduler_event *event ) + { + Context *ctx; + + ctx = arg; + + if ( event->operation == T_SCHEDULER_BLOCK ) { + ctx->request.handler = Flush; + ctx->request.arg = ctx; + CallWithinISRSubmit( &ctx->request ); + T_scheduler_set_event_handler( NULL, NULL ); + } + } +test-target: testsuites/validation/tr-tq-flush-fifo.c +test-teardown: + brief: null + code: | + TQReset( ctx->tq_ctx ); + description: null +text: | + When the ${/glossary/fifo:/term} thread queue is flushed. +transition-map: +- enabled-by: true + post-conditions: + Operation: Nop + pre-conditions: + Queue: + - Empty +- enabled-by: true + post-conditions: + Operation: TryExtract + pre-conditions: + Queue: + - NonEmpty +type: requirement diff --git a/spec/score/tq/req/flush-filter-stop.yml b/spec/score/tq/req/flush-filter-stop.yml new file mode 100644 index 00000000..f39a69ea --- /dev/null +++ b/spec/score/tq/req/flush-filter-stop.yml @@ -0,0 +1,16 @@ +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 +links: +- role: requirement-refinement + uid: ../if/group +functional-type: function +rationale: null +references: [] +requirement-type: functional +text: | + When the caller provided filter handler returns a value equal to + ${/c/if/null:/name}, the thread queue flush operation shall stop extracting + threads from the thread queue. +type: requirement diff --git a/spec/score/tq/req/flush-filter.yml b/spec/score/tq/req/flush-filter.yml new file mode 100644 index 00000000..d304f7b9 --- /dev/null +++ b/spec/score/tq/req/flush-filter.yml @@ -0,0 +1,15 @@ +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 +links: +- role: requirement-refinement + uid: ../if/group +functional-type: function +rationale: null +references: [] +requirement-type: functional +text: | + The thread queue flush operation shall invoke the caller provided filter + handler for each thread to extract. +type: requirement diff --git a/spec/score/tq/req/flush-remove-timer.yml b/spec/score/tq/req/flush-remove-timer.yml new file mode 100644 index 00000000..7dcea402 --- /dev/null +++ b/spec/score/tq/req/flush-remove-timer.yml @@ -0,0 +1,15 @@ +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 +links: +- role: requirement-refinement + uid: ../if/group +functional-type: function +rationale: null +references: [] +requirement-type: functional +text: | + While the extracted thread is in the blocked wait state, the thread queue + flush operation shall remove the thread timer. +type: requirement diff --git a/spec/score/tq/req/flush-unblock.yml b/spec/score/tq/req/flush-unblock.yml new file mode 100644 index 00000000..02019007 --- /dev/null +++ b/spec/score/tq/req/flush-unblock.yml @@ -0,0 +1,15 @@ +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 +links: +- role: requirement-refinement + uid: ../if/group +functional-type: function +rationale: null +references: [] +requirement-type: functional +text: | + While the extracted thread is in the blocked wait state, the thread queue + flush operation shall unblock the thread. +type: requirement -- cgit v1.2.3