On Wed, Apr 05, 2017 at 01:37:10PM +0200, Paolo Bonzini wrote: > > > On 05/04/2017 09:09, Christoffer Dall wrote: > >>> - 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. > > ok, but the pattern above was not common to me (and I'm pretty sure I'm > > not the only fool in the bunch here), so if we can reference something > > that explains that this is a known pattern which has been tried and > > proven, that would be even better. > > I found https://lwn.net/Articles/573436/ which shows this example: > > CPU 0 CPU 1 > --------------------- ---------------------- > WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); > smp_mb(); smp_mb(); > r2 = READ_ONCE(y); r4 = READ_ONCE(x); > > And says that it is a bug if r2 == 0 && r4 == 0. This is exactly what > happens in KVM: > > CPU 0 CPU 1 > --------------------- ---------------------- > vcpu->mode = IN_GUEST_MODE; kvm_make_request(REQ, vcpu); > smp_mb(); smp_mb(); > r2 = kvm_request_pending(vcpu) r4 = (vcpu->mode == IN_GUEST_MODE) > if (r2) if (r4) > abort entry kick(); > > If r2 sees no request and r4 doesn't kick there would be a bug. > But why can't this happen? > > - if no request is pending at the time of the read to r2, CPU 1 must > not have executed kvm_make_request yet. In CPU 0, kvm_request_pending > must happen after vcpu->mode is set to IN_GUEST_MODE, therefore CPU 1 > will read IN_GUEST_MODE and kick. > > - if no kick happens in CPU 1, CPU 0 must not have set vcpu->mode yet. > In CPU 1, vcpu->mode is read after setting the request bit, therefore > CPU 0 will see the request bit and abort the guest entry. > > >>> - 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). > > > > That sounds reasonable, but I think part of the problem was that we > > simply didn't understand what the paradigms were (see the > > kvm_make_all_cpus_request above as an example), so Drew's action about > > documenting what this all is and the constraints of using it is really > > important for me to do that. > > Yes, totally agreed on that. > > >> 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. > >> > > I played with using blast on some of the KVM/ARM code a long time ago, > > and while I was able to find a bug with it, it was sort of an obvious > > bug, and the things I was able to do with it was pretty limited to the > > problems I could imagine myself anyhow. Perhaps this is what you mean > > with executable documentation. > > I prepared three examples of a spin model for KVM vCPU kicking, and > the outcome was actually pretty surprising: the mode check seems not > to be necessary. > > I haven't covered all x86 cases so I'm not going to remove it right > ahead, but for ARM it really seems like EXITING_GUEST_MODE is nothing > but an optimization of consecutive kvm_vcpu_kicks. > > All three models can use C preprocessor #defines to inject bugs: > > - kvm-arm-pause.promela: the "paused" mechanism; the model proves that > the "paused" test in the interrupt-disabled region is necessary > > - kvm-req.promela: the requests mechanism; the model proves that > the requests check in the interrupt-disabled region is necessary > > - kvm-x86-pi.promela: the x86 posted interrupt mechanism (simplified > a bit); the model proves that KVM must disable interrupts before > checking for interrupts injected while outside guest mode > (commit b95234c84004, "kvm: x86: do not use KVM_REQ_EVENT for APICv > interrupt injection", 2017-02-15) > > So it seems like there are no races after all in KVM/ARM code No races after Drew's fix has been applied to set vcpu->mode = IN_GUEST_MODE, before checking the pause flag, correct? (I think that's what the spin model below is modeling). (Currently, we have a window between checking the pause flag for the last time and etting mode = IN_GUEST_MODE, where we would loose IPIs and not check any variables.) > , though > the code can still be cleaned up. And I have been convinced of the wrong > thing all the time. :) > > But why is KVM/ARM using KVM_REQ_VCPU_EXIT > just fine without checking for requests (kvm-req.promela)? Because, > as mentioned earlier in the thread, KVM/ARM is using kvm_make_all_vcpus_request > simply to kick all VCPUs. The paused variable _is_ checked after disabling > interrupts, and that is fine. > > After this experiment, I think I like Drew's KVM_REQ_PAUSE more than I did > yesterday. However, yet another alternative is to leave pause/power_off as > they are, while taking some inspiration from his patch to do some cleanups: > > 1) change the "if" > > if (ret <= 0 || need_new_vmid_gen(vcpu->kvm) || > vcpu->arch.power_off || vcpu->arch.pause) { > > to test kvm_requests_pending instead of pause/power_off > > 2) clear KVM_REQ_VCPU_EXIT before the other "if": > > if (vcpu->arch.power_off || vcpu->arch.pause) > vcpu_sleep(vcpu); > I like using requests as only requests from one thread to the VCPU thread, and not to maintain specific state about a VCPU. The benefit of Drew's approach is that since these pieces of state are boolean, you can have just a single check in the critical path in the run loop instead of having to access multiple fields. I think I'll let Drew decide at this point what he prefers. > > In any case, the no-wakeup behavior of kvm_make_all_vcpus_request suits > either use of requests (KVM_REQ_PAUSE or "fixed" KVM_REQ_VCPU_EXIT). > Agreed. Thanks, -Christoffer > /* To run the model checker: > * > * spin -a kvm-arm-pause.promela > * gcc -O2 pan.c > * ./a.out -a -f > * > * Remove the tests using -DREMOVE_MODE_TEST, -DREMOVE_PAUSED_TEST > * right after -a. The mode test is not necessary, the paused test is. > */ > #define OUTSIDE_GUEST_MODE 0 > #define IN_GUEST_MODE 1 > #define EXITING_GUEST_MODE 2 > > bool kick; > bool paused; > int vcpu_mode = OUTSIDE_GUEST_MODE; > > active proctype vcpu_run() > { > do > :: true -> { > /* In paused state, sleep with interrupts on */ > if > :: !paused -> skip; > fi; > > /* IPIs are eaten until interrupts are turned off. */ > kick = 0; > > /* Interrupts are now off. */ > vcpu_mode = IN_GUEST_MODE; > > if > #ifndef REMOVE_MODE_TEST > :: vcpu_mode != IN_GUEST_MODE -> skip; > #endif > #ifndef REMOVE_PAUSED_TEST > :: paused -> skip; > #endif > :: else -> { > do > /* Stay in guest mode until an IPI comes */ > :: kick -> break; > od; > } > fi; > vcpu_mode = OUTSIDE_GUEST_MODE; > > /* Turn on interrupts */ > } > od > } > > active proctype vcpu_kick() > { > int old; > > do > :: true -> { > paused = 1; > /* cmpxchg */ > atomic { > old = vcpu_mode; > if > :: vcpu_mode == IN_GUEST_MODE -> > vcpu_mode = EXITING_GUEST_MODE; > :: else -> skip; > fi; > } > > if > :: old == IN_GUEST_MODE -> kick = 1; > :: else -> skip; > fi; > > if > :: vcpu_mode == OUTSIDE_GUEST_MODE -> paused = 0; > fi; > } > od; > } > > never { > do > /* After an arbitrarily long prefix */ > :: 1 -> skip; > > /* if we get a pause request */ > :: paused -> break; > od; > > accept: > /* we must eventually leave guest mode (this condition is reversed!) */ > do > :: vcpu_mode != OUTSIDE_GUEST_MODE > od; > } > /* To run the model checker: > * > * spin -a kvm-req.promela > * gcc -O2 pan.c > * ./a.out -a -f > * > * Remove the tests using -DREMOVE_MODE_TEST, -DREMOVE_REQ_TEST > * right after -a. The mode test is not necessary, the vcpu_req test is. > */ > #define OUTSIDE_GUEST_MODE 0 > #define IN_GUEST_MODE 1 > #define EXITING_GUEST_MODE 2 > > bool kick; > int vcpu_req; > int vcpu_mode = OUTSIDE_GUEST_MODE; > > active proctype vcpu_run() > { > do > :: true -> { > /* Requests are processed with interrupts on */ > vcpu_req = 0; > > /* IPIs are eaten until interrupts are turned off. */ > kick = 0; > > /* Interrupts are now off. */ > vcpu_mode = IN_GUEST_MODE; > > if > #ifndef REMOVE_MODE_TEST > :: vcpu_mode != IN_GUEST_MODE -> skip; > #endif > #ifndef REMOVE_REQ_TEST > :: vcpu_req -> skip; > #endif > :: else -> { > do > /* Stay in guest mode until an IPI comes */ > :: kick -> break; > od; > } > fi; > vcpu_mode = OUTSIDE_GUEST_MODE; > > /* Turn on interrupts */ > } > od > } > > active proctype vcpu_kick() > { > int old; > > do > :: true -> { > vcpu_req = 1; > if > :: old == 0 -> { > /* cmpxchg */ > atomic { > old = vcpu_mode; > if > :: vcpu_mode == IN_GUEST_MODE -> > vcpu_mode = EXITING_GUEST_MODE; > :: else -> skip; > fi; > } > > if > :: old == IN_GUEST_MODE -> kick = 1; > :: else -> skip; > fi; > } > :: else -> skip; > fi; > } > od; > } > > never { > do > /* After an arbitrarily long prefix */ > :: 1 -> skip; > > /* we get in guest mode */ > :: vcpu_mode == IN_GUEST_MODE -> break; > od; > > accept: > /* and never leave it (this condition is reversed!) */ > do > :: vcpu_mode != OUTSIDE_GUEST_MODE > od; > } > /* To run the model checker: > * > * spin -a kvm-x86-pi.promela > * gcc -O2 pan.c > * ./a.out -a -f > * > * Remove the test using -DREMOVE_MODE_TEST, move the PIR->IRR sync > * before local_irq_disable() with SYNC_WITH_INTERRUPTS_ENABLED. The > * mode test is not necessary, while sync_pir_to_irr must be placed > * after interrupts are disabled. > */ > #define OUTSIDE_GUEST_MODE 0 > #define IN_GUEST_MODE 1 > #define EXITING_GUEST_MODE 2 > > bool kick; > bool posted_interrupt; > int vcpu_pir; > int vcpu_mode = OUTSIDE_GUEST_MODE; > > active proctype vcpu_run() > { > do > :: true -> { > #ifdef SYNC_WITH_INTERRUPTS_ENABLED > /* Guest interrupts are injected with interrupts off */ > vcpu_pir = 0; > #endif > > /* Both kinds of IPI are eaten until interrupts are turned off. */ > atomic { > kick = 0; > posted_interrupt = 0; > } > > /* Interrupts are now off. */ > vcpu_mode = IN_GUEST_MODE; > > #ifndef SYNC_WITH_INTERRUPTS_ENABLED > /* Guest interrupts are injected with interrupts off */ > vcpu_pir = 0; > #endif > > if > #ifndef REMOVE_MODE_TEST > :: vcpu_mode != IN_GUEST_MODE -> skip; > #endif > > :: else -> { > do > /* Stay in guest mode until an IPI comes */ > :: kick -> break; > > /* The processor handles the posted interrupt IPI */ > :: posted_interrupt -> vcpu_pir = 0; > od; > } > fi; > vcpu_mode = OUTSIDE_GUEST_MODE; > > /* Turn on interrupts */ > } > od > } > > active proctype vcpu_posted_interrupt() > { > int old; > > do > :: vcpu_pir == 0 -> { > vcpu_pir = 1; > if > :: vcpu_mode == IN_GUEST_MODE -> > /* If in guest mode, we can send a posted interrupt IPI */ > posted_interrupt = 1; > > :: else -> { > /* Else, do a kvm_vcpu_kick. */ > atomic { > old = vcpu_mode; > if > :: vcpu_mode == IN_GUEST_MODE -> > vcpu_mode = EXITING_GUEST_MODE; > :: else -> skip; > fi; > } > > if > :: old == IN_GUEST_MODE -> kick = 1; > :: else -> skip; > fi; > } > fi; > } > od; > } > > never { > do > /* After an arbitrarily long prefix */ > :: 1 -> skip; > > /* if we get an interrupt */ > :: vcpu_pir -> break; > od; > > accept: > /* we must eventually inject it (this condition is reversed!) */ > do > :: vcpu_pir > od; > }
