duplicate ids in used ring

duplicate ids in used ring

[Siddharth Priya]

TL;DR: The virtio spec does not consider duplicate entries (IDs) in the used
ring. Should this case be promoted to undefined behaviour [1] in the spec?

Background: I am developing proofs that the rust-vmm/virtio-queue [2]
implementation meets the virtio spec. I noticed that the spec does not state
anything about queue behaviour when a device adds a 
descriptor_table_index ID to
the used ring that is already present. As a result, implementations diverge:

* QEMU (with VIRTIO_F_IN_ORDER): The queue enforces a uniqueness invariant —
only one copy of an element may exist in the ring. If a duplicate is 
added, QEMU
overwrites the matching element with the new length [3].

* QEMU (with VIRTIO_F_RING_PACKED or split): The implementation assumes the
device will not add duplicates, and correctness relies on the device [4].

Problem: For packed and split queues, the implementation implicitly 
expects the
device to uphold the uniqueness invariant. For in-order queues, uniqueness
emerges implicitly from ordering. From a device developer’s perspective, 
it is
not clear that duplicates must never be inserted into the used ring. Since
implementations differ, the invariant is not consistently enforced, making
device conformance difficult to check.

Proposed solution: The spec could explicitly state that breaking the 
uniqueness
invariant is undefined behaviour. This mirrors the ISO C standard’s 
practice of
using "undefined behaviour" to signal obligations developers must 
uphold. The
term is widely understood by systems developers and would make expectations
clear.

```
Example change (to section 2.7.8 The Virtqueue Used Ring):
   ...
   Adding an index into the used ring when a virtq_used_elem entry with 
the same
   id already exists and has not yet been read by the driver results in 
undefined
   behaviour.
```

Looking forward to your thoughts.

Siddharth

[1] https://en.cppreference.com/w/c/language/behavior.html [2]
https://github.com/rust-vmm/vm-virtio [3]
https://github.com/qemu/qemu/blob/master/hw/virtio/virtio.c#L938 [4]
https://github.com/qemu/qemu/blob/5836af0783213b9355a6bbf85d9e6bc4c9c9363f/hw/net/virtio-net.c#L1977

Re: duplicate ids in used ring

[Stefan Hajnoczi]

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

On Tue, Aug 19, 2025 at 12:14:42PM -0400, Siddharth Priya wrote:
> TL;DR: The virtio spec does not consider duplicate entries (IDs) in the used
> ring. Should this case be promoted to undefined behaviour [1] in the spec?
> 
> Background: I am developing proofs that the rust-vmm/virtio-queue [2]
> implementation meets the virtio spec. I noticed that the spec does not state
> anything about queue behaviour when a device adds a descriptor_table_index
> ID to
> the used ring that is already present. As a result, implementations diverge:
> 
> * QEMU (with VIRTIO_F_IN_ORDER): The queue enforces a uniqueness invariant —
> only one copy of an element may exist in the ring. If a duplicate is added,
> QEMU
> overwrites the matching element with the new length [3].
> 
> * QEMU (with VIRTIO_F_RING_PACKED or split): The implementation assumes the
> device will not add duplicates, and correctness relies on the device [4].
> 
> Problem: For packed and split queues, the implementation implicitly expects
> the
> device to uphold the uniqueness invariant. For in-order queues, uniqueness
> emerges implicitly from ordering. From a device developer’s perspective, it
> is
> not clear that duplicates must never be inserted into the used ring. Since
> implementations differ, the invariant is not consistently enforced, making
> device conformance difficult to check.
> 
> Proposed solution: The spec could explicitly state that breaking the
> uniqueness
> invariant is undefined behaviour. This mirrors the ISO C standard’s practice
> of
> using "undefined behaviour" to signal obligations developers must uphold.
> The
> term is widely understood by systems developers and would make expectations
> clear.
> 
> ```
> Example change (to section 2.7.8 The Virtqueue Used Ring):
>   ...
>   Adding an index into the used ring when a virtq_used_elem entry with the
> same
>   id already exists and has not yet been read by the driver results in
> undefined
>   behaviour.
> ```
> 
> Looking forward to your thoughts.

The conformance clauses (\devicenormative) in the VIRTIO spec provide a
way to forbid things without specifying what has to happen in the
forbidden case. That can be used rather than introducing undefined
behavior into the spec.

How about adding a "The device MUST mark each buffer used at most once"?

