[mc] Cross-process access to smx_process and simcall

Process and host names are not handled yet.

diff --git a/include/xbt/dynar.h b/include/xbt/dynar.h
index 823dd41..31b5adb 100644 (file)
--- a/include/xbt/dynar.h
+++ b/include/xbt/dynar.h
@@ -284,6 +284,11 @@ xbt_dynar_foreach (dyn,cpt,str) {
       _xbt_dynar_cursor_get(_dynar,_cursor,&_data) ; \
             (_cursor)++         )
 
       _xbt_dynar_cursor_get(_dynar,_cursor,&_data) ; \
             (_cursor)++         )
 

+#define xbt_dynar_foreach_ptr(_dynar,_cursor,_ptr) \
+       for (_xbt_dynar_cursor_first(_dynar,&(_cursor))       ; \
+      (_ptr = _cursor < _dynar->used ? xbt_dynar_get_ptr(_dynar,_cursor) : NULL) ; \
+            (_cursor)++         )
+

 /** @} */
 
 SG_END_DECL()
 /** @} */
 
 SG_END_DECL()

diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c
index 96c14b2..20d8f43 100644 (file)
--- a/src/mc/mc_base.c
+++ b/src/mc/mc_base.c
@@ -13,6 +13,7 @@
 #ifdef HAVE_MC
 #include "mc_process.h"
 #include "mc_model_checker.h"
 #ifdef HAVE_MC
 #include "mc_process.h"
 #include "mc_model_checker.h"

+#include "mc_protocol.h"

 #endif
 
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 #endif
 
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");


@@ -37,6 +38,9 @@ int MC_request_is_enabled(smx_simcall_t req)
 {
   unsigned int index = 0;
   smx_synchro_t act = 0;
 {
   unsigned int index = 0;
   smx_synchro_t act = 0;

+#ifdef HAVE_MC
+  s_smx_synchro_t temp_synchro;
+#endif

 
   switch (req->call) {
   case SIMCALL_NONE:
 
   switch (req->call) {
   case SIMCALL_NONE:


@@ -45,6 +49,17 @@ int MC_request_is_enabled(smx_simcall_t req)
   case SIMCALL_COMM_WAIT:
     /* FIXME: check also that src and dst processes are not suspended */
     act = simcall_comm_wait__get__comm(req);
   case SIMCALL_COMM_WAIT:
     /* FIXME: check also that src and dst processes are not suspended */
     act = simcall_comm_wait__get__comm(req);

+
+#ifdef HAVE_MC
+    // Fetch from MCed memory:
+    if (!MC_process_is_self(&mc_model_checker->process)) {
+      MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+        &temp_synchro, act, sizeof(temp_synchro),
+        MC_PROCESS_INDEX_ANY);
+      act = &temp_synchro;
+    }
+#endif
+

     if (simcall_comm_wait__get__timeout(req) >= 0) {
       /* If it has a timeout it will be always be enabled, because even if the
        * communication is not ready, it can timeout and won't block. */
     if (simcall_comm_wait__get__timeout(req) >= 0) {
       /* If it has a timeout it will be always be enabled, because even if the
        * communication is not ready, it can timeout and won't block. */


@@ -60,9 +75,21 @@ int MC_request_is_enabled(smx_simcall_t req)
 
   case SIMCALL_COMM_WAITANY:
     /* Check if it has at least one communication ready */
 
   case SIMCALL_COMM_WAITANY:
     /* Check if it has at least one communication ready */

-    xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act)
+    xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+
+#ifdef HAVE_MC
+      // Fetch from MCed memory:
+      if (!MC_process_is_self(&mc_model_checker->process)) {
+        MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+          &temp_synchro, act, sizeof(temp_synchro),
+          MC_PROCESS_INDEX_ANY);
+        act = &temp_synchro;
+      }
+#endif
+

       if (act->comm.src_proc && act->comm.dst_proc)
         return TRUE;
       if (act->comm.src_proc && act->comm.dst_proc)
         return TRUE;

+    }

     return FALSE;
 
   default:
     return FALSE;
 
   default:

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 1fdf717..0a5d94e 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -737,11 +737,10 @@ mc_snapshot_t MC_take_snapshot(int num_state)
   snapshot->address_space.address_space_class = &mc_snapshot_class;
 
   snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
   snapshot->address_space.address_space_class = &mc_snapshot_class;
 
   snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);

+

   smx_process_t process;
   smx_process_t process;

-  // FIXME, cross-process support (simix_global->process_list)
-  xbt_swag_foreach(process, simix_global->process_list) {
-    xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid);
-  }
+  MC_EACH_SIMIX_PROCESS(process,
+    xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid));

 
   MC_snapshot_handle_ignore(snapshot);
 
 
   MC_snapshot_handle_ignore(snapshot);
 

diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h
index 638a8ea..f5d01a5 100644 (file)
--- a/src/mc/mc_client.h
+++ b/src/mc/mc_client.h
@@ -23,8 +23,9 @@ void MC_client_hello(void);
 void MC_client_handle_messages(void);
 void MC_client_send_message(void* message, size_t size);
 
 void MC_client_handle_messages(void);
 void MC_client_send_message(void* message, size_t size);
 

+#ifdef HAVE_MC

 void MC_ignore(void* addr, size_t size);
 void MC_ignore(void* addr, size_t size);

-
+#endif

 
 SG_END_DECL()
 
 
 SG_END_DECL()
 

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 6576d60..d892dde 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -165,12 +165,14 @@ static void print_incomplete_communications_pattern(){
   }
 }
 
   }
 }
 

