Use thread_local instead of compiler extensions (#210)

C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.

27 files changed, 70 insertions, 390 deletions

diff --git a/COPYING b/COPYING
index 4e3e64bce..b251f6c77 100644
--- a/COPYING
+++ b/COPYING
@@ -130,40 +130,6 @@ copyright.  See config/pkg.m4.  Its copyright:
   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 Petteno` <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 the m4 macro file "boost.m4", excluded from the above
 copyright and downloaded from http://github.com/tsuna/boost.m4 .
 See config/boost.m4.  Its copyright:
diff --git a/config/ax_tls.m4 b/config/ax_tls.m4
deleted file mode 100644
index 033e3b135..000000000
--- a/config/ax_tls.m4
+++ /dev/null
@@ -1,76 +0,0 @@
-# ===========================================================================
-#          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 Petteno` <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 10
-
-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 1c0240f36..a46585a77 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1213,35 +1213,6 @@ fi
 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
 
-# Check for availability of TLS support (e.g. __thread storage class)
-AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
-AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
-if test $cvc4_has_threads = no; then
-  # We disable TLS entirely by simply telling the build system that
-  # the empty string is the __thread keyword.
-  AC_MSG_RESULT([multithreading disabled])
-  CVC4_TLS_SUPPORTED=1
-  CVC4_TLS=
-  CVC4_TLS_explanation='disabled (no multithreading support)'
-else
-  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
-    CVC4_TLS_explanation="$CVC4_TLS"
-  else
-    CVC4_TLS_explanation='pthread_getspecific()'
-    CVC4_TLS_SUPPORTED=0
-  fi
-fi
-AC_SUBST([CVC4_TLS])
-AC_SUBST([CVC4_TLS_SUPPORTED])
-
 # Whether to compile with google profiling tools
 cvc4_use_google_perftools=0
 AC_ARG_WITH(
@@ -1499,7 +1470,6 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then
   fi
 fi
 
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 
@@ -1540,7 +1510,6 @@ Compat lib   : $CVC4_BUILD_LIBCOMPAT
 Bindings     : $bindings_to_be_built
 
 Multithreaded: $support_multithreaded
-TLS support  : $CVC4_TLS_explanation
 Portfolio    : $with_portfolio
 
 MP library   : $mplibrary
diff --git a/src/Makefile.am b/src/Makefile.am
index 916733016..974f599e4 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -620,7 +620,6 @@ install-data-local:
 	(echo include/cvc4.h; \
 	 echo include/cvc4_public.h; \
 	 echo include/cvc4parser_public.h; \
-	 echo base/tls.h; \
 	 echo util/integer.h; \
 	 echo util/rational.h; \
 	 find * -name '*.h' | \
@@ -653,7 +652,6 @@ uninstall-local:
 	-(echo include/cvc4.h; \
 	  echo include/cvc4_public.h; \
 	  echo include/cvc4parser_public.h; \
-	  echo base/tls.h; \
 	  echo util/integer.h; \
 	  echo util/rational.h; \
 	  find * -name '*.h' | \
diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index 491baaa90..5537bbbdd 100644
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -5,7 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbase.la
 
-# Do not list built sources (like tls.h) here!
+# Do not list built sources here!
 # Rather, list them under BUILT_SOURCES, and their .in versions under
 # EXTRA_DIST.  Otherwise, they're packaged up in the tarball, which is
 # no good---they belong in the configured builds/ directory.  If they
@@ -26,17 +26,14 @@ libbase_la_SOURCES = \
 	listener.h \
 	modal_exception.h \
 	output.cpp \
-	output.h
-
-
-BUILT_SOURCES = \
+	output.h \
 	tls.h
 
 # listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it
 # after building (if it does, we don't get the "cached" effect with
 # the .tmp files below, and we have to re-compile and re-link each
 # time, even when there are no changes).
-BUILT_SOURCES += \
+BUILT_SOURCES = \
 	Debug_tags.h \
 	Debug_tags \
 	Trace_tags.h \
@@ -55,12 +52,7 @@ EXTRA_DIST = \
 	exception.i \
 	mktagheaders \
 	mktags \
-	modal_exception.i \
-	tls.h.in
-
-DISTCLEANFILES = \
-	tls.h.tmp \
-	tls.h
+	modal_exception.i
 
 %_tags.h: %_tags mktagheaders
 	$(AM_V_at)chmod +x @srcdir@/mktagheaders
diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
index c122667f3..f342f5562 100644
--- a/src/base/cvc4_assert.cpp
+++ b/src/base/cvc4_assert.cpp
@@ -20,13 +20,14 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
+#include "base/tls.h"
 
 using namespace std;
 
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-//CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
+//CVC4_THREAD_LOCAL const char* s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 
@@ -140,7 +141,7 @@ void AssertionException::construct(const char* header, const char* extra,
  */
 void debugAssertionFailed(const AssertionException& thisException,
                           const char* propagatingException) {
-  static CVC4_THREADLOCAL(bool) alreadyFired = false;
+  static CVC4_THREAD_LOCAL bool alreadyFired = false;
 
   if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
     throw thisException;
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
index d4942f47c..bb4d57170 100644
--- a/src/base/cvc4_assert.h
+++ b/src/base/cvc4_assert.h
@@ -26,7 +26,6 @@
 #include <string>
 
 #include "base/exception.h"
-#include "base/tls.h"
 
 // output.h not strictly needed for this header, but it _is_ needed to
 // actually _use_ anything in this header, so let's include it.
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index 7df050726..990ae77c6 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -28,7 +28,7 @@ using namespace std;
 
 namespace CVC4 {
 
-CVC4_THREADLOCAL(LastExceptionBuffer*) LastExceptionBuffer::s_currentBuffer = NULL;
+CVC4_THREAD_LOCAL LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL;
 
 LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {}
 
diff --git a/src/base/exception.h b/src/base/exception.h
index 1ce2ae757..01a054b19 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -160,7 +160,7 @@ private:
 
   char* d_contents;
 
-  static CVC4_THREADLOCAL(LastExceptionBuffer*) s_currentBuffer;
+  static CVC4_THREAD_LOCAL LastExceptionBuffer* s_currentBuffer;
 }; /* class LastExceptionBuffer */
 
 }/* CVC4 namespace */
diff --git a/src/base/tls.h b/src/base/tls.h
new file mode 100644
index 000000000..a60b0d8f9
--- /dev/null
+++ b/src/base/tls.h
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file tls.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Definiton of CVC4_THREAD_LOCAL
+ **
+ ** This header defines CVC4_THREAD_LOCAL, which should be used instead of
+ ** thread_local because it is not supported by all build types (e.g. Swig).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__BASE__TLS_H
+#define __CVC4__BASE__TLS_H
+
+#if SWIG && (!defined(SWIG_VERSION) || SWIG_VERSION < 0x030000)
+// SWIG versions older than 3.0 do not support thread_local, so just redefine
+// CVC4_THREAD_LOCAL to be empty for those versions.
+#define CVC4_THREAD_LOCAL
+#else
+#define CVC4_THREAD_LOCAL thread_local
+#endif
+
+#endif /* __CVC4__BASE__TLS_H */
diff --git a/src/base/tls.h.in b/src/base/tls.h.in
deleted file mode 100644
index c66aef767..000000000
--- a/src/base/tls.h.in
+++ /dev/null
@@ -1,198 +0,0 @@
-/*********************                                                        */
-/*! \file tls.h.in
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, ACSYS, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  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
-
-// A bit obnoxious: we have to take varargs to support multi-argument
-// template types in the threadlocals.
-// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise,
-// due to the embedded comma.
-#if @CVC4_TLS_SUPPORTED@
-#  define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type
-#  define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type
-#  define CVC4_THREADLOCAL_TYPE(__type...) __type
-#else
-#  include <pthread.h>
-#  define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
-#  define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
-#  define CVC4_THREADLOCAL_TYPE(__type...) ::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(const 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 static_cast<T>(reinterpret_cast<size_t>(pthread_getspecific(d_key)));
-  }
-};/* class ThreadLocalImpl<T, true> */
-
-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(const 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 static_cast<T*>(pthread_getspecific(d_key));
-  }
-
-  T operator*() {
-    return *static_cast<T*>(pthread_getspecific(d_key));
-  }
-  T* operator->() {
-    return static_cast<T*>(pthread_getspecific(d_key));
-  }
-};/* class ThreadLocalImpl<T*, true> */
-
-template <class T>
-class ThreadLocalImpl<T, false> {
-};/* class ThreadLocalImpl<T, false> */
-
-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) {}
-
-  ThreadLocal<T>& operator=(const T& t) {
-    return static_cast< ThreadLocal<T>& >(super::operator=(t));
-  }
-  ThreadLocal<T>& operator=(const ThreadLocal<T>& tl) {
-    return static_cast< ThreadLocal<T>& >(super::operator=(tl));
-  }
-};/* class ThreadLocal<T> */
-
-template <class T>
-class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> {
-  typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super;
-
-public:
-  ThreadLocal() : super() {}
-  ThreadLocal(T* t) : super(t) {}
-  ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {}
-
-  ThreadLocal<T*>& operator=(T* t) {
-    return static_cast< ThreadLocal<T*>& >(super::operator=(t));
-  }
-  ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) {
-    return static_cast< ThreadLocal<T*>& >(super::operator=(tl));
-  }
-  // special operators for pointers
-  T& operator*() {
-    return *static_cast<T*>(*this);
-  }
-  const T& operator*() const {
-    return *static_cast<const T*>(*this);
-  }
-  T* operator->() {
-    return static_cast<T*>(*this);
-  }
-  const T* operator->() const {
-    return static_cast<const T*>(*this);
-  }
-  T* operator++() {
-    T* p = *this;
-    *this = ++p;
-    return p;
-  }
-  T* operator++(int) {
-    T* p = *this;
-    *this = p + 1;
-    return p;
-  }
-  T* operator--() {
-    T* p = *this;
-    *this = --p;
-    return p;
-  }
-  T* operator--(int) {
-    T* p = *this;
-    *this = p - 1;
-    return p;
-  }
-};/* class ThreadLocal<T*> */
-
-}/* CVC4 namespace */
-
-#endif /* @CVC4_TLS_SUPPORTED@ */
-
-#endif /* __CVC4__TLS_H */
diff --git a/src/bindings/swig.h b/src/bindings/swig.h
index f73ddd9bb..053cb7172 100644
--- a/src/bindings/swig.h
+++ b/src/bindings/swig.h
@@ -26,15 +26,9 @@
 #endif /* SWIG_VERSION */
 
 %import "cvc4_public.h"
