diff options
| -rw-r--r-- | AUTHORS | 3 | ||||
| -rw-r--r-- | COPYING | 56 | ||||
| -rw-r--r-- | config/ax_tls.m4 | 76 | ||||
| -rw-r--r-- | configure.ac | 21 | ||||
| -rw-r--r-- | contrib/editing-with-emacs | 4 | ||||
| -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 |
15 files changed, 292 insertions, 43 deletions
@@ -23,5 +23,8 @@ CVC4 contains the doxygen.m4 autoconf module by Oren Ben-Kiki. CVC4 contains the pkg.m4 autoconf module by Scott James Remnant. +CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and +Diego Elio Petteno. + CVC4 maintainer versions contain the script autogen.sh, by the U.S. Army Research Laboratory @@ -51,23 +51,23 @@ See autogen.sh. Its copyright: Copyright (c) 2005-2009 United States Government as represented by the U.S. Army Research Laboratory. - + Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: - + 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. - + 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. - + 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. - + THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE @@ -95,21 +95,55 @@ copyright. See config/pkg.m4. Its copyright: it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. - + This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. - + You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - + As a special exception to the GNU General Public License, if you distribute this file as part of a program that contains a configuration script generated by Autoconf, you may include it under the same distribution terms that you use for the rest of that program. +CVC4 incorporates the m4 macro file "ax_tls.m4", excluded from the above +copyright and downloaded from +http://www.gnu.org/software/autoconf-archive/ax_tls.html. +See config/ax_tls.m4. Its copyright: + + Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk> + Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com> + + This program is free software: you can redistribute it and/or modify it + under the terms of the GNU General Public License as published by the + Free Software Foundation, either version 3 of the License, or (at your + option) any later version. + + This program is distributed in the hope that it will be useful, but + WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General + Public License for more details. + + You should have received a copy of the GNU General Public License along + with this program. If not, see <http://www.gnu.org/licenses/>. + + As a special exception, the respective Autoconf Macro's copyright owner + gives unlimited permission to copy, distribute and modify the configure + scripts that are the output of Autoconf when processing the Macro. You + need not follow the terms of the GNU General Public License when using + or distributing such scripts, even though portions of the text of the + Macro appear in them. The GNU General Public License (GPL) does govern + all other use of the material that constitutes the Autoconf Macro. + + This special exception to the GPL applies to versions of the Autoconf + Macro released by the Autoconf Archive. When you make and distribute a + modified version of the Autoconf Macro, you may extend this special + exception to the GPL to apply to your modified version as well. + CVC4 incorporates code from ANTLR3, excluded from the above copyright. See http://www.antlr.org/, and the files src/parser/bounded_token_buffer.h, src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp. @@ -119,9 +153,9 @@ Their copyright: Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC http://www.temporal-wave.com http://www.linkedin.com/in/jimidle - + All rights reserved. - + Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: @@ -132,7 +166,7 @@ Their copyright: documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. - + THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. diff --git a/config/ax_tls.m4 b/config/ax_tls.m4 new file mode 100644 index 000000000..1d7736852 --- /dev/null +++ b/config/ax_tls.m4 @@ -0,0 +1,76 @@ +# =========================================================================== +# http://www.gnu.org/software/autoconf-archive/ax_tls.html +# =========================================================================== +# +# SYNOPSIS +# +# AX_TLS([action-if-found], [action-if-not-found]) +# +# DESCRIPTION +# +# Provides a test for the compiler support of thread local storage (TLS) +# extensions. Defines TLS if it is found. Currently knows about GCC/ICC +# and MSVC. I think SunPro uses the same as GCC, and Borland apparently +# supports either. +# +# LICENSE +# +# Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk> +# Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com> +# +# This program is free software: you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by the +# Free Software Foundation, either version 3 of the License, or (at your +# option) any later version. +# +# This program is distributed in the hope that it will be useful, but +# WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General +# Public License for more details. +# +# You should have received a copy of the GNU General Public License along +# with this program. If not, see <http://www.gnu.org/licenses/>. +# +# As a special exception, the respective Autoconf Macro's copyright owner +# gives unlimited permission to copy, distribute and modify the configure +# scripts that are the output of Autoconf when processing the Macro. You +# need not follow the terms of the GNU General Public License when using +# or distributing such scripts, even though portions of the text of the +# Macro appear in them. The GNU General Public License (GPL) does govern +# all other use of the material that constitutes the Autoconf Macro. +# +# This special exception to the GPL applies to versions of the Autoconf +# Macro released by the Autoconf Archive. When you make and distribute a +# modified version of the Autoconf Macro, you may extend this special +# exception to the GPL to apply to your modified version as well. + +#serial 8 + +AC_DEFUN([AX_TLS], [ + AC_MSG_CHECKING(for thread local storage (TLS) class) + AC_CACHE_VAL(ac_cv_tls, [ + ax_tls_keywords="__thread __declspec(thread) none" + for ax_tls_keyword in $ax_tls_keywords; do + AS_CASE([$ax_tls_keyword], + [none], [ac_cv_tls=none ; break], + [AC_TRY_COMPILE( + [#include <stdlib.h> + static void + foo(void) { + static ] $ax_tls_keyword [ int bar; + exit(1); + }], + [], + [ac_cv_tls=$ax_tls_keyword ; break], + ac_cv_tls=none + )]) + done + ]) + AC_MSG_RESULT($ac_cv_tls) + + AS_IF([test "$ac_cv_tls" != "none"], + AC_DEFINE_UNQUOTED([TLS], $ac_cv_tls, [If the compiler supports a TLS storage class define it to that here]) + m4_ifnblank([$1], [$1]), + m4_ifnblank([$2], [$2]) + ) +]) diff --git a/configure.ac b/configure.ac index 8ab8f3792..ae681d2eb 100644 --- a/configure.ac +++ b/configure.ac @@ -655,6 +655,25 @@ AC_CHECK_HEADERS([getopt.h unistd.h]) #AC_TYPE_UINT64_T #AC_TYPE_SIZE_T +# Check for availability of TLS support (e.g. __thread storage class) +AC_MSG_CHECKING([whether user wants wants to use compiler-supported TLS]) +AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS])) +if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then + AC_MSG_RESULT([yes]) + AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=]) +else + AC_MSG_RESULT([no]) + CVC4_TLS= +fi +if test -n "$CVC4_TLS"; then + CVC4_TLS_SUPPORTED=1 +else + CVC4_TLS='pthread_getspecific()' + CVC4_TLS_SUPPORTED=0 +fi +AC_SUBST([CVC4_TLS]) +AC_SUBST([CVC4_TLS_SUPPORTED]) + # Checks for library functions. # (empty) @@ -726,6 +745,7 @@ AC_CONFIG_FILES([ m4_esyscmd([find contrib src test -name Makefile.am | sort | sed 's,\.am$,,']) src/util/rational.h src/util/integer.h + src/util/tls.h ) AC_OUTPUT @@ -786,6 +806,7 @@ Unit tests : $support_unit_tests Static libs : $enable_static Shared libs : $enable_shared Static binary: $enable_static_binary +TLS support : $CVC4_TLS MP library : $mplibrary diff --git a/contrib/editing-with-emacs b/contrib/editing-with-emacs index 66ee555a9..529e4fadc 100644 --- a/contrib/editing-with-emacs +++ b/contrib/editing-with-emacs @@ -12,7 +12,7 @@ describing your usual cvc4 editing location(s): (setq c-basic-offset 2) (c-set-offset 'innamespace 0) (setq indent-tabs-mode nil)) -(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\|y\\|yy\\|ypp\\|lex\\|l\\|ll\\|lpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist)) +(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\|y\\|yy\\|ypp\\|lex\\|l\\|ll\\|lpp\\)\\(\\.in\\)?$" . cvc4-c++-editing-mode) auto-mode-alist)) --- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 18:19:22 -0500 +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 27 Sep 2010 17:35:38 -0400 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 */ |