[thirdparty/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, 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;
}
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	*
	16	* Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, TEST_EXPENSIVE.
	17	*/
	18
	19	// Define the missing parameters for the model
	20	#ifndef N_CPUS
	21	#define N_CPUS 2
	22	#warning defaulting to 2 CPU processes
	23	#endif
	24
	25	// the expensive test is not so expensive for <= 3 CPUs
	26	#if N_CPUS <= 3
	27	#define TEST_EXPENSIVE
	28	#endif
	29
	30	#ifndef N_EXCLUSIVE
	31	# if !defined N_CYCLES \|\| N_CYCLES <= 1 \|\| defined TEST_EXPENSIVE
	32	# define N_EXCLUSIVE 2
	33	# warning defaulting to 2 concurrent exclusive sections
	34	# else
	35	# define N_EXCLUSIVE 1
	36	# warning defaulting to 1 concurrent exclusive sections
	37	# endif
	38	#endif
	39	#ifndef N_CYCLES
	40	# if N_EXCLUSIVE <= 1 \|\| defined TEST_EXPENSIVE
	41	# define N_CYCLES 2
	42	# warning defaulting to 2 CPU cycles
	43	# else
	44	# define N_CYCLES 1
	45	# warning defaulting to 1 CPU cycles
	46	# endif
	47	#endif
	48
	49
	50	// synchronization primitives. condition variables require a
	51	// process-local "cond_t saved;" variable.
	52
	53	#define mutex_t byte
	54	#define MUTEX_LOCK(m) atomic { m == 0 -> m = 1 }
	55	#define MUTEX_UNLOCK(m) m = 0
	56
	57	#define cond_t int
	58	#define COND_WAIT(c, m) { \
	59	saved = c; \
	60	MUTEX_UNLOCK(m); \
	61	c != saved -> MUTEX_LOCK(m); \
	62	}
	63	#define COND_BROADCAST(c) c++
	64
65	// this is the logic from cpus-common.c
66
67	mutex_t mutex;
68	cond_t exclusive_cond;
69	cond_t exclusive_resume;
70	byte pending_cpus;
71
72	byte running[N_CPUS];
73	byte has_waiter[N_CPUS];
74
75	#define exclusive_idle() \
76	do \
77	:: pending_cpus -> COND_WAIT(exclusive_resume, mutex); \
78	:: else -> break; \
79	od
80
81	#define start_exclusive() \
82	MUTEX_LOCK(mutex); \
83	exclusive_idle(); \
84	pending_cpus = 1; \
85	\
86	i = 0; \
87	do \
88	:: i < N_CPUS -> { \
89	if \
90	:: running[i] -> has_waiter[i] = 1; pending_cpus++; \
91	:: else -> skip; \
92	fi; \
93	i++; \
94	} \
95	:: else -> break; \
96	od; \
97	\
98	do \
99	:: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex); \
100	:: else -> break; \
758e1b2b PB	101	od; \
758e1b2b PB	102	MUTEX_UNLOCK(mutex);
a200f2fb PB	103
a200f2fb PB	104	#define end_exclusive() \
758e1b2b	105	MUTEX_LOCK(mutex); \
a200f2fb PB	106	pending_cpus = 0; \
	107	COND_BROADCAST(exclusive_resume); \
	108	MUTEX_UNLOCK(mutex);
	109
	110	#define cpu_exec_start(id) \
	111	MUTEX_LOCK(mutex); \
	112	exclusive_idle(); \
	113	running[id] = 1; \
	114	MUTEX_UNLOCK(mutex);
	115
	116	#define cpu_exec_end(id) \
	117	MUTEX_LOCK(mutex); \
	118	running[id] = 0; \
	119	if \
	120	:: pending_cpus -> { \
	121	pending_cpus--; \
	122	if \
	123	:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
	124	:: else -> skip; \
	125	fi; \
	126	} \
	127	:: else -> skip; \
	128	fi; \
a200f2fb PB	129	MUTEX_UNLOCK(mutex);
	130
	131	// Promela processes
	132
	133	byte done_cpu;
	134	byte in_cpu;
	135	active[N_CPUS] proctype cpu()
	136	{
	137	byte id = _pid % N_CPUS;
	138	byte cycles = 0;
	139	cond_t saved;
	140
	141	do
	142	:: cycles == N_CYCLES -> break;
	143	:: else -> {
	144	cycles++;
	145	cpu_exec_start(id)
	146	in_cpu++;
	147	done_cpu++;
	148	in_cpu--;
	149	cpu_exec_end(id)
	150	}
	151	od;
	152	}
	153
	154	byte done_exclusive;
	155	byte in_exclusive;
	156	active[N_EXCLUSIVE] proctype exclusive()
	157	{
	158	cond_t saved;
	159	byte i;
	160
	161	start_exclusive();
	162	in_exclusive = 1;
	163	done_exclusive++;
	164	in_exclusive = 0;
	165	end_exclusive();
	166	}
	167
	168	#define LIVENESS (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
	169	#define SAFETY !(in_exclusive && in_cpu)
	170
	171	never { /* ! ([] SAFETY && <> [] LIVENESS) */
	172	do
	173	// once the liveness property is satisfied, this is not executable
	174	// and the never clause is not accepted
	175	:: ! LIVENESS -> accept_liveness: skip
	176	:: 1 -> assert(SAFETY)
	177	od;
	178	}