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

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

[Jasper Haag]

[-- Attachment #1: Type: text/plain, Size: 2206 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 3120 bytes --]

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

[Jasper Haag]

[-- Attachment #1: Type: text/plain, Size: 2974 bytes --]

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.

Regards,
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).
> |      .....
> |
> | 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
>

[-- Attachment #2: Type: text/html, Size: 4434 bytes --]

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

[Cornelia Huck]

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?


This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

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

[Michael S. Tsirkin]

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


This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

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

[Jasper Haag]

[-- Attachment #1: Type: text/plain, Size: 7452 bytes --]

Folks,

Thank you kindly for the thoughtful responses! From the point of view
of formal modelling/verification I think there is a lot of benefit to be had
from tightening the language in the VIRTIO specification. I also think
that the formal methods work we do at BedRock Systems puts us in a
position to contribute on this front - although I need to coordinate with
my managers regarding the logistics of such contributions, including
sponsoring
membership(s) to the "OASIS Virtual I/O Device (VIRTIO) Technical Committee"
<https://www.oasis-open.org/committees/membership.php?wg_abbrev=virtio>.

> Maybe we should add some text like "free entries in the
> descriptor table, henceforth referred to as 'free descriptors'".
This clarified text seems like an improvement, but it still leaves some
open questions in my mind - which Michael's response helps to tease
out.

> 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.
Overall, we're interested in understanding the ownership discipline
involved with the descriptor-entry/payload "resources" (in the sense of
linear logic). Our operational model will need to codify this discipline in
order to track/cede ownership of these "resources" at the appropriate
times, and aliasing will complicate the story here. To wit:
1) If a Device owns two buffers which alias each other's descriptors, and
   sends one of the buffers back to the Driver, does the Device still own
   the other buffer it hasn't yet returned, including the buffer's
descriptors?
2) If a Device owns two buffers which alias payload memory, and sends one
   of the buffers back to the Driver, does the Device still own the payload
   memory referred to by the buffer it hasn't yet returned?

Along these lines, a few clarifications:
i)   Are Drivers allowed to alias descriptor chain suffixes, or only
complete
     descriptor chains?
ii)  May a Driver /simultaneously expose/ multiple buffers which share
descriptor
     chain (suffixes)?
iii) May a Driver /simultaneously expose/ multiple buffers which
(partially) alias
     the same payload memory?

I look forward to continuing this discussion.

~Jasper

On Fri, Oct 20, 2023 at 7:12 AM Michael S. Tsirkin <mst@redhat.com> wrote:

> 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
>
>
> This publicly archived list offers a means to provide input to the
> OASIS Virtual I/O Device (VIRTIO) TC.
>
> In order to verify user consent to the Feedback License terms and
> to minimize spam in the list archive, subscription is required
> before posting.
>
> Subscribe: virtio-comment-subscribe@lists.oasis-open.org
> Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
> List help: virtio-comment-help@lists.oasis-open.org
> List archive: https://lists.oasis-open.org/archives/virtio-comment/
> Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
> List Guidelines:
> https://www.oasis-open.org/policies-guidelines/mailing-lists
> Committee: https://www.oasis-open.org/committees/virtio/
> Join OASIS: https://www.oasis-open.org/join/
>
>

