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