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 67mutex_t mutex; 68cond_t exclusive_cond; 69cond_t exclusive_resume; 70byte pending_cpus; 71 72byte running[N_CPUS]; 73byte 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; \ 101 od; \ 102 MUTEX_UNLOCK(mutex); 103 104#define end_exclusive() \ 105 MUTEX_LOCK(mutex); \ 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; \ 129 MUTEX_UNLOCK(mutex); 130 131// Promela processes 132 133byte done_cpu; 134byte in_cpu; 135active[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 154byte done_exclusive; 155byte in_exclusive; 156active[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 171never { /* ! ([] 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} 179