+// FIXME, remote comm

 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
 {
   mc_process_t process = &mc_model_checker->process;
   void *addr_pointed;
   comm_pattern->src_proc = comm->comm.src_proc->pid;
   comm_pattern->dst_proc = comm->comm.dst_proc->pid;
 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
 {
   mc_process_t process = &mc_model_checker->process;
   void *addr_pointed;
   comm_pattern->src_proc = comm->comm.src_proc->pid;
   comm_pattern->dst_proc = comm->comm.dst_proc->pid;

+  // FIXME, get remote host name

   comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
   comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
   if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {
   comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
   comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
   if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {


@@ -216,7 +218,7 @@ void list_comm_pattern_free_voidp(void *p) {
   list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
 }
 
   list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
 }
 

-void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type)
+void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const e_mc_call_type_t call_type)

 {
   mc_process_t process = &mc_model_checker->process;
   mc_comm_pattern_t pattern = NULL;
 {
   mc_process_t process = &mc_model_checker->process;
   mc_comm_pattern_t pattern = NULL;


@@ -224,7 +226,13 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t
   pattern->data_size = -1;
   pattern->data = NULL;
 
   pattern->data_size = -1;
   pattern->data = NULL;
 

-  pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t));
+  const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, request);
+  mc_list_comm_pattern_t initial_pattern =
+    (mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+  xbt_dynar_t incomplete_pattern =
+    (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+  pattern->index =
+    initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);

   
   void *addr_pointed;
   
   
   void *addr_pointed;
   


@@ -234,7 +242,8 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t
     pattern->comm = simcall_comm_isend__get__result(request);
     pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
     pattern->src_proc = pattern->comm->comm.src_proc->pid;
     pattern->comm = simcall_comm_isend__get__result(request);
     pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
     pattern->src_proc = pattern->comm->comm.src_proc->pid;

-    pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
+    // FIXME, get remote host name
+    pattern->src_host = simcall_host_get_name(issuer->smx_host);

     if(pattern->comm->comm.src_buff != NULL){
       pattern->data_size = pattern->comm->comm.src_buff_size;
       pattern->data = xbt_malloc0(pattern->data_size);
     if(pattern->comm->comm.src_buff != NULL){
       pattern->data_size = pattern->comm->comm.src_buff_size;
       pattern->data = xbt_malloc0(pattern->data_size);


@@ -250,14 +259,15 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t
     pattern->comm = simcall_comm_irecv__get__result(request);
     pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
     pattern->comm = simcall_comm_irecv__get__result(request);
     pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;

-    pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
+    // FIXME, remote process access
+    pattern->dst_host = simcall_host_get_name(issuer->smx_host);

   } else {
     xbt_die("Unexpected call_type %i", (int) call_type);
   }
 
   } else {
     xbt_die("Unexpected call_type %i", (int) call_type);
   }
 

-  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern);
+  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);

 
 

-  XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid);
+  XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);

 }
 
 void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) {
 }
 
 void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) {


@@ -358,11 +368,11 @@ void MC_pre_modelcheck_comm_determinism(void)
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */

-  xbt_swag_foreach(process, simix_global->process_list) {
+  MC_EACH_SIMIX_PROCESS(process,

     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
     }
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
     }

-  }
+  );

 
   xbt_fifo_unshift(mc_stack, initial_state);
 
 
   xbt_fifo_unshift(mc_stack, initial_state);
 


@@ -417,7 +427,7 @@ void MC_modelcheck_comm_determinism(void)
       }
 
       /* Answer the request */
       }
 
       /* Answer the request */

-      SIMIX_simcall_handle(req, value);    /* After this call req is no longer useful */
+      MC_simcall_handle(req, value);    /* After this call req is no longer useful */

 
       MC_SET_MC_HEAP;
       if(!initial_global_state->initial_communications_pattern_done)
 
       MC_SET_MC_HEAP;
       if(!initial_global_state->initial_communications_pattern_done)


@@ -437,11 +447,11 @@ void MC_modelcheck_comm_determinism(void)
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */

-        xbt_swag_foreach(process, simix_global->process_list) {
+        MC_EACH_SIMIX_PROCESS(process,

           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
           }
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
           }

-        }
+        );

 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index d520ffb..0ea7c5f 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -336,12 +336,12 @@ int MC_deadlock_check()
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {
     deadlock = TRUE;
   smx_process_t process;
   if (xbt_swag_size(simix_global->process_list)) {
     deadlock = TRUE;

-    xbt_swag_foreach(process, simix_global->process_list) {
+    MC_EACH_SIMIX_PROCESS(process,

       if (MC_process_is_enabled(process)) {
         deadlock = FALSE;
         break;
       }
       if (MC_process_is_enabled(process)) {
         deadlock = FALSE;
         break;
       }

-    }
+    );

   }
   return deadlock;
 }
   }
   return deadlock;
 }


