[mirror_qemu.git] / 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, USE_MUTEX,
 *                           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 <= 2 CPUs
// If the mutex is used, it's also cheap (300 MB / 4 seconds) for 3 CPUs
// For 3 CPUs and the lock-free option it needs 1.5 GB of RAM
#if N_CPUS <= 2 || (N_CPUS <= 3 && defined USE_MUTEX)
#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);

#ifdef USE_MUTEX
// Simple version using mutexes
#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);
#else
// Wait-free fast path, only needs mutex when concurrent with
// an exclusive section
#define cpu_exec_start(id)                                                   \
    running[id] = 1;                                                         \
    if                                                                       \
        :: pending_cpus -> {                                                 \
            MUTEX_LOCK(mutex);                                               \
            if                                                               \
                :: !has_waiter[id] -> {                                      \
                    running[id] = 0;                                         \
                    exclusive_idle();                                        \
                    running[id] = 1;                                         \
                }                                                            \
                :: else -> skip;                                             \
            fi;                                                              \
            MUTEX_UNLOCK(mutex);                                             \
        }                                                                    \
        :: else -> skip;                                                     \
    fi;

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

// 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;
}
Commit	Line	Data
a200f2fb PB	1	/*
	2	* This model describes the implementation of exclusive sections in
	3	* cpus-common.c (start_exclusive, end_exclusive, cpu_exec_start,
	4	* cpu_exec_end).
	5	*
	6	* Author: Paolo Bonzini <pbonzini@redhat.com>
	7	*
	8	* This file is in the public domain. If you really want a license,
	9	* the WTFPL will do.
	10	*
	11	* To verify it:
	12	* spin -a docs/tcg-exclusive.promela
	13	* gcc pan.c -O2
	14	* ./a.out -a
	15	*
c265e976 PB	16	* Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX,
c265e976 PB	17	* TEST_EXPENSIVE.
a200f2fb PB	18	*/
	19
	20	// Define the missing parameters for the model
	21	#ifndef N_CPUS
	22	#define N_CPUS 2
	23	#warning defaulting to 2 CPU processes
	24	#endif
	25
c265e976 PB	26	// the expensive test is not so expensive for <= 2 CPUs
	27	// If the mutex is used, it's also cheap (300 MB / 4 seconds) for 3 CPUs
	28	// For 3 CPUs and the lock-free option it needs 1.5 GB of RAM
	29	#if N_CPUS <= 2 \|\| (N_CPUS <= 3 && defined USE_MUTEX)
a200f2fb PB	30	#define TEST_EXPENSIVE
	31	#endif
	32
	33	#ifndef N_EXCLUSIVE
	34	# if !defined N_CYCLES \|\| N_CYCLES <= 1 \|\| defined TEST_EXPENSIVE
	35	# define N_EXCLUSIVE 2
	36	# warning defaulting to 2 concurrent exclusive sections
	37	# else
	38	# define N_EXCLUSIVE 1
	39	# warning defaulting to 1 concurrent exclusive sections
	40	# endif
	41	#endif
	42	#ifndef N_CYCLES
	43	# if N_EXCLUSIVE <= 1 \|\| defined TEST_EXPENSIVE
	44	# define N_CYCLES 2
	45	# warning defaulting to 2 CPU cycles
	46	# else
	47	# define N_CYCLES 1
	48	# warning defaulting to 1 CPU cycles
	49	# endif
	50	#endif
	51
	52
	53	// synchronization primitives. condition variables require a
	54	// process-local "cond_t saved;" variable.
	55
	56	#define mutex_t byte
	57	#define MUTEX_LOCK(m) atomic { m == 0 -> m = 1 }
	58	#define MUTEX_UNLOCK(m) m = 0
	59
	60	#define cond_t int
	61	#define COND_WAIT(c, m) { \
	62	saved = c; \
	63	MUTEX_UNLOCK(m); \
	64	c != saved -> MUTEX_LOCK(m); \
	65	}
	66	#define COND_BROADCAST(c) c++
	67
	68	// this is the logic from cpus-common.c
	69
	70	mutex_t mutex;
	71	cond_t exclusive_cond;
	72	cond_t exclusive_resume;
	73	byte pending_cpus;
	74
	75	byte running[N_CPUS];
	76	byte has_waiter[N_CPUS];
	77
	78	#define exclusive_idle() \
	79	do \
	80	:: pending_cpus -> COND_WAIT(exclusive_resume, mutex); \
	81	:: else -> break; \
	82	od
	83
	84	#define start_exclusive() \
	85	MUTEX_LOCK(mutex); \
	86	exclusive_idle(); \
	87	pending_cpus = 1; \
	88	\
	89	i = 0; \
	90	do \
	91	:: i < N_CPUS -> { \
	92	if \
	93	:: running[i] -> has_waiter[i] = 1; pending_cpus++; \
94	:: else -> skip; \
95	fi; \
96	i++; \
97	} \
98	:: else -> break; \
99	od; \
100	\
101	do \
102	:: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex); \
103	:: else -> break; \
758e1b2b PB	104	od; \
758e1b2b PB	105	MUTEX_UNLOCK(mutex);
a200f2fb PB	106
a200f2fb PB	107	#define end_exclusive() \
758e1b2b	108	MUTEX_LOCK(mutex); \
a200f2fb PB	109	pending_cpus = 0; \
	110	COND_BROADCAST(exclusive_resume); \
	111	MUTEX_UNLOCK(mutex);
	112
