OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.

 


Help: OASIS Mailing Lists Help | MarkMail Help

virtio-comment message

[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]


Subject: Re: [virtio-comment] Formal specification of virtIO


On Tue, Nov 12, 2019 at 10:29:29AM +0000, Stefan Hajnoczi wrote:
> 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

The metamodel would contain concepts like VirtQueue and VirtIOAvailable ring, and the relation
between these concepts, e.g., "a virtqueue has a reference to a
VirtIOAvailable ring". This can be used to validate data structures. However, these are only 
syntactic relationships. A second step would be to add behavior. For example, by adding events
and causality relationships between. 

Matias


[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]