From: Brian Demsky Date: Fri, 12 Oct 2012 05:01:33 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=a4090d03cc1a5f5bca8f10986d74b76a9bb45371;hp=88e6ab1f325b2b67695f20954b5d1f1746d13c8a 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 index 232648cd..00000000 --- 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 - -#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 52198375..5984e722 100644 --- 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 index 00000000..232648cd --- /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 + +#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 8bbd9884..b4410971 100644 --- 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 0122c696..889a960b 100644 --- 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::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 index 00000000..591b2925 --- /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 + +#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 93e87a03..8c4c2a04 100644 --- 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 index 00000000..31fd7eb1 --- /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 035f848d..7b3ff800 100644 --- 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 index 591b2925..00000000 --- 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 - -#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 a96a79c8..b3b517ca 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #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 ce747351..91b0b9a3 100644 --- a/mutex.cc +++ b/mutex.cc @@ -1,4 +1,5 @@ -#include "mutex.h" +#include + #include "model.h" #include "threads-model.h" #include "clockvector.h" diff --git a/mutex.h b/mutex.h deleted file mode 100644 index 53fccb2b..00000000 --- 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