[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]