Formal Verification within the ESA funded RTEMS-SMP qualification activity

[Andrew Butterfield]

Hi Joel,

 some quick (off the cuff) responses to your Qs:

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

Yes - FV definitely benefits from good modular decomposition - in the fact the
parallels with good software modularity are very close.
> 
> 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.


Yes and no. To formally verify RBtrees we need 3 things: 
  (1) The RBTree code.

  (2) A formal semantics for the programming language
  (3) A formal specification for the behaviour of RBtrees
Given all three, we can then, in principle at least, formally verify the code correctness.

In order to formally verify a scheduler while also gaining advantage of code modularity,
we would take the scheduler code, apply our formal code semantics,
but whenever we encountered a call to a RBtree operation,
we would replace that by the formal specification (3 above) of the RBtree,
rather than the formal semantics of the RBTree code.

So given a formal specification of RBTrees, we can
 (A) use it as a basis for verifying RBTree code correctness
 (B) use it as an assumption (that RBtree code is correct) in formally verifying any other code that uses RBtrees.

We cannot formally verifying everything, not within the scope of this project, at least.
So we have to ask the following hard Q:

 Given that I have a formal model of some API operation,
 should I but effort into formally verifying that its implementation is correct,
 or into formally verifying clients of the API, under the assumption that the formal API model is what is actually implemented?

There is no clear cut answer, but it is worth asking the following question about the API:
  Do I need to go to the bother of formally verifying this API operator's code,
  or is plain good old traditional testing good enough to make a convincing case for its correctness?


Formally verifying data structures and their operations generally makes for
nice projects, as they are often straightforward, so it is tempting to do these.


In fact one the big areas where good synergy comes from combining FV and testing
is precisely when we have parts easy to test well (maybe hard to do FV)
and other parts very hard to test (poor controllability/non-deterministic),
but quite amenable to formal reasoning. The parts that are well tested
are then coded into formal statements that those parts are correct,
and those formal assumptions support the proof of the correctness of the other parts.

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

This builds a good case for wanting to be really sure that their implementation is correct, indeed.
> 
> 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.

A key issue here is the multi-core/SMP part.
 If all of this was single-core, life would be relatively easy,
but we are faced with a lot of non-deterministic behaviour (cache behavour, weak memory models) that we have to reason about,
and this is intimately related with the synchronisation primitives and the scheduling.
> 
> 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?

Yes - I'll get back to you on this later 
> 
Regards, Andrew

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