[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). > | ..... > | > | 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?
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]