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