+++ /dev/null
-/** @file cmodelint.h
- * @brief C interface to the model checker.
- */
-
-#ifndef CMODELINT_H
-#define CMODELINT_H
-#include <inttypes.h>
-
-#if __cplusplus
-using std::memory_order;
-extern "C" {
-#endif
-
-uint64_t model_read_action(void * obj, memory_order ord);
-void model_write_action(void * obj, memory_order ord, uint64_t val);
-void model_init_action(void * obj, uint64_t val);
-uint64_t model_rmwr_action(void *obj, memory_order ord);
-void model_rmw_action(void *obj, memory_order ord, uint64_t val);
-void model_rmwc_action(void *obj, memory_order ord);
-void model_fence_action(memory_order ord);
-
-
-#if __cplusplus
-}
-#endif
-
-#endif
+/**
+ * @file atomic
+ * @brief C++11 atomic interface header
+ */
+
#ifndef __CXX_ATOMIC__
#define __CXX_ATOMIC__
--- /dev/null
+/** @file cmodelint.h
+ * @brief C interface to the model checker.
+ */
+
+#ifndef CMODELINT_H
+#define CMODELINT_H
+#include <inttypes.h>
+
+#if __cplusplus
+using std::memory_order;
+extern "C" {
+#endif
+
+uint64_t model_read_action(void * obj, memory_order ord);
+void model_write_action(void * obj, memory_order ord, uint64_t val);
+void model_init_action(void * obj, uint64_t val);
+uint64_t model_rmwr_action(void *obj, memory_order ord);
+void model_rmw_action(void *obj, memory_order ord, uint64_t val);
+void model_rmwc_action(void *obj, memory_order ord);
+void model_fence_action(memory_order ord);
+
+
+#if __cplusplus
+}
+#endif
+
+#endif
+/**
+ * @file cstdatomic
+ * @brief C11 atomic interface header
+ */
#include "impatomic.h"
+/**
+ * @file impatomic.h
+ * @brief Common header for C11/C++11 atomics
+ *
+ * Note that some features are unavailable, as they require support from a true
+ * C11/C++11 compiler.
+ */
+
+#ifndef __IMPATOMIC_H__
+#define __IMPATOMIC_H__
+
#include "memoryorder.h"
#include "cmodelint.h"
} // namespace std
#endif
+#endif /* __IMPATOMIC_H__ */
--- /dev/null
+/** @file librace.h
+ * @brief Interface to check normal memory operations for data races.
+ */
+
+#ifndef __LIBRACE_H__
+#define __LIBRACE_H__
+
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+ void store_8(void *addr, uint8_t val);
+ void store_16(void *addr, uint16_t val);
+ void store_32(void *addr, uint32_t val);
+ void store_64(void *addr, uint64_t val);
+
+ uint8_t load_8(void *addr);
+ uint16_t load_16(void *addr);
+ uint32_t load_32(void *addr);
+ uint64_t load_64(void *addr);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* __LIBRACE_H__ */
+/**
+ * @file memoryorder.h
+ * @brief C11/C++11 atomic memory order listings
+ */
+
#ifndef MEMORYORDER_H
#define MEMORYORDER_H
#ifdef __cplusplus
--- /dev/null
+/**
+ * @file mutex
+ * @brief C++11 mutex interface header
+ */
+
+#ifndef __CXX_MUTEX__
+#define __CXX_MUTEX__
+
+#include "modeltypes.h"
+
+namespace std {
+ struct mutex_state {
+ bool islocked;
+ thread_id_t alloc_tid;
+ modelclock_t alloc_clock;
+ };
+
+ class mutex {
+ public:
+ mutex();
+ ~mutex();
+ void lock();
+ bool try_lock();
+ void unlock();
+ struct mutex_state * get_state() {return &state;}
+
+ private:
+ struct mutex_state state;
+ };
+}
+#endif /* __CXX_MUTEX__ */
+/**
+ * @file stdatomic.h
+ * @brief C11 atomic interface header
+ */
+
#ifndef __STDATOMIC_H__
#define __STDATOMIC_H__
using std::memory_order_acq_rel;
using std::memory_order_seq_cst;
-#endif
+#endif /* __cplusplus */
#endif /* __STDATOMIC_H__ */
+++ /dev/null
-/** @file librace.h
- * @brief Interface to check normal memory operations for data races.
- */
-
-#ifndef __LIBRACE_H__
-#define __LIBRACE_H__
-
-#include <stdint.h>
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
- void store_8(void *addr, uint8_t val);
- void store_16(void *addr, uint16_t val);
- void store_32(void *addr, uint32_t val);
- void store_64(void *addr, uint64_t val);
-
- uint8_t load_8(void *addr);
- uint16_t load_16(void *addr);
- uint32_t load_32(void *addr);
- uint64_t load_64(void *addr);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif /* __LIBRACE_H__ */
#include <stdio.h>
#include <algorithm>
+#include <mutex>
#include "model.h"
#include "action.h"
#include "cyclegraph.h"
#include "promise.h"
#include "datarace.h"
-#include "mutex.h"
#include "threads-model.h"
#define INITIAL_THREAD_ID 0
-#include "mutex.h"
+#include <mutex>
+
#include "model.h"
#include "threads-model.h"
#include "clockvector.h"
+++ /dev/null
-#ifndef MUTEX_H
-#define MUTEX_H
-
-#include "modeltypes.h"
-
-namespace std {
- struct mutex_state {
- bool islocked;
- thread_id_t alloc_tid;
- modelclock_t alloc_clock;
- };
-
- class mutex {
- public:
- mutex();
- ~mutex();
- void lock();
- bool try_lock();
- void unlock();
- struct mutex_state * get_state() {return &state;}
-
- private:
- struct mutex_state state;
- };
-}
-#endif