src/mc/mc_config.cpp

   1 /* Copyright (c) 2008-2018. 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.hpp>
  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 static void _mc_cfg_cb_check(const char* spec, bool more_check = true)
  40 {
  41   if (_sg_cfg_init_status && not _sg_do_model_check && more_check)
  42     xbt_die("You are specifying a %s after the initialization (through MSG_config?), but the program was not run under "
  43             "the model-checker (with simgrid-mc)). This won't work, sorry.",
  44             spec);
  45 }
  46
  47 void _mc_cfg_cb_timeout(const char *name)
  48 {
  49   _mc_cfg_cb_check("value to enable/disable timeout for wait requests", MC_record_path.empty());
  50
  51   _sg_mc_timeout = xbt_cfg_get_boolean(name);
  52 }
  53
  54 #if SIMGRID_HAVE_MC
  55 int _sg_do_model_check = 0;
  56 int _sg_do_model_check_record = 0;
  57 int _sg_mc_checkpoint = 0;
  58 int _sg_mc_sparse_checkpoint = 0;
  59 int _sg_mc_ksm = 0;
  60 std::string _sg_mc_property_file;
  61 int _sg_mc_hash = 0;
  62 int _sg_mc_max_depth = 1000;
  63 int _sg_mc_max_visited_states = 0;
  64 std::string _sg_mc_dot_output_file;
  65 int _sg_mc_comms_determinism = 0;
  66 int _sg_mc_send_determinism = 0;
  67 int _sg_mc_snapshot_fds = 0;
  68 int _sg_mc_termination = 0;
  69
  70 void _mc_cfg_cb_reduce(const char *name)
  71 {
  72   _mc_cfg_cb_check("reduction strategy");
  73
  74   std::string val = xbt_cfg_get_string(name);
  75   if (val == "none")
  76     simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
  77   else if (val == "dpor")
  78     simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
  79   else
  80     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", name);
  81 }
  82
  83 void _mc_cfg_cb_checkpoint(const char *name)
  84 {
  85   _mc_cfg_cb_check("checkpointing value");
  86
  87   _sg_mc_checkpoint = xbt_cfg_get_int(name);
  88 }
  89
  90 void _mc_cfg_cb_sparse_checkpoint(const char *name) {
  91   _mc_cfg_cb_check("checkpointing value");
  92
  93   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name);
  94 }
  95
  96 void _mc_cfg_cb_ksm(const char *name)
  97 {
  98   _mc_cfg_cb_check("KSM value");
  99
 100   _sg_mc_ksm = xbt_cfg_get_boolean(name);
 101 }
 102
 103 void _mc_cfg_cb_property(const char *name)
 104 {
 105   _mc_cfg_cb_check("property");
 106
 107   _sg_mc_property_file = xbt_cfg_get_string(name);
 108 }
 109
 110 void _mc_cfg_cb_hash(const char *name)
 111 {
 112   _mc_cfg_cb_check("value to enable/disable the use of global hash to speedup state comparaison");
 113
 114   _sg_mc_hash = xbt_cfg_get_boolean(name);
 115 }
 116
 117 void _mc_cfg_cb_snapshot_fds(const char *name)
 118 {
 119   _mc_cfg_cb_check("value to enable/disable the use of FD snapshotting");
 120
 121   _sg_mc_snapshot_fds = xbt_cfg_get_boolean(name);
 122 }
 123
 124 void _mc_cfg_cb_max_depth(const char *name)
 125 {
 126   _mc_cfg_cb_check("max depth value");
 127
 128   _sg_mc_max_depth = xbt_cfg_get_int(name);
 129 }
 130
 131 void _mc_cfg_cb_visited(const char *name)
 132 {
 133   _mc_cfg_cb_check("number of stored visited states");
 134
 135   _sg_mc_max_visited_states = xbt_cfg_get_int(name);
 136 }
 137
 138 void _mc_cfg_cb_dot_output(const char *name)
 139 {
 140   _mc_cfg_cb_check("file name for a dot output of graph state");
 141
 142   _sg_mc_dot_output_file = xbt_cfg_get_string(name);
 143 }
 144
 145 void _mc_cfg_cb_comms_determinism(const char *name)
 146 {
 147   _mc_cfg_cb_check("value to enable/disable the detection of determinism in the communications schemes");
 148
 149   _sg_mc_comms_determinism = xbt_cfg_get_boolean(name);
 150 }
 151
 152 void _mc_cfg_cb_send_determinism(const char *name)
 153 {
 154   _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes");
 155
 156   _sg_mc_send_determinism = xbt_cfg_get_boolean(name);
 157 }
 158
 159 void _mc_cfg_cb_termination(const char *name)
 160 {
 161   _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles");
 162
 163   _sg_mc_termination = xbt_cfg_get_boolean(name);
 164 }
 165
 166 #endif