src/mc/mc_dwarf_tagnames.h
src/mc/mc_hash.cpp
src/mc/mc_ignore.cpp
+ src/mc/mcer_ignore.cpp
+ src/mc/mcer_ignore.h
src/mc/mc_ignore.h
src/mc/mc_liveness.h
src/mc/mc_location.h
// Lookup the host name in the dictionary (or create it):
xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
if (!elt) {
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
xbt_dict_set(this->hostnames_, hostname, NULL, NULL);
elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
assert(elt);
- mmalloc_set_current_heap(heap);
}
return elt->key;
}
message.size = size;
MC_client_send_message(&message, sizeof(message));
}
-
- // TODO, remove this once the migration has been completed
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- MC_process_ignore_memory(&mc_model_checker->process(), addr, size);
- mmalloc_set_current_heap(heap);
}
}
static void MC_pre_modelcheck_comm_determinism(void)
{
- MC_SET_MC_HEAP;
-
mc_state_t initial_state = NULL;
smx_process_t process;
int i;
}
initial_state = MC_state_new();
- MC_SET_STD_HEAP;
XBT_DEBUG("********* Start communication determinism verification *********");
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
- MC_SET_MC_HEAP;
-
/* Get an enabled process and insert it in the interleave set of the initial state */
MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
);
xbt_fifo_unshift(mc_stack, initial_state);
-
- MC_SET_STD_HEAP;
-
}
static void MC_modelcheck_comm_determinism_main(void)
xbt_free(req_str);
if (dot_output != NULL) {
- MC_SET_MC_HEAP;
req_str = MC_request_get_dot_output(req, value);
- MC_SET_STD_HEAP;
}
MC_state_set_executed_request(state, req, value);
/* Answer the request */
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_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
else
MC_handle_comm_pattern(call, req, value, NULL, 0);
- MC_SET_STD_HEAP;
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
/* Create the new expanded state */
- MC_SET_MC_HEAP;
-
next_state = MC_state_new();
if ((visited_state = is_visited_state(next_state)) == NULL) {
if (dot_output != NULL)
xbt_free(req_str);
- MC_SET_STD_HEAP;
-
} else {
if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
}
- MC_SET_MC_HEAP;
-
if (!initial_global_state->initial_communications_pattern_done)
initial_global_state->initial_communications_pattern_done = 1;
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
- MC_SET_STD_HEAP;
-
visited_state = NULL;
/* Check for deadlocks */
return;
}
- MC_SET_MC_HEAP;
-
while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) {
if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
MC_replay(mc_stack);
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
}
}
-
- MC_SET_STD_HEAP;
}
}
MC_print_statistics(mc_stats);
- MC_SET_STD_HEAP;
-
exit(0);
}
MC_client_handle_messages();
}
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
/* Create exploration stack */
mc_stack = xbt_fifo_new();
- MC_SET_STD_HEAP;
-
MC_pre_modelcheck_comm_determinism();
- MC_SET_MC_HEAP;
initial_global_state = xbt_new0(s_mc_global_t, 1);
initial_global_state->snapshot = MC_take_snapshot(0);
initial_global_state->initial_communications_pattern_done = 0;
initial_global_state->recv_diff = NULL;
initial_global_state->send_diff = NULL;
- MC_SET_STD_HEAP;
-
MC_modelcheck_comm_determinism_main();
-
- mmalloc_set_current_heap(heap);
}
}
/* Init parmap */
//parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
/* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
MC_restore_snapshot(state->system_state);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_restore_communications_pattern(state);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
return;
}
}
MC_restore_snapshot(initial_global_state->snapshot);
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
start_item = xbt_fifo_get_last_item(stack);
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
// int n = xbt_dynar_length(incomplete_communications_pattern);
}
}
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
/* Traverse the stack from the state at position start and re-execute the transitions */
for (item = start_item;
MC_simcall_handle(req, value);
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, value, NULL, 1);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
MC_wait_for_requests();
pair = (mc_pair_t) xbt_fifo_get_item_content(item);
if(pair->graph_state->system_state){
MC_restore_snapshot(pair->graph_state->system_state);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
return;
}
}
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
if (!initial_global_state->raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
/* Traverse the stack from the initial state and re-execute the transitions */
for (item = xbt_fifo_get_last_item(stack);
XBT_DEBUG("**** End Replay ****");
if (initial_global_state->raw_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
else
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
}
mc_state_t state;
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
mmalloc_set_current_heap(heap);
// structure but they are currently used before the MC initialisation
// (in standalone mode).
-extern xbt_dynar_t mc_heap_comparison_ignore;
+
extern xbt_dynar_t stacks_areas;
/**************************** Structures ******************************/
/***********************************************************************/
-// Mcer
-void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
+// ***** Model-checked
+
+void MC_ignore_heap(void *address, size_t size)
{
- if (mc_heap_comparison_ignore == NULL) {
- mc_heap_comparison_ignore =
- xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
- heap_ignore_region_free_voidp);
- xbt_dynar_push(mc_heap_comparison_ignore, ®ion);
+ if (mc_mode != MC_MODE_CLIENT)
return;
- }
- unsigned int cursor = 0;
- mc_heap_ignore_region_t current_region = NULL;
- int start = 0;
- int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
-
- // Find the position where we want to insert the mc_heap_ignore_region_t:
- while (start <= end) {
- cursor = (start + end) / 2;
- current_region =
- (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
- cursor,
- mc_heap_ignore_region_t);
- if (current_region->address == region->address) {
- heap_ignore_region_free(region);
- return;
- } else if (current_region->address < region->address) {
- start = cursor + 1;
- } else {
- end = cursor - 1;
- }
+ s_mc_heap_ignore_region_t region;
+ memset(®ion, 0, sizeof(region));
+ region.address = address;
+ region.size = size;
+ region.block =
+ ((char *) address -
+ (char *) std_heap->heapbase) / BLOCKSIZE + 1;
+ if (std_heap->heapinfo[region.block].type == 0) {
+ region.fragment = -1;
+ std_heap->heapinfo[region.block].busy_block.ignore++;
+ } else {
+ region.fragment =
+ ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap->
+ heapinfo[region.block].type;
+ std_heap->heapinfo[region.block].busy_frag.ignore[region.fragment]++;
}
- // Insert it mc_heap_ignore_region_t:
- if (current_region->address < region->address)
- xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, ®ion);
- else
- xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
-}
-
-// MCed:
-static void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
-{
s_mc_ignore_heap_message_t message;
message.type = MC_MESSAGE_IGNORE_HEAP;
- message.region = *region;
+ message.region = region;
if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
xbt_die("Could not send ignored region to MCer");
}
-// MCed:
-void MC_ignore_heap(void *address, size_t size)
-{
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
- mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1);
- region->address = address;
- region->size = size;
-
- region->block =
- ((char *) address -
- (char *) std_heap->heapbase) / BLOCKSIZE + 1;
-
- if (std_heap->heapinfo[region->block].type == 0) {
- region->fragment = -1;
- std_heap->heapinfo[region->block].busy_block.ignore++;
- } else {
- region->fragment =
- ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap->
- heapinfo[region->block].type;
- std_heap->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
- }
-
- MC_heap_region_ignore_insert(region);
-
-#if 1
- if (mc_mode == MC_MODE_CLIENT)
- MC_heap_region_ignore_send(region);
-#endif
- mmalloc_set_current_heap(heap);
-}
-
void MC_remove_ignore_heap(void *address, size_t size)
{
- if (mc_mode == MC_MODE_CLIENT) {
- s_mc_ignore_memory_message_t message;
- message.type = MC_MESSAGE_UNIGNORE_HEAP;
- message.addr = address;
- message.size = size;
- MC_client_send_message(&message, sizeof(message));
+ if (mc_mode != MC_MODE_CLIENT)
return;
- }
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- unsigned int cursor = 0;
- int start = 0;
- int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
- mc_heap_ignore_region_t region;
- int ignore_found = 0;
-
- while (start <= end) {
- cursor = (start + end) / 2;
- region =
- (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
- cursor,
- mc_heap_ignore_region_t);
- if (region->address == address) {
- ignore_found = 1;
- break;
- } else if (region->address < address) {
- start = cursor + 1;
- } else {
- if ((char *) region->address <= ((char *) address + size)) {
- ignore_found = 1;
- break;
- } else {
- end = cursor - 1;
- }
- }
- }
-
- if (ignore_found == 1) {
- xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
- MC_remove_ignore_heap(address, size);
- }
- mmalloc_set_current_heap(heap);
+ s_mc_ignore_memory_message_t message;
+ message.type = MC_MESSAGE_UNIGNORE_HEAP;
+ message.addr = address;
+ message.size = size;
+ MC_client_send_message(&message, sizeof(message));
}
-// MCer
+// ***** Model-checker:
+
void MC_ignore_global_variable(const char *name)
{
mc_process_t process = &mc_model_checker->process();
SG_BEGIN_DECL();
-void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
void MC_stack_area_add(stack_region_t stack_area);
xbt_dynar_t MC_checkpoint_ignore_new(void);
-
SG_END_DECL();
return values;
}
-static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
+static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
+{
mc_visited_pair_t new_pair = NULL;
new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
new_pair->acceptance_pair = 1;
// Parallell implementation
/*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
if(res != -1){
- if(!raw_mem_set)
- MC_SET_STD_HEAP;
return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
} */
xbt_fifo_shift(mc_stack);
if (dot_output != NULL)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
- mmalloc_set_current_heap(heap);
return NULL;
}
}
xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
}
}
-
}
- mmalloc_set_current_heap(heap);
return new_pair;
}
static void remove_acceptance_pair(int pair_num)
{
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
unsigned int cursor = 0;
mc_visited_pair_t pair_test = NULL;
int pair_found = 0;
MC_visited_pair_delete(pair_test);
}
-
- mmalloc_set_current_heap(heap);
}
MC_wait_for_requests();
- MC_SET_MC_HEAP;
-
acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
if(_sg_mc_visited > 0)
visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
}
}
- MC_SET_STD_HEAP;
-
MC_modelcheck_liveness_main();
-
- if (initial_global_state->raw_mem_set)
- MC_SET_MC_HEAP;
}
static void MC_modelcheck_liveness_main(void)
if ((current_pair->exploration_started == 0) && (visited_num = is_visited_pair(reached_pair, current_pair)) != -1) {
if (dot_output != NULL){
- MC_SET_MC_HEAP;
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req);
fflush(dot_output);
- MC_SET_STD_HEAP;
}
XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
- MC_SET_MC_HEAP;
current_pair->requests = 0;
- MC_SET_STD_HEAP;
goto backtracking;
}else{
req = MC_state_get_request(current_pair->graph_state, &value);
if (dot_output != NULL) {
- MC_SET_MC_HEAP;
if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
xbt_free(initial_global_state->prev_req);
if (current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
fflush(dot_output);
- MC_SET_STD_HEAP;
}
char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
- MC_SET_MC_HEAP;
-
current_pair->requests--;
current_pair->exploration_started = 1;
}
cursor--;
}
-
- MC_SET_STD_HEAP;
-
+
} /* End of visited_pair test */
} else {
if(visited_num == -1)
XBT_DEBUG("No more request to execute. Looking for backtracking point.");
- MC_SET_MC_HEAP;
-
xbt_dynar_free(&prop_values);
/* Traverse the stack backwards until a pair with a non empty interleave
/* We found a backtracking point */
XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
xbt_fifo_unshift(mc_stack, current_pair);
- MC_SET_STD_HEAP;
MC_replay_liveness(mc_stack);
XBT_DEBUG("Backtracking done");
break;
MC_pair_delete(current_pair);
}
}
-
- MC_SET_STD_HEAP;
+
} /* End of if (current_pair->requests > 0) else ... */
} /* End of while(xbt_fifo_size(mc_stack) > 0) */
XBT_DEBUG("Starting the liveness algorithm");
_sg_mc_liveness = 1;
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
/* Create exploration stack */
mc_stack = xbt_fifo_new();
/* Create the initial state */
initial_global_state = xbt_new0(s_mc_global_t, 1);
- MC_SET_STD_HEAP;
-
MC_pre_modelcheck_liveness();
/* We're done */
MC_print_statistics(mc_stats);
xbt_free(mc_time);
-
- mmalloc_set_current_heap(heap);
-
}
}
/* size_t bytes_free; /\* Byte total of chunks in the free list. *\/ */
/* }; */
-#define MC_SET_MC_HEAP mmalloc_set_current_heap(mc_heap)
-#define MC_SET_STD_HEAP mmalloc_set_current_heap(std_heap)
-
SG_END_DECL()
#endif
assert(!MC_process_is_self(process));
// Read/dereference/refresh the std_heap pointer:
if (!process->heap) {
- xbt_mheap_t oldheap = mmalloc_set_current_heap(mc_heap);
process->heap = (struct mdesc*) malloc(sizeof(struct mdesc));
- mmalloc_set_current_heap(oldheap);
}
MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
process->heap, process->heap_address, sizeof(struct mdesc),
// Refresh process->heapinfo:
size_t malloc_info_bytesize =
(process->heap->heaplimit + 1) * sizeof(malloc_info);
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
process->heap_info = (malloc_info*) realloc(process->heap_info, malloc_info_bytesize);
- mmalloc_set_current_heap(heap);
-
MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
process->heap_info,
process->heap->heapinfo, malloc_info_bytesize,
*/
static void MC_pre_modelcheck_safety()
{
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
if (_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
mc_state_t initial_state = MC_state_new();
- MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
- MC_SET_MC_HEAP;
-
/* Get an enabled process and insert it in the interleave set of the initial state */
smx_process_t process;
MC_EACH_SIMIX_PROCESS(process,
);
xbt_fifo_unshift(mc_stack, initial_state);
- mmalloc_set_current_heap(heap);
}
xbt_free(req_str);
if (dot_output != NULL) {
- MC_SET_MC_HEAP;
req_str = MC_request_get_dot_output(req, value);
- MC_SET_STD_HEAP;
}
MC_state_set_executed_request(state, req, value);
MC_wait_for_requests();
/* Create the new expanded state */
- MC_SET_MC_HEAP;
-
next_state = MC_state_new();
if(_sg_mc_termination && is_exploration_stack_state(next_state)){
if (dot_output != NULL)
xbt_free(req_str);
- MC_SET_STD_HEAP;
-
/* Let's loop again */
/* The interleave set is empty or the maximum depth is reached, let's back-track */
}
- MC_SET_MC_HEAP;
-
/* Trash the current state, no longer needed */
xbt_fifo_shift(mc_stack);
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
- MC_SET_STD_HEAP;
-
visited_state = NULL;
/* Check for deadlocks */
return;
}
- MC_SET_MC_HEAP;
/* Traverse the stack backwards until a state with a non empty interleave
set is found, deleting all the states that have it empty in the way.
For each deleted state, check if the request that has generated it
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
}
}
- MC_SET_STD_HEAP;
}
}
MC_print_statistics(mc_stats);
- MC_SET_STD_HEAP;
-
return;
}
_sg_mc_safety = 1;
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
/* Create exploration stack */
mc_stack = xbt_fifo_new();
- MC_SET_STD_HEAP;
-
MC_pre_modelcheck_safety();
- MC_SET_MC_HEAP;
/* Save the initial state */
initial_global_state = xbt_new0(s_mc_global_t, 1);
initial_global_state->snapshot = MC_take_snapshot(0);
- MC_SET_STD_HEAP;
MC_modelcheck_safety_main();
- mmalloc_set_current_heap(heap);
-
xbt_abort();
//MC_exit();
}
#include "mc_server.h"
#include "mc_private.h"
#include "mc_ignore.h"
+#include "mcer_ignore.h"
extern "C" {
if (size != sizeof(message))
xbt_die("Broken messsage");
memcpy(&message, buffer, sizeof(message));
- MC_remove_ignore_heap(message.addr, message.size);
+ MC_heap_region_ignore_remove(message.addr, message.size);
break;
}
void MC_smx_process_info_clear(mc_smx_process_info_t p)
{
p->hostname = NULL;
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
free(p->name);
- mmalloc_set_current_heap(heap);
-
p->name = NULL;
}
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);
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);
}
/** Get the issuer of a simcall (`req->issuer`)
mc_smx_process_info_t info = MC_smx_process_get_info(p);
if (!info->name) {
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
info->name = MC_process_read_string(process, p->name);
- mmalloc_set_current_heap(heap);
}
return info->name;
}
*/
int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
{
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
int cursor = 0, previous_cursor;
int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
void *ref_test;
*max = next_cursor;
next_cursor++;
}
- mmalloc_set_current_heap(heap);
return -1;
}
}
}
-
- mmalloc_set_current_heap(heap);
return cursor;
}
}
}
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
mc_visited_state_t new_state = visited_state_new();
graph_state->system_state = new_state->system_state;
graph_state->in_visited_states = 1;
if (xbt_dynar_is_empty(visited_states)) {
xbt_dynar_push(visited_states, &new_state);
- mmalloc_set_current_heap(heap);
return NULL;
} else {
XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
- if(!raw_mem_set)
- MC_SET_STD_HEAP;
return new_state->other_num;
} */
xbt_dynar_insert_at(visited_states, cursor, &new_state);
XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
- mmalloc_set_current_heap(heap);
return state_test;
}
cursor++;
XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
- mmalloc_set_current_heap(heap);
return NULL;
}
}
if (_sg_mc_visited == 0)
return -1;
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
mc_visited_pair_t new_visited_pair = NULL;
if (visited_pair == NULL) {
MC_pair_delete(pair_test);
}
}
- if(!raw_mem_set)
- MC_SET_STD_HEAP;
return pair->other_num;
} */
cursor = min;
} else {
MC_visited_pair_delete(pair_test);
}
- mmalloc_set_current_heap(heap);
return new_visited_pair->other_num;
}
}
}
}
-
- mmalloc_set_current_heap(heap);
return -1;
}
--- /dev/null
+/* Copyright (c) 2008-2015. The SimGrid Team.
+ * All rights reserved. */
+
+/* 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 "internal_config.h"
+#include "mc_object_info.h"
+#include "mc/mc_private.h"
+#include "smpi/private.h"
+#include "mc/mc_snapshot.h"
+#include "mc/mc_ignore.h"
+#include "mc/mc_protocol.h"
+#include "mc/mc_client.h"
+
+extern "C" {
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mcer_ignore, mc,
+ "Logging specific to MC ignore mechanism");
+
+extern xbt_dynar_t mc_heap_comparison_ignore;
+
+void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
+{
+ if (mc_heap_comparison_ignore == NULL) {
+ mc_heap_comparison_ignore =
+ xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
+ heap_ignore_region_free_voidp);
+ xbt_dynar_push(mc_heap_comparison_ignore, ®ion);
+ return;
+ }
+
+ unsigned int cursor = 0;
+ mc_heap_ignore_region_t current_region = NULL;
+ int start = 0;
+ int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+
+ // Find the position where we want to insert the mc_heap_ignore_region_t:
+ while (start <= end) {
+ cursor = (start + end) / 2;
+ current_region =
+ (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
+ cursor,
+ mc_heap_ignore_region_t);
+ if (current_region->address == region->address) {
+ heap_ignore_region_free(region);
+ return;
+ } else if (current_region->address < region->address) {
+ start = cursor + 1;
+ } else {
+ end = cursor - 1;
+ }
+ }
+
+ // Insert it mc_heap_ignore_region_t:
+ if (current_region->address < region->address)
+ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, ®ion);
+ else
+ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
+}
+
+void MC_heap_region_ignore_remove(void *address, size_t size)
+{
+ unsigned int cursor = 0;
+ int start = 0;
+ int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+ mc_heap_ignore_region_t region;
+ int ignore_found = 0;
+
+ while (start <= end) {
+ cursor = (start + end) / 2;
+ region =
+ (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
+ cursor,
+ mc_heap_ignore_region_t);
+ if (region->address == address) {
+ ignore_found = 1;
+ break;
+ } else if (region->address < address) {
+ start = cursor + 1;
+ } else {
+ if ((char *) region->address <= ((char *) address + size)) {
+ ignore_found = 1;
+ break;
+ } else {
+ end = cursor - 1;
+ }
+ }
+ }
+
+ if (ignore_found == 1) {
+ xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
+ MC_remove_ignore_heap(address, size);
+ }
+}
+
+}
--- /dev/null
+/* Copyright (c) 2015. The SimGrid Team. All rights reserved. */
+
+/* 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 <xbt/dynar.h>
+
+#include "mc/datatypes.h"
+#include "mc/mc_process.h"
+
+#include "xbt/misc.h" /* SG_BEGIN_DECL */
+
+SG_BEGIN_DECL();
+
+void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
+void MC_heap_region_ignore_remove(void *address, size_t size);
+
+SG_END_DECL();
XBT_LOG_CONNECT(mc_dwarf);
XBT_LOG_CONNECT(mc_hash);
XBT_LOG_CONNECT(mc_ignore);
+ XBT_LOG_CONNECT(mcer_ignore);
XBT_LOG_CONNECT(mc_liveness);
XBT_LOG_CONNECT(mc_memory);
XBT_LOG_CONNECT(mc_memory_map);