- mc_snapshot_t state_test = NULL;
-
- xbt_dynar_foreach(visited_states, cursor, state_test){
- if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
- XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
- if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
- if(raw_mem_set)
- MC_SET_RAW_MEM;
- else
- MC_UNSET_RAW_MEM;
-
- return 1;
- }
+ int previous_cursor = 0, next_cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(visited_states) - 1;
+
+ mc_safety_visited_state_t state_test = NULL;
+ size_t chunks_used_test;
+ int same_chunks_not_found = 1;
+
+ while(start <= end && same_chunks_not_found){
+ cursor = (start + end) / 2;
+ state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
+ chunks_used_test = state_test->system_state->heap_chunks_used;
+ if(chunks_used_test < current_chunks_used)
+ start = cursor + 1;
+ if(chunks_used_test > current_chunks_used)
+ end = cursor - 1;
+ if(chunks_used_test == current_chunks_used){
+ same_chunks_not_found = 0;
+ if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
+ xbt_dynar_remove_at(visited_states, cursor, NULL);
+ xbt_dynar_insert_at(visited_states, cursor, &new_state);
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }else{
+ /* Search another state with same number of chunks used */
+ previous_cursor = cursor - 1;
+ while(previous_cursor >= 0){
+ state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
+ chunks_used_test = state_test->system_state->heap_chunks_used;
+ if(chunks_used_test != current_chunks_used)
+ break;
+ if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
+ xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
+ xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ previous_cursor--;
+ }
+ next_cursor = cursor + 1;
+ while(next_cursor < xbt_dynar_length(visited_states)){
+ state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
+ chunks_used_test = state_test->system_state->heap_chunks_used;
+ if(chunks_used_test != current_chunks_used)
+ break;
+ if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
+ xbt_dynar_remove_at(visited_states, next_cursor, NULL);
+ xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ next_cursor++;
+ }
+ }
+ }