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, USE_MUTEX, 17 * TEST_EXPENSIVE. 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 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) 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 70mutex_t mutex; 71cond_t exclusive_cond; 72cond_t exclusive_resume; 73byte pending_cpus; 74 75byte running[N_CPUS]; 76byte 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; \ 104 od; \ 105 MUTEX_UNLOCK(mutex); 106 107#define end_exclusive() \ 108 MUTEX_LOCK(mutex); \ 109 pending_cpus = 0; \ 110 COND_BROADCAST(exclusive_resume); \ 111 MUTEX_UNLOCK(mutex); 112 113#ifdef USE_MUTEX 114// Simple version using mutexes 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; \ 134 MUTEX_UNLOCK(mutex); 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 177 178// Promela processes 179 180byte done_cpu; 181byte in_cpu; 182active[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 201byte done_exclusive; 202byte in_exclusive; 203active[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 218never { /* ! ([] 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} 226