From ef83b403e228c79b1d613d6c52dff1418ab6b71c Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 25 Aug 2015 13:10:16 +0200 Subject: [PATCH] [mc] Add a test to examplify that we should handle mutex operations in MC In this test, we have two senders sending one message to a common receiver. The receiver should be able to see any ordering between the two messages. If we model-check the application with assertions on a specific order of the messages (see the assertions in the receiver code), it should fail because both ordering are possible. If the senders sends the message directly, the current version of the MC finds that the ordering may differ and the MC find a counter-example. However, if the senders send the message in a mutex, the MC always let the first process take the mutex because it thinks that the effect of a mutex is purely local: the ordering of the messages is always the same and the MC does not find the counter-example. --- teshsuite/mc/CMakeLists.txt | 15 +++++ teshsuite/mc/mutex_handling.c | 93 +++++++++++++++++++++++++++++ teshsuite/mc/mutex_handling.tesh | 4 ++ teshsuite/mc/mutex_handling.xml | 16 +++++ teshsuite/mc/no_mutex_handling.tesh | 4 ++ tools/cmake/AddTests.cmake | 3 + 6 files changed, 135 insertions(+) create mode 100644 teshsuite/mc/mutex_handling.c create mode 100644 teshsuite/mc/mutex_handling.tesh create mode 100644 teshsuite/mc/mutex_handling.xml create mode 100644 teshsuite/mc/no_mutex_handling.tesh diff --git a/teshsuite/mc/CMakeLists.txt b/teshsuite/mc/CMakeLists.txt index 5c2f3d20e1..b6e1d81c15 100644 --- a/teshsuite/mc/CMakeLists.txt +++ b/teshsuite/mc/CMakeLists.txt @@ -4,11 +4,26 @@ if(HAVE_MC) set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}") endif() +add_executable(mutex_handling mutex_handling.c) +target_link_libraries(mutex_handling simgrid) + +add_executable(no_mutex_handling mutex_handling.c) +target_link_libraries(no_mutex_handling simgrid) +set_target_properties(no_mutex_handling PROPERTIES COMPILE_FLAGS -DDISABLE_THE_MUTEX=1) + set(tesh_files ${tesh_files} + ${CMAKE_CURRENT_SOURCE_DIR}/mutex_handling.tesh + ${CMAKE_CURRENT_SOURCE_DIR}/no_mutex_handling.tesh PARENT_SCOPE ) set(testsuite_src ${testsuite_src} + ${CMAKE_CURRENT_SOURCE_DIR}/mutex_handling.c + PARENT_SCOPE + ) +set(xml_files + ${xml_files} + ${CMAKE_CURRENT_SOURCE_DIR}/mutex_handling.xml PARENT_SCOPE ) diff --git a/teshsuite/mc/mutex_handling.c b/teshsuite/mc/mutex_handling.c new file mode 100644 index 0000000000..4db2783552 --- /dev/null +++ b/teshsuite/mc/mutex_handling.c @@ -0,0 +1,93 @@ +/* Copyright (c) 2015. 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. */ + +/* In this test, we have two senders sending one message to a common receiver. + * The receiver should be able to see any ordering between the two messages. + * If we model-check the application with assertions on a specific order of + * the messages (see the assertions in the receiver code), it should fail + * because both ordering are possible. + * + * If the senders sends the message directly, the current version of the MC + * finds that the ordering may differ and the MC find a counter-example. + * + * However, if the senders send the message in a mutex, the MC always let + * the first process take the mutex because it thinks that the effect of + * a mutex is purely local: the ordering of the messages is always the same + * and the MC does not find the counter-example. + */ + +#include +#include "simgrid/msg.h" +#include "xbt/log.h" +#include "mc/mc.h" +#include + +XBT_LOG_NEW_DEFAULT_CATEGORY(msg_test, + "Messages specific for this msg example"); + +#define BOX_NAME "box" + +#ifndef DISABLE_THE_MUTEX +static xbt_mutex_t mutex = NULL; +#endif + +static int receiver(int argc, char *argv[]) +{ + msg_task_t task = NULL; + + MSG_task_receive(&task, BOX_NAME); + MC_assert(strcmp(MSG_task_get_name(task), "X") == 0); + MSG_task_destroy(task); + + MSG_task_receive(&task, BOX_NAME); + MC_assert(strcmp(MSG_task_get_name(task), "Y") == 0); + MSG_task_destroy(task); + + return 0; +} + +static int sender(int argc, char *argv[]) +{ + char* message_name = argv[1]; +#ifndef DISABLE_THE_MUTEX + xbt_mutex_acquire(mutex); +#endif + MSG_task_send(MSG_task_create(message_name, 0.0, 0.0, NULL), BOX_NAME); +#ifndef DISABLE_THE_MUTEX + xbt_mutex_release(mutex); +#endif + return 0; +} + +int main(int argc, char *argv[]) +{ + MSG_init(&argc, argv); + if (argc != 3) { + printf("Usage: %s platform_file deployment_file\n", argv[0]); + printf("example: %s msg_platform.xml msg_deployment.xml\n", argv[0]); + exit(1); + } + const char *platform_file = argv[1]; + const char *application_file = argv[2]; + MSG_create_environment(platform_file); + MSG_function_register("receiver", receiver); + MSG_function_register("sender", sender); + + MSG_launch_application(application_file); +#ifndef DISABLE_THE_MUTEX + mutex = xbt_mutex_init(); +#endif + msg_error_t res = MSG_main(); +#ifndef DISABLE_THE_MUTEX + xbt_mutex_destroy(mutex); mutex = NULL; +#endif + XBT_INFO("Simulation time %g", MSG_get_clock()); + + if (res == MSG_OK) + return 0; + else + return 1; +} \ No newline at end of file diff --git a/teshsuite/mc/mutex_handling.tesh b/teshsuite/mc/mutex_handling.tesh new file mode 100644 index 0000000000..4839f3f5de --- /dev/null +++ b/teshsuite/mc/mutex_handling.tesh @@ -0,0 +1,4 @@ +#!/usr/bin/env tesh +! expect return 1 +! output ignore +$ ${bindir:=.}/../../bin/simgrid-mc ${bindir:=.}/mutex_handling --cfg=model-check:1 ../../examples/platforms/platform.xml mutex_handling.xml diff --git a/teshsuite/mc/mutex_handling.xml b/teshsuite/mc/mutex_handling.xml new file mode 100644 index 0000000000..73e165aba6 --- /dev/null +++ b/teshsuite/mc/mutex_handling.xml @@ -0,0 +1,16 @@ + + + + + + + + + + + + + + + + diff --git a/teshsuite/mc/no_mutex_handling.tesh b/teshsuite/mc/no_mutex_handling.tesh new file mode 100644 index 0000000000..58f31e8131 --- /dev/null +++ b/teshsuite/mc/no_mutex_handling.tesh @@ -0,0 +1,4 @@ +#!/usr/bin/env tesh +! expect return 1 +! output ignore +$ ${bindir:=.}/../../bin/simgrid-mc ${bindir:=.}/no_mutex_handling --cfg=model-check:1 ../../examples/platforms/platform.xml mutex_handling.xml diff --git a/tools/cmake/AddTests.cmake b/tools/cmake/AddTests.cmake index e433f108a2..dca967f2be 100644 --- a/tools/cmake/AddTests.cmake +++ b/tools/cmake/AddTests.cmake @@ -101,6 +101,9 @@ IF(NOT enable_memcheck) ADD_TESH(tesh-mc-dwarf --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf dwarf.tesh) ADD_TESH(tesh-mc-dwarf-expression --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf_expression --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf_expression dwarf_expression.tesh) + ADD_TESH(tesh-mc-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc mutex_handling.tesh) + ADD_TESH(tesh-mc-no-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc no_mutex_handling.tesh) + ADD_TESH(mc-record-random-bug --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/replay --setenv srcdir=${CMAKE_HOME_DIRECTORY}/teshsuite/mc/replay --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/replay random_bug.tesh) ADD_TESH_FACTORIES(mc-bugged1 "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/msg/mc bugged1.tesh) -- 2.20.1