Formal Verification within the ESA funded RTEMS-SMP qualification activity

[Andrew Butterfield]

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
 - RTEMS API specifications 

Any other suggestions?

Sebastian Huber has pointed me at the following source files:

https://git.rtems.org/rtems/tree/cpukit/score/include/rtems/score/schedulersmpimpl.h
https://git.rtems.org/rtems/tree/cpukit/score/include/rtems/score/threadq.h#n393
https://sourceware.org/git/gitweb.cgi?p=newlib-cygwin.git;a=blob;f=newlib/libc/sys/rtems/include/sys/lock.h;h=ec3415a5222f6ac055d5041aaf44970fd212c600;hb=HEAD
https://git.rtems.org/rtems/tree/cpukit/score/src/threadqenqueue.c
https://git.rtems.org/rtems/tree/cpukit/score/src/threadqops.c

https://git.rtems.org/rtems/tree/bsps/sparc/shared/start/start.S
https://git.rtems.org/rtems/tree/cpukit/score/cpu/sparc/cpu_asm.S
https://git.rtems.org/rtems/tree/cpukit/score/cpu/sparc/syscall.S
https://git.rtems.org/rtems/tree/cpukit/score/cpu/sparc/window.S

Anything that should be added?

Regards, and thanks, 

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