Re: [PATCH] glossary: Add terms

[Sebastian Huber]

On 29.11.23 09:13, Sebastian Huber wrote:

On 28.11.23 20:49, andrew.butterfi...@scss.tcd.ie wrote:

    +    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.

In the context in which Sebastian asked me for this entry, the term 
`scenario` is used as described above.


But you are right that there are nuances here. In the Promela/SPIN 
based test-generation work, each
counter example we get from SPIN describes a scenario as defined 
above, and we generate C test code
that reproduces that scenario, including the precise interleaving of 
the tasks as per  that scenario.


The term scenario is used a lot in the formal verification chapter, so 
it should have an entry. Joel, do you have a suggestion to improve the 
wording?


I added an "In the context of formal verification, ..." to the term 
definition and checked it in.


--
embedded brains GmbH & Co. KG
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH] glossary: Add terms

[Sebastian Huber]

On 28.11.23 20:49, andrew.butterfi...@scss.tcd.ie wrote:

+    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.

In the context in which Sebastian asked me for this entry, the term 
`scenario` is used as described above.


But you are right that there are nuances here. In the Promela/SPIN based 
test-generation work, each
counter example we get from SPIN describes a scenario as defined above, 
and we generate C test code
that reproduces that scenario, including the precise interleaving of the 
tasks as per  that scenario.


The term scenario is used a lot in the formal verification chapter, so 
it should have an entry. Joel, do you have a suggestion to improve the 
wording?



--
embedded brains GmbH & Co. KG
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH] glossary: Add terms

[Sebastian Huber]

On 28.11.23 20:31, Joel Sherrill wrote:

+    GPL
+        This term is an acronym for
+        `GNU General Public License >`__.
+
+    GPLv3
+        This term is an acronym for
+        `GNU General Public License Version 3
>`__.
+


Do we need to include an entry for the GPLv2 w/exception that is 
actually used by some RTEMS code.


I will add an entry for GPLv2.

--
embedded brains GmbH & Co. KG
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH] glossary: Add terms

[Sebastian Huber]

On 28.11.23 20:31, Joel Sherrill wrote:

+    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?


We have a single source of truth:

https://git.rtems.org/rtems-central/tree/spec-glossary/glossary

The c-user/glossary.rst contains all terms. The other documents only the 
terms used in the document.


--
embedded brains GmbH & Co. KG
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax:   +49-89-18 94 741 - 08

Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH] glossary: Add terms

[andrew.butterfi...@scss.tcd.ie]

From: devel  on behalf of Joel Sherrill 

Reply to: "j...@rtems.org" 
Date: Tuesday 28 November 2023 at 19:31
To: Sebastian Huber 
Cc: "devel@rtems.org" 
Subject: Re: [PATCH] glossary: Add terms



