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 struct s_mc_transition{
  71   XBT_SETSET_HEADERS;
  72   char* name;
  73   mc_trans_type_t type;
  74   smx_process_t process;
  75   smx_rdv_t rdv;
  76   smx_comm_t comm;          /* reference to the simix network communication */
  77
  78   /* Used only for random transitions */
  79   int min;                  /* min random value */
  80   int max;                  /* max random value */
  81   int current_value;        /* current value */
  82 } s_mc_transition_t;
  83
  84 void MC_random_create(int,int);
  85 void MC_transition_delete(mc_transition_t);
  86 int MC_transition_depend(mc_transition_t, mc_transition_t);
  87
  88 /******************************** States **************************************/
  89 typedef struct mc_state{
  90   xbt_setset_set_t created_transitions;   /* created in this state */
  91   xbt_setset_set_t transitions;           /* created in this state + inherited */
  92   xbt_setset_set_t enabled_transitions;   /* they can be executed by the mc */
  93   xbt_setset_set_t interleave;            /* the ones to be executed by the mc */
  94   xbt_setset_set_t done;                  /* already executed transitions */
  95   mc_transition_t executed_transition;    /* last executed transition */
  96 } s_mc_state_t, *mc_state_t;
  97
  98 extern xbt_fifo_t mc_stack;
  99 extern xbt_setset_t mc_setset;
 100 extern mc_state_t mc_current_state;
 101
 102 mc_state_t MC_state_new(void);
 103 void MC_state_delete(mc_state_t);
 104
 105 /****************************** Statistics ************************************/
 106 typedef struct mc_stats{
 107   unsigned long state_size;
 108   unsigned long visited_states;
 109   unsigned long expanded_states;
 110   unsigned long executed_transitions;
 111 }s_mc_stats_t, *mc_stats_t;
 112
 113 extern mc_stats_t mc_stats;
 114
 115 void MC_print_statistics(mc_stats_t);
 116
 117 /********************************** MEMORY ******************************/
 118 /* The possible memory modes for the modelchecker are standard and raw. */
 119 /* Normally the system should operate in std, for switching to raw mode */
 120 /* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */
 121
 122 extern void *std_heap;
 123 extern void *raw_heap;
 124 extern void *libsimgrid_data_addr_start;
 125 extern size_t libsimgrid_data_size;
 126
 127 #define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
 128 #define MC_UNSET_RAW_MEM    mmalloc_set_current_heap(std_heap)
 129
 130 /******************************* MEMORY MAPPINGS ***************************/
 131 /* These functions and data structures implements a binary interface for   */
 132 /* the proc maps ascii interface                                           */
 133
 134 #define MAP_READ   1 << 0
 135 #define MAP_WRITE  1 << 1
 136 #define MAP_EXEC   1 << 2
 137 #define MAP_SHARED 1 << 3
 138 #define MAP_PRIV   1 << 4
 139
 140 /* Each field is defined as documented in proc's manual page  */
 141 typedef struct s_map_region {
 142
 143   void *start_addr;     /* Start address of the map */
 144   void *end_addr;       /* End address of the map */
 145   int perms;            /* Set of permissions */
 146   void *offset;         /* Offset in the file/whatever */
 147   char dev_major;       /* Major of the device */
 148   char dev_minor;       /* Minor of the device */
 149   unsigned long inode;  /* Inode in the device */
 150   char *pathname;       /* Path name of the mapped file */
 151
 152 } s_map_region;
 153
 154 typedef struct s_memory_map {
 155
 156   s_map_region *regions;  /* Pointer to an array of regions */
 157   int mapsize;            /* Number of regions in the memory */
 158
 159 } s_memory_map_t, *memory_map_t;
 160
 161 memory_map_t get_memory_map(void);
 162
 163
 164 #endif