From: Gabriel Corona Date: Fri, 17 Apr 2015 10:32:33 +0000 (+0200) Subject: [mc] Remove standalone mode and remove MC_do_the_modelcheck_for_real() X-Git-Tag: v3_12~732^2~57 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d97d6e19cb366fd112e63d56a9f411d968ee8670?hp=8139a23d31f0561dc2119001779692c3e0487b52 [mc] Remove standalone mode and remove MC_do_the_modelcheck_for_real() --- diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 112140d344..ee2fc7c497 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -582,6 +582,7 @@ set(MC_SRC_BASE src/mc/mc_base.cpp src/mc/mc_base.h src/mc/mc_record.h + src/mc/mc_replay.h src/mc/mc_record.cpp src/mc/mc_config.cpp src/mc/mc_global.cpp diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index 2cf32341fc..ff34bf3dfa 100644 --- a/examples/msg/chord/chord.c +++ b/examples/msg/chord/chord.c @@ -10,6 +10,7 @@ #include "xbt/asserts.h" #include "simgrid/modelchecker.h" #include +#include "mc/mc_replay.h" /** @addtogroup MSG_examples * diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index 0ebb4ec890..cc85d75e2b 100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@ -2,7 +2,7 @@ ! timeout 60 $ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic -> [0.000000] [mc_global/INFO] Check communication determinism +> [0.000000] [mc_comm_determinism/INFO] Check communication determinism > [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s) > [0.000000] [mc_global/INFO] ****************************************************** > [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern **** diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 3cc7e2d583..15b877dcbe 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -17,17 +17,6 @@ SG_BEGIN_DECL() -/** Replay path (if any) in string representation - * - * This is a path as generated by `MC_record_stack_to_string()`. - */ -XBT_PUBLIC_DATA(char*) MC_record_path; - -/** Whether the replay mode is enabled */ -static inline bool MC_record_replay_is_active(void) { - return MC_record_path; -} - XBT_PUBLIC(int) MC_random(int min, int max); #ifdef HAVE_MC diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 23be47f024..317ade94a4 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -73,7 +73,7 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos); void _mc_cfg_cb_send_determinism(const char *name, int pos); void _mc_cfg_cb_termination(const char *name, int pos); -XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); +XBT_PUBLIC(void) MC_run(void); XBT_PUBLIC(void) MC_init(void); XBT_PUBLIC(void) MC_exit(void); XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index fd67dae861..45a1b98ceb 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -10,7 +10,8 @@ #include "mc_base.h" #include "../simix/smx_private.h" -#include "mc_record.h" +#include "mc/mc_record.h" +#include "mc/mc_replay.h" #ifdef HAVE_MC #include "mc_process.h" diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index e180720787..192770fe5e 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -25,12 +25,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, void MC_assert(int prop) { if (MC_is_active() && !prop) { - if (mc_mode == MC_MODE_STANDALONE) { - MC_report_assertion_error(); - } else { - MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED); - MC_client_handle_messages(); - } + MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED); + MC_client_handle_messages(); } } diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index ab30d5c14d..61b2027390 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -501,6 +501,10 @@ static void MC_modelcheck_comm_determinism_main(void) void MC_modelcheck_comm_determinism(void) { + XBT_INFO("Check communication determinism"); + mc_reduce_kind = e_mc_reduce_none; + MC_wait_for_requests(); + if (mc_mode == MC_MODE_CLIENT) { // This will move somehwere else: MC_client_handle_messages(); diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 9239ba8774..1169f2d4d0 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -10,6 +10,7 @@ #include #include +#include "mc/mc_replay.h" #include diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 28cbc9d3c2..353eb42d07 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -106,17 +106,6 @@ static void MC_init_dot_output() } -static void MC_init_mode(void) -{ - if (mc_mode == MC_MODE_NONE) { - if (getenv(MC_ENV_SOCKET_FD)) { - mc_mode = MC_MODE_CLIENT; - } else { - mc_mode = MC_MODE_STANDALONE; - } - } -} - #ifdef HAVE_MC void MC_init() { @@ -196,7 +185,7 @@ void MC_init_pid(pid_t pid, int socket) /* SIMIX */ MC_ignore_global_variable("smx_total_comms"); - if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) { + if (mc_mode == MC_MODE_CLIENT) { /* Those requests are handled on the client side and propagated by message * to the server: */ @@ -217,58 +206,13 @@ void MC_init_pid(pid_t pid, int socket) /******************************* Core of MC *******************************/ /**************************************************************************/ -void MC_do_the_modelcheck_for_real() +void MC_run() { - MC_init_mode(); - - switch(mc_mode) { - default: - xbt_die("Unexpected mc mode"); - break; - case MC_MODE_CLIENT: - MC_init(); - MC_client_main_loop(); - return; - case MC_MODE_SERVER: - break; - case MC_MODE_STANDALONE: - MC_init(); - break; - } - - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - XBT_INFO("Check communication determinism"); - mc_reduce_kind = e_mc_reduce_none; - MC_wait_for_requests(); - MC_modelcheck_comm_determinism(); - } - - else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { - if(_sg_mc_termination) - mc_reduce_kind = e_mc_reduce_none; - else if (mc_reduce_kind == e_mc_reduce_unset) - mc_reduce_kind = e_mc_reduce_dpor; - _sg_mc_safety = 1; - if (_sg_mc_termination) - XBT_INFO("Check non progressive cycles"); - else - XBT_INFO("Check a safety property"); - MC_wait_for_requests(); - MC_modelcheck_safety(); - } - - else { - if (mc_reduce_kind == e_mc_reduce_unset) - mc_reduce_kind = e_mc_reduce_none; - XBT_INFO("Check the liveness property %s", _sg_mc_property_file); - MC_automaton_load(_sg_mc_property_file); - MC_wait_for_requests(); - MC_modelcheck_liveness(); - } - + mc_mode = MC_MODE_CLIENT; + MC_init(); + MC_client_main_loop(); } - void MC_exit(void) { xbt_free(mc_time); diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp index 293eebd007..41be27f176 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/mc_liveness.cpp @@ -16,6 +16,8 @@ #include "mc_record.h" #include "mc_smx.h" #include "mc_client.h" +#include "mc_replay.h" +#include "mc_safety.h" extern "C" { @@ -405,6 +407,12 @@ static void MC_modelcheck_liveness_main(void) void MC_modelcheck_liveness(void) { + if (mc_reduce_kind == e_mc_reduce_unset) + mc_reduce_kind = e_mc_reduce_none; + XBT_INFO("Check the liveness property %s", _sg_mc_property_file); + MC_automaton_load(_sg_mc_property_file); + MC_wait_for_requests(); + XBT_DEBUG("Starting the liveness algorithm"); _sg_mc_liveness = 1; diff --git a/src/mc/mc_model_checker.cpp b/src/mc/mc_model_checker.cpp index 45b13b266e..0484dd20f1 100644 --- a/src/mc/mc_model_checker.cpp +++ b/src/mc/mc_model_checker.cpp @@ -33,9 +33,6 @@ void MC_model_checker_delete(mc_model_checker_t mc) unsigned long MC_smx_get_maxpid(void) { - if (mc_mode == MC_MODE_STANDALONE) - return simix_process_maxpid; - unsigned long maxpid; MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid", &maxpid, sizeof(maxpid)); diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp index 2e5ffd3eb6..01c4f9dd40 100644 --- a/src/mc/mc_protocol.cpp +++ b/src/mc/mc_protocol.cpp @@ -119,8 +119,6 @@ const char* MC_mode_name(e_mc_mode_t mode) switch(mode) { case MC_MODE_NONE: return "NONE"; - case MC_MODE_STANDALONE: - return "STANDALONE"; case MC_MODE_CLIENT: return "CLIENT"; case MC_MODE_SERVER: diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h index 6ad420b715..722c71d080 100644 --- a/src/mc/mc_protocol.h +++ b/src/mc/mc_protocol.h @@ -27,7 +27,6 @@ SG_BEGIN_DECL() typedef enum { MC_MODE_NONE = 0, - MC_MODE_STANDALONE, MC_MODE_CLIENT, MC_MODE_SERVER } e_mc_mode_t; diff --git a/src/mc/mc_replay.h b/src/mc/mc_replay.h new file mode 100644 index 0000000000..2918305649 --- /dev/null +++ b/src/mc/mc_replay.h @@ -0,0 +1,29 @@ +/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid */ + +/* Copyright (c) 2008-2014. 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 + +#ifndef SIMGRID_MC_REPLAY_H +#define SIMGRID_MC_REPLAY_H + +SG_BEGIN_DECL() + +/** Replay path (if any) in string representation + * + * This is a path as generated by `MC_record_stack_to_string()`. + */ +XBT_PUBLIC_DATA(char*) MC_record_path; + +/** Whether the replay mode is enabled */ +static inline int MC_record_replay_is_active(void) { + return MC_record_path != 0; +} + +SG_END_DECL() + +#endif diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp index 4717ab9390..f05de0665f 100644 --- a/src/mc/mc_safety.cpp +++ b/src/mc/mc_safety.cpp @@ -272,6 +272,17 @@ static void MC_modelcheck_safety_main(void) void MC_modelcheck_safety(void) { + if(_sg_mc_termination) + mc_reduce_kind = e_mc_reduce_none; + else if (mc_reduce_kind == e_mc_reduce_unset) + mc_reduce_kind = e_mc_reduce_dpor; + _sg_mc_safety = 1; + if (_sg_mc_termination) + XBT_INFO("Check non progressive cycles"); + else + XBT_INFO("Check a safety property"); + MC_wait_for_requests(); + XBT_DEBUG("Starting the safety algorithm"); _sg_mc_safety = 1; diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 71d0388828..1e9d352c5b 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -31,6 +31,8 @@ #include "mc_server.h" #include "mc_model_checker.h" #include "mc_safety.h" +#include "mc_comm_pattern.h" +#include "mc_liveness.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); @@ -82,7 +84,12 @@ static int do_parent(int socket, pid_t child) mc_server = new s_mc_server(child, socket); mc_server->start(); MC_init_pid(child, socket); - MC_do_the_modelcheck_for_real(); + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) + MC_modelcheck_comm_determinism(); + else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') + MC_modelcheck_safety(); + else + MC_modelcheck_liveness(); mc_server->shutdown(); mc_server->exit(); } diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c index b9351e8bc1..6deb8957c5 100644 --- a/src/msg/msg_global.c +++ b/src/msg/msg_global.c @@ -122,7 +122,7 @@ msg_error_t MSG_main(void) fflush(stderr); if (MC_is_active()) { - MC_do_the_modelcheck_for_real(); + MC_run(); } else { SIMIX_run(); } diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index ad2bbb84ee..0ff07a2b98 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -22,6 +22,7 @@ #include "mc/mc.h" #include "mc/mc_record.h" #include "simgrid/instr.h" +#include "mc/mc_replay.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(surf_config, surf, "About the configuration of simgrid"); diff --git a/src/simix/libsmx.c b/src/simix/libsmx.c index 35b3c8ec62..17ff1ba9e5 100644 --- a/src/simix/libsmx.c +++ b/src/simix/libsmx.c @@ -10,6 +10,7 @@ /* 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 "mc/mc_replay.h" #include "smx_private.h" #include "mc/mc_interface.h" #include "xbt/ex.h" diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c index 0011f977f2..d0ba2747a0 100644 --- a/src/simix/smx_global.c +++ b/src/simix/smx_global.c @@ -13,6 +13,7 @@ #include "xbt/str.h" #include "xbt/ex.h" /* ex_backtrace_display */ #include "mc/mc.h" +#include "mc/mc_replay.h" #include "simgrid/sg_config.h" #ifdef HAVE_MC @@ -220,8 +221,6 @@ void SIMIX_global_init(int *argc, char **argv) MC_client_init(); MC_client_hello(); MC_client_handle_messages(); - } else { - mc_mode = MC_MODE_STANDALONE; } } #endif diff --git a/src/simix/smx_host.c b/src/simix/smx_host.c index be58fe500e..20e7abbbc7 100644 --- a/src/simix/smx_host.c +++ b/src/simix/smx_host.c @@ -9,6 +9,7 @@ #include "xbt/log.h" #include "xbt/dict.h" #include "mc/mc.h" +#include "mc/mc_replay.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_host, simix, "SIMIX hosts"); diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index 942deb5779..fbeb548248 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -7,10 +7,10 @@ #include "smx_private.h" #include "xbt/log.h" #include "mc/mc.h" +#include "mc/mc_replay.h" #include "xbt/dict.h" #include "smpi/private.h" - XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_network, simix, "SIMIX network-related synchronization"); diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c index 8fa3c6b8da..8771f6ed32 100644 --- a/src/simix/smx_process.c +++ b/src/simix/smx_process.c @@ -9,6 +9,7 @@ #include "xbt/log.h" #include "xbt/dict.h" #include "mc/mc.h" +#include "mc/mc_replay.h" #include "mc/mc_client.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix, diff --git a/src/smpi/smpi_base.c b/src/smpi/smpi_base.c index c75e51dabf..af7deebdcd 100644 --- a/src/smpi/smpi_base.c +++ b/src/smpi/smpi_base.c @@ -7,6 +7,7 @@ #include "private.h" #include "xbt/virtu.h" #include "mc/mc.h" +#include "mc/mc_replay.h" #include "xbt/replay.h" #include #include "simix/smx_private.h" diff --git a/src/smpi/smpi_bench.c b/src/smpi/smpi_bench.c index 35971e220e..b6b56e8740 100644 --- a/src/smpi/smpi_bench.c +++ b/src/smpi/smpi_bench.c @@ -13,6 +13,7 @@ #include "surf/surf.h" #include "simgrid/sg_config.h" #include "simgrid/modelchecker.h" +#include "mc/mc_replay.h" #ifndef WIN32 #include diff --git a/src/smpi/smpi_global.c b/src/smpi/smpi_global.c index ac3cd86c9e..f47536e177 100644 --- a/src/smpi/smpi_global.c +++ b/src/smpi/smpi_global.c @@ -12,6 +12,7 @@ #include "surf/surf.h" #include "simix/smx_private.h" #include "simgrid/sg_config.h" +#include "mc/mc_replay.h" #include /* DBL_MAX */ #include @@ -666,7 +667,7 @@ int smpi_main(int (*realmain) (int argc, char *argv[]), int argc, char *argv[]) fflush(stderr); if (MC_is_active()) { - MC_do_the_modelcheck_for_real(); + MC_run(); } else { SIMIX_run();