Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid
authorPierre Veyre <pierre.veyre@cc.in2p3.fr>
Mon, 7 Oct 2013 08:52:18 +0000 (10:52 +0200)
committerPierre Veyre <pierre.veyre@cc.in2p3.fr>
Mon, 7 Oct 2013 08:52:18 +0000 (10:52 +0200)
Conflicts:
src/surf/storage.c

16 files changed:
examples/msg/chord/chord.c
examples/msg/mc/bugged1_liveness_visited.tesh
examples/platforms/storage.xml
examples/simdag/dot/test_simdag_dotload.tesh
src/mc/mc_checkpoint.c
src/mc/mc_compare.c
src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/mc_liveness.c
src/mc/mc_pair.c
src/mc/mc_private.h
src/msg/msg_io.c
src/smpi/smpi_bench.c
src/surf/storage.c
src/xbt/xbt_sha.c
teshsuite/msg/storage/storage.c

index 9744413..7289d43 100644 (file)
@@ -608,7 +608,12 @@ static void quit_notify(node_t node)
 
   msg_task_t task_sent = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data);
   XBT_DEBUG("Sending a 'PREDECESSOR_LEAVING' to my successor %d",node->fingers[0].id);
-  MSG_task_send_with_timeout(task_sent, node->fingers[0].mailbox, timeout);
+  if (MSG_task_send_with_timeout(task_sent, node->fingers[0].mailbox, timeout)==
+      MSG_TIMEOUT) {
+    XBT_DEBUG("Timeout expired when sending a 'PREDECESSOR_LEAVING' to my successor %d",
+        node->fingers[0].id);
+    task_free(task_sent);
+  }
 
   //send the SUCCESSOR_LEAVING to our predecessor
   get_mailbox(node->pred_id, mailbox);
@@ -621,7 +626,12 @@ static void quit_notify(node_t node)
 
   msg_task_t task_sent_s = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data_s);
   XBT_DEBUG("Sending a 'SUCCESSOR_LEAVING' to my predecessor %d",node->pred_id);
-  MSG_task_send_with_timeout(task_sent_s, mailbox, timeout);
+  if (MSG_task_send_with_timeout(task_sent_s, mailbox, timeout)==
+      MSG_TIMEOUT) {
+    XBT_DEBUG("Timeout expired when sending a 'SUCCESSOR_LEAVING' to my predecessor %d",
+        node->pred_id);
+    task_free(task_sent_s);
+  }
 
 }
 
index 49d40fc..3341b5a 100644 (file)
@@ -20,11 +20,57 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
+> [  0.000000] (2:client@Boivin) Ask the request
+> [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
@@ -35,6 +81,7 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
+> [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
@@ -57,6 +104,7 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
+> [  0.000000] (3:client@Fafard) Propositions changed : r=1, cs=0
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
@@ -129,5 +177,5 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62)
 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54)
 > [  0.000000] (0:@) Expanded pairs = 57
-> [  0.000000] (0:@) Visited pairs = 208
-> [  0.000000] (0:@) Executed transitions = 207
\ No newline at end of file
+> [  0.000000] (0:@) Visited pairs = 365
+> [  0.000000] (0:@) Executed transitions = 364
index 451a0bf..84310bd 100644 (file)
@@ -26,7 +26,9 @@
 
                <storage id="Disk1" typeId="single_HDD"/>
                <storage id="Disk2" typeId="single_SSD"/>
-               <storage id="Disk3" typeId="single_HDD"/>
+               <storage id="Disk3" typeId="single_HDD"
+                         content="content/storage_content.txt" 
+                        content_type="txt_unix"/>
                <storage id="Disk4" typeId="single_SSD"/>
 
                <host id="bob" power="1Gf">
index 5b49c31..d62188c 100644 (file)
@@ -503,4 +503,4 @@ $ $SG_TEST_EXENV ./dot_test --log=no_loc ${srcdir:=.}/../2clusters.xml ${srcdir:
 > [0.000000] [sd_daxparse/WARNING] the task 5 is in a cycle
 > [0.000000] [sd_daxparse/WARNING] the task 6 is in a cycle
 > [0.000000] [sd_dotparse/ERROR] The DOT described in dag_with_cycle.dot is not a DAG. It contains a cycle.
-> [0.000000] [test/CRITICAL] No dot load may be you have a cycle in your graph
+> [0.000000] [test/CRITICAL] No dot loaded. Do you have a cycle in your graph?
\ No newline at end of file
index 832005f..2b2fe9d 100644 (file)
@@ -725,7 +725,7 @@ static void MC_dump_checkpoint_ignore(mc_snapshot_t snapshot){
 }
 
 
-mc_snapshot_t MC_take_snapshot(){
+mc_snapshot_t MC_take_snapshot(int num_state){
 
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
   snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
@@ -741,7 +741,8 @@ mc_snapshot_t MC_take_snapshot(){
     //MC_get_hash_local(snapshot->hash_local, snapshot->stacks);
   }
 
-  MC_dump_checkpoint_ignore(snapshot);
+  if(num_state > 0)
+    MC_dump_checkpoint_ignore(snapshot);
 
   return snapshot;
 
@@ -756,7 +757,7 @@ void MC_restore_snapshot(mc_snapshot_t snapshot){
 }
 
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall){
-  return MC_take_snapshot();
+  return MC_take_snapshot(1);
 }
 
 void *MC_snapshot(void){
index 7f2ea63..e7ece50 100644 (file)
@@ -337,10 +337,10 @@ int snapshot_compare(void *state1, void *state2){
   int num1, num2;
   
   if(_sg_mc_property_file && _sg_mc_property_file[0] != '\0'){ /* Liveness MC */
-    s1 = ((mc_pair_t)state1)->graph_state->system_state;
-    s2 = ((mc_pair_t)state2)->graph_state->system_state;
-    num1 = ((mc_pair_t)state1)->num;
-    num2 =  ((mc_pair_t)state2)->num;
+    s1 = ((mc_visited_pair_t)state1)->graph_state->system_state;
+    s2 = ((mc_visited_pair_t)state2)->graph_state->system_state;
+    num1 = ((mc_visited_pair_t)state1)->num;
+    num2 =  ((mc_visited_pair_t)state2)->num;
     /* Firstly compare automaton state */
     /*if(xbt_automaton_state_compare(((mc_pair_t)state1)->automaton_state, ((mc_pair_t)state2)->automaton_state) != 0)
       return 1;
index 643acf8..ebda309 100644 (file)
@@ -33,7 +33,7 @@ static mc_visited_state_t visited_state_new(){
   new_state = xbt_new0(s_mc_visited_state_t, 1);
   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
-  new_state->system_state = MC_take_snapshot();
+  new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
   new_state->num = mc_stats->expanded_states;
   new_state->other_num = -1;
 
@@ -276,6 +276,7 @@ void MC_dpor(void)
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
+  mc_state_t state_test = NULL;
   int pos;
   int visited_state = -1;
   int enabled = 0;
@@ -287,9 +288,9 @@ void MC_dpor(void)
       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
+    XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
               xbt_fifo_size(mc_stack_safety), state, state->num,
-              MC_state_interleave_size(state), user_max_depth_reached);
+              MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
       
     /* Update statistics */
     mc_stats->visited_states++;
@@ -343,7 +344,7 @@ void MC_dpor(void)
         }
 
         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
-          next_state->system_state = MC_take_snapshot();
+          next_state->system_state = MC_take_snapshot(next_state->num);
         }
 
         if(dot_output != NULL)
@@ -395,8 +396,6 @@ void MC_dpor(void)
             char *key = bprintf("%lu", process->pid);
             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
             xbt_free(key);
-            mc_state_t state_test = NULL;
-            xbt_fifo_item_t item = NULL;
             int cursor = xbt_fifo_size(mc_stack_safety);
             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
               if(cursor-- == enabled){ 
@@ -406,7 +405,7 @@ void MC_dpor(void)
                   break;
                 }
               }
-            } 
+            }
           }
         }
 
@@ -504,7 +503,7 @@ void MC_dpor(void)
             MC_UNSET_RAW_MEM;
             MC_replay(mc_stack_safety, -1);
           }
-          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
+          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
           break;
         } else {
           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
index 2fba00d..4ae023d 100644 (file)
@@ -1875,7 +1875,7 @@ void MC_modelcheck_safety(void)
   MC_SET_RAW_MEM;
   /* Save the initial state */
   initial_state_safety = xbt_new0(s_mc_global_t, 1);
-  initial_state_safety->snapshot = MC_take_snapshot();
+  initial_state_safety->snapshot = MC_take_snapshot(0);
   MC_UNSET_RAW_MEM;
 
   MC_dpor();
index 2007c64..d0303b5 100644 (file)
@@ -36,20 +36,20 @@ static xbt_dynar_t get_atomic_propositions_values(){
   return values;
 }
 
-static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min, int *max){
+static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 
   int cursor = 0, previous_cursor, next_cursor;
-  mc_pair_t pair_test;
+  mc_visited_pair_t pair_test;
   int start = 0;
   int end = xbt_dynar_length(all_pairs) - 1;
   
   while(start <= end){
     cursor = (start + end) / 2;
-    pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_pair_t);
+    pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_visited_pair_t);
     if(pair_test->nb_processes < pair->nb_processes){
       start = cursor + 1;
     }else if(pair_test->nb_processes > pair->nb_processes){
@@ -63,7 +63,7 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min,
         *min = *max = cursor;
         previous_cursor = cursor - 1;
         while(previous_cursor >= 0){
-          pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_pair_t);
+          pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_visited_pair_t);
           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
             break;
           *min = previous_cursor;
@@ -71,7 +71,7 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min,
         }
         next_cursor = cursor + 1;
         while(next_cursor < xbt_dynar_length(all_pairs)){
-          pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_pair_t);
+          pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_visited_pair_t);
           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
             break;
           *max = next_cursor;
@@ -90,35 +90,25 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min,
   return cursor;
 }
 
-static int is_reached_acceptance_pair(mc_pair_t pair){
+static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
+  
+  mc_visited_pair_t pair = NULL;
+  pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+  pair->acceptance_pair = 1;
+  
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
-    if(pair->graph_state->system_state == NULL){
-      pair->graph_state->system_state = MC_take_snapshot();
-      pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-    }
     xbt_dynar_push(acceptance_pairs, &pair); 
 
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
-
-    return -1;
-
   }else{
 
-    if(pair->graph_state->system_state == NULL){
-      pair->graph_state->system_state = MC_take_snapshot();
-      pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-    }
-
     int min = -1, max = -1, index;
     //int res;
-    mc_pair_t pair_test;
+    mc_visited_pair_t pair_test;
     int cursor;
 
     index = get_search_interval(acceptance_pairs, pair, &min, &max);
@@ -132,13 +122,20 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
         }*/
       cursor = min;
       while(cursor <= max){
-        pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
+        pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
         if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
           if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
             if(snapshot_compare(pair_test, pair) == 0){
+              XBT_INFO("Pair %d already reached (equal to pair %d) !", pair->num, pair_test->num);
+              
+              xbt_fifo_shift(mc_stack_liveness);
+              if(dot_output != NULL)
+                fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, pair_test->num, initial_state_liveness->prev_req);
+
               if(!raw_mem_set)
                 MC_UNSET_RAW_MEM;
-              return pair_test->num;
+
+              return NULL;
             }
           }
         }
@@ -146,7 +143,7 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
       }
       xbt_dynar_insert_at(acceptance_pairs, min, &pair);
     }else{
-      pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_pair_t);
+      pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
       if(pair_test->nb_processes < pair->nb_processes){
         xbt_dynar_insert_at(acceptance_pairs, index+1, &pair);
       }else{
@@ -156,119 +153,48 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
           xbt_dynar_insert_at(acceptance_pairs, index, &pair);
       }
     }
-
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
-    
-    return -1;
-    
-  }
-}
-
-
-static void set_acceptance_pair_reached(mc_pair_t pair){
-
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  MC_SET_RAW_MEM;
-
-  if(xbt_dynar_is_empty(acceptance_pairs)){
-
-     if(pair->graph_state->system_state == NULL){
-       pair->graph_state->system_state = MC_take_snapshot();
-       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-     }
-     xbt_dynar_push(acceptance_pairs, &pair); 
-
-  }else{
-
-    if(pair->graph_state->system_state == NULL){
-      pair->graph_state->system_state = MC_take_snapshot();
-      pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-    }
     
-    size_t current_bytes_used = pair->heap_bytes_used;
-    int current_nb_processes = pair->nb_processes;
-
-    int cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(acceptance_pairs) - 1;
-
-    mc_pair_t pair_test = NULL;
-    size_t bytes_used_test = 0;
-    int nb_processes_test;
-
-    while(start <= end){
-      cursor = (start + end) / 2;
-      pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
-      bytes_used_test = pair_test->heap_bytes_used;
-      nb_processes_test = pair_test->nb_processes;
-      if(nb_processes_test < current_nb_processes)
-        start = cursor + 1;
-      if(nb_processes_test > current_nb_processes)
-        end = cursor - 1; 
-      if(nb_processes_test == current_nb_processes){
-        if(bytes_used_test < current_bytes_used)
-          start = cursor + 1;
-        if(bytes_used_test > current_bytes_used)
-          end = cursor - 1;
-        if(bytes_used_test == current_bytes_used)
-          break;
-      }
-    }
-
-    if(pair_test->nb_processes < pair->nb_processes){
-      xbt_dynar_insert_at(acceptance_pairs, cursor+1, &pair);
-    }else{
-      if(pair_test->heap_bytes_used < pair->heap_bytes_used)
-        xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
-      else
-        xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
-    }    
-
   }
 
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
-    
+
+  return pair;
 }
 
