root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h

INCLUDED FROM

DEFINITIONS

1. lock_impl_lock
2. lock_impl_unlock
3. lock_impl_trylock
4. lock_impl_init
5. lock_impl_trylock
6. lock_impl_lock
7. lock_impl_unlock
8. lock_impl_init
9. spin_lock_init
10. spin_lock
11. spin_unlock
12. spin_trylock
13. init_completion
14. wait_for_completion
15. complete
16. try_wait_for_completion
17. completion_done
18. complete_all

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