Add a simgrid model-checking trivial test for now

tests/model-checking/Makefile

@@ -0,0 +1,10 @@
+STARPU=../../
+CPPFLAGS=-I$(STARPU)/src
+CFLAGS=-Wall -Wextra -g $(STARPU)/src/common/rbtree.c
+LDFLAGS=-lsimgrid
+
+test: prio_list
+	simgrid-mc ./prio_list platform.xml MAIN
+
+debug: prio_list
+	simgrid-mc ./prio_list platform.xml MAIN --log=mc_safety.thres:debug

tests/model-checking/platform.xml

@@ -0,0 +1,18 @@
+<?xml version='1.0'?>
+<!DOCTYPE platform SYSTEM 'http://simgrid.gforge.inria.fr/simgrid/simgrid.dtd'>
+ <platform version="4">
+ <config id="General">
+   <prop id="network/TCP-gamma" value="-1"></prop>
+   <prop id="network/latency-factor" value="1"></prop>
+   <prop id="network/bandwidth-factor" value="1"></prop>
+ </config>
+ <AS  id="AS0"  routing="Full">
+   <host id="MAIN" speed="1f"/>
+   <host id="CPU0" speed="2000000000f"/>
+   <host id="CPU1" speed="2000000000f"/>
+
+   <host id="RAM" speed="1f"/>
+
+   <link id="Host" bandwidth="0.000000Bps" latency="0.000000s"/>
+ </AS>
+ </platform>

tests/model-checking/prio_list.c

@@ -0,0 +1,122 @@
+#define _STARPU_MALLOC(p, s) do {p = malloc(s);} while (0)
+#define STARPU_ATTRIBUTE_UNUSED __attribute((__unused__))
+
+#include <unistd.h>
+#include <stdlib.h>
+#include <limits.h>
+#include <common/list.h>
+#include <common/prio_list.h>
+#include <simgrid/msg.h>
+#include <simgrid/modelchecker.h>
+#include <xbt/synchro.h>
+
+#define N 2
+#define M 2
+
+/* avoid diverging, for now */
+#define lrand48() 42
+
+xbt_mutex_t mutex;
+
+
+LIST_TYPE(foo,
+		unsigned prio;
+		unsigned back;	/* Push at back instead of front? */
+	 );
+PRIO_LIST_TYPE(foo, prio);
+
+struct foo_prio_list mylist;
+
+void check_list_prio(struct foo_prio_list *list)
+{
+	struct foo *cur;
+	unsigned lastprio = UINT_MAX;
+	unsigned back = 0;
+	for (cur  = foo_prio_list_begin(list);
+	     cur != foo_prio_list_end(list);
+	     cur  = foo_prio_list_next(list, cur))
+	{
+		if (cur->prio == lastprio)
+                        /* For same prio, back elements should never get before
+                         * front elements */
+			MC_assert(!(back && !cur->back));
+		else
+			MC_assert(lastprio > cur->prio);
+		lastprio = cur->prio;
+		back = cur->back;
+	}
+}
+
+int worker(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSED)
+{
+	unsigned i, n;
+	struct foo *elem;
+
+	for (i = 0; i < M; i++) {
+		elem = malloc(sizeof(*elem));
+		MSG_process_sleep(1);
+		elem->prio = lrand48()%10;
+		elem->back = lrand48()%2;
+		xbt_mutex_acquire(mutex);
+		if (elem->back)
+			foo_prio_list_push_back(&mylist, elem);
+		else
+			foo_prio_list_push_front(&mylist, elem);
+		check_list_prio(&mylist);
+		xbt_mutex_release(mutex);
+	}
+
+	for (i = 0; i < M; i++) {
+		n = lrand48()%(M-i);
+
+		xbt_mutex_acquire(mutex);
+		for (elem  = foo_prio_list_begin(&mylist);
+		     n--;
+		     elem  = foo_prio_list_next(&mylist, elem))
+			;
+		foo_prio_list_erase(&mylist, elem);
+		check_list_prio(&mylist);
+		xbt_mutex_release(mutex);
+	}
+
+	return 0;
+}
+
+int master(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSED)
+{
+	msg_process_t process[N];
+	unsigned i;
+
+	mutex = xbt_mutex_init();
+	foo_prio_list_init(&mylist);
+
+	for (i = 0; i < N; i++)
+	{
+		process[i] = MSG_process_create("test", worker, NULL, MSG_host_self());
+		MSG_process_ref(process[i]);
+	}
+	for (i = 0; i < N; i++)
+	{
+		MSG_process_join(process[i], 1000000);
+		MSG_process_unref(process[i]);
+	}
+
+	xbt_mutex_destroy(mutex);
+
+	return 0;
+}
+
+int main(int argc, char *argv[]) {
+	if (argc < 3) {
+		fprintf(stderr,"usage: %s platform.xml host\n", argv[0]);
+		exit(EXIT_FAILURE);
+	}
+	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();
+	return 0;
+}