[PATCH] glossary: Add terms
Joel Sherrill
joel at rtems.org
Tue Nov 28 19:31:00 UTC 2023
On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber <
sebastian.huber at embedded-brains.de> wrote:
> ---
> c-user/glossary.rst | 50 +++++++++++++++++++++++++++++++++++++++++++
> eng/fv/approaches.rst | 2 +-
> eng/fv/overview.rst | 6 +++---
> eng/glossary.rst | 26 +++++++++++++++++-----
> 4 files changed, 75 insertions(+), 9 deletions(-)
>
> diff --git a/c-user/glossary.rst b/c-user/glossary.rst
> index 82aedcd..9a9d12c 100644
> --- a/c-user/glossary.rst
> +++ b/c-user/glossary.rst
> @@ -1,5 +1,6 @@
> .. SPDX-License-Identifier: CC-BY-SA-4.0
>
> +.. Copyright (C) 2022, 2023 Trinity College Dublin
> .. Copyright (C) 2020 Richi Dubey (richidubey at gmail.com)
> .. Copyright (C) 2015, 2023 embedded brains GmbH & Co. KG
> .. Copyright (C) 1988, 1998 On-Line Applications Research Corporation
> (OAR)
> @@ -17,6 +18,9 @@ Glossary
> A term used to describe an object which has been created by an
> application.
>
> + AMP
> + This term is an acronym for Asymmetric Multiprocessing.
> +
> APA
> This term is an acronym for Arbitrary Processor Affinity. APA
> schedulers
> allow a thread to have an arbitrary affinity to a processor set,
> rather than
> @@ -357,6 +361,10 @@ Glossary
> mathematically intensive situations. It is typically viewed as a
> logical
> extension of the primary processor.
>
> + formal model
> + A model of a computing component (hardware or software) that has a
> + mathematically based :term:`semantics`.
>
This is in the neighborhood of the definitions I found but is missing a word
like rigorous.
> +
> freed
> A resource that has been released by the application to RTEMS.
>
> @@ -386,6 +394,14 @@ Glossary
> GNU
> This term is an acronym for `GNU's Not Unix <https://www.gnu.org/
> >`_.
>
> + GPL
> + This term is an acronym for
> + `GNU General Public License <https://www.gnu.org/licenses>`__.
> +
> + GPLv3
> + This term is an acronym for
> + `GNU General Public License Version 3 <
> https://www.gnu.org/licenses/gpl-3.0.html>`__.
> +
>
Do we need to include an entry for the GPLv2 w/exception that is actually
used by some RTEMS code.
> GR712RC
> The
> `GR712RC <
> https://www.gaisler.com/index.php/products/components/gr712rc>`_
> @@ -511,6 +527,10 @@ Glossary
> LIFO
> This term is an acronym for :term:`Last In First Out`.
>
> + Linear Temporal Logic
> + This is a logic that states properties about (possibly infinite)
> sequences of
> + states.
> +
> list
> A data structure which allows for dynamic addition and removal of
> entries. It is not statically limited to a particular size.
> @@ -520,6 +540,12 @@ Glossary
> are arranged such that the least significant byte is at the lowest
> address.
>
> + LLVM
> + This term is an acronym for
> + `Low Level Virtual Machine <https://www.llvm.org>`__.
> + The LLVM Project is a collection of modular and reusable compiler
> and
> + toolchain technologies.
> +
> local
> An object which was created with the LOCAL attribute and is
> accessible
> only on the node it was created and resides upon. In a single
> processor
> @@ -541,6 +567,9 @@ Glossary
> A :term:`task` ``L`` has a lower :term:`priority` than a task
> ``H``, if
> task ``L`` is less important than task ``H``.
>
> + LTL
> + This term is an acronym for :term:`Linear Temporal Logic`.
> +
> major number
> The index of a device driver in the Device Driver Table.
>
> @@ -632,6 +661,9 @@ Glossary
> mathematically intensive situations. It is typically viewed as a
> logical
> extension of the primary processor.
>
> + OBC
> + This term is an acronym for On-Board Computer.
> +
> object
> In this document, this term is used to refer collectively to
> tasks,
> timers, message queues, partitions, regions, semaphores, ports,
> and rate
> @@ -806,6 +838,10 @@ Glossary
> A term used to describe routines which do not modify themselves
> or global
> variables.
>
> + refinement
> + A *refinement* is a relationship between a specification and its
> + implementation as code.
> +
> region
> An RTEMS object which is used to allocate and deallocate variable
> size
> blocks of memory from a dynamically specified area of memory.
> @@ -818,6 +854,9 @@ Glossary
> Registers are locations physically located within a component,
> typically
> used for device control or general purpose storage.
>
> + reification
> + Another term used to denote :term:`refinement`.
> +
> remote
> Any object that does not reside on the local node.
>
> @@ -865,6 +904,12 @@ Glossary
> The state of a rate monotonic timer while it is being used to
> delineate a
> period. The timer exits this state by either expiring or being
> canceled.
>
> + scenario
> + In a setting that involves many concurrent tasks that interleave
> in arbitrary
> + ways, a scenario describes a single specific possible
> interleaving. One
> + interpretation of the behaviour of a concurrent system is the set
> of all its
> + scenarios.
> +
>
This doesn't cover the common use case of a test scenario which is usually
less about threading and more about values and using a set of methods in
a particular manner.
> schedulable
> A set of tasks which can be guaranteed to meet their deadlines
> based upon
> a specific scheduling algorithm.
> @@ -901,6 +946,11 @@ Glossary
> segments
> Variable sized memory blocks allocated from a region.
>
> + semantics
> + This term refers to the meaning of text or utterances in some
> language. In a
> + software engineering context these will be programming, modelling
> or
> + specification languages.
> +
> semaphore
> An RTEMS object which is used to synchronize tasks and provide
> mutually
> exclusive access to resources.
> diff --git a/eng/fv/approaches.rst b/eng/fv/approaches.rst
> index 6bbac20..fe58a06 100644
> --- a/eng/fv/approaches.rst
> +++ b/eng/fv/approaches.rst
> @@ -168,7 +168,7 @@ in such a way that tests can be generated using the
> SPIN model checker
> 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
> +assertions, and :term:`Linear Temporal Logic` (:term:`LTL`) to express
> properties of
> interest.
>
> Given a Promela model that checks key properties successfully,
> diff --git a/eng/fv/overview.rst b/eng/fv/overview.rst
> index 15ce7d8..da981f2 100755
> --- a/eng/fv/overview.rst
> +++ b/eng/fv/overview.rst
> @@ -30,9 +30,9 @@ such as a specification. This relationship is commonly
> referred to as a
>
> 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.
> +:term:`scenarios <scenario>` that describe possible correct behaviors of
> the
> +system at the relevant level of abstraction. A refinement for these can be
> +defined by using them to generate test code.
>
This definition of scenario is different from the one in the glossary. It
is more inline with what I expected.
> 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/glossary.rst b/eng/glossary.rst
> index 0e0b708..42cadc4 100644
> --- a/eng/glossary.rst
> +++ b/eng/glossary.rst
> @@ -1,5 +1,6 @@
> .. SPDX-License-Identifier: CC-BY-SA-4.0
>
> +.. Copyright (C) 2022, 2023 Trinity College Dublin
> .. Copyright (C) 2017, 2019 embedded brains GmbH & Co. KG
> .. Copyright (C) 1988, 1998 On-Line Applications Research Corporation
> (OAR)
>
> @@ -39,6 +40,10 @@ Glossary
> This term is an acronym for
> `Executable and Linkable Format <
> https://en.wikipedia.org/wiki/Executable_and_Linkable_Format>`_.
>
> + formal model
> + A model of a computing component (hardware or software) that has a
> + mathematically based :term:`semantics`.
>
Why is this duplicated? Don't we have a single glossary file?
There are other duplicates below. Can we have a single source of truth?
+
> GCC
> This term is an acronym for `GNU Compiler Collection <
> https://gcc.gnu.org/>`_.
>
> @@ -64,15 +69,15 @@ Glossary
> 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.
> + This is a logic that states properties about (possibly infinite)
> sequences of
> + states.
>
> LTL
> - This term is an acronym for Linear Temporal Logic.
> + This term is an acronym for :term:`Linear Temporal Logic`.
>
> refinement
> - A *refinement* is a relationship between a specification
> - and its implementation as code.
> + A *refinement* is a relationship between a specification and its
> + implementation as code.
>
> reification
> Another term used to denote :term:`refinement`.
> @@ -84,6 +89,17 @@ Glossary
> RTEMS
> This term is an acronym for Real-Time Executive for
> Multiprocessor Systems.
>
> + scenario
> + In a setting that involves many concurrent tasks that interleave
> in arbitrary
> + ways, a scenario describes a single specific possible
> interleaving. One
> + interpretation of the behaviour of a concurrent system is the set
> of all its
> + scenarios.
> +
> + semantics
> + This term refers to the meaning of text or utterances in some
> language. In a
> + software engineering context these will be programming, modelling
> or
> + specification languages.
> +
> software component
> This term is defined by ECSS-E-ST-40C 3.2.28 as a "part of a
> software
> system". For this project a *software component* shall be any of
> the
> --
> 2.35.3
>
> _______________________________________________
> devel mailing list
> devel at rtems.org
> http://lists.rtems.org/mailman/listinfo/devel
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/devel/attachments/20231128/e9eded0e/attachment-0001.htm>
More information about the devel
mailing list