Ver código fonte

Add barrier modelchecker test

Samuel Thibault 8 anos atrás
pai
commit
0c4fcd28fc

+ 1 - 0
configure.ac

@@ -3133,6 +3133,7 @@ AC_CONFIG_COMMANDS([executable-scripts], [
   test -e tests/datawizard/locality.sh || ln -sf $ac_abs_top_srcdir/tests/datawizard/locality.sh tests/datawizard/
   mkdir -p tests/model-checking
   test -e tests/model-checking/prio_list.sh || ln -sf $ac_abs_top_srcdir/tests/model-checking/prio_list.sh tests/model-checking/
+  test -e tests/model-checking/barrier.sh || ln -sf $ac_abs_top_srcdir/tests/model-checking/barrier.sh tests/model-checking/
   mkdir -p examples/heat
   test -e examples/heat/heat.sh || ln -sf $ac_abs_top_srcdir/examples/heat/heat.sh examples/heat/
   mkdir -p examples/lu

+ 7 - 1
tests/Makefile.am

@@ -396,11 +396,17 @@ TESTS += datawizard/locality.sh
 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
 noinst_PROGRAMS += model-checking/prio_list
 if !STARPU_QUICK_CHECK
 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
+#TESTS += model-checking/barrier.sh
+endif
 endif
 
 #######################

+ 10 - 4
tests/model-checking/Makefile

@@ -14,8 +14,8 @@
 # See the GNU Lesser General Public License in COPYING.LGPL for more details.
 
 STARPU=../../
-CPPFLAGS=-I$(STARPU)/src
-CFLAGS=-Wall -Wextra -g $(STARPU)/src/common/rbtree.c -DNOCONFIG
+CPPFLAGS=-I$(STARPU)/src -I$(STARPU)/include -I.
+CFLAGS=-Wall -Wextra -g -DNOCONFIG
 LDFLAGS=-lsimgrid
 
 MC_FLAGS=--cfg=model-check/reduction:none
@@ -42,7 +42,13 @@ test: prio_list
 debug: prio_list
 	simgrid-mc ./prio_list platform.xml MAIN --log=mc_safety.thres:debug $(MC_FLAGS)
 
-all: prio_list prio_list2
+test-barrier: starpu_barrier
+	simgrid-mc ./starpu_barrier platform.xml MAIN $(MC_FLAGS)
+
+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
+	rm -f prio_list starpu_barrier

+ 19 - 0
tests/model-checking/barrier.sh

@@ -0,0 +1,19 @@
+#!/bin/bash -x
+#
+# StarPU --- Runtime system for heterogeneous multicore architectures.
+#
+# Copyright (C) 2017  Université de Bordeaux
+#
+# 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.
+
+source $(dirname $0)/starpu-mc.sh
+test starpu_barrier

+ 5 - 0
tests/model-checking/common/config.h

@@ -0,0 +1,5 @@
+#define STARPU_SIMGRID
+#define STARPU_MAXIMPLEMENTATIONS 4
+#define STARPU_NMAXBUFS 8
+#define STARPU_MAXNODES 2
+#define STARPU_NMAXWORKERS 16

+ 2 - 0
tests/model-checking/prio_list.c

@@ -43,6 +43,8 @@
 #include <xbt/synchro_core.h>
 #endif
 
+#include <common/rbtree.c>
+
 #ifndef NLISTS
 #define NLISTS 1
 #endif

+ 128 - 0
tests/model-checking/starpu_barrier.c

@@ -0,0 +1,128 @@
+/* StarPU --- Runtime system for heterogeneous multicore architectures.
+ *
+ * Copyright (C) 2017  Université de Bordeaux
+ *
+ * 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 __COMMON_UTILS_H__
+#define _STARPU_MALLOC(p, s) do {p = malloc(s);} while (0)
+#define _STARPU_CALLOC(p, n, s) do {p = calloc(n, s);} while (0)
+#define _STARPU_REALLOC(p, s) do {p = realloc(p, s);} while (0)
+//#define STARPU_ATTRIBUTE_UNUSED __attribute((__unused__))
+
+#define STARPU_DEBUG_PREFIX "[starpu]"
+#ifdef STARPU_VERBOSE
+#  define _STARPU_DEBUG(fmt, ...) do { if (!_starpu_silent) {fprintf(stderr, STARPU_DEBUG_PREFIX"[%s] " fmt ,__starpu_func__ ,## __VA_ARGS__); fflush(stderr); }} while(0)
+#else
+#  define _STARPU_DEBUG(fmt, ...) do { } while (0)
+#endif
+
+#define STARPU_UYIELD() ((void)0)
+
+#ifndef NOCONFIG
+#include <config.h>
+#else
+#define _GNU_SOURCE
+// Assuming recent simgrid
+#define STARPU_HAVE_SIMGRID_MSG_H
+#define STARPU_HAVE_XBT_SYNCHRO_H
+#endif
+#include <unistd.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <limits.h>
+#include <common/barrier.h>
+#ifdef STARPU_HAVE_SIMGRID_MSG_H
+#include <simgrid/msg.h>
+#else
+#include <msg/msg.h>
+#endif
+#include <simgrid/modelchecker.h>
+#ifdef STARPU_HAVE_XBT_SYNCHRO_H
+#include <xbt/synchro.h>
+#else
+#include <xbt/synchro_core.h>
+#endif
+
+int
+_starpu_simgrid_thread_start(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSED)
+{
+	return 0;
+}
+
+#include <common/barrier.c>
+#include <common/thread.c>
+
+#ifndef NTHREADS
+#define NTHREADS 2
+#endif
+
+#ifndef NITERS
+#define NITERS 1
+#endif
+
+struct _starpu_barrier barrier;
+
+int worker(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSED)
+{
+	unsigned iter;
+
+	for (iter = 0; iter < NITERS; iter++)
+	{
+		MC_assert(barrier.count <= NTHREADS);
+		_starpu_barrier_wait(&barrier);
+	}
+
+	return 0;
+}
+
+int master(int argc STARPU_ATTRIBUTE_UNUSED, char *argv[] STARPU_ATTRIBUTE_UNUSED)
+{
+	unsigned i;
+
+	_starpu_barrier_init(&barrier, NTHREADS);
+
+	for (i = 0; i < NTHREADS; i++)
+	{
+		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;
+}
+
+#undef main
+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);
+#if SIMGRID_VERSION_MAJOR < 3 || (SIMGRID_VERSION_MAJOR == 3 && SIMGRID_VERSION_MINOR < 13)
+	extern xbt_cfg_t _sg_cfg_set;
+	xbt_cfg_set_int(_sg_cfg_set, "contexts/stack-size", 128);
+#else
+	xbt_cfg_set_int("contexts/stack-size", 128);
+#endif
+	MSG_create_environment(argv[1]);
+	MSG_process_create("master", master, NULL, MSG_get_host_by_name(argv[2]));
+	MSG_main();
+	return 0;
+}

+ 40 - 0
tests/model-checking/starpu_config.h

@@ -0,0 +1,40 @@
+#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
+