4 ms·
What Stefan (the author) calls my vision, I call my arrogance. :) Some bits of my plan, especially with respect to how the async runtime in QEMU is designed, w
by bonzini 3y ago
What Stefan (the author) calls my vision, I call my arrogance. :)
Some bits of my plan, especially with respect to how the async runtime in QEMU is designed, were good. However I had vastly underestimated the complexity of one step. The various disk images form a graph that can change on the fly, for example if you make a live snapshot of a VM disk. The method I had thought of to handle changes to the graph would have added a lot of technical debt. Fortunately it was nacked by the maintainer Kevin Wolf and replaced with something better.
For more details on both my plan and what was actually done, see https://kvm-forum.qemu.org/2023/Multiqueue_in_the_block_layer_wLom4Bt.pdf https://kvm-forum.qemu.org/2023/Multiqueue_in_the_block_laye... (slides, also linked from the post) or https://youtu.be/Ubped0PgvZI?si=IsckfZ7uDNYJNp_y https://youtu.be/Ubped0PgvZI?si=IsckfZ7uDNYJNp_y (video).
The important thing, at every step, was being committed to getting it done. Some of the intermediate steps were better in terms of bugs fixed, but worse in terms of complexity because you had to juggle both the "good" locks and the legacy global locks.
- epilys 3y agoThanks for your work, Paolo! Question about TSA: did you consider combining it with a formal specification of the locking model e.g. with Alloy? Or other formal method.
- bonzini 3y agoThis is really everybody else's work. All I did was some mentoring of Emanuele, who is also the first presenter in the linked video. We didn't use formal methods, but some small parts of the async runtime were validated with spin. The Promela sources are in the QEMU source repository. In the end, the locking changes are relatively low tech. The verification part are where the magic happens, and TSA plus my call graph analysis tool vrc are enough for that.