1 /* $Id: private.h 5497 2008-05-26 12:19:15Z cristianrosa $ */
3 /* Copyright (c) 2007 Arnaud Legrand, Bruno Donnassolo.
4 All rights reserved. */
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. */
14 #include "mc/datatypes.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"
22 /****************************** Snapshots ***********************************/
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;*/
28 typedef struct s_mc_snapshot {
34 } s_mc_snapshot_t, *mc_snapshot_t;
36 extern mc_snapshot_t initial_snapshot;
38 size_t MC_save_heap(void **);
39 void MC_restore_heap(void *, size_t);
41 size_t MC_save_dataseg(void **);
42 void MC_restore_dataseg(void *, size_t);
44 void MC_take_snapshot(mc_snapshot_t);
45 void MC_restore_snapshot(mc_snapshot_t);
46 void MC_free_snapshot(mc_snapshot_t);
48 /********************************* MC Global **********************************/
50 /* Bound of the MC depth-first search algorithm */
51 #define MAX_DEPTH 1000
53 extern char mc_replay_mode;
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);
64 void MC_dfs_exit(void);
65 void MC_dpor_exit(void);
69 /******************************* Transitions **********************************/
79 typedef struct s_mc_transition{
82 smx_process_t process;
114 mc_transition_t MC_trans_isend_new(smx_rdv_t);
115 mc_transition_t MC_trans_irecv_new(smx_rdv_t);
116 mc_transition_t MC_trans_wait_new(smx_comm_t);
117 mc_transition_t MC_trans_test_new(smx_comm_t);
118 mc_transition_t MC_trans_waitany_new(xbt_dynar_t);
119 mc_transition_t MC_trans_random_new(int, int);
120 void MC_transition_delete(mc_transition_t);
121 int MC_transition_depend(mc_transition_t, mc_transition_t);
122 void MC_trans_compute_enabled(xbt_setset_set_t, xbt_setset_set_t);
124 /******************************** States **************************************/
125 typedef struct mc_state{
126 xbt_setset_set_t created_transitions; /* created in this state */
127 xbt_setset_set_t transitions; /* created in this state + inherited */
128 xbt_setset_set_t enabled_transitions; /* they can be executed by the mc */
129 xbt_setset_set_t interleave; /* the ones to be executed by the mc */
130 xbt_setset_set_t done; /* already executed transitions */
131 mc_transition_t executed_transition; /* last executed transition */
132 } s_mc_state_t, *mc_state_t;
134 extern xbt_fifo_t mc_stack;
135 extern xbt_setset_t mc_setset;
136 extern mc_state_t mc_current_state;
138 mc_state_t MC_state_new(void);
139 void MC_state_delete(mc_state_t);
141 /****************************** Statistics ************************************/
142 typedef struct mc_stats{
143 unsigned long state_size;
144 unsigned long visited_states;
145 unsigned long expanded_states;
146 unsigned long executed_transitions;
147 }s_mc_stats_t, *mc_stats_t;
149 extern mc_stats_t mc_stats;
151 void MC_print_statistics(mc_stats_t);
153 /********************************** MEMORY ******************************/
154 /* The possible memory modes for the modelchecker are standard and raw. */
155 /* Normally the system should operate in std, for switching to raw mode */
156 /* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */
158 extern void *std_heap;
159 extern void *raw_heap;
160 extern void *libsimgrid_data_addr_start;
161 extern size_t libsimgrid_data_size;
163 #define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap)
164 #define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
166 /******************************* MEMORY MAPPINGS ***************************/
167 /* These functions and data structures implements a binary interface for */
168 /* the proc maps ascii interface */
170 #define MAP_READ 1 << 0
171 #define MAP_WRITE 1 << 1
172 #define MAP_EXEC 1 << 2
173 #define MAP_SHARED 1 << 3
174 #define MAP_PRIV 1 << 4
176 /* Each field is defined as documented in proc's manual page */
177 typedef struct s_map_region {
179 void *start_addr; /* Start address of the map */
180 void *end_addr; /* End address of the map */
181 int perms; /* Set of permissions */
182 void *offset; /* Offset in the file/whatever */
183 char dev_major; /* Major of the device */
184 char dev_minor; /* Minor of the device */
185 unsigned long inode; /* Inode in the device */
186 char *pathname; /* Path name of the mapped file */
190 typedef struct s_memory_map {
192 s_map_region *regions; /* Pointer to an array of regions */
193 int mapsize; /* Number of regions in the memory */
195 } s_memory_map_t, *memory_map_t;
197 memory_map_t get_memory_map(void);