Move model-checking rules to its own Makefile

This avoids having to empty LDADD etc. by hand.
Also remove independent build, it is not working any more anyway.

configure.ac

@@ -3624,6 +3624,7 @@ AC_OUTPUT([
 	examples/stencil/Makefile
 	tests/Makefile
 	tests/loader-cross.sh
+	tests/model-checking/Makefile
 	tests/model-checking/starpu-mc.sh
 	examples/loader-cross.sh
 	examples/stencil/loader-cross.sh

tests/Makefile.am

@@ -67,11 +67,7 @@ EXTRA_DIST =					\
 	datawizard/interfaces/tensor/tensor_opencl_kernel.cl \
 	perfmodels/opencl_memset_kernel.cl \
 	$(MICROBENCHS:=.sh) \
-	microbenchs/microbench.sh \
-	model-checking/platform.xml \
-	model-checking/prio_list.sh \
-	model-checking/barrier.sh \
-	model-checking/starpu-mc.sh.in
+	microbenchs/microbench.sh
 
 CLEANFILES = 					\
 	*.gcno *.gcda *.linkinfo core starpu_idle_microsec.log *.mod *.png *.output tasks.rec perfs.rec perfs2.rec fortran90/starpu_mod.f90 bandwidth-*.dat bandwidth.gp bandwidth.eps bandwidth.svg
@@ -459,19 +455,7 @@ endif
 ################################
 
 if STARPU_SIMGRID_MC
-model_checking_prio_list_LDADD = 
-model_checking_prio_list_LDFLAGS = 
-noinst_PROGRAMS += model-checking/prio_list
-if !STARPU_QUICK_CHECK
-SHELL_TESTS += model-checking/prio_list.sh
-endif
-
-model_checking_starpu_barrier_LDADD = 
-model_checking_starpu_barrier_LDFLAGS = 
-noinst_PROGRAMS += model-checking/starpu_barrier
-if !STARPU_QUICK_CHECK
-#SHELL_TESTS += model-checking/barrier.sh
-endif
+SUBDIRS += model-checking
 endif
 
 #######################

tests/model-checking/Makefile

@@ -13,25 +13,36 @@
 #
 # See the GNU Lesser General Public License in COPYING.LGPL for more details.
 #
-STARPU=../../
-CPPFLAGS=-I$(STARPU)/src -I$(STARPU)/include -I.
-CFLAGS+=-Wall -Wextra -g -DNOCONFIG
-LDFLAGS+=-lsimgrid -lm -Wl,-znorelro -Wl,-znoseparate-code
 
-MC_FLAGS=--cfg=model-check/reduction:none
+EXTRA_DIST =				\
+	platform.xml	\
+	prio_list.sh	\
+	barrier.sh	\
+	starpu-mc.sh.in
+
+AM_CPPFLAGS = -I$(top_builddir)/src -I$(top_srcdir)/src -I$(top_builddir)/include -I$(top_srcdir)/include $(SIMGRID_CFLAGS)
+AM_LDFLAGS  = -Wl,-znorelro -Wl,-znoseparate-code
+
+noinst_PROGRAMS = \
+		  prio_list \
+		  prio_list2 \
+		  starpu_barrier
 
-ifeq (1,0)
-MC_FLAGS+=--cfg=contexts/factory:ucontext
-MC_FLAGS+=--cfg=model-check/sparse-checkpoint:yes
-MC_FLAGS+=--cfg=model-check/visited:1000
+if !STARPU_QUICK_CHECK
+SHELL_TESTS = prio_list.sh
+#SHELL_TESTS += barrier.sh
 endif
 
+MC_FLAGS=--cfg=model-check/reduction:none
+
+#MC_FLAGS+=--cfg=contexts/factory:ucontext
+#MC_FLAGS+=--cfg=model-check/sparse-checkpoint:yes
+#MC_FLAGS+=--cfg=model-check/visited:1000
+
 # To record the failing trace
-ifeq (1,0)
-MC_FLAGS+=--cfg=model-check/record:1
-# And replay it without simgrid-mc
+#MC_FLAGS+=--cfg=model-check/record:1
+## And replay it without simgrid-mc
 #MC_FLAGS+=--cfg=model-check/reply:'1;3;4'
-endif
 
 # To see which simix calls are made
 #MC_FLAGS+=--log=simix_popping.thres:debug
@@ -47,8 +58,3 @@ test-barrier: starpu_barrier
 
 debug-barrier: starpu_barrier
 	simgrid-mc ./starpu_barrier platform.xml MAIN --log=mc_safety.thres:debug $(MC_FLAGS)
-
-all: prio_list prio_list2 starpu_barrier
-
-clean:
-	rm -f prio_list prio_list2 starpu_barrier

tests/model-checking/common/config.h

@@ -1,20 +0,0 @@
-/* StarPU --- Runtime system for heterogeneous multicore architectures.
- *
- * Copyright (C) 2017-2020  Université de Bordeaux, CNRS (LaBRI UMR 5800), Inria
- *
- * StarPU is free software; 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; either version 2.1 of the License, or (at
- * your option) any later version.
- *
- * StarPU 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 in COPYING.LGPL for more details.
- */
-#define STARPU_SIMGRID
-#define STARPU_MAXIMPLEMENTATIONS 4
-#define STARPU_NMAXBUFS 8
-#define STARPU_MAXNODES 2
-#define STARPU_NMAXWORKERS 16

tests/model-checking/starpu_config.h

@@ -1,55 +0,0 @@
-/* StarPU --- Runtime system for heterogeneous multicore architectures.
- *
- * Copyright (C) 2017-2020  Université de Bordeaux, CNRS (LaBRI UMR 5800), Inria
- *
- * StarPU is free software; 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; either version 2.1 of the License, or (at
- * your option) any later version.
- *
- * StarPU 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 in COPYING.LGPL for more details.
- */
-#define STARPU_SIMGRID
-#define STARPU_MAXIMPLEMENTATIONS 4
-#define STARPU_NMAXBUFS 8
-#define STARPU_MAXNODES 2
-#define STARPU_NMAXWORKERS 16
-
-#ifndef _MSC_VER
-#include <stdint.h>
-#else
-#include <windows.h>
-typedef unsigned char uint8_t;
-typedef unsigned short uint16_t;
-typedef unsigned int uint32_t;
-typedef unsigned long long uint64_t;
-typedef UINT_PTR uintptr_t;
-typedef char int8_t;
-typedef short int16_t;
-typedef int int32_t;
-typedef long long int64_t;
-typedef INT_PTR intptr_t;
-#endif
-
-#ifdef _MSC_VER
-typedef long starpu_ssize_t;
-#define __starpu_func__ __FUNCTION__
-#else
-#  include <sys/types.h>
-typedef ssize_t starpu_ssize_t;
-#define __starpu_func__ __func__
-#endif
-
-#if defined(c_plusplus) || defined(__cplusplus)
-/* inline is part of C++ */
-#  define __starpu_inline inline
-#elif defined(_MSC_VER) || defined(__HP_cc)
-#  define __starpu_inline __inline
-#else
-#  define __starpu_inline __inline__
-#endif
-