[virtio-comment] Formal specification of virtIO

[virtio-comment] Formal specification of virtIO

[Matias Vara]

[-- Attachment #1: Type: text/plain, Size: 705 bytes --]

Hello everyone,

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?

Regards, Matias.

[-- Attachment #2: Type: text/html, Size: 846 bytes --]

Re: [virtio-comment] Formal specification of virtIO

[Matti Moell]

Hi Matias,

I think that would be a great idea! It would have the added benefit that 
the protocol data types and structures could be used to generate header 
files so we could all have a true single information source for them 
(thinking of virtio_gen from crosvm/firecracker here).

Making a formal model part of the specification could allow generating 
some parts of the spec or at least validating the LaTeX itself against 
the model. On the other hand it might also raise the barrier to add new 
devices.

All in all, I'd be very interested to have a formal specification.

Cheers,

		Matti

On 10.11.19 15:33, Matias Vara wrote:
> Hello everyone,
> 
> 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?
> 
> Regards, Matias.
> 

This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

Re: [virtio-comment] Formal specification of virtIO

[Stefan Hajnoczi]

[-- Attachment #1: Type: text/plain, Size: 1276 bytes --]

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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: [virtio-comment] Formal specification of virtIO

[Matias Vara]

[-- Attachment #1: Type: text/plain, Size: 1899 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 2311 bytes --]

Re: [virtio-comment] Formal specification of virtIO

[Stefan Hajnoczi]

[-- Attachment #1: Type: text/plain, Size: 2249 bytes --]

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 #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: [virtio-comment] Formal specification of virtIO

[Matias Ezequiel Vara Larsen]

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

This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

[virtio-comment] Re: Formal specification of virtIO

[Matias Ezequiel Vara Larsen]

Hello,

I am investigating the possibility to use a higher-level language to
describe virtio concepts. I am writing down this research at
https://github.com/MatiasVara/virtioml. I defined a metamodel that
captures concepts and relationships between these concepts. I also built
a simple transformation to generate the headers in C. This transformation
may be extended to other languages. I am currently investigating the
possibility to model the VIRTIO_CONFIG_S_* status register state machine to verify
that a virtio driver follows the specification. To do this, I am first using
a formalism to encode the specification, and from that code, I generate
the instrumentation code that goes in the driver. The instrumentation code 
warns when the specification is violated. This is, however, a very draft work.

Regards, Matias.

On Sun, Nov 10, 2019 at 03:33:20PM +0100, Matias Vara wrote:
> Hello everyone,
> 
> 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?
> 
> Regards, Matias.

This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

Re: [virtio-comment] Formal specification of virtIO

[Michael S. Tsirkin]

On Sun, Nov 10, 2019 at 03:33:20PM +0100, Matias Vara wrote:
> Hello everyone,
> 
> 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? 
> 
> Regards, Matias.       

I think the most intersting thing to model would be the virtqueue for
systems with weak memory concurrency. Right now we have two virtqueue
formats and getting concurrency right is the hardest part.  Having a
formal model would be useful so we can extend the ring. Paul E.
McKenney's talks gave me the impression that modeling any kind of weak
memory concurrency is very challenging though.

-- 
MST


This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

Re: [virtio-comment] Formal specification of virtIO

[Matias Ezequiel Vara Larsen]

On Mon, Mar 09, 2020 at 04:03:34AM -0400, Michael S. Tsirkin wrote:
> On Sun, Nov 10, 2019 at 03:33:20PM +0100, Matias Vara wrote:
> > Hello everyone,
> > 
> > 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? 
> > 
> > Regards, Matias.       
> 
> I think the most intersting thing to model would be the virtqueue for
> systems with weak memory concurrency. Right now we have two virtqueue
> formats and getting concurrency right is the hardest part.  Having a
> formal model would be useful so we can extend the ring. Paul E.
> McKenney's talks gave me the impression that modeling any kind of weak
> memory concurrency is very challenging though.
> 

Thanks Michael for your answer. Modeling weak memory concurrency sounds very challenging.
Other possible use of a model could be to verify that an implementation follows the
specification. To do so, the model must contain information information about how 
the driver and device shall behave, e.g., set DriverOK before initialize the virtqueues.
I think this may be easier to achieve. I do not know if this is interesting though.    

Regards, Matias.
> -- 
> MST
> 

This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/