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 || MC_record_path))
  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 char *_sg_mc_property_file = nullptr;
  55 int _sg_mc_hash = 0;
  56 int _sg_mc_max_depth = 1000;
  57 int _sg_mc_max_visited_states = 0;
  58 char *_sg_mc_dot_output_file = nullptr;
  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   char *val = xbt_cfg_get_string(name);
  71   if (not strcasecmp(val, "none"))
  72     simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
  73   else if (not strcasecmp(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",
  77             name);
  78 }
  79
  80 void _mc_cfg_cb_checkpoint(const char *name)
  81 {
  82   if (_sg_cfg_init_status && not _sg_do_model_check)
  83     xbt_die
  84         ("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.");
  85
  86   _sg_mc_checkpoint = xbt_cfg_get_int(name);
  87 }
  88
  89 void _mc_cfg_cb_sparse_checkpoint(const char *name) {
  90   if (_sg_cfg_init_status && not _sg_do_model_check)
  91     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.");
  92
  93   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(name);
  94 }
  95
  96 void _mc_cfg_cb_ksm(const char *name)
  97 {
  98   if (_sg_cfg_init_status && not _sg_do_model_check)
  99     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.");
 100
 101   _sg_mc_ksm = xbt_cfg_get_boolean(name);
 102 }
 103
 104 void _mc_cfg_cb_property(const char *name)
 105 {
 106   if (_sg_cfg_init_status && not _sg_do_model_check)
 107     xbt_die
 108         ("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.");
 109
 110   _sg_mc_property_file = xbt_cfg_get_string(name);
 111 }
 112
 113 void _mc_cfg_cb_hash(const char *name)
 114 {
 115   if (_sg_cfg_init_status && not _sg_do_model_check)
 116     xbt_die
 117         ("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.");
 118
 119   _sg_mc_hash = xbt_cfg_get_boolean(name);
 120 }
 121
 122 void _mc_cfg_cb_snapshot_fds(const char *name)
 123 {
 124   if (_sg_cfg_init_status && not _sg_do_model_check)
 125     xbt_die
 126         ("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.");
 127
 128   _sg_mc_snapshot_fds = xbt_cfg_get_boolean(name);
 129 }
 130
 131 void _mc_cfg_cb_max_depth(const char *name)
 132 {
 133   if (_sg_cfg_init_status && not _sg_do_model_check)
 134     xbt_die
 135         ("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.");
 136
 137   _sg_mc_max_depth = xbt_cfg_get_int(name);
 138 }
 139
 140 void _mc_cfg_cb_visited(const char *name)
 141 {
 142   if (_sg_cfg_init_status && not _sg_do_model_check)
 143     xbt_die
 144         ("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.");
 145
 146   _sg_mc_max_visited_states = xbt_cfg_get_int(name);
 147 }
 148
 149 void _mc_cfg_cb_dot_output(const char *name)
 150 {
 151   if (_sg_cfg_init_status && not _sg_do_model_check)
 152     xbt_die
 153         ("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.");
 154
 155   _sg_mc_dot_output_file = xbt_cfg_get_string(name);
 156 }
 157
 158 void _mc_cfg_cb_comms_determinism(const char *name)
 159 {
 160   if (_sg_cfg_init_status && not _sg_do_model_check)
 161     xbt_die
 162         ("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.");
 163
 164   _sg_mc_comms_determinism = xbt_cfg_get_boolean(name);
 165 }
 166
 167 void _mc_cfg_cb_send_determinism(const char *name)
 168 {
 169   if (_sg_cfg_init_status && not _sg_do_model_check)
 170     xbt_die
 171         ("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.");
 172
 173   _sg_mc_send_determinism = xbt_cfg_get_boolean(name);
 174 }
 175
 176 void _mc_cfg_cb_termination(const char *name)
 177 {
 178   if (_sg_cfg_init_status && not _sg_do_model_check)
 179     xbt_die
 180         ("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.");
 181
 182   _sg_mc_termination = xbt_cfg_get_boolean(name);
 183 }
 184
 185 #endif