@@ -474,7 +474,9 @@ void MC_replay(xbt_fifo_t stack)
     if (saved_req) {
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */
     if (saved_req) {
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */

-      req = &saved_req->issuer->simcall;
+
+      const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+      req = &issuer->simcall;

 
       /* Debug information */
       if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 
       /* Debug information */
       if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {


@@ -488,7 +490,7 @@ void MC_replay(xbt_fifo_t stack)
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         call = mc_get_call_type(req);
 
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         call = mc_get_call_type(req);
 

-      SIMIX_simcall_handle(req, value);
+      MC_simcall_handle(req, value);

 
       MC_SET_MC_HEAP;
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 
       MC_SET_MC_HEAP;
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)


@@ -559,7 +561,8 @@ void MC_replay_liveness(xbt_fifo_t stack)
         if (saved_req != NULL) {
           /* because we got a copy of the executed request, we have to fetch the
              real one, pointed by the request field of the issuer process */
         if (saved_req != NULL) {
           /* because we got a copy of the executed request, we have to fetch the
              real one, pointed by the request field of the issuer process */

-          req = &saved_req->issuer->simcall;
+          const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+          req = &issuer->simcall;

 
           /* Debug information */
           if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 
           /* Debug information */
           if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {


@@ -570,7 +573,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
 
         }
 
 
         }
 

-        SIMIX_simcall_handle(req, value);
+        MC_simcall_handle(req, value);

         MC_wait_for_requests();
       }
 
         MC_wait_for_requests();
       }
 

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index ec50dad..07fbd74 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -201,11 +201,11 @@ void MC_pre_modelcheck_liveness(void) {
       initial_pair->depth = 1;
 
       /* Get enabled processes and insert them in the interleave set of the graph_state */
       initial_pair->depth = 1;
 
       /* Get enabled processes and insert them in the interleave set of the graph_state */

-      xbt_swag_foreach(process, simix_global->process_list) {
+      MC_EACH_SIMIX_PROCESS(process,

         if (MC_process_is_enabled(process)) {
           MC_state_interleave_process(initial_pair->graph_state, process);
         }
         if (MC_process_is_enabled(process)) {
           MC_state_interleave_process(initial_pair->graph_state, process);
         }

-      }
+      );

 
       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
       initial_pair->search_cycle = 0;
 
       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
       initial_pair->search_cycle = 0;


@@ -311,7 +311,7 @@ void MC_modelcheck_liveness()
            mc_stats->visited_pairs++;
 
          /* Answer the request */
            mc_stats->visited_pairs++;
 
          /* Answer the request */

-         SIMIX_simcall_handle(req, value);
+         MC_simcall_handle(req, value);

          
          /* Wait for requests (schedules processes) */
          MC_wait_for_requests();
          
          /* Wait for requests (schedules processes) */
          MC_wait_for_requests();


@@ -336,11 +336,11 @@ void MC_modelcheck_liveness()
               next_pair->atomic_propositions = get_atomic_propositions_values();
               next_pair->depth = current_pair->depth + 1;
               /* Get enabled processes and insert them in the interleave set of the next graph_state */
               next_pair->atomic_propositions = get_atomic_propositions_values();
               next_pair->depth = current_pair->depth + 1;
               /* Get enabled processes and insert them in the interleave set of the next graph_state */

-              xbt_swag_foreach(process, simix_global->process_list) {
+              MC_EACH_SIMIX_PROCESS(process,

                 if (MC_process_is_enabled(process)) {
                   MC_state_interleave_process(next_pair->graph_state, process);
                 }
                 if (MC_process_is_enabled(process)) {
                   MC_state_interleave_process(next_pair->graph_state, process);
                 }

-              }
+              );

 
               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 
 
               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 

diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h
index 308cf12..9c6b876 100644 (file)
--- a/src/mc/mc_model_checker.h
+++ b/src/mc/mc_model_checker.h
@@ -10,10 +10,12 @@
 #include <sys/types.h>
 
 #include <simgrid_config.h>
 #include <sys/types.h>
 
 #include <simgrid_config.h>

+#include <xbt/dynar.h>

 
 #include "mc_forward.h"
 #include "mc_process.h"
 #include "mc_page_store.h"
 
 #include "mc_forward.h"
 #include "mc_process.h"
 #include "mc_page_store.h"

+#include "mc_protocol.h"

 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 


@@ -37,6 +39,21 @@ struct s_mc_model_checker {
 mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
 void MC_model_checker_delete(mc_model_checker_t mc);
 
 mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
 void MC_model_checker_delete(mc_model_checker_t mc);
 

+#define MC_EACH_SIMIX_PROCESS(process, code) \
+  if (MC_process_is_self(&mc_model_checker->process)) { \
+    xbt_swag_foreach(process, simix_global->process_list) { \
+      code; \
+    } \
+  } else { \
+    MC_process_refresh_simix_processes(&mc_model_checker->process); \
+    unsigned int _smx_process_index; \
+    mc_smx_process_info_t _smx_process_info; \
+    xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, _smx_process_index, _smx_process_info) { \
+      smx_process_t process = &_smx_process_info->copy; \
+      code; \
+    } \
+  }
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c
index 65c77a8..0beaf82 100644 (file)
--- a/src/mc/mc_process.c
+++ b/src/mc/mc_process.c
@@ -26,6 +26,8 @@
 #include "mc_snapshot.h"
 #include "mc_ignore.h"
 
 #include "mc_snapshot.h"
 #include "mc_ignore.h"
 

+#include "simix/smx_private.h"
+

 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
                                 "MC process information");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
                                 "MC process information");
 


@@ -80,6 +82,9 @@ void MC_process_init(mc_process_t process, pid_t pid, int sockfd)
     &process->heap_address, std_heap_var->address, sizeof(struct mdesc*),
     MC_PROCESS_INDEX_DISABLED);
 
     &process->heap_address, std_heap_var->address, sizeof(struct mdesc*),
     MC_PROCESS_INDEX_DISABLED);
 

+  process->smx_process_infos = mc_smx_process_info_list_new();
+  process->smx_old_process_infos = mc_smx_process_info_list_new();
+

   process->checkpoint_ignore = MC_checkpoint_ignore_new();
 
   process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors  , __BYTE_ORDER);
   process->checkpoint_ignore = MC_checkpoint_ignore_new();
 
   process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors  , __BYTE_ORDER);


@@ -106,6 +111,9 @@ void MC_process_clear(mc_process_t process)
 
   xbt_dynar_free(&process->checkpoint_ignore);
 
 
   xbt_dynar_free(&process->checkpoint_ignore);
 

+  xbt_dynar_free(&process->smx_process_infos);
+  xbt_dynar_free(&process->smx_old_process_infos);
+

   size_t i;
   for (i=0; i!=process->object_infos_size; ++i) {
     MC_free_object_info(&process->object_infos[i]);
   size_t i;
   for (i=0; i!=process->object_infos_size; ++i) {
     MC_free_object_info(&process->object_infos[i]);


@@ -170,6 +178,66 @@ void MC_process_refresh_malloc_info(mc_process_t process)
     MC_PROCESS_INDEX_DISABLED);
 }
 
     MC_PROCESS_INDEX_DISABLED);
 }
 

