Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

diff --git a/cmodelint.h b/cmodelint.h
deleted file mode 100644 (file)
index 232648c..0000000
--- a/cmodelint.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/** @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

diff --git a/include/atomic b/include/atomic
index 52198375aff4221a58d86326209216f5dc35e93d..5984e722b3f27fe008e6504137a26ac1b1a2d048 100644 (file)
--- a/include/atomic
+++ b/include/atomic
@@ -1,3 +1,8 @@
+/**
+ * @file atomic
+ * @brief C++11 atomic interface header
+ */
+
 #ifndef __CXX_ATOMIC__
 #define __CXX_ATOMIC__
 

diff --git a/include/cmodelint.h b/include/cmodelint.h
new file mode 100644 (file)
index 0000000..232648c
--- /dev/null
+++ b/include/cmodelint.h
@@ -0,0 +1,27 @@
+/** @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

diff --git a/include/cstdatomic b/include/cstdatomic
index 8bbd988406b09e1fa8d374967b39ef7cc6263432..b44109713697838f74f209647ae0e097ba932e01 100644 (file)
--- a/include/cstdatomic
+++ b/include/cstdatomic
@@ -1,3 +1,7 @@
+/**
+ * @file cstdatomic
+ * @brief C11 atomic interface header
+ */
 
 #include "impatomic.h"
 

diff --git a/include/impatomic.h b/include/impatomic.h
index 0122c69602b33ca0b6231821f74d012468f1e884..889a960b3888a1beab03d3dc75c9acf92541ea79 100644 (file)
--- a/include/impatomic.h
+++ b/include/impatomic.h
@@ -1,3 +1,14 @@
+/**
+ * @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"
 
@@ -3985,3 +3996,4 @@ T* atomic<T*>::fetch_sub( ptrdiff_t __v__, memory_order __x__ ) volatile
 } // namespace std
 #endif
 
+#endif /* __IMPATOMIC_H__ */

diff --git a/include/librace.h b/include/librace.h
new file mode 100644 (file)
index 0000000..591b292
--- /dev/null
+++ b/include/librace.h
@@ -0,0 +1,28 @@
+/** @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__ */

diff --git a/include/memoryorder.h b/include/memoryorder.h
index 93e87a037001fff1c6db234f1d459fa092eddb31..8c4c2a047c11df7c526495054458f9be4099a4d7 100644 (file)
--- a/include/memoryorder.h
+++ b/include/memoryorder.h
@@ -1,3 +1,8 @@
+/**
+ * @file memoryorder.h
+ * @brief C11/C++11 atomic memory order listings
+ */
+
 #ifndef MEMORYORDER_H
 #define MEMORYORDER_H
 #ifdef __cplusplus

diff --git a/include/mutex b/include/mutex
new file mode 100644 (file)
index 0000000..31fd7eb
--- /dev/null
+++ b/include/mutex
@@ -0,0 +1,31 @@
+/**
+ * @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__ */

diff --git a/include/stdatomic.h b/include/stdatomic.h
index 035f848d33b648eaad450e7c29d38b7b422c5060..7b3ff8004546e77e9e8996d521ebaf46e57aa994 100644 (file)
--- a/include/stdatomic.h
+++ b/include/stdatomic.h
@@ -1,3 +1,8 @@
+/**
+ * @file stdatomic.h
+ * @brief C11 atomic interface header
+ */
+
 #ifndef __STDATOMIC_H__
 #define __STDATOMIC_H__
 
@@ -59,6 +64,6 @@ using std::memory_order_release;
 using std::memory_order_acq_rel;
 using std::memory_order_seq_cst;
 
-#endif
+#endif /* __cplusplus */
 
 #endif /* __STDATOMIC_H__ */

diff --git a/librace.h b/librace.h
deleted file mode 100644 (file)
index 591b292..0000000
--- a/librace.h
+++ /dev/null
@@ -1,28 +0,0 @@
-/** @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__ */

diff --git a/model.cc b/model.cc
index a96a79c851ee83b5624df3bdafda7487802bf5b1..b3b517caed9c087b0ed1daaeb9a271c4a3a7bc20 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1,5 +1,6 @@
 #include <stdio.h>
 #include <algorithm>
+#include <mutex>
 
 #include "model.h"
 #include "action.h"
@@ -11,7 +12,6 @@
 #include "cyclegraph.h"
 #include "promise.h"
 #include "datarace.h"
-#include "mutex.h"
 #include "threads-model.h"
 
 #define INITIAL_THREAD_ID      0

diff --git a/mutex.cc b/mutex.cc
index ce747351d09d328708d5410874f77eb40725df1e..91b0b9a33f8a4109d82e9334f127534b1d6ec137 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -1,4 +1,5 @@
-#include "mutex.h"
+#include <mutex>
+
 #include "model.h"
 #include "threads-model.h"
 #include "clockvector.h"

diff --git a/mutex.h b/mutex.h
deleted file mode 100644 (file)
index 53fccb2..0000000
--- a/mutex.h
+++ /dev/null
@@ -1,26 +0,0 @@
-#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