diff options
author | Frank Kühndel <frank.kuehndel@embedded-brains.de> | 2021-09-07 15:05:41 +0200 |
---|---|---|
committer | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2021-09-14 16:00:54 +0200 |
commit | 248df1d31ceb4a935af41e047fd7c308ad54e273 (patch) | |
tree | a63bda904034c0d874eaa2eaf03572d83c5b52fb | |
parent | score: Fix priority inheritance flush test (diff) | |
download | rtems-central-248df1d31ceb4a935af41e047fd7c308ad54e273.tar.bz2 |
spec: Update message manager specification
-rw-r--r-- | spec/rtems/attr/req/default-equals.yml (renamed from spec/rtems/message/req/attributes.yml) | 9 | ||||
-rw-r--r-- | spec/rtems/attr/val/attr.yml | 18 | ||||
-rw-r--r-- | spec/rtems/message/glossary/firstmessage.yml | 6 | ||||
-rw-r--r-- | spec/rtems/message/glossary/lastmessage.yml | 2 | ||||
-rw-r--r-- | spec/rtems/message/glossary/receiver.yml | 14 | ||||
-rw-r--r-- | spec/rtems/message/glossary/unblock.yml | 23 | ||||
-rw-r--r-- | spec/rtems/message/req/broadcast.yml | 794 | ||||
-rw-r--r-- | spec/rtems/message/req/flush-pending.yml | 562 | ||||
-rw-r--r-- | spec/rtems/message/req/receive.yml | 2 | ||||
-rw-r--r-- | spec/rtems/message/req/urgent-send.yml | 5 | ||||
-rw-r--r-- | spec/rtems/message/val/message-macros.yml | 36 | ||||
-rw-r--r-- | spec/rtems/option/req/default-equals.yml (renamed from spec/rtems/message/req/options.yml) | 6 | ||||
-rw-r--r-- | spec/rtems/option/val/options.yml | 13 |
13 files changed, 1432 insertions, 58 deletions
diff --git a/spec/rtems/message/req/attributes.yml b/spec/rtems/attr/req/default-equals.yml index 5e9ecdff..ed3bd174 100644 --- a/spec/rtems/message/req/attributes.yml +++ b/spec/rtems/attr/req/default-equals.yml @@ -4,15 +4,12 @@ copyrights: enabled-by: true links: - role: requirement-refinement - uid: ../../attr/if/default + uid: ../if/default non-functional-type: interface rationale: null references: [] requirement-type: non-functional text: | - The value of macro ${../../attr/if/default:/name} shall be equal to the value - of the expression ``RTEMS_FIFO | RTEMS_LOCAL``. - - Note: ${../../attr/if/global:/name} is not part of the space profile - because no remote ${/glossary/node:/plural} are supported. + The value of macro ${../if/default:/name} shall be equal to the value + of expression ``${../if/fifo:/name} | ${../if/local:/name}``. type: requirement diff --git a/spec/rtems/attr/val/attr.yml b/spec/rtems/attr/val/attr.yml index eea9f10f..eef9c4ea 100644 --- a/spec/rtems/attr/val/attr.yml +++ b/spec/rtems/attr/val/attr.yml @@ -248,6 +248,24 @@ test-actions: - role: validation uid: ../req/semaphore-class links: [] +- action-brief: | + Check the value of ${../if/default:/name}. + action-code: | + /* No action */ + checks: + - brief: | + Check ${../if/default:/name} equals + ``${../if/fifo:/name} | ${../if/local:/name}``. + code: | + T_step_eq_int( + ${step}, + ${../if/default:/name}, + ${../if/fifo:/name} | ${../if/local:/name} + ); + links: + - role: validation + uid: ../req/default-equals + links: [] test-brief: | Tests the attribute constants of the Classic API. test-context: [] diff --git a/spec/rtems/message/glossary/firstmessage.yml b/spec/rtems/message/glossary/firstmessage.yml index d206665f..139850b8 100644 --- a/spec/rtems/message/glossary/firstmessage.yml +++ b/spec/rtems/message/glossary/firstmessage.yml @@ -6,7 +6,7 @@ glossary-type: term links: - role: glossary-member uid: /glossary-requirements -term: First message +term: first message text: | Messages are stored - and kept - in a ${/glossary/messagequeue:/term} in a defined order: Mgs[0], Mgs[1], Mgs[2] till Msg[N-1] when N @@ -20,14 +20,14 @@ text: | place so that "old" message Msg[i] becomes "new" Msg[i-1]. Messages are stored by ${../if/send:/name} in a - ${/glossary/messagequeue:/term} in {/glossary/fifo:/term} order + ${/glossary/messagequeue:/term} in ${/glossary/fifo:/term} order (if no ${../if/receive:/name} directive is waiting to receive a message). ${../if/send:/name} adds the message as "new" last message Msg[N] to the queue and the number of messages in the queue increases by one: N+1. In contrast, messages are stored by ${../if/urgent:/name} in a - ${/glossary/messagequeue:/term} in {/glossary/lifo:/term} order + ${/glossary/messagequeue:/term} in ${/glossary/lifo:/term} order (if no ${../if/receive:/name} directive is waiting to receive a message). ${../if/urgent:/name} adds the message as "new" first message Msg[0] to the queue. The messages which have been in the queue before diff --git a/spec/rtems/message/glossary/lastmessage.yml b/spec/rtems/message/glossary/lastmessage.yml index 73642344..b63fe803 100644 --- a/spec/rtems/message/glossary/lastmessage.yml +++ b/spec/rtems/message/glossary/lastmessage.yml @@ -6,7 +6,7 @@ glossary-type: term links: - role: glossary-member uid: /glossary-requirements -term: Last message +term: last message text: | See ${../glossary/firstmessage:/term}. type: glossary diff --git a/spec/rtems/message/glossary/receiver.yml b/spec/rtems/message/glossary/receiver.yml index f50fbec0..d2e2fb3b 100644 --- a/spec/rtems/message/glossary/receiver.yml +++ b/spec/rtems/message/glossary/receiver.yml @@ -6,12 +6,12 @@ glossary-type: term links: - role: glossary-member uid: /glossary-requirements -term: Receiver +term: receiver text: | - In this particular case, *receiver* shall be a task which invoked - directive ${../if/receice:/name} on the empty ${/glossary/messagequeue:/term} - with ${../if/receive:/params[3]/name} set to ${../../option/if/wait:/name} - and which is still waiting to receive a message when a - ${../if/send:/name} or ${../if/urgent:/name} directive is invoked on - that ${/glossary/messagequeue:/term}. + In this particular case, *receiver* shall be a ${/glossary/task:/term} + which has invoked directive ${../if/receive:/name} with + ${../if/receive:/params[3]/name} set to ${../../option/if/wait:/name} on an + empty ${/glossary/messagequeue:/term} and which is still waiting to receive + a message when a ${../if/send:/name} or ${../if/urgent:/name} directive + is invoked on that ${/glossary/messagequeue:/term}. type: glossary diff --git a/spec/rtems/message/glossary/unblock.yml b/spec/rtems/message/glossary/unblock.yml new file mode 100644 index 00000000..69410c12 --- /dev/null +++ b/spec/rtems/message/glossary/unblock.yml @@ -0,0 +1,23 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +glossary-type: term +links: +- role: glossary-member + uid: /glossary-requirements +term: unblock +text: | + Given a ${/glossary/task:/term} which has invoked an + ${/glossary/rtems:/term} directive and that directive stopped the + execution of this ${/glossary/task:/term}. *Unblock* means that this + ${/glossary/task:/term} stops waiting, the directive returns and the + execution of this ${/glossary/task:/term} continues. + + For example a ${/glossary/task:/term} + which has invoked directive ${../if/receive:/name} and which was + waiting to receive a message from the ${/glossary/messagequeue:/term} + stops waiting because it received a message, + directive ${../if/receive:/name} returns and the execution of this + ${/glossary/task:/term} continues. +type: glossary diff --git a/spec/rtems/message/req/broadcast.yml b/spec/rtems/message/req/broadcast.yml new file mode 100644 index 00000000..9aebd8d2 --- /dev/null +++ b/spec/rtems/message/req/broadcast.yml @@ -0,0 +1,794 @@ +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/broadcast +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_rsc_success( ctx->status ); + text: | + The return status of ${../if/broadcast:/name} shall be + ${../../status/if/successful:/name} + - name: InvId + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ID ); + text: | + The return status of ${../if/broadcast:/name} shall be + ${../../status/if/invalid-id:/name}. + - name: InvAddr + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); + text: | + The return status of ${../if/broadcast:/name} shall be + ${../../status/if/invalid-address:/name}. + - name: InvSize + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_SIZE ); + text: | + The return status of ${../if/broadcast:/name} shall be + ${../../status/if/invalid-size:/name}. + test-epilogue: null + test-prologue: null +- name: Count + states: + - name: Zero + test-code: | + T_eq_u32( ctx->count, 0 ); + text: | + The value of the object referenced by the + ${../if/broadcast:/params[3]/name} parameter shall be set to 0 after + the return of the ${../if/broadcast:/name} call. + - name: Set + test-code: | + T_eq_u32( ctx->count, NUMBER_OF_WORKERS ); + text: | + The value of the object referenced by the + ${../if/broadcast:/params[3]/name} parameter shall be set to the number + of tasks unblocked (see ${../glossary/unblock:/term}) by the call + to directive ${../if/broadcast:/name} after the + return of the ${../if/broadcast:/name} call. + - name: Nop + test-code: | + T_eq_u32( ctx->count, UINT8_MAX ); + text: | + The value of the object referenced by the + ${../if/broadcast:/params[3]/name} + parameter in past call to ${../if/broadcast:/name} shall not be + accessed by the ${../if/broadcast:/name} call + (see also ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: MsgQueue + states: + - name: Nop + test-code: | + ctx->check_msgq_unchanged( ctx ); + text: | + Objects referenced by the ${../if/broadcast:/params[0]/name} + parameter in the past call to ${../if/broadcast:/name} shall not be + accessed by that call (see also ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Receivers + states: + - name: Unblocked + test-code: | + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + T_rsc_success( ctx->receive_status[i] ); + } + text: | + The call to the ${../if/broadcast:/name} directive shall + ${../glossary/unblock:/term} all ${../glossary/receiver:/plural} + waiting for a message at the ${/glossary/messagequeue:/term}. + + Note: Currently, ${../if/broadcast:/name} unblocks + ${../glossary/receiver:/plural} in a none-atomic way. Meaning, + it will not only ${../glossary/unblock:/term} those + ${../glossary/receiver:/plural} it finds waiting at the queue + when ${../if/broadcast:/name} is invoked but also any new + ${../glossary/receiver:/plural} which start waiting for + messages after ${../if/broadcast:/name} is invoked and + before it returns. This may lead to infinite unblocking loops. + - name: Nop + test-code: | + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + T_rsc( ctx->receive_status[i], RTEMS_TIMEOUT ); + } + text: | + The ${../glossary/receiver:/plural} waiting for + a message at the ${/glossary/messagequeue:/term} shall not be affected + by the call to the ${../if/broadcast:/name} directive. + test-epilogue: null + test-prologue: | + size_t i; +- name: RecSize + states: + - name: Message + test-code: | + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + CheckForMessage( + ctx, + ctx->receive_status[i], + ctx->receive_buffer[i], + ctx->receive_size[i] + ); + } + text: | + The values of the objects referenced by the + ${../if/receive:/params[2]/name} parameter in all calls to + ${../if/receive:/name} which are unblocked (see + ${../glossary/unblock:/term}) by the ${../if/broadcast:/name} + call shall be set to the same value as provided by parameter + ${../if/broadcast:/params[2]/name} of the ${../if/broadcast:/name} + call after the return of the ${../if/broadcast:/name} call. + - name: Nop + test-code: | + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + T_eq_sz( ctx->receive_size[i], SIZE_MAX ); + } + text: | + Objects referenced by the ${../if/receive:/params[2]/name} + parameter in past calls to ${../if/receive:/name} shall not be + accessed by the ${../if/broadcast:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: | + size_t i; +- name: RecBuffer + states: + - name: Message + test-code: | + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + CheckForMessage( + ctx, + ctx->receive_status[i], + ctx->receive_buffer[i], + ctx->receive_size[i] + ); + } + text: | + Bytes 0 till ${../if/receive:/params[2]/name} - 1 of the object + referenced by the ${../if/receive:/params[1]/name} parameter in all + calls to ${../if/receive:/name} which are unblocked (see + ${../glossary/unblock:/term}) by the ${../if/broadcast:/name} + call shall be set to the same values as bytes 0 till + ${../if/receive:/params[2]/name} - 1 of the object + referenced by parameter ${../if/broadcast:/params[1]/name} of the + ${../if/broadcast:/name} call after the return of the + ${../if/receive:/name} call. + - name: Nop + test-code: | + for ( w = 0; w < NUMBER_OF_WORKERS; ++w ) { + for ( i = 0; i < MAXIMUM_MESSAGE_SIZE; ++i ) { + T_eq_u8( ctx->receive_buffer[w][i], UINT8_MAX ); + } + } + text: | + Objects referenced by the ${../if/receive:/params[1]/name} + parameter in past calls to ${../if/receive:/name} shall not be + accessed by the ${../if/broadcast:/name} call (see also + ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: | + size_t w, i; +pre-conditions: +- name: SendBuffer + states: + - name: Valid + test-code: | + ctx->buffer_param = &message; + text: | + While the ${../if/broadcast:/params[1]/name} parameter references a memory + area where the message to be sent is stored. + - name: 'Null' + test-code: | + ctx->buffer_param = NULL; + text: | + While the ${../if/broadcast:/params[1]/name} parameter is + ${/c/if/null:/name}. + test-epilogue: null + test-prologue: null +- name: Count + states: + - name: Valid + test-code: | + ctx->count_param = &ctx->count; + text: | + While the ${../if/broadcast:/params[3]/name} parameter references + an ``uint32_t`` object. + - name: 'Null' + test-code: | + ctx->count_param = NULL; + text: | + While the ${../if/broadcast:/params[3]/name} parameter is + ${/c/if/null:/name}. + test-epilogue: null + test-prologue: null +- name: Id + states: + - name: Valid + test-code: | + ctx->id_param = ctx->message_queue_id; + text: | + While the ${../if/broadcast:/params[0]/name} parameter is valid. + - name: Invalid + test-code: | + ctx->id_param = RTEMS_ID_NONE; + text: | + While the ${../if/broadcast:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: MsgSize + states: + - name: Zero + test-code: | + ctx->size_param = 0; + text: | + While the ${../if/broadcast:/params[2]/name} parameter is 0. + - name: SomeSize + test-code: | + ctx->size_param = MAXIMUM_MESSAGE_SIZE / 2 + 1; + text: | + While the ${../if/broadcast:/params[2]/name} parameter has a value + between 0 and the ${../glossary/maximummessagesize:/term}. + - name: MaxSize + test-code: | + ctx->size_param = MAXIMUM_MESSAGE_SIZE; + text: | + While the ${../if/broadcast:/params[2]/name} parameter has a value + of the ${../glossary/maximummessagesize:/term}. + - name: TooLarge + test-code: | + ctx->size_param = MAXIMUM_MESSAGE_SIZE + 1; + text: | + While the ${../if/broadcast:/params[2]/name} parameter has a value + greater than the ${../glossary/maximummessagesize:/term}. + test-epilogue: null + test-prologue: null +- name: MsgQueue + states: + - name: Empty + test-code: | + /* Message queue is already empty. */ + ctx->check_msgq_unchanged = CheckForNoMessageInQueue; + text: | + While there is no message in the ${/glossary/messagequeue:/term}. + - name: Several + test-code: | + SendMsg( ctx ); + SendMsg( ctx ); + ctx->check_msgq_unchanged = CheckForSeveralMessagesInQueue; + text: | + While there are messages in the ${/glossary/messagequeue:/term}. + test-epilogue: null + test-prologue: null +- name: Receivers + states: + - name: Waiting + test-code: | + size_t i; + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + SendEvents( ctx->worker_id[i], EVENT_RECEIVE ); + } + text: | + While one or more ${../glossary/receiver:/plural} are waiting to + receive a message. + - name: None + test-code: | + /* There is already no receiver waiting. */ + text: | + While no ${../glossary/receiver:/term} is waiting to receive a message. + test-epilogue: null + test-prologue: null +- name: Storage + states: + - name: Nop + test-code: | + /* Only a requirement text. */ + text: | + While the memory area to which a pointer is provided as member + ${../if/config:/definition[3]/default/name} of type + ${../if/config:/name} when the ${/glossary/messagequeue:/term} is + constructed by ${../if/construct:/name} is altered only by the + ${/glossary/rtems:/term} operating system. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: + NoWait: | + The ${/glossary/messagequeue:/term} must be empty for an + ${../glossary/receiver:/term} to wait for a message. +test-action: | + ctx->status = rtems_message_queue_broadcast( + ctx->id_param, + ctx->buffer_param, + ctx->size_param, + ctx->count_param + ); + + FinalClockTick(); +test-brief: null +test-cleanup: | + T_rsc_success( rtems_message_queue_delete( ctx->message_queue_id ) ); +test-context: +- brief: | + This member contains a valid ${/glossary/id:/term} of a + ${/glossary/messagequeue:/term}. + description: null + member: | + rtems_id message_queue_id +- brief: | + This member is used as storage area for the + ${/glossary/messagequeue:/term}. + description: null + member: | + RTEMS_MESSAGE_QUEUE_BUFFER( MAXIMUM_MESSAGE_SIZE ) + storage_area[ MAXIMUM_PENDING_MESSAGES ] +- brief: | + This member contains a buffer to receive messages from the queue. + description: null + member: | + uint8_t receive_buffer[ NUMBER_OF_WORKERS ][ MAXIMUM_MESSAGE_SIZE ] +- brief: | + This member contains several buffers to receive a messages size. + description: null + member: | + size_t receive_size[ NUMBER_OF_WORKERS ] +- brief: | + This member contains the returned ${/glossary/statuscode:/plural} + of the receivers. + description: null + member: | + rtems_status_code receive_status[ NUMBER_OF_WORKERS ] +- brief: | + This member specifies the ${../if/broadcast:/params[0]/name} parameter + of the action. + description: null + member: | + rtems_id id_param +- brief: | + This member specifies the ${../if/broadcast:/params[1]/name} parameter + of the action. + description: null + member: | + const void *buffer_param +- brief: | + This member specifies the ${../if/broadcast:/params[2]/name} parameter + of the action. + description: null + member: | + size_t size_param +- brief: | + This member specifies the ${../if/broadcast:/params[3]/name} parameter + of the action. + description: null + member: | + uint32_t *count_param +- brief: | + This member contains the returned ${/glossary/statuscode:/term} + of the action. + description: null + member: | + rtems_status_code status +- brief: | + This member contains the value returned in parameter + ${../if/broadcast:/params[3]/name} of the action. + description: null + member: | + uint32_t count +- brief: | + This member contains the ${/glossary/task:/term} identifier of the + main ${/glossary/task:/term}. + description: null + member: | + rtems_id task_id +- brief: | + This member contains the ${/glossary/task:/term} identifiers of the + worker ${/glossary/task:/plural}. + description: null + member: | + rtems_id worker_id[ NUMBER_OF_WORKERS ] +- brief: | + This member contains a pointer to a function which is executed + to check that the action has not changed the content of the + ${/glossary/messagequeue:/term}. + description: null + member: | + void (*check_msgq_unchanged)( void *ctx_in ) +test-context-support: | + #define MAXIMUM_PENDING_MESSAGES 3 + #define MAXIMUM_MESSAGE_SIZE 5 + #define NUMBER_OF_WORKERS 3 +test-description: null +test-header: null +test-includes: +- rtems.h +test-local-includes: +- tx-support.h +test-prepare: | + rtems_status_code status; + size_t i; + + rtems_message_queue_config config = { + .name = rtems_build_name( 'M', 'S', 'G', 'Q' ), + .maximum_pending_messages = MAXIMUM_PENDING_MESSAGES, + .maximum_message_size = MAXIMUM_MESSAGE_SIZE, + .storage_area = ctx->storage_area, + .storage_size = sizeof( ctx->storage_area ), + .storage_free = NULL, + .attributes = RTEMS_DEFAULT_ATTRIBUTES + }; + + status = rtems_message_queue_construct( + &config, + &ctx->message_queue_id + ); + T_rsc_success( status ); + + ctx->count = UINT8_MAX; + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + ctx->receive_size[i] = SIZE_MAX; + memset( ctx->receive_buffer[i], UINT8_MAX, MAXIMUM_MESSAGE_SIZE ); + } +test-setup: + brief: null + code: | + size_t i; + ctx->task_id = rtems_task_self(); + SetSelfPriority( PRIO_NORMAL ); + + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + ctx->worker_id[i] = CreateTask( "WORK", PRIO_HIGH ); + StartTask( ctx->worker_id[i], WorkerTask, ctx ); + } + description: null +test-stop: null +test-support: | + typedef ${.:/test-context-type} Context; + static const rtems_interval TIMEOUT_TICKS = 1; + static const rtems_event_set EVENT_RECEIVE = RTEMS_EVENT_17; + static const uint8_t message[ MAXIMUM_MESSAGE_SIZE ] = + { 13, 42, 99, 222, 101 }; + static const uint8_t queued_message[] = { 200, 201, 202 }; + + static void Receive( Context *ctx, size_t worker_index ) + { + ctx->receive_status[worker_index] = rtems_message_queue_receive( + ctx->message_queue_id, + ctx->receive_buffer[worker_index], + &ctx->receive_size[worker_index], + RTEMS_WAIT, + TIMEOUT_TICKS + ); + } + + static void WorkerTask( rtems_task_argument argument ) + { + static size_t worker_number = 0; + size_t worker_index = worker_number++; + Context *ctx = (Context *) argument; + + while ( true ) { + ReceiveAnyEvents(); + Receive( ctx, worker_index ); + } + } + + static void CheckForNoMessage( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + { + (void) ctx; + (void) message_buffer; + (void) message_size; + T_rsc( status, RTEMS_UNSATISFIED ); + } + + static void CheckForMessage( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + { + T_rsc_success( status ); + T_eq_u32( message_size, ctx->size_param ); + T_eq_mem( message_buffer, message, ctx->size_param ); + } + + static void CheckForQueuedMessage( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + { + (void) ctx; + T_rsc_success( status ); + T_eq_u32( message_size, sizeof( queued_message ) ); + T_eq_mem( message_buffer, queued_message, sizeof( queued_message ) ); + } + + static void PopMessage( + Context *ctx, + void (*check_fn)( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + ) + { + rtems_status_code status; + uint8_t message_buffer[ MAXIMUM_MESSAGE_SIZE ]; + size_t message_size; + + status = rtems_message_queue_receive( + ctx->message_queue_id, + &message_buffer, + &message_size, + RTEMS_LOCAL | RTEMS_NO_WAIT, + RTEMS_NO_TIMEOUT + ); + + check_fn( ctx, status, message_buffer, message_size ); + } + + static void CheckForNoMessageInQueue( void *ctx_in ) + { + Context *ctx = ctx_in; + PopMessage( ctx, CheckForNoMessage ); + } + + static void CheckForSeveralMessagesInQueue( void *ctx_in ) + { + Context *ctx = ctx_in; + PopMessage( ctx, CheckForQueuedMessage ); + PopMessage( ctx, CheckForQueuedMessage ); + PopMessage( ctx, CheckForNoMessage ); + } + + static void SendMsg( Context *ctx ) + { + rtems_status_code status; + + status = rtems_message_queue_send( + ctx->message_queue_id, + queued_message, + sizeof( queued_message ) + ); + T_rsc_success( status ); + } + +test-target: testsuites/validation/tc-message-broadcast.c +test-teardown: + brief: null + code: | + size_t i; + + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + DeleteTask( ctx->worker_id[i] ); + } + RestoreRunnerPriority(); + description: null +text: ${.:text-template} +transition-map: + +# ---- Ok Case ---- + +- enabled-by: true + post-conditions: + Status: Ok + Count: + - if: + pre-conditions: + Receivers: Waiting + then: Set + - else: Zero + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Unblocked + - else: N/A + RecSize: + - if: + pre-conditions: + Receivers: Waiting + then: Message + - else: N/A + RecBuffer: + - if: + pre-conditions: + Receivers: Waiting + then: Message + - else: N/A + pre-conditions: + SendBuffer: + - Valid + Count: + - Valid + Id: + - Valid + MsgSize: + - Zero + - SomeSize + - MaxSize + MsgQueue: all + Receivers: all + Storage: all + +# ---- InvAddr: SendBuffer ---- + +- enabled-by: true + post-conditions: + Status: InvAddr + Count: Nop + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecSize: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecBuffer: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + SendBuffer: + - 'Null' + Count: all + Id: all + MsgSize: all + MsgQueue: all + Receivers: all + Storage: all + +# ---- InvAddr: Count ---- + +- enabled-by: true + post-conditions: + Status: InvAddr + Count: Nop + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecSize: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecBuffer: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + SendBuffer: + - Valid + Count: + - 'Null' + Id: all + MsgSize: all + MsgQueue: all + Receivers: all + Storage: all + +# ---- InvId ---- + +- enabled-by: true + post-conditions: + Status: InvId + Count: Nop + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecSize: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecBuffer: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + SendBuffer: + - Valid + Count: + - Valid + Id: + - Invalid + MsgSize: all + MsgQueue: all + Receivers: all + Storage: all + +# ---- InvSize ---- + +- enabled-by: true + post-conditions: + Status: InvSize + Count: Nop + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecSize: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecBuffer: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + SendBuffer: + - Valid + Count: + - Valid + Id: + - Valid + MsgSize: + - TooLarge + MsgQueue: all + Receivers: all + Storage: all + +# ---- Impossible Cases ---- + +- enabled-by: true + post-conditions: NoWait + pre-conditions: + SendBuffer: all + Count: all + Id: all + MsgSize: all + MsgQueue: + - Several + Receivers: + - Waiting + Storage: all + +type: requirement diff --git a/spec/rtems/message/req/flush-pending.yml b/spec/rtems/message/req/flush-pending.yml new file mode 100644 index 00000000..3214af93 --- /dev/null +++ b/spec/rtems/message/req/flush-pending.yml @@ -0,0 +1,562 @@ +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/flush +- role: interface-function + uid: ../if/get-number-pending +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_rsc_success( ctx->status ); + text: | + The return status of the called directive (${../if/flush:/name} or + ${../if/get-number-pending:/name}) shall be + ${../../status/if/successful:/name} + - name: InvId + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ID ); + text: | + The return status of the called directive (${../if/flush:/name} or + ${../if/get-number-pending:/name}) shall be + ${../../status/if/invalid-id:/name}. + - name: InvAddr + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); + text: | + The return status of the called directive (${../if/flush:/name} or + ${../if/get-number-pending:/name}) shall be + ${../../status/if/invalid-address:/name}. + test-epilogue: null + test-prologue: null +- name: Count + states: + - name: Zero + test-code: | + T_eq_u32( ctx->count, 0 ); + text: | + The value of the object referenced by the + ${../if/flush:/params[1]/name} parameter shall be 0 after + the return of the ${../if/flush:/name} or + ${../if/get-number-pending:/name} call. + - name: Set + test-code: | + T_eq_u32( ctx->count, NUMBER_OF_PENDING_MESSAGES ); + text: | + The ${../if/get-number-pending:/name} directive shall set + the value of the object referenced by the + ${../if/get-number-pending:/params[1]/name} parameter to the number + of messages present in the ${/glossary/messagequeue:/term} + at a point in time during the single execution of the + ${../if/get-number-pending:/name} directive. + + The ${../if/flush:/name} directive shall set + the value of the object referenced by the + ${../if/flush:/params[1]/name} parameter to the number + of messages it removed from the ${/glossary/messagequeue:/term} + during the single execution of the ${../if/flush:/name} directive. + - name: Nop + test-code: | + T_eq_u32( ctx->count, UINT8_MAX ); + text: | + The value of the object referenced by the + ${../if/flush:/params[1]/name} parameter in past call + to ${../if/flush:/name} or ${../if/get-number-pending:/name} + shall not be accessed by the ${../if/flush:/name} or + ${../if/get-number-pending:/name} call + (see also ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: MsgQueue + states: + - name: Empty + test-code: | + PopMessage( ctx, CheckForNoMessage ); + text: | + The ${/glossary/messagequeue:/term} shall contain no messages + after the last call to ${../if/flush:/params[0]/name}. + - name: Nop + test-code: | + ctx->check_msgq_unchanged( ctx ); + text: | + Objects referenced by the ${../if/flush:/params[0]/name} + parameter in the past call to ${../if/flush:/name} or + ${../if/get-number-pending:/name} shall not be + changed by that call (see also ${../glossary/nop:/term}). + test-epilogue: null + test-prologue: null +- name: Receivers + states: + - name: Nop + test-code: | + size_t i; + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + T_rsc( ctx->receive_status[i], RTEMS_TIMEOUT ); + } + text: | + The ${../glossary/receiver:/plural} waiting for + a message at the ${/glossary/messagequeue:/term} shall not be affected + by the call to the ${../if/flush:/name} or + ${../if/get-number-pending:/name} directive. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: Count + states: + - name: Valid + test-code: | + ctx->count_param = &ctx->count; + text: | + While the ${../if/flush:/params[1]/name} parameter references + an ``uint32_t`` object. + - name: 'Null' + test-code: | + ctx->count_param = NULL; + text: | + While the ${../if/flush:/params[1]/name} parameter is + ${/c/if/null:/name}. + test-epilogue: null + test-prologue: null +- name: Id + states: + - name: Valid + test-code: | + ctx->id_param = ctx->message_queue_id; + text: | + While the ${../if/flush:/params[0]/name} parameter is valid. + - name: Invalid + test-code: | + ctx->id_param = RTEMS_ID_NONE; + text: | + While the ${../if/flush:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: MsgQueue + states: + - name: Empty + test-code: | + /* Message queue is already empty. */ + ctx->check_msgq_unchanged = CheckForNoMessageInQueue; + text: | + While there is no message in the ${/glossary/messagequeue:/term}. + - name: Several + test-code: | + uint32_t i; + for ( i = 0; i < NUMBER_OF_PENDING_MESSAGES; ++i ) { + SendMsg( ctx ); + } + ctx->check_msgq_unchanged = CheckForSeveralMessagesInQueue; + text: | + While there are messages in the ${/glossary/messagequeue:/term}. + test-epilogue: null + test-prologue: null +- name: Receivers + states: + - name: Waiting + test-code: | + size_t i; + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + SendEvents( ctx->worker_id[i], EVENT_RECEIVE ); + } + text: | + While one or more ${../glossary/receiver:/plural} are waiting to + receive a message. + - name: None + test-code: | + /* There is already no receiver waiting. */ + text: | + While no ${../glossary/receiver:/term} is waiting to receive a message. + test-epilogue: null + test-prologue: null +- name: Directive + states: + - name: Flush + test-code: | + ctx->action = rtems_message_queue_flush; + text: | + While the directive ${../if/flush:/name} is called. + - name: Pending + test-code: | + ctx->action = rtems_message_queue_get_number_pending; + text: | + While the directive ${../if/get-number-pending:/name} is called. + test-epilogue: null + test-prologue: null +- name: Storage + states: + - name: Nop + test-code: | + /* Only a requirement text. */ + text: | + While the memory area to which a pointer is provided as member + ${../if/config:/definition[3]/default/name} of type + ${../if/config:/name} when the ${/glossary/messagequeue:/term} is + constructed by ${../if/construct:/name} is altered only by the + ${/glossary/rtems:/term} operating system. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: + NoWait: | + The ${/glossary/messagequeue:/term} must be empty for an + ${../glossary/receiver:/term} to wait for a message. +test-action: | + ctx->status = (ctx->action)( + ctx->id_param, + ctx->count_param + ); + + FinalClockTick(); +test-brief: null +test-cleanup: | + T_rsc_success( rtems_message_queue_delete( ctx->message_queue_id ) ); +test-context: +- brief: | + This member contains a valid ${/glossary/id:/term} of a + ${/glossary/messagequeue:/term}. + description: null + member: | + rtems_id message_queue_id +- brief: | + This member is used as storage area for the + ${/glossary/messagequeue:/term}. + description: null + member: | + RTEMS_MESSAGE_QUEUE_BUFFER( MAXIMUM_MESSAGE_SIZE ) + storage_area[ MAXIMUM_PENDING_MESSAGES ] +- brief: | + This member contains the returned ${/glossary/statuscode:/plural} + of the receivers. + description: null + member: | + rtems_status_code receive_status[ NUMBER_OF_WORKERS ] +- brief: | + This member specifies the directive to be called as action. + description: | + This is either ${../if/flush:/name} or ${../if/get-number-pending:/name}. + member: + rtems_status_code (*action)( rtems_id id, uint32_t *count ) +- brief: | + This member specifies the ${../if/flush:/params[0]/name} parameter + of the action. + description: null + member: | + rtems_id id_param +- brief: | + This member specifies the ${../if/flush:/params[1]/name} parameter + of the action. + description: null + member: | + uint32_t *count_param +- brief: | + This member contains the returned ${/glossary/statuscode:/term} + of the action. + description: null + member: | + rtems_status_code status +- brief: | + This member contains the value returned in parameter + ${../if/flush:/params[1]/name} of the action. + description: null + member: | + uint32_t count +- brief: | + This member contains the ${/glossary/task:/term} identifier of the + main ${/glossary/task:/term}. + description: null + member: | + rtems_id task_id +- brief: | + This member contains the ${/glossary/task:/term} identifiers of the + worker ${/glossary/task:/plural}. + description: null + member: | + rtems_id worker_id[ NUMBER_OF_WORKERS ] +- brief: | + This member contains a pointer to a function which is executed + to check that the action has not changed the content of the + ${/glossary/messagequeue:/term}. + description: null + member: | + void (*check_msgq_unchanged)( void *ctx_in ) +test-context-support: | + #define MAXIMUM_PENDING_MESSAGES 3 + #define MAXIMUM_MESSAGE_SIZE 5 + #define NUMBER_OF_WORKERS 3 +test-description: null +test-header: null +test-includes: +- rtems.h +test-local-includes: +- tx-support.h +test-prepare: | + rtems_status_code status; + + rtems_message_queue_config config = { + .name = rtems_build_name( 'M', 'S', 'G', 'Q' ), + .maximum_pending_messages = MAXIMUM_PENDING_MESSAGES, + .maximum_message_size = MAXIMUM_MESSAGE_SIZE, + .storage_area = ctx->storage_area, + .storage_size = sizeof( ctx->storage_area ), + .storage_free = NULL, + .attributes = RTEMS_DEFAULT_ATTRIBUTES + }; + + status = rtems_message_queue_construct( + &config, + &ctx->message_queue_id + ); + T_rsc_success( status ); + + ctx->count = UINT8_MAX; +test-setup: + brief: null + code: | + size_t i; + ctx->task_id = rtems_task_self(); + SetSelfPriority( PRIO_NORMAL ); + + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + ctx->worker_id[i] = CreateTask( "WORK", PRIO_HIGH ); + StartTask( ctx->worker_id[i], WorkerTask, ctx ); + } + description: null +test-stop: null +test-support: | + typedef ${.:/test-context-type} Context; + static const uint32_t NUMBER_OF_PENDING_MESSAGES = 2; + static const rtems_interval TIMEOUT_TICKS = 1; + static const rtems_event_set EVENT_RECEIVE = RTEMS_EVENT_17; + static const uint8_t queued_message[] = { 200, 201, 202 }; + + static void Receive( Context *ctx, size_t worker_index ) + { + size_t size; + uint8_t buffer[ MAXIMUM_MESSAGE_SIZE ]; + + ctx->receive_status[worker_index] = rtems_message_queue_receive( + ctx->message_queue_id, + buffer, + &size, + RTEMS_WAIT, + TIMEOUT_TICKS + ); + } + + static void WorkerTask( rtems_task_argument argument ) + { + static size_t worker_number = 0; + size_t worker_index = worker_number++; + Context *ctx = (Context *) argument; + + while ( true ) { + ReceiveAnyEvents(); + Receive( ctx, worker_index ); + } + } + + static void CheckForNoMessage( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + { + (void) ctx; + (void) message_buffer; + (void) message_size; + T_rsc( status, RTEMS_UNSATISFIED ); + } + + static void CheckForQueuedMessage( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + { + (void) ctx; + T_rsc_success( status ); + T_eq_u32( message_size, sizeof( queued_message ) ); + T_eq_mem( message_buffer, queued_message, sizeof( queued_message ) ); + } + + static void PopMessage( + Context *ctx, + void (*check_fn)( + Context *ctx, + rtems_status_code status, + uint8_t *message_buffer, + size_t message_size + ) + ) + { + rtems_status_code status; + uint8_t message_buffer[ MAXIMUM_MESSAGE_SIZE ]; + size_t message_size; + + status = rtems_message_queue_receive( + ctx->message_queue_id, + &message_buffer, + &message_size, + RTEMS_LOCAL | RTEMS_NO_WAIT, + RTEMS_NO_TIMEOUT + ); + + check_fn( ctx, status, message_buffer, message_size ); + } + + static void CheckForNoMessageInQueue( void *ctx_in ) + { + Context *ctx = ctx_in; + PopMessage( ctx, CheckForNoMessage ); + } + + static void CheckForSeveralMessagesInQueue( void *ctx_in ) + { + Context *ctx = ctx_in; + uint32_t i; + for ( i = 0; i < NUMBER_OF_PENDING_MESSAGES; ++i ) { + PopMessage( ctx, CheckForQueuedMessage ); + } + PopMessage( ctx, CheckForNoMessage ); + } + + static void SendMsg( Context *ctx ) + { + rtems_status_code status; + + status = rtems_message_queue_send( + ctx->message_queue_id, + queued_message, + sizeof( queued_message ) + ); + T_rsc_success( status ); + } + +test-target: testsuites/validation/tc-message-flush-pending.c +test-teardown: + brief: null + code: | + size_t i; + + for ( i = 0; i < NUMBER_OF_WORKERS; ++i ) { + DeleteTask( ctx->worker_id[i] ); + } + RestoreRunnerPriority(); + description: null +text: ${.:text-template} +transition-map: + +# ---- Ok Case ---- + +- enabled-by: true + post-conditions: + Status: Ok + Count: + - if: + pre-conditions: + MsgQueue: Several + then: Set + - else: Zero + MsgQueue: + - if: + pre-conditions: + Directive: Flush + then: Empty + - else: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + Count: + - Valid + Id: + - Valid + MsgQueue: all + Receivers: all + Directive: all + Storage: all + +# ---- InvAddr: Count ---- + +- enabled-by: true + post-conditions: + Status: InvAddr + Count: Nop + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + Count: + - 'Null' + Id: all + MsgQueue: all + Receivers: all + Directive: all + Storage: all + +# ---- InvId ---- + +- enabled-by: true + post-conditions: + Status: InvId + Count: Nop + MsgQueue: Nop + Receivers: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecSize: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + RecBuffer: + - if: + pre-conditions: + Receivers: Waiting + then: Nop + - else: N/A + pre-conditions: + Count: + - Valid + Id: + - Invalid + MsgQueue: all + Receivers: all + Directive: all + Storage: all + +# ---- Impossible Cases ---- + +- enabled-by: true + post-conditions: NoWait + pre-conditions: + Count: all + Id: all + MsgQueue: + - Several + Receivers: + - Waiting + Directive: all + Storage: all + +type: requirement diff --git a/spec/rtems/message/req/receive.yml b/spec/rtems/message/req/receive.yml index ce20d336..b32b9eb7 100644 --- a/spec/rtems/message/req/receive.yml +++ b/spec/rtems/message/req/receive.yml @@ -644,6 +644,8 @@ test-support: | size_t message_size ) { + (void) message_buffer; + (void) message_size; T_rsc( status, RTEMS_UNSATISFIED ); } diff --git a/spec/rtems/message/req/urgent-send.yml b/spec/rtems/message/req/urgent-send.yml index 92c1cbe0..5a0c7a4e 100644 --- a/spec/rtems/message/req/urgent-send.yml +++ b/spec/rtems/message/req/urgent-send.yml @@ -329,9 +329,10 @@ test-context: uint8_t send_message[ MAXIMUM_MESSAGE_SIZE ] - brief: | This member specifies the directive to be called as action. - description: This is either ${../if/send:/name} or ${../if/urgent:/name}. + description: | + This is either ${../if/send:/name} or ${../if/urgent:/name}. member: - rtems_status_code (*action)( rtems_id id, const void *buffer, size_t size ) + rtems_status_code (*action)( rtems_id id, const void *buffer, size_t size ) - brief: | This member specifies the ${../if/send:/params[0]/name} parameter for the action. diff --git a/spec/rtems/message/val/message-macros.yml b/spec/rtems/message/val/message-macros.yml index c4eab2bc..e956ee1f 100644 --- a/spec/rtems/message/val/message-macros.yml +++ b/spec/rtems/message/val/message-macros.yml @@ -5,42 +5,6 @@ enabled-by: true links: [] test-actions: -# ---- RTEMS_DEFAULT_ATTRIBUTES ---- - -- action-brief: | - Check the value of the ${../../attr/if/default:/name}. - action-code: | - /* No action */ - checks: - - brief: | - Check ${../../attr/if/default:/name} equals ``RTEMS_FIFO | RTEMS_LOCAL``. - code: | - T_step_eq_int( - ${step}, - ${../../attr/if/default:/name}, - RTEMS_FIFO | RTEMS_LOCAL - ); - links: - - role: validation - uid: ../req/attributes - links: [] - -# ---- RTEMS_DEFAULT_OPTIONS ---- - -- action-brief: | - Check the value of the ${../../option/if/default:/name}. - action-code: | - /* No action */ - checks: - - brief: | - Check ${../../option/if/default:/name} equals ``RTEMS_WAIT``. - code: | - T_step_eq_int( ${step}, ${../../option/if/default:/name}, RTEMS_WAIT ); - links: - - role: validation - uid: ../req/options - links: [] - # ---- RTEMS_MESSAGE_QUEUE_BUFFER ---- - action-brief: | diff --git a/spec/rtems/message/req/options.yml b/spec/rtems/option/req/default-equals.yml index a0fe5a0b..bf133569 100644 --- a/spec/rtems/message/req/options.yml +++ b/spec/rtems/option/req/default-equals.yml @@ -4,12 +4,12 @@ copyrights: enabled-by: true links: - role: requirement-refinement - uid: ../../option/if/default + uid: ../if/default non-functional-type: interface rationale: null references: [] requirement-type: non-functional text: | - The value of macro ${../../option/if/default:/name} shall be equal - to the value of the expression ``RTEMS_WAIT``. + The value of macro ${../if/default:/name} shall be equal + to the value of expression ``${../if/wait:/name}``. type: requirement diff --git a/spec/rtems/option/val/options.yml b/spec/rtems/option/val/options.yml index 21a8c0ee..6659e26d 100644 --- a/spec/rtems/option/val/options.yml +++ b/spec/rtems/option/val/options.yml @@ -85,6 +85,19 @@ test-actions: - role: validation uid: ../if/no-wait links: [] +- action-brief: | + Check the value of ${../if/default:/name}. + action-code: | + /* No action */ + checks: + - brief: | + Check ${..//if/default:/name} equals ``${../if/wait:/name}``. + code: | + T_step_eq_int( ${step}, ${../if/default:/name}, ${../if/wait:/name} ); + links: + - role: validation + uid: ../req/default-equals + links: [] test-brief: | Tests the option constants of the Classic API. test-context: [] |