model-checker : forget file

[simgrid.git] / src / mc / mc_private.h

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 20e4ab8..e7a2703 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -21,6 +21,7 @@
 #include "xbt/function_types.h"
 #include "xbt/mmalloc.h"
 #include "../simix/smx_private.h"
+#include "../xbt/mmalloc/mmprivate.h"
 #include "xbt/automaton.h"
 #include "xbt/hash.h"
 #include "msg/msg.h"
@@ -48,6 +49,8 @@ typedef struct s_mc_snapshot{
   size_t heap_bytes_used;
   mc_mem_region_t regions[NB_REGIONS];
   int nb_processes;
+  mc_mem_region_t* privatization_regions;
+  int privatization_index;
   size_t *stack_sizes;
   xbt_dynar_t stacks;
   xbt_dynar_t to_ignore;
@@ -90,6 +93,13 @@ typedef struct s_mc_checkpoint_ignore_region{
   size_t size;
 }s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
 
+inline static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
+  if(snapshot==NULL)
+    xbt_die("snapshot is NULL");
+  xbt_mheap_t heap = (xbt_mheap_t)snapshot->regions[0]->data;
+  return heap->breakval;
+}
+
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
 mc_snapshot_t MC_take_snapshot(int num_state);
 void MC_restore_snapshot(mc_snapshot_t);
@@ -138,9 +148,11 @@ void MC_wait_for_requests(void);
 void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
-void MC_init(void);
 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max);
 
+extern xbt_fifo_t mc_stack;
+int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
+
 
 /********************************* Requests ***********************************/
 
@@ -157,6 +169,8 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value);
 
 /******************************** States **************************************/
 
+extern mc_global_t initial_global_state;
+
 /* Possible exploration status of a process in a state */
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */
@@ -219,7 +233,7 @@ void MC_print_statistics(mc_stats_t);
 /* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */
 
 extern void *std_heap;
-extern void *raw_heap;
+extern void *mc_heap;
 
 
 /* FIXME: Horrible hack! because the mmalloc library doesn't provide yet of */
@@ -234,8 +248,8 @@ extern void *raw_heap;
 /*   size_t bytes_free;            /\* Byte total of chunks in the free list. *\/ */
 /* }; */
 
-#define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
-#define MC_UNSET_RAW_MEM  mmalloc_set_current_heap(std_heap)
+#define MC_SET_MC_HEAP    mmalloc_set_current_heap(mc_heap)
+#define MC_SET_STD_HEAP  mmalloc_set_current_heap(std_heap)
 
 
 /******************************* MEMORY MAPPINGS ***************************/
@@ -293,7 +307,7 @@ void print_comparison_times(void);
 //#define MC_DEBUG 1
 #define MC_VERBOSE 1
 
-/********************************** DPOR for safety property **************************************/
+/********************************** Safety verification **************************************/
 
 typedef enum {
   e_mc_reduce_unset,
@@ -302,12 +316,10 @@ typedef enum {
 } e_mc_reduce_t;
 
 extern e_mc_reduce_t mc_reduce_kind;
-extern mc_global_t initial_state_safety;
-extern xbt_fifo_t mc_stack_safety;
 extern xbt_dict_t first_enabled_state;
 
-void MC_dpor_init(void);
-void MC_dpor(void);
+void MC_pre_modelcheck_safety(void);
+void MC_modelcheck_safety(void);
 
 typedef struct s_mc_visited_state{
   mc_snapshot_t system_state;
@@ -317,13 +329,14 @@ typedef struct s_mc_visited_state{
   int other_num; // dot_output for
 }s_mc_visited_state_t, *mc_visited_state_t;
 
+extern xbt_dynar_t visited_states;
+int is_visited_state(void);
+void visited_state_free(mc_visited_state_t state);
+void visited_state_free_voidp(void *s);
 
-/********************************** Double-DFS for liveness property **************************************/
+/********************************** Liveness verification **************************************/
 
-extern xbt_fifo_t mc_stack_liveness;
-extern mc_global_t initial_state_liveness;
 extern xbt_automaton_t _mc_property_automaton;
-extern int compare;
 
 typedef struct s_mc_pair{
   int num;
@@ -353,11 +366,14 @@ void mc_pair_free_voidp(void *p);
 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
 void MC_visited_pair_delete(mc_visited_pair_t p);
 
-void MC_ddfs_init(void);
-void MC_ddfs(void);
+void MC_pre_modelcheck_liveness(void);
+void MC_modelcheck_liveness(void);
 void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);
 
+extern xbt_dynar_t visited_pairs;
+int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
+
 
 /********************************** Variables with DWARF **********************************/
 
@@ -399,6 +415,7 @@ extern size_t mc_object_infos_size;
 
 void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
 void MC_post_process_types(mc_object_info_t info);
+void MC_post_process_object_info(mc_object_info_t info);
 
 // ***** Expressions
 
@@ -554,20 +571,21 @@ typedef struct s_mc_comm_pattern{
   int num;
   smx_action_t comm;
   e_smx_comm_type_t type;
-  int completed;
   unsigned long src_proc;
   unsigned long dst_proc;
   const char *src_host;
   const char *dst_host;
   char *rdv;
-  size_t data_size;
+  ssize_t data_size;
   void *data;
-  int matched_comm;
 }s_mc_comm_pattern_t, *mc_comm_pattern_t;
 
 extern xbt_dynar_t communications_pattern;
+extern xbt_dynar_t incomplete_communications_pattern;
 
 void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
+void MC_pre_modelcheck_comm_determinism(void);
 
 /* *********** Sets *********** */