Re: Phrases for CONSTRAINTS section in the directive documentation
Hi Sebastian, I'd prefer 2. The directive may be called from an interrupt context (substituting "must", "must not", as appropriate) Regards, Andrew > On 22 Jan 2021, at 12:09, Sebastian Huber > wrote: > > Hello, > > since there is an agreement to add a CONSTRAINTS section to the directive > documentation, I need some standard phrases. > > 1. > > The directive may be called in interrupt context. > > 2. > > The directive may be called from interrupt context. > > 3. > > The directive can be called ... interrupt context. > > What do you prefer? > > I would use it for other contexts as well. > > -- > embedded brains GmbH > 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 Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH v2] eng: Requirements counting shall start at zero
Hello Frank, I have a use case where the numbers will exceed 10 . It's not for numbered requirements but numbered test-files. These result from different scenarios generated by our SPIN models, as part of the qualification activity. The files are generated (and numbered) automatically, so the constraints are somewhat different. For the Events Manager, for example, I'd expect the final number of generated test source files to exceed 10. It is unlikely that we would reach 100, though. Regards, Andrew > On 11 Dec 2020, at 15:16, Frank Kühndel > wrote: > > Hello Joel, > > On 12/11/20 3:49 PM, Joel Sherrill wrote: >> >> >> On Fri, Dec 11, 2020, 8:41 AM Frank Kuehndel >> > <mailto:frank.kuehn...@embedded-brains.de>> wrote: >> >>From: Frank Kühndel ><mailto:frank.kuehn...@embedded-brains.de>> >> >>--- >> eng/req/req-for-req.rst | 21 + >> 1 file changed, 21 insertions(+) >> >>diff --git a/eng/req/req-for-req.rst b/eng/req/req-for-req.rst >>index 9225e95..dcc4c11 100644 >>--- a/eng/req/req-for-req.rst >>+++ b/eng/req/req-for-req.rst >>@@ -308,6 +308,27 @@ spec:/classic/task/create-err-invname >> >> ... >> >>+If requirements or the YAML files which contain them are to be >>numbered, >>+the numbering shall start with 0. For example: >> >>+ >>+.. code-block:: none >>+ >>+weak-alias-0.yml >>+weak-alias-1.yml >>+ >>+Smaller numbers shall be prefixed with 0 to the same count of digits >>+as the largest number. For example: >> >> >> When one goes from 99 to 100 requirements and didn't anticipate having >> that many, does this mean all the files will have to be renamed? > > I can change the text to what Gedare Bloom suggested: "If we know the > max count (N) ahead of time, ..." > > Just from my experience with the requirements for the basedefs, when I > create the requirements for an operation, I know the number I end up > with before checking them in. The issue we discuss would only cause > trouble if later more requirements for the same operation must be added. > This is not totally unlikely but it means that one actually has 9 and > then need a 10th one. > >> >> Should we start with a minimum of three or four digits? What would drive >> the number of requirements in a set? How large of a functional area will >> a single numbered set contain? >> >> I'm just wondering if it is simpler to just have 001 as a minimum. > > I think that 99 requirements for a single operation are really out of > scope. That will hopefully never ever happen. Even 9 is already a lot. > Also it is rather advisable to adapt the names of the requirements to > indicate the purpose. The numbering is more for the case that there are > two or more requirements on the same topic (like on handling the same > bad input argument). > > my-function-0 > my-function-1 > my-function-global-side-effect > my-function-bad-argument-x-error-handling > my-function-bad-argument-y-error-handling > my-function-called-in-wrong-state > > My opinion is that defining whether we start counting with 0 or with 1 > makes sense. Everything else seems to me a bit like solving theoretical > problems. > >> >>+ >>+.. code-block:: none >>+ >>+alias-00.yml >>+alias-01.yml >>+alias-02.yml >>+... >>+alias-09.yml >>+alias-10.yml >>+alias-11.yml >>+ >> Conflict Free Requirements >> -- >> >>-- >>2.26.2 >> >>___ >>devel mailing list >>devel@rtems.org <mailto:devel@rtems.org> >>http://lists.rtems.org/mailman/listinfo/devel >><http://lists.rtems.org/mailman/listinfo/devel> >> > > Greetings > Frank > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH] eng: Requirements counting shall start at zero
Hi Frank, I plan to generate numbered test sources - should these also be numbered from 0? E.g. tr-model-events-mgr-n.c - I was going to have `n` range from 1..N -- should I adopt the same convention as you suggest for consistency? Regards, Andrew > On 9 Dec 2020, at 13:36, Frank Kuehndel > wrote: > > From: Frank Kühndel > > --- > eng/req/req-for-req.rst | 8 > 1 file changed, 8 insertions(+) > > diff --git a/eng/req/req-for-req.rst b/eng/req/req-for-req.rst > index 9225e95..8345e35 100644 > --- a/eng/req/req-for-req.rst > +++ b/eng/req/req-for-req.rst > @@ -308,6 +308,14 @@ spec:/classic/task/create-err-invname > > ... > > +If requirements or the YAML files which contain them are to be numbered, > +the numbering shall start with 0. For example: > + > +.. code-block:: none > + > +weak-alias-0.yml > +weak-alias-1.yml > + > Conflict Free Requirements > -- > > -- > 2.26.2 > > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: [PATCH] eng: Move code formatting rules into one section
Hi Sebastian > + /* > + * Excessively long comments should be broken up at a word boundary or > + * somewhere that makes sense, for example. > + */ > + > +Note that multiline comments have a single asterisk aligned with the asterisk > +in the opening ``/*``. > The closing ``*/`` should go at the end of the last line. I think this is closer to what was discussed earlier: The closing ``*/`` should appear on a line by itself at the end. -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Out of tree builds with waf?
Hi Sebastian, I'm not a waf expert, but might this section in their book help? https://waf.io/book/#_fundamental_waf_commands <https://waf.io/book/#_fundamental_waf_commands> Can variables `top` and `out` in the example there be manipulated to do want you want? Regards, Andrew > On 5 Nov 2020, at 16:45, Sebastian Huber > wrote: > > On 05/11/2020 17:09, Joel Sherrill wrote: > >> >> >> On Thu, Nov 5, 2020 at 10:04 AM Sebastian Huber >> > <mailto:sebastian.hu...@embedded-brains.de>> wrote: >> >>Hello, >> >>I tried to do an out of tree build with waf: >> >>~/src/rtems/waf configure --rtems-config $PWD/config.ini --out >>$PWD/build --top $HOME/src/rtems >> >>This seems to work, however, I get a message like this (CWD /home >>...): >> >>~/src/rtems/waf --out $PWD/build --top $HOME/src/rtems >>Waf: Entering directory >>`/home/EB/sebastian_h/src/rtems-source-builder/tmp/build' >>Waf: Leaving directory >>`/home/EB/sebastian_h/src/rtems-source-builder/tmp/build' >>'build' finished successfully (0.332s) >>Waf: Entering directory >>`/home/EB/sebastian_h/src/rtems-source-builder/tmp/build/sparc/erc32' >>CWD /home/EB/sebastian_h/src/rtems-source-builder/tmp is not under >>/home/EB/sebastian_h/src/rtems, forcing --targets=* (run distclean?) >>Waf: Leaving directory >>`/home/EB/sebastian_h/src/rtems-source-builder/tmp/build/sparc/erc32' >>'build_sparc/erc32' finished successfully (0.438s) >> >>I this something to worry about? Are out of tree builds supported >>by waf? >> >> >> I hope they can be. Or at least the build directory name changed based >> on user input. >> >> For automated testing, I have been building multiple BSPs in parallel >> completely independently. I don't know a way to do this with waf. > > If out of tree builds and a read-only source tree should be supported by the > build system, then this should be added to the goals in eng/build-system.rst. > > I need some support from a waf expert to add proper support for this to the > wscript. > > Another open issue is the --target option which currently doesn't work. > > -- > embedded brains GmbH > 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 > PGP: Public key available on request. > > embedded brains GmbH > 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 Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Problem re-building RTEMS docs
HI Sebastian, reading https://docs.rtems.org/branches/master/eng/vc-users.html <https://docs.rtems.org/branches/master/eng/vc-users.html> (Sec 6.1.3 Making Changes), I found the following sequence that fixed things. git checkout master git pull git checkout git rebase master Now the documents all build, off 6.8fe0da2-modified (27th October 2020) - thanks for you support Andrew > On 3 Nov 2020, at 18:12, Andrew Butterfield > wrote: > > Hi Sebastian, > > I thought `git submodule update` would do it - my bad > > I tried `git submodule sync`, but this still leaves me back in 3rd July 2020 > > Doing a `git pull` afterwards, in rtems-docs makes no change. What do I need > to do to bring all the submodules up to date? > > Thanks, Andrew > >> On 3 Nov 2020, at 18:01, Sebastian Huber > <mailto:sebastian.hu...@embedded-brains.de>> wrote: >> >> On 03/11/2020 18:47, Andrew Butterfield wrote: >> >>> $ ./waf >>> Waf: Entering directory >>> `/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/build' >>> Build: 6.0c13e94-modified (3rd July 2020) >> >> This is an extremely out dated version. You should see something like this: >> >> Waf: Entering directory >> `/home/EB/sebastian_h/src/rtems-central/modules/rtems-docs/build' >> Build: 6.9628dfd (1st October 2020) >> >> -- >> Sebastian Huber, embedded brains GmbH >> >> Address : Dornierstr. 4, D-82178 Puchheim, Germany >> Phone : +49 89 189 47 41-16 >> Fax : +49 89 189 47 41-09 >> E-Mail : sebastian.hu...@embedded-brains.de >> <mailto:sebastian.hu...@embedded-brains.de> >> PGP : Public key available on request. >> >> Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. >> > > > Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 > Lero@TCD, Head of Software Foundations & Verification Research Group > School of Computer Science and Statistics, > Room G.39, O'Reilly Institute, Trinity College, University of Dublin > http://www.scss.tcd.ie/Andrew.Butterfield/ > <http://www.scss.tcd.ie/Andrew.Butterfield/> > -------- > > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Problem re-building RTEMS docs
Hi Sebastian, I thought `git submodule update` would do it - my bad I tried `git submodule sync`, but this still leaves me back in 3rd July 2020 Doing a `git pull` afterwards, in rtems-docs makes no change. What do I need to do to bring all the submodules up to date? Thanks, Andrew > On 3 Nov 2020, at 18:01, Sebastian Huber > wrote: > > On 03/11/2020 18:47, Andrew Butterfield wrote: > >> $ ./waf >> Waf: Entering directory >> `/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/build' >> Build: 6.0c13e94-modified (3rd July 2020) > > This is an extremely out dated version. You should see something like this: > > Waf: Entering directory > `/home/EB/sebastian_h/src/rtems-central/modules/rtems-docs/build' > Build: 6.9628dfd (1st October 2020) > > -- > Sebastian Huber, embedded brains GmbH > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > Phone : +49 89 189 47 41-16 > Fax : +49 89 189 47 41-09 > E-Mail : sebastian.hu...@embedded-brains.de > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Problem re-building RTEMS docs
Hi Sebatian, sorry - a typo - the line was . env/bin/active as it says in the rtems-central README.md file. I was running in the venv - I just edited out all the (env) indicators... > On 3 Nov 2020, at 17:59, Sebastian Huber > wrote: > > On 03/11/2020 18:47, Andrew Butterfield wrote: > >> cp git-hooks/sanity-check.sh .git/hooks/pre-push >> git submodule update >> make env >> env/bin/activate > > This doesn't active the virtual environment. You need: > > source env/bin/activate > > -- > Sebastian Huber, embedded brains GmbH > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > Phone : +49 89 189 47 41-16 > Fax : +49 89 189 47 41-09 > E-Mail : sebastian.hu...@embedded-brains.de > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Problem re-building RTEMS docs
not import name 'l_' from 'sphinx.locale' (/Users/butrfeld/REPOS/rtems-central/env/lib/python3.8/site-packages/sphinx/locale/__init__.py)) Waf: Leaving directory `/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/build' Build failed -> task in '/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/build/user/html/index.html' failed with exit status 2 (run with -v to display more information) ANy ideas? Note that I can run Sphinx based document builds in the ESA gitlab folders without any difficulties, and no virtual envs. Regards, Andrew > On 3 Nov 2020, at 16:10, Sebastian Huber > wrote: > > On 03/11/2020 17:00, Andrew Butterfield wrote: > >> I am trying to edit RTEMS docs to fix an error regarding large comments >> (ticket #4163). >> >> I'm working out of the rtems-doc submodule of rtems-central, >> and following instructions in the Soft Eng manual (6.1 Soft Devpt (Git users) >> >> I have created a branch and edited rtems-docs/eng/coding-80cols.rts >> >> Before creating/emailing patches, I want to rebuild the eng document. >> >> However ./waf configure fails in rtems-docs >> >> :- ./waf configure >> Waf: The wscript in '/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs' >> is unreadable >> Traceback (most recent call last): >> ... stuff deleted >> File >> "/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/common/conf.py", >> line 86, in >> import sphinx_rtd_theme_rtems >> File >> "/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/common/sphinx_rtd_theme_rtems/__init__.py", >> line 9, in >> import sphinx >> ImportError: No module named sphinx >> >> I tried messing around with python/pip versions, virtual environments, >> and using pip(3) to re-install sphinx and sphinxcontrib-bibtex. >> >> Pip can see these packages - why can't waf? > > This is strange. I use the virtual environment of rtems-central to build the > docs. Did you activate the virtual environment? What is the output of > > which python > > ? > > -- > Sebastian Huber, embedded brains GmbH > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > Phone : +49 89 189 47 41-16 > Fax : +49 89 189 47 41-09 > E-Mail : sebastian.hu...@embedded-brains.de > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Problem re-building RTEMS docs
Dear all, I am trying to edit RTEMS docs to fix an error regarding large comments (ticket #4163). I'm working out of the rtems-doc submodule of rtems-central, and following instructions in the Soft Eng manual (6.1 Soft Devpt (Git users) I have created a branch and edited rtems-docs/eng/coding-80cols.rts Before creating/emailing patches, I want to rebuild the eng document. However ./waf configure fails in rtems-docs :- ./waf configure Waf: The wscript in '/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs' is unreadable Traceback (most recent call last): ... stuff deleted File "/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/common/conf.py", line 86, in import sphinx_rtd_theme_rtems File "/Users/butrfeld/REPOS/rtems-central/modules/rtems-docs/common/sphinx_rtd_theme_rtems/__init__.py", line 9, in import sphinx ImportError: No module named sphinx I tried messing around with python/pip versions, virtual environments, and using pip(3) to re-install sphinx and sphinxcontrib-bibtex. Pip can see these packages - why can't waf? :- pip list Package Version - --- ... Sphinx3.3.0 sphinxcontrib-applehelp 1.0.1 sphinxcontrib-bibtex 1.0.0 sphinxcontrib-devhelp 1.0.1 sphinxcontrib-htmlhelp1.0.2 sphinxcontrib-jsmath 1.0.1 sphinxcontrib-qthelp 1.0.2 sphinxcontrib-serializinghtml 1.1.3 ... This is on OS X Catalina All suggestions welcome Best regards, Andrew -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: RTEMS big comment conventions
Hi Gedare, thanks for your analysis and comments! > On 22 Oct 2020, at 17:22, Gedare Bloom wrote: > > For standalone tools it is really your choice. We would prefer > adoption of an easily maintained style consistent with some kind of > sane default. Given that Promela is based on C with the same comment syntax, I am happy to adopt the RTEMS C/C++ comment standards for my files. Regards, Andrew -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: RTEMS big comment conventions
Hi Joel, > On 22 Oct 2020, at 17:13, Joel Sherrill wrote: > > Please not the first. Looks like a documentation bug to me. Phew! I was hoping for that response. > > Please feel free to submit a patch and ticket for this. Sure - thing - so now I will have to look at the how-tos for these . Ticket first, then patch, I assume. Regards, Andrew -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
RTEMS big comment conventions
Dear all, In the RTEMS Software Engineering manual, Sec 6.3.2.1 https://docs.rtems.org/branches/master/eng/coding-80cols.html#breaking-long-lines it recommends excessively long comments be broken as follows: /* first line * second line * third, and in this case last line */ In Sec 6.3.5.2 https://docs.rtems.org/branches/master/eng/coding-file-hdr.html#fileheadercopyright we see a copyright and license header which uses the following format convention: /** * first line * second line * third, and in this case last line */ Most RTEMS code I look at seems to follow this second approach, or the following with only one asterisk on the first line - particularly the comments that are used to generate Doxygen docs. /* * first line * second line * third, and in this case last line */ PS - I prefer this secon/third approach, particularly when the large comment immediately precedes code. I am developing code (C and Promela) for the qualification activity, and want to start to get this right - so which should I use? Regards, Andrew Butterfield Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Build fail on debian - Toolset build error
Hi Karel, I have no idea what's wrong. If I ask nicely: :- which python2 /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 :- python2 --version Python 2.7.18 all seems well. I have has this problem before and usually I just purge all "brew" versions of python, and perhaps re-install/update the command line tools from x-code - then all works fine. Right now my Mac reports my X-code and command line tools as up to date. When it is checking for python - what is the check? How does it determine "usability"? It's not simple presence of the binary. Currently I have three python2s: :- type -a python2 python2 is /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 python2 is /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 python2 is /usr/local/bin/python2 The first one an the $PATH is the one the tool builder doesn't like. :- type python2 python2 is hashed (/Library/Frameworks/Python.framework/Versions/2.7/bin/python2) Thanks, Andrew > On 12 Oct 2020, at 11:21, Karel Gardas wrote: > > On 10/12/20 12:17 PM, Andrew Butterfield wrote: >> Dear all, >> I am having a problem building RTEMs master, on OS X Mojave - see below > > checking whether to use python... > /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 > checking for python... no > configure: error: no usable python found at > /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 > > Something wrong with your python2 install? E.g. gdb needs python2 and if > you don't have it, it'll fail which will fail tools compile which will > fail whole rtems compile... > > Cheers, > Karel > >> >>> Begin forwarded message: >>> >>> *From: *Sebastian Huber >> <mailto:sebastian.hu...@embedded-brains.de>> >>> *Subject: **Re: Build fail on debian - Toolset build error* >>> *Date: *12 October 2020 at 10:48:17 IST >>> *To: *Andrew Butterfield >> <mailto:andrew.butterfi...@scss.tcd.ie>> >>> >>> Hello Andrew, >>> >>> could you please forward this e-mail to devel@rtems.org >>> <mailto:devel@rtems.org>. >>> >>> On 12/10/2020 11:45, Andrew Butterfield wrote: >>>> Hi Sebastian, >>>> >>>> I get a python error - despite using the virtual environment, >>>> which maps `python` to the OS X \System installation of python 3.8 >>>> >>>> It complains about python2 being unusable - see tail of report below... >>>> >>>> My command-line tools and Xcode are up-to-date. Now this is on a >>>> Mojave machine, which is >>>> one that is not listed in the User Manual where OS X is discussed. >>>> >>>> I'll try to do this on my laptop which is now Catalina >>>> >>>> Regards, Andrew >>>> >>>> tail of error report follows: >>>> >>>> checking for library containing socketpair... none required >>>> checking for ld used by GCC... >>>> /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ld >>>> checking if the linker >>>> (/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ld) >>>> is GNU ld... no >>>> checking for shared library run path origin... done >>>> checking for iconv... yes >>>> checking how to link with libiconv... -liconv >>>> checking for iconv declaration... >>>> extern size_t iconv (iconv_t cd, char * *inbuf, size_t >>>> *inbytesleft, char * *outbuf, size_t *outbytesleft); >>>> checking for library containing waddstr... -lncurses >>>> checking for library containing tgetent... none required >>>> checking size of unsigned long long... 8 >>>> checking size of unsigned long... 8 >>>> checking size of unsigned __int128... 16 >>>> checking for library containing dlopen... none required >>>> checking whether to use expat... yes >>>> checking for libexpat... yes >>>> checking how to link with libexpat... -lexpat >>>> checking for XML_StopParser... yes >>>> checking whether to use MPFR... auto >>>> checking for libmpfr... no >>>> configure: WARNING: MPFR is missing or unusable; some features may be >>>> unavailable. >>>> checking whether to use python... >>>> /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 >>>> checking for python... no >>>> configure: error: no usable python found at >>>> /Library/F
Fwd: Build fail on debian - Toolset build error
Dear all, I am having a problem building RTEMs master, on OS X Mojave - see below > Begin forwarded message: > > From: Sebastian Huber > Subject: Re: Build fail on debian - Toolset build error > Date: 12 October 2020 at 10:48:17 IST > To: Andrew Butterfield > > Hello Andrew, > > could you please forward this e-mail to devel@rtems.org. > > On 12/10/2020 11:45, Andrew Butterfield wrote: >> Hi Sebastian, >> >> I get a python error - despite using the virtual environment, >> which maps `python` to the OS X \System installation of python 3.8 >> >> It complains about python2 being unusable - see tail of report below... >> >> My command-line tools and Xcode are up-to-date. Now this is on a Mojave >> machine, which is >> one that is not listed in the User Manual where OS X is discussed. >> >> I'll try to do this on my laptop which is now Catalina >> >> Regards, Andrew >> >> tail of error report follows: >> >> checking for library containing socketpair... none required >> checking for ld used by GCC... >> /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ld >> checking if the linker >> (/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ld) >> is GNU ld... no >> checking for shared library run path origin... done >> checking for iconv... yes >> checking how to link with libiconv... -liconv >> checking for iconv declaration... >> extern size_t iconv (iconv_t cd, char * *inbuf, size_t >> *inbytesleft, char * *outbuf, size_t *outbytesleft); >> checking for library containing waddstr... -lncurses >> checking for library containing tgetent... none required >> checking size of unsigned long long... 8 >> checking size of unsigned long... 8 >> checking size of unsigned __int128... 16 >> checking for library containing dlopen... none required >> checking whether to use expat... yes >> checking for libexpat... yes >> checking how to link with libexpat... -lexpat >> checking for XML_StopParser... yes >> checking whether to use MPFR... auto >> checking for libmpfr... no >> configure: WARNING: MPFR is missing or unusable; some features may be >> unavailable. >> checking whether to use python... >> /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 >> checking for python... no >> configure: error: no usable python found at >> /Library/Frameworks/Python.framework/Versions/2.7/bin/python2 >> make[1]: *** [configure-gdb] Error 1 >> make: *** [all] Error 2 >> shell cmd failed: /bin/sh -ex >> /Users/butrfeld/REPOS/rtems-smp-qualification-qual/modules/rsb/rtems/build/sparc-rtems6-gdb-0295dde-x86_64-apple-darwin18.7.0-1/do-build >> error: building sparc-rtems6-gdb-0295dde-x86_64-apple-darwin18.7.0-1 >> >>> On 12 Oct 2020, at 09:19, Sebastian Huber >>> >> <mailto:sebastian.hu...@embedded-brains.de>> wrote: >>> >>> On 12/10/2020 10:14, Andrew Butterfield wrote: >>> >>>> Is there any point me trying to build on my OS X machine, or will I just >>>> get the same error? >>> It is unlikely that you get the same error. This seems to be a Debian >>> specific issue. >> >> -------- >> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 >> Lero@TCD, Head of Software Foundations & Verification Research Group >> School of Computer Science and Statistics, >> Room G.39, O'Reilly Institute, Trinity College, University of Dublin >> http://www.scss.tcd.ie/Andrew.Butterfield/ >> >> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Strong APA Scheduler : First Draft
Hi Richi, a quick answer to 1 below > On 23 Jul 2020, at 15:20, Richi Dubey wrote: > 1)Both the algorithms require the use of a FIFO Queue to support the insert > and dequeue operations. > > I believe we can use chains and use the chain_append() and combination of > _Chain_Extract and _Chain_First or just _Chain_First and node->next to > achieve the FIFO requirements. You might want to look at chain_get() - it removes the first element, so does a FIFO protocol in tandem with chain_append() Regards, Andrew > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Update to waf 2.0.19?
Hi Sebastian, this is fine by me. Regards, Andrew Sent from my iPad > On 25 Feb 2020, at 08:02, Sebastian Huber > wrote: > > Hello, > > in order to close this bug: > > https://devel.rtems.org/ticket/3569 > > I would like to update waf to the latest version 2.0.19 in: > > rtems-docs > rtems-tools > rtems-libbsd > rtems-examples > > -- > Sebastian Huber, embedded brains GmbH > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > Phone : +49 89 189 47 41-16 > Fax : +49 89 189 47 41-09 > E-Mail : sebastian.hu...@embedded-brains.de > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: SPDX License Identifier Only and Full Copy?
Hi Joel, any test files we develop (at Lero/TCD) will be generated by python tools, so we could include file level Doxygen quite easily, if that is helpful. Regards, Andrew > On 24 Feb 2020, at 12:22, Joel Sherrill wrote: > > > > On Mon, Feb 24, 2020, 6:03 AM Sebastian Huber > <mailto:sebastian.hu...@embedded-brains.de>> wrote: > Hello Andrew, > > On 24/02/2020 10:48, Andrew Butterfield wrote: > > Hi Sebastian, > > > > a quick question > > - does the Doxygen block requirement also apply to test programs > > (xxtest/init.c), > > either hand-written or model-generated? > > we currently don't use Doxygen in the tests. There is some test > documentation in the *.doc files of the test suite. I would like to > improve the test documentation with the test specification items, but > this is a future topic. > > It is probably a good approach to add some documentation to generated > files if it is available at a higher level. > > It would be good if the tests had at least file level Doxygen. But that's a > lot of retrofitting. > > Andrew may not realise that Doxygen is newer than RTEMS and that all Doxygen > comments are later additions or conversions of the previous comment format. > > -- > Sebastian Huber, embedded brains GmbH > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > Phone : +49 89 189 47 41-16 > Fax : +49 89 189 47 41-09 > E-Mail : sebastian.hu...@embedded-brains.de > <mailto:sebastian.hu...@embedded-brains.de> > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > ___ > devel mailing list > devel@rtems.org <mailto:devel@rtems.org> > http://lists.rtems.org/mailman/listinfo/devel > <http://lists.rtems.org/mailman/listinfo/devel> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: SPDX License Identifier Only and Full Copy?
Hi Sebastian, a quick question - does the Doxygen block requirement also apply to test programs (xxtest/init.c), either hand-written or model-generated? Regards, Andrew > On 24 Feb 2020, at 07:52, Sebastian Huber > wrote: > > Hello, > > I updated the File Template section: > > https://docs.rtems.org/branches/master/eng/coding-file-hdr.html > > Please have a look at it and check if it is all right for you. > > -- > Sebastian Huber, embedded brains GmbH > > Address : Dornierstr. 4, D-82178 Puchheim, Germany > Phone : +49 89 189 47 41-16 > Fax : +49 89 189 47 41-09 > E-Mail : sebastian.hu...@embedded-brains.de > PGP : Public key available on request. > > Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG. > ___ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel ---- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: SPDX License Identifier Only and Full Copy?
I like this because, 1. It tells me it is a BSD license (which the BSD license at the bottom doesn't) 2 . Then the stuff that tells me if the file is interesting (as per Joel's comment) 3. Then the license Just my thruppence worth ;-) Andrew > On 21 Feb 2020, at 14:26, Sebastian Huber > wrote: > > We can keep the BSD-2-Clause text in the file. We can also keep the @file on > the top. Example: > > /* SPDX-License-Identifier: BSD-2-Clause */ > > /** > * @file > * > * @ingroup RTEMSApplicationConfiguration > * > * @brief Evaluate Configuration Options > * > * This header file includes a couple of header files which evaluate the > * configuration options specified by the application. The macros and defines > * used to configure the system are documented in the Configuring a System > * chapter of the Classic API User's Guide. > */ > > /* > * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) > * Copyright (C) 1989, 2000 On-Line Applications Research Corporation (OAR) > * > * Redistribution and use in source and binary forms, with or without > * modification, are permitted provided that the following conditions > * are met: > * 1. Redistributions of source code must retain the above copyright > *notice, this list of conditions and the following disclaimer. > * 2. Redistributions in binary form must reproduce the above copyright > *notice, this list of conditions and the following disclaimer in the > *documentation and/or other materials provided with the distribution. > * > * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" > * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE > * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE > * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE > * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR > * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF > * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS > * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN > * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) > * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE > * POSSIBILITY OF SUCH DAMAGE. > */ > Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Software Foundations & Verification Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: RTEMS qualification and code annotations
ht only want to trigger a Frama-C verification re-run if the relevant files have been touched, for example. > - I don't like that it has issues on other hosts but if the Frama-C > community is willing > to help address that, it can be worked. What range of hosts are you considering? > I suspect that any of > these special purpose, > relatively low user base tools will have great cross host support > unless we work with them. > will not have great cross host support? Best regards, Andrew Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: RTEMS qualification and code annotations
Dear Chris, first, thanks for trying to install it ! Frama-C is one of a number of tools we are considering, so it's not a done deal. If used, it would only be applied to a small part of the codebase: typically code that is very critical, but hard to test reliably. I would expect that this code would be unlikely to change much, if at all. The contents of the annotations would have to be maintained by those familiar with the annotation language(ACSL*) and how it should be used. They would also be responsible for ensuring that any loop annotations in .c files would be revised if there was any significant code refactoring that altered the number or purpose of those loops. The annotation in the .h files capture the specification of what the code should do, as pre/post-condition pairs - once setup and validated, they shouldn't change much. Frama-C has two main components: ` frama-c` : a command line tool that does all the work, and is highly automatable `frama-c-gui` : a nice GUI that interacts with `frama-c`, and produces verification results that can be re-run from the command line. The plan is that the GUI might be used to develop/debug/validate the various annotations, but that the day-to-day use of Frama-C as part of the qualification toolset would simply involve re-running the verifications using the command-line tool, all automated. It would only be if this reported some verification failure that any action would need to be taken. This would mean that only the command-line tool would need to be installed, which might reduce the package count somewhat. A quick potted history of Frama-C was that it was developed, starting in 2010, by CEA (http://www-list.cea.fr/en/ <http://www-list.cea.fr/en/>) on top of a previous tool called CAVEAT they had that was used internally by Airbus. It was designed specifically to automate formal verification of Airbus C code, and then made available to the community at large. An issue with it is that it handles C99, but not C11, which may be a show-stopper for us. Regards, Andrew * ACSL = "ANSI C Specification Language" > On 10 Sep 2019, at 02:36, Chris Johns wrote: > > On 6/9/19 9:40 pm, Andrew Butterfield wrote: >> However, if the implementation code contains loops, then we need annotations >> in >> the code at those loops. The following, from the Frama-C ACSL Tutorial >> (https://frama-c.com/acsl_tutorial_index.html) shows the annotations >> required to >> verify the correctness of a function that finds the maximum of a sequence of >> integers. > > Am I to assume Frama-C is the analysis tool for this work? > > I have taken a look at this tool however it would be nice to get some > understanding of its history and how you see it fitting in to the RTEMS > project > and how we as a project take these annotations and maintained them. > > I see on the Frama-C website Linux is supported and so I decided see how > FreeBSD > goes. I installed ocaml for FreeBSD as a result of some configure errors with > .. > > $ pkg install ocaml ocaml-findlib > > however configure returned ... > > checking for ocamlgraph... ocamlfind: Package `ocamlgraph' not found > > This one package wants to install 118 packages some dependent on gnome, > gnome-theme, docbook, gstreamer, bash and more so I have said no to installing > them and I have decided to give up for now. The box I am using is a headless > build server. > > Chris Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
FormalRTEMS - Postdoc in formal verification of real-time OS
The School of Computer Science and Statistics in Trinity College Dublin is seeking a post-doctoral Research Fellow in the field of formal software verification, for a duration of 15-18 months, to start as soon as possible. Salary range €40k-€51.5k p.a., depending on experience and precise duration. RTEMS-SMP Qualification is an activity funded by the European Space Agency to perform pre-qualification of an upcoming release of the open-source real-time operating system RTEMS (rtems.org). This release provides support for running RTEMS on multi-core systems. Researchers from Lero, the Irish Software Research Centre are involved in a task that explores the use of formal verification techniques in this qualification process. The task is to deploy formal techniques such as model-checking and possibly theorem proving, to assist in improving the quality of qualification results in key areas. Key areas under consideration include: modelling and verifying the multicore scheduling algorithms MrsP and OMIP and key synchronisation primitives; exploring how formal methods can help with test generation, and particularly for assembly code, with coverage analysis; and probabilistic reasoning to work around testing difficulties due to lack of predictability inherent in multi-core systems. This will require the development and revision of requirements for these algorithms, development of formal models for appropriate formal tools and ways to automate, as far as is practical, the running of those tools. Two key challenges are: to produce outputs that are suitable for software qualification; while doing this in a way that is acceptable to the open-source community (rtems.org) that maintains the operating system. The ideal candidate will have a PhD in software verification with PhD and postdoctoral experience of a number of the following: formal verification tools used in industry such as Promela/SPIN,TLA+, Frama-C; formal models of concurrency; weak memory models; probabilistic modelling; refactoring code to minimise false positives from static analysis tools; software certification and qualification processes; real-time operating systems; and related topics. The position is based at Trinity College Dublin, Ireland (http://www.tcd.ie) and the research fellow will become of a member of Lero - the Irish Software Research Centre (http://lero.ie). It will also involve travel to some of the partners, as well as the the European Space Research and Technology Centre (ESTEC). The activity is being run by a consortium led by Thales Edisoft (Portugal), with partners Embedded Brains (Germany), Jena Optronik (Germany), CISTER Research Centre, ISEP (Portugal), and Trinity College Dublin (Ireland) as part of Lero, the Irish Software Research Centre. Further details, including how to apply, can be obtained from https://www.scss.tcd.ie/Andrew.Butterfield/recruitment/ESA-RTEMS-SMP-Task-3.html which will be regularly updated, or via twitter hashtag #FormalRTEMS. Application deadline, 12noon, Irish Standard Time, Wednesday, 18th September. Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
FormalRTEMS - Postdoc in formal verification of real-time OS
The School of Computer Science and Statistics in Trinity College Dublin is seeking a post-doctoral Research Fellow in the field of formal software verification, for a duration of 15-18 months, to start as soon as possible. Salary range €40k-€51.5k p.a., depending on experience and precise duration. RTEMS-SMP Qualification is an activity funded by the European Space Agency to perform pre-qualification of an upcoming release of the open-source real-time operating system RTEMS (rtems.org). This release provides support for running RTEMS on multi-core systems. Researchers from Lero, the Irish Software Research Centre are involved in a task that explores the use of formal verification techniques in this qualification process. The task is to deploy formal techniques such as model-checking and possibly theorem proving, to assist in improving the quality of qualification results in key areas. Key areas under consideration include: modelling and verifying the multicore scheduling algorithms MrsP and OMIP and key synchronisation primitives; exploring how formal methods can help with test generation, and particularly for assembly code, with coverage analysis; and probabilistic reasoning to work around testing difficulties due to lack of predictability inherent in multi-core systems. This will require the development and revision of requirements for these algorithms, development of formal models for appropriate formal tools and ways to automate, as far as is practical, the running of those tools. Two key challenges are: to produce outputs that are suitable for software qualification; while doing this in a way that is acceptable to the open-source community (rtems.org) that maintains the operating system. The ideal candidate will have a PhD in software verification with PhD and postdoctoral experience of a number of the following: formal verification tools used in industry such as Promela/SPIN,TLA+, Frama-C; formal models of concurrency; weak memory models; probabilistic modelling; refactoring code to minimise false positives from static analysis tools; software certification and qualification processes; real-time operating systems; and related topics. The position is based at Trinity College Dublin, Ireland (http://www.tcd.ie) and the research fellow will become of a member of Lero - the Irish Software Research Centre (http://lero.ie). It will also involve travel to some of the partners, as well as the the European Space Research and Technology Centre (ESTEC). The activity is being run by a consortium led by Thales Edisoft (Portugal), with partners Embedded Brains (Germany), Jena Optronik (Germany), CISTER Research Centre, ISEP (Portugal), and Trinity College Dublin (Ireland) as part of Lero, the Irish Software Research Centre. Further details, including how to apply, can be obtained from https://www.scss.tcd.ie/Andrew.Butterfield/recruitment/ESA-RTEMS-SMP-Task-3.html which will be regularly updated, or via twitter hashtag #FormalRTEMS. Application deadline, 12noon, Irish Standard Time, Wednesday, 18th September. Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: Formal Verification within the ESA funded RTEMS-SMP qualification activity
Hi Joel, some quick (off the cuff) responses to your Qs: > > Assuming formal verification benefits from modular decomposition like software > construction and admitting I don't know how you plan to go about this, I would > tend to look at the APIs of interest and then look at what score > objects/algorithms > yield the most cross-coverage. Assuming you benefit from "inheriting" the > analysis of a major supporting component. Yes - FV definitely benefits from good modular decomposition - in the fact the parallels with good software modularity are very close. > > Certainly scheduler and threadq algorithms are high on the list. Would > starting > with rbtree formal verification be a strong foundation? That is used in at > least > some scheduling algorithms (EDF SMP being one), priority blocking in the > thread queue, timers/timeouts/delays, and RB Heap. I would assume that once > the RBTree is verified, it lends to easing verifying the users of it I > just listed. Yes and no. To formally verify RBtrees we need 3 things: (1) The RBTree code. (2) A formal semantics for the programming language (3) A formal specification for the behaviour of RBtrees Given all three, we can then, in principle at least, formally verify the code correctness. In order to formally verify a scheduler while also gaining advantage of code modularity, we would take the scheduler code, apply our formal code semantics, but whenever we encountered a call to a RBtree operation, we would replace that by the formal specification (3 above) of the RBtree, rather than the formal semantics of the RBTree code. So given a formal specification of RBTrees, we can (A) use it as a basis for verifying RBTree code correctness (B) use it as an assumption (that RBtree code is correct) in formally verifying any other code that uses RBtrees. We cannot formally verifying everything, not within the scope of this project, at least. So we have to ask the following hard Q: Given that I have a formal model of some API operation, should I but effort into formally verifying that its implementation is correct, or into formally verifying clients of the API, under the assumption that the formal API model is what is actually implemented? There is no clear cut answer, but it is worth asking the following question about the API: Do I need to go to the bother of formally verifying this API operator's code, or is plain good old traditional testing good enough to make a convincing case for its correctness? Formally verifying data structures and their operations generally makes for nice projects, as they are often straightforward, so it is tempting to do these. In fact one the big areas where good synergy comes from combining FV and testing is precisely when we have parts easy to test well (maybe hard to do FV) and other parts very hard to test (poor controllability/non-deterministic), but quite amenable to formal reasoning. The parts that are well tested are then coded into formal statements that those parts are correct, and those formal assumptions support the proof of the correctness of the other parts. > > Otherwise, I could see working a lot on the EDF SMP scheduling algorithm > and it having little benefit on the other users of the RBTree. And as a > starting > point, if it uses an RB Tree (except RBHeap), I would consider it a > core capability. This builds a good case for wanting to be really sure that their implementation is correct, indeed. > > Looking from the bottom up, focusing on the score mutex behaviors may cover > the algorithmic case for the Classic and POSIX API uses. But even the POSIX > API > mutex has a handful of behaviors to account for so you can't just wave > your hands > at that and say too complex. There is no portable API that I know of > that separates > mutexes based on the blocking and priority inversion avoidance protocol. A key issue here is the multi-core/SMP part. If all of this was single-core, life would be relatively easy, but we are faced with a lot of non-deterministic behaviour (cache behavour, weak memory models) that we have to reason about, and this is intimately related with the synchronisation primitives and the scheduling. > > Andrew.. beyond focusing on what we think we think are the core areas, > what areas > have previously been the focus in OS formal verification? Any > academic papers giving hints there? Yes - I'll get back to you on this later > Regards, Andrew Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ---
Formal Verification within the ESA funded RTEMS-SMP qualification activity
Dear RTEMS developers, qualifiers, I am involved with the ESA funded RTEMS (SMP) qualification activity, and I, with colleagues, will be exploring how formal verification techniques can help. We will not "formally prove" all of RTEMS, but will focus on critical parts of the code, particularly those parts that are hard to test. The planning underway is looking at two key aspects of the work to be done: (1) Which algorithms/code should we consider? (2) How should we do the formal verification so we get the best results with least effort and disruption to users and developers. This email focusses from here onwards on (1) above. I'll get back later regarding (2). The following suggestions have been made for code and other design artefacts that we should consider: - The key scheduler algorithms: MrsP, OMIP - Synchronisation primitives incl. C11 Atomics - The assembly code portions - RTEMS API specifications Any other suggestions? Sebastian Huber has pointed me at the following source files: https://git.rtems.org/rtems/tree/cpukit/score/include/rtems/score/schedulersmpimpl.h https://git.rtems.org/rtems/tree/cpukit/score/include/rtems/score/threadq.h#n393 https://sourceware.org/git/gitweb.cgi?p=newlib-cygwin.git;a=blob;f=newlib/libc/sys/rtems/include/sys/lock.h;h=ec3415a5222f6ac055d5041aaf44970fd212c600;hb=HEAD https://git.rtems.org/rtems/tree/cpukit/score/src/threadqenqueue.c https://git.rtems.org/rtems/tree/cpukit/score/src/threadqops.c https://git.rtems.org/rtems/tree/bsps/sparc/shared/start/start.S https://git.rtems.org/rtems/tree/cpukit/score/cpu/sparc/cpu_asm.S https://git.rtems.org/rtems/tree/cpukit/score/cpu/sparc/syscall.S https://git.rtems.org/rtems/tree/cpukit/score/cpu/sparc/window.S Anything that should be added? Regards, and thanks, Andrew Butterfield -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: RTEMS Software Coding Standard
Hi Joel, unfortunately, Taster is closed-source, so that won't help. I'll see what output I can get out of Frama-C and its open-source plugins. Regards, Andrew > On 25 Jul 2019, at 10:37, Andrew Butterfield > wrote: > > Hi Joel, > > a quick answer: > >> On 24 Jul 2019, at 18:23, Joel Sherrill wrote: >> >> Random question: Does Frama-C offer anything here? > > I've found a Frama-C plugin called "Taster" that does this - seems to be > built around Airbus coding standards. > I'll do a bit more digging into this later today. > > Regards, Andrew > > ---- > Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 > Lero@TCD, Head of Foundations & Methods Research Group > School of Computer Science and Statistics, > Room G.39, O'Reilly Institute, Trinity College, University of Dublin > http://www.scss.tcd.ie/Andrew.Butterfield/ > ------------ > Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
Re: RTEMS Software Coding Standard
Hi Joel, a quick answer: > On 24 Jul 2019, at 18:23, Joel Sherrill wrote: > > Random question: Does Frama-C offer anything here? I've found a Frama-C plugin called "Taster" that does this - seems to be built around Airbus coding standards. I'll do a bit more digging into this later today. Regards, Andrew -------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ ___ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
