RTEMS qualification and code annotations

[Andrew Butterfield]

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.

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

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

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

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

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

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