Re: [PATCH v2 4/9] KVM: arm/arm64: replace vcpu->arch.pause with a vcpu request

[Paolo Bonzini <pbonzini@redhat.com>]

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



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, 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);


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).

Paolo

[-- Attachment #2: kvm-arm-pause.promela --]
[-- Type: text/plain, Size: 2286 bytes --]

/* 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; 
}

[-- Attachment #3: kvm-req.promela --]
[-- Type: text/plain, Size: 2358 bytes --]

/* 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; 
}

[-- Attachment #4: kvm-x86-pi.promela --]
[-- Type: text/plain, Size: 3000 bytes --]

/* 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; 
}

[-- Attachment #5: Type: text/plain, Size: 151 bytes --]

_______________________________________________
kvmarm mailing list
kvmarm@lists.cs.columbia.edu
https://lists.cs.columbia.edu/mailman/listinfo/kvmarm