diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 3 | ||||
-rw-r--r-- | src/main/util.cpp | 3 | ||||
-rw-r--r-- | src/util/Assert.cpp | 3 | ||||
-rw-r--r-- | src/util/Assert.h | 3 | ||||
-rw-r--r-- | src/util/Makefile.am | 6 | ||||
-rw-r--r-- | src/util/configuration.cpp | 8 | ||||
-rw-r--r-- | src/util/configuration.h | 2 | ||||
-rw-r--r-- | src/util/configuration_private.h | 54 | ||||
-rw-r--r-- | src/util/tls.h.in | 90 |
10 files changed, 145 insertions, 30 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 1f15f7e29..31b848885 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -28,6 +28,7 @@ #include "theory/bv/theory_bv_type_rules.h" #include "util/Assert.h" +#include "util/tls.h" #include <ext/hash_set> #include <algorithm> @@ -38,7 +39,7 @@ using __gnu_cxx::hash_set; namespace CVC4 { -__thread NodeManager* NodeManager::s_current = 0; +CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = 0; /** * This class sets it reference argument to true and ensures that it gets set diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index bf1bed5f0..5fb7c57ad 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -38,6 +38,7 @@ #include "expr/node_value.h" #include "context/context.h" #include "util/configuration_private.h" +#include "util/tls.h" namespace CVC4 { @@ -70,7 +71,7 @@ class NodeManager { expr::NodeValueIDHashFunction, expr::NodeValueEq> ZombieSet; - static __thread NodeManager* s_current; + static CVC4_THREADLOCAL(NodeManager*) s_current; NodeValuePool d_nodeValuePool; diff --git a/src/main/util.cpp b/src/main/util.cpp index 968563b97..ddb9f84c8 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -94,7 +94,8 @@ void cvc4unexpected() { fprintf(stderr, "The exception is unknown (maybe it's not a CVC4::Exception).\n\n"); } else { - fprintf(stderr, "The exception is:\n%s\n\n", CVC4::s_debugLastException); + fprintf(stderr, "The exception is:\n%s\n\n", + static_cast<const char*>(CVC4::s_debugLastException)); } if(segvNoSpin) { fprintf(stderr, "No-spin requested.\n"); diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 7856b3da4..01c40aca2 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -22,13 +22,14 @@ #include "util/Assert.h" #include "util/exception.h" +#include "util/tls.h" using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -__thread CVC4_PUBLIC const char* s_debugLastException = NULL; +CVC4_PUBLIC CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; #endif /* CVC4_DEBUG */ void AssertionException::construct(const char* header, const char* extra, diff --git a/src/util/Assert.h b/src/util/Assert.h index 62375daff..65c067b7e 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -29,6 +29,7 @@ #include "util/exception.h" #include "util/output.h" +#include "util/tls.h" namespace CVC4 { @@ -199,7 +200,7 @@ public: #ifdef CVC4_DEBUG #ifdef CVC4_DEBUG -extern __thread CVC4_PUBLIC const char* s_debugLastException; +extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException; #endif /* CVC4_DEBUG */ /** diff --git a/src/util/Makefile.am b/src/util/Makefile.am index bac0064bf..78f91edc5 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -39,7 +39,8 @@ libutil_la_SOURCES = \ BUILT_SOURCES = \ rational.h \ - integer.h + integer.h \ + tls.h if CVC4_CLN_IMP libutil_la_SOURCES += \ @@ -62,4 +63,5 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ integer_gmp_imp.cpp \ rational.h.in \ - integer.h.in + integer.h.in \ + tls.h.in diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 072a93b18..499b0c8e2 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -78,11 +78,15 @@ string Configuration::about() { } bool Configuration::isBuiltWithGmp() { - return IS_GMP_BUILD; + return IS_GMP_BUILD; } bool Configuration::isBuiltWithCln() { - return IS_CLN_BUILD; + return IS_CLN_BUILD; +} + +bool Configuration::isBuiltWithTlsSupport() { + return USING_TLS; } }/* CVC4 namespace */ diff --git a/src/util/configuration.h b/src/util/configuration.h index cca9202bf..ff89a3d6c 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -66,6 +66,8 @@ public: static bool isBuiltWithGmp(); static bool isBuiltWithCln(); + + static bool isBuiltWithTlsSupport(); }; }/* CVC4 namespace */ diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 913fcc3e9..227250745 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -11,10 +11,15 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Provides compile-time configuration information about the + ** \brief Provides compile-time configuration information about the ** CVC4 library. **/ +#include "cvc4_private.h" + +#ifndef __CVC4__CONFIGURATION_PRIVATE_H +#define __CVC4__CONFIGURATION_PRIVATE_H + #include "cvc4autoconfig.h" using namespace std; @@ -22,59 +27,65 @@ using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -#define IS_DEBUG_BUILD true +# define IS_DEBUG_BUILD true #else /* CVC4_DEBUG */ -#define IS_DEBUG_BUILD false +# define IS_DEBUG_BUILD false #endif /* CVC4_DEBUG */ - + #ifdef CVC4_TRACING -#define IS_TRACING_BUILD true +# define IS_TRACING_BUILD true #else /* CVC4_TRACING */ -#define IS_TRACING_BUILD false +# define IS_TRACING_BUILD false #endif /* CVC4_TRACING */ #ifdef CVC4_MUZZLE -#define IS_MUZZLED_BUILD true +# define IS_MUZZLED_BUILD true #else /* CVC4_MUZZLE */ -#define IS_MUZZLED_BUILD false +# define IS_MUZZLED_BUILD false #endif /* CVC4_MUZZLE */ #ifdef CVC4_ASSERTIONS -#define IS_ASSERTIONS_BUILD true +# define IS_ASSERTIONS_BUILD true #else /* CVC4_ASSERTIONS */ -#define IS_ASSERTIONS_BUILD false +# define IS_ASSERTIONS_BUILD false #endif /* CVC4_ASSERTIONS */ #ifdef CVC4_COVERAGE -#define IS_COVERAGE_BUILD true +# define IS_COVERAGE_BUILD true #else /* CVC4_COVERAGE */ -#define IS_COVERAGE_BUILD false +# define IS_COVERAGE_BUILD false #endif /* CVC4_COVERAGE */ #ifdef CVC4_PROFILING -#define IS_PROFILING_BUILD true +# define IS_PROFILING_BUILD true #else /* CVC4_PROFILING */ -#define IS_PROFILING_BUILD false +# define IS_PROFILING_BUILD false #endif /* CVC4_PROFILING */ #ifdef CVC4_COMPETITION_MODE -#define IS_COMPETITION_BUILD true +# define IS_COMPETITION_BUILD true #else /* CVC4_COMPETITION_MODE */ -#define IS_COMPETITION_BUILD false +# define IS_COMPETITION_BUILD false #endif /* CVC4_COMPETITION_MODE */ #ifdef CVC4_GMP_IMP -#define IS_GMP_BUILD true +# define IS_GMP_BUILD true #else /* CVC4_GMP_IMP */ -#define IS_GMP_BUILD false +# define IS_GMP_BUILD false #endif /* CVC4_GMP_IMP */ #ifdef CVC4_CLN_IMP -#define IS_CLN_BUILD true +# define IS_CLN_BUILD true #else /* CVC4_CLN_IMP */ -#define IS_CLN_BUILD false +# define IS_CLN_BUILD false #endif /* CVC4_CLN_IMP */ +#ifdef TLS +# define USING_TLS true +#else /* TLS */ +# define USING_TLS false +#endif /* TLS */ + #define CVC4_ABOUT_STRING string("\ This is a pre-release of CVC4.\n\ Copyright (C) 2009, 2010\n\ @@ -92,5 +103,6 @@ of CVC4 that links against GMP, and can be used in such applications.\n" : \ "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\ CVC4 is open-source and is covered by the BSD license (modified).\n") - }/* CVC4 namespace */ + +#endif /* __CVC4__CONFIGURATION_PRIVATE_H */ diff --git a/src/util/tls.h.in b/src/util/tls.h.in new file mode 100644 index 000000000..29a52497a --- /dev/null +++ b/src/util/tls.h.in @@ -0,0 +1,90 @@ +/********************* */ +/*! \file tls.h.in + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Header to define CVC4_THREAD whether or not TLS is + ** supported by the compiler/runtime platform + ** + ** Header to define CVC4_THREAD whether or not TLS is supported by + ** the compiler/runtime platform. If not, an implementation based on + ** pthread_getspecific() / pthread_setspecific() is given. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__TLS_H +#define __CVC4__TLS_H + +#if @CVC4_TLS_SUPPORTED@ +# define CVC4_THREADLOCAL(__type) @CVC4_TLS@ __type +# define CVC4_THREADLOCAL_PUBLIC(__type) @CVC4_TLS@ CVC4_PUBLIC __type +#else +# include <pthread.h> +# define CVC4_THREADLOCAL(__type) ::CVC4::ThreadLocal< __type > +# define CVC4_THREADLOCAL_PUBLIC(__type) CVC4_PUBLIC ::CVC4::ThreadLocal< __type > + +namespace CVC4 { + +template <class T, bool small> +class ThreadLocalImpl; + +template <class T> +class ThreadLocalImpl<T, true> { + pthread_key_t d_key; + + static void cleanup(void*) { + } + +public: + ThreadLocalImpl() { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + } + + ThreadLocalImpl(T t) { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t))); + } + + ThreadLocalImpl(const ThreadLocalImpl& tl) { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl)))); + } + + ThreadLocalImpl& operator=(const T& t) { + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t))); + return *this; + } + ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) { + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl)))); + return *this; + } + + operator T() const { + return reinterpret_cast<T>(pthread_getspecific(d_key)); + } +};/* class ThreadLocalImpl<T, true> */ + +template <class T> +class ThreadLocal : public ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> { + typedef ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> super; + +public: + ThreadLocal() : super() {} + ThreadLocal(const T& t) : super(t) {} + ThreadLocal(const ThreadLocal<T>& tl) : super(tl) {} +};/* class ThreadLocal<T> */ + +}/* CVC4 namespace */ + +#endif /* @CVC4_TLS_SUPPORTED@ */ + +#endif /* _CVC4__TLS_H */ |