Add --enable-simgrid-mc to selectively enable the model checker

configure.ac

@@ -198,8 +198,15 @@ if test x$enable_simgrid = xyes ; then
 			  CXXFLAGS="-std=c++11 $CXXFLAGS"
 			  NVCCFLAGS="-std=c++11 $NVCCFLAGS")
 	AC_LANG_POP([C++])
-	AC_PATH_PROG([SIMGRID_MC], [simgrid-mc])
+	AC_ARG_ENABLE(simgrid-mc, [AS_HELP_STRING([--enable-simgrid-mc],
+				[Enable using Model Checker of simgrid])],
+				enable_simgrid_mc=$enableval, enable_simgrid_mc=no)
+	if test x$enable_simgrid_mc = xyes ; then
+		AC_DEFINE(STARPU_SIMGRID_MC, [1], [Define this to enable Model Checker in simgrid execution])
+		AC_PATH_PROG([SIMGRID_MC], [simgrid-mc], [$simgrid_dir/bin:$PATH])
+	fi
 fi
+AM_CONDITIONAL(STARPU_SIMGRID_MC, test x$enable_simgrid_mc = xyes)
 AM_CONDITIONAL(STARPU_SIMGRID, test x$enable_simgrid = xyes)
 AC_SUBST(SIMGRID_CFLAGS)
 AC_SUBST(SIMGRID_LIBS)

doc/doxygen/chapters/510_configure_options.doxy

@@ -645,6 +645,14 @@ allows to specify the location to the SimGrid lib directory.
 Use the smpirun at <c>path</c>
 </dd>
 
+<dt>--enable-simgrid-mc</dt>
+<dd>
+\anchor enable-simgrid-mc
+\addindex __configure__--enable-simgrid-mc
+Enable the Model Checker in simulation of execution in simgrid, to allow
+exploring various execution paths.
+</dd>
+
 <dt>--enable-calibration-heuristic</dt>
 <dd>
 \anchor enable-calibration-heuristic

include/starpu_util.h

@@ -29,6 +29,10 @@
 #include <execinfo.h>
 #endif
 
+#ifdef STARPU_SIMGRID_MC
+#include <simgrid/modelchecker.h>
+#endif
+
 #ifdef __cplusplus
 extern "C"
 {
@@ -111,17 +115,23 @@ extern "C"
 #  define STARPU_DUMP_BACKTRACE() do { } while (0)
 #endif
 
+#ifdef STARPU_SIMGRID_MC
+#define STARPU_SIMGRID_ASSERT(x) MC_assert(!!(x))
+#else
+#define STARPU_SIMGRID_ASSERT(x)
+#endif
+
 #ifdef STARPU_NO_ASSERT
 #define STARPU_ASSERT(x)		do { if (0) { (void) (x); } } while(0)
 #define STARPU_ASSERT_ACCESSIBLE(x)	do { if (0) { (void) (x); } } while(0)
 #define STARPU_ASSERT_MSG(x, msg, ...)	do { if (0) { (void) (x); (void) msg; } } while(0)
 #else
 #  if defined(__CUDACC__) || defined(STARPU_HAVE_WINDOWS)
-#    define STARPU_ASSERT(x)		do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); *(int*)NULL = 0; } } while(0)
-#    define STARPU_ASSERT_MSG(x, msg, ...)	do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); fprintf(stderr, "\n[starpu][%s][assert failure] " msg "\n\n", __starpu_func__, ## __VA_ARGS__); *(int*)NULL = 0; }} while(0)
+#    define STARPU_ASSERT(x)		do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); STARPU_SIMGRID_ASSERT(x); *(int*)NULL = 0; } } while(0)
+#    define STARPU_ASSERT_MSG(x, msg, ...)	do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); fprintf(stderr, "\n[starpu][%s][assert failure] " msg "\n\n", __starpu_func__, ## __VA_ARGS__); STARPU_SIMGRID_ASSERT(x); *(int*)NULL = 0; }} while(0)
 #  else
-#    define STARPU_ASSERT(x)		do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); assert(x); } } while (0)
-#    define STARPU_ASSERT_MSG(x, msg, ...)	do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); fprintf(stderr, "\n[starpu][%s][assert failure] " msg "\n\n", __starpu_func__, ## __VA_ARGS__); assert(x); } } while(0)
+#    define STARPU_ASSERT(x)		do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); STARPU_SIMGRID_ASSERT(x); assert(x); } } while (0)
+#    define STARPU_ASSERT_MSG(x, msg, ...)	do { if (STARPU_UNLIKELY(!(x))) { STARPU_DUMP_BACKTRACE(); fprintf(stderr, "\n[starpu][%s][assert failure] " msg "\n\n", __starpu_func__, ## __VA_ARGS__); STARPU_SIMGRID_ASSERT(x); assert(x); } } while(0)
 
 #  endif
 #  define STARPU_ASSERT_ACCESSIBLE(ptr)	do { \

tests/Makefile.am

@@ -383,7 +383,13 @@ if STARPU_SIMGRID
 TESTS += $(MICROBENCHS:=.sh)
 endif
 
-if STARPU_SIMGRID
+TESTS += datawizard/locality.sh
+
+################################
+# Simgrid Model Checking tests #
+################################
+
+if STARPU_SIMGRID_MC
 model_checking_prio_list_LDADD = 
 model_checking_prio_list_LDFLAGS = 
 model_checking_prio_list_SOURCES = model-checking/prio_list.c ../src/common/rbtree.c
@@ -393,8 +399,6 @@ TESTS += model-checking/prio_list.sh
 endif
 endif
 
-TESTS += datawizard/locality.sh
-
 #######################
 # Source files        #
 #######################

tests/model-checking/prio_list.c

@@ -31,6 +31,8 @@
 #define N 2 /* number of threads */
 #define M 4 /* number of elements */
 
+// MC_ignore
+
 xbt_mutex_t mutex;