From: Jasper Haag <jasper@bedrocksystems.com>
To: "Michael S. Tsirkin" <mst@redhat.com>
Cc: Cornelia Huck <cohuck@redhat.com>,
virtio-comment@lists.oasis-open.org,
Awais Masood <awais@bedrocksystems.com>,
Gordon Stewart <gordon@bedrocksystems.com>
Subject: Re: [virtio-comment] [virtio-queue] CLARIFICATION: "free descriptors" External
Date: Mon, 23 Oct 2023 12:53:41 -0400 [thread overview]
Message-ID: <CA+c=0Wc9bx32ytDQSj5HTMWgP4z1S07qrKB-Zyx6XGw08e8JgA@mail.gmail.com> (raw)
In-Reply-To: <20231023071953-mutt-send-email-mst@kernel.org>
[-- 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 --]
prev parent reply other threads:[~2023-10-23 16:53 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2023-10-12 16:41 [virtio-comment] [virtio-queue] CLARIFICATION: "free descriptors" External Jasper Haag
2023-10-19 18:41 ` [virtio-comment] " Jasper Haag
2023-10-20 10:38 ` [virtio-comment] " Cornelia Huck
2023-10-20 11:11 ` Michael S. Tsirkin
2023-10-20 17:35 ` Jasper Haag
2023-10-23 11:21 ` Michael S. Tsirkin
2023-10-23 16:53 ` Jasper Haag [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='CA+c=0Wc9bx32ytDQSj5HTMWgP4z1S07qrKB-Zyx6XGw08e8JgA@mail.gmail.com' \
--to=jasper@bedrocksystems.com \
--cc=awais@bedrocksystems.com \
--cc=cohuck@redhat.com \
--cc=gordon@bedrocksystems.com \
--cc=mst@redhat.com \
--cc=virtio-comment@lists.oasis-open.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).