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.hu...@embedded-brains.de
PGP : Public key available on request.
Diese Nachricht ist keine geschäftliche Mitteilung im Sinne des EHUG.
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