+/** Load the remote swag of processes into a dynar
+ *
+ *  @param process     MCed process
+ *  @param target      Local dynar (to be filled with copies of `s_smx_process_t`)
+ *  @param remote_swag Address of the process SWAG in the remote list
+ */
+static void MC_process_refresh_simix_process_list(
+  mc_process_t process,
+  xbt_dynar_t target, xbt_swag_t remote_swag)
+{
+  // swag = REMOTE(*simix_global->process_list)
+  s_xbt_swag_t swag;
+  MC_process_read(process, MC_PROCESS_NO_FLAG, &swag, remote_swag, sizeof(swag),
+    MC_PROCESS_INDEX_ANY);
+
+  smx_process_t p;
+  xbt_dynar_reset(target);
+
+  int i = 0;
+  for (p = swag.head; p; ++i) {
+
+    s_mc_smx_process_info_t info;
+    info.address = p;
+    MC_process_read(process, MC_PROCESS_NO_FLAG,
+      &info.copy, p, sizeof(info.copy), MC_PROCESS_INDEX_ANY);
+    xbt_dynar_push(target, &info);
+
+    // Lookup next process address:
+    p = xbt_swag_getNext(&info.copy, swag.offset);
+  }
+  assert(i == swag.count);
+}
+
+void MC_process_refresh_simix_processes(mc_process_t process)
+{
+  if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
+    return;
+
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+  // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
+
+  // simix_global_p = REMOTE(simix_global);
+  smx_global_t simix_global_p;
+  MC_process_read_variable(process, "simix_global", &simix_global_p, sizeof(simix_global_p));
+
+  // simix_global = REMOTE(*simix_global)
+  s_smx_global_t simix_global;
+  MC_process_read(process, MC_PROCESS_NO_FLAG, &simix_global, simix_global_p, sizeof(simix_global),
+    MC_PROCESS_INDEX_ANY);
+
+  MC_process_refresh_simix_process_list(
+    process, process->smx_process_infos, simix_global.process_list);
+  MC_process_refresh_simix_process_list(
+    process, process->smx_old_process_infos, simix_global.process_to_destroy);
+
+  process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+  mmalloc_set_current_heap(heap);
+}
+

 #define SO_RE "\\.so[\\.0-9]*$"
 #define VERSION_RE "-[\\.0-9]*$"
 
 #define SO_RE "\\.so[\\.0-9]*$"
 #define VERSION_RE "-[\\.0-9]*$"
 


@@ -371,15 +439,37 @@ dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char*
 {
   const size_t n = process->object_infos_size;
   size_t i;
 {
   const size_t n = process->object_infos_size;
   size_t i;

+
+  // First lookup the variable in the executable shared object.
+  // A global variable used directly by the executable code from a library
+  // is reinstanciated in the executable memory .data/.bss.
+  // We need to look up the variable in the execvutable first.
+  if (process->binary_info) {
+    mc_object_info_t info = process->binary_info;
+    dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
+    if (var)
+      return var;
+  }
+

   for (i=0; i!=n; ++i) {
     mc_object_info_t info =process->object_infos[i];
     dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
     if (var)
       return var;
   }
   for (i=0; i!=n; ++i) {
     mc_object_info_t info =process->object_infos[i];
     dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name);
     if (var)
       return var;
   }

+

   return NULL;
 }
 
   return NULL;
 }
 

+void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size)
+{
+  dw_variable_t var = MC_process_find_variable_by_name(process, name);
+  if (!var->address)
+    xbt_die("No simple location for this variable");
+  MC_process_read(process, MC_PROCESS_NO_FLAG, target, var->address, size,
+    MC_PROCESS_INDEX_ANY);
+}
+

 // ***** Memory access
 
 int MC_process_vm_open(pid_t pid, int flags)
 // ***** Memory access
 
 int MC_process_vm_open(pid_t pid, int flags)


@@ -512,3 +602,72 @@ void MC_process_clear_memory(mc_process_t process, void* remote, size_t len)
     }
   }
 }
     }
   }
 }

+
+/** Get the issuer of a simcall (`req->issuer`)
+ *
+ *  In split-process mode, it does the black magic necessary to get an address
+ *  of a (shallow) copy of the data structure the issuer SIMIX process in the local
+ *  address space.
+ *
+ *  @param process the MCed process
+ *  @param req     the simcall (copied in the local process)
+ */
+smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req)
+{
+  if (MC_process_is_self(&mc_model_checker->process))
+    return req->issuer;
+
+  MC_process_refresh_simix_processes(process);
+
+  // This is the address of the smx_process in the MCed process:
+  void* address = req->issuer;
+
+  unsigned i;
+  mc_smx_process_info_t p;
+
+  xbt_dynar_foreach_ptr(process->smx_process_infos, i, p)
+    if (p->address == address)
+      return &p->copy;
+  xbt_dynar_foreach_ptr(process->smx_old_process_infos, i, p)
+    if (p->address == address)
+      return &p->copy;
+
+  xbt_die("Issuer not found");
+}
+
+void MC_simcall_handle(smx_simcall_t req, int value)
+{
+  if (MC_process_is_self(&mc_model_checker->process)) {
+    SIMIX_simcall_handle(req, value);
+    return;
+  }
+
+  MC_process_refresh_simix_processes(&mc_model_checker->process);
+
+  unsigned i;
+  mc_smx_process_info_t pi = NULL;
+
+  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+    smx_process_t p = (smx_process_t) pi->address;
+    if (req == &pi->copy.simcall) {
+      smx_simcall_t real_req = &p->simcall;
+      // TODO, use a remote call
+      SIMIX_simcall_handle(real_req, value);
+      return;
+    }
+  }
+
+  // Check (remove afterwards):
+  xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
+    smx_process_t p = (smx_process_t) pi->address;
+    if (req == &p->simcall)
+      xbt_die("The real simcall was passed. We expected the local copy.");
+  }
+
+  xbt_die("Could not find the request");
+}
+
+void mc_smx_process_info_clear(mc_smx_process_info_t p)
+{
+  // Nothing yet
+}

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 1e4384d..762cb69 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -18,11 +18,13 @@
 #include "xbt/mmalloc/mmprivate.h"
 
 #include "simix/popping_private.h"
 #include "xbt/mmalloc/mmprivate.h"
 
 #include "simix/popping_private.h"

