using docker to deliver qualification tools

[Andrew Butterfield]

Hi Joel,

thanks for your prompt reply and definitive answer. It helps to have clear
boundaries regarding what is feasible or not.

It's taken me a while to get back - I understand that you, Chris and Sebastian discussed this,
and I recently had a good phone call with Sebastian where we discussed this issue.

First, reproducible is good - I quite agree. 
Docker/Ansible(*) can help here but I quite understand why it has to be a third-party thing,
rather than part of RTEMS proper.

From the perspective of using formal verification tools, there are two broad approaches we could take:

The first approach is to use formal models (of requirements and/or specifications) in a behind the scenes way
to produce tests. These tests would be deployed to RTEMS just like any other tests from other
sources, and would be amenable to code review.

The models and any tools use to produce these test would not be part of RTEMS proper,
but we would make them freely available for those who are interested.

This is the least intrusive way to reap the benefits of formal modelling of RTEMS requirements.

The second approach is when we want to use a formal tool to analyse RTEMS code,
ideally as part of a standard CI/regression testing process.
This would require us to ensure that such tools had a "reasonably sized" footprint.
One possible candidate for this, Frama-C, seems a bit large, but we may be able to produce
a stripped-down command-line version with a smaller footprint.

Another  issue that was raised is the use of source-code annotations to assist some tools. 
It is clear that this will only make sense in the long-term if there is a plan to ensure
long-term maintenance of these, or else "logic-rot" will set in. I intend to stay around
as part of the RTEMS community after this project is over to watch over things, but I
think we'd all prefer if we could build a group of formal enthusiasts willing to help.

Currently we feel we should start with approach 1 - see how far this can go.
Approach 2 requires us to do some thinking and work.
Annotation should be deferred until we can have a convincing long-term maintenance plan.

Hope this helps,

 Best regards, Andrew


(*) thanks, Stanislav!

> On 24 Oct 2019, at 13:00, Joel Sherrill <joel at rtems.org> wrote:
> 
> 
> 
> On Thu, Oct 24, 2019, 5:58 AM Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie> wrote:
> Dear RTEMS users,
> 
>  give that the RTEMS-SMP qualification project requires a lot of new
> tooling, some very standard, some more experimental, we have a proposal
> that we distribute these using Docker CE (Community Edition).
> 
> This will make it easier for users to install only the parts that they
> are interested in, and also makes it possible for us to host the
> tools in the cloud somewhere as an on-line qualification service.
> 
> What are the thoughts of the community regarding this?
> 
> I don't care what ESA does after the work is delivered for their own internal use. But requiring a Docker instance for community qualification work is unacceptable to me. It is a Linux specific technology and that violates a few key tenets of the RTEMS project.
> 
> Host Independence and Reproducible being the top two.
> 
> Instructions on how to build the environment are key. This includes what to install with pop or with the RSB or as a host package.
> 
> If a user wants a pre-configured VM or container that's their business. I personally don't think it is configuration controlled enough under the auspices of the project and even if used must be under the end user system's control to be able to pass a qualification audit.
> 
> Think reproducible
> 
> 
> 
> 
> Best regards,
>   Andrew Butterfield
> --------------------------------------------------------------------
> 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/
> --------------------------------------------------------------------
> 
> _______________________________________________
> users mailing list
> users at rtems.org
> http://lists.rtems.org/mailman/listinfo/users

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