On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber 
mailto:sebastian.hu...@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 
(richidu...@gmail.com<mailto:richidu...@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.

For me "mathematically based" implies "rigorous", but I think you are right to 
emphasise this

How about: "A rigorous model of " ?


+
 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
+Anothe

Re: [PATCH] glossary: Add terms

[Joel Sherrill]

On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber <
sebastian.hu...@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 (richidu...@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  >`_.
>
> +GPL
> +This term is an acronym for
> +`GNU General Public License `__.
> +
> +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 `__.
> +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
> 

[PATCH] glossary: Add terms

[Sebastian Huber]

---
 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 (richidu...@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`.
+
 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 `_.
 
+GPL
+This term is an acronym for
+`GNU General Public License `__.
+
+GPLv3
+This term is an acronym for
+`GNU General Public License Version 3 
`__.
+
 GR712RC
 The
 `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 `__.
+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.
+
 schedulable
 A set of tasks which can be guaranteed to meet their deadlines based 
upon
 a specific scheduling algorithm.
@@ 

Re: [PATCH] glossary: Add terms

[Chris Johns]

OK

On 29/9/21 8:45 pm, Sebastian Huber wrote:
> ---
>  c-user/glossary.rst | 30 ++
>  1 file changed, 30 insertions(+)
> 
> diff --git a/c-user/glossary.rst b/c-user/glossary.rst
> index f85c08c..e91e356 100644
> --- a/c-user/glossary.rst
> +++ b/c-user/glossary.rst
> @@ -101,9 +101,21 @@ Glossary
>  C++11
>  The standard ISO/IEC 14882:2011.
>  
> +C++14
> +The standard ISO/IEC 14882:2014.
> +
> +C++17
> +The standard ISO/IEC 14882:2017.
> +
> +C++20
> +The standard ISO/IEC 14882:2020.
> +
>  C11
>  The standard ISO/IEC 9899:2011.
>  
> +C17
> +The standard ISO/IEC 9899:2018.
> +
>  calling convention
>  The processor and compiler dependent rules which define the mechanism
>  used to invoke subroutines in a high-level language.  These rules 
> define
> @@ -250,6 +262,9 @@ Glossary
>  EARS
>  This term is an acronym for Easy Approach to Requirements Syntax.
>  
> +EDF
> +This term is an acronym for Earliest Deadline First.
> +
>  ELF
>  This term is an acronym for
>  `Executable and Linkable Format 
> `_.
> @@ -349,6 +364,14 @@ Glossary
>  freed
>  A resource that has been released by the application to RTEMS.
>  
> +Futex
> +This term is an abbreviation for
> +`Fast User-Space Locking 
> `_.
> +The futex support in RTEMS is provided for the barriers of the
> +:term:`OpenMP` library provided by :term:`GCC`.  It could be used to
> +implement high performance :term:`SMP` synchronization primitives 
> which
> +offer random-fairness.
> +
>  GCC
>  This term is an acronym for `GNU Compiler Collection 
> `_.
>  
> @@ -547,6 +570,9 @@ Glossary
>  This term is an acronym for
>  :term:`Multiprocessor Communications Interface Layer`.
>  
> +MrsP
> +This term is an acronym for Multiprocessor Resource-Sharing Protocol.
> +
>  multiprocessing
>  The simultaneous execution of two or more processes by a multiple
>  processor computer system.
> @@ -610,6 +636,10 @@ Glossary
>  clustered scheduling.  The ``m`` denotes the number of processors in 
> the
>  system.
>  
> +OpenMP
> +This term is an acronym for
> +`Open Multi-Processing `_.
> +
>  operating system
>  The software which controls all the computer's resources and 
> provides the
>  base upon which application programs can be written.
> 
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

[PATCH] glossary: Add terms

[Sebastian Huber]

---
 c-user/glossary.rst | 30 ++
 1 file changed, 30 insertions(+)

diff --git a/c-user/glossary.rst b/c-user/glossary.rst
index f85c08c..e91e356 100644
--- a/c-user/glossary.rst
+++ b/c-user/glossary.rst
@@ -101,9 +101,21 @@ Glossary
 C++11
 The standard ISO/IEC 14882:2011.
 
+C++14
+The standard ISO/IEC 14882:2014.
+
+C++17
+The standard ISO/IEC 14882:2017.
+
+C++20
+The standard ISO/IEC 14882:2020.
+
 C11
 The standard ISO/IEC 9899:2011.
 
+C17
+The standard ISO/IEC 9899:2018.
+
 calling convention
 The processor and compiler dependent rules which define the mechanism
 used to invoke subroutines in a high-level language.  These rules 
define
@@ -250,6 +262,9 @@ Glossary
 EARS
 This term is an acronym for Easy Approach to Requirements Syntax.
 
+EDF
+This term is an acronym for Earliest Deadline First.
+
 ELF
 This term is an acronym for
 `Executable and Linkable Format 
`_.
@@ -349,6 +364,14 @@ Glossary
 freed
 A resource that has been released by the application to RTEMS.
 
+Futex
+This term is an abbreviation for
+`Fast User-Space Locking 
`_.
+The futex support in RTEMS is provided for the barriers of the
+:term:`OpenMP` library provided by :term:`GCC`.  It could be used to
+implement high performance :term:`SMP` synchronization primitives which
+offer random-fairness.
+
 GCC
 This term is an acronym for `GNU Compiler Collection 
`_.
 
@@ -547,6 +570,9 @@ Glossary
 This term is an acronym for
 :term:`Multiprocessor Communications Interface Layer`.
 
+MrsP
+This term is an acronym for Multiprocessor Resource-Sharing Protocol.
+
 multiprocessing
 The simultaneous execution of two or more processes by a multiple
 processor computer system.
@@ -610,6 +636,10 @@ Glossary
 clustered scheduling.  The ``m`` denotes the number of processors in 
the
 system.
 
+OpenMP
+This term is an acronym for
+`Open Multi-Processing `_.
+
 operating system
 The software which controls all the computer's resources and provides 
the
 base upon which application programs can be written.
-- 
2.31.1

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel