diff options
author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-04-27 10:05:51 +0000 |
---|---|---|
committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-04-27 10:05:51 +0000 |
commit | 5d1646d90e1f2cceb9f0828f4b28318cd0ec7744 (patch) | |
tree | a94efe259b9009378be6d90eb30d2b019d95c194 /tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h | |
parent | Initial commit. (diff) | |
download | linux-430c2fc249ea5c0536abd21c23382884005c9093.tar.xz linux-430c2fc249ea5c0536abd21c23382884005c9093.zip |
Adding upstream version 5.10.209.upstream/5.10.209upstream
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h')
-rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h | 221 |
1 files changed, 221 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h new file mode 100644 index 000000000..cf6938d67 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h @@ -0,0 +1,221 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +#ifndef LOCKS_H +#define LOCKS_H + +#include <limits.h> +#include <pthread.h> +#include <stdbool.h> + +#include "assume.h" +#include "bug_on.h" +#include "preempt.h" + +int nondet_int(void); + +#define __acquire(x) +#define __acquires(x) +#define __release(x) +#define __releases(x) + +/* Only use one lock mechanism. Select which one. */ +#ifdef PTHREAD_LOCK +struct lock_impl { + pthread_mutex_t mutex; +}; + +static inline void lock_impl_lock(struct lock_impl *lock) +{ + BUG_ON(pthread_mutex_lock(&lock->mutex)); +} + +static inline void lock_impl_unlock(struct lock_impl *lock) +{ + BUG_ON(pthread_mutex_unlock(&lock->mutex)); +} + +static inline bool lock_impl_trylock(struct lock_impl *lock) +{ + int err = pthread_mutex_trylock(&lock->mutex); + + if (!err) + return true; + else if (err == EBUSY) + return false; + BUG(); +} + +static inline void lock_impl_init(struct lock_impl *lock) +{ + pthread_mutex_init(&lock->mutex, NULL); +} + +#define LOCK_IMPL_INITIALIZER {.mutex = PTHREAD_MUTEX_INITIALIZER} + +#else /* !defined(PTHREAD_LOCK) */ +/* Spinlock that assumes that it always gets the lock immediately. */ + +struct lock_impl { + bool locked; +}; + +static inline bool lock_impl_trylock(struct lock_impl *lock) +{ +#ifdef RUN + /* TODO: Should this be a test and set? */ + return __sync_bool_compare_and_swap(&lock->locked, false, true); +#else + __CPROVER_atomic_begin(); + bool old_locked = lock->locked; + lock->locked = true; + __CPROVER_atomic_end(); + + /* Minimal barrier to prevent accesses leaking out of lock. */ + __CPROVER_fence("RRfence", "RWfence"); + + return !old_locked; +#endif +} + +static inline void lock_impl_lock(struct lock_impl *lock) +{ + /* + * CBMC doesn't support busy waiting, so just assume that the + * lock is available. + */ + assume(lock_impl_trylock(lock)); + + /* + * If the lock was already held by this thread then the assumption + * is unsatisfiable (deadlock). + */ +} + +static inline void lock_impl_unlock(struct lock_impl *lock) +{ +#ifdef RUN + BUG_ON(!__sync_bool_compare_and_swap(&lock->locked, true, false)); +#else + /* Minimal barrier to prevent accesses leaking out of lock. */ + __CPROVER_fence("RWfence", "WWfence"); + + __CPROVER_atomic_begin(); + bool old_locked = lock->locked; + lock->locked = false; + __CPROVER_atomic_end(); + + BUG_ON(!old_locked); +#endif +} + +static inline void lock_impl_init(struct lock_impl *lock) +{ + lock->locked = false; +} + +#define LOCK_IMPL_INITIALIZER {.locked = false} + +#endif /* !defined(PTHREAD_LOCK) */ + +/* + * Implement spinlocks using the lock mechanism. Wrap the lock to prevent mixing + * locks of different types. + */ +typedef struct { + struct lock_impl internal_lock; +} spinlock_t; + +#define SPIN_LOCK_UNLOCKED {.internal_lock = LOCK_IMPL_INITIALIZER} +#define __SPIN_LOCK_UNLOCKED(x) SPIN_LOCK_UNLOCKED +#define DEFINE_SPINLOCK(x) spinlock_t x = SPIN_LOCK_UNLOCKED + +static inline void spin_lock_init(spinlock_t *lock) +{ + lock_impl_init(&lock->internal_lock); +} + +static inline void spin_lock(spinlock_t *lock) +{ + /* + * Spin locks also need to be removed in order to eliminate all + * memory barriers. They are only used by the write side anyway. + */ +#ifndef NO_SYNC_SMP_MB + preempt_disable(); + lock_impl_lock(&lock->internal_lock); +#endif +} + +static inline void spin_unlock(spinlock_t *lock) +{ +#ifndef NO_SYNC_SMP_MB + lock_impl_unlock(&lock->internal_lock); + preempt_enable(); +#endif +} + +/* Don't bother with interrupts */ +#define spin_lock_irq(lock) spin_lock(lock) +#define spin_unlock_irq(lock) spin_unlock(lock) +#define spin_lock_irqsave(lock, flags) spin_lock(lock) +#define spin_unlock_irqrestore(lock, flags) spin_unlock(lock) + +/* + * This is supposed to return an int, but I think that a bool should work as + * well. + */ +static inline bool spin_trylock(spinlock_t *lock) +{ +#ifndef NO_SYNC_SMP_MB + preempt_disable(); + return lock_impl_trylock(&lock->internal_lock); +#else + return true; +#endif +} + +struct completion { + /* Hopefuly this won't overflow. */ + unsigned int count; +}; + +#define COMPLETION_INITIALIZER(x) {.count = 0} +#define DECLARE_COMPLETION(x) struct completion x = COMPLETION_INITIALIZER(x) +#define DECLARE_COMPLETION_ONSTACK(x) DECLARE_COMPLETION(x) + +static inline void init_completion(struct completion *c) +{ + c->count = 0; +} + +static inline void wait_for_completion(struct completion *c) +{ + unsigned int prev_count = __sync_fetch_and_sub(&c->count, 1); + + assume(prev_count); +} + +static inline void complete(struct completion *c) +{ + unsigned int prev_count = __sync_fetch_and_add(&c->count, 1); + + BUG_ON(prev_count == UINT_MAX); +} + +/* This function probably isn't very useful for CBMC. */ +static inline bool try_wait_for_completion(struct completion *c) +{ + BUG(); +} + +static inline bool completion_done(struct completion *c) +{ + return c->count; +} + +/* TODO: Implement complete_all */ +static inline void complete_all(struct completion *c) +{ + BUG(); +} + +#endif |