[-- Attachment #2: Type: text/html, Size: 9845 bytes --]

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

[Michael S. Tsirkin]

On Fri, Oct 20, 2023 at 01:35:00PM -0400, Jasper Haag wrote:
> Folks,
> 
> Thank you kindly for the thoughtful responses! From the point of view
> of formal modelling/verification I think there is a lot of benefit to be had
> from tightening the language in the VIRTIO specification. I also think
> that the formal methods work we do at BedRock Systems puts us in a
> position to contribute on this front - although I need to coordinate with
> my managers regarding the logistics of such contributions, including sponsoring
> membership(s) to the "OASIS Virtual I/O Device (VIRTIO) Technical Committee"
> <https://www.oasis-open.org/committees/membership.php?wg_abbrev=virtio>.
> 
> > Maybe we should add some text like "free entries in the
> > descriptor table, henceforth referred to as 'free descriptors'".
> This clarified text seems like an improvement, but it still leaves some
> open questions in my mind - which Michael's response helps to tease
> out.
> 
> > 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.
> Overall, we're interested in understanding the ownership discipline
> involved with the descriptor-entry/payload "resources" (in the sense of
> linear logic). Our operational model will need to codify this discipline in
> order to track/cede ownership of these "resources" at the appropriate
> times, and aliasing will complicate the story here. To wit:
> 1) If a Device owns two buffers which alias each other's descriptors, and
>    sends one of the buffers back to the Driver, does the Device still own
>    the other buffer it hasn't yet returned, including the buffer's descriptors?
> 2) If a Device owns two buffers which alias payload memory, and sends one
>    of the buffers back to the Driver, does the Device still own the payload
>    memory referred to by the buffer it hasn't yet returned?

I would say yes.

> Along these lines, a few clarifications:
> i)   Are Drivers allowed to alias descriptor chain suffixes, or only complete
>      descriptor chains?
> ii)  May a Driver /simultaneously expose/ multiple buffers which share
> descriptor
>      chain (suffixes)?
> iii) May a Driver /simultaneously expose/ multiple buffers which (partially)
> alias
>      the same payload memory?

Nothing seems to disallow this. iii actually happens sometimes.

> 
> I look forward to continuing this discussion.
> 
> ~Jasper
> 
> On Fri, Oct 20, 2023 at 7:12 AM Michael S. Tsirkin <mst@redhat.com> wrote:
> 
>     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
> 
> 
>     This publicly archived list offers a means to provide input to the
>     OASIS Virtual I/O Device (VIRTIO) TC.
> 
>     In order to verify user consent to the Feedback License terms and
>     to minimize spam in the list archive, subscription is required
>     before posting.
> 
>     Subscribe: virtio-comment-subscribe@lists.oasis-open.org
>     Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
>     List help: virtio-comment-help@lists.oasis-open.org
>     List archive: https://lists.oasis-open.org/archives/virtio-comment/
>     Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
>     List Guidelines: https://www.oasis-open.org/policies-guidelines/
>     mailing-lists
>     Committee: https://www.oasis-open.org/committees/virtio/
>     Join OASIS: https://www.oasis-open.org/join/
> 
> 


This publicly archived list offers a means to provide input to the
OASIS Virtual I/O Device (VIRTIO) TC.

In order to verify user consent to the Feedback License terms and
to minimize spam in the list archive, subscription is required
before posting.

Subscribe: virtio-comment-subscribe@lists.oasis-open.org
Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
List help: virtio-comment-help@lists.oasis-open.org
List archive: https://lists.oasis-open.org/archives/virtio-comment/
Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
List Guidelines: https://www.oasis-open.org/policies-guidelines/mailing-lists
Committee: https://www.oasis-open.org/committees/virtio/
Join OASIS: https://www.oasis-open.org/join/

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

[Jasper Haag]

