From: Gabriel Corona Date: Fri, 31 Oct 2014 15:09:04 +0000 (+0100) Subject: [mc] Split config code into mc_config.c X-Git-Tag: v3_12~732^2~267 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c8c284176e4f5ae35bf26ad48515f4b029866ef2 [mc] Split config code into mc_config.c --- diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 87a15f508a..05b579ce9f 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -606,6 +606,7 @@ set(MC_SRC src/mc/mc_page_snapshot.cpp src/mc/mc_comm_determinism.c src/mc/mc_compare.cpp + src/mc/mc_config.c src/mc/mc_diff.c src/mc/mc_dwarf.c src/mc/mc_dwarf_attrnames.h diff --git a/src/mc/mc_config.c b/src/mc/mc_config.c new file mode 100644 index 0000000000..eeb080a1e6 --- /dev/null +++ b/src/mc/mc_config.c @@ -0,0 +1,152 @@ +/* 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 + +#include +#include + +#include + +#include + +#include "mc_private.h" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, + "Configuration of MC"); + +/* Configuration support */ +e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset; + +int _sg_do_model_check = 0; +int _sg_mc_checkpoint = 0; +int _sg_mc_sparse_checkpoint = 0; +int _sg_mc_soft_dirty = 0; +char *_sg_mc_property_file = NULL; +int _sg_mc_timeout = 0; +int _sg_mc_hash = 0; +int _sg_mc_max_depth = 1000; +int _sg_mc_visited = 0; +char *_sg_mc_dot_output_file = NULL; +int _sg_mc_comms_determinism = 0; +int _sg_mc_send_determinism = 0; +int _sg_mc_safety = 0; +int _sg_mc_liveness = 0; + + +void _mc_cfg_cb_reduce(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + char *val = xbt_cfg_get_string(_sg_cfg_set, name); + if (!strcasecmp(val, "none")) { + mc_reduce_kind = e_mc_reduce_none; + } else if (!strcasecmp(val, "dpor")) { + mc_reduce_kind = e_mc_reduce_dpor; + } else { + xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", + name); + } +} + +void _mc_cfg_cb_checkpoint(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name); +} + +void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name); +} + +void _mc_cfg_cb_soft_dirty(const char *name, int pos) { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die("You are specifying a soft dirty value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name); +} + +void _mc_cfg_cb_property(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name); +} + +void _mc_cfg_cb_timeout(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name); +} + +void _mc_cfg_cb_hash(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name); +} + +void _mc_cfg_cb_max_depth(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name); +} + +void _mc_cfg_cb_visited(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name); +} + +void _mc_cfg_cb_dot_output(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name); +} + +void _mc_cfg_cb_comms_determinism(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); + mc_reduce_kind = e_mc_reduce_none; +} + +void _mc_cfg_cb_send_determinism(const char *name, int pos) +{ + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die + ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); + mc_reduce_kind = e_mc_reduce_none; +} diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index c66e9c9285..0d4543dd6d 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -24,140 +24,8 @@ XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); -/* Configuration support */ -e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset; - -int _sg_do_model_check = 0; -int _sg_mc_checkpoint = 0; -int _sg_mc_sparse_checkpoint = 0; -int _sg_mc_soft_dirty = 0; -char *_sg_mc_property_file = NULL; -int _sg_mc_timeout = 0; -int _sg_mc_hash = 0; -int _sg_mc_max_depth = 1000; -int _sg_mc_visited = 0; -char *_sg_mc_dot_output_file = NULL; -int _sg_mc_comms_determinism = 0; -int _sg_mc_send_determinism = 0; -int _sg_mc_safety = 0; -int _sg_mc_liveness = 0; - int user_max_depth_reached = 0; -void _mc_cfg_cb_reduce(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - char *val = xbt_cfg_get_string(_sg_cfg_set, name); - if (!strcasecmp(val, "none")) { - mc_reduce_kind = e_mc_reduce_none; - } else if (!strcasecmp(val, "dpor")) { - mc_reduce_kind = e_mc_reduce_dpor; - } else { - xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", - name); - } -} - -void _mc_cfg_cb_checkpoint(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name); -} - -void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) { - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name); -} - -void _mc_cfg_cb_soft_dirty(const char *name, int pos) { - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die("You are specifying a soft dirty value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name); -} - -void _mc_cfg_cb_property(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name); -} - -void _mc_cfg_cb_timeout(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name); -} - -void _mc_cfg_cb_hash(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name); -} - -void _mc_cfg_cb_max_depth(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name); -} - -void _mc_cfg_cb_visited(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name); -} - -void _mc_cfg_cb_dot_output(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name); -} - -void _mc_cfg_cb_comms_determinism(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); - mc_reduce_kind = e_mc_reduce_none; -} - -void _mc_cfg_cb_send_determinism(const char *name, int pos) -{ - if (_sg_cfg_init_status && !_sg_do_model_check) { - xbt_die - ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); - } - _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); - mc_reduce_kind = e_mc_reduce_none; -} - /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; @@ -478,7 +346,7 @@ void MC_wait_for_requests(void) while (!xbt_dynar_is_empty(simix_global->process_to_run)) { SIMIX_process_runall(); - xbt_dynar_foreach(simix_global->process_that_ran, iter, process) { + xbt_dynar_foreach(simix_global->process_that_ran, iter, process) { req = &process->simcall; if (req->call != SIMCALL_NONE && !MC_request_is_visible(req)) SIMIX_simcall_enter(req, 0);