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