Re: [virtio-comment] [virtio-queue] CLARIFICATION: "free descriptors" External

[Jasper Haag <jasper@bedrocksystems.com>]

Thanks for the concise response. It seems clear to us at BedRock Systems

that our VIRTIO Queue operational model will need to support aliasing of

both descriptor entries and payload memory.

For now we are focusing on making such updates to our operational model.

We will follow up with any other clarification questions which arise.

Your responsiveness has been much appreciated.

~Jasper

On Mon, Oct 23, 2023 at 7:21âAM Michael S. Tsirkin <mst@redhat.com> wrote:

On Fri, Oct 20, 2023 at 01:35:00PM -0400, Jasper Haag wrote:
> Folks,
>
> Thank you kindly for the thoughtful responses! From the point of view
> of formal modelling/verification I think there is a lot of benefit to be had
> from tightening the language in the VIRTIO specification. I also think
> that the formal methods work we do at BedRock Systems puts us in a
> position to contribute on this front - although I need to coordinate with
> my managers regarding the logistics of such contributions, including sponsoring
> membership(s) to the "OASIS Virtual I/O Device (VIRTIO) Technical Committee"
> <https://www.oasis-open.org/committees/membership.php?wg_abbrev=virtio>.
>
> > Maybe we should add some text like "free entries in the
> > descriptor table, henceforth referred to as 'free descriptors'".
> This clarified text seems like an improvement, but it still leaves some
> open questions in my mind - which Michael's response helps to tease
> out.
>
> > Yes I think descriptors means free entries in the descriptor table.
> > I don't think the MUST there is right - in theory
> > I think the same descriptor chain can be used by multiple
> > buffers, though I am not aware of any drivers that do this.
> Overall, we're interested in understanding the ownership discipline
> involved with the descriptor-entry/payload "resources" (in the sense of
> linear logic). Our operational model will need to codify this discipline in
> order to track/cede ownership of these "resources" at the appropriate
> times, and aliasing will complicate the story here. To wit:
> 1) If a Device owns two buffers which alias each other's descriptors, and
> Â Âsends one of the buffers back to the Driver, does the Device still own
> Â Âthe other buffer it hasn't yet returned, including the buffer's descriptors?
> 2) If a Device owns two buffers which alias payload memory, and sends one
> Â Âof the buffers back to the Driver, does the Device still own the payload
> Â Âmemory referred to by the buffer it hasn't yet returned?

I would say yes.

> Along these lines, a few clarifications:
> i) Â Are Drivers allowed to alias descriptor chain suffixes, or only complete
> Â Â Âdescriptor chains?
> ii) ÂMay a Driver /simultaneously expose/ multiple buffers which share
> descriptor
> Â Â Âchain (suffixes)?
> iii) May a Driver /simultaneously expose/ multiple buffers which (partially)
> alias
> Â Â Âthe same payload memory?

Nothing seems to disallow this. iii actually happens sometimes.