+#include "simix/smx_private.h"

 
 #include "mc_forward.h"
 #include "mc_mmalloc.h" // std_heap
 #include "mc_memory_map.h"
 #include "mc_address_space.h"
 
 #include "mc_forward.h"
 #include "mc_mmalloc.h" // std_heap
 #include "mc_memory_map.h"
 #include "mc_address_space.h"

+#include "mc_protocol.h"

 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 


@@ -38,8 +40,16 @@ typedef enum {
 typedef enum {
   MC_PROCESS_CACHE_FLAG_HEAP = 1,
   MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2,
 typedef enum {
   MC_PROCESS_CACHE_FLAG_HEAP = 1,
   MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2,

+  MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4,

 } e_mc_process_cache_flags_t ;
 
 } e_mc_process_cache_flags_t ;
 

+struct s_mc_smx_process_info {
+  void* address;
+  struct s_smx_process copy;
+};
+
+typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t;
+

 /** Representation of a process
  */
 struct s_mc_process {
 /** Representation of a process
  */
 struct s_mc_process {


@@ -57,13 +67,13 @@ struct s_mc_process {
   size_t object_infos_size;
   int memory_file;
 
   size_t object_infos_size;
   int memory_file;
 

-  // Cache: don't use those fields directly but with the getters
-  // which ensure that proper synchronisation has been done.
+  xbt_dynar_t smx_process_infos;
+  xbt_dynar_t smx_old_process_infos;

 
 

+  /** State of the cache (which variables are up to date) */

   e_mc_process_cache_flags_t cache_flags;
 
   e_mc_process_cache_flags_t cache_flags;
 

-  /** Address of the heap structure in the target process.
-   */
+  /** Address of the heap structure in the MCed process. */

   void* heap_address;
 
   /** Copy of the heap structure of the process
   void* heap_address;
 
   /** Copy of the heap structure of the process


@@ -125,6 +135,8 @@ void MC_process_refresh_heap(mc_process_t process);
  * */
 void MC_process_refresh_malloc_info(mc_process_t process);
 
  * */
 void MC_process_refresh_malloc_info(mc_process_t process);
 

+void MC_process_refresh_simix_processes(mc_process_t process);
+

 static inline
 bool MC_process_is_self(mc_process_t process)
 {
 static inline
 bool MC_process_is_self(mc_process_t process)
 {


@@ -164,6 +176,8 @@ mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void
 
 dw_frame_t MC_process_find_function(mc_process_t process, const void* ip);
 
 
 dw_frame_t MC_process_find_function(mc_process_t process, const void* ip);
 

+void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size);
+

 static inline xbt_mheap_t MC_process_get_heap(mc_process_t process)
 {
   if (MC_process_is_self(process))
 static inline xbt_mheap_t MC_process_get_heap(mc_process_t process)
 {
   if (MC_process_is_self(process))


@@ -186,6 +200,21 @@ static inline malloc_info* MC_process_get_malloc_info(mc_process_t process)
  */
 dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
 
  */
 dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name);
 

+// ***** Things to move somewhere else:
+
+smx_process_t MC_process_get_issuer(mc_process_t process, smx_simcall_t req);
+
+void MC_simcall_handle(smx_simcall_t req, int value);
+
+void mc_smx_process_info_clear(mc_smx_process_info_t p);
+
+static inline
+xbt_dynar_t mc_smx_process_info_list_new()
+{
+  return xbt_dynar_new(
+    sizeof(s_mc_smx_process_info_t), (void_f_pvoid_t) &mc_smx_process_info_clear);
+}
+

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c
index d9d79e1..de2242d 100644 (file)
--- a/src/mc/mc_record.c
+++ b/src/mc/mc_record.c
@@ -108,7 +108,8 @@ char* MC_record_stack_to_string(xbt_fifo_t stack)
     mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
     int value = 0;
     smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
     mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
     int value = 0;
     smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);

-    int pid = saved_req->issuer->pid;
+    const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, saved_req);
+    const int pid = issuer->pid;

 
     // Serialization the (pid, value) pair:
     const char* sep = (item!=start) ? ";" : "";
 
     // Serialization the (pid, value) pair:
     const char* sep = (item!=start) ? ";" : "";

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index af7f1ef..2d6bdee 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -42,6 +42,8 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
         simcall_comm_irecv__get__rdv(r1);
 
         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
         simcall_comm_irecv__get__rdv(r1);
 

+    // FIXME, remote access to comm object
+

     if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return FALSE;
     if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return FALSE;


@@ -233,20 +235,25 @@ char *MC_request_to_string(smx_simcall_t req, int value)
   smx_synchro_t act = NULL;
   size_t size = 0;
 
   smx_synchro_t act = NULL;
   size_t size = 0;
 

+  // FIXME, host_get_name
+  // FIXME, buffer access (issuer->name, issuer->smx_host)
+
+  smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+

   switch (req->call) {
   case SIMCALL_COMM_ISEND:
     type = xbt_strdup("iSend");
     p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
     bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
   switch (req->call) {
   case SIMCALL_COMM_ISEND:
     type = xbt_strdup("iSend");
     p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
     bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       args =
       args =

-          bprintf("src=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+          bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host), issuer->name,

                   p, bs);
     else
       args =
                   p, bs);
     else
       args =

-          bprintf("src=(%lu)%s, buff=%s, size=%s", req->issuer->pid,
-                  req->issuer->name, p, bs);
+          bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
+                  issuer->name, p, bs);

     break;
   case SIMCALL_COMM_IRECV:
     size =
     break;
   case SIMCALL_COMM_IRECV:
     size =


@@ -255,15 +262,15 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     type = xbt_strdup("iRecv");
     p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
     bs = buff_size_to_string(size);
     type = xbt_strdup("iRecv");
     p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
     bs = buff_size_to_string(size);

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       args =
       args =

-          bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+          bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host), issuer->name,

                   p, bs);
     else
       args =
                   p, bs);
     else
       args =

-          bprintf("dst=(%lu)%s, buff=%s, size=%s", req->issuer->pid,
-                  req->issuer->name, p, bs);
+          bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
+                  issuer->name, p, bs);

     break;
   case SIMCALL_COMM_WAIT:
     act = simcall_comm_wait__get__comm(req);
     break;
   case SIMCALL_COMM_WAIT:
     act = simcall_comm_wait__get__comm(req);