-static void remove_acceptance_pair(mc_pair_t pair){
+static void remove_acceptance_pair(int pair_num){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
+  fprintf(stderr, "Search acceptance pair %d\n", pair_num);
+
   MC_SET_RAW_MEM;
 
   unsigned int cursor = 0;
-  mc_pair_t pair_test;
-  int pair_found = 0;
+  mc_visited_pair_t pair_test = NULL;
 
   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
-    if(pair_test->num == pair->num){
-      pair_found = 1;
+    if(pair_test->num == pair_num){
       break;
     }
   }
 
-  if(pair_found)
-    xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
+  xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
   
-  pair->acceptance_removed = 1;
+  pair_test->acceptance_removed = 1;
 
-  if(pair->stack_removed && pair->acceptance_removed){
-    if(_sg_mc_visited == 0){
-      MC_pair_delete(pair);
-    }else if(pair->visited_removed){
-      MC_pair_delete(pair);
-    }
+  if(_sg_mc_visited == 0){
+    MC_visited_pair_delete(pair_test);
+  }else if(pair_test->visited_removed == 1){
+    MC_visited_pair_delete(pair_test);
   }
 
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
 }
 
-static int is_visited_pair(mc_pair_t pair){
+static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
   if(_sg_mc_visited == 0)
     return -1;
@@ -277,28 +203,26 @@ static int is_visited_pair(mc_pair_t pair){
 
   MC_SET_RAW_MEM;
 
-  if(xbt_dynar_is_empty(visited_pairs)){
+  mc_visited_pair_t new_pair = NULL;
 
-    if(pair->graph_state->system_state == NULL)
-      pair->graph_state->system_state = MC_take_snapshot();
-    xbt_dynar_push(visited_pairs, &pair); 
+  if(pair == NULL){
+    new_pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+  }else{
+    new_pair = pair;
+  }
 
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
+  if(xbt_dynar_is_empty(visited_pairs)){
 
-    return -1;
+    xbt_dynar_push(visited_pairs, &new_pair); 
 
   }else{
 
-    if(pair->graph_state->system_state == NULL)
-      pair->graph_state->system_state = MC_take_snapshot();
-
     int min = -1, max = -1, index;
     //int res;
-    mc_pair_t pair_test;
+    mc_visited_pair_t pair_test;
     int cursor;
 
-    index = get_search_interval(visited_pairs, pair, &min, &max);
+    index = get_search_interval(visited_pairs, new_pair, &min, &max);
 
     if(min != -1 && max != -1){ // Visited pair with same number of processes and same heap bytes used exists
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
@@ -330,48 +254,47 @@ static int is_visited_pair(mc_pair_t pair){
         }*/
       cursor = min;
       while(cursor <= max){
-        pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
-        if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-          if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
-            if(snapshot_compare(pair_test, pair) == 0){
-              if(pair_test->other_num == -1)
-                pair->other_num = pair_test->num;
-              else
-                pair->other_num = pair_test->other_num;
-              if(dot_output == NULL)
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
-              else
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
-              xbt_dynar_remove_at(visited_pairs, cursor, NULL);
-              xbt_dynar_insert_at(visited_pairs, cursor, &pair);
-              pair_test->visited_removed = 1;
-              if(pair_test->stack_removed && pair_test->visited_removed){
-                if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
-                  if(pair_test->acceptance_removed){
-                    MC_pair_delete(pair_test);
-                  }
+        pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+        //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
+          if(xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0){
+            if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0){
+              if(snapshot_compare(pair_test, new_pair) == 0){
+                if(pair_test->other_num == -1)
+                  new_pair->other_num = pair_test->num;
+                else
+                  new_pair->other_num = pair_test->other_num;
+                if(dot_output == NULL)
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                else
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
+                xbt_dynar_remove_at(visited_pairs, cursor, NULL);
+                xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+                pair_test->visited_removed = 1;
+                if(pair_test->acceptance_pair){
+                  if(pair_test->acceptance_removed == 1)
+                    MC_visited_pair_delete(pair_test);
                 }else{
-                  MC_pair_delete(pair_test);
+                  MC_visited_pair_delete(pair_test);
                 }
+                if(!raw_mem_set)
+                  MC_UNSET_RAW_MEM;
+                return new_pair->other_num;
               }
-              if(!raw_mem_set)
-                MC_UNSET_RAW_MEM;
-              return pair->other_num;
             }
-          }
+            //}
         }
         cursor++;
       }
-      xbt_dynar_insert_at(visited_pairs, min, &pair);
+      xbt_dynar_insert_at(visited_pairs, min, &new_pair);
     }else{
-      pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_pair_t);
-      if(pair_test->nb_processes < pair->nb_processes){
-        xbt_dynar_insert_at(visited_pairs, index+1, &pair);
+      pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
+      if(pair_test->nb_processes < new_pair->nb_processes){
+        xbt_dynar_insert_at(visited_pairs, index+1, &new_pair);
       }else{
-        if(pair_test->heap_bytes_used < pair->heap_bytes_used)
-          xbt_dynar_insert_at(visited_pairs, index + 1, &pair);
+        if(pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+          xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
         else
-          xbt_dynar_insert_at(visited_pairs, index, &pair);
+          xbt_dynar_insert_at(visited_pairs, index, &new_pair);
       }
     }
 
@@ -387,17 +310,20 @@ static int is_visited_pair(mc_pair_t pair){
       }
       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
       pair_test->visited_removed = 1;
-      if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
-        MC_pair_delete(pair_test);
-      
+      if(pair_test->acceptance_pair){
+        if(pair_test->acceptance_removed)
+          MC_visited_pair_delete(pair_test);
+      }else{
+        MC_visited_pair_delete(pair_test);
+      }
     }
 
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
-    
-    return -1;
-
   }
+
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
+  
+  return -1;
 }
 
 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
@@ -456,11 +382,11 @@ void MC_ddfs_init(void){
 
   MC_SET_RAW_MEM;
 
-  acceptance_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL); 
-  visited_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL); 
+  acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
+  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 
-  initial_state_liveness->snapshot = MC_take_snapshot();
+  initial_state_liveness->snapshot = MC_take_snapshot(0);
   initial_state_liveness->prev_pair = 0;
 
   MC_UNSET_RAW_MEM; 
@@ -497,40 +423,7 @@ void MC_ddfs_init(void){
       if(cursor != 0){
         MC_restore_snapshot(initial_state_liveness->snapshot);
         MC_UNSET_RAW_MEM;
-      }
-      
-
-    }else if(automaton_state->type == 2){ /* Acceptance automaton state */
-      
-      MC_SET_RAW_MEM;
-
-      initial_pair = MC_pair_new();
-      initial_pair->automaton_state = automaton_state;
-      initial_pair->graph_state = MC_state_new();
-      initial_pair->atomic_propositions = get_atomic_propositions_values();
-        
-      /* Get enabled process and insert it in the interleave set of the graph_state */
-      xbt_swag_foreach(process, simix_global->process_list){
-        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 = 1;
-        
-      xbt_fifo_unshift(mc_stack_liveness, initial_pair);
-        
-      MC_UNSET_RAW_MEM;
-
-      set_acceptance_pair_reached(initial_pair);
-  
-      MC_ddfs();
-
-      if(cursor != 0){
-        MC_restore_snapshot(initial_state_liveness->snapshot);
-        MC_UNSET_RAW_MEM;
-      }
+      } 
     }
   }
 
@@ -557,7 +450,7 @@ void MC_ddfs(){
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state));
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state), current_pair->num);
  
   mc_stats->visited_pairs++;
 
