src/mc/private.h

   1 /*      $Id: private.h 5497 2008-05-26 12:19:15Z cristianrosa $  */
   2
   3 /* Copyright (c) 2007 Arnaud Legrand, Bruno Donnassolo.
   4    All rights reserved.                                          */
   5
   6 /* This program is free software; you can redistribute it and/or modify it
   7  * under the terms of the license (GNU LGPL) which comes with this package. */
   8
   9 #ifndef MC_PRIVATE_H
  10 #define MC_PRIVATE_H
  11
  12 #include <stdio.h>
  13 #include "mc/mc.h"
  14 #include "mc/datatypes.h"
  15 #include "xbt/fifo.h"
  16 #include "xbt/setset.h"
  17 #include "xbt/config.h"
  18 #include "xbt/function_types.h"
  19 #include "xbt/mmalloc.h"
  20 #include "../simix/private.h"
  21
  22 /****************************** Snapshots ***********************************/
  23
  24 /*typedef struct s_mc_process_checkpoint {
  25         xbt_checkpoint_t machine_state;  Here we save the cpu + stack
  26 } s_mc_process_checkpoint_t, *mc_process_checkpoint_t;*/
  27
  28 typedef struct s_mc_snapshot {
  29   size_t heap_size;
  30   size_t data_size;
  31         void* data;
  32         void* heap;
  33
  34 } s_mc_snapshot_t, *mc_snapshot_t;
  35
  36 extern mc_snapshot_t initial_snapshot;
  37
  38 size_t MC_save_heap(void **);
  39 void MC_restore_heap(void *, size_t);
  40
  41 size_t MC_save_dataseg(void **);
  42 void MC_restore_dataseg(void *, size_t);
  43
  44 void MC_take_snapshot(mc_snapshot_t);
  45 void MC_restore_snapshot(mc_snapshot_t);
  46 void MC_free_snapshot(mc_snapshot_t);
  47
  48 /********************************* MC Global **********************************/
  49
  50 /* Bound of the MC depth-first search algorithm */
  51 #define MAX_DEPTH 1000
  52
  53 extern char mc_replay_mode;
  54
  55 void MC_show_stack(xbt_fifo_t stack);
  56 void MC_dump_stack(xbt_fifo_t stack);
  57 void MC_execute_surf_actions(void);
  58 void MC_replay(xbt_fifo_t stack);
  59 void MC_schedule_enabled_processes(void);
  60 void MC_dfs_init(void);
  61 void MC_dpor_init(void);
  62 void MC_dfs(void);
  63 void MC_dpor(void);
  64 void MC_dfs_exit(void);
  65 void MC_dpor_exit(void);
  66
  67
  68
  69 /******************************* Transitions **********************************/
  70 typedef enum {
  71   mc_isend,
  72   mc_irecv,
  73   mc_test,
  74   mc_wait,
  75   mc_waitany,
  76   mc_random
  77 } mc_trans_type_t;
  78
  79 typedef struct s_mc_transition{
  80   XBT_SETSET_HEADERS;
  81   char* name;
  82   smx_process_t process;
  83   mc_trans_type_t type;
  84
  85   union {
  86     struct {
  87       smx_rdv_t rdv;
  88     } isend;
  89
  90     struct {
  91       smx_rdv_t rdv;
  92     } irecv;
  93
  94     struct {
  95       smx_comm_t comm;
  96     } wait;
  97
  98     struct {
  99       smx_comm_t comm;
 100     } test;
 101
 102     struct {
 103       xbt_dynar_t comms;
 104     } waitany;
 105
 106     struct {
 107       int value;
 108     } random;
 109   };
 110 } s_mc_transition_t;
 111
 112 mc_transition_t MC_trans_isend_new(smx_rdv_t);
 113 mc_transition_t MC_trans_irecv_new(smx_rdv_t);
 114 mc_transition_t MC_trans_wait_new(smx_comm_t);
 115 mc_transition_t MC_trans_test_new(smx_comm_t);
 116 mc_transition_t MC_trans_waitany_new(xbt_dynar_t);
 117 mc_transition_t MC_trans_random_new(int);
 118 void MC_transition_delete(mc_transition_t);
 119 int MC_transition_depend(mc_transition_t, mc_transition_t);
 120 void MC_trans_compute_enabled(xbt_setset_set_t, xbt_setset_set_t);
 121
 122 /******************************** States **************************************/
 123 typedef struct mc_state{
 124   xbt_setset_set_t created_transitions;   /* created in this state */
 125   xbt_setset_set_t transitions;           /* created in this state + inherited */
 126   xbt_setset_set_t enabled_transitions;   /* they can be executed by the mc */
 127   xbt_setset_set_t interleave;            /* the ones to be executed by the mc */
 128   xbt_setset_set_t done;                  /* already executed transitions */
 129   mc_transition_t executed_transition;    /* last executed transition */
 130 } s_mc_state_t, *mc_state_t;
 131
 132 extern xbt_fifo_t mc_stack;
 133 extern xbt_setset_t mc_setset;
 134 extern mc_state_t mc_current_state;
 135
 136 mc_state_t MC_state_new(void);
 137 void MC_state_delete(mc_state_t);
 138
 139 /****************************** Statistics ************************************/
 140 typedef struct mc_stats{
 141   unsigned long state_size;
 142   unsigned long visited_states;
 143   unsigned long expanded_states;
 144   unsigned long executed_transitions;
 145 }s_mc_stats_t, *mc_stats_t;
 146
 147 extern mc_stats_t mc_stats;
 148
 149 void MC_print_statistics(mc_stats_t);
 150
 151 /********************************** MEMORY ******************************/
 152 /* The possible memory modes for the modelchecker are standard and raw. */
 153 /* Normally the system should operate in std, for switching to raw mode */
 154 /* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */
 155
 156 extern void *std_heap;
 157 extern void *raw_heap;
 158 extern void *libsimgrid_data_addr_start;
 159 extern size_t libsimgrid_data_size;
 160
 161 #define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
 162 #define MC_UNSET_RAW_MEM    mmalloc_set_current_heap(std_heap)
 163
 164 /******************************* MEMORY MAPPINGS ***************************/
 165 /* These functions and data structures implements a binary interface for   */
 166 /* the proc maps ascii interface                                           */
 167
 168 #define MAP_READ   1 << 0
 169 #define MAP_WRITE  1 << 1
 170 #define MAP_EXEC   1 << 2
 171 #define MAP_SHARED 1 << 3
 172 #define MAP_PRIV   1 << 4
 173
 174 /* Each field is defined as documented in proc's manual page  */
 175 typedef struct s_map_region {
 176
 177   void *start_addr;     /* Start address of the map */
 178   void *end_addr;       /* End address of the map */
 179   int perms;            /* Set of permissions */
 180   void *offset;         /* Offset in the file/whatever */
 181   char dev_major;       /* Major of the device */
 182   char dev_minor;       /* Minor of the device */
 183   unsigned long inode;  /* Inode in the device */
 184   char *pathname;       /* Path name of the mapped file */
 185
 186 } s_map_region;
 187
 188 typedef struct s_memory_map {
 189
 190   s_map_region *regions;  /* Pointer to an array of regions */
 191   int mapsize;            /* Number of regions in the memory */
 192
 193 } s_memory_map_t, *memory_map_t;
 194
 195 memory_map_t get_memory_map(void);
 196
 197
 198 #endif