summaryrefslogtreecommitdiff
path: root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
diff options
context:
space:
mode:
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.h220
1 files changed, 220 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 000000000000..356004665576
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h
@@ -0,0 +1,220 @@
+#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