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

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

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