diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index d12aa009d2530f4ca3015a5037fa76cf1e5c274b..afc89c322e8e373f3408e907dc33065c8f1748bd 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -26,6 +26,7 @@ share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROP
share/e-acsl/internals/e_acsl_alias.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_bits.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_bits.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+share/e-acsl/internals/e_acsl_concurrency.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_config.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_debug.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h
new file mode 100644
index 0000000000000000000000000000000000000000..4961dd4466d715e5b50fd8c8ddbb843d56773d44
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h
@@ -0,0 +1,158 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It 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 Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+/*! ***********************************************************************
+ * \file
+ * \brief E-ACSL concurrency utility macros and functions.
+ **************************************************************************/
+
+#ifndef E_ACSL_CONCURRENCY
+#define E_ACSL_CONCURRENCY
+
+#ifdef E_ACSL_CONCURRENCY_PTHREAD
+# include <pthread.h>
+# include <string.h>
+
+# include "e_acsl_debug.h"
+# include "e_acsl_rtl_error.h"
+
+/************************************************************************/
+/*** Run once function {{{ ***/
+/************************************************************************/
+
+# ifdef E_ACSL_DEBUG
+/*! \brief Buffer to hold a thread-specific error message.
+
+ This buffer and `rtl_strerror_t()` are used instead of directly
+ `rtl_strerror()` because since `E_ACSL_RUN_ONCE` is called when processing
+ logging functions, the message returned by `rtl_strerror()` in a
+ `DVASSERT()` call could be overwritten. */
+static __thread char __e_acsl_run_once_error_buffer[255];
+# endif
+
+/*! \brief The first call to `E_ACSL_RUN_ONCE` will call the initialization
+ function `init_fct()` without arguments. Any subsequent call to
+ `E_ACSL_RUN_ONCE` will not call `init_fct()`. After calling
+ `E_ACSL_RUN_ONCE`, the function `init_fct()` has been called. */
+# define E_ACSL_RUN_ONCE(init_fct) \
+ do { \
+ static pthread_once_t already_run = PTHREAD_ONCE_INIT; \
+ int result = pthread_once(&already_run, init_fct); \
+ DVASSERT(result == 0, \
+ "Unable to initialize with function '" #init_fct "()': %s\n", \
+ rtl_strerror_r(errno, __e_acsl_run_once_error_buffer, \
+ sizeof(__e_acsl_run_once_error_buffer))); \
+ } while (0)
+
+/*! \brief The first call to `E_ACSL_RUN_ONCE_WITH_ARGS` will call the
+ initialization function `init_fct()` with arguments `args...`. Any
+ subsequent call to `E_ACSL_RUN_ONCE_WITH_ARGS` will not call `init_fct()`.
+ After calling `E_ACSL_RUN_ONCE_WITH_ARGS`, the function `init_fct()` has
+ been called. */
+# define E_ACSL_RUN_ONCE_WITH_ARGS(init_fct, args...) \
+ do { \
+ static int already_run = 0; \
+ static pthread_rwlock_t rwlock = PTHREAD_RWLOCK_INITIALIZER; \
+ pthread_rwlock_rdlock(&rwlock); \
+ if (!already_run) { \
+ pthread_rwlock_unlock(&rwlock); \
+ pthread_rwlock_wrlock(&rwlock); \
+ if (!already_run) { \
+ init_fct(args); \
+ already_run = 1; \
+ } \
+ } \
+ pthread_rwlock_unlock(&rwlock); \
+ } while (0)
+
+/* }}} */
+
+/************************************************************************/
+/*** Mutex {{{ ***/
+/************************************************************************/
+
+/*! \brief Declare a static mutex variable named `mutex` with the initialization
+ `init`. */
+# define E_ACSL_MUTEX_DECL_INIT(mutex, init) \
+ static pthread_mutex_t mutex = init
+
+/*! \brief Lock the given mutex */
+# define E_ACSL_MUTEX_LOCK(mutex) pthread_mutex_lock(&(mutex))
+
+/*! \brief Unlock the given mutex */
+# define E_ACSL_MUTEX_UNLOCK(mutex) pthread_mutex_unlock(&(mutex))
+
+/* }}} */
+
+/************************************************************************/
+/*** Read-write lock {{{ ***/
+/************************************************************************/
+
+/*! \brief Declare a read-write lock variable named `rwlock`. */
+# define E_ACSL_RWLOCK_DECL(rwlock) pthread_rwlock_t rwlock
+
+/*! \brief Initialize the given read-write lock with the given attributes. */
+# define E_ACSL_RWINIT(rwlock, attrs) pthread_rwlock_init(&(rwlock), attrs)
+
+/*! \brief Destroy the given read-write lock. */
+# define E_ACSL_RWDESTROY(rwlock) pthread_rwlock_destroy(&(rwlock))
+
+/*! \brief Apply a read lock to the given read-write lock. */
+# define E_ACSL_RLOCK(rwlock) \
+ pthread_rwlock_rdlock((pthread_rwlock_t *)&(rwlock))
+
+/*! \brief Apply a write lock to the given read-write lock. */
+# define E_ACSL_WLOCK(rwlock) pthread_rwlock_wrlock(&(rwlock))
+
+/*! \brief Unlock the given read-write lock. */
+# define E_ACSL_RWUNLOCK(rwlock) \
+ pthread_rwlock_unlock((pthread_rwlock_t *)&(rwlock))
+
+/* }}} */
+
+#else
+
+# define E_ACSL_RUN_ONCE_WITH_ARGS(init_fct, args...) \
+ do { \
+ static int already_run = 0; \
+ if (!already_run) { \
+ init_fct(args); \
+ already_run = 1; \
+ } \
+ } while (0)
+
+# define E_ACSL_RUN_ONCE(init_fct) E_ACSL_RUN_ONCE_WITH_ARGS(init_fct)
+
+# define E_ACSL_MUTEX_DECL_INIT(mutex, init)
+# define E_ACSL_MUTEX_LOCK(mutex)
+# define E_ACSL_MUTEX_UNLOCK(mutex)
+
+# define E_ACSL_RWLOCK_DECL(rwlock)
+# define E_ACSL_RWINIT(rwlock, attrs)
+# define E_ACSL_RWDESTROY(rwlock)
+# define E_ACSL_RLOCK(rwlock)
+# define E_ACSL_WLOCK(rwlock)
+# define E_ACSL_RWUNLOCK(rwlock)
+
+#endif
+
+#endif // E_ACSL_CONCURRENCY