c265e976 PB	113	#ifdef USE_MUTEX
c265e976 PB	114	// Simple version using mutexes
a200f2fb PB	115	#define cpu_exec_start(id) \
	116	MUTEX_LOCK(mutex); \
	117	exclusive_idle(); \
	118	running[id] = 1; \
	119	MUTEX_UNLOCK(mutex);
	120
	121	#define cpu_exec_end(id) \
	122	MUTEX_LOCK(mutex); \
	123	running[id] = 0; \
	124	if \
	125	:: pending_cpus -> { \
	126	pending_cpus--; \
	127	if \
	128	:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
	129	:: else -> skip; \
	130	fi; \
	131	} \
	132	:: else -> skip; \
	133	fi; \
a200f2fb	134	MUTEX_UNLOCK(mutex);
c265e976 PB	135	#else
	136	// Wait-free fast path, only needs mutex when concurrent with
	137	// an exclusive section
	138	#define cpu_exec_start(id) \
	139	running[id] = 1; \
	140	if \
	141	:: pending_cpus -> { \
	142	MUTEX_LOCK(mutex); \
	143	if \
	144	:: !has_waiter[id] -> { \
	145	running[id] = 0; \
	146	exclusive_idle(); \
	147	running[id] = 1; \
	148	} \
	149	:: else -> skip; \
	150	fi; \
	151	MUTEX_UNLOCK(mutex); \
	152	} \
	153	:: else -> skip; \
	154	fi;
	155
	156	#define cpu_exec_end(id) \
	157	running[id] = 0; \
	158	if \
	159	:: pending_cpus -> { \
	160	MUTEX_LOCK(mutex); \
	161	if \
	162	:: has_waiter[id] -> { \
	163	has_waiter[id] = 0; \
	164	pending_cpus--; \
	165	if \
	166	:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
	167	:: else -> skip; \
	168	fi; \
	169	} \
	170	:: else -> skip; \
	171	fi; \
	172	MUTEX_UNLOCK(mutex); \
	173	} \
	174	:: else -> skip; \
	175	fi
	176	#endif
a200f2fb PB	177
	178	// Promela processes
	179
	180	byte done_cpu;
	181	byte in_cpu;
	182	active[N_CPUS] proctype cpu()
	183	{
	184	byte id = _pid % N_CPUS;
	185	byte cycles = 0;
	186	cond_t saved;
	187
	188	do
	189	:: cycles == N_CYCLES -> break;
	190	:: else -> {
	191	cycles++;
	192	cpu_exec_start(id)
	193	in_cpu++;
	194	done_cpu++;
	195	in_cpu--;
	196	cpu_exec_end(id)
	197	}
	198	od;
	199	}
	200
	201	byte done_exclusive;
	202	byte in_exclusive;
	203	active[N_EXCLUSIVE] proctype exclusive()
	204	{
	205	cond_t saved;
	206	byte i;
	207
	208	start_exclusive();
	209	in_exclusive = 1;
	210	done_exclusive++;
	211	in_exclusive = 0;
	212	end_exclusive();
	213	}
	214
	215	#define LIVENESS (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
	216	#define SAFETY !(in_exclusive && in_cpu)
	217
	218	never { /* ! ([] SAFETY && <> [] LIVENESS) */
	219	do
	220	// once the liveness property is satisfied, this is not executable
	221	// and the never clause is not accepted
	222	:: ! LIVENESS -> accept_liveness: skip
	223	:: 1 -> assert(SAFETY)
	224	od;
	225	}