Re: [virtio-comment] Formal specification of virtIO

[Stefan Hajnoczi <stefanha@redhat.com>]

On Mon, Nov 11, 2019 at 08:07:06PM +0100, Matias Vara wrote:
> On Mon, 11 Nov 2019 at 12:34, Stefan Hajnoczi <stefanha@redhat.com> wrote:
> 
> > On Sun, Nov 10, 2019 at 03:33:20PM +0100, Matias Vara wrote:
> > > I have started to think of the formalization of the virtIO specification.
> > > Roughly speaking, I could use a formal language to "code" the virtIO
> > spec.
> > > As far as I can think, this has three benefits:
> > > 1. You can validate any implementation.
> > > 2. You can generate the implementation for a given target. For example,
> > you
> > > could be able to generate the implementation of a virtIO device in VHDL.
> > > 3. You can provide simulation and verification before any implementation.
> > > In automotive, this is interesting because you ease the certification so
> > > formalization pays off.
> > >
> > > Do you think this may be interesting work to do to become the virtIO
> > > specification more robust?
> >
> > As a starting point you could propose a formal model of an aspect of the
> > specification, like the device lifecycle VIRTIO_CONFIG_S_* status
> > register state machine (start easy!).
> >
> > It would already offer the advantages you mentioned for a subset of the
> > specification and give the community a chance to get familiar with the
> > tools and workflow.
> >
> > Even if it turns out to be impractical to formalize the entire VIRTIO
> > specification, it will certainly reveal things that can be improved in
> > the current spec.
> >
> > Stefan
> >
> 
> Thanks for the comments. First, I would capture data structures by using a
> metamodel. This would allow generating the structures depending on the
> target language, e.g., C, Rust, Latex. To do this, it is needed a
> model-to-text transformation. Then, I would base on a subset of the
> specification to describe the behavior by using a formal language. The
> VIRTIO_CONFIG_S_* status register state machine may be a good candidate for
> starting. I will keep you updated on the progress.

By the way, the virtqueue is the most interesting aspect of VIRTIO.
Formalizing the split and packed virtqueue layouts would do the most to
ensure correctness.  They are non-trivial though :).

Stefan

Attachment: signature.asc
Description: PGP signature