From ca758d1a46331c6bf7e8ef405e67fa76a6f2f7c5 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Fri, 25 Sep 2020 09:02:19 +0200 Subject: spec: Add rtems_message_queue_construct() --- spec/rtems/message/if/buffer.yml | 34 +++ spec/rtems/message/if/config.yml | 85 ++++++ spec/rtems/message/if/construct.yml | 92 ++++++ spec/rtems/message/req/construct-errors.yml | 456 ++++++++++++++++++++++++++++ spec/score/msgq/if/buffer.yml | 11 + spec/score/msgq/if/header.yml | 12 + spec/score/msgq/if/header2.yml | 12 + 7 files changed, 702 insertions(+) create mode 100644 spec/rtems/message/if/buffer.yml create mode 100644 spec/rtems/message/if/config.yml create mode 100644 spec/rtems/message/if/construct.yml create mode 100644 spec/rtems/message/req/construct-errors.yml create mode 100644 spec/score/msgq/if/buffer.yml create mode 100644 spec/score/msgq/if/header.yml create mode 100644 spec/score/msgq/if/header2.yml diff --git a/spec/rtems/message/if/buffer.yml b/spec/rtems/message/if/buffer.yml new file mode 100644 index 00000000..0ff6bd16 --- /dev/null +++ b/spec/rtems/message/if/buffer.yml @@ -0,0 +1,34 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: | + Defines a structure which can be used as a message queue buffer for messages + of the specified maximum size. +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +definition: + default: | + struct { + ${/score/msgq/if/buffer:/name} _buffer; + char _message[ ${.:/params[0]/name} ]; + } + variants: [] +description: null +enabled-by: true +interface-type: macro +links: +- role: interface-placement + uid: header +- role: interface-ingroup + uid: group +name: RTEMS_MESSAGE_QUEUE_BUFFER +notes: | + Use this macro to define the message buffer storage area for + ${construct:/name}. +params: +- description: | + is the maximum message size in bytes. + dir: null + name: _maximum_message_size +return: + return: null + return-values: [] +type: interface diff --git a/spec/rtems/message/if/config.yml b/spec/rtems/message/if/config.yml new file mode 100644 index 00000000..81c052f7 --- /dev/null +++ b/spec/rtems/message/if/config.yml @@ -0,0 +1,85 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: | + This structure defines the configuration of a message queue constructed by + ${construct:/name}. +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +definition: +- default: + brief: | + This member defines the name of the message queue. + definition: ${../../type/if/name:/name} ${.:name} + description: null + kind: member + name: name + variants: [] +- default: + brief: | + This member defines the maximum number of pending messages supported by + the message queue. + definition: ${/c/if/uint32_t:/name} ${.:name} + description: null + kind: member + name: maximum_pending_messages + variants: [] +- default: + brief: | + This member defines the maximum message size supported by the message + queue. + definition: ${/c/if/size_t:/name} ${.:name} + description: null + kind: member + name: maximum_message_size + variants: [] +- default: + brief: | + This member shall point to the message buffer storage area begin. + definition: void *${.:name} + description: | + The message buffer storage area for the message queue shall be an array + of the type defined by ${buffer:/name} with a maximum message size equal + to the maximum message size of this configuration. + kind: member + name: storage_area + variants: [] +- default: + brief: | + This member defines size of the message buffer storage area in bytes. + definition: ${/c/if/size_t:/name} ${.:name} + description: null + kind: member + name: storage_size + variants: [] +- default: + brief: | + This member defines the optional handler to free the message buffer + storage area. + definition: void ( *${.:name} )( void * ) + description: | + It is called when the message queue is deleted. It is called from task + context under protection of the object allocator lock. It is allowed to + call ${/c/if/free:/name} in this handler. If handler is + ${/c/if/null:/name}, then no action will be performed. + kind: member + name: storage_free + variants: [] +- default: + brief: | + This member defines the attributes of the message queue. + definition: ${../../attr/if/attribute:/name} ${.:name} + description: null + kind: member + name: attributes + variants: [] +definition-kind: typedef-only +description: null +enabled-by: true +interface-type: struct +links: +- role: interface-placement + uid: header +- role: interface-ingroup + uid: group +name: rtems_message_queue_config +notes: null +type: interface diff --git a/spec/rtems/message/if/construct.yml b/spec/rtems/message/if/construct.yml new file mode 100644 index 00000000..92b5ff92 --- /dev/null +++ b/spec/rtems/message/if/construct.yml @@ -0,0 +1,92 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: | + Constructs a message queue from the specified the message queue + configuration. +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +definition: + default: + body: null + params: + - const ${config:/name} *${.:/params[0]/name} + - ${../../type/if/id:/name} *${.:/params[1]/name} + return: ${../../status/if/code:/name} + variants: [] +description: null +enabled-by: true +interface-type: function +links: +- role: interface-placement + uid: header +- role: interface-ingroup + uid: group +name: rtems_message_queue_construct +notes: | + In contrast to message queues created by ${create:/name}, the message queues + constructed by this directive use a user-provided message buffer storage + area. + + This directive is intended for applications which do not want to use the + RTEMS Workspace and instead statically allocate all operating system + resources. An application based solely on static allocation can avoid any + runtime memory allocators. This can simplify the application architecture + as well as any analysis that may be required. + + The value for ${/acfg/if/message-buffer-memory:/name} should not include + memory for message queues constructed by ${.:/name}. +params: +- description: is the message queue configuration. + dir: null + name: config +- description: | + is the pointer to an object identifier variable. The identifier of the + constructed message queue object will be stored in this variable, in case + of a successful operation. + dir: out + name: id +return: + return: null + return-values: + - description: | + The requested operation was successful. + value: ${../../status/if/successful:/name} + - description: | + The ${.:/params[1]/name} parameter was ${/c/if/null:/name}. + value: ${../../status/if/invalid-address:/name} + - description: | + The message queue name in the configuration was invalid. + value: ${../../status/if/invalid-name:/name} + - description: | + The maximum number of pending messages in the configuration was zero. + value: ${../../status/if/invalid-number:/name} + - description: | + The maximum message size in the configuration was zero. + value: ${../../status/if/invalid-size:/name} + - description: | + There was no inactive message queue object available to construct a + message queue. + value: ${../../status/if/too-many:/name} + - description: | + In multiprocessing configurations, there was no inactive global object + available to construct a global message queue. + value: ${../../status/if/too-many:/name} + - description: | + The maximum message size in the configuration was too big and resulted in + integer overflows in calculations carried out to determine the size of + the message buffer area. + value: ${../../status/if/invalid-size:/name} + - description: | + The maximum number of pending messages in the configuration was too big + and resulted in integer overflows in calculations carried out to + determine the size of the message buffer area. + value: ${../../status/if/invalid-number:/name} + - description: | + The message queue storage area begin pointer in the configuration was + ${/c/if/null:/name}. + value: ${../../status/if/unsatisfied:/name} + - description: | + The message queue storage area size in the configuration was not equal to + the size calculated from the maximum number of pending messages and the + maximum message size. + value: ${../../status/if/unsatisfied:/name} +type: interface diff --git a/spec/rtems/message/req/construct-errors.yml b/spec/rtems/message/req/construct-errors.yml new file mode 100644 index 00000000..72f91926 --- /dev/null +++ b/spec/rtems/message/req/construct-errors.yml @@ -0,0 +1,456 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +functional-type: action +links: +- role: interface-function + uid: ../if/construct +post-conditions: +- name: Status + states: + - name: Ok + test-code: | + T_rsc_success( ctx->status ); + T_eq_ptr( ctx->id, &ctx->id_value ); + T_ne_u32( ctx->id_value, 0xffffffff ); + + sc = rtems_message_queue_delete( ctx->id_value ); + T_rsc_success( sc ); + text: | + The status shall be RTEMS_SUCCESSFUL. The value of the object identifier + referenced by the id parameter shall identify the constructed message + queue. + - name: InvAddress + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); + T_null( ctx->id ); + T_eq_u32( ctx->id_value, 0xffffffff ); + text: | + The status shall be RTEMS_INVALID_ADDRESS. + - name: InvName + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_NAME ); + T_eq_u32( ctx->id_value, 0xffffffff ); + text: | + The status shall be RTEMS_INVALID_NAME. If the id parameter is not NULL, + then the value of the object identifier referenced by the id parameter + shall be unchanged. + - name: InvNumber + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_NUMBER ); + T_eq_u32( ctx->id_value, 0xffffffff ); + text: | + The status shall be RTEMS_INVALID_NUMBER. If the id parameter is not + NULL, then the value of the object identifier referenced by the id + parameter shall be unchanged. + - name: InvSize + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_SIZE ); + T_eq_u32( ctx->id_value, 0xffffffff ); + text: | + The status shall be RTEMS_INVALID_SIZE. If the id parameter is not NULL, + then the value of the object identifier referenced by the id parameter + shall be unchanged. + - name: TooMany + test-code: | + T_rsc( ctx->status, RTEMS_TOO_MANY ); + T_eq_u32( ctx->id_value, 0xffffffff ); + text: | + The status shall be RTEMS_TOO_MANY. If the id parameter is not NULL, + then the value of the object identifier referenced by the id parameter + shall be unchanged. + - name: Unsatisfied + test-code: | + T_rsc( ctx->status, RTEMS_UNSATISFIED ); + T_eq_u32( ctx->id_value, 0xffffffff ); + text: | + The status shall be RTEMS_UNSATISFIED. If the id parameter is not NULL, + then the value of the object identifier referenced by the id parameter + shall be unchanged. + test-epilogue: null + test-prologue: | + rtems_status_code sc; +pre-conditions: +- name: Id + states: + - name: Id + test-code: | + ctx->id = &ctx->id_value; + text: | + The id parameter shall reference an object identifier value. + - name: 'Null' + test-code: | + ctx->id = NULL; + text: | + The id parameter shall be NULL. + test-epilogue: null + test-prologue: null +- name: Name + states: + - name: Valid + test-code: | + ctx->config.name = rtems_build_name( 'N', 'A', 'M', 'E' ); + text: | + The name of the message queue configuration shall be valid. + - name: Invalid + test-code: | + ctx->config.name = 0; + text: | + The name of the message queue configuration shall be invalid. + test-epilogue: null + test-prologue: null +- name: MaxPending + states: + - name: Valid + test-code: | + ctx->config.maximum_pending_messages = MAX_PENDING_MESSAGES; + text: | + The maximum number of pending messages of the message queue configuration + shall be valid. + - name: Zero + test-code: | + ctx->config.maximum_pending_messages = 0; + text: | + The maximum number of pending messages of the message queue configuration + shall be zero. + - name: Big + test-code: | + ctx->config.maximum_pending_messages = UINT32_MAX; + text: | + The maximum number of pending messages of the message queue configuration + shall be big enough so that a calculation to get the message buffer + storage area size overflows. + test-epilogue: null + test-prologue: null +- name: MaxSize + states: + - name: Valid + test-code: | + ctx->config.maximum_message_size = MAX_MESSAGE_SIZE; + text: | + The maximum message size of the message queue configuration shall be + valid. + - name: Zero + test-code: | + ctx->config.maximum_message_size = 0; + text: | + The maximum message size of the message queue configuration shall be + zero. + - name: Big + test-code: | + ctx->config.maximum_message_size = SIZE_MAX; + text: | + The maximum message size of the message queue configuration + shall be big enough so that a calculation to get the message buffer + storage area size overflows. + test-epilogue: null + test-prologue: null +- name: Queues + states: + - name: Avail + test-code: | + /* Nothing to do */ + text: | + There shall be at least one inactive message queue object available. + - name: None + test-code: | + memset( &config, 0, sizeof( config ) ); + config.name = rtems_build_name( 'M', 'S', 'G', 'Q' ); + config.maximum_pending_messages = MAX_PENDING_MESSAGES; + config.maximum_message_size = MAX_MESSAGE_SIZE; + config.storage_size = sizeof( exhaust_buffers[ 0 ] ); + config.attributes = RTEMS_DEFAULT_ATTRIBUTES; + + i = 0; + + while ( i < MAX_MESSAGE_QUEUES ) { + rtems_status_code sc; + rtems_id id; + + config.storage_area = exhaust_buffers[ i ]; + + sc = rtems_message_queue_construct( &config, &id ); + + if ( sc == RTEMS_SUCCESSFUL ) { + Objects_Control *obj; + const Objects_Information *info; + + info = _Objects_Get_information_id( id ); + T_quiet_assert_not_null( info ); + obj = _Objects_Get_no_protection( id, info ); + T_quiet_assert_not_null( obj ); + _Chain_Append_unprotected( &ctx->message_queues, &obj->Node ); + } else { + T_quiet_rsc( sc, RTEMS_TOO_MANY ); + break; + } + + ++i; + } + text: | + There shall be no inactive message queue object available. + test-epilogue: null + test-prologue: | + rtems_message_queue_config config; + size_t i; +- name: Area + states: + - name: Valid + test-code: | + ctx->config.storage_area = buffers; + text: | + The message buffer storage area begin pointer of the message queue + configuration shall be valid. + - name: 'Null' + test-code: | + ctx->config.storage_area = NULL; + text: | + The message buffer storage area begin pointer of the message queue + configuration shall be NULL. + test-epilogue: null + test-prologue: null +- name: AreaSize + states: + - name: Valid + test-code: | + ctx->config.storage_size = sizeof( buffers ); + text: | + The message buffer storage area size of the message queue configuration + shall be valid. + - name: Invalid + test-code: | + ctx->config.storage_size = SIZE_MAX; + text: | + The message buffer storage area size of the message queue configuration + shall be invalid. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->status = rtems_message_queue_construct( &ctx->config, ctx->id ); +test-brief: null +test-cleanup: | + Chain_Node *node; + + while ( ( node = _Chain_Get_unprotected( &ctx->message_queues ) ) ) { + Objects_Control *obj; + rtems_status_code sc; + + obj = (Objects_Control *) node; + sc = rtems_message_queue_delete( obj->id ); + T_quiet_rsc_success( sc ); + } +test-context: +- brief: null + description: null + member: rtems_status_code status +- brief: null + description: null + member: rtems_message_queue_config config +- brief: null + description: null + member: rtems_id *id +- brief: null + description: null + member: rtems_id id_value +- brief: null + description: null + member: Chain_Control message_queues +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +- rtems/score/chainimpl.h +- rtems/score/objectimpl.h +- string.h +test-local-includes: [] +test-prepare: | + ctx->id_value = 0xffffffff; + memset( &ctx->config, 0, sizeof( ctx->config ) ); +test-setup: + brief: null + code: | + _Chain_Initialize_empty( &ctx->message_queues ); + description: null +test-stop: null +test-support: | + #define MAX_MESSAGE_QUEUES 4 + + #define MAX_PENDING_MESSAGES 1 + + #define MAX_MESSAGE_SIZE 1 + + static RTEMS_MESSAGE_QUEUE_BUFFER( MAX_MESSAGE_SIZE ) + exhaust_buffers[ MAX_MESSAGE_QUEUES ][ MAX_PENDING_MESSAGES ]; + + static RTEMS_MESSAGE_QUEUE_BUFFER( MAX_MESSAGE_SIZE ) + buffers[ MAX_PENDING_MESSAGES ]; +test-target: testsuites/validation/tc-message-construct-errors.c +test-teardown: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: Ok + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Valid + MaxSize: + - Valid + Queues: + - Avail + Area: + - Valid + AreaSize: + - Valid +- enabled-by: true + post-conditions: + Status: InvAddress + pre-conditions: + Id: + - 'Null' + Name: all + MaxPending: all + MaxSize: all + Queues: all + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: InvName + pre-conditions: + Id: + - Id + Name: + - Invalid + MaxPending: all + MaxSize: all + Queues: all + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: InvNumber + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Zero + MaxSize: all + Queues: all + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: InvSize + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Valid + - Big + MaxSize: + - Zero + Queues: all + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: TooMany + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Valid + - Big + MaxSize: + - Valid + - Big + Queues: + - None + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: InvNumber + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Big + MaxSize: + - Valid + Queues: + - Avail + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: InvSize + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Valid + - Big + MaxSize: + - Big + Queues: + - Avail + Area: all + AreaSize: all +- enabled-by: true + post-conditions: + Status: Unsatisfied + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Valid + MaxSize: + - Valid + Queues: + - Avail + Area: + - 'Null' + AreaSize: all +- enabled-by: true + post-conditions: + Status: Unsatisfied + pre-conditions: + Id: + - Id + Name: + - Valid + MaxPending: + - Valid + MaxSize: + - Valid + Queues: + - Avail + Area: + - Valid + AreaSize: + - Invalid +type: requirement diff --git a/spec/score/msgq/if/buffer.yml b/spec/score/msgq/if/buffer.yml new file mode 100644 index 00000000..f644b08a --- /dev/null +++ b/spec/score/msgq/if/buffer.yml @@ -0,0 +1,11 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +interface-type: unspecified +links: +- role: interface-placement + uid: header2 +name: CORE_message_queue_Buffer +reference: null +type: interface diff --git a/spec/score/msgq/if/header.yml b/spec/score/msgq/if/header.yml new file mode 100644 index 00000000..7643d547 --- /dev/null +++ b/spec/score/msgq/if/header.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: This header file defines interfaces of the Message Queue Handler. +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +interface-type: header-file +links: +- role: interface-placement + uid: ../../if/domain +path: rtems/score/coremsg.h +prefix: cpukit/include +type: interface diff --git a/spec/score/msgq/if/header2.yml b/spec/score/msgq/if/header2.yml new file mode 100644 index 00000000..2ef9bc6a --- /dev/null +++ b/spec/score/msgq/if/header2.yml @@ -0,0 +1,12 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: This header file defines interfaces of the Message Queue Handler. +copyrights: +- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +interface-type: header-file +links: +- role: interface-placement + uid: ../../if/domain +path: rtems/score/coremsgbuffer.h +prefix: cpukit/include +type: interface -- cgit v1.2.3