[eacsl] Use locks in dlmalloc to support multi-threaded environment

We use spin locks so as to not require Pthreads.

src/plugins/e-acsl/Makefile.in

@@ -162,7 +162,7 @@ VERSION_FILE=$(FRAMAC_ROOT_SRCDIR)/VERSION
 
 EACSL_VERSION:=$(shell sed -e 's/\\(.*\\)/\\1/' $(VERSION_FILE))
 
-$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_FILE)
+$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile $(VERSION_FILE)
 	$(PRINT_MAKING) $@
 	$(RM) $@
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
@@ -272,9 +272,11 @@ EACSL_DLMALLOC_FLAGS = \
   -DMSPACES=1 \
   -DONLY_MSPACES \
   -DMALLOC_ALIGNMENT=32 \
-  -DMSPACE_PREFIX="__e_acsl_"
+  -DMSPACE_PREFIX="__e_acsl_" \
+  -DUSE_LOCKS=1 \
+  -DUSE_SPIN_LOCKS=1
 
-$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC)
+$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC) $(EACSL_PLUGIN_DIR)/Makefile
 	$(MKDIR) $(EACSL_LIBDIR)
 	echo 'CC           $<'
 	$(CC) $< -c -O2 -g3 -o$(EACSL_DLMALLOC_OBJ) $(EACSL_DLMALLOC_FLAGS)

src/plugins/e-acsl/scripts/e-acsl-gcc.sh

@@ -925,6 +925,8 @@ if [ "$OPTION_DLMALLOC_FROM_SOURCES" = "1" -o \
     -DONLY_MSPACES \
     -DMALLOC_ALIGNMENT=32 \
     -DMSPACE_PREFIX=__e_acsl_ \
+    -DUSE_LOCKS=1 \
+    -DUSE_SPIN_LOCKS=1 \
     $OPTION_DLMALLOC_COMPILE_FLAGS
   "
 

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c

@@ -22,6 +22,10 @@
 
 #include "e_acsl_malloc.h"
 
+#define eacsl_create_mspace export_alias(create_mspace)
+
+extern mspace eacsl_create_mspace(size_t, int);
+
 struct memory_spaces mem_spaces = {
     .rtl_mspace = NULL,
     .heap_mspace = NULL,
@@ -32,12 +36,16 @@ struct memory_spaces mem_spaces = {
     .heap_mspace_least = 0,
 };
 
+mspace eacsl_create_locked_mspace(size_t size) {
+  return eacsl_create_mspace(size, 1);
+}
+
 /* \brief Create two memory spaces, one for RTL and the other for application
    memory. This function *SHOULD* be called before any allocations are made
    otherwise execution fails */
 void eacsl_make_memory_spaces(size_t rtl_size, size_t heap_size) {
-  mem_spaces.rtl_mspace = eacsl_create_mspace(rtl_size, 0);
-  mem_spaces.heap_mspace = eacsl_create_mspace(heap_size, 0);
+  mem_spaces.rtl_mspace = eacsl_create_locked_mspace(rtl_size);
+  mem_spaces.heap_mspace = eacsl_create_locked_mspace(heap_size);
   /* Do not use `eacsl_mspace_least_addr` here, as it returns the address of the
      mspace header. */
   mem_spaces.rtl_start =

src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h

@@ -28,7 +28,7 @@
  * is split into two mspaces (memory spaces). Memory allocation itself is
  * delegated to a slightly customised version of dlmalloc shipped with the
  * RTL. The overall pattern is as follows:
- *    mspace space = eacsl_create_mspace(capacity, locks);
+ *    mspace space = eacsl_create_locked_mspace(capacity);
  *    char *p = eacsl_mspace_malloc(space, size);
  **************************************************************************/
 
@@ -70,7 +70,7 @@ void eacsl_destroy_memory_spaces();
 /*** Mspace allocators (from dlmalloc) {{{ ***/
 /************************************************************************/
 
-#define eacsl_create_mspace         export_alias(create_mspace)
+#define eacsl_create_locked_mspace  export_alias(create_locked_mspace)
 #define eacsl_destroy_mspace        export_alias(destroy_mspace)
 #define eacsl_mspace_least_addr     export_alias(mspace_least_addr)
 #define eacsl_mspace_malloc         export_alias(mspace_malloc)
@@ -93,7 +93,7 @@ struct memory_spaces {
 };
 extern struct memory_spaces mem_spaces;
 
-extern mspace eacsl_create_mspace(size_t, int);
+/* Original functions from dlmalloc */
 extern size_t eacsl_destroy_mspace(mspace);
 extern void *eacsl_mspace_malloc(mspace, size_t);
 extern void eacsl_mspace_free(mspace, void *);
@@ -103,6 +103,10 @@ extern void *eacsl_mspace_aligned_alloc(mspace, size_t, size_t);
 extern int eacsl_mspace_posix_memalign(mspace, void **, size_t, size_t);
 extern void *eacsl_mspace_least_addr(mspace);
 
+/*! \brief Wrapper around `eacsl_create_mspace` to always create a thread-safe
+ *  mspace. */
+mspace eacsl_create_locked_mspace(size_t size);
+
 /* }}} */
 
 /************************************************************************/

src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c

@@ -675,7 +675,7 @@ void set_shadow_segment(memory_segment *seg, memory_segment *parent,
   seg->name = name;
   seg->shadow_ratio = ratio;
   seg->size = parent->size / seg->shadow_ratio;
-  seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
+  seg->mspace = eacsl_create_locked_mspace(seg->size + SHADOW_SEGMENT_PADDING);
   seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace, 1);
   seg->end = seg->start + seg->size - 1;
   seg->shadow_offset = parent->start - seg->start;