Devices could behave in many different ways that make operation
impossible and the spec does not explicitly list each one. The scenario
you mentioned seems like one of these to me.

If it's helpful to add some of them to the spec, that should be fine. I
think the only drawback is that the spec may accumulate a large number
of clauses forbidding nonsensical behavior, making it harder to identify
the non-obvious clauses that implementors really need to watch out for.

Stefan

> 
> Siddharth
> 
> [1] https://en.cppreference.com/w/c/language/behavior.html [2]
> https://github.com/rust-vmm/vm-virtio [3]
> https://github.com/qemu/qemu/blob/master/hw/virtio/virtio.c#L938 [4]
> https://github.com/qemu/qemu/blob/5836af0783213b9355a6bbf85d9e6bc4c9c9363f/hw/net/virtio-net.c#L1977
> 
> 

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: duplicate ids in used ring

[Siddharth Priya]

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



On Wed, 20 Aug 2025, Stefan Hajnoczi wrote:

> On Tue, Aug 19, 2025 at 12:14:42PM -0400, Siddharth Priya wrote:
>> TL;DR: The virtio spec does not consider duplicate entries (IDs) in the used
>> ring. Should this case be promoted to undefined behaviour [1] in the spec?
>>
>> Background: I am developing proofs that the rust-vmm/virtio-queue [2]
>> implementation meets the virtio spec. I noticed that the spec does not state
>> anything about queue behaviour when a device adds a descriptor_table_index
>> ID to
>> the used ring that is already present. As a result, implementations diverge:
>>
>> * QEMU (with VIRTIO_F_IN_ORDER): The queue enforces a uniqueness invariant —
>> only one copy of an element may exist in the ring. If a duplicate is added,
>> QEMU
>> overwrites the matching element with the new length [3].
>>
>> * QEMU (with VIRTIO_F_RING_PACKED or split): The implementation assumes the
>> device will not add duplicates, and correctness relies on the device [4].
>>
>> Problem: For packed and split queues, the implementation implicitly expects
>> the
>> device to uphold the uniqueness invariant. For in-order queues, uniqueness
>> emerges implicitly from ordering. From a device developer’s perspective, it
>> is
>> not clear that duplicates must never be inserted into the used ring. Since
>> implementations differ, the invariant is not consistently enforced, making
>> device conformance difficult to check.
>>
>> Proposed solution: The spec could explicitly state that breaking the
>> uniqueness
>> invariant is undefined behaviour. This mirrors the ISO C standard’s practice
>> of
>> using "undefined behaviour" to signal obligations developers must uphold.
>> The
>> term is widely understood by systems developers and would make expectations
>> clear.
>>
>> ```
>> Example change (to section 2.7.8 The Virtqueue Used Ring):
>>   ...
>>   Adding an index into the used ring when a virtq_used_elem entry with the
>> same
>>   id already exists and has not yet been read by the driver results in
>> undefined
>>   behaviour.
>> ```
>>
>> Looking forward to your thoughts.
>
> The conformance clauses (\devicenormative) in the VIRTIO spec provide a
> way to forbid things without specifying what has to happen in the
> forbidden case. That can be used rather than introducing undefined
> behavior into the spec.
>
> How about adding a "The device MUST mark each buffer used at most once"?
Adding a normative clause sounds right to me.
>
> Devices could behave in many different ways that make operation
> impossible and the spec does not explicitly list each one. The scenario
> you mentioned seems like one of these to me.
>
> If it's helpful to add some of them to the spec, that should be fine. I
> think the only drawback is that the spec may accumulate a large number
> of clauses forbidding nonsensical behavior, making it harder to identify
> the non-obvious clauses that implementors really need to watch out for.
>
Agreed. One long term solution is to add pre-and-post conditions for 
functions in the reference implementation.
These could be in comments or runtime checks in debug builds.

I will send a conformance patch.

Siddharth
> Stefan
>
>>
>> Siddharth
>>
>> [1] https://en.cppreference.com/w/c/language/behavior.html [2]
>> https://github.com/rust-vmm/vm-virtio [3]
>> https://github.com/qemu/qemu/blob/master/hw/virtio/virtio.c#L938 [4]
>> https://github.com/qemu/qemu/blob/5836af0783213b9355a6bbf85d9e6bc4c9c9363f/hw/net/virtio-net.c#L1977
>>
>>
>