src/mc/mc_config.cpp

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