tcg-exclusive.promela (9546B)
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 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; \ 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 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 }