RTEMS qualification and code annotations

[Joel Sherrill]

On Wed, Sep 11, 2019 at 7:59 AM Andrew Butterfield
<Andrew.Butterfield at scss.tcd.ie> wrote:
>
> Hi Joel,
>
>  thanks for a very detailed and comprehensive response.
>
> Some of the issues you raise here are very high level,
> for the consortium and community to discuss/agree at a high level.
>
> For now I will just focus on the issue of annotations and the kinds of
> tools that might be involved.
>
> I have inlined responses below
>
> > On 10 Sep 2019, at 14:56, Joel Sherrill <joel at rtems.org> wrote:
> >
> > I don't like to top post but in this case I hope this is OK.
> >
> > This is a very challenging area from a project integration
> > perspective. There are a handful
> > of issues which we will have to figure out how to address. I think
> > these also apply to other
> > annotations like requirements and licensing annotation
> >
> > + Annotation
> >   - Standards based?
>
> Not as far as I can tell - ACSL used by Frama-C is their own invention
>
> >     - For example, will we add annotation for a scanner like Coverity?
>
> These seem to be limited to suppressing warnings deemed to be false positives.
> We are inclined to take the JPL approach to false positives which involves re-writing
> the code so they go away.

I generally agree with that approach. If the code confuses the
scanner, it usually
can be simplified to be less likely to confuse a human.

FWIW most of the Coverity issues we have now are not in the core threading
or file systems. There are two in the score in threadqops.c (CID 1399744)
and objectextendinformation.c (CID 26033). I don't see any in rtems/, sapi/
or posix/ and a few in libcsupport/. Most appear to be in libmisc, particularly
in the shell which is full of third party code.


> >   - Invasive/Intruding/Bulk
>
> Yes - as my example shows. A good configurable editor might be able
> to do syntax highlighting that makes life easier, but that may not suit a lot of people

Whatever is decided, the bigger issue is maintenance.

We have also discussed tagging files which meet a certain level of rigor.
If it has annotations in it, that would be nice to easily know. The idea
was that we would have tiers and increasing levels of rigor associated
with touching a file.

But the annotation needs to be a core competency of the core developer
community. Otherwise it will bitrot. We don't want to wait for someone to
let a contract to update it.

> >   - In source file or separate
>
> This is the key question to answer - you express an opinion below,
> and I'll respond more fully down there.
> But, in passing,
> what happens if we want to put several annotations from different tools
> at the same source code location?

Oh. That is awful. I can see your point to providing a mechanism to
have annotation for multiple tools.

> > + Supporting Tools
> >   - Free, Libre and Open Source Software
>
> Frama-C - yes, LGPLv2
>
> >   - Upstream Project not dead
>
> Frama-C is still actively maintained and upgraded.
>
> >   - Wide Host Support
> >      - On other cases, have accepted that not all hosts can run the tool
>
> I have installed it on Debian and OS/X. It claims availability for Linux, OS X and Windows

With that as a base, perhaps FreeBSD isn't so far off. Just a matter
of interacting with them.


> >
> > + Maintenance
>
>  Of annotations, I assume.
> >  - Availability of Knowledgeable Developers
>
>  Yes - initially they would come from our consortium, myself, and the research fellow
>  who I hope to recruit.
>  I plan to hang around after this activity is over to keep an eye on things,
> and hopefully others will get some feeling and expertise for them over time.

Thinking out loud, I personally am not opposed to learning this type of thing.
But I don't have time for a big course (assuming the local universities had
someone who can teach it), much less a degree in formal methods.
A quick path to some basic level of competency would be really appreciated
so we can learn and encourage the community.

> This is why stable + critical code is a good place to start.

+1

> >  - Running Checks as part of Continuous Integration (pre-check ideal)
>
> This is key for us as well - Frama-C has a comprehensive command-line system,
> and seems to have been tailored to make it easy to automatically re-run verifications.
> Even when the GUI is used to develop them, they are automatically stored in
> a way that allows the to re-run from the command line.

Good. But I am equally concerned about rtems.org CIT setup side. Our sysadmin
is volunteer and unfortunately has never gotten any sponsorship to install or
upgrade anything.

This needs to be in the public facing rtems.org project infrastructure

> >  - Automated notification of need to update and tracking system
>
> If the C code changes, but the annotations, that need to change accordingly, don't,
> then the re-run of the verification will fail.

And then we have the find a maintainer issue. :)

We can't block improvements if annotation is out of date. So this may
just be a problem we have to battle and/or accept.

> >
> > I suggested some guidance in the Software Engineering Guide on broad
> > tool review
> > criteria (FLOSS, etc) with a section/chapter on each type of tool we
> > use (e.g. requirements
> > for source code control and why git).
> >
> > I  am pretty sure someone has already used Frama-C on RTEMS. Perhaps
> > contact the Frama-C
> > folks and ask.
>
> > I met one of their core folks at a conference a few
> > years and he mentioned it.
> > Perhaps asking their community about this may turn up something.
> >
>
> I've emailed their key contacts - still awaiting a reply.
> A goggle search uncovered an MSc thesis from University of Beira Interior in Portugal,
> using Frama-C to verify part of an operating system (xLuna) that was a fusion of RTEMS and Linux.

I have vague recollection that this was ESA or Airbus sponsored. Portugal may
be right as the country of origin though. Wish I remembered him. :(

> > I'm just trying to make sure we ask all the right questions. Andrew
> > covered some of them
> > in great detail.
> >
> > My first thoughts are:
> >   - Frama-C seems to be fairly well accepted and meets FLOSS requirement
> >   - Is ACSL standard?  Supported by anything besides Frama-C?
> >   -  Annotation needs to be in the source files or it is
> > unmaintainable IMO. I don't want a
> >      special tool to merge source. There will end up being annotation
> > in the source file anyway.
>
> Yes - I can see why you prefer this - my tagging idea does have a number
> of risks associated with it - it also separates the annotation text from the annotated code,
> making it difficult to check them side-by-side.
>
> Perhaps the initial approach, should we use Frama-C, on a few key source files,
> is to add the annotations in to the file as you recommend.
> It may be quite workable in reality.
>
> If later on we encounter difficulties with code size/clarity, we could consider a tagged system
>
> >   - Any tool like this has to be part of the currently immature
> > pre-commit checks and Continuous
> >     Integration Testing at rtems.org.
>
> yes  - that should be easy to do - I don't what kind of performance issue might arise.
> We might only want to trigger a Frama-C verification re-run if the relevant files have been touched,
> for example.

Our tagging idea would be useful here.

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

>From memory, the core developers tend to use Linux (Centos, Ubuntu, or
SUSE I think),
FreeBSD, MacOS, and Windows.

The RTEMS.org server infrastructure is FreeBSD. Hence the concern
for lack of FreeBSD support.

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

Sorry, will not support much more than Ubuntu and Windows.

It is increasingly common to find open source packages that won't
compile for anything but Linux.

>
> Best regards,
>   Andrew
>
> --------------------------------------------------------------------
> Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
> Lero at 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/
> --------------------------------------------------------------------
>