Hey all,
I hope everyone had a nice weekend (and those of you attending LPC and
KVM Forum I hope had nice conferences! I definitely enjoyed meeting some
rust-vmm community members at LPC :)
This e-mail is born from some discussions about formal verification
Matias, Stefano and me had at LPC last week. Matias held a session
titled "Verifying the Conformance of a VirtIO Driver to the VirtIO
Specification" [1], which touched on rust-vmm's virtio stack, and I have
done similar work for Firecracker's virtio stack [3] using the Kani Rust
verifier [2]. We also had an intern at AWS in the Kani team work on some
formal verification in vmm-sys-util recently [4].
Since there seems to be quite some interest in introducing formal
methods to rust-vmm, I thought we could talk about it at the next
community sync meeting next Monday (4pm BST, as always)? :D
Best,
Patrick
[1]: https://lpc.events/event/18/contributions/1897/
[2]: https://github.com/model-checking/kani/
[3]: https://github.com/firecracker-microvm/firecracker/blob/4bbbec06ee0d529add0…
[4]: https://github.com/rust-vmm/vmm-sys-util/pull/227
Hi,
so, I was a bit curious about trying out to use virtio devices with
UML. virtiofsd is obviously interesting, but I also tried vhost-device-
sound (not that I expect anyone actually wants sound).
Anyway, I needed some fixes to make it work, see
https://lore.kernel.org/linux-um/20241103212854.1436046-1-benjamin@sipsolut…
Two of these related to the Rust implementation:
1. The code for VHOST_USER_SET_MEM_TABLE does not accept the message
if it is larger than expected.
2. The VHOST_USER_SET_VRING_NUM call for vhost-device-sound seems to
have an artificial limit for the queue length of 64.
For 1. the fix is easy, we can just send the correct message.
However, 2. is more problematic. It does not look like there is a way
to discover the limit that vhost-device-sound is enforcing. That means
we would be stuck with a hard-coding a limit based on the device type
ID, which does not seem like a good idea.
Could the limit be lifted in the implementation? Am I maybe missing
something and it is possible to discover the limit somehow?
Benjamin