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

[Jasper Haag <jasper@bedrocksystems.com>]

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.

Regards,

Jasper Haag