Formal Verification within the ESA funded RTEMS-SMP qualification activity

[Sebastian Huber]

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.

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.