From 2c88912893ebbcc3b9fa14d4fcc100c42252d0df Mon Sep 17 00:00:00 2001 From: Andrew Butterfield Date: Thu, 9 Nov 2023 11:26:56 +0000 Subject: eng: Add formal verification chapter --- eng/fv/appendix-fv.rst | 1749 ++++++++++++++++++++++++++++++++++++++++++++++ eng/fv/approaches.rst | 178 +++++ eng/fv/index.rst | 16 + eng/fv/methodology.rst | 62 ++ eng/fv/overview.rst | 38 + eng/fv/promela-index.rst | 9 + eng/fv/promela.rst | 323 +++++++++ eng/fv/refinement.rst | 559 +++++++++++++++ eng/fv/tool-setup.rst | 317 +++++++++ eng/glossary.rst | 14 + eng/index.rst | 3 + 11 files changed, 3268 insertions(+) create mode 100755 eng/fv/appendix-fv.rst create mode 100644 eng/fv/approaches.rst create mode 100755 eng/fv/index.rst create mode 100755 eng/fv/methodology.rst create mode 100755 eng/fv/overview.rst create mode 100644 eng/fv/promela-index.rst create mode 100755 eng/fv/promela.rst create mode 100755 eng/fv/refinement.rst create mode 100755 eng/fv/tool-setup.rst (limited to 'eng') 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-.h`` and ``tr-.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..6bbac20 --- /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` (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..15ce7d8 --- /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` 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 + ``{ ; ; ... ; }`` where each ```` can be any + kind of statement, atomic or composite. The sub-statements execute in + sequence in the usual way. + +Selection + .. code-block:: none + + if + :: + :: + ... + :: + fi + + A selection construct is blocked if all the ```` are blocked. It is + executable if at least one ```` is executable. The scheduler will make + a non-deterministic choice from all of those ```` that are executable. + The construct terminates when/if the chosen ```` 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 ```` has the form ``else -> ...``, then the ``else`` is + executable only when all the other selection statements are blocked. + +Repetition + .. code-block:: none + + do + :: + :: + ... + :: + od + + The executability rules here are the same as for Selection above. The key + difference is that when/if a chosen ```` 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 ```` 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`: + + ``@@@ ... `` + +The leading ``@@@`` is a marker that makes it easy to filter out this +information from other SPIN output. + +Parameters take the following forms: + + ```` Promela Process Id of ``proctype`` generating annotation + + ```` chunk of text containing no white space + + ```` Promela variable/structure/constant identifier + + ```` Promela type identifier + + ```` OS Task/Thread/Process Id + + ``_`` unused argument (within containers) + +Each ```` is associated with specific forms of parameters: + +.. code-block:: none + + LOG ... + NAME + INIT + DEF + DECL [] + DCLARRAY + TASK + SIGNAL + WAIT + STATE tid + SCALAR (|_) [] + PTR + STRUCT + SEQ + END + CALL ... + + +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 ```` + (``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 (````). + +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 ```` 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 ... `` (Direct Output) + Generate a call to ``T_log()`` with a message formed from the ```` + parameters. + This message will appear in the test output for certain verbosity settings. + +NAME +^^^^ + +``NAME `` (Keyword Refinement) + Looks up ``NAME`` (currently ignoring ````) 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 Refinement) + Lookup ```` and return corresponding C code. + +SIGNAL +^^^^^^ + +``SIGNAL `` (Keyword Refinement) + Lookup `SIGNAL` and return code with `` substituted in. + +WAIT +^^^^ + +``WAIT `` (Keyword Refinement) + Lookup `WAIT` and return code with `` substituted in. + +DEF +^^^ + +``DEF `` (Direct Output) + Output ``#define ``. + +DECL +^^^^ + +``DECL []`` (Name Refinement) + Lookup ``_DCL`` and substitute ```` in. If ```` is + present, append ``=``. Add a final semicolon. If the `` value + is zero, prepend ``static``. + +DCLARRAY +^^^^^^^^ + +``DCLARRAY `` (Name Refinement) + Lookup ``_DCL`` and substitute ```` and ```` in. If the + `` value is zero, prepend ``static``. + +CALL +^^^^ + +``CALL .. `` (Name refinement, ``N`` < 6) + Lookup ```` and substitute all ```` in. + +STATE +^^^^^ + +``STATE `` (Name Refinement) + Lookup ```` and substitute in ````. + +STRUCT +^^^^^^ + +``STRUCT `` + Declares the output of the contents of variable ```` + that is itself a structure. The ```` 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 `` + Declares the output of the contents of array variable ````. + The ```` 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 Refinement) + If not inside a ``STRUCT``, lookup ``_PTR``. Two lines of code should + be returned. If the ```` is zero, use the first line, otherwise use + the second with ```` substituted in. This is required to handle NULL + pointers. + + If inside a ``STRUCT``, lookup ``_FPTR``. Two lines of code should + be returned. If the ```` is zero, use the first line, otherwise use + the second with ```` substituted in. This is required to handle NULL + pointers. + +SCALAR +^^^^^^ + +There are quite a few variations here. + +``SCALAR _ `` + Should only be used inside a ``SEQ``. A space and ```` is appended + to the string being accumulated by this ``SEQ``. + +``SCALAR `` (Name Refinement) + If not inside a ``STRUCT``, lookup ````, and substitute ```` + into the resulting code. + + If inside a ``STRUCT``, lookup ``_FSCALAR`` and substitute the saved + ``STRUCT`` name and ```` into the resulting code. + + This should not be used inside a ``SEQ``. + +``SCALAR `` (Name Refinement) + If not inside a ``STRUCT``, lookup ````, and substitute ```` + and ```` into the resulting code. + + If inside a ``STRUCT``, lookup ``_FSCALAR`` and substitute the saved + ``STRUCT`` name and ```` into the resulting code. + + This should not be used inside a ``SEQ``. + +END +^^^ + +``END `` + If inside a ``STRUCT``, terminates processing a + structured variable. + + If inside a ``SEQ``, lookup ``_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.py + rtems: # rtems.git, or ..../modules/rtems/ + rsb: /rtems/6/bin/ + simulator: /sparc-rtems6-sis + testyamldir: /spec/build/testsuites/validation/ # directory containing .yml + testcode: /testsuites/validation/ + testexedir: /build/.../testsuites/validation/ # directory containing ts-.exe + testsuite: model-0 + simulatorargs: -leon3 -r s -m 2 # run command executes " /ts-.exe" + spinallscenarios: -DTEST_GEN -run -E -c0 -e # trail generation "spin .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 ````. + +* 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*: + + ``/spec/build/testsuites/validation/`` + +* testcode: + This should be the absolute path to where validation test sources + are found: + + ``/testsuites/validation/`` + +* testexedir: + This should be the absolute path to where + the model-based validation test executable + will be found: + + ``/build/.../testsuites/validation/`` + + This will contain ``ts-.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. + + ``- -r s -m `` + + 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 []`` + +The commands provided are: + +``clean `` + Removes generated files. + +``spin `` + Runs SPIN to find all scenarios. The scenarios are found in numbered files + called ``N.spn``. + +``gentests `` + Convert SPIN scenarios to test sources. Each ``N.spn`` produces a numbered + test source file. + +``copy `` + Copies the generated test files to the relevant test source directory, and + updates the relevant test configuration files. + +``archive `` + 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 `` + 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: + ``.pml``, + ``-rfn.yml``, + ``-pre.h``, + ``-post.h``, and + ``-run.h``. +In addition there may be other files +whose names have 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 da23fea..0e0b708 100644 --- a/eng/glossary.rst +++ b/eng/glossary.rst @@ -63,6 +63,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 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 `_. diff --git a/eng/index.rst b/eng/index.rst index a4d4563..e4712ae 100644 --- a/eng/index.rst +++ b/eng/index.rst @@ -11,6 +11,7 @@ RTEMS Software Engineering (|version|) .. topic:: Copyrights and License + | |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 -- cgit v1.2.3