Prevent random number generation from diverging, by making threads always get the same values

tests/model-checking/Makefile

@@ -19,9 +19,12 @@ CFLAGS=-Wall -Wextra -g $(STARPU)/src/common/rbtree.c
 LDFLAGS=-lsimgrid
 
 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
+
+ifeq (1,1)
+MC_FLAGS+=--cfg=contexts/factory:ucontext
+MC_FLAGS+=--cfg=model-check/sparse-checkpoint:yes
+MC_FLAGS+=--cfg=model-check/visited:1000
+endif
 
 test: prio_list
 	simgrid-mc ./prio_list platform.xml MAIN $(MC_FLAGS)

tests/model-checking/prio_list.c

@@ -17,8 +17,10 @@
 #define _STARPU_MALLOC(p, s) do {p = malloc(s);} while (0)
 #define STARPU_ATTRIBUTE_UNUSED __attribute((__unused__))
 
+#define _GNU_SOURCE
 #include <unistd.h>
 #include <stdlib.h>
+#include <stdio.h>
 #include <limits.h>
 #include <common/list.h>
 #include <common/prio_list.h>
@@ -60,16 +62,22 @@ void check_list_prio(struct foo_prio_list *list)
 	}
 }
 
-int worker(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSED)
+int worker(int argc, char *argv[])
 {
 	unsigned i, n;
 	struct foo *elem;
+	struct drand48_data buffer;
+	long res;
+
+	srand48_r(atoi(argv[0]), &buffer);
 
 	for (i = 0; i < M; i++)
 	{
 		elem = malloc(sizeof(*elem));
-		elem->prio = lrand48()%10;
-		elem->back = lrand48()%2;
+		lrand48_r(&buffer, &res);
+		elem->prio = res%10;
+		lrand48_r(&buffer, &res);
+		elem->back = res%2;
 		xbt_mutex_acquire(mutex);
 		if (elem->back)
 			foo_prio_list_push_back(&mylist, elem);
@@ -81,7 +89,8 @@ int worker(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSE
 
 	for (i = 0; i < M; i++)
 	{
-		n = lrand48()%(M-i);
+		lrand48_r(&buffer, &res);
+		n = res%(M-i);
 
 		xbt_mutex_acquire(mutex);
 		for (elem  = foo_prio_list_begin(&mylist);
@@ -104,7 +113,14 @@ int master(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSE
 	foo_prio_list_init(&mylist);
 
 	for (i = 0; i < N; i++)
-		MSG_process_create("test", worker, NULL, MSG_host_self());
+	{
+		char *s;
+		asprintf(&s, "%d\n", i);
+		char **args = malloc(sizeof(char*)*2);
+		args[0] = s;
+		args[1] = NULL;
+		MSG_process_create_with_arguments("test", worker, NULL, MSG_host_self(), 1, args);
+	}
 
 	return 0;
 }
@@ -119,7 +135,6 @@ int main(int argc, char *argv[])
 	srand48(0);
 	MSG_init(&argc, argv);
 	xbt_cfg_set_int("contexts/stack-size", 128);
-	//xbt_cfg_set_boolean("model-check/sparse-checkpoint", "true");
 	MSG_create_environment(argv[1]);
 	MSG_process_create("master", master, NULL, MSG_get_host_by_name(argv[2]));
 	MSG_main();