src/mc/mc_config.cpp

   1 /* Copyright (c) 2008-2017. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "xbt/config.h"
   8 #include "xbt/log.h"
   9 #include <xbt/sysdep.h>
  10
  11 #include <mc/mc.h>
  12 #include "src/mc/mc_replay.h"
  13
  14 #include <simgrid/sg_config.h>
  15
  16 #if SIMGRID_HAVE_MC
  17 #include "src/mc/mc_private.hpp"
  18 #include "src/mc/mc_safety.hpp"
  19 #endif
  20
  21 #include "src/mc/mc_record.hpp"
  22
  23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, "Configuration of the Model Checker");
  24
  25 #if SIMGRID_HAVE_MC
  26 namespace simgrid {
  27 namespace mc {
  28 /* Configuration support */
  29 simgrid::mc::ReductionMode reduction_mode = simgrid::mc::ReductionMode::unset;
  30 }
  31 }
  32 #endif
  33
  34 #if !SIMGRID_HAVE_MC
  35 #define _sg_do_model_check 0
  36 #endif
  37
  38 int _sg_mc_timeout = 0;
  39
  40 void _mc_cfg_cb_timeout(const char *name)
  41 {
  42   if (_sg_cfg_init_status && not(_sg_do_model_check || not MC_record_path.empty()))
  43     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 bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
  44
  45   _sg_mc_timeout = xbt_cfg_get_boolean(name);
  46 }
  47
  48 #if SIMGRID_HAVE_MC
  49 int _sg_do_model_check = 0;
  50 int _sg_do_model_check_record = 0;
  51 int _sg_mc_checkpoint = 0;
  52 int _sg_mc_sparse_checkpoint = 0;
  53 int _sg_mc_ksm = 0;
  54 std::string _sg_mc_property_file;
  55 int _sg_mc_hash = 0;
  56 int _sg_mc_max_depth = 1000;
  57 int _sg_mc_max_visited_states = 0;
  58 std::string _sg_mc_dot_output_file;
  59 int _sg_mc_comms_determinism = 0;
  60 int _sg_mc_send_determinism = 0;
  61 int _sg_mc_snapshot_fds = 0;
  62 int _sg_mc_termination = 0;
  63
  64 void _mc_cfg_cb_reduce(const char *name)
  65 {
  66   if (_sg_cfg_init_status && not _sg_do_model_check)
  67     xbt_die
  68         ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
  69
  70   std::string val = xbt_cfg_get_string(name);
  71   if (val == "none")
  72     simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
  73   else if (val == "dpor")
  74     simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
  75   else
  76     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", name);
  77 }
  78
  79 void _mc_cfg_cb_checkpoint(const char *name)
  80 {
  81   if (_sg_cfg_init_status && not _sg_do_model_check)
  82     xbt_die
  83         ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
  84
  85   _sg_mc_checkpoint = xbt_cfg_get_int(name);
  86 }
  87
  88 void _mc_cfg_cb_sparse_checkpoint(const char *name) {
  89   if (_sg_cfg_init_status && not _sg_do_model_check)
  90     xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
  91
  92   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name);
  93 }
  94
  95 void _mc_cfg_cb_ksm(const char *name)
  96 {
  97   if (_sg_cfg_init_status && not _sg_do_model_check)
  98     xbt_die("You are specifying a KSM 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.");
  99
 100   _sg_mc_ksm = xbt_cfg_get_boolean(name);
 101 }
 102
 103 void _mc_cfg_cb_property(const char *name)
 104 {
 105   if (_sg_cfg_init_status && not _sg_do_model_check)
 106     xbt_die
 107         ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 108
 109   _sg_mc_property_file = xbt_cfg_get_string(name);
 110 }
 111
 112 void _mc_cfg_cb_hash(const char *name)
 113 {
 114   if (_sg_cfg_init_status && not _sg_do_model_check)
 115     xbt_die
 116         ("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 bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 117
 118   _sg_mc_hash = xbt_cfg_get_boolean(name);
 119 }
 120
 121 void _mc_cfg_cb_snapshot_fds(const char *name)
 122 {
 123   if (_sg_cfg_init_status && not _sg_do_model_check)
 124     xbt_die
 125         ("You are specifying a value to enable/disable the use of FD snapshotting, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 126
 127   _sg_mc_snapshot_fds = xbt_cfg_get_boolean(name);
 128 }
 129
 130 void _mc_cfg_cb_max_depth(const char *name)
 131 {
 132   if (_sg_cfg_init_status && not _sg_do_model_check)
 133     xbt_die
 134         ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 135
 136   _sg_mc_max_depth = xbt_cfg_get_int(name);
 137 }
 138
 139 void _mc_cfg_cb_visited(const char *name)
 140 {
 141   if (_sg_cfg_init_status && not _sg_do_model_check)
 142     xbt_die
 143         ("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 bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 144
 145   _sg_mc_max_visited_states = xbt_cfg_get_int(name);
 146 }
 147
 148 void _mc_cfg_cb_dot_output(const char *name)
 149 {
 150   if (_sg_cfg_init_status && not _sg_do_model_check)
 151     xbt_die
 152         ("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 bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 153
 154   _sg_mc_dot_output_file = xbt_cfg_get_string(name);
 155 }
 156
 157 void _mc_cfg_cb_comms_determinism(const char *name)
 158 {
 159   if (_sg_cfg_init_status && not _sg_do_model_check)
 160     xbt_die
 161         ("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 bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 162
 163   _sg_mc_comms_determinism = xbt_cfg_get_boolean(name);
 164 }
 165
 166 void _mc_cfg_cb_send_determinism(const char *name)
 167 {
 168   if (_sg_cfg_init_status && not _sg_do_model_check)
 169     xbt_die
 170         ("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 bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 171
 172   _sg_mc_send_determinism = xbt_cfg_get_boolean(name);
 173 }
 174
 175 void _mc_cfg_cb_termination(const char *name)
 176 {
 177   if (_sg_cfg_init_status && not _sg_do_model_check)
 178     xbt_die
 179         ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 180
 181   _sg_mc_termination = xbt_cfg_get_boolean(name);
 182 }
 183
 184 #endif