### define source packages
set(EXTRA_DIST
+ src/include/instr/instr_interface.h
src/include/mc/datatypes.h
src/include/mc/mc.h
src/include/simgrid/platf_interface.h
--- /dev/null
+void TRACE_help(int detailed);
SG_BEGIN_DECL()
+/********************************** Configuration of MC **************************************/
+extern int _sg_do_model_check;
+extern int _sg_mc_checkpoint;
+extern char* _sg_mc_property_file;
+extern int _sg_mc_timeout;
+extern int _sg_mc_max_depth;
+extern int _sg_mc_visited;
+
extern char*_surf_mc_property_file; /* fixme: better location? */
extern xbt_dynar_t mc_heap_comparison_ignore;
-
#include "xbt/config.h"
/*******************************************/
SG_BEGIN_DECL()
/* Actions and models are highly connected structures... */
+/* user-visible parameters */
+extern double sg_tcp_gamma;
+extern double sg_sender_gap;
+extern double sg_latency_factor;
+extern double sg_bandwidth_factor;
+extern double sg_weight_S_parameter;
+extern int sg_maxmin_selective_update;
+extern int sg_network_crosstraffic;
+#ifdef HAVE_GTNETS
+extern double sg_gtnets_jitter;
+extern int sg_gtnets_jitter_seed;
+#endif
+extern xbt_dynar_t surf_path;
+
+
typedef enum {
SURF_NETWORK_ELEMENT_NULL = 0, /* NULL */
SURF_NETWORK_ELEMENT_HOST, /* host type */
void surf_watched_hosts(void);
+/*
+ * Returns the initial path. On Windows the initial path is
+ * the current directory for the current process in the other
+ * case the function returns "./" that represents the current
+ * directory on Unix/Linux platforms.
+ */
+const char *__surf_get_initial_path(void);
+
SG_END_DECL()
#endif /* _SURF_SURF_H */
#ifndef INSTR_PRIVATE_H_
#define INSTR_PRIVATE_H_
+#include "instr/instr_interface.h"
#include "simgrid_config.h"
#ifdef HAVE_TRACING
#define INSTR_DEFAULT_STR_SIZE 500
-#include "instr/instr.h"
#include "msg/msg.h"
#include "simdag/private.h"
#include "simix/smx_private.h"
char *TRACE_get_viva_uncat_conf (void);
char *TRACE_get_viva_cat_conf (void);
void TRACE_global_init(int *argc, char **argv);
-void TRACE_help(int detailed);
void TRACE_generate_viva_uncat_conf (void);
void TRACE_generate_viva_cat_conf (void);
void instr_pause_tracing (void);
}
}
- if(_surf_mc_visited > 0 || strcmp(_surf_mc_property_file,""))
+ if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,""))
snapshot->stacks = take_snapshot_stacks(heap);
free_memory_map(maps);
static int is_visited_state(){
- if(_surf_mc_visited == 0)
+ if(_sg_mc_visited == 0)
return 0;
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
}
}
- if(xbt_dynar_length(visited_states) == _surf_mc_visited){
+ if(xbt_dynar_length(visited_states) == _sg_mc_visited){
mc_snapshot_t state_to_remove = NULL;
xbt_dynar_shift(visited_states, &state_to_remove);
MC_free_snapshot(state_to_remove);
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
- if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
+ if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
(req = MC_state_get_request(state, &value))) {
/* Debug information */
}
}
- if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
+ if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
next_state->system_state = MC_take_snapshot();
}
/* The interleave set is empty or the maximum depth is reached, let's back-track */
} else {
- if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth)
+ if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
else
XBT_DEBUG("There are no more processes to interleave.");
if (MC_state_interleave_size(state)) {
/* We found a back-tracking point, let's loop */
- if(_surf_mc_checkpoint){
+ if(_sg_mc_checkpoint){
if(state->system_state != NULL){
MC_restore_snapshot(state->system_state);
xbt_fifo_unshift(mc_stack_safety, state);
/* Configuration support */
e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
+int _sg_do_model_check = 0;
+int _sg_mc_checkpoint=0;
+char* _sg_mc_property_file=NULL;
+int _sg_mc_timeout=0;
+int _sg_mc_max_depth=1000;
+int _sg_mc_visited=0;
+
extern int _sg_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
if (_sg_init_status && !_sg_do_model_check) {
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.");
}
- _surf_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
+ _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_property(const char *name, int pos) {
if (_sg_init_status && !_sg_do_model_check) {
xbt_die("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.");
}
- _surf_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
+ _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
}
void _mc_cfg_cb_timeout(const char *name, int pos) {
if (_sg_init_status && !_sg_do_model_check) {
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 --cfg=model-check:1). This won't work, sorry.");
}
- _surf_mc_timeout= xbt_cfg_get_int(_sg_cfg_set, name);
+ _sg_mc_timeout= xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_max_depth(const char *name, int pos) {
if (_sg_init_status && !_sg_do_model_check) {
xbt_die("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.");
}
- _surf_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
+ _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_visited(const char *name, int pos) {
if (_sg_init_status && !_sg_do_model_check) {
xbt_die("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.");
}
- _surf_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
+ _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
}
static void MC_get_global_variables(char *elf_file);
void MC_do_the_modelcheck_for_real() {
- if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
+ if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
if (mc_reduce_kind==e_mc_reduce_unset)
mc_reduce_kind=e_mc_reduce_dpor;
if (mc_reduce_kind==e_mc_reduce_unset)
mc_reduce_kind=e_mc_reduce_none;
- XBT_INFO("Check the liveness property %s",_surf_mc_property_file);
- MC_automaton_load(_surf_mc_property_file);
+ XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
+ MC_automaton_load(_sg_mc_property_file);
MC_modelcheck_liveness();
}
}
MC_UNSET_RAW_MEM;
- if(_surf_mc_visited > 0){
+ if(_sg_mc_visited > 0){
MC_init();
}else{
MC_SET_RAW_MEM;
MC_show_stack_safety(stack);
- if(!_surf_mc_checkpoint){
+ if(!_sg_mc_checkpoint){
mc_state_t state;
int visited(xbt_state_t st){
- if(_surf_mc_visited == 0)
+ if(_sg_mc_visited == 0)
return 0;
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
}
}
- if(xbt_dynar_length(visited_pairs) == _surf_mc_visited){
+ if(xbt_dynar_length(visited_pairs) == _sg_mc_visited){
xbt_dynar_remove_at(visited_pairs, 0, NULL);
}
mc_pair_stateless_t remove_pair;
mc_pair_reached_t remove_pair_reached;
- if(xbt_fifo_size(mc_stack_liveness) < _surf_mc_max_depth){
+ if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
if(current_pair->requests > 0){
}
- if(xbt_fifo_size(mc_stack_liveness) == _surf_mc_max_depth ){
+ if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
}else{
XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
/********************************** Configuration of MC **************************************/
extern xbt_fifo_t mc_stack_safety;
-extern int _surf_mc_checkpoint;
-extern char* _surf_mc_property_file;
-extern int _surf_mc_timeout;
-extern int _surf_mc_max_depth;
-extern int _surf_mc_visited;
-
/****** Core dump ******/
int create_dump(int pair);
* communication is not ready, it can timeout and won't block.
* On the other hand if it hasn't a timeout, check if the comm is ready.*/
if(simcall_comm_wait__get__timeout(req) >= 0){
- if(_surf_mc_timeout == 1){
+ if(_sg_mc_timeout == 1){
return TRUE;
}else{
act = simcall_comm_wait__get__comm(req);
#include "xbt/log.h"
#include "xbt/mallocator.h"
#include "xbt/str.h"
-#include "surf/surf_private.h"
-#include "surf/surf_routing.h" /* COORD_HOST_LEVEL and COORD_ASR_LEVEL */
+#include "xbt/lib.h"
+#include "xbt/sysdep.h"
+#include "surf/surf.h"
+#include "surf/maxmin.h"
+#include "instr/instr_interface.h"
#include "simgrid/simix.h"
#include "simgrid/sg_config.h"
#include "mc/mc.h"
xbt_cfg_t _sg_cfg_set = NULL;
-int _sg_do_model_check = 0;
-int _surf_mc_checkpoint=0;
-char* _surf_mc_property_file=NULL;
-int _surf_mc_timeout=0;
-int _surf_mc_max_depth=1000;
-int _surf_mc_visited=0;
-
int _sg_init_status = 0; /* 0: beginning of time (config cannot be changed yet);
1: initialized: cfg_set created (config can now be changed);
2: configured: command line parsed and config part of platform file was integrated also, platform construction ongoing or done.
}
}
-static void _sg_cfg_cb_surf_nthreads(const char *name, int pos)
-{
- surf_set_nthreads(xbt_cfg_get_int(_sg_cfg_set, name));
-}
-
static void _sg_cfg_cb__surf_network_coordinates(const char *name,
int pos)
{
}
}
+static void _sg_cfg_cb_surf_nthreads(const char *name, int pos)
+{
+ surf_set_nthreads(xbt_cfg_get_int(_sg_cfg_set, name));
+}
+
static void _sg_cfg_cb__surf_network_crosstraffic(const char *name,
int pos)
{
#define NO_MAX_DURATION -1.0
-/* user-visible parameters */
-extern double sg_tcp_gamma;
-extern double sg_sender_gap;
-extern double sg_latency_factor;
-extern double sg_bandwidth_factor;
-extern double sg_weight_S_parameter;
-extern int sg_maxmin_selective_update;
-extern int sg_network_crosstraffic;
-#ifdef HAVE_GTNETS
-extern double sg_gtnets_jitter;
-extern int sg_gtnets_jitter_seed;
-#endif
-
extern xbt_dict_t watched_hosts_lib;
extern const char *surf_action_state_names[6];
FILE *surf_fopen(const char *name, const char *mode);
extern tmgr_history_t history;
-extern xbt_dynar_t surf_path;
//void surf_config_init(int *argc, char **argv);
//void surf_config_finalize(void);
int net_get_link_latency_limited(surf_action_t action);
#endif
-/*
- * Returns the initial path. On Windows the initial path is
- * the current directory for the current process in the other
- * case the function returns "./" that represents the current
- * directory on Unix/Linux platforms.
- */
-const char *__surf_get_initial_path(void);
-
/* The __surf_is_absolute_file_path() returns 1 if
* file_path is a absolute file path, in the other
* case the function returns 0.