text: #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
  