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-queue] CLARIFICATION: "free descriptors" External

Hello again,

I hope you've been well since my last message. I'm still interested in getting clarification regarding whether the use of the term "free descriptor" in "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> implies that compliant VIRTIO Drivers 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.

Please let me know whether I can clarify any aspects of my question.

Jasper Haag

On Thu, Oct 12, 2023 at 12:41âPM 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.

Jasper Haag

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