path: root/docs/tcg-exclusive.promela

/*
 * This model describes the implementation of exclusive sections in
 * cpus-common.c (start_exclusive, end_exclusive, cpu_exec_start,
 * cpu_exec_end).
 *
 * Author: Paolo Bonzini <pbonzini@redhat.com>
 *
 * This file is in the public domain.  If you really want a license,
 * the WTFPL will do.
 *
 * To verify it:
 *     spin -a docs/tcg-exclusive.promela
 *     gcc pan.c -O2
 *     ./a.out -a
 *
 * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, TEST_EXPENSIVE.
 */

// Define the missing parameters for the model
#ifndef N_CPUS
#define N_CPUS 2
#warning defaulting to 2 CPU processes
#endif

// the expensive test is not so expensive for <= 3 CPUs
#if N_CPUS <= 3
#define TEST_EXPENSIVE
#endif

#ifndef N_EXCLUSIVE
# if !defined N_CYCLES || N_CYCLES <= 1 || defined TEST_EXPENSIVE
#  define N_EXCLUSIVE     2
#  warning defaulting to 2 concurrent exclusive sections
# else
#  define N_EXCLUSIVE     1
#  warning defaulting to 1 concurrent exclusive sections
# endif
#endif
#ifndef N_CYCLES
# if N_EXCLUSIVE <= 1 || defined TEST_EXPENSIVE
#  define N_CYCLES        2
#  warning defaulting to 2 CPU cycles
# else
#  define N_CYCLES        1
#  warning defaulting to 1 CPU cycles
# endif
#endif


// synchronization primitives.  condition variables require a
// process-local "cond_t saved;" variable.

#define mutex_t              byte
#define MUTEX_LOCK(m)        atomic { m == 0 -> m = 1 }
#define MUTEX_UNLOCK(m)      m = 0

#define cond_t               int
#define COND_WAIT(c, m)      {                                  \
                               saved = c;                       \
                               MUTEX_UNLOCK(m);                 \
                               c != saved -> MUTEX_LOCK(m);     \
                             }
#define COND_BROADCAST(c)    c++

// this is the logic from cpus-common.c

mutex_t mutex;
cond_t exclusive_cond;
cond_t exclusive_resume;
byte pending_cpus;

byte running[N_CPUS];
byte has_waiter[N_CPUS];

#define exclusive_idle()                                          \
  do                                                              \
      :: pending_cpus -> COND_WAIT(exclusive_resume, mutex);      \
      :: else         -> break;                                   \
  od

#define start_exclusive()                                         \
    MUTEX_LOCK(mutex);                                            \
    exclusive_idle();                                             \
    pending_cpus = 1;                                             \
                                                                  \
    i = 0;                                                        \
    do                                                            \
       :: i < N_CPUS -> {                                         \
           if                                                     \
              :: running[i] -> has_waiter[i] = 1; pending_cpus++; \
              :: else       -> skip;                              \
           fi;                                                    \
           i++;                                                   \
       }                                                          \
       :: else -> break;                                          \
    od;                                                           \
                                                                  \
    do                                                            \
      :: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex);    \
      :: else             -> break;                               \
    od;                                                           \
    MUTEX_UNLOCK(mutex);

#define end_exclusive()                                           \
    MUTEX_LOCK(mutex);                                            \
    pending_cpus = 0;                                             \
    COND_BROADCAST(exclusive_resume);                             \
    MUTEX_UNLOCK(mutex);

#define cpu_exec_start(id)                                                   \
    MUTEX_LOCK(mutex);                                                       \
    exclusive_idle();                                                        \
    running[id] = 1;                                                         \
    MUTEX_UNLOCK(mutex);

#define cpu_exec_end(id)                                                     \
    MUTEX_LOCK(mutex);                                                       \
    running[id] = 0;                                                         \
    if                                                                       \
        :: pending_cpus -> {                                                 \
            pending_cpus--;                                                  \
            if                                                               \
                :: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond);      \
                :: else -> skip;                                             \
            fi;                                                              \
        }                                                                    \
        :: else -> skip;                                                     \
    fi;                                                                      \
    MUTEX_UNLOCK(mutex);

// Promela processes

byte done_cpu;
byte in_cpu;
active[N_CPUS] proctype cpu()
{
    byte id = _pid % N_CPUS;
    byte cycles = 0;
    cond_t saved;

    do
       :: cycles == N_CYCLES -> break;
       :: else -> {
           cycles++;
           cpu_exec_start(id)
           in_cpu++;
           done_cpu++;
           in_cpu--;
           cpu_exec_end(id)
       }
    od;
}

byte done_exclusive;
byte in_exclusive;
active[N_EXCLUSIVE] proctype exclusive()
{
    cond_t saved;
    byte i;

    start_exclusive();
    in_exclusive = 1;
    done_exclusive++;
    in_exclusive = 0;
    end_exclusive();
}

#define LIVENESS   (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
#define SAFETY     !(in_exclusive && in_cpu)

never {    /* ! ([] SAFETY && <> [] LIVENESS) */
    do
    // once the liveness property is satisfied, this is not executable
    // and the never clause is not accepted
    :: ! LIVENESS -> accept_liveness: skip
    :: 1          -> assert(SAFETY)
    od;
}