On 04/04/2017 21:04, Christoffer Dall wrote: > - (On a related work, I suddenly felt it weird that > kvm_make_all_cpus_request() doesn't wake up sleeping VCPUs, but only > sends an IPI; does this mean that calling this function should be > followed by a kick() for each VCPU? Maybe Radim was looking at this > in his series already.) Yes, kvm_make_all_cpus_request in x86 is only used for "non urgent" requests, i.e. things to do before the next guest entry. > - In the explanation you wrote, you use the term 'we' a lot, but when > talking about SMP barriers, I think it only makes sense to talk about > actions and observations between multiple CPUs and we have to be > specific about which CPU observes or does what with respect to the > other. Maybe I'm being a stickler here, but there something here > which is making me uneasy. The write1-mb-if(read2) / write2-mb-if(read1) pattern is pretty common, so I think it is justified to cut the ordering on the reasoning and just focus on what the two memory locations and conditions mean. But I'd wait for v3, since I'm sure that Drew also understands the synchronization better. > - Finally, it feels very hard to prove the correctness of this, and > equally hard to test it (given how long we've been running with > apparently racy code). I would hope that we could abstract some of > this into architecture generic things, that someone who eat memory > barriers for breakfast could help us verify, but again, maybe this is > Radim's series I'm asking for here. What I can do here is to suggest copying the paradigms from x86, which is quite battle tested (Windows hammers it really hard). For QEMU I did use model checking in the past for some similarly hairy synchronization code, but that is really just "executable documentation" because the model is not written in C. Paolo