[-- Attachment #1: Type: text/plain, Size: 9816 bytes --]

Thanks for the concise response. It seems clear to us at BedRock Systems
that our VIRTIO Queue operational model will need to support aliasing of
both descriptor entries and payload memory.

For now we are focusing on making such updates to our operational model.
We will follow up with any other clarification questions which arise.

Your responsiveness has been much appreciated.

~Jasper



On Mon, Oct 23, 2023 at 7:21 AM Michael S. Tsirkin <mst@redhat.com> wrote:

> On Fri, Oct 20, 2023 at 01:35:00PM -0400, Jasper Haag wrote:
> > Folks,
> >
> > Thank you kindly for the thoughtful responses! From the point of view
> > of formal modelling/verification I think there is a lot of benefit to be
> had
> > from tightening the language in the VIRTIO specification. I also think
> > that the formal methods work we do at BedRock Systems puts us in a
> > position to contribute on this front - although I need to coordinate with
> > my managers regarding the logistics of such contributions, including
> sponsoring
> > membership(s) to the "OASIS Virtual I/O Device (VIRTIO) Technical
> Committee"
> > <https://www.oasis-open.org/committees/membership.php?wg_abbrev=virtio>.
> >
> > > Maybe we should add some text like "free entries in the
> > > descriptor table, henceforth referred to as 'free descriptors'".
> > This clarified text seems like an improvement, but it still leaves some
> > open questions in my mind - which Michael's response helps to tease
> > out.
> >
> > > 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.
> > Overall, we're interested in understanding the ownership discipline
> > involved with the descriptor-entry/payload "resources" (in the sense of
> > linear logic). Our operational model will need to codify this discipline
> in
> > order to track/cede ownership of these "resources" at the appropriate
> > times, and aliasing will complicate the story here. To wit:
> > 1) If a Device owns two buffers which alias each other's descriptors, and
> >    sends one of the buffers back to the Driver, does the Device still own
> >    the other buffer it hasn't yet returned, including the buffer's
> descriptors?
> > 2) If a Device owns two buffers which alias payload memory, and sends one
> >    of the buffers back to the Driver, does the Device still own the
> payload
> >    memory referred to by the buffer it hasn't yet returned?
>
> I would say yes.
>
> > Along these lines, a few clarifications:
> > i)   Are Drivers allowed to alias descriptor chain suffixes, or only
> complete
> >      descriptor chains?
> > ii)  May a Driver /simultaneously expose/ multiple buffers which share
> > descriptor
> >      chain (suffixes)?
> > iii) May a Driver /simultaneously expose/ multiple buffers which
> (partially)
> > alias
> >      the same payload memory?
>
> Nothing seems to disallow this. iii actually happens sometimes.
>
> >
> > I look forward to continuing this discussion.
> >
> > ~Jasper
> >
> > On Fri, Oct 20, 2023 at 7:12 AM Michael S. Tsirkin <mst@redhat.com>
> wrote:
> >
> >     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
> >
> >
> >     This publicly archived list offers a means to provide input to the
> >     OASIS Virtual I/O Device (VIRTIO) TC.
> >
> >     In order to verify user consent to the Feedback License terms and
> >     to minimize spam in the list archive, subscription is required
> >     before posting.
> >
> >     Subscribe: virtio-comment-subscribe@lists.oasis-open.org
> >     Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
> >     List help: virtio-comment-help@lists.oasis-open.org
> >     List archive: https://lists.oasis-open.org/archives/virtio-comment/
> >     Feedback License:
> https://www.oasis-open.org/who/ipr/feedback_license.pdf
> >     List Guidelines: https://www.oasis-open.org/policies-guidelines/
> >     mailing-lists
> >     Committee: https://www.oasis-open.org/committees/virtio/
> >     Join OASIS: https://www.oasis-open.org/join/
> >
> >
>
>
> This publicly archived list offers a means to provide input to the
> OASIS Virtual I/O Device (VIRTIO) TC.
>
> In order to verify user consent to the Feedback License terms and
> to minimize spam in the list archive, subscription is required
> before posting.
>
> Subscribe: virtio-comment-subscribe@lists.oasis-open.org
> Unsubscribe: virtio-comment-unsubscribe@lists.oasis-open.org
> List help: virtio-comment-help@lists.oasis-open.org
> List archive: https://lists.oasis-open.org/archives/virtio-comment/
> Feedback License: https://www.oasis-open.org/who/ipr/feedback_license.pdf
> List Guidelines:
> https://www.oasis-open.org/policies-guidelines/mailing-lists
> Committee: https://www.oasis-open.org/committees/virtio/
> Join OASIS: https://www.oasis-open.org/join/
>
>

[-- Attachment #2: Type: text/html, Size: 13955 bytes --]