@@ -349,13 +356,13 @@ char *MC_request_to_string(smx_simcall_t req, int value)
 
   if (args != NULL) {
     str =
 
   if (args != NULL) {
     str =

-        bprintf("[(%lu)%s (%s)] %s(%s)", req->issuer->pid,
-                MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+        bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
+                MSG_host_get_name(issuer->smx_host), issuer->name,

                 type, args);
   } else {
     str =
                 type, args);
   } else {
     str =

-        bprintf("[(%lu)%s (%s)] %s ", req->issuer->pid,
-                MSG_host_get_name(req->issuer->smx_host), req->issuer->name,
+        bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
+                MSG_host_get_name(issuer->smx_host), issuer->name,

                 type);
   }
 
                 type);
   }
 


@@ -417,48 +424,51 @@ int MC_process_is_enabled(smx_process_t process)
 
 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 {
 
 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 {

+  // TODO, remote access to MSG_host_get_name(issuer->smx_host)

 
   char *str = NULL, *label = NULL;
   smx_synchro_t act = NULL;
 
 
   char *str = NULL, *label = NULL;
   smx_synchro_t act = NULL;
 

+  const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+

   switch (req->call) {
   case SIMCALL_COMM_ISEND:
   switch (req->call) {
   case SIMCALL_COMM_ISEND:

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       label =
       label =

-          bprintf("[(%lu)%s] iSend", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host));
+          bprintf("[(%lu)%s] iSend", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host));

     else
     else

-      label = bprintf("[(%lu)] iSend", req->issuer->pid);
+      label = bprintf("[(%lu)] iSend", issuer->pid);

     break;
 
   case SIMCALL_COMM_IRECV:
     break;
 
   case SIMCALL_COMM_IRECV:

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       label =
       label =

-          bprintf("[(%lu)%s] iRecv", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host));
+          bprintf("[(%lu)%s] iRecv", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host));

     else
     else

-      label = bprintf("[(%lu)] iRecv", req->issuer->pid);
+      label = bprintf("[(%lu)] iRecv", issuer->pid);

     break;
 
   case SIMCALL_COMM_WAIT:
     act = simcall_comm_wait__get__comm(req);
     if (value == -1) {
     break;
 
   case SIMCALL_COMM_WAIT:
     act = simcall_comm_wait__get__comm(req);
     if (value == -1) {

-      if (req->issuer->smx_host)
+      if (issuer->smx_host)

         label =
         label =

-            bprintf("[(%lu)%s] WaitTimeout", req->issuer->pid,
-                    MSG_host_get_name(req->issuer->smx_host));
+            bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
+                    MSG_host_get_name(issuer->smx_host));

       else
       else

-        label = bprintf("[(%lu)] WaitTimeout", req->issuer->pid);
+        label = bprintf("[(%lu)] WaitTimeout", issuer->pid);

     } else {
     } else {

-      if (req->issuer->smx_host)
+      if (issuer->smx_host)

         label =
         label =

-            bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", req->issuer->pid,
-                    MSG_host_get_name(req->issuer->smx_host),
+            bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
+                    MSG_host_get_name(issuer->smx_host),

                     act->comm.src_proc ? act->comm.src_proc->pid : 0,
                     act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
       else
         label =
                     act->comm.src_proc ? act->comm.src_proc->pid : 0,
                     act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
       else
         label =

-            bprintf("[(%lu)] Wait [(%lu)->(%lu)]", req->issuer->pid,
+            bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,

                     act->comm.src_proc ? act->comm.src_proc->pid : 0,
                     act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
     }
                     act->comm.src_proc ? act->comm.src_proc->pid : 0,
                     act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
     }


@@ -467,81 +477,81 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
   case SIMCALL_COMM_TEST:
     act = simcall_comm_test__get__comm(req);
     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
   case SIMCALL_COMM_TEST:
     act = simcall_comm_test__get__comm(req);
     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {

-      if (req->issuer->smx_host)
+      if (issuer->smx_host)

         label =
         label =

-            bprintf("[(%lu)%s] Test FALSE", req->issuer->pid,
-                    MSG_host_get_name(req->issuer->smx_host));
+            bprintf("[(%lu)%s] Test FALSE", issuer->pid,
+                    MSG_host_get_name(issuer->smx_host));

       else
       else

-        label = bprintf("[(%lu)] Test FALSE", req->issuer->pid);
+        label = bprintf("[(%lu)] Test FALSE", issuer->pid);

     } else {
     } else {

-      if (req->issuer->smx_host)
+      if (issuer->smx_host)

         label =
         label =

-            bprintf("[(%lu)%s] Test TRUE", req->issuer->pid,
-                    MSG_host_get_name(req->issuer->smx_host));
+            bprintf("[(%lu)%s] Test TRUE", issuer->pid,
+                    MSG_host_get_name(issuer->smx_host));

       else
       else

-        label = bprintf("[(%lu)] Test TRUE", req->issuer->pid);
+        label = bprintf("[(%lu)] Test TRUE", issuer->pid);

     }
     break;
 
   case SIMCALL_COMM_WAITANY:
     }
     break;
 
   case SIMCALL_COMM_WAITANY:

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       label =
       label =

-          bprintf("[(%lu)%s] WaitAny [%d of %lu]", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host), value + 1,
+          bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host), value + 1,

                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
     else
       label =
                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
     else
       label =

