src/mc/mc_private.h

   1 /* Copyright (c) 2007-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 #ifndef MC_PRIVATE_H
   8 #define MC_PRIVATE_H
   9
  10 #include "simgrid_config.h"
  11 #include <stdio.h>
  12 #include <stdbool.h>
  13 #ifndef WIN32
  14 #include <sys/mman.h>
  15 #endif
  16 #include <elfutils/libdw.h>
  17
  18 #include "mc/mc.h"
  19 #include "mc_base.h"
  20 #include "mc/datatypes.h"
  21 #include "xbt/fifo.h"
  22 #include "xbt/config.h"
  23 #include "xbt/function_types.h"
  24 #include "xbt/mmalloc.h"
  25 #include "../simix/smx_private.h"
  26 #include "../xbt/mmalloc/mmprivate.h"
  27 #include "xbt/automaton.h"
  28 #include "xbt/hash.h"
  29 #include "msg/msg.h"
  30 #include "msg/datatypes.h"
  31 #include "xbt/strbuff.h"
  32 #include "xbt/parmap.h"
  33
  34 #include "mc_forward.h"
  35 #include "mc_mmu.h"
  36 #include "mc_page_store.h"
  37 #include "mc_interface.h"
  38 #include "mc_mmalloc.h"
  39 #include "mc_model_checker.h"
  40 #include "mc_snapshot.h"
  41 #include "mc_object_info.h"
  42 #include "mc_location.h"
  43 #include "mc_state.h"
  44 #include "mc_comm_pattern.h"
  45 #include "mc_request.h"
  46 #include "mc_safety.h"
  47 #include "mc_liveness.h"
  48 #include "mc_memory_map.h"
  49
  50 SG_BEGIN_DECL()
  51
  52 typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t;
  53
  54 /****************************** Snapshots ***********************************/
  55
  56 extern xbt_dynar_t mc_checkpoint_ignore;
  57
  58 /********************************* MC Global **********************************/
  59
  60 extern FILE *dot_output;
  61 extern const char* colors[13];
  62 extern xbt_parmap_t parmap;
  63
  64 extern int user_max_depth_reached;
  65
  66 int MC_deadlock_check(void);
  67 void MC_replay(xbt_fifo_t stack, int start);
  68 void MC_replay_liveness(xbt_fifo_t stack, int all_stack);
  69 void MC_show_deadlock(smx_simcall_t req);
  70 void MC_show_stack_safety(xbt_fifo_t stack);
  71 void MC_dump_stack_safety(xbt_fifo_t stack);
  72
  73 /** Stack (of `mc_state_t`) representing the current position of the
  74  *  the MC in the exploration graph
  75  *
  76  *  It is managed by its head (`xbt_fifo_shift` and `xbt_fifo_unshift`).
  77  */
  78 extern xbt_fifo_t mc_stack;
  79
  80 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
  81
  82
  83 /****************************** Statistics ************************************/
  84
  85 typedef struct mc_stats {
  86   unsigned long state_size;
  87   unsigned long visited_states;
  88   unsigned long visited_pairs;
  89   unsigned long expanded_states;
  90   unsigned long expanded_pairs;
  91   unsigned long executed_transitions;
  92 } s_mc_stats_t, *mc_stats_t;
  93
  94 extern mc_stats_t mc_stats;
  95
  96 void MC_print_statistics(mc_stats_t stats);
  97
  98 extern char *libsimgrid_path;
  99
 100 /********************************** Snapshot comparison **********************************/
 101
 102 typedef struct s_mc_comparison_times{
 103   double nb_processes_comparison_time;
 104   double bytes_used_comparison_time;
 105   double stacks_sizes_comparison_time;
 106   double binary_global_variables_comparison_time;
 107   double libsimgrid_global_variables_comparison_time;
 108   double heap_comparison_time;
 109   double stacks_comparison_time;
 110 }s_mc_comparison_times_t, *mc_comparison_times_t;
 111
 112 extern __thread mc_comparison_times_t mc_comp_times;
 113 extern __thread double mc_snapshot_comparison_time;
 114
 115 int snapshot_compare(void *state1, void *state2);
 116 void print_comparison_times(void);
 117
 118 //#define MC_DEBUG 1
 119 #define MC_VERBOSE 1
 120
 121 /********************************** Variables with DWARF **********************************/
 122
 123 dw_frame_t MC_find_function_by_ip(void* ip);
 124 mc_object_info_t MC_ip_find_object_info(void* ip);
 125
 126 void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
 127
 128 /********************************** Miscellaneous **********************************/
 129
 130 typedef struct s_local_variable{
 131   dw_frame_t subprogram;
 132   unsigned long ip;
 133   char *name;
 134   dw_type_t type;
 135   void *address;
 136   int region;
 137 }s_local_variable_t, *local_variable_t;
 138
 139 /* *********** Sets *********** */
 140
 141 typedef struct s_mc_address_set *mc_address_set_t;
 142
 143 mc_address_set_t mc_address_set_new();
 144 void mc_address_set_free(mc_address_set_t* p);
 145 void mc_address_add(mc_address_set_t p, const void* value);
 146 bool mc_address_test(mc_address_set_t p, const void* value);
 147
 148 /* *********** Hash *********** */
 149
 150 /** \brief Hash the current state
 151  *  \param num_state number of states
 152  *  \param stacks stacks (mc_snapshot_stak_t) used fot the stack unwinding informations
 153  *  \result resulting hash
 154  * */
 155 uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
 156
 157 /* *********** Snapshot *********** */
 158
 159 #define MC_LOG_REQUEST(log, req, value) \
 160   if (XBT_LOG_ISENABLED(log, xbt_log_priority_debug)) { \
 161     char* req_str = MC_request_to_string(req, value); \
 162     XBT_DEBUG("Execute: %s", req_str); \
 163     xbt_free(req_str); \
 164   }
 165
 166 /** @brief Dump the stacks of the application processes
 167  *
 168  *   This functions is currently not used but it is quite convenient
 169  *   to call from the debugger.
 170  *
 171  *   Does not work when an application thread is running.
 172  */
 173 void MC_dump_stacks(FILE* file);
 174
 175 SG_END_DECL()
 176
 177 #endif