src/mc/mc_config.c

   1 /* Copyright (c) 2008-2014. 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 <strings.h>
   8
   9 #include <xbt/log.h>
  10 #include <xbt/config.h>
  11
  12 #include <mc/mc.h>
  13
  14 #include <simgrid/sg_config.h>
  15
  16 #ifdef HAVE_MC
  17 #include "mc_safety.h"
  18 #include "mc_private.h"
  19 #endif
  20
  21 #include "mc_record.h"
  22
  23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc,
  24                                 "Configuration of MC");
  25
  26 #ifdef HAVE_MC
  27 /* Configuration support */
  28 e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset;
  29 #endif
  30
  31 #ifndef HAVE_MC
  32 #define _sg_do_model_check 0
  33 #endif
  34
  35 int _sg_mc_timeout = 0;
  36
  37 void _mc_cfg_cb_timeout(const char *name, int pos)
  38 {
  39   if (_sg_cfg_init_status && !(_sg_do_model_check || MC_record_path)) {
  40     xbt_die
  41         ("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.");
  42   }
  43   _sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name);
  44 }
  45
  46 #ifdef HAVE_MC
  47 int _sg_do_model_check = 0;
  48 int _sg_do_model_check_record = 0;
  49 int _sg_mc_checkpoint = 0;
  50 int _sg_mc_sparse_checkpoint = 0;
  51 int _sg_mc_soft_dirty = 0;
  52 char *_sg_mc_property_file = NULL;
  53 int _sg_mc_hash = 0;
  54 int _sg_mc_max_depth = 1000;
  55 int _sg_mc_visited = 0;
  56 char *_sg_mc_dot_output_file = NULL;
  57 int _sg_mc_comms_determinism = 0;
  58 int _sg_mc_send_determinism = 0;
  59 int _sg_mc_safety = 0;
  60 int _sg_mc_liveness = 0;
  61
  62
  63 void _mc_cfg_cb_reduce(const char *name, int pos)
  64 {
  65   if (_sg_cfg_init_status && !_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 --cfg=model-check:1). This won't work, sorry.");
  68   }
  69   char *val = xbt_cfg_get_string(_sg_cfg_set, name);
  70   if (!strcasecmp(val, "none")) {
  71     mc_reduce_kind = e_mc_reduce_none;
  72   } else if (!strcasecmp(val, "dpor")) {
  73     mc_reduce_kind = e_mc_reduce_dpor;
  74   } else {
  75     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",
  76             name);
  77   }
  78 }
  79
  80 void _mc_cfg_cb_checkpoint(const char *name, int pos)
  81 {
  82   if (_sg_cfg_init_status && !_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 --cfg=model-check:1). This won't work, sorry.");
  85   }
  86   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
  87 }
  88
  89 void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
  90   if (_sg_cfg_init_status && !_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 --cfg=model-check:1). This won't work, sorry.");
  92   }
  93   _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
  94 }
  95
  96 void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
  97   if (_sg_cfg_init_status && !_sg_do_model_check) {
  98     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.");
  99   }
 100   _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name);
 101 }
 102
 103 void _mc_cfg_cb_property(const char *name, int pos)
 104 {
 105   if (_sg_cfg_init_status && !_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 --cfg=model-check:1). This won't work, sorry.");
 108   }
 109   _sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name);
 110 }
 111
 112 void _mc_cfg_cb_hash(const char *name, int pos)
 113 {
 114   if (_sg_cfg_init_status && !_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 --cfg=model-check:1). This won't work, sorry.");
 117   }
 118   _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
 119 }
 120
 121 void _mc_cfg_cb_max_depth(const char *name, int pos)
 122 {
 123   if (_sg_cfg_init_status && !_sg_do_model_check) {
 124     xbt_die
 125         ("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.");
 126   }
 127   _sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name);
 128 }
 129
 130 void _mc_cfg_cb_visited(const char *name, int pos)
 131 {
 132   if (_sg_cfg_init_status && !_sg_do_model_check) {
 133     xbt_die
 134         ("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.");
 135   }
 136   _sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name);
 137 }
 138
 139 void _mc_cfg_cb_dot_output(const char *name, int pos)
 140 {
 141   if (_sg_cfg_init_status && !_sg_do_model_check) {
 142     xbt_die
 143         ("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.");
 144   }
 145   _sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name);
 146 }
 147
 148 void _mc_cfg_cb_comms_determinism(const char *name, int pos)
 149 {
 150   if (_sg_cfg_init_status && !_sg_do_model_check) {
 151     xbt_die
 152         ("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.");
 153   }
 154   _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
 155   mc_reduce_kind = e_mc_reduce_none;
 156 }
 157
 158 void _mc_cfg_cb_send_determinism(const char *name, int pos)
 159 {
 160   if (_sg_cfg_init_status && !_sg_do_model_check) {
 161     xbt_die
 162         ("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.");
 163   }
 164   _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
 165   mc_reduce_kind = e_mc_reduce_none;
 166 }
 167
 168 #endif