1 #ifndef LOCKS_H 2 #define LOCKS_H 3 4 #include <limits.h> 5 #include <pthread.h> 6 #include <stdbool.h> 7 8 #include "assume.h" 9 #include "bug_on.h" 10 #include "preempt.h" 11 12 int nondet_int(void); 13 14 #define __acquire(x) 15 #define __acquires(x) 16 #define __release(x) 17 #define __releases(x) 18 19 /* Only use one lock mechanism. Select which one. */ 20 #ifdef PTHREAD_LOCK 21 struct lock_impl { 22 pthread_mutex_t mutex; 23 }; 24 25 static inline void lock_impl_lock(struct lock_impl *lock) 26 { 27 BUG_ON(pthread_mutex_lock(&lock->mutex)); 28 } 29 30 static inline void lock_impl_unlock(struct lock_impl *lock) 31 { 32 BUG_ON(pthread_mutex_unlock(&lock->mutex)); 33 } 34 35 static inline bool lock_impl_trylock(struct lock_impl *lock) 36 { 37 int err = pthread_mutex_trylock(&lock->mutex); 38 39 if (!err) 40 return true; 41 else if (err == EBUSY) 42 return false; 43 BUG(); 44 } 45 46 static inline void lock_impl_init(struct lock_impl *lock) 47 { 48 pthread_mutex_init(&lock->mutex, NULL); 49 } 50 51 #define LOCK_IMPL_INITIALIZER {.mutex = PTHREAD_MUTEX_INITIALIZER} 52 53 #else /* !defined(PTHREAD_LOCK) */ 54 /* Spinlock that assumes that it always gets the lock immediately. */ 55 56 struct lock_impl { 57 bool locked; 58 }; 59 60 static inline bool lock_impl_trylock(struct lock_impl *lock) 61 { 62 #ifdef RUN 63 /* TODO: Should this be a test and set? */ 64 return __sync_bool_compare_and_swap(&lock->locked, false, true); 65 #else 66 __CPROVER_atomic_begin(); 67 bool old_locked = lock->locked; 68 lock->locked = true; 69 __CPROVER_atomic_end(); 70 71 /* Minimal barrier to prevent accesses leaking out of lock. */ 72 __CPROVER_fence("RRfence", "RWfence"); 73 74 return !old_locked; 75 #endif 76 } 77 78 static inline void lock_impl_lock(struct lock_impl *lock) 79 { 80 /* 81 * CBMC doesn't support busy waiting, so just assume that the 82 * lock is available. 83 */ 84 assume(lock_impl_trylock(lock)); 85 86 /* 87 * If the lock was already held by this thread then the assumption 88 * is unsatisfiable (deadlock). 89 */ 90 } 91 92 static inline void lock_impl_unlock(struct lock_impl *lock) 93 { 94 #ifdef RUN 95 BUG_ON(!__sync_bool_compare_and_swap(&lock->locked, true, false)); 96 #else 97 /* Minimal barrier to prevent accesses leaking out of lock. */ 98 __CPROVER_fence("RWfence", "WWfence"); 99 100 __CPROVER_atomic_begin(); 101 bool old_locked = lock->locked; 102 lock->locked = false; 103 __CPROVER_atomic_end(); 104 105 BUG_ON(!old_locked); 106 #endif 107 } 108 109 static inline void lock_impl_init(struct lock_impl *lock) 110 { 111 lock->locked = false; 112 } 113 114 #define LOCK_IMPL_INITIALIZER {.locked = false} 115 116 #endif /* !defined(PTHREAD_LOCK) */ 117 118 /* 119 * Implement spinlocks using the lock mechanism. Wrap the lock to prevent mixing 120 * locks of different types. 121 */ 122 typedef struct { 123 struct lock_impl internal_lock; 124 } spinlock_t; 125 126 #define SPIN_LOCK_UNLOCKED {.internal_lock = LOCK_IMPL_INITIALIZER} 127 #define __SPIN_LOCK_UNLOCKED(x) SPIN_LOCK_UNLOCKED 128 #define DEFINE_SPINLOCK(x) spinlock_t x = SPIN_LOCK_UNLOCKED 129 130 static inline void spin_lock_init(spinlock_t *lock) 131 { 132 lock_impl_init(&lock->internal_lock); 133 } 134 135 static inline void spin_lock(spinlock_t *lock) 136 { 137 /* 138 * Spin locks also need to be removed in order to eliminate all 139 * memory barriers. They are only used by the write side anyway. 140 */ 141 #ifndef NO_SYNC_SMP_MB 142 preempt_disable(); 143 lock_impl_lock(&lock->internal_lock); 144 #endif 145 } 146 147 static inline void spin_unlock(spinlock_t *lock) 148 { 149 #ifndef NO_SYNC_SMP_MB 150 lock_impl_unlock(&lock->internal_lock); 151 preempt_enable(); 152 #endif 153 } 154 155 /* Don't bother with interrupts */ 156 #define spin_lock_irq(lock) spin_lock(lock) 157 #define spin_unlock_irq(lock) spin_unlock(lock) 158 #define spin_lock_irqsave(lock, flags) spin_lock(lock) 159 #define spin_unlock_irqrestore(lock, flags) spin_unlock(lock) 160 161 /* 162 * This is supposed to return an int, but I think that a bool should work as 163 * well. 164 */ 165 static inline bool spin_trylock(spinlock_t *lock) 166 { 167 #ifndef NO_SYNC_SMP_MB 168 preempt_disable(); 169 return lock_impl_trylock(&lock->internal_lock); 170 #else 171 return true; 172 #endif 173 } 174 175 struct completion { 176 /* Hopefuly this won't overflow. */ 177 unsigned int count; 178 }; 179 180 #define COMPLETION_INITIALIZER(x) {.count = 0} 181 #define DECLARE_COMPLETION(x) struct completion x = COMPLETION_INITIALIZER(x) 182 #define DECLARE_COMPLETION_ONSTACK(x) DECLARE_COMPLETION(x) 183 184 static inline void init_completion(struct completion *c) 185 { 186 c->count = 0; 187 } 188 189 static inline void wait_for_completion(struct completion *c) 190 { 191 unsigned int prev_count = __sync_fetch_and_sub(&c->count, 1); 192 193 assume(prev_count); 194 } 195 196 static inline void complete(struct completion *c) 197 { 198 unsigned int prev_count = __sync_fetch_and_add(&c->count, 1); 199 200 BUG_ON(prev_count == UINT_MAX); 201 } 202 203 /* This function probably isn't very useful for CBMC. */ 204 static inline bool try_wait_for_completion(struct completion *c) 205 { 206 BUG(); 207 } 208 209 static inline bool completion_done(struct completion *c) 210 { 211 return c->count; 212 } 213 214 /* TODO: Implement complete_all */ 215 static inline void complete_all(struct completion *c) 216 { 217 BUG(); 218 } 219 220 #endif 221