-#warning "Working around a SWIG segfault in C++ template parsing."
-//%import "base/tls.h"
-#define CVC4_THREADLOCAL(__type...) __type
-#define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC __type
-#define CVC4_THREADLOCAL_TYPE(__type...) __type
+%import "base/tls.h"
 
-// swig doesn't like the __thread storage class...
-#define __thread
-// ...or GCC attributes
+// swig doesn't like GCC attributes
 #define __attribute__(x)
 
 #endif /* __CVC4__BINDINGS__SWIG_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e440261cb..33f057274 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -23,7 +23,6 @@
 
 #include "base/cvc4_assert.h"
 #include "base/listener.h"
-#include "base/tls.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_manager_listeners.h"
@@ -38,7 +37,7 @@ using namespace CVC4::expr;
 
 namespace CVC4 {
 
-CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL;
+CVC4_THREAD_LOCAL NodeManager* NodeManager::s_current = NULL;
 
 namespace {
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index fab5d4688..b1b0bc974 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -101,7 +101,7 @@ class NodeManager {
                              expr::NodeValueIDHashFunction,
                              expr::NodeValueIDEquality> NodeValueIDSet;
 
-  static CVC4_THREADLOCAL(NodeManager*) s_current;
+  static CVC4_THREAD_LOCAL NodeManager* s_current;
 
   Options* d_options;
   StatisticsRegistry* d_statisticsRegistry;
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 2a9202898..cad662d90 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -26,6 +26,7 @@
 // This must come before PORTFOLIO_BUILD.
 #include "cvc4autoconfig.h"
 
+#include "base/tls.h"
 #include "base/configuration.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
@@ -55,7 +56,7 @@ using namespace CVC4::main;
 namespace CVC4 {
   namespace main {
     /** Global options variable */
-    CVC4_THREADLOCAL(Options*) pOptions;
+    CVC4_THREAD_LOCAL Options* pOptions;
 
     /** Full argv[0] */
     const char *progPath;
diff --git a/src/main/main.h b/src/main/main.h
index dcb5c2a0a..8a5d0971e 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -17,8 +17,8 @@
 #include <exception>
 #include <string>
 
-#include "base/exception.h"
 #include "base/tls.h"
+#include "base/exception.h"
 #include "cvc4autoconfig.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
@@ -54,7 +54,7 @@ extern CVC4::TimerStat* pTotalTime;
 extern bool segvSpin;
 
 /** A pointer to the options in play */
-extern CVC4_THREADLOCAL(Options*) pOptions;
+extern CVC4_THREAD_LOCAL Options* pOptions;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw(Exception);
diff --git a/src/main/util.cpp b/src/main/util.cpp
index e08628848..110fc2c67 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -33,7 +33,6 @@
 #endif /* __WIN32__ */
 
 #include "base/exception.h"
-#include "base/tls.h"
 #include "cvc4autoconfig.h"
 #include "main/command_executor.h"
 #include "main/main.h"
diff --git a/src/options/options.h b/src/options/options.h
index 6b2bfedad..f93663095 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -29,8 +29,8 @@
 #include "base/tls.h"
 #include "options/argument_extender.h"
 #include "options/language.h"
-#include "options/printer_modes.h"
 #include "options/option_exception.h"
+#include "options/printer_modes.h"
 
 namespace CVC4 {
 
@@ -47,7 +47,7 @@ class CVC4_PUBLIC Options {
   options::OptionsHandler* d_handler;
 
   /** The current Options in effect */
-  static CVC4_THREADLOCAL(Options*) s_current;
+  static CVC4_THREAD_LOCAL Options* s_current;
 
   /** Listeners for options::forceLogicString being set. */
   ListenerCollection d_forceLogicListeners;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 54fbd3c81..7d71c267a 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -25,7 +25,6 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
-#include "base/tls.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index bc97e6028..a48b22625 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -48,10 +48,10 @@ extern int optreset;
 #include <sstream>
 #include <limits>
 
+#include "base/tls.h"
 #include "base/cvc4_assert.h"
 #include "base/exception.h"
 #include "base/output.h"
-#include "base/tls.h"
 #include "options/argument_extender.h"
 #include "options/argument_extender_implementation.h"
 #include "options/didyoumean.h"
@@ -75,7 +75,7 @@ using namespace CVC4::options;
 
 namespace CVC4 {
 
-CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
+CVC4_THREAD_LOCAL Options* Options::s_current = NULL;
 
 
 
@@ -532,10 +532,10 @@ namespace options {
 
 /** Set a given Options* as "current" just for a particular scope. */
 class OptionsGuard {
-  CVC4_THREADLOCAL_TYPE(Options*)* d_field;
+  Options** d_field;
   Options* d_old;
 public:
-  OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) :
+  OptionsGuard(Options** field, Options* opts) :
     d_field(field),
     d_old(*field) {
     *field = opts;
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 6c360cdc9..d5fb87dbc 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -17,6 +17,7 @@
 
 #include "smt/smt_engine_scope.h"
 
+#include "base/tls.h"
 #include "base/configuration_private.h"
 #include "base/cvc4_assert.h"
 #include "base/output.h"
@@ -27,7 +28,7 @@
 namespace CVC4 {
 namespace smt {
 
-CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
+CVC4_THREAD_LOCAL SmtEngine* s_smtEngine_current = NULL;
 
 SmtEngine* currentSmtEngine() {
   Assert(s_smtEngine_current != NULL);
diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h
index 8c02af82d..ffd05c83f 100644
--- a/src/smt_util/node_visitor.h
+++ b/src/smt_util/node_visitor.h
@@ -20,6 +20,7 @@
 
 #include <vector>
 
+#include "base/tls.h"
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -32,7 +33,7 @@ template<typename Visitor>
 class NodeVisitor {
 
   /** For re-entry checking */
-  static CVC4_THREADLOCAL(bool) s_inRun;
+  static CVC4_THREAD_LOCAL bool s_inRun;
 
   /**
    * Guard against NodeVisitor<> being re-entrant.
@@ -73,7 +74,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
+    GuardReentry<bool> guard(s_inRun);
 
     // Notify of a start
     visitor.start(node);
@@ -115,6 +116,6 @@ public:
 };/* class NodeVisitor<> */
 
 template <typename Visitor>
-CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false;
+CVC4_THREAD_LOCAL bool NodeVisitor<Visitor>::s_inRun = false;
 
 }/* CVC4 namespace */
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index a40db89a7..ccab94221 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -17,6 +17,7 @@
 #include "theory/arith/dual_simplex.h"
 
 #include "base/output.h"
+#include "base/tls.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
@@ -62,7 +63,7 @@ DualSimplexDecisionProcedure::Statistics::~Statistics(){
 Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   Assert(d_conflictVariables.empty());
 
-  static CVC4_THREADLOCAL(unsigned int) instance = 0;
+  static CVC4_THREAD_LOCAL unsigned int instance = 0;
   instance = instance + 1;
   d_pivots = 0;
 
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 59bb35293..db40f3580 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -17,6 +17,7 @@
 #include "theory/arith/fc_simplex.h"
 
 #include "base/output.h"
+#include "base/tls.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
@@ -91,7 +92,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static CVC4_THREADLOCAL(unsigned int) instance = 0;
+  static CVC4_THREAD_LOCAL unsigned int instance = 0;
   instance = instance + 1;
   static const bool verbose = false;
 
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index b2f7b08b5..60c7ed56f 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -19,6 +19,7 @@
 #include <algorithm>
 
 #include "base/output.h"
+#include "base/tls.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
@@ -103,7 +104,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static CVC4_THREADLOCAL(unsigned int) instance = 0;
+  static CVC4_THREAD_LOCAL unsigned int instance = 0;
   instance = instance + 1;
   static const bool verbose = false;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ab5a19858..a3e2d8ee4 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -24,6 +24,7 @@
 #include <vector>
 
 #include "base/output.h"
+#include "base/tls.h"
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
@@ -56,12 +57,12 @@
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/matrix.h"
 #include "theory/arith/matrix.h"
+#include "theory/arith/nonlinear_extension.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/theory_arith.h"
-#include "theory/arith/nonlinear_extension.h"
 #include "theory/ite_utilities.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/rewriter.h"
@@ -4389,7 +4390,7 @@ void TheoryArithPrivate::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
-  static CVC4_THREADLOCAL(unsigned) callCount = 0;
+  static CVC4_THREAD_LOCAL unsigned callCount = 0;
   if(Debug.isOn("arith::presolve")) {
     Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl;
     callCount = callCount + 1;
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 0c20c48a4..fe58f658d 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) {
 }
 
 #ifdef CVC4_ASSERTIONS
-static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
+static CVC4_THREAD_LOCAL std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
 #endif /* CVC4_ASSERTIONS */
 
 class RewriterInitializer {