>
> I look forward to continuing this discussion.
>
> ~Jasper
>
> On Fri, Oct 20, 2023 at 7:12âAM Michael S. Tsirkin <mst@redhat.com> wrote:
>
>Â Â ÂOn Fri, Oct 20, 2023 at 12:38:47PM +0200, Cornelia Huck wrote:
>Â Â Â> On Thu, Oct 12 2023, Jasper Haag <jasper@bedrocksystems.com> wrote:
>Â Â Â>
>Â Â Â> > To whom it may concern,
>Â Â Â> >
>Â Â Â> > BedRock Systems is working to formally model VIRTIO Queues and formally
>Â Â Â> > verify our implementation of VIRTIO Queues <
>Â Â Â> > https://github.com/bedrocksystems/vml/tree/main/devices/virtio_base>.
>Â Â ÂOne
>Â Â Â> > question which we've been unable to answer solely using the Standard
>Â Â Âtext
>Â Â Â> > relates to "free descriptors" - as referred to within "2.7.13 -
>Â Â ÂSupplying
>Â Â Â> > Buffers to The Device" <
>Â Â Â> > https://docs.oasis-open.org/virtio/virtio/v1.2/csd01/
>Â Â Âvirtio-v1.2-csd01.html#x1-6400013>.
>Â Â Â> > In particular, the text states:
>Â Â Â> >
>Â Â Â> > | 2.7.13 - Supplying Buffers to The Device
>Â Â Â> > | The driver offers buffers to one of the deviceâs virtqueues as
>Â Â Âfollows:
>Â Â Â> > |Â Â Â1. The driver places the buffer into free descriptor(s) in the
>Â Â Â> > descriptor table, chaining as necessary (see 2.7.5 The Virtqueue
>Â Â ÂDescriptor
>Â Â Â> > Table).
>Â Â Â> > |Â Â Â .....
>Â Â Â> > |
>Â Â Â> > | 2.7.13.1 - Placing Buffers Into The Descriptor Table
>Â Â Â> > | A buffer consists of zero or more device-readable
>Â Â Âphysically-contiguous
>Â Â Â> > elements followed by zero or more physically-contiguous device-writable
>Â Â Â> > elements (each has at least one element).
>Â Â Â> > | This algorithm maps it into the descriptor table to form a descriptor
>Â Â Â> > chain:
>Â Â Â> > | for each buffer element, b:
>Â Â Â> > |Â Â Â1. Get the next free descriptor table entry, d
>Â Â Â> > |Â Â Â2. Set d.addr to the physical address of the start of b
>Â Â Â> > |Â Â Â3. Set d.len to the length of b.
>Â Â Â> > |Â Â Â4. If b is device-writable, set d.flags to VIRTQ_DESC_F_WRITE,
>Â Â Â> > otherwise 0.
>Â Â Â> > |Â Â Â5. If there is a buffer element after this:
>Â Â Â> > |Â Â Â Â Âa. Set d.next to the index of the next free descriptor
>Â Â Âelement.
>Â Â Â> > |Â Â Â Â Âb. Set the VIRTQ_DESC_F_NEXT bit in d.flags.
>Â Â Â> > | In practice, d.next is usually used to chain free descriptors, and a
>Â Â Â> > separate count kept to check there are enough free descriptors before
>Â Â Â> > beginning the mappings.
>Â Â Â> >
>Â Â Â> > However, the term "free descriptor" doesn't appear to be defined
>Â Â Âanywhere
>Â Â Â> > within the Standard text. What characterizes such a "free descriptor",
>Â Â Âand
>Â Â Â> > does the use of the term "free descriptor" imply that the Driver MUST
>Â Â ÂNOT <
>Â Â Â> > https://docs.oasis-open.org/virtio/virtio/v1.2/csd01/
>Â Â Âvirtio-v1.2-csd01.html#x1-50003>
>Â Â Â> > use the same descriptor within multiple chains?
>Â Â Â> >
>Â Â Â> > I look forward to hearing your clarification.
>Â Â Â>
>Â Â Â> My guess is that this is mostly a case of a bit of sloppyness in a very
>Â Â Â> old part of the spec. A better term might be "free entries in the
>Â Â Â> descriptor table" (or even "unused entries..."), although that would be
>Â Â Â> a bit unwieldy. Maybe we should add some text like "free entries in the
>Â Â Â> descriptor table, henceforth referred to as 'free descriptors'".
>Â Â Â>
>Â Â Â> Michael, what do you think?
>
>Â Â ÂYes I think descriptors means free entries in the descriptor table.
>Â Â ÂI don't think the MUST there is right - in theory
>Â Â ÂI think the same descriptor chain can be used by multiple
>Â Â Âbuffers, though I am not aware of any drivers that do this.
>Â Â ÂSo I feel "free" here merely means "not used for some other
>Â Â Âpurpose". E.g. entries not referenced by any chains can be used
>Â Â Âby driver to keep some data for its internal purposes
>Â Â Â(and sometimes is) - if an entry is used like this and the driver
>Â Â Âneeds the data there then I guess it should not be used for
>Â Â Âdescriptors.
>
>Â Â ÂWe do say:
>Â Â ÂÂ Â Â Â A driver MUST NOT alter virtqueue entries for exposed buffers,
>Â Â ÂÂ Â Â Â i.e., buffers which have been
>Â Â ÂÂ Â Â Â made available to the device (and not been used by the device)
>Â Â ÂÂ Â Â Â of a live virtqueue.
>Â Â ÂSo such chains must not be modified while available to device.
>
>
>
>
>
>
>Â Â ÂI also think we still need a lot of cleanup in the buffer/descriptor/entry
>Â Â Âarea. And I feel we should just bite the bullet and talk about entries
>Â Â Âhere though - descriptors are widely used to mean valid/available
>Â Â Âentries.
>
>
>Â Â Â--
>Â Â Â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/
>
>


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/