-          bprintf("[(%lu)] WaitAny [%d of %lu]", req->issuer->pid, value + 1,
+          bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,

                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
     break;
 
   case SIMCALL_COMM_TESTANY:
     if (value == -1) {
                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
     break;
 
   case SIMCALL_COMM_TESTANY:
     if (value == -1) {

-      if (req->issuer->smx_host)
+      if (issuer->smx_host)

         label =
         label =

-            bprintf("[(%lu)%s] TestAny FALSE", req->issuer->pid,
-                    MSG_host_get_name(req->issuer->smx_host));
+            bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
+                    MSG_host_get_name(issuer->smx_host));

       else
       else

-        label = bprintf("[(%lu)] TestAny FALSE", req->issuer->pid);
+        label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);

     } else {
     } else {

-      if (req->issuer->smx_host)
+      if (issuer->smx_host)

         label =
         label =

-            bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", req->issuer->pid,
-                    MSG_host_get_name(req->issuer->smx_host), value + 1,
+            bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
+                    MSG_host_get_name(issuer->smx_host), value + 1,

                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
       else
         label =
                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
       else
         label =

-            bprintf("[(%lu)] TestAny TRUE [%d of %lu]", req->issuer->pid,
+            bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,

                     value + 1,
                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
     }
     break;
 
   case SIMCALL_MC_RANDOM:
                     value + 1,
                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
     }
     break;
 
   case SIMCALL_MC_RANDOM:

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       label =
       label =

-          bprintf("[(%lu)%s] MC_RANDOM (%d)", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host), value);
+          bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host), value);

     else
     else

-      label = bprintf("[(%lu)] MC_RANDOM (%d)", req->issuer->pid, value);
+      label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);

     break;
 
   case SIMCALL_MC_SNAPSHOT:
     break;
 
   case SIMCALL_MC_SNAPSHOT:

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       label =
       label =

-          bprintf("[(%lu)%s] MC_SNAPSHOT", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host));
+          bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host));

     else
     else

-      label = bprintf("[(%lu)] MC_SNAPSHOT", req->issuer->pid);
+      label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);

     break;
 
   case SIMCALL_MC_COMPARE_SNAPSHOTS:
     break;
 
   case SIMCALL_MC_COMPARE_SNAPSHOTS:

-    if (req->issuer->smx_host)
+    if (issuer->smx_host)

       label =
       label =

-          bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", req->issuer->pid,
-                  MSG_host_get_name(req->issuer->smx_host));
+          bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
+                  MSG_host_get_name(issuer->smx_host));

     else
     else

-      label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", req->issuer->pid);
+      label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);

     break;
 
   default:
     break;
 
   default:


@@ -550,7 +560,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
   str =
       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
 
   str =
       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,

-              colors[req->issuer->pid - 1], colors[req->issuer->pid - 1]);
+              colors[issuer->pid - 1], colors[issuer->pid - 1]);

   xbt_free(label);
   return str;
 
   xbt_free(label);
   return str;
 

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 3d0fc9e..2aafad6 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -4,6 +4,8 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 

+#include <assert.h>
+

 #include "mc_state.h"
 #include "mc_request.h"
 #include "mc_safety.h"
 #include "mc_state.h"
 #include "mc_request.h"
 #include "mc_safety.h"


@@ -29,7 +31,6 @@ void MC_pre_modelcheck_safety()
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
   initial_state = MC_state_new();
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
   initial_state = MC_state_new();

-

   MC_SET_STD_HEAP;
 
   XBT_DEBUG("**************************************************");
   MC_SET_STD_HEAP;
 
   XBT_DEBUG("**************************************************");


@@ -41,13 +42,13 @@ void MC_pre_modelcheck_safety()
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */

-  xbt_swag_foreach(process, simix_global->process_list) {
+  MC_EACH_SIMIX_PROCESS(process,

     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
       if (mc_reduce_kind != e_mc_reduce_none)
         break;
     }
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
       if (mc_reduce_kind != e_mc_reduce_none)
         break;
     }

-  }
+  );

 
   xbt_fifo_unshift(mc_stack, initial_state);
   mmalloc_set_current_heap(heap);
 
   xbt_fifo_unshift(mc_stack, initial_state);
   mmalloc_set_current_heap(heap);


@@ -101,7 +102,7 @@ void MC_modelcheck_safety(void)
       mc_stats->executed_transitions++;
 
       /* Answer the request */
       mc_stats->executed_transitions++;
 
       /* Answer the request */

-      SIMIX_simcall_handle(req, value);
+      MC_simcall_handle(req, value);

 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();


@@ -114,13 +115,13 @@ void MC_modelcheck_safety(void)
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */

-        xbt_swag_foreach(process, simix_global->process_list) {
+        MC_EACH_SIMIX_PROCESS(process,

           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
             if (mc_reduce_kind != e_mc_reduce_none)
               break;
           }
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
             if (mc_reduce_kind != e_mc_reduce_none)
               break;
           }

-        }
+        );

 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);


@@ -187,6 +188,7 @@ void MC_modelcheck_safety(void)
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);

+          const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);

           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {


@@ -201,8 +203,8 @@ void MC_modelcheck_safety(void)
                 xbt_free(req_str);
               }
 
                 xbt_free(req_str);
               }
 

-              if (!MC_state_process_is_done(prev_state, req->issuer))
-                MC_state_interleave_process(prev_state, req->issuer);
+              if (!MC_state_process_is_done(prev_state, issuer))
+                MC_state_interleave_process(prev_state, issuer);

               else
                 XBT_DEBUG("Process %p is in done set", req->issuer);
 
               else
                 XBT_DEBUG("Process %p is in done set", req->issuer);
 


@@ -215,10 +217,11 @@ void MC_modelcheck_safety(void)
 
             } else {
 
 
             } else {
 

+              const smx_process_t previous_issuer = MC_process_get_issuer(&mc_model_checker->process, MC_state_get_internal_request(prev_state));

               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",

-                        req->call, req->issuer->pid, state->num,
+                        req->call, issuer->pid, state->num,

                         MC_state_get_internal_request(prev_state)->call,
                         MC_state_get_internal_request(prev_state)->call,

-                        MC_state_get_internal_request(prev_state)->issuer->pid,
+                        previous_issuer->pid,

                         prev_state->num);
 
             }
                         prev_state->num);
 
             }

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 84db3e8..49dbb7e 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -4,6 +4,8 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 