@@ -568,10 +461,12 @@ void MC_ddfs(){
   xbt_automaton_transition_t transition_succ;
   unsigned int cursor = 0;
   int res;
-  int reached_num, visited_num;
+  int visited_num;
 
   mc_pair_t next_pair = NULL;
   xbt_dynar_t prop_values = NULL;
+  int new_pair = 0;
+  mc_visited_pair_t reached_pair = NULL;
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
@@ -580,16 +475,7 @@ void MC_ddfs(){
       if(current_pair->search_cycle){
 
         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ 
-          
-          if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
-        
-            XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
-            
-            MC_SET_RAW_MEM;
-            xbt_fifo_shift(mc_stack_liveness);
-            if(dot_output != NULL)
-              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req);
-            MC_UNSET_RAW_MEM;
+          if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
 
             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
             XBT_INFO("|             ACCEPTANCE CYCLE            |");
@@ -604,14 +490,13 @@ void MC_ddfs(){
         }
       }
 
-      if((visited_num = is_visited_pair(current_pair)) != -1){
+      if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
 
         MC_SET_RAW_MEM;
         if(dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
         MC_UNSET_RAW_MEM;
-        
-      
+              
       }else{  
 
         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
@@ -662,6 +547,9 @@ void MC_ddfs(){
 
             if(res == 1){ // enabled transition in automaton
 
+              if(new_pair)
+                MC_replay_liveness(mc_stack_liveness, 1); 
+
               MC_SET_RAW_MEM;
 
               next_pair = MC_pair_new();
@@ -688,6 +576,8 @@ void MC_ddfs(){
 
               MC_UNSET_RAW_MEM;
 
+              new_pair = 1;
+
               MC_ddfs();
 
             }
@@ -701,6 +591,9 @@ void MC_ddfs(){
             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
   
             if(res == 2){ // true transition in automaton
+
+              if(new_pair)
+                MC_replay_liveness(mc_stack_liveness, 1); 
             
               MC_SET_RAW_MEM;
             
@@ -728,6 +621,8 @@ void MC_ddfs(){
             
               MC_UNSET_RAW_MEM;
 
+              new_pair = 1;
+
               MC_ddfs();
 
             }
@@ -743,117 +638,6 @@ void MC_ddfs(){
 
       }
  
-    }else{
-
-      mc_stats->executed_transitions++;
-      
-      XBT_DEBUG("No request to execute in this state, search evolution in B├╝chi Automaton.");
-
-      if(current_pair->search_cycle){
-
-        if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ 
-          
-          if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
-        
-            XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
-            
-            MC_SET_RAW_MEM;
-            xbt_fifo_shift(mc_stack_liveness);
-            MC_UNSET_RAW_MEM;
-
-            XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-            XBT_INFO("|             ACCEPTANCE CYCLE            |");
-            XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-            XBT_INFO("Counter-example that violates formula :");
-            MC_show_stack_liveness(mc_stack_liveness);
-            MC_dump_stack_liveness(mc_stack_liveness);
-            MC_print_statistics(mc_stats);
-            xbt_abort();
-
-          }
-        }
-      }
-
-      if((visited_num = is_visited_pair(current_pair)) != -1){
-
-        XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
-      
-      }else{            
-        
-        MC_SET_RAW_MEM;
-        prop_values = get_atomic_propositions_values();
-        MC_UNSET_RAW_MEM;
-
-        /* Evaluate enabled transition according to atomic propositions values */
-        cursor= 0;
-        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-
-          res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
-
-          if(res == 1){ // enabled transition in automaton
-
-            MC_SET_RAW_MEM;
-
-            next_pair = MC_pair_new();
-            next_pair->graph_state = MC_state_new();
-            next_pair->automaton_state = transition_succ->dst;
-            next_pair->atomic_propositions = get_atomic_propositions_values();
-            next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
-              
-            if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
-              next_pair->search_cycle = 1;
-            
-            xbt_fifo_unshift(mc_stack_liveness, next_pair);
-
-            if(mc_stats->expanded_pairs%1000 == 0)
-              XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-
-            if(dot_output != NULL)
-              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
-
-            MC_UNSET_RAW_MEM;
-
-            MC_ddfs();
-
-          }
-
-        }
-
-        /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
-        cursor = 0;   
-        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-      
-          res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
-  
-          if(res == 2){ // true transition in automaton
-
-            MC_SET_RAW_MEM;
-            
-            next_pair = MC_pair_new();
-            next_pair->graph_state = MC_state_new();
-            next_pair->automaton_state = transition_succ->dst;
-            next_pair->atomic_propositions = get_atomic_propositions_values();
-            next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
-            
-            if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
-              next_pair->search_cycle = 1;
-
-            xbt_fifo_unshift(mc_stack_liveness, next_pair);
-
-            if(mc_stats->expanded_pairs%1000 == 0)
-              XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-            
-            if(dot_output != NULL)
-              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
-
-            MC_UNSET_RAW_MEM;
-
-            MC_ddfs();
-
-          }
-
-        }
-      }
     }
     
   }else{
@@ -877,15 +661,10 @@ void MC_ddfs(){
   MC_SET_RAW_MEM;
   xbt_dynar_free(&prop_values);
   current_pair = xbt_fifo_shift(mc_stack_liveness);
-  current_pair->stack_removed = 1;
-  if(current_pair->search_cycle){
-    remove_acceptance_pair(current_pair);
-  }else{
-    if(_sg_mc_visited == 0)
-      MC_pair_delete(current_pair);
-    else if(current_pair->visited_removed)
-      MC_pair_delete(current_pair);
+  if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
+    remove_acceptance_pair(current_pair->num);
   }
+  MC_pair_delete(current_pair);
 
   MC_UNSET_RAW_MEM;
 
index ca6678b..1056f44 100644 (file)
@@ -9,19 +9,43 @@
 mc_pair_t MC_pair_new(){
   mc_pair_t p = NULL;
   p = xbt_new0(s_mc_pair_t, 1);
-  p->nb_processes = xbt_swag_size(simix_global->process_list);
   p->num = ++mc_stats->expanded_pairs;
   p->search_cycle = 0;
-  p->other_num = -1;
   return p;
 }
 
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
+  mc_visited_pair_t pair = NULL;
+  pair = xbt_new0(s_mc_visited_pair_t, 1);
+  pair->graph_state = MC_state_new();
+  pair->graph_state->system_state = MC_take_snapshot(pair_num);
+  pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  pair->nb_processes = xbt_swag_size(simix_global->process_list);
+  pair->automaton_state = automaton_state;
+  pair->num = pair_num;
+  pair->other_num = -1;
+  pair->acceptance_removed = 0;
+  pair->visited_removed = 0;
+  pair->acceptance_pair = 0;
+  pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
+  unsigned int cursor = 0;
+  int value;
+  xbt_dynar_foreach(atomic_propositions, cursor, value)
+    xbt_dynar_push_as(pair->atomic_propositions, int, value);
+  return pair;
+}
+
+void MC_visited_pair_delete(mc_visited_pair_t p){
+  p->automaton_state = NULL;
+  MC_state_delete(p->graph_state);
+  xbt_dynar_free(&(p->atomic_propositions));
+  xbt_free(p);
+  p = NULL;
+}
+
 void MC_pair_delete(mc_pair_t p){
   p->automaton_state = NULL;
   MC_state_delete(p->graph_state);
-  p->stack_removed = 0;
-  p->visited_removed = 0;
-  p->acceptance_removed = 0;
   xbt_dynar_free(&(p->atomic_propositions));
   xbt_free(p);
   p = NULL;
index f112c7e..9e1db34 100644 (file)
@@ -66,7 +66,7 @@ typedef struct s_mc_checkpoint_ignore_region{
 }s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
 
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
-mc_snapshot_t MC_take_snapshot(void);
+mc_snapshot_t MC_take_snapshot(int num_state);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
@@ -299,22 +299,31 @@ extern xbt_dynar_t mc_data_bss_comparison_ignore;
 
 typedef struct s_mc_pair{
   int num;
-  int other_num; /* Dot output for */
   int search_cycle;
   mc_state_t graph_state; /* System state included */
   xbt_automaton_state_t automaton_state;
   xbt_dynar_t atomic_propositions;
   int requests;
+}s_mc_pair_t, *mc_pair_t;
+
+typedef struct s_mc_visited_pair{
+  int num;
+  int other_num; /* Dot output for */
+  int acceptance_pair;
+  mc_state_t graph_state; /* System state included */
+  xbt_automaton_state_t automaton_state;
+  xbt_dynar_t atomic_propositions;
   size_t heap_bytes_used;
   int nb_processes;
-  int stack_removed;
-  int visited_removed;
   int acceptance_removed;
-}s_mc_pair_t, *mc_pair_t;
+  int visited_removed;
+}s_mc_visited_pair_t, *mc_visited_pair_t;
 
 mc_pair_t MC_pair_new(void);
 void MC_pair_delete(mc_pair_t);
 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);
index 0bf3c59..cafcd12 100644 (file)
@@ -146,7 +146,12 @@ int MSG_file_close(msg_file_t fd)
  */
 int MSG_file_unlink(msg_file_t fd)
 {
-  return simcall_file_unlink(fd->simdata->smx_file);
+  int res = simcall_file_unlink(fd->simdata->smx_file);
+  free(fd->fullname);
+  xbt_free(fd->simdata);
+  xbt_free(fd->info);
+  xbt_free(fd);
+  return res;
 }
 
 /** \ingroup msg_file_management
index ccbf9b3..6feda0f 100644 (file)
@@ -8,6 +8,7 @@
 #include "xbt/dict.h"
 #include "xbt/sysdep.h"
 #include "xbt/ex.h"
+#include "xbt/hash.h"
 #include "surf/surf.h"
 #include "simgrid/sg_config.h"
 
@@ -350,28 +351,48 @@ static void smpi_shared_alloc_free(void *p)
   xbt_free(data);
 }
 
+static char *smpi_shared_alloc_hash(char *loc)
+{
+  char hash[42];
+  char s[7];
+  unsigned val;
+  int i, j;
+
+  xbt_sha(loc, hash);
+  hash[41] = '\0';
+  s[6] = '\0';
+  loc = xbt_realloc(loc, 30);
+  loc[0] = '/';
+  for (i = 0; i < 40; i += 6) { /* base64 encode */
+    memcpy(s, hash + i, 6);
+    val = strtoul(s, NULL, 16);
+    for (j = 0; j < 4; j++) {
+      unsigned char x = (val >> (18 - 3 * j)) & 0x3f;
+      loc[1 + 4 * i / 6 + j] =
+        "ABCDEFGHIJKLMNOPQRSTUVZXYZabcdefghijklmnopqrstuvzxyz0123456789-_"[x];
+    }
+  }
+  loc[29] = '\0';
+  return loc;
+}
+
 void *smpi_shared_malloc(size_t size, const char *file, int line)
 {
-  char *loc = bprintf("%zu_%s_%d", (size_t)getpid(), file, line);
-  size_t len = strlen(loc);
-  size_t i;
-  int fd;
   void* mem;
-  shared_data_t *data;
   if (sg_cfg_get_boolean("smpi/use_shared_malloc")){
-    for(i = 0; i < len; i++) {
-      /* Make the 'loc' ID be a flat filename */
-      if(loc[i] == '/') {
-        loc[i] = '_';
-      }
-    }
+    char *loc = bprintf("%zu_%s_%d", (size_t)getpid(), file, line);
+    int fd;
+    shared_data_t *data;
+    loc = smpi_shared_alloc_hash(loc); /* hash loc, in order to have something
+                                        * not too long */
     if (!allocs) {
       allocs = xbt_dict_new_homogeneous(smpi_shared_alloc_free);
     }
     data = xbt_dict_get_or_null(allocs, loc);
-    if(!data) {
-      fd = shm_open(loc, O_RDWR | O_CREAT | O_EXCL, S_IRUSR | S_IWUSR | S_IRGRP | S_IROTH);
-      if(fd < 0) {
+    if (!data) {
+      fd = shm_open(loc, O_RDWR | O_CREAT | O_EXCL,
+                    S_IRUSR | S_IWUSR | S_IRGRP | S_IROTH);
+      if (fd < 0) {
         switch(errno) {
           case EEXIST:
             xbt_die("Please cleanup /dev/shm/%s", loc);
@@ -384,7 +405,7 @@ void *smpi_shared_malloc(size_t size, const char *file, int line)
       data->count = 1;
       data->loc = loc;
       mem = shm_map(fd, size, data);
-      if(shm_unlink(loc) < 0) {
+      if (shm_unlink(loc) < 0) {
         XBT_WARN("Could not early unlink %s: %s", loc, strerror(errno));
       }
       xbt_dict_set(allocs, loc, data, NULL);
@@ -395,7 +416,7 @@ void *smpi_shared_malloc(size_t size, const char *file, int line)
       data->count++;
     }
     XBT_DEBUG("Shared malloc %zu in %p (metadata at %p)", size, mem, data);
-  }else{
+  } else {
     mem = xbt_malloc(size);
     XBT_DEBUG("Classic malloc %zu in %p", size, mem);
   }
index e367973..6d3e23e 100644 (file)
@@ -207,8 +207,8 @@ static xbt_dict_t storage_get_content(void *storage)
   xbt_dict_t content_dict = xbt_dict_new_homogeneous(NULL);
   xbt_dict_cursor_t cursor = NULL;
   char *file;
-  char *size;
-  xbt_dict_foreach(((storage_t)storage_resource)->content, cursor, file, size){
+  sg_storage_size_t *size;
+  xbt_dict_foreach(((storage_t)st)->content, cursor, file, size){
     xbt_dict_set(content_dict,file,(void*)size,NULL);
   }
   return content_dict;
index 34026b1..d03cd89 100644 (file)
@@ -6,7 +6,7 @@
  */
 
 /* Later adapted to fit into SimGrid. Distributed under LGPL v2.1, Feb 1999.*/
-/* Copyright (c) 2008-2012. The SimGrid Team.
+/* Copyright (c) 2008-2013. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -99,7 +99,7 @@ static void xbt_sha_finalize(xbt_sha_t sha)
 /** @brief returns the sha hash into a newly allocated buffer (+ reset sha object) */
 char *xbt_sha_read(xbt_sha_t sha)
 {
-  char *res = xbt_malloc(40);
+  char *res = xbt_malloc(41);
   xbt_sha_print(sha, res);
   return res;
 }
index 33dfab5..ce305fe 100644 (file)
@@ -1,5 +1,6 @@
 #include "msg/msg.h"
 #include "xbt/log.h"
+#include "inttypes.h"
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(storage,"Messages specific for this simulation");
 
@@ -29,13 +30,13 @@ void storage_info(msg_host_t host)
 
   xbt_dict_foreach(storage_list,cursor,mount_name,storage_name)
   {
-       XBT_INFO("Storage name: %s, mount name: %s", storage_name, mount_name);
+    XBT_INFO("Storage name: %s, mount name: %s", storage_name, mount_name);
 
     sg_storage_size_t free_size = MSG_storage_get_free_size(mount_name);
     sg_storage_size_t used_size = MSG_storage_get_used_size(mount_name);
 
-    XBT_INFO("Free size: %zu bytes", free_size);
-    XBT_INFO("Used size: %zu bytes", used_size);
+    XBT_INFO("Free size: %" PRIu64 " bytes", free_size);
+    XBT_INFO("Used size: %" PRIu64 " bytes", used_size);
 
     storage = MSG_storage_get_by_name(storage_name);
     display_storage_properties(storage);
@@ -62,7 +63,7 @@ int hsm_put(const char *remote_host, const char *src, const char *dest){
   sg_storage_size_t read_size = read_local_file(src);
 
   // Send file
-  XBT_INFO("%s sends %zu to %s",MSG_host_get_name(MSG_host_self()),read_size,remote_host);
+  XBT_INFO("%s sends %" PRIu64 " to %s",MSG_host_get_name(MSG_host_self()),read_size,remote_host);
   msg_task_t to_execute = MSG_task_create((const char*)"hsm_put", 0, (double) read_size, (void*)dest);
   MSG_task_send(to_execute, remote_host);
 
@@ -85,7 +86,7 @@ sg_storage_size_t read_local_file(const char *src)
   file_size = MSG_file_get_size(file);
 
   read = MSG_file_read(file, file_size);
-  XBT_INFO("%s has read %zu on %s",MSG_host_get_name(MSG_host_self()),read,src);
+  XBT_INFO("%s has read %" PRIu64 " on %s",MSG_host_get_name(MSG_host_self()),read,src);
   MSG_file_close(file);
 
   return read;
@@ -128,9 +129,9 @@ void display_storage_content(msg_storage_t storage){
   xbt_dict_t content = MSG_storage_get_content(storage);
   if (content){
     xbt_dict_foreach(content, cursor, file, size)
-         XBT_INFO("%s size: %zu bytes", file, size);
-  }else{
-       XBT_INFO("No content.");
+    XBT_INFO("%s size: %" PRIu64 " bytes", file, size);
+  } else {
+    XBT_INFO("No content.");
   }
 }