From b24c14fba1046bbf5577d5b0ab1fe47b2af69a0d Mon Sep 17 00:00:00 2001 From: mquinson Date: Wed, 5 May 2010 23:17:06 +0000 Subject: [PATCH] Some MSG examples mainly useful to test the model-checker git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@7706 48e7efb5-ca39-0410-a469-dd3cf9ba447f --- buildtools/Cmake/prog_test/prog_va_copy.c | 60 +++++++--------- buildtools/Cmake/src/CMakeMakeExeLib.txt | 1 + examples/msg/Makefile.am | 18 ++++- examples/msg/mc/CMakeLists.txt | 11 +++ examples/msg/mc/bugged1.c | 55 +++++++++++++++ examples/msg/mc/bugged2.c | 58 +++++++++++++++ examples/msg/mc/centralized_mutex.c | 86 +++++++++++++++++++++++ examples/msg/mc/deploy_bugged1.xml | 16 +++++ examples/msg/mc/deploy_bugged2.xml | 13 ++++ examples/msg/mc/deploy_mutex.xml | 39 ++++++++++ examples/msg/mc/platform.xml | 18 +++++ include/mc/modelchecker.h | 3 + 12 files changed, 344 insertions(+), 34 deletions(-) create mode 100644 examples/msg/mc/CMakeLists.txt create mode 100644 examples/msg/mc/bugged1.c create mode 100644 examples/msg/mc/bugged2.c create mode 100644 examples/msg/mc/centralized_mutex.c create mode 100644 examples/msg/mc/deploy_bugged1.xml create mode 100644 examples/msg/mc/deploy_bugged2.xml create mode 100644 examples/msg/mc/deploy_mutex.xml create mode 100644 examples/msg/mc/platform.xml create mode 100644 include/mc/modelchecker.h diff --git a/buildtools/Cmake/prog_test/prog_va_copy.c b/buildtools/Cmake/prog_test/prog_va_copy.c index 82800ebf3b..d0797ae051 100644 --- a/buildtools/Cmake/prog_test/prog_va_copy.c +++ b/buildtools/Cmake/prog_test/prog_va_copy.c @@ -1,34 +1,28 @@ -/* Copyright (c) 2010. The SimGrid Team. - * All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - #include -#include -#include -#define DO_VA_COPY(d,s) memcpy((void *)(d), (void *)(s)), sizeof(*(s)) -void test(char *str, ...) -{ - va_list ap, ap2; - int i; - va_start(ap, str); - DO_VA_COPY(ap2, ap); - for (i = 1; i <= 9; i++) { - int k = (int)va_arg(ap, int); - if (k != i) - abort(); - } - DO_VA_COPY(ap, ap2); - for (i = 1; i <= 9; i++) { - int k = (int)va_arg(ap, int); - if (k != i) - abort(); - } - va_end(ap); -} -int main(int argc, char *argv[]) -{ - test(test, 1, 2, 3, 4, 5, 6, 7, 8, 9); - exit(0); -} + #include + #include + #define DO_VA_COPY(d,s) memcpy((void *)(d), (void *)(s)), sizeof(*(s)) + void test(char *str, ...) + { + va_list ap, ap2; + int i; + va_start(ap, str); + DO_VA_COPY(ap2, ap); + for (i = 1; i <= 9; i++) { + int k = (int)va_arg(ap, int); + if (k != i) + abort(); + } + DO_VA_COPY(ap, ap2); + for (i = 1; i <= 9; i++) { + int k = (int)va_arg(ap, int); + if (k != i) + abort(); + } + va_end(ap); + } + int main(int argc, char *argv[]) + { + test(test, 1, 2, 3, 4, 5, 6, 7, 8, 9); + exit(0); + } diff --git a/buildtools/Cmake/src/CMakeMakeExeLib.txt b/buildtools/Cmake/src/CMakeMakeExeLib.txt index 49870b3e95..7f58ea6bd8 100644 --- a/buildtools/Cmake/src/CMakeMakeExeLib.txt +++ b/buildtools/Cmake/src/CMakeMakeExeLib.txt @@ -125,6 +125,7 @@ add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/priority) add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/masterslave) add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/trace) add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/tracing) +add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/mc) if(HAVE_GTNETS) add_definitions("-lgtnets -L${gtnets_path}/lib -I${gtnets_path}/include/gtnets") add_subdirectory(${PROJECT_DIRECTORY}/examples/msg/gtnets) diff --git a/examples/msg/Makefile.am b/examples/msg/Makefile.am index 6e1382c76e..aae1c9eac5 100644 --- a/examples/msg/Makefile.am +++ b/examples/msg/Makefile.am @@ -99,7 +99,10 @@ noinst_PROGRAMS = sendrecv/sendrecv \ priority/priority \ properties/msg_prop \ actions/actions \ - trace/test_trace_integration + trace/test_trace_integration \ + mc/centralized \ + mc/bugged1 \ + mc/bugged2 if HAVE_GTNETS noinst_PROGRAMS += gtnets/gtnets @@ -158,6 +161,19 @@ masterslave_masterslave_bypass_LDADD = $(top_builddir)/src/libsimgrid.la trace_test_trace_integration_SOURCES = trace/test_trace_integration.c trace_test_trace_integration_LDADD = $(top_builddir)/src/libsimgrid.la +# Model-checking examples +mc_centralized_SOURCES = mc/centralized_mutex.c +mc_centralized_LDADD = $(top_builddir)/src/libsimgrid.la + +# bugged example 1 +mc_bugged1_SOURCES = mc/bugged1.c +mc_bugged1_LDADD = $(top_builddir)/src/libsimgrid.la + +# bugged example 2 +mc_bugged2_SOURCES = mc/bugged2.c +mc_bugged2_LDADD = $(top_builddir)/src/libsimgrid.la + + # verify if the GTNETS feature is working if HAVE_GTNETS gtnets_gtnets_SOURCES = gtnets/gtnets.c diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt new file mode 100644 index 0000000000..59bbe93b7a --- /dev/null +++ b/examples/msg/mc/CMakeLists.txt @@ -0,0 +1,11 @@ +cmake_minimum_required(VERSION 2.6) + +set(EXECUTABLE_OUTPUT_PATH "${PROJECT_DIRECTORY}/examples/msg/actions/") + +add_executable(centralized centralized_mutex.c) +add_executable(bugged1 bugged1.c) +add_executable(bugged2 bugged2.c) + +target_link_libraries(centralized simgrid m -fprofile-arcs) +target_link_libraries(bugged1 simgrid m -fprofile-arcs) +target_link_libraries(bugged2 simgrid m -fprofile-arcs) diff --git a/examples/msg/mc/bugged1.c b/examples/msg/mc/bugged1.c new file mode 100644 index 0000000000..ce8a687b9c --- /dev/null +++ b/examples/msg/mc/bugged1.c @@ -0,0 +1,55 @@ +#include +#include +#define N 3 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example,"this example"); + +int server(int argc,char *argv[]); +int client(int argc,char *argv[]); + +int server(int argc,char *argv[]) { + m_task_t task = NULL; + int count = 0; + while(count < N){ + if(task){ + MSG_task_destroy(task); + task = NULL; + } + MSG_task_receive(&task,"mymailbox"); + count++; + } + MC_assert(atoi(MSG_task_get_name(task)) == 3); + + INFO0("OK"); + return 0; +} + +int client(int argc,char *argv[]) { + + m_task_t task = MSG_task_create(argv[1], 0/*comp cost*/, 10000/*comm size*/, NULL /*arbitrary data*/); + + MSG_task_send(task,"mymailbox"); + + INFO0("Sent!"); + return 0; +} + +int main(int argc,char*argv[]) { + + MSG_global_init(&argc,argv); + + MSG_create_environment("platform.xml"); + + MSG_function_register("server", server); + + MSG_function_register("client", client); + + MSG_launch_application("deploy.xml"); + + MSG_main(); + + return 0; + +} + + diff --git a/examples/msg/mc/bugged2.c b/examples/msg/mc/bugged2.c new file mode 100644 index 0000000000..55574ae584 --- /dev/null +++ b/examples/msg/mc/bugged2.c @@ -0,0 +1,58 @@ +#include +#include +#define N 3 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example,"this example"); + +int server(int argc,char *argv[]); +int client(int argc,char *argv[]); + +int server(int argc,char *argv[]) +{ + m_task_t task1, task2; + long val1, val2; + + MSG_task_receive(&task1,"mymailbox"); + val1 = (long)MSG_task_get_data(task1); + INFO1("Received %lu", val1); + + MSG_task_receive(&task2,"mymailbox"); + val2 = (long)MSG_task_get_data(task2); + INFO1("Received %lu", val2); + + MC_assert( min(val1, val2) == 1 ); + + INFO0("OK"); + return 0; +} + +int client(int argc,char *argv[]) +{ + m_task_t task1 = MSG_task_create("task", 0, 10000, (void *) atol(argv[1])); + m_task_t task2 = MSG_task_create("task", 0, 10000, (void *) atol(argv[1])); + + INFO1("Send %d!", atoi(argv[1])); + MSG_task_send(task1,"mymailbox"); + + INFO1("Send %d!", atoi(argv[1])); + MSG_task_send(task2,"mymailbox"); + + return 0; +} + +int main(int argc,char*argv[]) +{ + MSG_global_init(&argc,argv); + + MSG_create_environment("platform.xml"); + + MSG_function_register("server", server); + + MSG_function_register("client", client); + + MSG_launch_application("deploy.xml"); + + MSG_main(); + + return 0; +} \ No newline at end of file diff --git a/examples/msg/mc/centralized_mutex.c b/examples/msg/mc/centralized_mutex.c new file mode 100644 index 0000000000..3d6ed63aa0 --- /dev/null +++ b/examples/msg/mc/centralized_mutex.c @@ -0,0 +1,86 @@ +/* Centralized Mutual Exclusion Algorithm + * + * This constitutes the answer to the exercice 2 of the practical + * lab on implementing mutual exclusion algorithms with SimGrid. + * + * YOU SHOULD TRY IMPLEMENTING IT YOURSELF BEFORE READING THE SOLUTION. + */ + +#include "msg/msg.h" + +#define AMOUNT_OF_CLIENTS 5 +#define CS_PER_PROCESS 2 +XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages"); + +int coordinator(int argc, char** argv); +int client(int argc, char** argv); + +int coordinator(int argc, char*argv[]) { + xbt_dynar_t requests=xbt_dynar_new(sizeof(char*),NULL); // dynamic vector storing requests (which are char*) + int CS_used=0; // initially the CS is idle + int todo= AMOUNT_OF_CLIENTS*CS_PER_PROCESS; // amount of releases we are expecting + while(todo>0) { + m_task_t task=NULL; + MSG_task_receive(&task,"coordinator"); + const char *kind = MSG_task_get_name(task); //is it a request or a release? + if (!strcmp(kind,"request")) { // that's a request + char *req = MSG_task_get_data(task); + if (CS_used) { // need to push the request in the vector + INFO0("CS already used. Queue the request"); + xbt_dynar_push(requests, &req); + } else { // can serve it immediatly + INFO0("CS idle. Grant immediatly"); + m_task_t answer = MSG_task_create("grant",0,1000,NULL); + MSG_task_send(answer,req); + CS_used = 1; + } + } else { // that's a release. Check if someone was waiting for the lock + if (xbt_dynar_length(requests)>0) { + INFO1("CS release. Grant to queued requests (queue size: %lu)",xbt_dynar_length(requests)); + char *req; + xbt_dynar_pop(requests,&req); + MSG_task_send(MSG_task_create("grant",0,1000,NULL),req); + todo--; + } else { // nobody wants it + INFO0("CS release. resource now idle"); + CS_used=0; + todo--; + } + } + //MSG_task_destoy(task); + } + INFO0("Received all releases, quit now"); + return 0; +} + +int client(int argc, char *argv[]) { + int my_pid=MSG_process_get_PID(MSG_process_self()); + // use my pid as name of mailbox to contact me + char *my_mailbox=bprintf("%d",my_pid); + // request the CS 3 times, sleeping a bit in between + int i; + for (i=0; i + + + + + + + + + + + + + + + diff --git a/examples/msg/mc/deploy_bugged2.xml b/examples/msg/mc/deploy_bugged2.xml new file mode 100644 index 0000000000..bd2532c0e1 --- /dev/null +++ b/examples/msg/mc/deploy_bugged2.xml @@ -0,0 +1,13 @@ + + + + + + + + + + + + + diff --git a/examples/msg/mc/deploy_mutex.xml b/examples/msg/mc/deploy_mutex.xml new file mode 100644 index 0000000000..0ff13e2a1c --- /dev/null +++ b/examples/msg/mc/deploy_mutex.xml @@ -0,0 +1,39 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/msg/mc/platform.xml b/examples/msg/mc/platform.xml new file mode 100644 index 0000000000..8e6f6cad1b --- /dev/null +++ b/examples/msg/mc/platform.xml @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + + + + + diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h new file mode 100644 index 0000000000..864860d875 --- /dev/null +++ b/include/mc/modelchecker.h @@ -0,0 +1,3 @@ +#include "xbt.h" + +XBT_PUBLIC(void) MC_assert(int); \ No newline at end of file -- 2.20.1