use S4U functions in mc tests

tests/model-checking/Makefile

@@ -16,7 +16,7 @@
 STARPU=../../
 CPPFLAGS=-I$(STARPU)/src -I$(STARPU)/include -I.
 CFLAGS+=-Wall -Wextra -g -DNOCONFIG
-LDFLAGS+=-lsimgrid
+LDFLAGS+=-lsimgrid -lm
 
 MC_FLAGS=--cfg=model-check/reduction:none
 

tests/model-checking/prio_list.c

@@ -26,6 +26,9 @@
 // Assuming recent simgrid
 #define STARPU_HAVE_SIMGRID_MSG_H
 #define STARPU_HAVE_XBT_SYNCHRO_H
+#define STARPU_HAVE_SIMGRID_MUTEX_H
+#define HAVE_SIMGRID_GET_CLOCK
+#define HAVE_SG_ACTOR_SLEEP_FOR
 #define HAVE_SG_CFG_SET_INT
 #endif
 #include <unistd.h>
@@ -63,7 +66,15 @@
 
 // MC_ignore
 
+#ifdef STARPU_HAVE_SIMGRID_MUTEX_H
+sg_mutex_t mutex[NLISTS];
+#define mutex_lock(l) sg_mutex_lock(l)
+#define mutex_unlock(l) sg_mutex_unlock(l)
+#else
 xbt_mutex_t mutex[NLISTS];
+#define mutex_lock(l) xbt_mutex_acquire(l)
+#define mutex_unlock(l) xbt_mutex_release(l)
+#endif
 
 
 LIST_TYPE(foo,
@@ -115,13 +126,13 @@ int worker(int argc, char *argv[])
 			elem->prio = res%10;
 			lrand48_r(&buffer, &res);
 			elem->back = res%2;
-			xbt_mutex_acquire(mutex[l]);
+			mutex_lock(mutex[l]);
 			if (elem->back)
 				foo_prio_list_push_back(&mylist[l], elem);
 			else
 				foo_prio_list_push_front(&mylist[l], elem);
 			check_list_prio(&mylist[l]);
-			xbt_mutex_release(mutex[l]);
+			mutex_unlock(mutex[l]);
 		}
 
 		for (i = 0; i < NELEMENTS; i++)
@@ -129,18 +140,22 @@ int worker(int argc, char *argv[])
 			lrand48_r(&buffer, &res);
 			n = res%(NELEMENTS-i);
 
-			xbt_mutex_acquire(mutex[l]);
+			mutex_lock(mutex[l]);
 			for (elem  = foo_prio_list_begin(&mylist[l]);
 			     n--;
 			     elem  = foo_prio_list_next(&mylist[l], elem))
 				;
 			foo_prio_list_erase(&mylist[l], elem);
 			check_list_prio(&mylist[l]);
-			xbt_mutex_release(mutex[l]);
+			mutex_unlock(mutex[l]);
 		}
 
 		/* horrible way to wait for list getting empty */
+#ifdef HAVE_SG_ACTOR_SLEEP_FOR
+		sg_actor_sleep_for(1000);
+#else
 		MSG_process_sleep(1000);
+#endif
 	}
 
 	return 0;
@@ -152,7 +167,11 @@ int master(int argc, char *argv[])
 
 	for (l = 0; l < NLISTS; l++)
 	{
+#ifdef STARPU_HAVE_SIMGRID_MUTEX_H
+		mutex[l] = sg_mutex_init();
+#else
 		mutex[l] = xbt_mutex_init();
+#endif
 		foo_prio_list_init(&mylist[l]);
 	}
 

tests/model-checking/starpu_barrier.c

@@ -42,6 +42,8 @@
 // Assuming recent simgrid
 #define STARPU_HAVE_SIMGRID_MSG_H
 #define STARPU_HAVE_XBT_SYNCHRO_H
+#define HAVE_SIMGRID_GET_CLOCK
+#define HAVE_SG_ACTOR_SLEEP_FOR
 #define HAVE_SG_CFG_SET_INT
 #endif
 #include <unistd.h>
@@ -70,7 +72,11 @@ _starpu_simgrid_thread_start(int argc, char *argv[])
 
 static void _starpu_clock_gettime(struct timespec *ts)
 {
+#ifdef HAVE_SIMGRID_GET_CLOCK
+	double now = simgrid_get_clock();
+#else
 	double now = MSG_get_clock();
+#endif
 	ts->tv_sec = floor(now);
 	ts->tv_nsec = floor((now - ts->tv_sec) * 1000000000);
 }