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);
65 /******************************* Transitions **********************************/
66 typedef struct s_mc_transition{
69 unsigned int refcount;
71 smx_process_t process;
73 smx_comm_t comm; /* reference to the simix network communication */
76 void MC_transition_delete(mc_transition_t);
77 int MC_transition_depend(mc_transition_t, mc_transition_t);
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;
88 extern xbt_fifo_t mc_stack;
89 extern xbt_setset_t mc_setset;
91 mc_state_t MC_state_new(void);
92 void MC_state_delete(mc_state_t);
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;
102 extern mc_stats_t mc_stats;
104 void MC_print_statistics(mc_stats_t);
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 */
111 extern void *std_heap;
112 extern void *raw_heap;
113 extern void *libsimgrid_data_addr_start;
114 extern size_t libsimgrid_data_size;
116 #define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap)
117 #define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
119 /******************************* MEMORY MAPPINGS ***************************/
120 /* These functions and data structures implements a binary interface for */
121 /* the proc maps ascii interface */
123 #define MAP_READ 1 << 0
124 #define MAP_WRITE 1 << 1
125 #define MAP_EXEC 1 << 2
126 #define MAP_SHARED 1 << 3
127 #define MAP_PRIV 1 << 4
129 /* Each field is defined as documented in proc's manual page */
130 typedef struct s_map_region {
132 void *start_addr; /* Start address of the map */
133 void *end_addr; /* End address of the map */
134 int perms; /* Set of permissions */
135 void *offset; /* Offset in the file/whatever */
136 char dev_major; /* Major of the device */
137 char dev_minor; /* Minor of the device */
138 unsigned long inode; /* Inode in the device */
139 char *pathname; /* Path name of the mapped file */
143 typedef struct s_memory_map {
145 s_map_region *regions; /* Pointer to an array of regions */
146 int mapsize; /* Number of regions in the memory */
148 } s_memory_map_t, *memory_map_t;
150 memory_map_t get_memory_map(void);