diff options
Diffstat (limited to 'eng')
34 files changed, 4720 insertions, 535 deletions
diff --git a/eng/build-system.rst b/eng/build-system.rst index e76b606..11e8ba7 100644 --- a/eng/build-system.rst +++ b/eng/build-system.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2020 embedded brains GmbH & Co. KG .. _BSPBuildSystem: @@ -73,13 +73,13 @@ the following ``waf`` commands do. BSP List -------- -In the ``./waf bsp_list`` command, the BSP list is generated from the +In the ``./waf bsplist`` command, the BSP list is generated from the :ref:`SpecTypeBuildBSPItemType` items. BSP Defaults ------------ -In the ``./waf bsp_defaults`` command, the BSP defaults are generated from the +In the ``./waf bspdefaults`` command, the BSP defaults are generated from the :ref:`SpecTypeBuildBSPItemType` and :ref:`SpecTypeBuildOptionItemType` items. Build specification items contribute to the command through the ``do_defaults()`` method in the ``wscript``. @@ -294,7 +294,7 @@ shows the GCC-specific ABI flags item of the ``sparc/leon3`` BSP family: - env-append: null build-type: option copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG default: - -mcpu=leon3 default-by-variant: @@ -355,8 +355,8 @@ Add a Base BSP to a BSP Family items ``spec:/build/bsps/arch/family/bsprst``, ``spec:/build/bsps/arch/family/bspuvw``, and ``spec:/build/bsps/arch/family/bspxyz`` just define the name of the base - BSP and set a link to the group item. The base BSP names can be used for - example in the ``default-by-variant`` attribute of + BSP and set a link to the group item. The base BSP and BSP family names + can be used for example in the ``default-by-variant`` attribute of :ref:`SpecTypeBuildOptionItemType` items. The items linked by the BSP items are shown using relative UIDs. @@ -489,3 +489,32 @@ Add a link to the new library item using a relative UID: links: - role: build-dependency uid: libnew + +Add an Object +------------- + +Build objects logically separate relatively independent segments of +functionality (for example a device driver, an architecture-dependent feature, +etc.). Let *new* be the name of the new object. You can add the new object +with: + +.. code-block:: none + + $ vi spec/build/cpukit/objnew.yml + +Define the attributes of your new object according to +:ref:`SpecTypeBuildObjectsItemType`. + +Edit corresponding group item: + +.. code-block:: none + + $ vi spec/build/cpukit/grp.yml + +Add a link to the new objects item using a relative UID: + +.. code-block:: yaml + + links: + - role: build-dependency + uid: objnew diff --git a/eng/coding-conventions.rst b/eng/coding-conventions.rst index 668a917..b56d3c2 100644 --- a/eng/coding-conventions.rst +++ b/eng/coding-conventions.rst @@ -206,7 +206,7 @@ Portability Maintainability --------------- -* Minimize modifications to `third-party code <https://devel.rtems.org/wiki/Developer/Coding/ThirdPartyCode>`_.. +* Minimize modifications to `third-party code <https://devel.rtems.org/wiki/Developer/Coding/ThirdPartyCode>`_. * Keep it simple! Simple code is easier to debug and easier to read than clever code. * Share code with other architectures, CPUs, and BSPs where possible. * Do not duplicate standard OS or C Library routines. @@ -219,8 +219,6 @@ Performance * Understand the constraints of `real-time programming <https://devel.rtems.org/wiki/TBR/Review/Real-Time_Resources>`_.. Limit execution times in interrupt contexts and critical sections, such as Interrupt and Timer Service Routines (TSRs). -* Functions used only through function pointers should be declared - 'static inline' (RTEMS_INLINE_ROUTINE) * Prefer to ++preincrement instead of postincrement++. * Avoid using floating point except where absolutely necessary. diff --git a/eng/coding-doxygen.rst b/eng/coding-doxygen.rst index b2e6b61..efd543b 100644 --- a/eng/coding-doxygen.rst +++ b/eng/coding-doxygen.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019 embedded brains GmbH +.. Copyright (C) 2019 embedded brains GmbH & Co. KG .. _DoxygenGuidelines: diff --git a/eng/coding-file-hdr.rst b/eng/coding-file-hdr.rst index 3167670..4fc17fd 100644 --- a/eng/coding-file-hdr.rst +++ b/eng/coding-file-hdr.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2018, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2018, 2020 embedded brains GmbH & Co. KG .. Copyright (C) 2018, 2020 Sebastian Huber .. _FileTemplates: diff --git a/eng/doc-guide.rst b/eng/doc-guide.rst index cdcd04f..f0de23f 100644 --- a/eng/doc-guide.rst +++ b/eng/doc-guide.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2020 embedded brains GmbH & Co. KG .. _DocGuide: diff --git a/eng/fv/appendix-fv.rst b/eng/fv/appendix-fv.rst new file mode 100755 index 0000000..687679a --- /dev/null +++ b/eng/fv/appendix-fv.rst @@ -0,0 +1,1749 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +Appendix: RTEMS Formal Model Guide +********************************** + +This appendix covers the various formal models of RTEMS that are currently in +existence. It serves two purposes: +one is to provide detailed documentation of each model, +while the other is provide a guide into how to go about developing and deploying such models. + +The general approach followed here is to start by looking at the API documentation and identifying the key data-structures and function prototypes. +These are then modelled appropriately in Promela. +Then, general behavior patterns of interest are identified, +and the Promela model is extended to provide those patterns. +A key aspect here is exploiting the fact that Promela allows non-deterministic choices to be specified, which gives the effect of producing arbitrary orderings of model behavior. +All of this leads to a situation were the SPIN model-checker can effectively generate scenarios for all possible interleavings. +The final stage is mapping those scenarios to RTEMS C test code, +which has two parts: generating machine-readable output from SPIN, and developing the refinement mapping from that output to C test code. + +Some familiarity is assumed here with the Software Test Framework section in this document. + +The following models are included in the directory ``formal/promela/models/`` +at the top-level in ``rtems-central``: + +Chains API (``chains/``) + Models the unprotected chain append and get API calls in the Classic + Chains API Guide. This was an early model to develop the basic methodology. + +Events Manager (``events/``) + Models the behaviour of all the API calls in the Classic Events Manager API + Guide. This had to tackle real concurrency and deal with multiple CPUs and priority + issues. + +Barrier Manager (``barriers/``) + Models the behaviour of all the API calls in then Classic Barrier Manager API. + +Message Manager (``messages/``) + Models the create, send and receive API calls in the Classic Message Manager API. + +At the end of this guide is a section that discusses various issues that should be tackled in future work. + +Testing Chains +-------------- + +Documentation: Chains section in the RTEMS Classic API Guide. + +Model Directory: ``formal/promela/models/chains``. + +Model Name: ``chains-api-model``. + +The Chains API provides a doubly-linked list data-structure, optimised for fast +operations in an SMP setting. It was used as proof of concept exercise, +and focussed on just two API calls: ``rtems-chain-append-unprotected`` +and ``rtems-chain-get-unprotected`` (hereinafter just ``append`` and ``get``). + + +API Model +^^^^^^^^^ + +File: ``chains-api-model.pml`` + +While smart code optimization techniques are very important for RTEMS code, +the focus when constructing formal models is on functional correctness, +not performance. What is required is the simplest, most obviously correct model. + +The ``append`` operation adds new nodes on the end of the list, +while ``get`` removes and returns the node at the start of the list. +The Chains API has many other operations that can add/remove nodes at either end, or somewhere in the middle, but these are considered out of scope. + +Data Structures +~~~~~~~~~~~~~~~ + +There are no pointers in Promela, so we have to use arrays, +with array indices modelling pointers. +With just ``append`` and ``get``, an array can be used to implement a collection +of nodes in memory. +A ``Node`` type is defined that has next and previous indices, +plus an item payload. +Access to the node list is via a special control node with head and tail pointers. +In the model, an explicit size value is added to this control node, +to allow the writing of properties about chain length, +and to prevent array out-of-bound errors in the model itself. +We assume a single ``chain``, +with list node storage statically allocated in ``memory``. + +.. code:: c + + #define PTR_SIZE 3 + #define MEM_SIZE 8 + + typedef Node { + unsigned nxt : PTR_SIZE + ; unsigned prv : PTR_SIZE + ; byte itm + } + Node memory[MEM_SIZE] ; + + typedef Control { + unsigned head : PTR_SIZE; + unsigned tail : PTR_SIZE; + unsigned size : PTR_SIZE + } + Control chain ; + +While there are 8 memory elements, element 0 is inaccessible, +as the index 0 is treated like a ``NULL`` pointer. + +Function Calls +~~~~~~~~~~~~~~ + +The RTEMS prototype for ``append`` is: + +.. code:: c + + void rtems_chain_append_unprotected( + rtems_chain_control *the_chain, + rtems_chain_node *the_node + ); + +Its implementation starts by checking that the node to be appended is "off +chain", before performing the append. +The model is designed to satisfy this property so the check is not modelled. +Also, the Chains documentation is not clear about certain error cases. +As this is a proof of concept exercise, these details are not modelled. + +A Promela inline definition ``append`` models the desired behavior, +simulating C pointers with array addresses. Here ``ch`` is the chain argument, +while ``np`` is a node index. +The model starts by checking that the node pointer is not ``NULL``, +and that there is room in ``memory`` for another node. +These are to ensure that the model does not have any runtime errors. +Doing a standard model-check of this model finds no errors, +which indicates that those assertions are never false. + +.. code:: c + + inline append(ch,np) { + assert(np!=0); assert(ch.size < (MEM_SIZE-1)); + if + :: (ch.head == 0) -> ch.head = np; ch.tail = np; ch.size = 1; + memory[np].nxt = 0; memory[np].prv = 0; + :: (ch.head != 0) -> memory[ch.tail].nxt = np; memory[np].prv = ch.tail; + ch.tail = np; ch.size = ch.size + 1; + fi + } + +The RTEMS prototype for ``get`` is: + +.. code:: c + + rtems_chain_node *rtems_chain_get_unprotected( + rtems_chain_control *the_chain + ); + +It returns a pointer to the node, with ``NULL`` returned if the chain is empty. + +Promela inlines involve textual substitution, +so the concept of returning a value makes no sense. +For ``get``, the model is that of a statement that assigns the return value to +a variable. Both the function argument and return variable name are passed as parameters: + +.. code:: c + + /* np = get(ch); */ + inline get(ch,np) { + np = ch.head ; + if + :: (np != 0) -> + ch.head = memory[np].nxt; + ch.size = ch.size - 1; + // memory[np].nxt = 0 + :: (np == 0) -> skip + fi + if + :: (ch.head == 0) -> ch.tail = 0 + :: (ch.head != 0) -> skip + fi + } + +Behavior patterns +^^^^^^^^^^^^^^^^^ + +File: ``chains-api-model.pml`` + +A key feature of using a modelling language like Promela is that it has both +explicit and implicit non-determinism. This can be exploited so that SPIN will +find all possible interleavings of behavior. + +The Chains API model consists of six processes, three which perform ``append``, +and three that perform ``get``, waiting if the chain is empty. This model relies +on implicit non-determinism, in that the SPIN scheduler can choose and switch +between any unblocked process at any point. There is no explicit non-determinism +in this model. + +Promela process ``doAppend`` takes node index ``addr`` and a value ``val`` as +parameters. It puts ``val`` into the node indexed by ``addr``, +then calls ``append``, and terminates. +It is all made atomic to avoid unnecessary internal interleaving of operations because unprotected versions of API calls should only be used when interrupts +are disabled. + +.. code:: c + + proctype doAppend(int addr; int val) { + atomic{ memory[addr].itm = val; + append(chain,addr); } ; + } + +The ``doNonNullGet`` process waits for the chain to be non-empty before attempting to ``get`` an element. The first statement inside the atomic +construct is an expression, as a statements, that blocks while it evaluates to +zero. That only happens if ``head`` is in fact zero. The model also has an +assertion that checks that a non-null node is returned. + +.. code:: c + + proctype doNonNullGet() { + atomic{ + chain.head != 0; + get(chain,nptr); + assert(nptr != 0); + } ; + } + +All processes terminate after they have performed their (sole) action. + +The top-level of a Promela model is an initial process declared by the ``init`` construct. This initializes the chain as empty and then runs all six processes concurrently. It then uses the special ``_nr_pr`` variable to wait for all six +processes to terminate. A final assertion checks that the chain is empty. + +.. code:: c + + init { + pid nr; + chain.head = 0; chain.tail = 0; chain.size = 0 ; + nr = _nr_pr; // assignment, sets `nr` to current number of procs + run doAppend(6,21); + run doAppend(3,22); + run doAppend(4,23); + run doNonNullGet(); + run doNonNullGet(); + run doNonNullGet(); + nr == _nr_pr; // expression, waits until number of procs equals `nr` + assert (chain.size == 0); + } + +Simulation of this model will show some execution sequence in which the appends +happen in a random order, and the gets also occur in a random order, whenever +the chain is not empty. All assertions are always satisfied, including the last +one above. Model checking this model explores all possible interleavings and reports no errors of any kind. In particular, when the model reaches the last +assert statement, the chain size is always zero. + +SPIN uses the C pre-processor, and generates the model as a C program. This +model has a simple flow of control: basically execute each process once in an +almost arbitrary order, assert that the chain is empty, and terminate. Test +generation here just requires the negation of the final assertion to get all +possible interleavings. The special C pre-processor definition ``TEST_GEN`` is +used to switch between the two uses of the model. The last line above is +replaced by: + +.. code:: c + + #ifdef TEST_GEN + assert (chain.size != 0); + #else + assert (chain.size == 0); + #endif + +A test generation run can then be invoked by passing in ``-DTEST_GEN`` as a +command-line argument. + +Annotations +^^^^^^^^^^^ + +File: ``chains-api-model.pml`` + +The model needs to have ``printf`` statements added to generation the +annotations used to perform the test generation. + +This model wraps each of six API calls in its own process, so that model +checking can generate all feasible interleavings. However, the plan for the test code is that it will be just one RTEMS Task, that executes all the API +calls in the order determined by the scenario under consideration. All the +annotations in this model specify ``0`` as the Promela process identifier. + +Data Structures +~~~~~~~~~~~~~~~ + +Annotations have to be provided for any variable or datastructure declarations +that will need to have corresponding code in the test program. +These have to be printed out as the model starts to run. +For this model, the ``MAX_SIZE`` parameter is important, +as are the variables ``memory``, ``nptr``, and ``chain``: + +.. code:: c + + printf("@@@ 0 NAME Chain_AutoGen\n") + printf("@@@ 0 DEF MAX_SIZE 8\n"); + printf("@@@ 0 DCLARRAY Node memory MAX_SIZE\n"); + printf("@@@ 0 DECL unsigned nptr NULL\n") + printf("@@@ 0 DECL Control chain\n"); + +At this point, a parameter-free initialization annotation is issued. This should +be refined to C code that initializes the above variables. + +.. code:: c + + printf("@@@INIT\n"); + +Function Calls +~~~~~~~~~~~~~~ + +For ``append``, two forms of annotation are produced. One uses the ``CALL`` +format to report the function being called along with its arguments. The other +form reports the resulting contents of the chain. + +.. code:: c + + proctype doAppend(int addr; int val) { + atomic{ memory[addr].itm = val; append(chain,addr); + printf("@@@ 0 CALL append %d %d\n",val,addr); + show_chain(); + } ; + } + +The statement ``show_chain()`` is an inline function that prints the +contents of the chain after append returns. +The resulting output is multi-line, +starting with ``@@@ 0 SEQ chain``, +ending with ``@@@ 0 END chain``, +and with entries in between of the form ``@@@ 0 SCALAR _ val`` +displaying chain elements, line by line. + +Something similar is done for ``get``, with the addition of a third annotation +``show_node()`` that shows the node that was got: + +.. code:: c + + proctype doNonNullGet() { + atomic{ + chain.head != 0; + get(chain,nptr); + printf("@@@ 0 CALL getNonNull %d\n",nptr); + show_chain(); + assert(nptr != 0); + show_node(); + } ; + } + +The statement ``show_node()`` is defined as follows: + +.. code:: c + + inline show_node (){ + atomic{ + printf("@@@ 0 PTR nptr %d\n",nptr); + if + :: nptr -> printf("@@@ 0 STRUCT nptr\n"); + printf("@@@ 0 SCALAR itm %d\n", memory[nptr].itm); + printf("@@@ 0 END nptr\n") + :: else -> skip + fi + } + } + +It prints out the value of ``nptr``, which is an array index. If it is not zero, +it prints out some details of the indexed node structure. + +Annotations are also added to the ``init`` process to show the chain and node. + +.. code:: c + + chain.head = 0; chain.tail = 0; chain.size = 0; + show_chain(); + show_node(); + +Refinement +^^^^^^^^^^ + +Files: + + ``chains-api-model-rfn.yml`` + + ``chains-api-model-pre.h`` + + ``tr-chains-api-model.c`` + +Model annotations are converted to C test code using a YAML file that maps +single names to test code snippets into which parameters can be substituted. +Parameters are numbered from zero, and the ``n`` th parameter will be substituted +wherever ``{n}`` occurs in the snippet. + +Refinement is more than just the above mapping from annotations to code. Some of +this code will refer to C variables, structures, and functions that are needed +to support the test. Some of these are declared ``chains-api-model-pre.h`` and implemented in ``tr-chains-api-model.c``. + +Data Structures +~~~~~~~~~~~~~~~ + +The initialization generates one each of ``NAME``, ``DEF``, ``DCLARRAY``, and +``INIT`` annotations, and two ``DECL`` annotations. + +The ``DEF`` entry is currently not looked up as it is automatically converted to a ``#define``. + +The ``NAME`` annotation is used to declare the test case name, which is +stored in the global variable ``rtems_test_name``. The current +refinement entry is: + +.. code:: python + + NAME: | + const char rtems_test_name[] = "Model_Chain_API"; + +In this case, the name is fixed and ignores what is declared in the model. + +The ``DCLARRAY Node memory MAX_SIZE`` annotation looks up ``memory_DCL`` in the +refinement file, passing in ``memory`` and ``MAX_SIZE`` as arguments. The entry in the refinement file is: + +.. code:: python + + memory_DCL: item {0}[{1}]; + +Here ``item`` is the type of the chains nodes used in the test code. It is +declared in ``chains-api-model.pre.h`` as: + +.. code:: c + + typedef struct item + { + rtems_chain_node node; + int val; + } item; + +Substituting the arguments gives: + +.. code:: c + + item memory[MAX_SIZE]; + +The two ``DECL`` annotations have two or three parameters. The first is the +type, the second is the variable name, and the optional third is an initial +value. The lookup key is the variable name with ``_DCL`` added on. +In the refinement file, the entry only provides the C type, and the other parts of the declaration are added in. +The entries are: + +.. code:: python + + nptr_DCL: item * + chain_DCL: rtems_chain_control + +Annotation ``DECL unsigned nptr NULL`` results in: + +.. code:: c + + item * nptr = NULL ; + +Annotation ``DECL Control chain`` results in: + +.. code:: c + + rtems_chain_control chain ; + +The ``INIT`` annotation is looked up as ``INIT`` itself. It should be mapped to +code that does all necessary initialization. The refinement entry for chains is: + +.. code:: python + + INIT: rtems_chain_initialize_empty( &chain ); + +In addition to all the above dealing with declarations and initialization, +there are the annotations, already described above, that are used to display +composite values, such as structure contents, and chain contents. + +In the model, all accesses to individual chain nodes are via index ``nptr``, +which occurs in two types of annotations, ``PTR`` and ``STRUCT``. The ``PTR`` +annotation is refined by looking up ``nptr_PTR`` with the value of ``nptr`` as the sole argument. The refinement entry is: + +.. code:: python + + nptr_PTR: | + T_eq_ptr( nptr, NULL ); + T_eq_ptr( nptr, &memory[{0}] ); + +The first line is used if the value of ``nptr`` is zero, otherwise the second +line is used. + +The use of ``STRUCT`` requires three annotation lines in a row, *e.g.*: + +.. code:: c + + @@@ 0 STRUCT nptr + @@@ 0 SCALAR itm 21 + @@@ 0 END nptr + +The ``STRUCT`` and ``END`` annotations do not generate any code, but open and +close a scope in which ``nptr`` is noted as the "name" of the struct. The +``SCALAR`` annotation is used to observe simple values such as numbers or booleans. However, within a ``STRUCT`` it belongs to a C ``struct``, so the +relevant field needs to be used to access the value. +Within this scope, the scalar variable ``itm`` is looked up as a field name, +by searching for ``itm_FSCALAR`` with arguments``nptr`` and ``21``, which returns the entry: + +.. code:: python + + itm_FSCALAR: T_eq_int( {0}->val, {1} ); + +This gets turned into the following test: + +.. code:: c + + T_eq_int( nptr->val, 21 ); + +A similar idea is used to test the contents of a chain. The annotations produced +start with a ``SEQ`` annotation, followed by a ``SCALAR`` annotation for each +item in the chain, and then ending with an ``END`` annotation. Again, there is +a scope defined where the ``SEQ`` argument is the "name" of the sequence. +The ``SCALAR`` entries have no name here (indicated by ``_``), and their values +are accumulated in a string, separated by spaces. Test code generation is +triggered this time by the ``END`` annotation, that looks up the "name" with ``_SEQ`` appended, and the accumulated string as an argument. The corresponding entry for chain sequences is: + +.. code:: python + + chain_SEQ: | + show_chain( &chain, ctx->buffer ); + T_eq_str( ctx->buffer, "{0} 0" ); + +So, the following chain annotation sequence: + +.. code:: c + + @@@ 0 SEQ chain + @@@ 0 SCALAR _ 21 + @@@ 0 SCALAR _ 22 + @@@ 0 END chain + +becomes the following C code: + +.. code:: C + + show_chain( &chain, ctx->buffer ); + T_eq_str( ctx->buffer, " 21 22 0" ); + +C function ``show_chain()`` is defined in ``tr-chains-api-model.c`` and +generates a string with exactly the same format as that produced above. These +are then compared for equality. + +.. note:: + + The Promela/SPIN model checker's prime focus is modelling and verifying + concurrency related properties. It is not intended for verifying sequential + code or data transformations. This is why some of the ``STRUCT``/``SEQ`` + material here is so clumsy. It plays virtually no role in the other models. + +Function Calls +~~~~~~~~~~~~~~ + +For ``@@@ 0 CALL append 22 3`` lookup ``append`` to get + +.. code-block:: c + + memory[{1}].val = {0}; + rtems_chain_append_unprotected( &chain, (rtems_chain_node*)&memory[{1}] ); + +Substitute ``22`` and ``3`` in to produce + +.. code-block:: c + + memory[3].val = 22; + rtems_chain_append_unprotected( &chain, (rtems_chain_node*)&memory[3] ); + +For ``@@@ 0 CALL getNonNull 3`` lookup ``getNonNull`` to obtain + +.. code:: c + + nptr = get_item( &chain ); + T_eq_ptr( nptr, &memory[{0}] ); + +Function ``get_item()`` is defined in ``tc-chains-api-model.c`` and calls ``rtems_chain_get_unprotected()``. Substitute ``3`` to produce: + +.. code:: c + + nptr = get_item( &chain ); + T_eq_ptr( nptr, &memory[3] ); + +Testing Concurrent Managers +--------------------------- + +All the other models are of Managers that provide some form of communication +between multiple RTEMS Tasks. This introduces a number of issues regarding +the timing and control of tasks, particularly when developing *reproducible* +tests, where the sequencing of behavior is the same every time the test runs. +The tests are generated by following the schemes already in use for regular +RTEMS handwritten tests. +In particular the pre-existing tests for Send and Receive in the Event Manager +where used as a guide. + +Testing Strategy +^^^^^^^^^^^^^^^^ + +The tests are organized as follows: + +1. A designated Task, the Runner, is responsible for initializing, + coordinating and tearing down a test run. + Coordination involves starting other Worker Tasks that perform tests, + and waiting for them to complete. + It may also run some tests itself. + +1. One or more Worker Tasks are used to perform test actions. + +1. Each RTEMS Task (Runner/Worker) is modelled by one Promela process. + +1. Simple Binary Semaphores + are used to coordinate all the tasks to ensure + that the interleaving is always the same + (See Semaphore Manager section in Classic API Manual). + +1. Two other Promela processes are required: + One, called ``Clock()`` is used to model timing and timeouts; + The other, called ``System()`` models relevant behavior of the RTEMS scheduler. + +Model Structure +^^^^^^^^^^^^^^^ + +All the models developed so far are based on this framework. +The structure of these models takes the following form: + + Constant Declarations + Mainly ``#define``\ s that define important constants. + + Datastructure Definitions + Promela ``typedef``\ s that describe key forms of data. + In particular there is a type ``Task`` that models RTEMS Tasks. + The Simple Binary Semaphores are modelled as boolean variables. + + Global Variable Declarations + Typically these are arrays of data-structures, + representing objects such as tasks or semaphores. + + Supporting Models + These are ``inline`` definitions that capture common behavior. + In all models this includes ``Obtain()`` and ``Release()`` to model semaphores, + and ``waitUntilReady()`` that models a blocked task waiting to be unblocked. + Included here are other definitions specific to the particular Manager being + modelled. + + API Models + These are ``inline`` definitions that model the behavior of each API call. + All behavior must be modelled, including bad calls that (should) result in + an error code being returned. + The parameter lists used in the Promela models will differ from those + of the actual API calls. + Consider a hypothetical RTEMS API call: + + .. code:: c + + rc = rtems_some_api(arg1,arg2,...,argN); + + One reason, common to all calls, is that the ``inline`` construct has + no concept of returning a value, + so a variable parameter has to be added to represent it, + and it has to be ensured the appropriate return code is assigned to it. + + .. code:: promela + + inline some_api(arg1,arg2,...,argN,rc) { + ... + rc = RC_some_code + } + + Another reason is that some RTEMS types encode a number of different + concepts in a single machine word. + The most notable of these is the ``rtems_options`` type, + that specifies various options, usually for calls that may block. + In some models, some options are modelled individually, for clarity. + So the API model may have two or more parameters where the RTEMS call has one. + + .. code:: promela + + inline some_api(arg1,arg2feat1,arg2feat2,...,argN,rc) { + ... + rc = RC_some_code + } + + The refinement of this will pass the multiple feature arguments to + a C function that will assemble the single RTEMS argument. + + A third reason is that sometimes it is important to also provide + the process id of the *calling* task. This can be important where + priority and preemption are involved. + + Scenario Generation + A Testsuite that exercises *all* the API code is highly desirable. + This requires running tests that explore a wide range of scenarios, + normally devised by hand when writing a testsuite. + With Promela/SPIN, the model-checker can generate all of these simplify + as a result of its exhaustive search of the model. + In practice, scenarios fall into a number of high-level categories, + so the first step is make a random choice of such a category. + Within a category there may be further choices to be done. + A collection of global scenario variables are used to records the choices made. + This is all managed by inline ``chooseScenario()``. + + RTEMS Test Task Modelling + This is a series of Promela ``proctype``\ s, one for the Runner Task, + and one for each of the Worker Tasks. + Their behavior is controlled by the global scenario variables. + + System Modelling + These are Promela processes that model relevant underlying RTEMS behavior, + such as the scheduler (``System()``) and timers (``Clock()``). + + Model Main Process + Called ``init``, this initialises variables, invokes ``chooseScenario()``, + runs all the processes, waits for them to terminate, + and then terminates itself. + +The Promela models developed so far for these Managers always terminate. +The last few lines of each are of the form: + +.. code:: promela + + #ifdef TEST_GEN + assert(false); + #endif + +If these models are run in the usual way (simulation or verification), +then a correct verified model is observed. +If ``-DTEST_GEN`` is provided as the first command-line argument, +in verification mode configured to find *all* counterexamples, +then all the possible (correct) behaviours of the system will be generated. + +Transforming Model Behavior to C Code +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +As described earlier, ``printf`` statements are used +to produce easy to parse output that makes +model events and outcomes easy to identify and process. +The YAML file used to define the refinement from model to code +provides a way of looking up an observation with arguments, +and then obtaining a C template that can be populated with those arguments. + +This refinement is a bridge between two distinct worlds: + + Model World: + where the key focus is on correctness and clarity. + + Code World: + where clarity is often sacrificed for efficiency. + +This means that the model-to-code relationship +need not be a simple one-to-one mapping. +This has already been alluded to above when the need for extra parameters +in API call models was discussed. +It can also be helpful when the model is better treating various attributes +separately, while the code handles those attributes packed into machine words. + +It is always reasonable to add test support code to the C test sources, +and this can include C functions that map distinct attribute values +down into some compact merged representation. + + +Testing the Event Manager +------------------------- + +Documentation: Event Manager section in the RTEMS Classic API Guide. + +Model Directory: ``formal/promela/models/events``. + +Model Name: ``event-mgr-model``. + +The Event Manager allows tasks to send events to, +and receive events from, other tasks. +From the perspective of the Event Manager, +events are just uninterpreted numbers in the range 0..31, +encoded as a 32-bit bitset. + +``rtems_event_send(id,event_in)`` + allows a task to send a bitset to a designated task + +``rtems_event_receive(event_in,option_set,ticks,event_out)`` + allows a task to specify a desired bitset + with options on what to do if it is not present. + +Most of the requirements are pretty straightforward, +but two were a little more complex, +and drove the more complex parts of the modelling. + +1. If a task was blocked waiting to receive events, + and a lower priority task then sent the events that would wake that + blocked task, + then the sending task would be immediately preempted by the receiver task. + +2. There was a requirement that explicitly discussed the situation + where the two tasks involved were running on different processors. + +A preliminary incomplete model of the Event Manager was originally developed +by the consortium early in the project. The model was then completed during +the rest of the activity by a Masters student: :cite:`Jennings:2021:FV`. +They also developed the first iteration of the ``testbuilder`` program. + +API Model +^^^^^^^^^ + +File: ``event-mgr-model.pml`` + +The RTEMS Event set contains 32 values, but in the model limits this to +just four, which is enough for test purposes. +Some inline definitions are provided to encode (``events``), display +(``printevents``), and subtract (``setminus``) events. + +The ``rtems_option_set`` is simplifiedto just two relevant bits: the timeout +setting (``Wait``, ``NoWait``), and how much of the desired event set will +satisfy the receiver (``All``, ``Any``). +These are passed in as two separate arguments to the model of the receive call. + +Event Send +~~~~~~~~~~ + +An RTEMS call ``rc = rtems_event_send(tid,evts)`` is modelled by an inline of +the form: + +.. code-block:: c + + event_send(self,tid,evts,rc) + +The four arguments are: + | ``self`` : id of process modelling the task/IDR making call. + | ``tid`` : id of process modelling the target task of the call. + | ``evts`` : event set being sent. + | ``rc`` : updated with the return code when the send completes. + +The main complication in the otherwise straightforward model is the requirement +to preempt under certain circumstances. + +.. code-block:: c + + inline event_send(self,tid,evts,rc) { + atomic{ + if + :: tid >= BAD_ID -> rc = RC_InvId + :: tid < BAD_ID -> + tasks[tid].pending = tasks[tid].pending | evts + // at this point, have we woken the target task? + unsigned got : NO_OF_EVENTS; + bool sat; + satisfied(tasks[tid],got,sat); + if + :: sat -> + tasks[tid].state = Ready; + printf("@@@ %d STATE %d Ready\n",_pid,tid) + preemptIfRequired(self,tid) ; + // tasks[self].state may now be OtherWait ! + waitUntilReady(self); + :: else -> skip + fi + rc = RC_OK; + fi + } + } + +Three inline abstractions are used: + +``satisfied(task,out,sat)`` + updates ``out`` with the wanted events received so far, and then checks if a receive has been satisfied. It + updates its ``sat`` argument to reflect the check outcome. + +``preemptIfRequired(self,tid)`` + forces the sending process to enter the ``OtherWait``, + if circumstances require it. + +``waitUntilReady(self)`` + basically waits for the process state to become ``Ready``. + +Event Receive +~~~~~~~~~~~~~ + +An RTEMS call ``rc = rtems_event_receive(evts,opts,interval,out)`` is modelled +by an inline of +the form: + +.. code-block:: c + + event_receive(self,evts,wait,wantall,interval,out,rc) + +The seven arguments are: + | ``self`` : id of process modelling the task making call + | ``evts`` : input event set + | ``wait`` : true if receive should wait + | ``what`` : all, or some? + | ``interval`` : wait interval (0 waits forever) + | ``out`` : pointer to location for satisfying events when the receive + completes. + | ``rc`` : updated with the return code when the receive completes. + + +There is a small complication, in that there are distinct variables in the model +for receiver options that are combined into a single RTEMS option set. The +actual calling sequence in C test code will be: + +.. code-block:: c + + opts = mergeopts(wait,wantall); + rc = rtems_event_receive(evts,opts,interval,out); + +Here ``mergeopts`` is a C function defined in the C Preamble. + +.. code-block:: c + + inline event_receive(self,evts,wait,wantall,interval,out,rc){ + atomic{ + printf("@@@ %d LOG pending[%d] = ",_pid,self); + printevents(tasks[self].pending); nl(); + tasks[self].wanted = evts; + tasks[self].all = wantall + if + :: out == 0 -> + printf("@@@ %d LOG Receive NULL out.\n",_pid); + rc = RC_InvAddr ; + :: evts == EVTS_PENDING -> + printf("@@@ %d LOG Receive Pending.\n",_pid); + recout[out] = tasks[self].pending; + rc = RC_OK + :: else -> + bool sat; + retry: satisfied(tasks[self],recout[out],sat); + if + :: sat -> + printf("@@@ %d LOG Receive Satisfied!\n",_pid); + setminus(tasks[self].pending,tasks[self].pending,recout[out]); + printf("@@@ %d LOG pending'[%d] = ",_pid,self); + printevents(tasks[self].pending); nl(); + rc = RC_OK; + :: !sat && !wait -> + printf("@@@ %d LOG Receive Not Satisfied (no wait)\n",_pid); + rc = RC_Unsat; + :: !sat && wait && interval > 0 -> + printf("@@@ %d LOG Receive Not Satisfied (timeout %d)\n",_pid,interval); + tasks[self].ticks = interval; + tasks[self].tout = false; + tasks[self].state = TimeWait; + printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval) + waitUntilReady(self); + if + :: tasks[self].tout -> rc = RC_Timeout + :: else -> goto retry + fi + :: else -> // !sat && wait && interval <= 0 + printf("@@@ %d LOG Receive Not Satisfied (wait).\n",_pid); + tasks[self].state = EventWait; + printf("@@@ %d STATE %d EventWait\n",_pid,self) + if + :: sendTwice && !sentFirst -> Released(sendSema); + :: else + fi + waitUntilReady(self); + goto retry + fi + fi + printf("@@@ %d LOG pending'[%d] = ",_pid,self); + printevents(tasks[self].pending); nl(); + } + } + +Here ``satisfied()`` and ``waitUntilReady()`` are also used. + +Behaviour Patterns +^^^^^^^^^^^^^^^^^^ + +File: ``event-mgr-model.pml`` + +The Event Manager model consists of +five Promela processes: + +``init`` + The first top-level Promela process that performs initialisation, + starts the other processes, waits for them to terminate, and finishes. + +``System`` + A Promela process that models the behaviour of the operating system, + in particular that of the scheduler. + +``Clock`` + A Promela process used to facilitate modelling timeouts. + +``Receiver`` + The Promela process modelling the test Runner, + that also invokes the receive API call. + +``Sender`` + A Promela process modelling a singe test Worker + that invokes the send API call. + + +Two simple binary semaphores are used to synchronise the tasks. + +The Task model only looks at an abstracted version of RTEMS Task states: + +``Zombie`` + used to model a task that has just terminated. It can only be deleted. + +``Ready`` + same as the RTEMS notion of ``Ready``. + +``EventWait`` + is ``Blocked`` inside a call of ``event_receive()`` with no timeout. + +``TimeWait`` + is ``Blocked`` inside a call of ``event_receive()`` with a timeout. + +``OtherWait`` + is ``Blocked`` for some other reason, which arises in this model when a + sender gets pre-empted by a higher priority receiver it has just satisfied. + + +Tasks are represented using a datastructure array. +As array indices are proxies here for C pointers, +the zeroth array entry is always unused, +as index value 0 is used to model a NULL C pointer. + +.. code-block:: c + + typedef Task { + byte nodeid; // So we can spot remote calls + byte pmlid; // Promela process id + mtype state ; // {Ready,EventWait,TickWait,OtherWait} + bool preemptable ; + byte prio ; // lower number is higher priority + int ticks; // + bool tout; // true if woken by a timeout + unsigned wanted : NO_OF_EVENTS ; // EvtSet, those expected by receiver + unsigned pending : NO_OF_EVENTS ; // EvtSet, those already received + bool all; // Do we want All? + }; + Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference + +.. code-block:: c + + byte sendrc; // Sender global variable + byte recrc; // Receiver global variable + byte recout[TASK_MAX] ; // models receive 'out' location. + +Task Scheduling +~~~~~~~~~~~~~~~ + +In order to produce a model that captures real RTEMS Task behaviour, +there need to be mechanisms that mimic the behaviour of the scheduler and other +activities that can modify the execution state of these Tasks. Given a scenario +generated by such a model, synchronisation needs to be added to the generated C +code to ensure test has the same execution patterns. + +Relevant scheduling behavior is modelled by two inlines that have already +been mentioned: ``waitUntilReady()`` and ``preemptIfRequired()``. + +For synchronisation, simple boolean semaphores are used, where True means +available, and False means the semaphore has been acquired. + +.. code-block:: c + + bool semaphore[SEMA_MAX]; // Semaphore + +The synchronisation mechanisms are: + + +``Obtain(sem_id)`` + call that waits to obtain semaphore ``sem_id``. + +``Release(sem_id)`` + call that releases semaphore ``sem_id`` + +``Released(sem_id)`` + simulates ecosystem behaviour that releases ``sem_id``. + +The difference between ``Release`` and ``Released`` is that the first issues +a ``SIGNAL`` annotation, while the second does not. + + +Scenarios +~~~~~~~~~ + +A number of different scenario schemes were defined +that cover various aspects of +Event Manager behaviour. Some schemes involve only one task, and are usually +used to test error-handling or abnormal situations. Other schemes involve two +tasks, with some mixture of event sending and receiving, with varying task +priorities. + +For example, an event send operation can involve a target identifier that +is invalid (``BAD_ID``), correctly identifies a receiver task (``RCV_ID``), or +is sending events to itself (``SEND_ID``). + +.. code-block:: c + + typedef SendInputs { + byte target_id ; + unsigned send_evts : NO_OF_EVENTS ; + } ; + SendInputs send_in[MAX_STEPS]; + +An event receive operation will be determined by values for desired events, +and the relevant to bits of the option-set parameter. + +.. code-block:: c + + typedef ReceiveInputs { + unsigned receive_evts : NO_OF_EVENTS ; + bool will_wait; + bool everything; + byte wait_length; + }; + ReceiveInputs receive_in[MAX_STEPS]; + +There is a range of global variables that define scenarios for both send and +receive. This defines a two-step process for choosing a scenario. +The first step is to select a scenario scheme. The possible schemes are +defined by the following ``mtype``: + +.. code-block:: c + + mtype = {Send,Receive,SndRcv,RcvSnd,SndRcvSnd,SndPre,MultiCore}; + mtype scenario; + +One of these is chosen by using a conditional where all alternatives are +executable, so behaving as a non-deterministic choice of one of them. + +.. code-block:: c + + if + :: scenario = Send; + :: scenario = Receive; + :: scenario = SndRcv; + :: scenario = SndPre; + :: scenario = SndRcvSnd; + :: scenario = MultiCore; + fi + + +Once the value of ``scenario`` is chosen, it is used in another conditional +to select a non-deterministic choice of the finer details of that scenario. + +.. code-block:: c + + if + :: scenario == Send -> + doReceive = false; + sendTarget = BAD_ID; + :: scenario == Receive -> + doSend = false + if + :: rcvWait = false + :: rcvWait = true; rcvInterval = 4 + :: rcvOut = 0; + fi + printf( "@@@ %d LOG sub-senario wait:%d interval:%d, out:%d\n", + _pid, rcvWait, rcvInterval, rcvOut ) + :: scenario == SndRcv -> + if + :: sendEvents = 14; // {1,1,1,0} + :: sendEvents = 11; // {1,0,1,1} + fi + printf( "@@@ %d LOG sub-senario send-receive events:%d\n", + _pid, sendEvents ) + :: scenario == SndPre -> + sendPrio = 3; + sendPreempt = true; + startSema = rcvSema; + printf( "@@@ %d LOG sub-senario send-preemptable events:%d\n", + _pid, sendEvents ) + :: scenario == SndRcvSnd -> + sendEvents1 = 2; // {0,0,1,0} + sendEvents2 = 8; // {1,0,0,0} + sendEvents = sendEvents1; + sendTwice = true; + printf( "@@@ %d LOG sub-senario send-receive-send events:%d\n", + _pid, sendEvents ) + :: scenario == MultiCore -> + multicore = true; + sendCore = 1; + printf( "@@@ %d LOG sub-senario multicore send-receive events:%d\n", + _pid, sendEvents ) + :: else // go with defaults + fi + +Ddefault values are defined for all the global scenario variables so that the +above code focusses on what differs. The default scenario is a receiver waiting +for a sender of the same priority which sends exactly what was requested. + +Sender Process (Worker Task) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The sender process then uses the scenario configuration to determine its +behaviour. A key feature is the way it acquires its semaphore before doing a +send, and releases the receiver semaphore when it has just finished sending. +Both these semaphores are initialised in the unavailable state. + +.. code-block:: c + + proctype Sender (byte nid, taskid) { + + tasks[taskid].nodeid = nid; + tasks[taskid].pmlid = _pid; + tasks[taskid].prio = sendPrio; + tasks[taskid].preemptable = sendPreempt; + tasks[taskid].state = Ready; + printf("@@@ %d TASK Worker\n",_pid); + if + :: multicore -> + // printf("@@@ %d CALL OtherScheduler %d\n", _pid, sendCore); + printf("@@@ %d CALL SetProcessor %d\n", _pid, sendCore); + :: else + fi + if + :: sendPrio > rcvPrio -> printf("@@@ %d CALL LowerPriority\n", _pid); + :: sendPrio == rcvPrio -> printf("@@@ %d CALL EqualPriority\n", _pid); + :: sendPrio < rcvPrio -> printf("@@@ %d CALL HigherPriority\n", _pid); + :: else + fi + repeat: + Obtain(sendSema); + if + :: doSend -> + if + :: !sentFirst -> printf("@@@ %d CALL StartLog\n",_pid); + :: else + fi + printf("@@@ %d CALL event_send %d %d %d sendrc\n",_pid,taskid,sendTarget,sendEvents); + if + :: sendPreempt && !sentFirst -> printf("@@@ %d CALL CheckPreemption\n",_pid); + :: !sendPreempt && !sentFirst -> printf("@@@ %d CALL CheckNoPreemption\n",_pid); + :: else + fi + event_send(taskid,sendTarget,sendEvents,sendrc); + printf("@@@ %d SCALAR sendrc %d\n",_pid,sendrc); + :: else + fi + Release(rcvSema); + if + :: sendTwice && !sentFirst -> + sentFirst = true; + sendEvents = sendEvents2; + goto repeat; + :: else + fi + printf("@@@ %d LOG Sender %d finished\n",_pid,taskid); + tasks[taskid].state = Zombie; + printf("@@@ %d STATE %d Zombie\n",_pid,taskid) + } + +Receiver Process (Runner Task) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The receiver process uses the scenario configuration to determine its +behaviour. It has the responsibility to trigger the start semaphore to allow +either itself or the sender to start. The start semaphore corresponds to either +the send or receive semaphore, depending on the scenario. The receiver acquires +the receive semaphore before proceeding, and releases the send sempahore when +done. + +.. code-block:: c + + proctype Receiver (byte nid, taskid) { + + tasks[taskid].nodeid = nid; + tasks[taskid].pmlid = _pid; + tasks[taskid].prio = rcvPrio; + tasks[taskid].preemptable = false; + tasks[taskid].state = Ready; + printf("@@@ %d TASK Runner\n",_pid,taskid); + if + :: multicore -> + printf("@@@ %d CALL SetProcessor %d\n", _pid, rcvCore); + :: else + fi + Release(startSema); // make sure stuff starts */ + /* printf("@@@ %d LOG Receiver Task %d running on Node %d\n",_pid,taskid,nid); */ + Obtain(rcvSema); + + // If the receiver is higher priority then it will be running + // The sender is either blocked waiting for its semaphore + // or because it is lower priority. + // A high priority receiver needs to release the sender now, before it + // gets blocked on its own event receive. + if + :: rcvPrio < sendPrio -> Release(sendSema); // Release send semaphore for preemption + :: else + fi + if + :: doReceive -> + printf("@@@ %d SCALAR pending %d %d\n",_pid,taskid,tasks[taskid].pending); + if + :: sendTwice && !sentFirst -> Release(sendSema) + :: else + fi + printf("@@@ %d CALL event_receive %d %d %d %d %d recrc\n", + _pid,rcvEvents,rcvWait,rcvAll,rcvInterval,rcvOut); + /* (self, evts, when, what, ticks, out, rc) */ + event_receive(taskid,rcvEvents,rcvWait,rcvAll,rcvInterval,rcvOut,recrc); + printf("@@@ %d SCALAR recrc %d\n",_pid,recrc); + if + :: rcvOut > 0 -> + printf("@@@ %d SCALAR recout %d %d\n",_pid,rcvOut,recout[rcvOut]); + :: else + fi + printf("@@@ %d SCALAR pending %d %d\n",_pid,taskid,tasks[taskid].pending); + :: else + fi + Release(sendSema); + printf("@@@ %d LOG Receiver %d finished\n",_pid,taskid); + tasks[taskid].state = Zombie; + printf("@@@ %d STATE %d Zombie\n",_pid,taskid) + } + +System Process +~~~~~~~~~~~~~~ + + A process is needed that periodically wakes up blocked processes. + This is modelling background behaviour of the system, + such as ISRs and scheduling. + All tasks are visited in round-robin order (to prevent starvation) + and are made ready if waiting on other things. Tasks waiting for events or timeouts are not touched. This terminates when all tasks are zombies. + +.. code-block:: c + + proctype System () { + byte taskid ; + bool liveSeen; + printf("@@@ %d LOG System running...\n",_pid); + loop: + taskid = 1; + liveSeen = false; + printf("@@@ %d LOG Loop through tasks...\n",_pid); + atomic { + printf("@@@ %d LOG Scenario is ",_pid); + printm(scenario); nl(); + } + do // while taskid < TASK_MAX .... + :: taskid == TASK_MAX -> break; + :: else -> + atomic { + printf("@@@ %d LOG Task %d state is ",_pid,taskid); + printm(tasks[taskid].state); nl() + } + if + :: tasks[taskid].state == Zombie -> taskid++ + :: else -> + if + :: tasks[taskid].state == OtherWait + -> tasks[taskid].state = Ready + printf("@@@ %d STATE %d Ready\n",_pid,taskid) + :: else -> skip + fi + liveSeen = true; + taskid++ + fi + od + printf("@@@ %d LOG ...all visited, live:%d\n",_pid,liveSeen); + if + :: liveSeen -> goto loop + :: else + fi + printf("@@@ %d LOG All are Zombies, game over.\n",_pid); + stopclock = true; + } + +Clock Process +~~~~~~~~~~~~~ + +A process is needed that handles a clock tick, +by decrementing the tick count for tasks waiting on a timeout. +Such a task whose ticks become zero is then made ``Ready``, +and its timer status is flagged as a timeout. This terminates when all +tasks are zombies (as signalled by ``System()`` via ``stopclock``). + +.. code-block:: c + + proctype Clock () { + int tid, tix; + printf("@@@ %d LOG Clock Started\n",_pid) + do + :: stopclock -> goto stopped + :: !stopclock -> + printf(" (tick) \n"); + tid = 1; + do + :: tid == TASK_MAX -> break + :: else -> + atomic{ + printf("Clock: tid=%d, state=",tid); + printm(tasks[tid].state); nl() + }; + if + :: tasks[tid].state == TimeWait -> + tix = tasks[tid].ticks - 1; + if + :: tix == 0 + tasks[tid].tout = true + tasks[tid].state = Ready + printf("@@@ %d STATE %d Ready\n",_pid,tid) + :: else + tasks[tid].ticks = tix + fi + :: else // state != TimeWait + fi + tid = tid + 1 + od + od + stopped: + printf("@@@ %d LOG Clock Stopped\n",_pid); + } + + +init Process +~~~~~~~~~~~~ + +The initial process outputs annotations for defines and declarations, +generates a scenario non-deterministically and then starts the system, clock +and send and receive processes running. It then waits for those to complete, +and them, if test generation is underway, asserts ``false`` to trigger a +seach for counterexamples: + +.. code-block:: c + + init { + pid nr; + printf("@@@ %d NAME Event_Manager_TestGen\n",_pid) + outputDefines(); + outputDeclarations(); + printf("@@@ %d INIT\n",_pid); + chooseScenario(); + run System(); + run Clock(); + run Sender(THIS_NODE,SEND_ID); + run Receiver(THIS_NODE,RCV_ID); + _nr_pr == 1; + #ifdef TEST_GEN + assert(false); + #endif + } + +The information regarding when tasks should wait and/or restart +can be obtained by tracking the process identifiers, +and noting when they change. +The ``spin2test`` program does this, +and also produces separate test code segments for each Promela process. + +Annotations +^^^^^^^^^^^ + +File: ``event-mgr-model.pml`` + +Nothing more to say here. + +Refinement +^^^^^^^^^^ + +File: ``event-mgr-model-rfn.yml`` + + +The test-code generated here is based on the test-code generated from the +specification items used to describe the Event Manager in the main (non-formal) +part of the new qualification material. + +The relevant specification item is ``spec/rtems/event/req/send-receive.yml`` +found in ``rtems-central``. The corresponding C test code is +``tr-event-send-receive.c`` found in ``rtems`` at ``testsuites/validation``. +That automatically generated C code is a single file that uses a set of deeply +nested loops to iterate through the scenarios it generates. + +The approach here is to generate a stand-alone C code file for each scenario +(``tr-event-mgr-model-N.c`` for ``N`` in range 0..8.) + + +The ``TASK`` annotations issued by the ``Sender`` and ``Receiver`` processes +lookup the following refinement entries, to get code that tests that the C +code Task does correspond to what is being defined in the model. + +.. code-block:: yaml + + Runner: | + checkTaskIs( ctx->runner_id ); + + Worker: | + checkTaskIs( ctx->worker_id ); + +The ``WAIT`` and ``SIGNAL`` annotations produced by ``Obtain()`` and +``Release()`` respectively, are mapped to the corresponding operations on +RTEMS semaphores in the test code. + +.. code-block:: yaml + + code content + SIGNAL: | + Wakeup( semaphore[{}] ); + + WAIT: | + Wait( semaphore[{}] ); + +Some of the ``CALL`` annotations are used to do more complex test setup +involving priorities, or other processors and schedulers. For example: + +.. code-block:: yaml + + HigherPriority: | + SetSelfPriority( PRIO_HIGH ); + rtems_task_priority prio; + rtems_status_code sc; + sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio ); + T_rsc_success( sc ); + T_eq_u32( prio, PRIO_HIGH ); + + SetProcessor: | + T_ge_u32( rtems_scheduler_get_processor_maximum(), 2 ); + uint32_t processor = {}; + cpu_set_t cpuset; + CPU_ZERO(&cpuset); + CPU_SET(processor, &cpuset); + +Some handle more complicated test outcomes, such as observing context-switches: + +.. code-block:: yaml + + CheckPreemption: | + log = &ctx->thread_switch_log; + T_eq_sz( log->header.recorded, 2 ); + T_eq_u32( log->events[ 0 ].heir, ctx->runner_id ); + T_eq_u32( log->events[ 1 ].heir, ctx->worker_id ); + +Most of the other refinement entries are similar to those described above for +the Chains API. + +Testing the Barrier Mananger +---------------------------- + +Documentation: Barrier Manager section in the RTEMS Classic API Guide. + +Model Directory: ``formal/promela/models/barriers``. + +Model Name: ``barrier-mgr-model``. + +The Barrier Manager is used to arrange for a number of tasks to wait on a +designated barrier object, until either another task releases them, or a +given number of tasks are waiting, at which point they are all released. + +All five directives were modelled: + +* ``rtems_barrier_create()`` + +* ``rtems_barrier_ident()`` + +* ``rtems_barrier_delete()`` + +* ``rtems_barrier_wait()`` + +* ``rtems_barrier_release()`` + +Barriers can be manual (released only by a call to ``..release()``), +or automatic (released by the call to ``..wait()`` that results in a wait count limit being reached.) +There is no notion of queuing in this manager, +only waiting for a barrier to be released. + +This model was developed by a Masters student :cite:`Jaskuc:2022:TESTGEN`, +using the Event Manager as a model. It was added into the QDP produced by +the follow-on IV&V activity. + +API Model +^^^^^^^^^ + +File: ``barrier-mgr-model.pml`` + +Modelling waiting is much easier than modelling queueing. +All that is required is an array of booleans (``waiters``), indexed by process id: + +.. code:: promela + + typedef Barrier { + byte b_name; // barrier name + bool isAutomatic; // true for automatic, false for manual barrier + int maxWaiters; // maximum count of waiters for automatic barrier + int waiterCount; // current amount of tasks waiting on the barrier + bool waiters[TASK_MAX]; // waiters on the barrier + bool isInitialised; // indicated whenever this barrier was created + } + +The name ``satisfied`` is currently used here for an inline that checks when +a barrier can be released. +Other helper inlines include ``waitAtBarrier()`` and ``barrierRelease()``. + +Behaviour Patterns +^^^^^^^^^^^^^^^^^^ + +File: ``barrier-mgr-model.pml`` + +The overall architecture in terms of Promela processes has processes ``init``, ``System``, ``Clock``, ``Runner``, +and two workers: ``Worker1`` and ``Worker2``. +The runner and workers each may perform one or more API calls, +in the following order: create, ident, wait, release, delete. +Scenarios mix and match which task does what. + +There are three top-level scenarios: + +.. code:: promela + + mtype = {ManAcqRel,AutoAcq,AutoToutDel}; + +In scenario ``ManAcqRel``, the runner will do create, release and delete, +with sub-scenarios to check error cases as well as good behaviour, +for manual barriers. +Good behaviour involves one or more workers doing a wait. +The ``AutoAcq`` and ``AutoToutDel`` +scenarios look at good and bad uses of automatic barriers. + +Annotations +^^^^^^^^^^^ + +File: ``barrier-mgr-model.pml`` + +Similiar to those used in the Event Manager. + +Refinement +^^^^^^^^^^ + +File: ``barrier-mgr-model-rfn.yml`` + +Similiar to those used in the Event Manager. + +Testing the Message Manager +--------------------------- + +Documentation: Message Manager section in the RTEMS Classic API Guide. + +Model Directory: ``formal/promela/models/messages``. + +Model Name: ``msg-mgr-model``. + +The Message Manager provides objects that act as message queues. Tasks can +interact with these by enqueuing and/or dequeuing message objects. + +There are 11 directives in total, but only the following were modelled: + + * ``rtems_message_queue_create()`` + + * ``rtems_message_queue_send()`` + + * ``rtems_message_queue_receive()`` + +The manager supports two queuing protocols, FIFO and priority-based. +Only the FIFO queueing was modelled. + +This model was developed by a Masters student :cite:`Lynch:2022:TESTGEN`, +using the Event Manager as a model. It was added into the QDP produced by +the follow-on IV&V activity. + +Below we focus on aspects of this model that differ from the Event Manager. + +API Model +^^^^^^^^^ + +File: ``msg-mgr-model.pml`` + +A key feature of this manager is that not only are messages in a queue, +but so are the tasks waiting for those messages. +Both task and message queues are modelled as circular buffers, +with inline definitions of enqueuing and dequeuing operations. + +While the Message Manager allows many queues to be created, +the model only uses one. + + +Behaviour Patterns +^^^^^^^^^^^^^^^^^^ + +File: ``msg-mgr-model.pml`` + +The overall architecture in terms of Promela processes has processes ``init``, ``System``, ``Clock``, ``Sender``, and two receivers: +``Receiver1`` and ``Receiver2``. +The ``Sender`` is the test runner, which performs the queue creation, +releases the start semaphore and then performs a send operation if needed. +The receivers are worker processes. + +There are four top level scenarios: + +.. code:: promela + + mtype = {Send,Receive,SndRcv, RcvSnd}; + +Scenarios ``Send`` and ``Receive`` are used for testing erroneous calls. +The ``SndRcv`` scenario fills up queues before the receivers run, +while the ``RcvSnd`` has the receivers waiting before messages are sent. + +Annotations +^^^^^^^^^^^ + +File: ``msg-mgr-model.pml`` + +Similiar to those used in the Event Manager. + +Refinement +^^^^^^^^^^ + +File: ``msg-mgr-model-rfn.yml`` + +Similiar to those used in the Event Manager. + +Current State of Play +--------------------- + +The models developed here are the result of +an ad-hoc incremental development process +and have a lot of overlapping material. + +Model State +^^^^^^^^^^^ + +The models were developed by first focusing on simple behavior +such as error handling, and then adding in simpler behaviors, +until sufficient coverage was acheived. +The basic philosophy at the time was not to fix anything not broken. + +This has led to the models being somewhat over-engineered, +particularly when it comes to scenario generation. +There is some conditional looping behaviour, +implemented using labels and ``goto``, +that should really be linearised, using conditionals to skip parts. +It is harder than it should be to understand what each scenario does. + +Also the API call models have perhaps a bit too much code devoted +to system behaviour. + +Model Refactoring +^^^^^^^^^^^^^^^^^ + +There is a case to be made to perform some model refactoring. +Some of this would address the model state issues above. +Other refactoring would extract the common model material out, +to be put into files that could be included. +This includes the binary semaphore models, +and the parts modelling preemption and waiting while blocked. + + +Test Code Refactoring +^^^^^^^^^^^^^^^^^^^^^ + +During the qualification activity, +a new file ``tx-support.c`` was added to the RTEMS validation testsuite codebase. +This gathers C test support functions used by most of the tests. +The contents of the ``tr-<modelname>.h`` and ``tr-<modelname>.c`` +files in particular should be brought in line with ``tx-support.c``. + +Suitable Promela models should also be produced +of relevant functions in ``tx-support.c``. + + + diff --git a/eng/fv/approaches.rst b/eng/fv/approaches.rst new file mode 100644 index 0000000..fe58a06 --- /dev/null +++ b/eng/fv/approaches.rst @@ -0,0 +1,178 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _FormalVerifApproaches: + +Formal Verification Approaches +============================== + +This is an overview of a range of formal methods and tools +that look feasible for use with RTEMS. + +A key criterion for any proposed tool is the ability to deploy it in a highly +automated manner. This amounts to the tool having a command-line interface that +covers all the required features. +One such feature is that the tool generates output that can be +easily transformed into the formats useful for qualification. +Tools with GUI interfaces can be very helpful while developing +and deploying formal models, as long as the models/tests/proofs +can be re-run automatically via the command-line. + +Other important criteria concerns the support available +for test generation support, +and how close the connection is between the formalism and actual C code. + +The final key criteria is whatever techniques are proposed should fit in +with the RTEMS Project Mission Statement, +in the Software Engineering manual. +This requires, among other things, +that any tool added to the tool-chain needs to be open-source. + +A more detailed report regarding this can be found in +:cite:`Butterfield:2021:FV1-200`. + + +Next is a general overview of formal methods and testing, +and discusses a number of formalisms and tools against the criteria above. + +Formal Methods Overview +----------------------- + +Formal specification languages can be divided into the following groups: + + Model-based: e.g., Z, VDM, B + + These have a language that describes a system in terms of having an abstract + state and how it is modified by operations. Reasoning is typically based + around the notions of pre- and post-conditions and state invariants. + The usual method of reasoning is by using theorem-proving. The resulting + models often have an unbounded number of possible states, and are capable + of describing unbounded numbers of operation steps. + + Finite State-based: e.g., finite-state machines (FSMs), SDL, Statecharts + + These are a variant of model-based specification, with the added constraint + that the number of states are bounded. Desired model properties are often + expressed using some form of temporal logic. The languages used to describe + these are often more constrained than in more general model-based + approaches. The finiteness allows reasoning by searching the model, + including doing exhaustive searches, a.k.a. model-checking. + + Process Algebras: e.g., CSP, CCS, pi-calculus, LOTOS + + These model systems in terms of the sequence of externally observable + events that they perform. There is no explicit definition of the abstract + states, but their underlying semantics is given as a state machine, + where the states are deduced from the overall behavior of the system, + and events denote transitions between these states. In general both the + number of such states and length of observed event sequences are unbounded. + While temporal logics can be used to express properties, many process + algebras use their own notation to express desired properties by simpler + systems. A technique called bisimulation is used to reason about the + relationships between these. + + Most of the methods above start with formal specifications/models. Also + needed is a way to bridge the gap to actual code. The relationship between + specification and code is often referred to as a :term:`refinement` + (some prefer the term :term:`reification`). Most model-based methods have refinement, + with the concept baked in as a key part of the methodology. + + Theorem Provers: e.g., CoQ, HOL4, PVS, Isabelle/HOL + + Many modern theorem provers are not only useful to help reason about the + formalisms mentioned above, but are often powerful enough to be used to + describe formal models in their own terms and then apply their proof + systems directly to those. + + Model Checkers: e.g., SPIN, FDR + + Model checkers are tools that do exhaustive searches over models with a + finite number of states. These are most commonly used with the finite-state + methods, as well as the process algebras where some bound is put on the + state-space. As model-checking is basically exhaustive testing, these are + often the easiest way to get test generation from formal techniques. + + Formal Development frameworks: e.g. TLA+, Frama-C, KeY + + There are also a number of frameworks that support a close connection + between a programming language, a formalism to specify desired behavior + for programs in that language, as well as tools to support the reasoning + (proof, simulation, test). + +Formal Methods actively considered +---------------------------------- + +Given the emphasis on verifying RTEMS C code, +the focus is on freely available tools that could easily connect to C. +These include: Frama-C, TLA+/PlusCal, Isabelle/HOL, and Promela/SPIN. +Further investigation ruled out TLA+/PlusCal because it is Java-based, +and requires installing a Java Runtime Environment. +Frama-C, Isabelle/HOL, and Promela/SPIN are discussed below in more detail, + +Frama-C +^^^^^^^ + +Frama-C (frama-c.com) is a platform supporting a range of tools for analysing C +code, including static analysers, support for functional specifications (ANSI-C +Specification Language – ACSL), and links to theorem provers. Some of its +analyses require code annotations, while others can extract useful information +from un-annotated code. It has a plug-in architecture, which makes it easy to +extend. It is used extensively by Airbus. + +Frama-C, and its plugins, are implemented in OCaml, +and it is installed using the ``opam`` package manager. +An issue here was that Frama-C has many quite large dependencies. +There was support for test generation, but it was not freely available. +Another issue was that Frama-C only supported C99, and not C11 +(the issue is how to handle C11 Atomics in terms of their semantics). + +Isabelle/HOL +^^^^^^^^^^^^ + +Isabelle/HOL is a wide-spectrum theorem-prover, implemented as an embedding of +Higher-Order Logic (HOL) into the Isabelle generic proof assistant +(isabelle.in.tum.de). It has a high degree of automation, including an ability +to link to third-party verification tools, and a very large library of verified +mathematical theorems, covering number and set theory, algebra, analysis. It is +based on the idea of a small trusted code kernel that defines an encapsulated +datatype representing a theorem, which can only be constructed using methods in +the kernel for that datatype, but which also scales effectively regardless of +how many theorems are so proven. +It is implemented using `polyml`, with the IDE implemented using Scala, +is open-source, and is easy to install. +However, like Frama-C, it is also a very large software suite. + +Formal Method actually used +--------------------------- + +A good survey of formal techniques and testing +is found in a 2009 ACM survey paper :cite:`Hierons:2009:FMT`. +Here they clearly state: + + "The most important role for formal verification in testing + is in the automated generation of test cases. + In this context, + model checking is the formal verification technology of choice; + this is due to the ability of model checkers + to produce counterexamples + in case a temporal property does not hold for a system model." + +Promela/SPIN +^^^^^^^^^^^^ + +The current use of formal methods in RTEMS is based on using the Promela +language to model key RTEMS features, +in such a way that tests can be generated using the SPIN model checker +(spinroot.com). +Promela is quite a low-level modelling language that makes it easy to get close +to code level, and is specifically targeted to modelling software. It is one of +the most widely used model-checkers, both in industry and education. It uses +assertions, and :term:`Linear Temporal Logic` (:term:`LTL`) to express properties of +interest. + +Given a Promela model that checks key properties successfully, +tests can be generated for a property *P* by asking +SPIN to check the negation of that property. +There are ways to get SPIN to generate multiple/all possible counterexamples, +as well as getting it to find the shortest. diff --git a/eng/fv/index.rst b/eng/fv/index.rst new file mode 100755 index 0000000..abeaa27 --- /dev/null +++ b/eng/fv/index.rst @@ -0,0 +1,16 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _FormalVerif: + +Formal Verification +******************* + +.. toctree:: + + overview + approaches + methodology + promela-index + diff --git a/eng/fv/methodology.rst b/eng/fv/methodology.rst new file mode 100755 index 0000000..71430cd --- /dev/null +++ b/eng/fv/methodology.rst @@ -0,0 +1,62 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _FormalVerifMethodology: + +Test Generation Methodology +=========================== + +The general approach to using any model-checking technology for test generation +has three major steps: + +Model desired behavior +---------------------- + +Construct a model that describes the desired properties (`P1`, ..., `PN`) +and use the model-checker to verify those properties. + +Promela can specify properties using the ``assert()`` statement, to be +true at the point where it gets executed, +and can use :term:`Linear Temporal Logic` +(LTL) to specify more complex properties over execution sequences. SPIN will +also check generic correctness properties such as deadlock and +livelock freedom. + +Make claims about undesired behavior +------------------------------------ + +Given a fully verified model, systematically negate each specified property. +Given that each property was verified as true, +then these negated properties will fail model-checking, +and counter-examples will be +generated. These counter-examples will in fact be scenarios describing correct +behavior of the system, demonstrating the truth of each property. + +.. warning:: + + It is very important that the negations only apply to stated properties, + and do not alter the possible behaviors of the model in any way. + The behaviours of the model are determined by the control-flow constructs, + so any boolean-valued expression statements used in these, + or used in sequential code to wait for some some condition, + should not be altered. + What can be altered are the expressions in ``assert()`` statements, + and any LTL properties. + +With Promela, there are a number of different ways to do systematic +negation. The precise approach adopted depends on the nature of the models, and +more details can be found +in the RTEMS Formal Models Guide Appendix in this document. + +Map good behavior scenarios to tests +------------------------------------ + +Define a mapping from counter-example output to test code, +and use this in the process of constructing a test program. + +A YAML file is used to define a mapping from SPIN output to +relevant fragments of RTEMS C test code, using the Test Framework section +in this document. +The process is automated by a python script called ``testbuilder``. + diff --git a/eng/fv/overview.rst b/eng/fv/overview.rst new file mode 100755 index 0000000..da981f2 --- /dev/null +++ b/eng/fv/overview.rst @@ -0,0 +1,38 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _FormalVerifOverview: + +Formal Verification Overview +============================ + +Formal Verification is a technique based on writing key design artifacts using +notations that have a well-defined mathematical :term:`semantics`. This means +that these descriptions can be rigorously analyzed using logic and other +mathematical tools. The term :term:`formal model` is used to refer to any such +description. + +Having a formal model of a software engineering artifact (requirements, +specification, code) allows it to be analyzed to assess the behavior it +describes. This means checks can be done that the model has desired properties, +and that it lacks undesired ones. A key feature of having a formal description +is that tools can be developed that parse the notation and perform much, +if not most, of the analysis. An industrial-strength formalism is one that has +very good tool support. + +Having two formal models of the same software object at different levels +of abstraction (specification and code, say) allows their comparison. In +particular, a formal analysis can establish if a lower level artifact like +code satisfies the properties described by a higher level, +such as a specification. This relationship is commonly referred to as a +:term:`refinement`. + +Often it is quite difficult to get a useful formal model of real code. Some +formal modelling approaches are capable of generating machine-readable +:term:`scenarios <scenario>` that describe possible correct behaviors of the +system at the relevant level of abstraction. A refinement for these can be +defined by using them to generate test code. +This is the technique that is used in :ref:`FormalVerifMethodology` to +verify parts of RTEMS. Formal models are constructed based on requirements +documentation, and are used as a basis for test generation. diff --git a/eng/fv/promela-index.rst b/eng/fv/promela-index.rst new file mode 100644 index 0000000..6b32841 --- /dev/null +++ b/eng/fv/promela-index.rst @@ -0,0 +1,9 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. toctree:: + + tool-setup + promela + refinement diff --git a/eng/fv/promela.rst b/eng/fv/promela.rst new file mode 100755 index 0000000..6ebb3eb --- /dev/null +++ b/eng/fv/promela.rst @@ -0,0 +1,323 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _PromelaModelling: + +Modelling with Promela +====================== + +Promela is a large language with many features, +but only a subset is used here for test generation. +This is a short overview of that subset. +The definitive documentation can be found at +https://spinroot.com/spin/Man/promela.html. + +Promela Execution +----------------- + +Promela is a *modelling* language, not a programming language. It is designed +to describe the kind of runtime behaviors that make reasoning about low-level +concurrency so difficult: namely shared mutable state and effectively +non-deterministic interleaving of concurrent threads. This means that there are +control constructs that specify non-deterministic outcomes, +and an execution model that allows the specification of when threads should +block. + +The execution model is based on the following concepts: + +Interleaving Concurrency + A running Promela system consists of one or more concurrent processes. Each + process is described by a segment of code that defines a sequence of + atomic steps. The scheduler looks at all the available next-steps and makes + a **non-deterministic choice** of which one will run. The scheduler is + invoked after every atomic step. + +Executability + At any point in time, a Promela process is either able to perform a step, + and is considered executable, or is unable to do so, and is considered + blocked. Whether a statement is executable or blocked may depend on the + global state of the model. The scheduler will only select from among the + executable processes. + +The Promela language is based loosely on C, and the SPIN model-checking tool +converts a Promela model into a C program that has the specific model +hard-coded and optimized for whatever analysis has been invoked. It also +supports the use of the C pre-processor. + +Simulation vs. Verification +^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +SPIN can run a model in several distinct modes: + +Simulation + SPIN simply makes random choices for the scheduler to produce a possible + execution sequence (a.k.a. scenario) allowed by the model. A readable + transcript is written to ``stdout`` as the simulation runs. + + The simplest SPIN invocation does simulation by default: + + .. code:: shell + + spin model.pml + +Verification + SPIN does an analysis of the whole model by exploring all the possible + choices that the scheduler can make. This will continue until either all + possible choices have been covered, or some form of error is uncovered. + If verification ends successfully, then this is simply reported as ok. + If an error occurs, verification stops, and the sequence of steps that led + to that failure are output to a so-called trail file. + + The simplest way to run a verification is to give the ``-run`` option: + + .. code:: shell + + spin -run model.pml + +Replaying + A trail file is an uninformative list of number-triples, but can be replayed + in simulation mode to produce human-readable output. + + .. code:: shell + + spin -t model.pml + +Promela Datatypes +----------------- + +Promela supports a subset of C scalar types (``short``, ``int``), but also +adds some of its own (``bit``, ``bool``, ``byte``, ``unsigned``). +It has support for one-dimensional arrays, +and its own variation of the C struct concept +(confusingly called a ``typedef``!). +It has a single enumeration type called ``mtype``. +There are no pointers in Promela, which means that modelling pointer +usage requires the use of arrays with their indices acting as proxies for +pointers. + +Promela Declarations +-------------------- + +Variables and one-dimensional arrays can be declared in Promela in much the +same way as they are done in C: + +.. code-block:: C + + int x, y[3] ; + +All global variables and arrays are initialized to zero. + +The identifier ``unsigned`` is the name of a type, rather than a modifier. +It is used to declare an unsigned number variable with a given bit-width: + +.. code-block:: C + + unsigned mask : 4 ; + + +Structure-like datatypes in Promela are defined using the ``typedef`` keyword +that associates a name with what is basically a C ``struct``: + +.. code-block:: C + + typedef CBuffer { + short count; + byte buffer[8] + } + + CBuffers cbuf[6]; + +Note that we can have arrays of ``typedef``\ s that themselves contain arrays. +This is the only way to get multi-dimensional arrays in Promela. + +There is only one enumeration type, which can be defined incrementally. +Consider the following sequence of four declarations that defines the values in +``mtype`` and declares two variables of that type: + +.. code-block:: C + + mtype = { up, down } ; + mtype dir1; + mtype = { left, right} ; + mtype dir2; + +This gives the same outcome with the following two declarations: + +.. code-block:: C + + mtype = { left, right, up, down } ; + mtype dir1, dir2; + +Special Identifiers +^^^^^^^^^^^^^^^^^^^ + +The are a number of variable identifiers that have a special meaning in Promela. +These all start with an underscore. We use the following: + +Process Id + ``_pid`` holds the process id of the currently active process + +Process Count + ``_nr_pr`` gives the number of currently active processes. + +Promela Atomic Statements +------------------------- + +Assignment + ``x = e`` where ``x`` is a variable and ``e`` is an expression. + + Expression ``e`` must have no side-effects. An assignment is always + executable. Its effect is to update the value of ``x`` with the current + value of ``e``. + +Condition Statement + ``e`` where ``e`` is an expression + + Expression ``e``, used standalone as a statement, is executable if its + value in the current state is non-zero. If its current value is zero, + then it is blocked. It behaves like a NO-OP when executed. + +Skip + ``skip``, a keyword + + ``skip`` is always executable, and behaves like a NO-OP when executed. + +Assertion + ``assert(e)`` where ``e`` is an expression + + An assertion is always executable. When executed, it evaluates its + expression. If the value is non-zero, then it behaves like a NO-OP. If the + value is zero, then it generates an assertion error and aborts further + simulation/verification of the model. + +Printing + ``printf(string,args)`` where ``string`` is a format-string and ``args`` + are values and expressions. + + A ``printf`` statement is completely ignored in verification mode. + In simulation mode, it is always executable, + and generates output to ``stdout`` in much the same way as in C. + This is is used in a structured way to assist with test generation. + +Goto + ``goto lbl`` where ``lbl`` is a statement label. + + Promela supports labels for statements, in the same manner as C. + The ``goto`` statement is always executable. + When executed, flow of control goes to the statement labelled by ``lbl:``. + +Break + ``break``, a keyword + + Can only occur within a loop (``do ... od``, see below). It is always + executable, and when executed performs a ``goto`` to the statement just + after the end of the innermost enclosing loop. + +Promela Composite Statements +---------------------------- + +Sequencing + ``{ <stmt> ; <stmt> ; ... ; <stmt> }`` where each ``<stmt>`` can be any + kind of statement, atomic or composite. The sub-statements execute in + sequence in the usual way. + +Selection + .. code-block:: none + + if + :: <stmt> + :: <stmt> + ... + :: <stmt> + fi + + A selection construct is blocked if all the ``<stmt>`` are blocked. It is + executable if at least one ``<stmt>`` is executable. The scheduler will make + a non-deterministic choice from all of those ``<stmt>`` that are executable. + The construct terminates when/if the chosen ``<stmt>`` does. + + Typically, a selection statement will be a sequence of the form + ``g ; s1 ; ... ; sN`` where ``g`` is an expression acting as a guard, + and the rest of the statements are intended to run if ``g`` is non-zero. + The symbol ``->`` plays the same syntactic role as ``;``, so this allows + for a more intuitive look and feel; ``g -> s1 ; ... ; sN``. + + If the last ``<stmt>`` has the form ``else -> ...``, then the ``else`` is + executable only when all the other selection statements are blocked. + +Repetition + .. code-block:: none + + do + :: <stmt> + :: <stmt> + ... + :: <stmt> + od + + The executability rules here are the same as for Selection above. The key + difference is that when/if a chosen ``<stmt>`` terminates, then the whole + construct is re-executed, making it basically an infinite loop. The only + way to exit this loop is for an active ``<stmt>`` to execute a ``break`` + or ``goto`` statement. + + A ``break`` statement only makes sense inside a Repetition, is always + executable, and its effect is to jump to the next statement after the + next ``od`` keyword in text order. + + +The selection and repetition syntax and semantics are based on Edsger +Djikstra's Guarded Command Language :cite:`Djikstra:1975:GCL` . + + +Atomic Composite + ``atomic{stmt}`` where ``stmt`` is usually a (sequential) composite. + + Wrapping the ``atomic`` keyword around a statement makes its entire + execution proceed without any interference from the scheduler. Once it is + executable, if the scheduler chooses it to run, then it runs to completion. + + There is one very important exception: if it should block internally because + some sub-statement is blocked, then the atomicity gets broken, and the + scheduler is free to find some other executable process to run. When/if the + sub-statement eventually becomes executable, once it gets chosen to run by + the scheduler then it continues to run atomically. + +Processes + ``proctype name (args) { sequence }`` where ``args`` is a list of zero + or more typed parameter declarations, + and ``sequence`` is a list of local declarations and statements. + + This defines a process type called ``name`` which takes parameters defined + by ``args`` and has the behavior defined by ``sequence``. When invoked, it + runs as a distinct concurrent process. Processes can be invoked explicitly + by an existing process using the ``run`` statement, + or can be setup to start automatically. + +Run + ``run name (exprs)`` where ``exprs`` is a list of expressions that match + the arguments defined the ``proctype`` declaration for ``name``. + + This is executable as long as the maximum process limit has not been reached, + and immediately starts the process running. + It is an atomic statement. + +Inlining + ``inline name (names) { sequence }`` where ``names`` is a list of zero or + more identifiers, and ``sequence`` is a list of declarations and statements. + + Inlining does textual substitution, and does not represent some kind of + function call. An invocation ``name(texts)`` gets replaced by + ``{ sequence }`` where each occurrence of an identifier in ``names`` is + replaced by the corresponding text in ``texts``. Such an invocation can + only appear in a context where a Promela statement can appear. + +Promela Top-Level +----------------- + +At the top-level, a Promela model is a list of declarations, much like a C +program. The Promela equivalent of ``main`` is a process called ``init`` that +has no arguments. There must be at least one Promela process setup to be running +at the start. This can be ``init``, or one or more ``proctype``\ s declared as +``active``. diff --git a/eng/fv/refinement.rst b/eng/fv/refinement.rst new file mode 100755 index 0000000..4cbad19 --- /dev/null +++ b/eng/fv/refinement.rst @@ -0,0 +1,559 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _Promela2CRefinement: + +Promela to C Refinement +======================= + +Promela models are more abstract than concrete C code. +A rigorous link, known as a :term:`refinement`, needs to be established +from Promela to C. +This is composed of two parts: +manual annotations in the Promela model to make its behavior easy +to identify and parse; +and a refinement defined as a YAML file that maps from +annotations to corresponding C code. +A single refinement YAML file is associated with each Promela model. + +Model Annotations +----------------- + +Promela ``printf`` statements are used in the models to output information that +is used by ``spin2test`` to generate test code. This information is used to +lookup keys in a YAML file that defines the mapping to C code. It uses a simple +format that makes it easy to parse and process, and is also designed to be +easily understood by a human reader. This is important because any V&V process +will require this information to be carefully assessed. + +Annotation Syntax +^^^^^^^^^^^^^^^^^ + +Format, where :math:`N \geq 0`: + + ``@@@ <pid> <KEYWORD> <parameter1> ... <parameterN>`` + +The leading ``@@@`` is a marker that makes it easy to filter out this +information from other SPIN output. + +Parameters take the following forms: + + ``<pid>`` Promela Process Id of ``proctype`` generating annotation + + ``<word>`` chunk of text containing no white space + + ``<name>`` Promela variable/structure/constant identifier + + ``<type>`` Promela type identifier + + ``<tid>`` OS Task/Thread/Process Id + + ``_`` unused argument (within containers) + +Each ``<KEYWORD>`` is associated with specific forms of parameters: + +.. code-block:: none + + LOG <word1> ... <wordN> + NAME <name> + INIT + DEF <name> <value> + DECL <type> <name> [<value>] + DCLARRAY <type> <name> <value> + TASK <name> + SIGNAL <name> <value> + WAIT <name> <value> + STATE tid <name> + SCALAR (<name>|_) [<index>] <value> + PTR <name> <value> + STRUCT <name> + SEQ <name> + END <name> + CALL <name> <value1> ... <valueN> + + +Annotation Lookup +----------------- + +The way that code is generated depends on the keyword in the annotation. +In particular, the keyword determines how, or if, +the YAML refinement file is looked up. + + Direct Output - no lookup + (``LOG``, ``DEF``) + + Keyword Refinement - lookup the ``<KEYWORD>`` + (``NAME``, ``INIT``, ``SIGNAL``, ``WAIT``) + + Name Refinement - lookup first parameter (considered as text) + (``TASK``, ``DECL``, ``DCLARRAY``, ``PTR``, ``CALL``, ``SCALAR``) + +The same name may appear in different contexts, +and the name can be extended with a suffix of the form +``_XXX`` to lookup less frequent uses: + + ``_DCL`` - A variable declaration + + ``_PTR`` - The pointer value itself + + ``_FSCALAR`` - A scalar that is a struct field + + ``_FPTR`` - A pointer that is a struct field + +Generally, the keyword, or name is used to lookup ``mymodel-rfn.yml`` to get a +string result. This string typically has substitution placeholders, as used by +the Python ``format()`` method for strings. The other parameters in the +annotation are then textually substituted in, to produce a segment of test code. + + +Specifying Refinement +--------------------- + +Using the terminology of the :ref:`RTEMSTestFramework` +each Promela model is converted into a set of Test Cases, +one for each complete scenario produced by test generation. +There are a number of template files, tailored for each model, +that are used to assemble the test code sources, +along with code segments for each Promela process, +based on the annotations output for any given scenario. + + +The refinement mapping from annotations to code is defined in a YAML file that +describes a Python dictionary that maps a name to some C code, with placeholders +that are used to allow for substituting in actual test values. + +The YAML file has entries of the following form: + +.. code:: yaml + + entity: | + C code line1{0} + ... + C code lineM{2} + +The entity is a reference to an annotation concept, which can refer to key +declarations, values, variables, types, API calls or model events. There can be +zero or more arguments in the annotations, and any occurrence of braces +enclosing a number in the C code means that the corresponding annotation +argument string is substituted in (using the python string object `format()` +method). + +The general pattern is working through all the annotations in order. The +code obtained by looking up the YAML file is collated into different +code-segments, one for each Promela process id (``<pid>``). + +In addition to the explicit annotations generated by the Promela models, there +are two implicit annotations produced by the python refinement code. These +occur when the ``<pid>`` part of a given explicit annotation is different to the +one belonging to the immediately preceding annotation. This indicates a point in +a test generation scenario where one task is suspended and another resumes. This +generates internal annotations with keywords ``SUSPEND`` and ``WAKEUP`` which +should have entries in the refinement file to provide code to ensure that the +corresponding RTEMS tasks in the test behave accordingly. + +The annotations can also be output as comments into the generated test-code, so +it is easy to check that parameters are correct, and the generated code is +correct. + +If a lookup fails, a C comment line is output stating the lookup failed. +The translation continues in any case. + +Lookup Example +^^^^^^^^^^^^^^ + +Consider the following annotation, from the Events Manager model: + + ``@@@ 1 CALL event_send 1 2 10 sendrc`` + +This uses Name refinement so a lookup with ``event_send`` as the key +and gets back the following text: + +.. code-block:: python3 + + T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, {1}), {2} ); + {3} = ( *ctx->send )( mapid( ctx, {1} ), {2} ); + T_log( T_NORMAL, "Returned 0x%x from Send", {3} ); + +Arguments ``1``, ``2``, ``10``, and ``sendrc`` +are then substituted to get the code: + +.. code-block:: c + + T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, 2), 10 ); + sendrc = ( *ctx->send )( mapid( ctx, 2 ), 10 ); + T_log( T_NORMAL, "Returned 0x%x from Send", sendrc ); + +Given a Promela process id of ``1``, this code is put into a code segment +for the corresponding RTEMS task. + + +Annotation Refinement Guide +--------------------------- + +This guide describes how each annotation is processed +by the test generation software. + +LOG +^^^ + +``LOG <word1> ... <wordN>`` (Direct Output) + Generate a call to ``T_log()`` with a message formed from the ``<word..>`` + parameters. + This message will appear in the test output for certain verbosity settings. + +NAME +^^^^ + +``NAME <name>`` (Keyword Refinement) + Looks up ``NAME`` (currently ignoring ``<name>``) and returns the resulting + text as is as part of the code. This code should define the name of the + testcase, if needed. + +INIT +^^^^ + +``INIT`` (Keyword Refinement) + Lookup ``INIT`` and expect to obtain test initialisation code. + +TASK +^^^^ + +``TASK <name>`` (Name Refinement) + Lookup ``<name>`` and return corresponding C code. + +SIGNAL +^^^^^^ + +``SIGNAL <value>`` (Keyword Refinement) + Lookup `SIGNAL` and return code with `<value>` substituted in. + +WAIT +^^^^ + +``WAIT <value>`` (Keyword Refinement) + Lookup `WAIT` and return code with `<value>` substituted in. + +DEF +^^^ + +``DEF <name> <value>`` (Direct Output) + Output ``#define <name> <value>``. + +DECL +^^^^ + +``DECL <type> <name> [<value>]`` (Name Refinement) + Lookup ``<name>_DCL`` and substitute ``<name>`` in. If ``<value>`` is + present, append ``=<value>``. Add a final semicolon. If the `<pid>` value + is zero, prepend ``static``. + +DCLARRAY +^^^^^^^^ + +``DCLARRAY <type> <name> <value>`` (Name Refinement) + Lookup ``<name>_DCL`` and substitute ``<name>`` and ``<value>`` in. If the + `<pid>` value is zero, prepend ``static``. + +CALL +^^^^ + +``CALL <name> <value0> .. <valueN>`` (Name refinement, ``N`` < 6) + Lookup ``<name>`` and substitute all ``<value..>`` in. + +STATE +^^^^^ + +``STATE <tid> <name>`` (Name Refinement) + Lookup ``<name>`` and substitute in ``<tid>``. + +STRUCT +^^^^^^ + +``STRUCT <name>`` + Declares the output of the contents of variable ``<name>`` + that is itself a structure. The ``<name>`` is noted, as is the fact + that a structured value is being processes. + Should not occur if already be processing a structure or a sequence. + +SEQ +^^^ + +``SEQ <name>`` + Declares the output of the contents of array variable ``<name>``. + The ``<name>`` is noted, as is the fact that an array is being processed. + Values are accumulated in a string now initialsed to empty. + Should not occur if already processing a structure or a sequence. + +PTR +^^^ + +``PTR <name> <value>`` (Name Refinement) + If not inside a ``STRUCT``, lookup ``<name>_PTR``. Two lines of code should + be returned. If the ``<value>`` is zero, use the first line, otherwise use + the second with ``<value>`` substituted in. This is required to handle NULL + pointers. + + If inside a ``STRUCT``, lookup ``<name>_FPTR``. Two lines of code should + be returned. If the ``<value>`` is zero, use the first line, otherwise use + the second with ``<value>`` substituted in. This is required to handle NULL + pointers. + +SCALAR +^^^^^^ + +There are quite a few variations here. + +``SCALAR _ <value>`` + Should only be used inside a ``SEQ``. A space and ``<value>`` is appended + to the string being accumulated by this ``SEQ``. + +``SCALAR <name> <value>`` (Name Refinement) + If not inside a ``STRUCT``, lookup ``<name>``, and substitute ``<value>`` + into the resulting code. + + If inside a ``STRUCT``, lookup ``<name>_FSCALAR`` and substitute the saved + ``STRUCT`` name and ``<value>`` into the resulting code. + + This should not be used inside a ``SEQ``. + +``SCALAR <name> <index> <value>`` (Name Refinement) + If not inside a ``STRUCT``, lookup ``<name>``, and substitute ``<index>`` + and ``<value>`` into the resulting code. + + If inside a ``STRUCT``, lookup ``<name>_FSCALAR`` and substitute the saved + ``STRUCT`` name and ``<value>`` into the resulting code. + + This should not be used inside a ``SEQ``. + +END +^^^ + +``END <name>`` + If inside a ``STRUCT``, terminates processing a + structured variable. + + If inside a ``SEQ``, lookup ``<name>_SEQ``. For each line of code obtained, + substitute in the saved sequence string. + Terminates processing a sequence/array variable. + + This should not be encountered outside of a ``STRUCT`` or ``SEQ``. + +SUSPEND and WAKEUP +^^^^^^^^^^^^^^^^^^ + +A change of Promela process id from ``oldid`` to ``newid`` has been found. +Increment a counter that tracks the number of such changes. + +``SUSPEND`` (Keyword Refinement) + + Lookup ``SUSPEND`` and substitute in the counter value, ``oldid`` and + ``newid``. + +``WAKEUP`` (Keyword Refinement) + + Lookup ``WAKEUP`` and substitute in the counter value, ``newid`` and + ``oldid``. + +Annotation Ordering +------------------- + +While most annotations occur in an order determined by any given test scenario, +there are some annotations that need to be issued first. These are, in order: +``NAME``, ``DEF``, ``DECL`` and ``DCLARRAY``, and finally, ``INIT``. + + +Test Code Assembly +------------------ + +The code snippets produced by refining annotations are not enough. +We also need boilerplate code to setup, coordinate and teardown the tests, +as well as providing useful C support functions. + +For a model called `mymodel` the following files are required: + +* ``mymodel.pml`` - the Promela model +* ``mymodel-rfn.yml`` - the model refinement to C test code +* ``tc-mymodel.c`` - the testcase setup C file +* ``tr-mymodel.h`` - the test-runner header file +* ``tr-mymodel.c`` - the test-runner setup C file + +The following files are templates used to assemble +a single test-runner C file +for each scenario generated by the Promela model: + +* ``mymodel-pre.h`` - preamble material at the start +* ``mymodel-run.h`` - test runner material +* ``mymodel-post.h`` - postamble material at the end. + +The process is entirely automated: + +.. code-block:: shell + + tbuild all mymodel + +The steps of the process are as follows: + +Scenario Generation +^^^^^^^^^^^^^^^^^^^ + +When SPIN is invoked to find all scenarios, +it will produce a number (N) of counterexample files +with a ``.trail`` extension. +These files hold numeric data that refer to SPIN internals. + +.. code-block:: none + + mymodel.pml1.trail + ... + mymodel.pmlN.trail + +SPIN is then used to take each trail file and produce a human-readable +text file, using the same format as the SPIN simulation output. +SPIN numbers files from 1 up, +whereas the RTEMS convention is to number things, +including filenames, from zero. +SPIN is used to produce readable output in text files with a ``.spn`` extension, +with 1 subtracted from the trail file number. +This results in the following files: + +.. code-block:: shell + + mymodel-0.spn + ... + mymodel-{N-1}.spn + +Test Code Generation +^^^^^^^^^^^^^^^^^^^^ + +Each SPIN output file ``mymodel-I.spn`` +is converted to a C test runner file ``tr-mymodel-I.c`` +by concatenating the following components: + +``mymodel-pre.h`` + This is a fairly standard first part of an RTEMS test C file. + It is used unchanged. + +refined test segments + The annotations in ``mymodel-I.spn`` are converted, in order, + into test code snippets using the refinement file ``mymodel-rfn.yml``. + Snippets are gathered into distinct code segments based on the Promela + process number reported in each annotation. + Each code segment is used to construct a C function called + ``TestSegmentP()``, where ``P`` is the relevant process number. + +``mymodel-post.h`` + This is static code that declares the top-level RTEMS Tasks + used in the test. + These are where the code segments above get invoked. + +``mymodel-run.h`` + This defines top-level C functions that implement a given test runner. The top-level function has a name like ``RtemsMyModel_Run`` + This is not valid C as it needs to produce a name parameterized by + the relevant scenario number. It contains Python string format substitution + placeholders that allow the relevant number to be added to end of the + function name. So the above run function actually appears in this file as ``RtemsMyModel_Run{0}``, so ``I`` will be substituted in for ``{0}`` to result in the name ``RtemsMyModel_RunI``. + In particular, it invokes ``TestSegment0()`` which contains code + generated from Promela process 0, which is the main model function. + This declares test variables, and initializes them. + +These will generate test-runner test files as follows: + +.. code-block:: none + + tr-mymodel-0.c + ... + tr-mymodel-{N-1}.c + +In addition, the test case file ``tc-mymodel.c`` needs to have entries added +manually of the form below, for ``I`` in the range 0 to N-1.: + +.. code-block:: c + + T_TEST_CASE( RtemsMyModelI ) + { + RtemsMyModel_RunI( + ... + ); + } + +These define the individual test cases in the model, each corresponding to precisely one SPIN scenario. + +Test Code Deployment +^^^^^^^^^^^^^^^^^^^^ + +All files starting with ``tc-`` or ``tr-`` are copied to the +relevant testsuite directory. +At present, this is ``testsuites/validation`` at the top level in +the ``rtems`` repository. +All the names of the above files with a ``.c`` extension are added +into a YAML file that +defines the Promela generated-test sources. +At present, this +is ``spec/build/testsuites/validation/model-0.yml`` +at the top-level in the ``rtems`` repository. +They appear in the YAML file under the ``source`` key: + +.. code-block:: yaml + + source: + - testsuites/validation/tc-mymodel.c + - testsuites/validation/tr-mymodel-0.c + ... + - testsuites/validation/tr-mymodel-{N-1}.c + - testsuites/validation/ts-model-0.c + +Performing Tests +^^^^^^^^^^^^^^^^ + +At this point build RTEMS as normal. e.g., with ``waf``, +and the tests will get built. +The executable will be found in the designated build directory, +*(e.g.):* + + ``rtems/build/sparc/gr740/testsuites/validation/ts-model-0.exe`` + + This can be run using the RTEMS Tester + (RTEMS User Manual, Host Tools, RTEMS Tester and Run). + + + Both building the code and running on the tester is also automated + (see :ref:`FormalToolSetup`). + +Traceability +------------ + +Traceability between requirements, specifications, designs, code, and tests, +is a key part of any qualification/certification effort. The test generation +methodology developed here supports this in two ways, when refining an +annotation: + +1. If the annotation is for a declaration of some sort, the annotation itself + is added as a comment to the output code, just before the refined declaration. + + .. code-block:: c + + // @@@ 0 NAME Chain_AutoGen + // @@@ 0 DEF MAX_SIZE 8 + #define MAX_SIZE 8 + // @@@ 0 DCLARRAY Node memory MAX_SIZE + static item memory[MAX_SIZE]; + // @@@ 0 DECL unsigned nptr NULL + static item * nptr = NULL; + // @@@ 0 DECL Control chain + static rtems_chain_control chain; + +2. If the annotation is for a test of some sort, a call to ``T_log()`` is + generated with the annotation as its text, just before the test code. + + .. code-block:: c + + T_log(T_NORMAL,"@@@ 0 INIT"); + rtems_chain_initialize_empty( &chain ); + T_log(T_NORMAL,"@@@ 0 SEQ chain"); + T_log(T_NORMAL,"@@@ 0 END chain"); + show_chain( &chain, ctx->buffer ); + T_eq_str( ctx->buffer, " 0" ); + +In addition to traceability, these also help when debugging models, refinement +files, and the resulting test code. diff --git a/eng/fv/tool-setup.rst b/eng/fv/tool-setup.rst new file mode 100755 index 0000000..f8cf046 --- /dev/null +++ b/eng/fv/tool-setup.rst @@ -0,0 +1,317 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _FormalToolSetup: + +Formal Tools Setup +================== + +The required formal tools consist of +the model checking software (Promela/SPIN), +and the test generation software (spin2test/testbuilder). + +Installing Tools +---------------- + +Installing Promela/SPIN +^^^^^^^^^^^^^^^^^^^^^^^ + +Follow the installation instructions for Promela/Spin +at https://spinroot.com/spin/Man/README.html. + +There are references there to the Spin Distribution which is now on +Github (https://github.com/nimble-code/Spin). + +Installing Test Generation Tools +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +The test generation tools are found in ``formal/promela/src``, written in +Python3, and installed using a virtual environment. +To build the tools, enter ``formal/promela/src`` and issue the +commands: + +.. code:: shell + + make env + . env/bin/activate + make py + +The test generation tools need to be used from within this Python virtual +environment. Use the ``deactivate`` command to exit from it. + +Test generation is managed at the top level by the script ``testbuilder.py`` +located in the top-level of ``formal/promela/src``. +To avoid using (long) absolute pathnames, +it helps to define an suitable alias +*(e.g.)*: + +.. code-block:: shell + + alias tbuild='python3 /..../formal/promela/src/testbuilder.py' + +This alias is used subsequently in this documentation. + +To check for a successful tool build, invoke the command without any +arguments, which should result in an extended help message being displayed: + +.. code-block:: shell + + (env) prompt % tbuild + USAGE: + help - more details about usage and commands below + all modelname - runs clean, spin, gentests, copy, compile and run + clean modelname - remove spin, test files + archive modelname - archives spin, test files + zero - remove all tesfiles from RTEMS + spin modelname - generate spin files + gentests modelname - generate test files + copy modelname - copy test files and configuration to RTEMS + compile - compiles RTEMS tests + run - runs RTEMS tests + +The tool is not yet ready for use, as it needs to be configured. + +Tool Configuration +------------------ + +Tool configuration involves setting up a new testsuite in RTEMS, and providing +information to ``tbuild`` that tells it where to find key locations, and some +command-line arguments for some of the tools. +A template file ``testbuilder-template.yml`` is included, +and contains the following entries: + +.. code-block:: python + + # This should be specialised for your setup, as testbuilder.yml, + # located in the same directory as testbuilder.py + # All pathnames should be absolute + + spin2test: <spin2test_directory>/spin2test.py + rtems: <path-to-main-rtems-directory> # rtems.git, or ..../modules/rtems/ + rsb: <rsb-build_directory>/rtems/6/bin/ + simulator: <path-to>/sparc-rtems6-sis + testyamldir: <rtems>/spec/build/testsuites/validation/ # directory containing <modelname>.yml + testcode: <rtems>/testsuites/validation/ + testexedir: <rtems>/build/.../testsuites/validation/ # directory containing ts-<modelname>.exe + testsuite: model-0 + simulatorargs: -leon3 -r s -m 2 # run command executes "<simulator> <simargs> <testexedir>/ts-<testsuite>.exe" + spinallscenarios: -DTEST_GEN -run -E -c0 -e # trail generation "spin <spinallscenarios> <model>.pml" + +This template should be copied/renamed to ``testbuilder.yml`` +and each entry updated as follows: + +* spin2test: + This should be the absolute path to ``spin2test.py`` + in the Promela sources directory. + + ``/.../formal/promela/src/spin2test.py`` + +* rtems: + This should be the absolute path to your RTEMS source directory, + with the terminating ``/``. + From ``rtems-central`` this would be: + + ``/.../rtems-central/modules/rtems/`` + + For a separate ``rtems`` installation + it would be where ``rtems.git`` was cloned. + + We refer to this path below as ``<rtems>``. + +* rsb: + This should be the absolute path + to your RTEMS source-builder binaries directory, + with the terminating ``/``. + From ``rtems-central`` this would be (assuming RTEMS 6): + + ``/.../rtems-central/modules/rsb/6/bin/`` + +* simulator: + This should be the absolute path to the RTEMS Tester + (See Host Tools in the RTEMS User Manual) + + It defaults at present to the ``sis`` simulator + + ``/.../rtems-central/modules/rsb/6/bin/sparc-rtems6-sis`` + +* testsuite: + This is the name for the testsuite : + + Default value: ``model-0`` + +* testyamldir: + This should be the absolute path to where validation tests are *specified*: + + ``<rtems>/spec/build/testsuites/validation/`` + +* testcode: + This should be the absolute path to where validation test sources + are found: + + ``<rtems>/testsuites/validation/`` + +* testexedir: + This should be the absolute path to where + the model-based validation test executable + will be found: + + ``<rtems>/build/.../testsuites/validation/`` + + This will contain ``ts-<testsuite>.exe`` (e.g. ``ts-model-0.exe``) + +* simulatorargs: + These are the command line arguments for the RTEMS Tester. + It defaults at present to those for the ``sis`` simulator. + + ``-<bsp> -r s -m <cpus>`` + + The first argument should be the BSP used when building RTEMS sources. + BSPs ``leon3``, ``gr712rc`` and ``gr740`` have been used. + The argument to the ``-m`` flag is the number of cores. + Possible values are: 1, 2 and 4 (BSP dependent) + + Default: ``-leon3 -r s -m 2`` + +* spinallscenarios: + These are command line arguments for SPIN, + that ensure that all counter-examples are generated. + + Default: ``-DTEST_GEN -run -E -c0 -e`` (recommended) + +Testsuite Setup +^^^^^^^^^^^^^^^ + +The C test code generated by these tools is installed into the main ``rtems`` +repository at ``testsuites/validation`` in the exact same way as other RTEMS +test code. +This means that whenever ``waf`` is used at the top level to build and/or run +tests, that the formally generated code is automatically included. +This requires adding and modifying some *Specification Items* +(See Software Requirements Engineering section in this document). + +To create a testsuite called ``model-0`` (say), do the following, in the +``spec/build/testsuites/validation`` directory: + +* Edit ``grp.yml`` and add the following two lines into the `links` entry: + + .. code-block:: YAML + + - role: build-dependency + uid: model-0 + +* Copy ``validation-0.yml`` (say) to ``model-0.yml``, and change the following + entries as shown: + + .. code-block:: YAML + + enabled-by: RTEMS_SMP + source: + - testsuites/validation/ts-model-0.c + target: testsuites/validation/ts-model-0.exe + +Then, go to the ``testsuites/validation`` directory, and copy +``ts-validation-0.c`` to ``ts-model-0.c``, and edit as follows: + + * Change all occurrences of ``Validation0`` in comments to ``Model0``. + + * Change ``rtems_test_name`` to ``Model0``. + +Running Test Generation +----------------------- + +The testbuilder takes a command as its first command-line argument. Some of +these commands require the model-name as a second argument: + + Usage: ``tbuild <command> [<modelname>]`` + +The commands provided are: + +``clean <model>`` + Removes generated files. + +``spin <model>`` + Runs SPIN to find all scenarios. The scenarios are found in numbered files + called ``<model>N.spn``. + +``gentests <model>`` + Convert SPIN scenarios to test sources. Each ``<model>N.spn`` produces a numbered + test source file. + +``copy <model>`` + Copies the generated test files to the relevant test source directory, and + updates the relevant test configuration files. + +``archive <model>`` + Copies generated spn, trail, source, and test log files to an archive + sub-directory of the model directory. + +``compile`` + Rebuilds the test executable. + +``run`` + Runs tests in a simulator. + +``all <model>`` + Does clean, spin, gentests, copy, compile, and run. + +``zero`` + Removes all generated test filenames from the test configuration files, but + does NOT remove the test sources from the test source directory. + +In order to generate test files the following input files are required: + ``<model>.pml``, + ``<model>-rfn.yml``, + ``<model>-pre.h``, + ``<model>-post.h``, and + ``<model>-run.h``. +In addition there may be other files +whose names have <model> embedded in them. These are included in what is +transfered to the test source directory by the copy command. + +The simplest way to check test generation is setup properly is to visit one of +the models, found under ``formal/promela/models`` and execute the following +command: + +.. code-block:: shell + + tbuild all mymodel + +This should end by generating a file `model-0-test.log`. The output is +identical to that generated by the regular RTEMS tests, using the +*Software Test Framework* described elsewhere in this document. + +Output for the Event Manager model, highly redacted: + +.. code-block:: + + SIS - SPARC/RISCV instruction simulator 2.29, copyright Jiri Gaisler 2020 + Bug-reports to jiri@gaisler.se + + GR740/LEON4 emulation enabled, 4 cpus online, delta 50 clocks + + Loaded ts-model-0.exe, entry 0x00000000 + + *** BEGIN OF TEST Model0 *** + *** TEST VERSION: 6.0.0.03337dab21e961585d323a9974c8eea6106c803d + *** TEST STATE: EXPECTED_PASS + *** TEST BUILD: RTEMS_SMP + *** TEST TOOLS: 10.3.1 20210409 (RTEMS 6, RSB 889cf95db0122bd1a6b21598569620c40ff2069d, Newlib eb03ac1) + A:Model0 + S:Platform:RTEMS + ... + B:RtemsModelSystemEventsMgr8 + ... + L:@@@ 3 CALL event_send 1 2 10 sendrc + L:Calling Send(167837697,10) + L:Returned 0x0 from Send + ... + E:RtemsModelEventsMgr0:N:21:F:0:D:0.005648 + Z:Model0:C:18:N:430:F:0:D:0.130464 + Y:ReportHash:SHA256:5EeLdWsRd25IE-ZsS6pduLDsrD_qzB59dMU-Mg2-BDA= + + *** END OF TEST Model0 *** + + cpu 0 in error mode (tt = 0x80) + 6927700 0000d580: 91d02000 ta 0x0 + diff --git a/eng/glossary.rst b/eng/glossary.rst index e4adbef..a015eda 100644 --- a/eng/glossary.rst +++ b/eng/glossary.rst @@ -1,6 +1,7 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2017, 2019 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2022, 2023 Trinity College Dublin +.. Copyright (C) 2017, 2019 embedded brains GmbH & Co. KG .. Copyright (C) 1988, 1998 On-Line Applications Research Corporation (OAR) Glossary @@ -39,6 +40,10 @@ Glossary This term is an acronym for `Executable and Linkable Format <https://en.wikipedia.org/wiki/Executable_and_Linkable_Format>`_. + formal model + A model of a computing component (hardware or software) that has a + mathematically based :term:`semantics`. + GCC This term is an acronym for `GNU Compiler Collection <https://gcc.gnu.org/>`_. @@ -63,6 +68,20 @@ Glossary ISVV This term is an acronym for Independent Software Verification and Validation. + Linear Temporal Logic + This is a logic that states properties about (possibly infinite) sequences of + states. + + LTL + This term is an acronym for :term:`Linear Temporal Logic`. + + refinement + A *refinement* is a relationship between a specification and its + implementation as code. + + reification + Another term used to denote :term:`refinement`. + ReqIF This term is an acronym for `Requirements Interchange Format <https://www.omg.org/spec/ReqIF/About-ReqIF/>`_. @@ -70,6 +89,17 @@ Glossary RTEMS This term is an acronym for Real-Time Executive for Multiprocessor Systems. + scenario + In the context of formal verification, in a setting that involves many + concurrent tasks that interleave in arbitrary ways, a scenario describes a + single specific possible interleaving. One interpretation of the behaviour + of a concurrent system is the set of all its scenarios. + + semantics + This term refers to the meaning of text or utterances in some language. In a + software engineering context these will be programming, modelling or + specification languages. + software component This term is defined by ECSS-E-ST-40C 3.2.28 as a "part of a software system". For this project a *software component* shall be any of the @@ -122,6 +152,9 @@ Glossary software as it is originally written (i.e., typed into a computer) by a human in plain text (i.e., human readable alphanumeric characters)." + target + The system on which the application will ultimately execute. + task This project uses the `thread definition of Wikipedia <https://en.wikipedia.org/wiki/Thread_(computing)>`_: diff --git a/eng/index.rst b/eng/index.rst index d5d6f85..e4712ae 100644 --- a/eng/index.rst +++ b/eng/index.rst @@ -11,7 +11,8 @@ RTEMS Software Engineering (|version|) .. topic:: Copyrights and License - | |copy| 2018, 2020 embedded brains GmbH + | |copy| 2022 Trinity College Dublin + | |copy| 2018, 2020 embedded brains GmbH & Co. KG | |copy| 2018, 2020 Sebastian Huber | |copy| 1988, 2015 On-Line Applications Research Corporation (OAR) @@ -31,11 +32,13 @@ RTEMS Software Engineering (|version|) management test-plan test-framework + fv/index build-system release-mgmt users-manuals license-requirements appendix-a + fv/appendix-fv function_and_variable concept glossary diff --git a/eng/issue-tracking.rst b/eng/issue-tracking.rst index 1039b41..790ae83 100644 --- a/eng/issue-tracking.rst +++ b/eng/issue-tracking.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019 embedded brains GmbH +.. Copyright (C) 2019 embedded brains GmbH & Co. KG .. Copyright (C) 2019 Sebastian Huber .. Copyright (C) 2018 Joel Sherill diff --git a/eng/license-requirements.rst b/eng/license-requirements.rst index b2720f2..537b45e 100644 --- a/eng/license-requirements.rst +++ b/eng/license-requirements.rst @@ -98,9 +98,33 @@ these guidelines: * Advertising obligations are not acceptable. * Some license restrictions may be permissible. These will be considered - on a case-by-case basis. + on a case-by-case basis. See below for a list of such restrictions. In practice, these guidelines are not hard to follow. Critically, they protect the freedom of the RTEMS source code and that of end users to select the license and distribution terms they prefer for their RTEMS-based application. + +License restrictions +-------------------- + +* Apache License 2.0 in section 4 (b) requires modified files to carry + prominent notice about performed modification. In case you modify such + file and the notice is not there yet you are required to put notice + below at the top of the modified file. If the notice is already + there you don't need to add it second time. + The notice should look: + + .. code-block:: c + + /* + * The file was modified by RTEMS contributors. + */ + + .. warning:: Do not import any project or files covered by the Apache + License 2.0 into the RTEMS project source tree without + discussing first with developers on the mailing list! + Handling of Apache License 2.0 projects is a bit + sensitive manner and RTEMS project is not prepared to + handle one kind of those projects yet. E.g. the projects + with NOTICE file present in the source tree. diff --git a/eng/mission.rst b/eng/mission.rst index e1b0ec5..2c6aef1 100644 --- a/eng/mission.rst +++ b/eng/mission.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020 embedded brains GmbH +.. Copyright (C) 2020 embedded brains GmbH & Co. KG .. Copyright (C) 2015 Chris Johns .. Copyright (C) 1988, 2008 On-Line Applications Research Corporation (OAR) diff --git a/eng/preface.rst b/eng/preface.rst index f6fda0c..68c84fb 100644 --- a/eng/preface.rst +++ b/eng/preface.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020 embedded brains GmbH +.. Copyright (C) 2020 embedded brains GmbH & Co. KG Preface ******* diff --git a/eng/prequalification.rst b/eng/prequalification.rst index ba1840a..0d4561b 100644 --- a/eng/prequalification.rst +++ b/eng/prequalification.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020 embedded brains GmbH +.. Copyright (C) 2020 embedded brains GmbH & Co. KG .. Copyright (C) 2016, 2018 RTEMS Foundation, The RTEMS Documentation Project .. Copyright (C) 1988, 2008 On-Line Applications Research Corporation (OAR) @@ -15,7 +15,7 @@ standards typically do not specify software functionality but address topics like requirements definition, traceability, having a documented change process, coding style, testing requirements, and a user's manual. During system test, these standards call for a review - usually -by an independent entity - that the standard has been adhered too. These +by an independent entity - that the standard has been adhered to. These reviews cover a broad variety of topics and activities, but the process is generally referred to as qualification, verification, or auditing against the specific standard in use. The RTEMS Project will use the @@ -83,8 +83,8 @@ Stakeholder Involvement Qualification of RTEMS is a specialized activity and only specific users of RTEMS will complete a formal qualification activity. The RTEMS Project -cannot self-fund this entire activity and requires stakeholder to invest -in an ongoing basis to ensure that any investment they make is maintained -and viable in an ongoing basis. The RTEMS core developers view steady +cannot self-fund this entire activity and requires stakeholders to invest +on an ongoing basis to ensure that any investment they make is maintained +and viable in the long-term. The RTEMS core developers view steady support of the qualification effort as necessary to continue to lower the overall costs of qualifying RTEMS. diff --git a/eng/python-devel.rst b/eng/python-devel.rst index b1e0fa6..f1502e4 100644 --- a/eng/python-devel.rst +++ b/eng/python-devel.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2020 embedded brains GmbH & Co. KG .. _PythonDevelGuide: diff --git a/eng/release-process.rst b/eng/release-process.rst index e571b0d..7c250ea 100644 --- a/eng/release-process.rst +++ b/eng/release-process.rst @@ -159,21 +159,23 @@ Release Repositories The following are the repositories that a release effects. Any repository action is to be performed in the following repositories: -#. ``rtems.git`` +* ``rtems.git`` -#. ``rtems-docs.git`` +* ``rtems-central.git`` -#. ``rtems-examples.git`` +* ``rtems-docs.git`` -#. ``rtems-libbsd.git`` +* ``rtems-examples.git`` -#. ``rtems-source-builder.git`` +* ``rtems-libbsd.git`` -#. ``rtems-tools.git`` +* ``rtems-release.git`` -#. ``rtems_waf.git`` +* ``rtems-source-builder.git`` -#. ``rtems-release.git`` +* ``rtems-tools.git`` + +* ``rtems_waf.git`` Pre-Release Procedure ===================== @@ -220,7 +222,7 @@ Pre-Branch Procedure * Check and make sure the RSB kernel, libbsd and tools configurations reference the ``master`` when the branch is made. - The RSB GIT builds reference a specific commit so it is important + The RSB Git builds reference a specific commit so it is important the relevant configurations are valid. Branch Procedure @@ -274,29 +276,29 @@ Post-Branch Procedure #. Add the milestones for the new development branch. The Trac page is: - .. code-block:: none + .. code-block:: none - = 6.1 (open) + = 6.1 (open) - == Statistics + == Statistics - || '''Total'''||[[TicketQuery(milestone=6.1,count)]] || - || Fixed||[[TicketQuery(status=closed&milestone=6.1,resolution=fixed,count,)]] || - || Invalid||[[TicketQuery(status=closed&milestone=6.1,resolution=invalid,count,)]] || - || Works for me||[[TicketQuery(status=closed&milestone=6.1,resolution=worksforme,count,)]] || - || Duplicate||[[TicketQuery(status=closed&milestone=6.1,resolution=duplicate,count,)]] || - || Won't fix||[[TicketQuery(status=closed&milestone=6.1,resolution=wontfix,count,)]] || + || '''Total'''||[[TicketQuery(milestone=6.1,count)]] || + || Fixed||[[TicketQuery(status=closed&milestone=6.1,resolution=fixed,count,)]] || + || Invalid||[[TicketQuery(status=closed&milestone=6.1,resolution=invalid,count,)]] || + || Works for me||[[TicketQuery(status=closed&milestone=6.1,resolution=worksforme,count,)]] || + || Duplicate||[[TicketQuery(status=closed&milestone=6.1,resolution=duplicate,count,)]] || + || Won't fix||[[TicketQuery(status=closed&milestone=6.1,resolution=wontfix,count,)]] || - == Distribution - [[TicketQuery(milestone=6.1&group=type,format=progress)]] + == Distribution + [[TicketQuery(milestone=6.1&group=type,format=progress)]] - == Summary - [[TicketQuery(milestone=6.1)]] + == Summary + [[TicketQuery(milestone=6.1)]] - == Details - [[TicketQuery(col=id|time|resolution|component|reporter|owner|changetime,status=closed&milestone=6.1,rows=summary|description,table)]] + == Details + [[TicketQuery(col=id|time|resolution|component|reporter|owner|changetime,status=closed&milestone=6.1,rows=summary|description,table)]] - Replace ``6.1`` with the required milestone. + Replace ``6.1`` with the required milestone. #. Create the RC1 release candidate with the source as close the branch point as possible. @@ -307,6 +309,14 @@ Post-Branch Procedure add no value to a released RSB. For example leaving RTEMS 6 tool building configurations in the RTEMS 5 release. +#. Check out the release branch of ``rtems-central.git``. Change all Git + submodules to reference commits of the corresponding release branch. Run + ``./spec2modules.py``. Inspect all Git submodules for changes. If there + are locally modified files, then there are two options. Firstly, integrate + the changes in the release branches. Afterwards update the Git submodule + commit. Secondly, change the specification so that a particular change is + not made. Make sure that there are no changes after this procedure. + Post-Branch Version Number Updates ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -316,17 +326,17 @@ the needed changes. #. RTEMS requires the following files be changed: - * :file:`aclocal/version.m4` + * :file:`Doxyfile`: Update ``PROJECT_NUMBER``. - * :file:`c/src/aclocal/version.m4` + * :file:`rtems-bsps`: Update ``rtems_version``. - * :file:`cpukit/aclocal/version.m4` + * :file:`spec/build/cpukit/optvermaj.yml`: Update ``set-value``. - * :file:`Doxyfile` + * :file:`spec/build/cpukit/optvermin.yml`: Update ``set-value``. - * :file:`testsuites/aclocal/version.m4` + * :file:`spec/build/cpukit/optverrev.yml`: Update ``set-value``. - * :file:`rtems-bsps` + * :file:`wscript`: Update ``default_prefix``. #. RTEMS Documentation the following files be changed: diff --git a/eng/req/howto.rst b/eng/req/howto.rst index c8bd8c5..325c443 100644 --- a/eng/req/howto.rst +++ b/eng/req/howto.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020, 2021 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2020, 2023 embedded brains GmbH & Co. KG How-To ====== @@ -33,16 +33,110 @@ environment in your shell: cd rtems-central . env/bin/activate +View the Specification Graph +---------------------------- + +The specification items form directed graphs through :ref:`SpecTypeLink` +attributes. Each link has a role. For a particular view only specific roles +may be of interest. For example, the requirements specification of RTEMS +starts with the ``spec:/req/root`` specification item. It should form a tree +(connected graph without cycles). A text representation of the tree can be +printed with the ``./specview.py`` script: + +.. code-block:: none + + cd rtems-central + . env/bin/activate + ./specview.py + +This gives the following example output (shortened): + +.. code-block:: none + + /req/root (type=requirement/non-functional/design) + /bsp/if/group (type=requirement/non-functional/design-group, role=requirement-refinement) + /bsp/if/acfg-idle-task-body (type=interface/unspecified-define, role=interface-ingroup) + /bsp/sparc/leon3/req/idle-task-body (type=requirement/functional/function, role=interface-function) + /bsp/sparc/leon3/req/idle-task-power-down (type=requirement/functional/function, role=requirement-refinement) + /bsp/sparc/leon3/val/errata-gr712rc-08 (type=validation, role=validation) + /bsp/sparc/leon3/req/idle-task-power-down-errata (type=requirement/functional/function, role=requirement-refinement) + /bsp/sparc/leon3/val/errata-gr712rc-08 (type=validation, role=validation) + +The actual specification graph depends on build configuration options which +enable or disable specification items. The ``--enabled`` command line option +may be used to specify the build configuration options, for example +``--enabled=sparc,bsps/sparc/leon3,sparc/gr740,RTEMS_SMP,RTEMS_QUAL``. + +The ``./specview.py`` script can display other views of the specification +through the ``--filter`` command line option. Transition maps of +:ref:`SpecTypeActionRequirementItemType` items can be printed using the +``--filter=action-table`` or ``--filter=action-list`` filters. For example, +``./specview.py --filter=action-table /rtems/timer/req/create`` prints +something like this: + +.. code-block:: none + + .. table:: + :class: longtable + + ===== ========== ======= ===== ==== ======= ======= ===== + Entry Descriptor Name Id Free Status Name IdVar + ===== ========== ======= ===== ==== ======= ======= ===== + 0 0 Valid Valid Yes Ok Valid Set + 1 0 Valid Valid No TooMany Invalid Nop + 2 0 Valid Null Yes InvAddr Invalid Nop + 3 0 Valid Null No InvAddr Invalid Nop + 4 0 Invalid Valid Yes InvName Invalid Nop + 5 0 Invalid Valid No InvName Invalid Nop + 6 0 Invalid Null Yes InvName Invalid Nop + 7 0 Invalid Null No InvName Invalid Nop + ===== ========== ======= ===== ==== ======= ======= ===== + +For example, ``./specview.py --filter=action-list /rtems/timer/req/create`` +prints something like this: + +.. code-block:: none + + Status = Ok, Name = Valid, IdVar = Set + + * Name = Valid, Id = Valid, Free = Yes + + Status = TooMany, Name = Invalid, IdVar = Nop + + * Name = Valid, Id = Valid, Free = No + + Status = InvAddr, Name = Invalid, IdVar = Nop + + * Name = Valid, Id = Null, Free = { Yes, No } + + Status = InvName, Name = Invalid, IdVar = Nop + + * Name = Invalid, Id = { Valid, Null }, Free = { Yes, No } + +The view above yields for each variation of post-condition states the list of +associated pre-condition state variations. + +Generate Files from Specification Items +--------------------------------------- + +The ``./spec2modules.py`` script generates program and documentation files in +:file:`modules/rtems` and :file:`modules/rtems-docs` using the specification +items as input. The script should be invoked whenever a specification item was +modified. After running the script, go into the subdirectories and create +corresponding patch sets. For these patch sets, the normal patch review +process applies, see *Support and Contributing* chapter of the *RTEMS User +Manual*. + Application Configuration Options --------------------------------- The application configuration options and groups are maintained by -specification items in the directory :file:`spec/if/acfg`. Application +specification items in the directory :file:`spec/acfg/if`. Application configuration options are grouped by :ref:`SpecTypeApplicationConfigurationGroupItemType` items which should be -stored in files using the :file:`spec/if/acfg/group-*.yml` pattern. Each +stored in files using the :file:`spec/acfg/if/group-*.yml` pattern. Each application configuration option shall link to exactly one group item with the -:ref:`SpecTypeApplicationConfigurationGroupMemberLinkRole`. There are four +:ref:`SpecTypeInterfaceGroupMembershipLinkRole`. There are four application option item types available which cover all existing options: * The *feature enable options* let the application enable a feature option. If @@ -83,9 +177,9 @@ restricted Sphinx formatting. Emphasis via one asterisk ("*"), strong emphasis via two asterisk ("**"), code samples via blockquotes ("``"), code blocks (".. code-block:: c") and lists are allowed. References to interface items are also allowed, for example "${appl-needs-clock-driver:/name}" and -"${../rtems/tasks/create:/name}". References to other parts of the -documentation are possible, however, they are currently provided by hard-coded -tables in :file:`rtemsspec/applconfig.py`. +"${/rtems/task/if/create:/name}". References to other parts of the +documentation are possible, however, they have to be provided by +:file:`spec:/doc/if/*` items. Modify an Existing Group ^^^^^^^^^^^^^^^^^^^^^^^^ @@ -95,9 +189,9 @@ file. For example: .. code-block:: none - $ grep -rl "name: General System Configuration" spec/if/acfg - spec/if/acfg/group-general.yml - $ vi spec/if/acfg/group-general.yml + $ grep -rl "name: General System Configuration" spec/acfg/if + spec/acfg/if/group-general.yml + $ vi spec/acfg/if/group-general.yml Modify an Existing Option ^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -107,20 +201,20 @@ specification item file. For example: .. code-block:: none - $ grep -rl CONFIGURE_APPLICATION_NEEDS_CLOCK_DRIVER spec/if/acfg - spec/if/acfg/appl-needs-clock-driver.yml - $ vi spec/if/acfg/appl-needs-clock-driver.yml + $ grep -rl CONFIGURE_APPLICATION_NEEDS_CLOCK_DRIVER spec/acfg/if + spec/acfg/if/appl-needs-clock-driver.yml + $ vi spec/acfg/if/appl-needs-clock-driver.yml Add a New Group ^^^^^^^^^^^^^^^ Let ``new`` be the UID name part of the new group. Create the file -:file:`spec/if/acfg/group-new.yml` and provide all attributes for an +:file:`spec/acfg/if/group-new.yml` and provide all attributes for an :ref:`SpecTypeApplicationConfigurationGroupItemType` item. For example: .. code-block:: none - $ vi spec/if/acfg/group-new.yml + $ vi spec/acfg/if/group-new.yml Add a New Option ^^^^^^^^^^^^^^^^ @@ -132,7 +226,7 @@ example: .. code-block:: none - $ vi spec/if/acfg/my-new-option.yml + $ vi spec/acfg/if/my-new-option.yml Generate Content after Changes ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -144,7 +238,7 @@ make sure the Git submodules are up-to-date. .. code-block:: none - $ ./spec2dmodules.py + $ ./spec2modules.py The script modifies or creates source files in :file:`modules/rtems` and :file:`modules/rtems-docs`. Create patch sets for these changes just as if @@ -169,7 +263,7 @@ specification. SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true glossary-type: term links: @@ -206,23 +300,25 @@ Interface Specification Specify an API Header File ^^^^^^^^^^^^^^^^^^^^^^^^^^ -The RTEMS :term:`API` header files are specified under ``spec:/if/rtems/*``. +The RTEMS :term:`API` header files are specified under ``spec:/rtems/*/if``. Create a subdirectory with a corresponding name for the API, for example in -:file:`spec/if/rtems/foo` for the `foo` API. In this new subdirectory place an +:file:`spec/rtems/foo/if` for the `foo` API. In this new subdirectory place an :ref:`SpecTypeInterfaceHeaderFileItemType` item named :file:`header.yml` -(:file:`spec/if/rtems/foo/header.yml`) and populate it with the required +(:file:`spec/rtems/foo/if/header.yml`) and populate it with the required attributes. .. code-block:: yaml SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true interface-type: header-file links: - role: interface-placement - uid: /if/domains/api + uid: /if/domain + - role: interface-ingroup + uid: ../req/group path: rtems/rtems/foo.h prefix: cpukit/include type: interface @@ -233,7 +329,7 @@ Specify an API Element Figure out the corresponding header file item. If it does not exist, see :ref:`ReqEngAddAPIHeaderFile`. Place a specialization of an :ref:`SpecTypeInterfaceItemType` item into the directory of the header file -item, for example :file:`spec/if/rtems/foo/bar.yml` for the :c:func:`bar` +item, for example :file:`spec/rtems/foo/if/bar.yml` for the :c:func:`bar` function. Add the required attributes for the new interface item. Do not hard code interface names which are used to define the new interface. Use ``${uid-of-interface-item:/name}`` instead. If the referenced interface is @@ -250,7 +346,7 @@ an :ref:`SpecTypeInterfaceForwardDeclarationItemType` item. SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause brief: Tries to create a magic object and returns it. copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG definition: default: body: null @@ -277,7 +373,7 @@ an :ref:`SpecTypeInterfaceForwardDeclarationItemType` item. return: Otherwise, the magic object is returned. return-values: - description: The caller did not have enough magic power. - value: ${/if/c/null} + value: ${/c/if/null} type: interface Requirements Depending on Build Configuration Options @@ -514,7 +610,7 @@ presentation we use a structured order. SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2021 embedded brains GmbH & Co. KG enabled-by: true functional-type: action rationale: null @@ -1030,3 +1126,88 @@ the following post-condition states. Objects referenced by the ${../if/directive:/params[0]/name} parameter in past calls to ${../if/directive:/name} shall not be accessed by the ${../if/directive:/name} call. + +Validation Test Guidelines +-------------------------- + +The validation test cases, test runners, and test suites are generated by the +``./spec2modules.py`` script from specification items. For the placement and +naming of the generated sources use the following rules: + +* Place architecture-specific validation test sources and programs into the + ``testsuites/validation/cpu`` directory. + +* Place BSP-specific validation test sources and programs into the + ``testsuites/validation/bsps`` directory. + +* Place all other validation test sources and programs into the + ``testsuites/validation`` directory. + +* Place architecture-specific unit test sources and programs into the + ``testsuites/unit/cpu`` directory. + +* Place BSP-specific unit test sources and programs into the + ``testsuites/unit/bsps`` directory. + +* Place all other unit test sources and programs into the + ``testsuites/unit`` directory. + +* Use dashes (``-``) to separate parts of a file name. Use only dashes, the + digits ``0`` to ``9``, and the lower case characters ``a`` to ``z`` for file + names. In particular, do not use underscores (``_``). + +* The parts of a file name shall be separated by dashes and ordered from most + general (left) to more specific (right), for example ``tc-task-construct.c``. + +* The file names associated with tests shall be unique within the system since + the test framework prints out only the base file names. + +* Use the prefix ``tc-`` for test case files. + +* Use the prefix ``tr-`` for test runner files. + +* Use the prefix ``ts-`` for test suite files. + +* Use the prefix ``tx-`` for test extension files (test support code). + +* Tests for fatal errors shall have ``fatal`` as the most general file part, + for example ``ts-fatal-too-large-tls-size.c``. + +* Validation test suites shall have ``validation`` as the most general file + part, for example ``ts-validation-no-clock-0.c``. + +* Unit test suites shall have ``unit`` as the most general file part, for + example ``ts-unit-no-clock-0.c``. + +* Architecture-specific files shall have the architecture name as a file part, + for example ``ts-fatal-sparc-leon3-clock-initialization.c``. + +* BSP-specific files shall have the BSP family or variant name as a file part, + for example ``tc-sparc-gr712rc.c``. + +* Architecture-specific or BSP-specific tests shall use the ``enabled-by`` + attribute of the associated specification item to make the build item + conditional, for example: + + .. code-block:: yaml + + ... + build-type: objects + enabled-by: arm + type: build + ... + + .. code-block:: yaml + + ... + build-type: test-program + enabled-by: bsps/sparc/leon3 + type: build + ... + +Verify the Specification Items +------------------------------ + +The ``./specverify.py`` script verifies that the specification items have the +format documented in :ref:`ReqEngSpecificationItems`. To some extent the +values of attributes are verified as well. diff --git a/eng/req/index.rst b/eng/req/index.rst index f0d11b3..524835d 100644 --- a/eng/req/index.rst +++ b/eng/req/index.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2020 embedded brains GmbH & Co. KG .. |E40| replace:: ECSS-E-ST-40C diff --git a/eng/req/items.rst b/eng/req/items.rst index db39547..286e998 100644 --- a/eng/req/items.rst +++ b/eng/req/items.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2021 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2023 embedded brains GmbH & Co. KG .. This file is part of the RTEMS quality process and was automatically .. generated. If you find something that needs to be fixed or @@ -77,8 +77,6 @@ The specification item types have the following hierarchy: * :ref:`SpecTypeInterfaceCompoundItemType` - * :ref:`SpecTypeInterfaceContainerItemType` - * :ref:`SpecTypeInterfaceDefineItemType` * :ref:`SpecTypeInterfaceDomainItemType` @@ -89,20 +87,24 @@ The specification item types have the following hierarchy: * :ref:`SpecTypeInterfaceForwardDeclarationItemType` - * :ref:`SpecTypeInterfaceFunctionItemType` + * :ref:`SpecTypeInterfaceFunctionOrMacroItemType` * :ref:`SpecTypeInterfaceGroupItemType` * :ref:`SpecTypeInterfaceHeaderFileItemType` - * :ref:`SpecTypeInterfaceMacroItemType` - * :ref:`SpecTypeInterfaceTypedefItemType` + * :ref:`SpecTypeInterfaceUnspecifiedHeaderFileItemType` + * :ref:`SpecTypeInterfaceUnspecifiedItemType` * :ref:`SpecTypeInterfaceVariableItemType` + * :ref:`SpecTypeRegisterBlockItemType` + + * :ref:`SpecTypeProxyItemTypes` + * :ref:`SpecTypeRequirementItemType` * :ref:`SpecTypeFunctionalRequirementItemType` @@ -115,12 +117,18 @@ The specification item types have the following hierarchy: * :ref:`SpecTypeDesignGroupRequirementItemType` + * :ref:`SpecTypeDesignTargetItemType` + * :ref:`SpecTypeGenericNonFunctionalRequirementItemType` + * :ref:`SpecTypeRuntimeMeasurementEnvironmentItemType` + * :ref:`SpecTypeRuntimePerformanceRequirementItemType` * :ref:`SpecTypeRequirementValidationItemType` + * :ref:`SpecTypeRequirementValidationMethod` + * :ref:`SpecTypeRuntimeMeasurementTestItemType` * :ref:`SpecTypeSpecificationItemType` @@ -191,6 +199,8 @@ This type is refined by the following types: * :ref:`SpecTypeInterfaceItemType` +* :ref:`SpecTypeProxyItemTypes` + * :ref:`SpecTypeRequirementItemType` * :ref:`SpecTypeRequirementValidationItemType` @@ -284,6 +294,10 @@ cppflags The attribute value shall be a list. Each list element shall be a :ref:`SpecTypeBuildCPreprocessorOption`. +cxxflags + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeBuildCXXCompilerOption`. + includes The attribute value shall be a list. Each list element shall be a :ref:`SpecTypeBuildIncludePath`. @@ -325,8 +339,9 @@ Please have a look at the following example: build-type: ada-test-program cflags: [] copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG cppflags: [] + cxxflags: [] enabled-by: true includes: [] ldflags: [] @@ -391,7 +406,7 @@ Please have a look at the following example: build-type: bsp cflags: [] copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG cppflags: [] enabled-by: true family: mybsp @@ -461,7 +476,7 @@ Please have a look at the following example: Name: ${ARCH}-rtems${__RTEMS_MAJOR__}-${BSP_NAME} # ... copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true install-path: ${PREFIX}/lib/pkgconfig links: [] @@ -509,6 +524,18 @@ referenced build items. The ``includes``, ``ldflags``, ``objects``, and attributes of the build group. All explicit attributes shall be specified. The explicit attributes for this type are: +cflags + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeBuildCCompilerOption`. + +cppflags + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeBuildCPreprocessorOption`. + +cxxflags + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeBuildCXXCompilerOption`. + includes The attribute value shall be a list. Each list element shall be a :ref:`SpecTypeBuildIncludePath`. @@ -536,8 +563,11 @@ Please have a look at the following example: SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause build-type: group + cflags: [] copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG + cppflags: [] + cxxflags: [] enabled-by: - BUILD_TESTS - BUILD_SAMPLES @@ -607,7 +637,7 @@ Please have a look at the following example: cflags: - -Wno-pointer-sign copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG cppflags: [] cxxflags: [] enabled-by: true @@ -631,8 +661,12 @@ Build Objects Item Type This type refines the :ref:`SpecTypeBuildItemType` through the ``build-type`` attribute if the value is ``objects``. This set of attributes specifies a set -of object files used to build static libraries or test programs. All explicit -attributes shall be specified. The explicit attributes for this type are: +of object files used to build static libraries or test programs. Objects Items +must not be included on multiple paths through the build dependency graph with +identical build options. Violating this can cause race conditions in the build +system due to duplicate installs and multiple instances of build tasks. All +explicit attributes shall be specified. The explicit attributes for this type +are: cflags The attribute value shall be a list. Each list element shall be a @@ -666,7 +700,7 @@ Please have a look at the following example: build-type: objects cflags: [] copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG cppflags: [] cxxflags: [] enabled-by: true @@ -696,8 +730,6 @@ option. The following explicit attributes are mandatory: * ``default`` -* ``default-by-variant`` - * ``description`` The explicit attributes for this type are: @@ -711,16 +743,11 @@ actions actions are carried out during the configure command execution. default - The attribute value shall be a :ref:`SpecTypeBuildOptionValue`. It shall be - the default value of the option if no variant-specific default value is - specified. Use ``null`` to specify that no default value exits. The - variant-specific default values may be specified by the - ``default-by-variant`` attribute. - -default-by-variant The attribute value shall be a list. Each list element shall be a - :ref:`SpecTypeBuildOptionDefaultByVariant`. The list is processed from top - to bottom. If a matching variant is found, then the processing stops. + :ref:`SpecTypeBuildOptionDefaultValue`. It shall be the list of default + values of the option. When a default value is needed, the first value on + the list which is enabled according to the enabled set is choosen. If no + value is enabled, then the default value is ``null``. description The attribute value shall be an optional string. It shall be the @@ -745,16 +772,17 @@ Please have a look at the following example: - define: null build-type: option copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) - default: 115200 - default-by-variant: - - value: 9600 - variants: + - Copyright (C) 2020, 2022 embedded brains GmbH & Co. KG + default: + - enabled-by: + - bsps/powerpc/motorola_powerpc - m68k/m5484FireEngine - powerpc/hsc_cm01 - - value: 19200 - variants: - - m68k/COBRA5475 + value: 9600 + - enabled-by: m68k/COBRA5475 + value: 19200 + - enabled-by: true + value: 115200 description: | Default baud for console and other serial devices. enabled-by: true @@ -841,6 +869,9 @@ stlib The attribute value shall be a list. Each list element shall be a :ref:`SpecTypeBuildLinkStaticLibraryDirective`. +target + The attribute value shall be a :ref:`SpecTypeBuildTarget`. + use-after The attribute value shall be a list. Each list element shall be a :ref:`SpecTypeBuildUseAfterDirective`. @@ -856,7 +887,7 @@ Please have a look at the following example: SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause build-type: script copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG default: null default-by-variant: [] do-build: | @@ -916,7 +947,7 @@ Please have a look at the following example: asflags: [] build-type: start-file copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG cppflags: [] enabled-by: true includes: [] @@ -992,7 +1023,7 @@ Please have a look at the following example: build-type: test-program cflags: [] copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG cppflags: [] cxxflags: [] enabled-by: true @@ -1113,8 +1144,6 @@ This type is refined by the following types: * :ref:`SpecTypeInterfaceCompoundItemType` -* :ref:`SpecTypeInterfaceContainerItemType` - * :ref:`SpecTypeInterfaceDefineItemType` * :ref:`SpecTypeInterfaceDomainItemType` @@ -1125,20 +1154,22 @@ This type is refined by the following types: * :ref:`SpecTypeInterfaceForwardDeclarationItemType` -* :ref:`SpecTypeInterfaceFunctionItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` * :ref:`SpecTypeInterfaceGroupItemType` * :ref:`SpecTypeInterfaceHeaderFileItemType` -* :ref:`SpecTypeInterfaceMacroItemType` - * :ref:`SpecTypeInterfaceTypedefItemType` +* :ref:`SpecTypeInterfaceUnspecifiedHeaderFileItemType` + * :ref:`SpecTypeInterfaceUnspecifiedItemType` * :ref:`SpecTypeInterfaceVariableItemType` +* :ref:`SpecTypeRegisterBlockItemType` + .. _SpecTypeApplicationConfigurationGroupItemType: Application Configuration Group Item Type @@ -1276,18 +1307,6 @@ name notes The attribute value shall be an :ref:`SpecTypeInterfaceNotes`. -.. _SpecTypeInterfaceContainerItemType: - -Interface Container Item Type -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -This type refines the :ref:`SpecTypeInterfaceItemType` through the -``interface-type`` attribute if the value is ``container``. Items of this type -specify an interface container. The item shall have exactly one link with the -:ref:`SpecTypeInterfacePlacementLinkRole` to an -:ref:`SpecTypeInterfaceDomainItemType` item. This link defines the interface -domain of the container. - .. _SpecTypeInterfaceDefineItemType: Interface Define Item Type @@ -1321,9 +1340,7 @@ Interface Domain Item Type This type refines the :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if the value is ``domain``. This set of attributes -specifies an interface domain. Items of the types -:ref:`SpecTypeInterfaceContainerItemType` and -:ref:`SpecTypeInterfaceHeaderFileItemType` are placed into domains through +specifies an interface domain. Interface items are placed into domains through links with the :ref:`SpecTypeInterfacePlacementLinkRole`. All explicit attributes shall be specified. The explicit attributes for this type are: @@ -1399,29 +1416,35 @@ with the :ref:`SpecTypeInterfaceTargetLinkRole` to an :ref:`SpecTypeInterfaceCompoundItemType` item. This link defines the type declared by the forward declaration. -.. _SpecTypeInterfaceFunctionItemType: +.. _SpecTypeInterfaceFunctionOrMacroItemType: -Interface Function Item Type -^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Interface Function or Macro Item Type +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -This type refines the :ref:`SpecTypeInterfaceItemType` through the -``interface-type`` attribute if the value is ``function``. This set of -attributes specifies a function. All explicit attributes shall be specified. -The explicit attributes for this type are: +This type refines the following types: + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``function`` + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``macro`` + +This set of attributes specifies a function or a macro. All explicit attributes +shall be specified. The explicit attributes for this type are: brief The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. definition The attribute value shall be an - :ref:`SpecTypeInterfaceFunctionDefinitionDirective`. + :ref:`SpecTypeInterfaceFunctionOrMacroDefinitionDirective`. description The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. name - The attribute value shall be a string. It shall be the name of the - function. + The attribute value shall be a string. It shall be the name of the function + or macro. notes The attribute value shall be an :ref:`SpecTypeInterfaceNotes`. @@ -1485,15 +1508,15 @@ prefix path to the header file in the interface domain. For example :file:`cpukit/include`. -.. _SpecTypeInterfaceMacroItemType: +.. _SpecTypeInterfaceTypedefItemType: -Interface Macro Item Type -^^^^^^^^^^^^^^^^^^^^^^^^^ +Interface Typedef Item Type +^^^^^^^^^^^^^^^^^^^^^^^^^^^ This type refines the :ref:`SpecTypeInterfaceItemType` through the -``interface-type`` attribute if the value is ``macro``. This set of attributes -specifies a macro. All explicit attributes shall be specified. The explicit -attributes for this type are: +``interface-type`` attribute if the value is ``typedef``. This set of +attributes specifies a typedef. All explicit attributes shall be specified. The +explicit attributes for this type are: brief The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. @@ -1506,7 +1529,7 @@ description The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. name - The attribute value shall be a string. It shall be the name of the macro. + The attribute value shall be a string. It shall be the name of the typedef. notes The attribute value shall be an :ref:`SpecTypeInterfaceNotes`. @@ -1518,31 +1541,23 @@ params return The attribute value shall be an :ref:`SpecTypeInterfaceReturnDirective`. -.. _SpecTypeInterfaceTypedefItemType: +.. _SpecTypeInterfaceUnspecifiedHeaderFileItemType: -Interface Typedef Item Type -^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Interface Unspecified Header File Item Type +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This type refines the :ref:`SpecTypeInterfaceItemType` through the -``interface-type`` attribute if the value is ``typedef``. This set of -attributes specifies a typedef. All explicit attributes shall be specified. The -explicit attributes for this type are: - -brief - The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. - -definition - The attribute value shall be an - :ref:`SpecTypeInterfaceDefinitionDirective`. - -description - The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. +``interface-type`` attribute if the value is ``unspecified-header-file``. This +set of attributes specifies an unspecified header file. All explicit attributes +shall be specified. The explicit attributes for this type are: -name - The attribute value shall be a string. It shall be the name of the typedef. +path + The attribute value shall be a string. It shall be the path used to include + the header file. For example :file:`rtems/confdefs.h`. -notes - The attribute value shall be an :ref:`SpecTypeInterfaceNotes`. +references + The attribute value shall be a list. Each list element shall be an + :ref:`SpecTypeExternalReference`. .. _SpecTypeInterfaceUnspecifiedItemType: @@ -1552,10 +1567,13 @@ Interface Unspecified Item Type This type refines the following types: * :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if - the value is ``unspecified`` + the value is ``unspecified-define`` * :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if - the value is ``unspecified-define`` + the value is ``unspecified-enum`` + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``unspecified-enumerator`` * :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if the value is ``unspecified-function`` @@ -1564,7 +1582,19 @@ This type refines the following types: the value is ``unspecified-group`` * :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if - the value is ``unspecified-type`` + the value is ``unspecified-macro`` + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``unspecified-object`` + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``unspecified-struct`` + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``unspecified-typedef`` + +* :ref:`SpecTypeInterfaceItemType` through the ``interface-type`` attribute if + the value is ``unspecified-union`` This set of attributes specifies an unspecified interface. All explicit attributes shall be specified. The explicit attributes for this type are: @@ -1574,7 +1604,8 @@ name unspecified interface. references - The attribute value shall be an :ref:`SpecTypeInterfaceReferencesSet`. + The attribute value shall be a list. Each list element shall be an + :ref:`SpecTypeExternalReference`. .. _SpecTypeInterfaceVariableItemType: @@ -1603,6 +1634,78 @@ name notes The attribute value shall be an :ref:`SpecTypeInterfaceNotes`. +.. _SpecTypeRegisterBlockItemType: + +Register Block Item Type +^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeInterfaceItemType` through the +``interface-type`` attribute if the value is ``register-block``. This set of +attributes specifies a register block. A register block may be used to specify +the interface of devices. Register blocks consist of register block members +specified by the ``definition`` attribute. Register block members are either +instances of registers specified by the ``registers`` attribute or instances of +other register blocks specified by links with the +:ref:`SpecTypeRegisterBlockIncludeRole`. Registers consists of bit fields (see +:ref:`SpecTypeRegisterBitsDefinition`. The register block members are placed +into the address space of the device relative to the base address of the +register block. Register member offsets and the register block size are +specified in units of the address space granule. All explicit attributes shall +be specified. The explicit attributes for this type are: + +brief + The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. + +definition + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterBlockMemberDefinitionDirective`. + +description + The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. + +identifier + The attribute value shall be an :ref:`SpecTypeInterfaceGroupIdentifier`. + +name + The attribute value shall be a string. It shall be the name of the register + block. + +notes + The attribute value shall be an :ref:`SpecTypeInterfaceNotes`. + +register-block-group + The attribute value shall be a string. It shall be the name of the + interface group defined for the register block. For the group identifier + see the ``identifier`` attribute. + +register-block-size + The attribute value shall be an :ref:`SpecTypeOptionalInteger`. If the + value is present, then it shall be the size of the register block in units + of the address space granule. + +register-prefix + The attribute value shall be an optional string. If the value is present, + then it will be used to prefix register bit field names, otherwise the + value of the ``name`` attribute will be used. + +registers + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterDefinition`. + +.. _SpecTypeProxyItemTypes: + +Proxy Item Types +^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeRootItemType` through the ``type`` +attribute if the value is ``proxy``. Items of similar characteristics may link +to a proxy item through links with the :ref:`SpecTypeProxyMemberLinkRole`. A +proxy item resolves to the first member item which is enabled. Proxies may be +used to provide an interface with a common name and implementations which +depend on configuration options. For example, in one configuration a constant +could be a compile time constant and in another configuration it could be a +read-only object. + .. _SpecTypeRequirementItemType: Requirement Item Type @@ -1618,8 +1721,8 @@ rationale then it shall state the rationale or justification of the requirement. references - The attribute value shall be a list. Each list element shall be a - :ref:`SpecTypeRequirementReference`. + The attribute value shall be a list. Each list element shall be an + :ref:`SpecTypeExternalReference`. requirement-type The attribute value shall be a :ref:`SpecTypeName`. It shall be the @@ -1641,7 +1744,7 @@ Please have a look at the following example: SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true functional-type: capability links: [] @@ -1787,7 +1890,7 @@ Please have a look at the following example: SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true functional-type: action links: [] @@ -1923,6 +2026,9 @@ This type refines the following types: attribute if the value is ``function`` * :ref:`SpecTypeFunctionalRequirementItemType` through the ``functional-type`` + attribute if the value is ``interface-define-not-defined`` + +* :ref:`SpecTypeFunctionalRequirementItemType` through the ``functional-type`` attribute if the value is ``operational`` * :ref:`SpecTypeFunctionalRequirementItemType` through the ``functional-type`` @@ -1949,8 +2055,12 @@ This type is refined by the following types: * :ref:`SpecTypeDesignGroupRequirementItemType` +* :ref:`SpecTypeDesignTargetItemType` + * :ref:`SpecTypeGenericNonFunctionalRequirementItemType` +* :ref:`SpecTypeRuntimeMeasurementEnvironmentItemType` + * :ref:`SpecTypeRuntimePerformanceRequirementItemType` .. _SpecTypeDesignGroupRequirementItemType: @@ -1969,7 +2079,29 @@ software source code. All explicit attributes shall be specified. The explicit attributes for this type are: identifier - The attribute value shall be an :ref:`SpecTypeInterfaceGroupIdentifier`. + The attribute value shall be a + :ref:`SpecTypeRequirementDesignGroupIdentifier`. + +.. _SpecTypeDesignTargetItemType: + +Design Target Item Type +^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeNonFunctionalRequirementItemType` through +the ``non-functional-type`` attribute if the value is ``design-target``. This +set of attributes specifies a design :term:`target`. All explicit attributes +shall be specified. The explicit attributes for this type are: + +brief + The attribute value shall be an optional string. If the value is present, + then it shall briefly describe the target. + +description + The attribute value shall be an optional string. If the value is present, + then it shall thoroughly describe the target. + +name + The attribute value shall be a string. It shall be the target name. .. _SpecTypeGenericNonFunctionalRequirementItemType: @@ -2003,6 +2135,10 @@ This type refines the following types: ``non-functional-type`` attribute if the value is ``performance`` * :ref:`SpecTypeNonFunctionalRequirementItemType` through the + ``non-functional-type`` attribute if the value is + ``performance-runtime-limits`` + +* :ref:`SpecTypeNonFunctionalRequirementItemType` through the ``non-functional-type`` attribute if the value is ``portability`` * :ref:`SpecTypeNonFunctionalRequirementItemType` through the @@ -2020,6 +2156,22 @@ This type refines the following types: Items of this type state a non-functional requirement with the non-functional type defined by the specification type refinement. +.. _SpecTypeRuntimeMeasurementEnvironmentItemType: + +Runtime Measurement Environment Item Type +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeNonFunctionalRequirementItemType` through +the ``non-functional-type`` attribute if the value is +``performance-runtime-environment``. This set of attributes specifies a runtime +measurement environment. All explicit attributes shall be specified. The +explicit attributes for this type are: + +name + The attribute value shall be a string. It shall be the runtime measurement + environment name. See also + :ref:`SpecTypeRuntimeMeasurementEnvironmentName`. + .. _SpecTypeRuntimePerformanceRequirementItemType: Runtime Performance Requirement Item Type @@ -2068,9 +2220,6 @@ the requirement, the validation test code to execute a measure runtime request is specified. All explicit attributes shall be specified. The explicit attributes for this type are: -limits - The attribute value shall be a :ref:`SpecTypeRuntimePerformanceLimitTable`. - params The attribute value shall be a :ref:`SpecTypeRuntimePerformanceParameterSet`. @@ -2106,34 +2255,11 @@ Please have a look at the following example: SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true links: - role: runtime-measurement-request - uid: ../val/performance - limits: - sparc/leon3: - DirtyCache: - max-upper-bound: 0.000005 - mean-upper-bound: 0.000005 - FullCache: - max-upper-bound: 0.000005 - mean-upper-bound: 0.000005 - HotCache: - max-upper-bound: 0.000005 - mean-upper-bound: 0.000005 - Load/1: - max-upper-bound: 0.00001 - mean-upper-bound: 0.00001 - Load/2: - max-upper-bound: 0.00001 - mean-upper-bound: 0.00001 - Load/3: - max-upper-bound: 0.00001 - mean-upper-bound: 0.00001 - Load/4: - max-upper-bound: 0.00001 - mean-upper-bound: 0.00001 + uid: ../val/perf params: {} rationale: null references: [] @@ -2160,11 +2286,11 @@ Please have a look at the following example: return tic == toc; description: null text: | - When a partition has exactly ${../val/performance:/params/buffer-count} free - buffers, the ${.:limit-kind} runtime of exactly - ${../val/performance:/params/sample-count} successful calls to + When a partition has exactly ${../val/perf:/params/buffer-count} free + buffers, the ${.:/limit-kind} runtime of exactly + ${../val/perf:/params/sample-count} successful calls to ${../if/get-buffer:/name} in the ${.:/environment} shall be - ${.:limit-condition}. + ${.:/limit-condition}. non-functional-type: performance-runtime requirement-type: non-functional type: requirement @@ -2182,8 +2308,13 @@ All explicit attributes shall be specified. The explicit attributes for this type are: method - The attribute value shall be a :ref:`SpecTypeRequirementValidationMethod`. - Validation by test is done through :ref:`SpecTypeTestCaseItemType` items. + The attribute value shall be a :ref:`SpecTypeName`. It shall specify the + requirement validation method (except validation by test). Validation by + test is done through :ref:`SpecTypeTestCaseItemType` items. + +references + The attribute value shall be a list. Each list element shall be an + :ref:`SpecTypeExternalReference`. text The attribute value shall be a string. It shall provide the validation @@ -2198,6 +2329,26 @@ text * *By review of design*: A rationale shall be provided to demonstrate how the requirement is satisfied implicitly by the software design. +This type is refined by the following types: + +* :ref:`SpecTypeRequirementValidationMethod` + +.. _SpecTypeRequirementValidationMethod: + +Requirement Validation Method +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the following types: + +* :ref:`SpecTypeRequirementValidationItemType` through the ``method`` attribute + if the value is ``by-analysis`` + +* :ref:`SpecTypeRequirementValidationItemType` through the ``method`` attribute + if the value is ``by-inspection`` + +* :ref:`SpecTypeRequirementValidationItemType` through the ``method`` attribute + if the value is ``by-review-of-design`` + .. _SpecTypeRuntimeMeasurementTestItemType: Runtime Measurement Test Item Type @@ -2303,7 +2454,7 @@ Please have a look at the following example: SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause copyrights: - - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) + - Copyright (C) 2020 embedded brains GmbH & Co. KG enabled-by: true links: - role: spec-member @@ -2447,10 +2598,16 @@ steps Test Suite Item Type ^^^^^^^^^^^^^^^^^^^^ -This type refines the :ref:`SpecTypeRootItemType` through the ``type`` -attribute if the value is ``test-suite``. This set of attributes specifies a -test suite. All explicit attributes shall be specified. The explicit attributes -for this type are: +This type refines the following types: + +* :ref:`SpecTypeRootItemType` through the ``type`` attribute if the value is + ``memory-benchmark`` + +* :ref:`SpecTypeRootItemType` through the ``type`` attribute if the value is + ``test-suite`` + +This set of attributes specifies a test suite. All explicit attributes shall be +specified. The explicit attributes for this type are: test-brief The attribute value shall be a string. It shall be the test suite brief @@ -2472,10 +2629,6 @@ test-local-includes The attribute value shall be a list of strings. It shall be a list of header files included via ``#include "..."``. -test-suite-name - The attribute value shall be a string. It shall be the name of the test - suite. - test-target The attribute value shall be a string. It shall be the path to the generated target test suite source file. @@ -2639,7 +2792,7 @@ Action Requirement Expression State Name The value shall be a string. It shall be the name of a state of the condition or ``N/A`` if the condition is not applicable. The value -* shall match with the regular expression "``^[A-Z][a-zA-Z0-9]+$``", +* shall match with the regular expression "``^[A-Z][a-zA-Z0-9]*$``", * or, shall be equal to "``N/A``". @@ -2661,7 +2814,7 @@ A value of this type shall be of one of the following variants: * The value may be a string. It shall be the name of a state of the condition or ``N/A`` if the condition is not applicable. The value - * shall match with the regular expression "``^[A-Z][a-zA-Z0-9]+$``", + * shall match with the regular expression "``^[A-Z][a-zA-Z0-9]*$``", * or, shall be equal to "``N/A``". @@ -2682,7 +2835,7 @@ the horizontal space is limited by the page width. The more conditions you have in an action requirement, the shorter the names should be. The name ``NA`` is reserved and indicates that a condition is not applicable. The value -* shall match with the regular expression "``^[A-Z][a-zA-Z0-9]+$``", +* shall match with the regular expression "``^[A-Z][a-zA-Z0-9]*$``", * and, shall be not equal to "``NA``". @@ -2796,7 +2949,7 @@ A value of this type shall be of one of the following variants: corresponding post-condition or ``N/A`` if the post-condition is not applicable. The value - * shall match with the regular expression "``^[A-Z][a-zA-Z0-9]+$``", + * shall match with the regular expression "``^[A-Z][a-zA-Z0-9]*$``", * or, shall be equal to "``N/A``". @@ -2826,7 +2979,7 @@ A value of this type shall be of one of the following variants: reason is given instead of a listing of post-condition states, then this transition is skipped and no test code runs for this transition. The value - * shall match with the regular expression "``^[A-Z][a-zA-Z0-9]+$``", + * shall match with the regular expression "``^[A-Z][a-zA-Z0-9]*$``", * and, shall be not equal to "``NA``". @@ -2883,15 +3036,6 @@ This type is used by the following types: * :ref:`SpecTypeActionRequirementTransition` -.. _SpecTypeApplicationConfigurationGroupMemberLinkRole: - -Application Configuration Group Member Link Role -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the -value is ``appl-config-group-member``. It defines the application configuration -group membership role of links. - .. _SpecTypeApplicationConfigurationOptionName: Application Configuration Option Name @@ -2956,6 +3100,8 @@ This type is used by the following types: * :ref:`SpecTypeBuildBSPItemType` +* :ref:`SpecTypeBuildGroupItemType` + * :ref:`SpecTypeBuildLibraryItemType` * :ref:`SpecTypeBuildObjectsItemType` @@ -2982,6 +3128,8 @@ This type is used by the following types: * :ref:`SpecTypeBuildBSPItemType` +* :ref:`SpecTypeBuildGroupItemType` + * :ref:`SpecTypeBuildLibraryItemType` * :ref:`SpecTypeBuildObjectsItemType` @@ -3004,6 +3152,10 @@ context. This type is used by the following types: +* :ref:`SpecTypeBuildAdaTestProgramItemType` + +* :ref:`SpecTypeBuildGroupItemType` + * :ref:`SpecTypeBuildLibraryItemType` * :ref:`SpecTypeBuildObjectsItemType` @@ -3014,6 +3166,20 @@ This type is used by the following types: * :ref:`SpecTypeBuildTestProgramItemType` +.. _SpecTypeBuildDependencyConditionalLinkRole: + +Build Dependency Conditional Link Role +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``build-dependency-conditional``. It defines the build dependency +conditional role of links. All explicit attributes shall be specified. The +explicit attributes for this type are: + +enabled-by + The attribute value shall be an :ref:`SpecTypeEnabledByExpression`. It + shall define under which conditions the build dependency is enabled. + .. _SpecTypeBuildDependencyLinkRole: Build Dependency Link Role @@ -3090,7 +3256,7 @@ Build Install Path A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. It shall be the installation path of a :ref:`SpecTypeBuildTarget`. @@ -3311,6 +3477,12 @@ get-string ``name`` attribute. If no such variable exists in the configuration file, then the default value is used. The value is converted to a string. +get-string-command-line + The attribute value shall be a string. The action gets the action value for + subsequent actions from the value of a command line option named by the + items ``name`` attribute. If no such command line option is present, then + the attribute value is used. The value is converted to a string. + script The attribute value shall be a string. The action executes the attribute value with the Python ``eval()`` function in the context of the script @@ -3387,22 +3559,20 @@ This type is used by the following types: * :ref:`SpecTypeBuildOptionAction` -.. _SpecTypeBuildOptionDefaultByVariant: +.. _SpecTypeBuildOptionDefaultValue: -Build Option Default by Variant -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Build Option Default Value +^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies build option default values by variant. All -explicit attributes shall be specified. The explicit attributes for this type -are: +This set of attributes specifies a build option default value. All explicit +attributes shall be specified. The explicit attributes for this type are: -value - The attribute value shall be a :ref:`SpecTypeBuildOptionValue`. It value - shall be the default value for the matching variants. +enabled-by + The attribute value shall be an :ref:`SpecTypeEnabledByExpression`. -variants - The attribute value shall be a list of strings. It shall be a list of - Python regular expression matching with the desired variants. +value + The attribute value shall be a :ref:`SpecTypeBuildOptionValue`. Its value + shall be the default value for the associated enabled-by expression. This type is used by the following types: @@ -3425,14 +3595,25 @@ This type is used by the following types: Build Option Set Test State Action ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies test states for a set of test programs. -Generic attributes may be specified. Each generic attribute key shall be a -:ref:`SpecTypeName`. Each generic attribute value shall be a -:ref:`SpecTypeBuildTestState`. The keys shall be test program names. The names -shall correspond to the name of a :ref:`SpecTypeBuildTestProgramItemType` or -:ref:`SpecTypeBuildAdaTestProgramItemType` item. Due to the processing order -of items, there is no way to check if the name specified by the attribute key -is valid. +This set of attributes specifies the test state for a set of test programs with +an optional reason. All explicit attributes shall be specified. The explicit +attributes for this type are: + +reason + The attribute value shall be an optional string. If the value is present, + then it shall be the reason for the test state definition. + +state + The attribute value shall be a :ref:`SpecTypeBuildTestState`. It shall be + the test state for the associated list of tests. + +tests + The attribute value shall be a list of strings. It shall be the list of + test program names associated with the test state. The names shall + correspond to the name of a :ref:`SpecTypeBuildTestProgramItemType` or + :ref:`SpecTypeBuildAdaTestProgramItemType` item. Due to the processing + order of items, there is no way to check if a specified test program name + is valid. This type is used by the following types: @@ -3451,7 +3632,7 @@ A value of this type shall be of one of the following variants: * The value may be a list. Each list element shall be a string. -* There may by be no value (null). +* There may be no value (null). * The value may be a string. @@ -3459,9 +3640,7 @@ This type is used by the following types: * :ref:`SpecTypeBuildOptionAction` -* :ref:`SpecTypeBuildOptionDefaultByVariant` - -* :ref:`SpecTypeBuildOptionItemType` +* :ref:`SpecTypeBuildOptionDefaultValue` .. _SpecTypeBuildSource: @@ -3504,6 +3683,8 @@ This type is used by the following types: * :ref:`SpecTypeBuildLibraryItemType` +* :ref:`SpecTypeBuildScriptItemType` + * :ref:`SpecTypeBuildStartFileItemType` * :ref:`SpecTypeBuildTestProgramItemType` @@ -3645,6 +3826,10 @@ This type is used by the following types: * :ref:`SpecTypeActionRequirementTransition` +* :ref:`SpecTypeBuildDependencyConditionalLinkRole` + +* :ref:`SpecTypeBuildOptionDefaultValue` + * :ref:`SpecTypeEnabledByExpression` * :ref:`SpecTypeInterfaceIncludeLinkRole` @@ -3660,6 +3845,111 @@ Please have a look at the following example: - RTEMS_NETWORKING - not: RTEMS_SMP +.. _SpecTypeExternalDocumentReference: + +External Document Reference +^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeExternalReference` through the ``type`` +attribute if the value is ``document``. It specifies a reference to a document. + +All explicit attributes shall be specified. The explicit attributes for this +type are: + +name + The attribute value shall be a string. It shall be the name of the + document. + +.. _SpecTypeExternalFileReference: + +External File Reference +^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeExternalReference` through the ``type`` +attribute if the value is ``file``. It specifies a reference to a file. + +All explicit attributes shall be specified. The explicit attributes for this +type are: + +hash + The attribute value shall be a :ref:`SpecTypeSHA256HashValue`. It shall be + the SHA256 hash value of the content of the referenced file. + +.. _SpecTypeExternalReference: + +External Reference +^^^^^^^^^^^^^^^^^^ + +This set of attributes specifies a reference to some object external to the +specification. All explicit attributes shall be specified. The explicit +attributes for this type are: + +identifier + The attribute value shall be a string. It shall be the type-specific + identifier of the referenced object. For *group* references use the Doxygen + group identifier. For *file* references use a file system path to the + file. + +type + The attribute value shall be a :ref:`SpecTypeName`. It shall be the type of + the referenced object. + +This type is refined by the following types: + +* :ref:`SpecTypeExternalDocumentReference` + +* :ref:`SpecTypeExternalFileReference` + +* :ref:`SpecTypeGenericExternalReference` + +This type is used by the following types: + +* :ref:`SpecTypeInterfaceUnspecifiedHeaderFileItemType` + +* :ref:`SpecTypeInterfaceUnspecifiedItemType` + +* :ref:`SpecTypeRequirementItemType` + +* :ref:`SpecTypeRequirementValidationItemType` + +.. _SpecTypeFunctionImplementationLinkRole: + +Function Implementation Link Role +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``function-implementation``. It defines the function implementation +role of links. It is used to indicate that a +:ref:`SpecTypeFunctionalRequirementItemType` item specifies parts of the +function. + +.. _SpecTypeGenericExternalReference: + +Generic External Reference +^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the following types: + +* :ref:`SpecTypeExternalReference` through the ``type`` attribute if the value + is ``define`` + +* :ref:`SpecTypeExternalReference` through the ``type`` attribute if the value + is ``function`` + +* :ref:`SpecTypeExternalReference` through the ``type`` attribute if the value + is ``group`` + +* :ref:`SpecTypeExternalReference` through the ``type`` attribute if the value + is ``macro`` + +* :ref:`SpecTypeExternalReference` through the ``type`` attribute if the value + is ``url`` + +* :ref:`SpecTypeExternalReference` through the ``type`` attribute if the value + is ``variable`` + +It specifies a reference to an object of the specified type. + .. _SpecTypeGlossaryMembershipLinkRole: Glossary Membership Link Role @@ -3692,7 +3982,7 @@ Interface Brief Description A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. It shall be the brief description of the interface. It should be a single sentence. The value shall not match with @@ -3710,18 +4000,22 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceEnumeratorItemType` -* :ref:`SpecTypeInterfaceFunctionItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` * :ref:`SpecTypeInterfaceGroupItemType` * :ref:`SpecTypeInterfaceHeaderFileItemType` -* :ref:`SpecTypeInterfaceMacroItemType` - * :ref:`SpecTypeInterfaceTypedefItemType` * :ref:`SpecTypeInterfaceVariableItemType` +* :ref:`SpecTypeRegisterBitsDefinition` + +* :ref:`SpecTypeRegisterBlockItemType` + +* :ref:`SpecTypeRegisterDefinition` + .. _SpecTypeInterfaceCompoundDefinitionKind: Interface Compound Definition Kind @@ -3786,23 +4080,27 @@ definition Interface Compound Member Definition ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies an interface compound member definition. All -explicit attributes shall be specified. The explicit attributes for this type -are: +A value of this type shall be of one of the following variants: -brief - The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. +* The value may be a set of attributes. This set of attributes specifies an + interface compound member definition. All explicit attributes shall be + specified. The explicit attributes for this type are: -description - The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. + brief + The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. -kind - The attribute value shall be a string. It shall be the interface compound - member kind. + description + The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. -name - The attribute value shall be a string. It shall be the interface compound - member name. + kind + The attribute value shall be a string. It shall be the interface compound + member kind. + + name + The attribute value shall be a string. It shall be the interface compound + member name. + +* There may be no value (null). This type is refined by the following types: @@ -3871,7 +4169,7 @@ Interface Definition A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. It shall be the definition. On the definition a context-sensitive substitution of item variables is performed. @@ -3906,8 +4204,6 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceEnumeratorItemType` -* :ref:`SpecTypeInterfaceMacroItemType` - * :ref:`SpecTypeInterfaceTypedefItemType` * :ref:`SpecTypeInterfaceVariableItemType` @@ -3941,7 +4237,7 @@ Interface Description A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. It shall be the description of the interface. The description should be short and concentrate on the average case. All special @@ -3963,12 +4259,10 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceEnumeratorItemType` -* :ref:`SpecTypeInterfaceFunctionItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` * :ref:`SpecTypeInterfaceGroupItemType` -* :ref:`SpecTypeInterfaceMacroItemType` - * :ref:`SpecTypeInterfaceParameter` * :ref:`SpecTypeInterfaceReturnValue` @@ -3977,6 +4271,12 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceVariableItemType` +* :ref:`SpecTypeRegisterBitsDefinition` + +* :ref:`SpecTypeRegisterBlockItemType` + +* :ref:`SpecTypeRegisterDefinition` + .. _SpecTypeInterfaceEnabledByExpression: Interface Enabled-By Expression @@ -4024,7 +4324,11 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceEnabledByExpression` -* :ref:`SpecTypeInterfaceFunctionDefinitionVariant` +* :ref:`SpecTypeInterfaceFunctionOrMacroDefinitionVariant` + +* :ref:`SpecTypeRegisterBitsDefinitionVariant` + +* :ref:`SpecTypeRegisterBlockMemberDefinitionVariant` .. _SpecTypeInterfaceEnumDefinitionKind: @@ -4054,79 +4358,98 @@ This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the value is ``interface-enumerator``. It defines the interface enumerator role of links. -.. _SpecTypeInterfaceFunctionDefinition: +.. _SpecTypeInterfaceFunctionLinkRole: -Interface Function Definition -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Interface Function Link Role +^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies a function definition. All explicit attributes -shall be specified. The explicit attributes for this type are: +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``interface-function``. It defines the interface function role of +links. It is used to indicate that a :ref:`SpecTypeActionRequirementItemType` +item specifies functional requirements of an +:ref:`SpecTypeInterfaceFunctionOrMacroItemType` item. -attributes - The attribute value shall be an optional string. If the value is present, - then it shall be the function attributes. On the attributes a - context-sensitive substitution of item variables is performed. A function - attribute is for example the indication that the function does not return - to the caller. +.. _SpecTypeInterfaceFunctionOrMacroDefinition: -body - The attribute value shall be an optional string. If the value is present, - then it shall be the definition of a static inline function. On the - function definition a context-sensitive substitution of item variables is - performed. If no value is present, then the function is declared as an - external function. +Interface Function or Macro Definition +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -params - The attribute value shall be a list of strings. It shall be the list of - parameter declarations of the function. On the function parameter - declarations a context-sensitive substitution of item variables is - performed. +A value of this type shall be of one of the following variants: -return - The attribute value shall be a string. It shall be the function return - type. On the return type a context-sensitive substitution of item - variables is performed. +* The value may be a set of attributes. This set of attributes specifies a + function definition. All explicit attributes shall be specified. The explicit + attributes for this type are: + + attributes + The attribute value shall be an optional string. If the value is present, + then it shall be the function attributes. On the attributes a + context-sensitive substitution of item variables is performed. A + function attribute is for example the indication that the function does + not return to the caller. + + body + The attribute value shall be an optional string. If the value is present, + then it shall be the definition of a static inline function. On the + function definition a context-sensitive substitution of item variables is + performed. If no value is present, then the function is declared as an + external function. + + params + The attribute value shall be a list of strings. It shall be the list of + parameter declarations of the function. On the function parameter + declarations a context-sensitive substitution of item variables is + performed. + + return + The attribute value shall be an optional string. If the value is present, + then it shall be the function return type. On the return type a + context-sensitive substitution of item variables is performed. + +* There may be no value (null). This type is used by the following types: -* :ref:`SpecTypeInterfaceFunctionDefinitionDirective` +* :ref:`SpecTypeInterfaceFunctionOrMacroDefinitionDirective` -* :ref:`SpecTypeInterfaceFunctionDefinitionVariant` +* :ref:`SpecTypeInterfaceFunctionOrMacroDefinitionVariant` -.. _SpecTypeInterfaceFunctionDefinitionDirective: +.. _SpecTypeInterfaceFunctionOrMacroDefinitionDirective: -Interface Function Definition Directive -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Interface Function or Macro Definition Directive +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies a function definition directive. All explicit -attributes shall be specified. The explicit attributes for this type are: +This set of attributes specifies a function or macro definition directive. All +explicit attributes shall be specified. The explicit attributes for this type +are: default - The attribute value shall be an :ref:`SpecTypeInterfaceFunctionDefinition`. - The default definition will be used if no variant-specific definition is - enabled. + The attribute value shall be an + :ref:`SpecTypeInterfaceFunctionOrMacroDefinition`. The default definition + will be used if no variant-specific definition is enabled. variants The attribute value shall be a list. Each list element shall be an - :ref:`SpecTypeInterfaceFunctionDefinitionVariant`. + :ref:`SpecTypeInterfaceFunctionOrMacroDefinitionVariant`. This type is used by the following types: -* :ref:`SpecTypeInterfaceFunctionItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` -.. _SpecTypeInterfaceFunctionDefinitionVariant: +.. _SpecTypeInterfaceFunctionOrMacroDefinitionVariant: -Interface Function Definition Variant -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Interface Function or Macro Definition Variant +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies a function definition variant. All explicit -attributes shall be specified. The explicit attributes for this type are: +This set of attributes specifies a function or macro definition variant. All +explicit attributes shall be specified. The explicit attributes for this type +are: definition - The attribute value shall be an :ref:`SpecTypeInterfaceFunctionDefinition`. - The definition will be used if the expression defined by the ``enabled-by`` - attribute evaluates to true. In generated header files, the expression is - evaluated by the C preprocessor. + The attribute value shall be an + :ref:`SpecTypeInterfaceFunctionOrMacroDefinition`. The definition will be + used if the expression defined by the ``enabled-by`` attribute evaluates to + true. In generated header files, the expression is evaluated by the C + preprocessor. enabled-by The attribute value shall be an @@ -4134,19 +4457,7 @@ enabled-by This type is used by the following types: -* :ref:`SpecTypeInterfaceFunctionDefinitionDirective` - -.. _SpecTypeInterfaceFunctionLinkRole: - -Interface Function Link Role -^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the -value is ``interface-function``. It defines the interface function role of -links. It is used to indicate that a :ref:`SpecTypeActionRequirementItemType` -item specifies functional requirements of an -:ref:`SpecTypeInterfaceFunctionItemType` or a -:ref:`SpecTypeInterfaceMacroItemType` item. +* :ref:`SpecTypeInterfaceFunctionOrMacroDefinitionDirective` .. _SpecTypeInterfaceGroupIdentifier: @@ -4158,10 +4469,10 @@ The value shall match with the regular expression "``^[A-Z][a-zA-Z0-9]*$``". This type is used by the following types: -* :ref:`SpecTypeDesignGroupRequirementItemType` - * :ref:`SpecTypeInterfaceGroupItemType` +* :ref:`SpecTypeRegisterBlockItemType` + .. _SpecTypeInterfaceGroupMembershipLinkRole: Interface Group Membership Link Role @@ -4171,6 +4482,18 @@ This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the value is ``interface-ingroup``. It defines the interface group membership role of links. +.. _SpecTypeInterfaceHiddenGroupMembershipLinkRole: + +Interface Hidden Group Membership Link Role +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``interface-ingroup-hidden``. It defines the interface hidden group +membership role of links. This role may be used to make an interface a group +member and hide this relationship in the documentation. An example is an +optimized macro implementation of a directive which has the same name as the +corresponding directive. + .. _SpecTypeInterfaceIncludeLinkRole: Interface Include Link Role @@ -4194,7 +4517,7 @@ Interface Notes A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. It shall be the notes for the interface. @@ -4208,14 +4531,14 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceEnumeratorItemType` -* :ref:`SpecTypeInterfaceFunctionItemType` - -* :ref:`SpecTypeInterfaceMacroItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` * :ref:`SpecTypeInterfaceTypedefItemType` * :ref:`SpecTypeInterfaceVariableItemType` +* :ref:`SpecTypeRegisterBlockItemType` + .. _SpecTypeInterfaceParameter: Interface Parameter @@ -4236,9 +4559,9 @@ name This type is used by the following types: -* :ref:`SpecTypeInterfaceFunctionItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` -* :ref:`SpecTypeInterfaceMacroItemType` +* :ref:`SpecTypeInterfaceTypedefItemType` .. _SpecTypeInterfaceParameterDirection: @@ -4247,7 +4570,7 @@ Interface Parameter Direction A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. It specifies the interface parameter direction. The value shall be an element of @@ -4274,41 +4597,32 @@ value is ``interface-placement``. It defines the interface placement role of links. It is used to indicate that an interface definition is placed into an interface container, for example a header file. -.. _SpecTypeInterfaceReferencesSet: - -Interface References Set -^^^^^^^^^^^^^^^^^^^^^^^^ - -This set of attributes defines references for the interface. Generic attributes -may be specified. Each generic attribute key shall be a :ref:`SpecTypeName`. -Each generic attribute value shall be a string. The key defines the reference -kind. The value shall be a kind-specific reference target. - -This type is used by the following types: - -* :ref:`SpecTypeInterfaceUnspecifiedItemType` - .. _SpecTypeInterfaceReturnDirective: Interface Return Directive ^^^^^^^^^^^^^^^^^^^^^^^^^^ -This set of attributes specifies an interface return. All explicit attributes -shall be specified. The explicit attributes for this type are: +A value of this type shall be of one of the following variants: -return - The attribute value shall be an optional string. It shall describe the - interface return for unspecified return values. +* The value may be a set of attributes. This set of attributes specifies an + interface return. All explicit attributes shall be specified. The explicit + attributes for this type are: -return-values - The attribute value shall be a list. Each list element shall be an - :ref:`SpecTypeInterfaceReturnValue`. + return + The attribute value shall be an optional string. It shall describe the + interface return for unspecified return values. + + return-values + The attribute value shall be a list. Each list element shall be an + :ref:`SpecTypeInterfaceReturnValue`. + +* There may be no value (null). This type is used by the following types: -* :ref:`SpecTypeInterfaceFunctionItemType` +* :ref:`SpecTypeInterfaceFunctionOrMacroItemType` -* :ref:`SpecTypeInterfaceMacroItemType` +* :ref:`SpecTypeInterfaceTypedefItemType` .. _SpecTypeInterfaceReturnValue: @@ -4358,12 +4672,14 @@ uid This type is refined by the following types: -* :ref:`SpecTypeApplicationConfigurationGroupMemberLinkRole` +* :ref:`SpecTypeBuildDependencyConditionalLinkRole` * :ref:`SpecTypeBuildDependencyLinkRole` * :ref:`SpecTypeConstraintLinkRole` +* :ref:`SpecTypeFunctionImplementationLinkRole` + * :ref:`SpecTypeGlossaryMembershipLinkRole` * :ref:`SpecTypeInterfaceEnumeratorLinkRole` @@ -4372,14 +4688,22 @@ This type is refined by the following types: * :ref:`SpecTypeInterfaceGroupMembershipLinkRole` +* :ref:`SpecTypeInterfaceHiddenGroupMembershipLinkRole` + * :ref:`SpecTypeInterfaceIncludeLinkRole` * :ref:`SpecTypeInterfacePlacementLinkRole` * :ref:`SpecTypeInterfaceTargetLinkRole` +* :ref:`SpecTypePerformanceRuntimeLimitsLinkRole` + * :ref:`SpecTypePlacementOrderLinkRole` +* :ref:`SpecTypeProxyMemberLinkRole` + +* :ref:`SpecTypeRegisterBlockIncludeRole` + * :ref:`SpecTypeRequirementRefinementLinkRole` * :ref:`SpecTypeRequirementValidationLinkRole` @@ -4414,7 +4738,7 @@ This type is used by the following types: * :ref:`SpecTypeBuildItemType` -* :ref:`SpecTypeBuildOptionSetTestStateAction` +* :ref:`SpecTypeExternalReference` * :ref:`SpecTypeFunctionalRequirementItemType` @@ -4422,14 +4746,16 @@ This type is used by the following types: * :ref:`SpecTypeInterfaceItemType` -* :ref:`SpecTypeInterfaceReferencesSet` - * :ref:`SpecTypeLink` * :ref:`SpecTypeNonFunctionalRequirementItemType` +* :ref:`SpecTypeRegisterDefinition` + * :ref:`SpecTypeRequirementItemType` +* :ref:`SpecTypeRequirementValidationItemType` + * :ref:`SpecTypeRootItemType` * :ref:`SpecTypeRuntimeMeasurementParameterSet` @@ -4448,6 +4774,32 @@ This type is used by the following types: * :ref:`SpecTypeSpecificationRefinementLinkRole` +.. _SpecTypeOptionalFloatingPointNumber: + +Optional Floating-Point Number +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +A value of this type shall be of one of the following variants: + +* The value may be a floating-point number. + +* There may be no value (null). + +.. _SpecTypeOptionalInteger: + +Optional Integer +^^^^^^^^^^^^^^^^ + +A value of this type shall be of one of the following variants: + +* The value may be an integer number. + +* There may be no value (null). + +This type is used by the following types: + +* :ref:`SpecTypeRegisterBlockItemType` + .. _SpecTypeOptionalString: Optional String @@ -4455,10 +4807,24 @@ Optional String A value of this type shall be of one of the following variants: -* There may by be no value (null). +* There may be no value (null). * The value may be a string. +.. _SpecTypePerformanceRuntimeLimitsLinkRole: + +Performance Runtime Limits Link Role +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``performance-runtime-limits``. It defines the performance runtime +limits role of links. All explicit attributes shall be specified. The explicit +attributes for this type are: + +limits + The attribute value shall be a + :ref:`SpecTypeRuntimeMeasurementEnvironmentTable`. + .. _SpecTypePlacementOrderLinkRole: Placement Order Link Role @@ -4469,49 +4835,267 @@ value is ``placement-order``. This link role defines the placement order of items in a container item (for example an interface function in a header file or a documentation section). -.. _SpecTypeRequirementReference: +.. _SpecTypeProxyMemberLinkRole: -Requirement Reference -^^^^^^^^^^^^^^^^^^^^^ +Proxy Member Link Role +^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``proxy-member``. It defines the proxy member role of links. Items +may use this role to link to :ref:`SpecTypeProxyItemTypes` items. + +.. _SpecTypeRegisterBitsDefinition: + +Register Bits Definition +^^^^^^^^^^^^^^^^^^^^^^^^ + +A value of this type shall be of one of the following variants: + +* The value may be a set of attributes. This set of attributes specifies a + register bit field. Single bits are bit fields with a width of one. All + explicit attributes shall be specified. The explicit attributes for this type + are: + + brief + The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. -This set of attributes specifies a requirement reference. All explicit + description + The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. + + name + The attribute value shall be a string. It shall be the name of the + register bit field. + + properties + The attribute value shall be a list of strings. It shall be the list of + bit field properties. Properties are for example if the bit field can be + read or written, or an access has side-effects such as clearing a status. + + start + The attribute value shall be an integer number. It shall be the start bit + of the bit field. Bit ``0`` is the least-significant bit. + + width + The attribute value shall be an integer number. It shall be the width in + bits of the bit field. + +* There may be no value (null). + +This type is used by the following types: + +* :ref:`SpecTypeRegisterBitsDefinitionDirective` + +* :ref:`SpecTypeRegisterBitsDefinitionVariant` + +.. _SpecTypeRegisterBitsDefinitionDirective: + +Register Bits Definition Directive +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This set of attributes specifies a register bits directive. All explicit attributes shall be specified. The explicit attributes for this type are: -identifier - The attribute value shall be a string. It shall be the type-specific - identifier of the reference target. For *group* references use the Doxygen - group identifier. +default + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterBitsDefinition`. The default definition will be used + if no variant-specific definition is enabled. -type - The attribute value shall be a :ref:`SpecTypeRequirementReferenceType`. +variants + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterBitsDefinitionVariant`. This type is used by the following types: -* :ref:`SpecTypeRequirementItemType` +* :ref:`SpecTypeRegisterDefinition` -.. _SpecTypeRequirementReferenceType: +.. _SpecTypeRegisterBitsDefinitionVariant: -Requirement Reference Type -^^^^^^^^^^^^^^^^^^^^^^^^^^ +Register Bits Definition Variant +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This set of attributes specifies a register bits variant. All explicit +attributes shall be specified. The explicit attributes for this type are: + +definition + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterBitsDefinition`. The definition will be used if the + expression defined by the ``enabled-by`` attribute evaluates to true. In + generated header files, the expression is evaluated by the C preprocessor. + +enabled-by + The attribute value shall be an + :ref:`SpecTypeInterfaceEnabledByExpression`. + +This type is used by the following types: + +* :ref:`SpecTypeRegisterBitsDefinitionDirective` + +.. _SpecTypeRegisterBlockIncludeRole: + +Register Block Include Role +^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the +value is ``register-block-include``. It defines the register block include role +of links. Links of this role are used to build register blocks using other +register blocks. All explicit attributes shall be specified. The explicit +attributes for this type are: + +name + The attribute value shall be a string. It shall be a name to identify the + included register block within the item. The name shall be unique within + the scope of the item links of this role and the + :ref:`SpecTypeRegisterList`. + +.. _SpecTypeRegisterBlockMemberDefinition: + +Register Block Member Definition +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +A value of this type shall be of one of the following variants: + +* The value may be a set of attributes. This set of attributes specifies a + register block member definition. All explicit attributes shall be specified. + The explicit attributes for this type are: + + count + The attribute value shall be an integer number. It shall be the count of + registers of the register block member. + + name + The attribute value shall be a :ref:`SpecTypeRegisterName`. + +* There may be no value (null). + +This type is used by the following types: + +* :ref:`SpecTypeRegisterBlockMemberDefinitionDirective` + +* :ref:`SpecTypeRegisterBlockMemberDefinitionVariant` + +.. _SpecTypeRegisterBlockMemberDefinitionDirective: + +Register Block Member Definition Directive +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This set of attributes specifies a register block member definition directive. +All explicit attributes shall be specified. The explicit attributes for this +type are: + +default + The attribute value shall be a + :ref:`SpecTypeRegisterBlockMemberDefinition`. The default definition will + be used if no variant-specific definition is enabled. + +offset + The attribute value shall be an integer number. It shall be the address of + the register block member relative to the base address of the register + block. + +variants + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterBlockMemberDefinitionVariant`. + +This type is used by the following types: + +* :ref:`SpecTypeRegisterBlockItemType` + +.. _SpecTypeRegisterBlockMemberDefinitionVariant: + +Register Block Member Definition Variant +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This set of attributes specifies a register block member definition variant. +All explicit attributes shall be specified. The explicit attributes for this +type are: + +definition + The attribute value shall be a + :ref:`SpecTypeRegisterBlockMemberDefinition`. The definition will be used + if the expression defined by the ``enabled-by`` attribute evaluates to + true. In generated header files, the expression is evaluated by the C + preprocessor. + +enabled-by + The attribute value shall be an + :ref:`SpecTypeInterfaceEnabledByExpression`. -The value shall be a string. It specifies the type of a requirement reference. -The value shall be an element of +This type is used by the following types: -* "``define``", +* :ref:`SpecTypeRegisterBlockMemberDefinitionDirective` -* "``file``", +.. _SpecTypeRegisterDefinition: -* "``function``", +Register Definition +^^^^^^^^^^^^^^^^^^^ + +This set of attributes specifies a register. All explicit attributes shall be +specified. The explicit attributes for this type are: -* "``group``", +bits + The attribute value shall be a list. Each list element shall be a + :ref:`SpecTypeRegisterBitsDefinitionDirective`. -* "``macro``", and +brief + The attribute value shall be an :ref:`SpecTypeInterfaceBriefDescription`. -* "``variable``". +description + The attribute value shall be an :ref:`SpecTypeInterfaceDescription`. + +name + The attribute value shall be a string. It shall be the name to identify the + register definition. The name shall be unique within the scope of the + :ref:`SpecTypeRegisterBlockIncludeRole` links of the item and the + :ref:`SpecTypeRegisterList`. + +width + The attribute value shall be an integer number. It shall be the width of + the register in bits. + +In addition to the explicit attributes, generic attributes may be specified. +Each generic attribute key shall be a :ref:`SpecTypeName`. The attribute value +may have any type. This type is used by the following types: -* :ref:`SpecTypeRequirementReference` +* :ref:`SpecTypeRegisterBlockItemType` + +.. _SpecTypeRegisterName: + +Register Name +^^^^^^^^^^^^^ + +The value shall be a string. The name consists either of an identifier, or an +identifier and an alias. The identifier and alias are separated by a colon +(``:``). The identifier shall match with the name of a register definition of +the item (see :ref:`SpecTypeRegisterDefinition`) or the name of a register +block include of the item (see :ref:`SpecTypeRegisterBlockIncludeRole`). If no +alias is specified, then the identifier is used for the register block member +name, otherwise the alias is used. If the register block member names are not +unique within the item, then a postfix number is appended to the names. The +number starts with zero for each set of names. The value shall match with the +regular expression "``^[a-zA-Z_][a-zA-Z0-9_]*(:[a-zA-Z_][a-zA-Z0-9_]*)?$``". + +This type is used by the following types: + +* :ref:`SpecTypeRegisterBlockMemberDefinition` + +.. _SpecTypeRequirementDesignGroupIdentifier: + +Requirement Design Group Identifier +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +A value of this type shall be of one of the following variants: + +* There may be no value (null). + +* The value may be a string. It shall be the identifier of the requirement + design group. The value shall match with the regular expression + "``^[a-zA-Z0-9_]*$``". + +This type is used by the following types: + +* :ref:`SpecTypeDesignGroupRequirementItemType` .. _SpecTypeRequirementRefinementLinkRole: @@ -4527,130 +5111,130 @@ of links. Requirement Text ^^^^^^^^^^^^^^^^ -The value shall be a string. It shall state a requirement or constraint. The -value shall not contain an element of +The value shall be a string. It shall state a requirement or constraint. The +text should not use one of the following words or phrases: -* "``acceptable``", +* acceptable -* "``adequate``", +* adequate -* "``almost always``", +* almost always -* "``and/or``", +* and/or -* "``appropriate``", +* appropriate -* "``approximately``", +* approximately -* "``as far as possible``", +* as far as possible -* "``as much as practicable``", +* as much as practicable -* "``best``", +* best -* "``best possible``", +* best possible -* "``easy``", +* easy -* "``efficient``", +* efficient -* "``e.g.``", +* e.g. -* "``enable``", +* enable -* "``enough``", +* enough -* "``etc.``", +* etc. -* "``few``", +* few -* "``first rate``", +* first rate -* "``flexible``", +* flexible -* "``generally``", +* generally -* "``goal``", +* goal -* "``graceful``", +* graceful -* "``great``", +* great -* "``greatest``", +* greatest -* "``ideally``", +* ideally -* "``i.e.``", +* i.e. -* "``if possible``", +* if possible -* "``in most cases``", +* in most cases -* "``large``", +* large -* "``many``", +* many -* "``maximize``", +* maximize -* "``minimize``", +* minimize -* "``most``", +* most -* "``multiple``", +* multiple -* "``necessary``", +* necessary -* "``numerous``", +* numerous -* "``optimize``", +* optimize -* "``ought to``", +* ought to -* "``probably``", +* probably -* "``quick``", +* quick -* "``rapid``", +* rapid -* "``reasonably``", +* reasonably -* "``relevant``", +* relevant -* "``robust``", +* robust -* "``satisfactory``", +* satisfactory -* "``several``", +* several -* "``shall be included but not limited to``", +* shall be included but not limited to -* "``simple``", +* simple -* "``small``", +* small -* "``some``", +* some -* "``state of the art``", +* state of the art -* "``sufficient``", +* sufficient -* "``suitable``", +* suitable -* "``support``", +* support -* "``systematically``", +* systematically -* "``transparent``", +* transparent -* "``typical``", +* typical -* "``user friendly``", +* user friendly -* "``usually``", +* usually -* "``versatile``", and +* versatile -* "``when necessary``". +* when necessary This type is used by the following types: @@ -4672,31 +5256,13 @@ Requirement Validation Link Role This type refines the :ref:`SpecTypeLink` through the ``role`` attribute if the value is ``validation``. It defines the requirement validation role of links. -.. _SpecTypeRequirementValidationMethod: - -Requirement Validation Method -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -The value shall be a string. This value type characterizes a requirement -validation method (except validation by test). The value shall be an element of +.. _SpecTypeRuntimeMeasurementEnvironmentName: -* "``by-analysis``", - -* "``by-inspection``", and - -* "``by-review-of-design``". - -This type is used by the following types: - -* :ref:`SpecTypeRequirementValidationItemType` - -.. _SpecTypeRuntimeMeasurementEnvironment: - -Runtime Measurement Environment -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Runtime Measurement Environment Name +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -The value shall be a string. It specifies the runtime measurement environment. -The value +The value shall be a string. It specifies the runtime measurement environment +name. The value * shall be an element of @@ -4719,12 +5285,12 @@ Runtime Measurement Environment Table This set of attributes provides runtime performance limits for a set of runtime measurement environments. Generic attributes may be specified. Each generic -attribute key shall be a :ref:`SpecTypeRuntimeMeasurementEnvironment`. Each +attribute key shall be a :ref:`SpecTypeRuntimeMeasurementEnvironmentName`. Each generic attribute value shall be a :ref:`SpecTypeRuntimeMeasurementValueTable`. This type is used by the following types: -* :ref:`SpecTypeRuntimePerformanceLimitTable` +* :ref:`SpecTypePerformanceRuntimeLimitsLinkRole` .. _SpecTypeRuntimeMeasurementParameterSet: @@ -4773,6 +5339,10 @@ value. The value shall be an element of * "``mean-upper-bound``", +* "``median-lower-bound``", + +* "``median-upper-bound``", + * "``min-lower-bound``", and * "``min-upper-bound``". @@ -4796,21 +5366,6 @@ This type is used by the following types: * :ref:`SpecTypeRuntimeMeasurementEnvironmentTable` -.. _SpecTypeRuntimePerformanceLimitTable: - -Runtime Performance Limit Table -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -This set of attributes provides runtime performance limits for BSP variants -specified by ``"<arch>/<bsp>"`` with <arch> being the architecture of the BSP -and <bsp> being the base name of the BSP. Generic attributes may be specified. -Each generic attribute key shall be a string. Each generic attribute value -shall be a :ref:`SpecTypeRuntimeMeasurementEnvironmentTable`. - -This type is used by the following types: - -* :ref:`SpecTypeRuntimePerformanceRequirementItemType` - .. _SpecTypeRuntimePerformanceParameterSet: Runtime Performance Parameter Set @@ -4824,6 +5379,19 @@ This type is used by the following types: * :ref:`SpecTypeRuntimePerformanceRequirementItemType` +.. _SpecTypeSHA256HashValue: + +SHA256 Hash Value +^^^^^^^^^^^^^^^^^ + +The value shall be a string. It shall be a SHA256 hash value encoded in +base64url. The value shall match with the regular expression +"``^[A-Za-z0-9+_=-]{44}$``". + +This type is used by the following types: + +* :ref:`SpecTypeExternalFileReference` + .. _SpecTypeSPDXLicenseIdentifier: SPDX License Identifier @@ -5471,7 +6039,7 @@ A value of this type shall be of one of the following variants: member definition. It shall be a valid C structure member definition without a trailing ``;``. -* There may by be no value (null). +* There may be no value (null). This type is used by the following types: @@ -5503,6 +6071,12 @@ A value of this type shall be of one of the following variants: scope after the general test declarations and before the test run function declaration. + freestanding + The attribute value shall be a boolean. The value shall be ``true``, if + the test case is freestanding, otherwise ``false``. Freestanding test + cases are not statically registered. Instead the generated test runner + uses :c:func:`T_case_begin` and :c:func:`T_case_end`. + includes The attribute value shall be a list of strings. It shall be a list of header files included by the header file via ``#include <...>``. @@ -5519,7 +6093,7 @@ A value of this type shall be of one of the following variants: The attribute value shall be a string. It shall be the path to the generated test header file. -* There may by be no value (null). +* There may be no value (null). This type is used by the following types: @@ -5581,7 +6155,7 @@ A value of this type shall be of one of the following variants: The attribute value shall be an optional string. It shall be the test support method description. -* There may by be no value (null). +* There may be no value (null). This type is used by the following types: diff --git a/eng/req/management.rst b/eng/req/management.rst index 3450471..4fb379c 100644 --- a/eng/req/management.rst +++ b/eng/req/management.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2020 embedded brains GmbH & Co. KG Requirement Management ====================== diff --git a/eng/req/req-for-req.rst b/eng/req/req-for-req.rst index 0c05ed6..5631b7d 100644 --- a/eng/req/req-for-req.rst +++ b/eng/req/req-for-req.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2020 embedded brains GmbH & Co. KG Requirements for Requirements ============================= diff --git a/eng/req/tooling.rst b/eng/req/tooling.rst index 3ca166b..2853932 100644 --- a/eng/req/tooling.rst +++ b/eng/req/tooling.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2020 embedded brains GmbH & Co. KG Tooling ======= diff --git a/eng/req/traceability.rst b/eng/req/traceability.rst index 9376a5f..99c4931 100644 --- a/eng/req/traceability.rst +++ b/eng/req/traceability.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2019, 2020 embedded brains GmbH (http://www.embedded-brains.de) +.. Copyright (C) 2019, 2020 embedded brains GmbH & Co. KG .. _ReqEngTrace: diff --git a/eng/stakeholders.rst b/eng/stakeholders.rst index 756c462..184f890 100644 --- a/eng/stakeholders.rst +++ b/eng/stakeholders.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2020 embedded brains GmbH +.. Copyright (C) 2020 embedded brains GmbH & Co. KG .. Copyright (C) 2018 RTEMS Foundation, The RTEMS Documentation Project RTEMS Stakeholders diff --git a/eng/test-framework.rst b/eng/test-framework.rst index bc6d300..25bbad9 100644 --- a/eng/test-framework.rst +++ b/eng/test-framework.rst @@ -1,6 +1,6 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2018, 2020 embedded brains GmbH +.. Copyright (C) 2018, 2020 embedded brains GmbH & Co. KG .. Copyright (C) 2018, 2020 Sebastian Huber Software Test Framework diff --git a/eng/tester.rst b/eng/tester.rst index a538caf..5b57842 100644 --- a/eng/tester.rst +++ b/eng/tester.rst @@ -1,12 +1,17 @@ .. SPDX-License-Identifier: CC-BY-SA-4.0 -.. Copyright (C) 2018. +.. Copyright (C) 2018, 2022. .. COMMENT: RTEMS Foundation, The RTEMS Documentation Project RTEMS Tester ************ -TBD - Convert the following to Rest and insert into this file -TBD https://devel.rtems.org/wiki/Testing/Tester -TBD - Above file is horribly out of date. Find new docs and refer to them +The RTEMS Tester is a test tool which provides a command line interface and +automates execution of test executables. It is part of the `rtems-tools` +repository and built as part of the RTEMS Tools for all targets by the +RTEMS Source Builder. The RTEMS Tester can be configured to test based +on local lab setup or to test on custom boards. + +The RTEMS Tester is documented the `RTEMS Tester and Run` section of the +`RTEMS User Manual`. diff --git a/eng/vc-users.rst b/eng/vc-users.rst index 64c2624..37fee64 100644 --- a/eng/vc-users.rst +++ b/eng/vc-users.rst @@ -422,20 +422,91 @@ then you rewrite those commits with ``git rebase`` and push them up again, the others will have to re-merge their work and trying to integrate their work into yours can become messy. -Accessing a developer's repository +Accessing a Developer's Repository ---------------------------------- RTEMS developers with Git commit access have personal repositories on https://git.rtems.org/ that can be cloned to view cutting-edge development work shared there. +Commit Message Guidance +----------------------- + +The commit message associated with a change to any software project +is of critical importance. It is the explanation of the change and the +rationale for it. Future users looing back through the project history +will rely on it. Even the author of the change will likely rely on it +once they have forgotten the details of the change. It is important to +make the message useful. Here are some guidelines followed by the RTEMS +Project to help improve the quality of our commit messages. + +* When committing a change the first line is a summary. Please make it short + while hinting at the nature of the change. You can discuses the change + if you wish in a ticket that has a PR number which can be referenced in + the commit message. After the first line, leave an empty line and add + whatever required details you feel are needed. + +* Patches should be as single purpose as possible. This is reflected in + the first line summary message. If you find yourself writing something + like "Fixed X and Y", "Updated A and B", or similar, then evaluate + whether the patch should really be a patch series rather than a single + larger patch. + +* Format the commit message so it is readable and clear. If you have + specific points related to the change make them with separate paragraphs + and if you wish you can optionally uses a `-` marker with suitable + indents and alignment to aid readability. + +* Limit the line length to less than 80 characters + +* Please use a real name with a valid email address. Please do not use + pseudonyms or provide anonymous contributions. + +* Please do not use terms such as "Fix bug", "With this change it + works", or "Bump hash". If you fix a bug please state the nature of the + bug and why this change fixes it. If a change makes something work then + detail the reason. You do not need to explain the change line by line + as the commits diff and associated ticket will. + +* If you change the formatting of source code in a repository please + make that a separate patch and use "Formatting changes only" on the first + line. Please indicate the reason or process. For example to "Conforming + to code standing", "Reverting to upstream format", "Result of automatic + formatting". + +* Similarly, if addressing a spelling, grammar, or Doxygen issue, please + put that in a commit by itself separate from technical changes. + +An example commit message: + +.. code-block:: shell + + test/change: Test message on formatting of commits + + - Shows a simple single first line + + - Has an empty second line + + - Shows the specifics of adding separate points in the commit message as + separate paragraphs. It also shows a `-` separator and multilines + that are less than the 80 character width + + - Show a ticket update and close + + Updates #9876 + Closes #8765 + +The first line generally starts with a file or directory name which +indicates the area in RTEMS to which the commit applies. For a patch +series which impacts multiple BSPs, it is common to put each BSP into +a separate patch. This improves the quality and specificity of the +commit messages. + Creating a Patch ----------------- +----------------- -Before submitting a patch read about `Contributing -<https://devel.rtems.org/wiki/Developer/Contributing>`_ to RTEMS and the -`Commit Message <https://devel.rtems.org/wiki/Developer/Git#GitCommits>`_ -formatting we require. +Before submitting a patch, please read `Commit Message Guidance`_ to +become familiar with the commit message formatting we require. The recommended way to create a patch is to branch the Git repository master and use one commit for each logical change. Then you can use @@ -466,6 +537,12 @@ the rtems-docs repo, use git format-patch --subject-prefix="PATCH rtems-docs" ... +You can set a default subject prefix for each repository locally, for example: + +.. code-block:: shell + + git config format.subjectprefix "PATCH rtems-docs" + Patches created using ``git format-patch`` are formatted so they can be emailed and rely on having Git configured with your name and email address, for example |