+#include <assert.h>
+

 #include "../simix/smx_private.h"
 #include "xbt/fifo.h"
 #include "mc_state.h"
 #include "../simix/smx_private.h"
 #include "xbt/fifo.h"
 #include "mc_state.h"


@@ -99,6 +101,7 @@ void MC_state_delete(mc_state_t state, int free_snapshot){
 
 void MC_state_interleave_process(mc_state_t state, smx_process_t process)
 {
 
 void MC_state_interleave_process(mc_state_t state, smx_process_t process)
 {

+  assert(state);

   state->proc_status[process->pid].state = MC_INTERLEAVE;
   state->proc_status[process->pid].interleave_count = 0;
 }
   state->proc_status[process->pid].state = MC_INTERLEAVE;
   state->proc_status[process->pid].interleave_count = 0;
 }


@@ -142,6 +145,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
   case SIMCALL_COMM_WAITANY:
     state->internal_req.call = SIMCALL_COMM_WAIT;
     state->internal_req.issuer = req->issuer;
   case SIMCALL_COMM_WAITANY:
     state->internal_req.call = SIMCALL_COMM_WAIT;
     state->internal_req.issuer = req->issuer;

+    // FIXME, read from remote process

     state->internal_comm =
         *xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
                           smx_synchro_t);
     state->internal_comm =
         *xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
                           smx_synchro_t);


@@ -154,6 +158,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
     state->internal_req.issuer = req->issuer;
 
     if (value > 0)
     state->internal_req.issuer = req->issuer;
 
     if (value > 0)

+      // FIXME, read from remote process

       state->internal_comm =
           *xbt_dynar_get_as(simcall_comm_testany__get__comms(req), value,
                             smx_synchro_t);
       state->internal_comm =
           *xbt_dynar_get_as(simcall_comm_testany__get__comms(req), value,
                             smx_synchro_t);


@@ -164,6 +169,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_COMM_WAIT:
     state->internal_req = *req;
 
   case SIMCALL_COMM_WAIT:
     state->internal_req = *req;

+    // FIXME, read from remote process

     state->internal_comm = *(simcall_comm_wait__get__comm(req));
     simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
     state->internal_comm = *(simcall_comm_wait__get__comm(req));
     simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);


@@ -171,6 +177,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_COMM_TEST:
     state->internal_req = *req;
 
   case SIMCALL_COMM_TEST:
     state->internal_req = *req;

+    // FIXME, read from remote process

     state->internal_comm = *simcall_comm_test__get__comm(req);
     simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
     state->internal_comm = *simcall_comm_test__get__comm(req);
     simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);


@@ -178,14 +185,16 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
 
   case SIMCALL_MC_RANDOM:
     state->internal_req = *req;
 
   case SIMCALL_MC_RANDOM:
     state->internal_req = *req;

-    if (value != simcall_mc_random__get__max(req)) {
-      xbt_swag_foreach(process, simix_global->process_list) {
+    int random_max = simcall_mc_random__get__max(req);
+    if (value != random_max) {
+      MC_EACH_SIMIX_PROCESS(process,

         procstate = &state->proc_status[process->pid];
         procstate = &state->proc_status[process->pid];

-        if (process->pid == req->issuer->pid) {
+        const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
+        if (process->pid == issuer->pid) {

           procstate->state = MC_MORE_INTERLEAVE;
           break;
         }
           procstate->state = MC_MORE_INTERLEAVE;
           break;
         }

-      }
+      );

     }
     break;
 
     }
     break;
 


@@ -213,7 +222,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
   unsigned int start_count;
   smx_synchro_t act = NULL;
 
   unsigned int start_count;
   smx_synchro_t act = NULL;
 

-  xbt_swag_foreach(process, simix_global->process_list) {
+  MC_EACH_SIMIX_PROCESS(process,

     procstate = &state->proc_status[process->pid];
 
     if (procstate->state == MC_INTERLEAVE
     procstate = &state->proc_status[process->pid];
 
     if (procstate->state == MC_INTERLEAVE


@@ -300,7 +309,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
         }
       }
     }
         }
       }
     }

-  }
+  );

 
   return NULL;
 }
 
   return NULL;
 }

diff --git a/src/xbt/dynar.c b/src/xbt/dynar.c
index 26c9196..e591967 100644 (file)
--- a/src/xbt/dynar.c
+++ b/src/xbt/dynar.c
@@ -827,6 +827,20 @@ XBT_TEST_UNIT("int", test_dynar_int, "Dynars of integers")
     xbt_test_log("Pop %d, length=%lu", cpt, xbt_dynar_length(d));
   }
 
     xbt_test_log("Pop %d, length=%lu", cpt, xbt_dynar_length(d));
   }
 

+  int* pi;
+  xbt_dynar_foreach_ptr(d, cursor, pi) {
+    *pi = 0;
+  }
+  xbt_dynar_foreach(d, cursor, i) {
+    xbt_test_assert(i == 0, "The value is not the same as the expected one.");
+  }
+  xbt_dynar_foreach_ptr(d, cursor, pi) {
+    *pi = 1;
+  }
+  xbt_dynar_foreach(d, cursor, i) {
+    xbt_test_assert(i == 1, "The value is not the same as the expected one.");
+  }
+

   /* 5. Free the resources */
   xbt_dynar_free(&d);           /* This code is used both as example and as regression test, so we try to */
   xbt_dynar_free(&d);           /* free the struct twice here to check that it's ok, but freeing  it only once */
   /* 5. Free the resources */
   xbt_dynar_free(&d);           /* This code is used both as example and as regression test, so we try to */
   xbt_dynar_free(&d);           /* free the struct twice here to check that it's ok, but freeing  it only once */