Formal Verification within the ESA funded RTEMS-SMP qualification activity

[Joel Sherrill]

On Wed, Aug 28, 2019 at 12:50 AM Sebastian Huber
<sebastian.huber at embedded-brains.de> wrote:
>
> Hello Andrew,
>
> On 27/08/2019 16:58, Andrew Butterfield wrote:
> > 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
>
> I think that formal verification of SPARC assembly code will not give a
> huge return of investment. SPARC is an obsolete architecture. The
> context switching and interrupt handling is complicated and exotic due
> to the register windows. Register windows are not present in any state
> of the art architecture.
>
> >   - RTEMS API specifications
> >
> > Any other suggestions?
>
> The scheduler operations in general could be a useful area for formal
> verification, e.g. the scheduler set affinity, pin and unpin operations.
> Several scheduler operations are involved in the locking protocols, e.g.
> the scheduler ask for help, withdraw node and reconsider help request.
>
> Another areas are the data structures such as the chain and red-black trees.
>
> A specification of the Classic API is difficult. For example we have:
>
> rtems_status_code rtems_semaphore_obtain(
>    rtems_id        id,
>    rtems_option    option_set,
>    rtems_interval  timeout
> );
>
> How do you know during static analysis to which object the id (a 32-bit
> integer) maps? It could be a
>
> * counting semaphore,
>
> * a binary semaphore,
>
> * a mutex with priority inheritance (OMIP),
>
> * a mutex with priority ceiling, or
>
> * a mutex with MrsP.

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.

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.

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.

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.

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?

--joel


>
> This is one of the reasons for introducing an API for self-contained
> objects:
>
> https://docs.rtems.org/branches/master/c-user/self_contained_objects.html
>
> The focus of the ESA pre-qualification project is the Classic API:
>
> https://ftp.rtems.org/pub/rtems/people/sebh/tn-space-profile-r2-18072019.pdf
>
> --
> 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.huber at embedded-brains.de
> PGP     : Public key available on request.
>
> Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG.
> _______________________________________________
> devel mailing list
> devel at rtems.org
> http://lists.rtems.org/mailman/listinfo/devel