On Wed, Aug 28, 2019 at 12:50 AM Sebastian Huber <sebastian.hu...@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.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 _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
