Author | Tokens | Token Proportion | Commits | Commit Proportion |
---|---|---|---|---|
Lance Roy | 707 | 99.86% | 1 | 50.00% |
Greg Kroah-Hartman | 1 | 0.14% | 1 | 50.00% |
Total | 708 | 2 |
/* 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
Information contained on this website is for historical information purposes only and does not indicate or represent copyright ownership.
Created with Cregit http://github.com/cregit/cregit
Version 2.0-RC1