spec: Add rtems_message_queue_construct()

7 files changed, 702 insertions, 0 deletions

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