OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.


Help: OASIS Mailing Lists Help | MarkMail Help

virtio-comment message

[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]

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

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).
> |      .....
> |
> | - 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?

[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]