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

["Michael S. Tsirkin" <mst@redhat.com>]

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/
> 
>