src/xbt/mallocator_private.h
src/xbt/mmalloc/mfree.c
src/xbt/mmalloc/mm.c
- src/xbt/mmalloc/mm_diff.c
src/xbt/mmalloc/mm_legacy.c
src/xbt/mmalloc/mm_module.c
src/xbt/mmalloc/mmalloc.c
set(MC_SRC
src/mc/mc_checkpoint.c
+ src/mc/mc_diff.c
src/mc/mc_compare.c
src/mc/mc_dpor.c
src/mc/mc_dwarf.c
XBT_PUBLIC( xbt_mheap_t ) xbt_mheap_new(int fd, void *baseaddr);
+#define XBT_MHEAP_OPTION_MEMSET 1
+
+XBT_PUBLIC( xbt_mheap_t ) xbt_mheap_new_options(int fd, void *baseaddr, int options);
+
XBT_PUBLIC( void ) xbt_mheap_destroy_no_free(xbt_mheap_t md);
XBT_PUBLIC( void ) *xbt_mheap_destroy(xbt_mheap_t md);
static void MC_region_destroy(mc_mem_region_t reg)
{
- munmap(reg->data, reg->size);
+ //munmap(reg->data, reg->size);
+ xbt_free(reg->data);
xbt_free(reg);
}
mc_mem_region_t new_reg = xbt_new(s_mc_mem_region_t, 1);
new_reg->start_addr = start_addr;
new_reg->size = size;
- new_reg->data = mmap(NULL, size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
- if(new_reg->data==MAP_FAILED)
- xbt_die("Could not mmap new memory for snapshot.");
+ //new_reg->data = mmap(NULL, size, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0);
+ //if(new_reg->data==MAP_FAILED)
+ //xbt_die("Could not mmap new memory for snapshot.");
+ new_reg->data = xbt_malloc(size);
memcpy(new_reg->data, start_addr, size);
- madvise(new_reg->data, size, MADV_MERGEABLE);
+ //madvise(new_reg->data, size, MADV_MERGEABLE);
XBT_DEBUG("New region : type : %d, data : %p (real addr %p), size : %zu", type, new_reg->data, start_addr, size);
}
-
mc_snapshot_t MC_take_snapshot(int num_state){
mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
MC_dump_checkpoint_ignore(snapshot);
// mprotect the region after zero-ing ignored parts:
- size_t i;
+ /*size_t i;
for(i=0; i!=NB_REGIONS; ++i) {
mc_mem_region_t region = snapshot->regions[i];
mprotect(region->data, region->size, PROT_READ);
- }
+ }*/
return snapshot;
#include "mc_private.h"
#include "xbt/mmalloc.h"
+#include "xbt/mmalloc/mmprivate.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
"Logging specific to mc_compare");
// * a pointer leads to the read-only segment of the current object;
// * a pointer lead to a different ELF object.
- // The pointers are both in the heap:
- if(addr_pointed1 > std_heap && (char *)addr_pointed1 < (char*) std_heap + STD_HEAP_SIZE){
- if(!(addr_pointed2 > std_heap && (char *)addr_pointed2 < (char*) std_heap + STD_HEAP_SIZE))
+ if(addr_pointed1 > std_heap && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)){
+ if(!(addr_pointed2 > std_heap && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)))
return 1;
+ // The pointers are both in the heap:
return compare_heap_area(addr_pointed1, addr_pointed2, snapshot1, snapshot2, NULL, type->subtype, pointer_level);
}
-/* mm_diff - Memory snapshooting and comparison */
+/* mc_diff - Memory snapshooting and comparison */
/* Copyright (c) 2008-2014. The SimGrid Team.
* All rights reserved. */
#include "mc/datatypes.h"
#include "mc/mc_private.h"
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
- "Logging specific to mm_diff in mmalloc");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
+ "Logging specific to mc_diff in mc");
xbt_dynar_t mc_heap_comparison_ignore;
xbt_dynar_t stacks_areas;
typedef char* type_name;
-struct s_mm_diff {
- void *s_heap, *heapbase1, *heapbase2;
+struct s_mc_diff {
+ /** \brief Base address of the real heap */
+ void *s_heap;
+ /** \brief Base address of the first heap snapshot */
+ void *heapbase1;
+ /** \brief Base address of the second heap snapshot */
+ void *heapbase2;
malloc_info *heapinfo1, *heapinfo2;
size_t heaplimit;
// Number of blocks in the heaps:
#define types1_(i,j) types1[ MAX_FRAGMENT_PER_BLOCK*(i) + (j)]
#define types2_(i,j) types2[ MAX_FRAGMENT_PER_BLOCK*(i) + (j)]
-__thread struct s_mm_diff* mm_diff_info = NULL;
+__thread struct s_mc_diff* mc_diff_info = NULL;
/*********************************** Free functions ************************************/
return 0;
}
-static void match_equals(struct s_mm_diff *state, xbt_dynar_t list){
+static void match_equals(struct s_mc_diff *state, xbt_dynar_t list){
unsigned int cursor = 0;
heap_area_pair_t current_pair;
* @param b2 Block of state 2
* @return if the blocks are known to be matching
*/
-static int equal_blocks(struct s_mm_diff *state, int b1, int b2){
+static int equal_blocks(struct s_mc_diff *state, int b1, int b2){
if(state->equals_to1_(b1,0).block == b2 && state->equals_to2_(b2,0).block == b1)
return 1;
* @param f2 Fragment of state 2
* @return if the fragments are known to be matching
*/
-static int equal_fragments(struct s_mm_diff *state, int b1, int f1, int b2, int f2){
+static int equal_fragments(struct s_mc_diff *state, int b1, int f1, int b2, int f2){
if(state->equals_to1_(b1,f1).block == b2
&& state->equals_to1_(b1,f1).fragment == f2
}
int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1, xbt_dynar_t i2){
- if(mm_diff_info==NULL) {
- mm_diff_info = xbt_new0(struct s_mm_diff, 1);
- mm_diff_info->equals_to1 = NULL;
- mm_diff_info->equals_to2 = NULL;
- mm_diff_info->types1 = NULL;
- mm_diff_info->types2 = NULL;
+ if(mc_diff_info==NULL) {
+ mc_diff_info = xbt_new0(struct s_mc_diff, 1);
+ mc_diff_info->equals_to1 = NULL;
+ mc_diff_info->equals_to2 = NULL;
+ mc_diff_info->types1 = NULL;
+ mc_diff_info->types2 = NULL;
}
- struct s_mm_diff *state = mm_diff_info;
+ struct s_mc_diff *state = mc_diff_info;
if((((struct mdesc *)heap1)->heaplimit != ((struct mdesc *)heap2)->heaplimit)
|| ((((struct mdesc *)heap1)->heapsize != ((struct mdesc *)heap2)->heapsize) ))
state->heaplimit = ((struct mdesc *)heap1)->heaplimit;
+ // Mamailloute in order to find the base address of the main heap:
state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
state->heapbase1 = (char *)heap1 + BLOCKSIZE;
memset(state->types2, 0, state->heaplimit * MAX_FRAGMENT_PER_BLOCK * sizeof(type_name *));
if(MC_is_active()){
- MC_ignore_global_variable("mm_diff_info");
+ MC_ignore_global_variable("mc_diff_info");
}
return 0;
int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2, xbt_mheap_t heap1, xbt_mheap_t heap2){
- struct s_mm_diff *state = mm_diff_info;
+ struct s_mc_diff *state = mc_diff_info;
if(heap1 == NULL && heap2 == NULL){
XBT_DEBUG("Malloc descriptors null");
if(i1 == state->heaplimit){
if(state->heapinfo1[i].busy_block.busy_size > 0){
if(state->equals_to1_(i,0).valid == 0){
- if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
+ if(XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)){
addr_block1 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)state->heapbase1));
XBT_DEBUG("Block %zu (%p) not found (size used = %zu)", i, addr_block1, state->heapinfo1[i].busy_block.busy_size);
//mmalloc_backtrace_block_display((void*)heapinfo1, i);
if(i1== state->heaplimit){
if(state->heapinfo1[i].busy_frag.frag_size[j] > 0){
if(state->equals_to1_(i,j).valid == 0){
- if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
+ if(XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)){
addr_frag1 = (void*) ((char *)addr_block1 + (j << state->heapinfo1[i].type));
real_addr_frag1 = (void*) ((char *)real_addr_block1 + (j << ((struct mdesc *)state->s_heap)->heapinfo[i].type));
XBT_DEBUG("Block %zu, Fragment %zu (%p - %p) not found (size used = %zd)", i, j, addr_frag1, real_addr_frag1, state->heapinfo1[i].busy_frag.frag_size[j]);
if(i1 == state->heaplimit){
if(state->heapinfo2[i].busy_block.busy_size > 0){
if(state->equals_to2_(i,0).valid == 0){
- if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
+ if(XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)){
addr_block2 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)state->heapbase2));
XBT_DEBUG("Block %zu (%p) not found (size used = %zu)", i, addr_block2, state->heapinfo2[i].busy_block.busy_size);
//mmalloc_backtrace_block_display((void*)heapinfo2, i);
if(i1 == state->heaplimit){
if(state->heapinfo2[i].busy_frag.frag_size[j] > 0){
if(state->equals_to2_(i,j).valid == 0){
- if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
+ if(XBT_LOG_ISENABLED(mc_diff, xbt_log_priority_debug)){
addr_frag2 = (void*) ((char *)addr_block2 + (j << state->heapinfo2[i].type));
real_addr_frag2 = (void*) ((char *)real_addr_block2 + (j << ((struct mdesc *)state->s_heap)->heapinfo[i].type));
XBT_DEBUG( "Block %zu, Fragment %zu (%p - %p) not found (size used = %zd)", i, j, addr_frag2, real_addr_frag2, state->heapinfo2[i].busy_frag.frag_size[j]);
* @param size
* @param check_ignore
*/
-static int compare_heap_area_without_type(struct s_mm_diff *state, void *real_area1, void *real_area2, void *area1, void *area2, mc_snapshot_t snapshot1, mc_snapshot_t snapshot2, xbt_dynar_t previous, int size, int check_ignore){
+static int compare_heap_area_without_type(struct s_mc_diff *state, void *real_area1, void *real_area2, void *area1, void *area2, mc_snapshot_t snapshot1, mc_snapshot_t snapshot2, xbt_dynar_t previous, int size, int check_ignore){
int i = 0;
void *addr_pointed1, *addr_pointed2;
if(addr_pointed1 > maestro_stack_start && addr_pointed1 < maestro_stack_end && addr_pointed2 > maestro_stack_start && addr_pointed2 < maestro_stack_end){
i = pointer_align + sizeof(void *);
continue;
- }else if((addr_pointed1 > state->s_heap) && ((char *)addr_pointed1 < (char *)state->s_heap + STD_HEAP_SIZE)
- && (addr_pointed2 > state->s_heap) && ((char *)addr_pointed2 < (char *)state->s_heap + STD_HEAP_SIZE)){
+ }else if(addr_pointed1 > state->s_heap && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
+ && addr_pointed2 > state->s_heap && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)){
+ // Both addreses are in the heap:
res_compare = compare_heap_area(addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, NULL, 0);
if(res_compare == 1){
return res_compare;
* @param pointer_level
* @return 0 (same), 1 (different), -1 (unknown)
*/
-static int compare_heap_area_with_type(struct s_mm_diff *state, void *real_area1, void *real_area2, void *area1, void *area2,
+static int compare_heap_area_with_type(struct s_mc_diff *state, void *real_area1, void *real_area2, void *area1, void *area2,
mc_snapshot_t snapshot1, mc_snapshot_t snapshot2,
xbt_dynar_t previous, dw_type_t type,
int area_size, int check_ignore, int pointer_level){
for(i=0; i<(area_size/sizeof(void *)); i++){
addr_pointed1 = *((void **)((char *)area1 + (i*sizeof(void *))));
addr_pointed2 = *((void **)((char *)area2 + (i*sizeof(void *))));
- if(addr_pointed1 > state->s_heap && (char *)addr_pointed1 < (char*) state->s_heap + STD_HEAP_SIZE && addr_pointed2 > state->s_heap && (char *)addr_pointed2 < (char*) state->s_heap + STD_HEAP_SIZE)
+ if(addr_pointed1 > state->s_heap && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
+ && addr_pointed2 > state->s_heap && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
res = compare_heap_area(addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, type->subtype, pointer_level);
else
res = (addr_pointed1 != addr_pointed2);
}else{
addr_pointed1 = *((void **)(area1));
addr_pointed2 = *((void **)(area2));
- if(addr_pointed1 > state->s_heap && (char *)addr_pointed1 < (char*) state->s_heap + STD_HEAP_SIZE && addr_pointed2 > state->s_heap && (char *)addr_pointed2 < (char*) state->s_heap + STD_HEAP_SIZE)
+ if(addr_pointed1 > state->s_heap && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
+ && addr_pointed2 > state->s_heap && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
return compare_heap_area(addr_pointed1, addr_pointed2, snapshot1, snapshot2, previous, type->subtype, pointer_level);
else
return (addr_pointed1 != addr_pointed2);
*/
int compare_heap_area(void *area1, void* area2, mc_snapshot_t snapshot1, mc_snapshot_t snapshot2, xbt_dynar_t previous, dw_type_t type, int pointer_level){
- struct s_mm_diff* state = mm_diff_info;
+ struct s_mc_diff* state = mc_diff_info;
int res_compare;
ssize_t block1, frag1, block2, frag2;
// Not used:
static int get_pointed_area_size(void *area, int heap){
- struct s_mm_diff *state = mm_diff_info;
+ struct s_mc_diff *state = mc_diff_info;
int block, frag;
malloc_info *heapinfo;
// Not used:
int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
- struct s_mm_diff *state = mm_diff_info;
+ struct s_mc_diff *state = mc_diff_info;
if(heap1 == NULL && heap1 == NULL){
XBT_DEBUG("Malloc descriptors null");
/* Heap information */
state->heaplimit = ((struct mdesc *)heap1)->heaplimit;
+
+ // Mamailloute in order to find the base address of the main heap:
state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
state->heapbase1 = (char *)heap1 + BLOCKSIZE;
#include "mc_private.h"
+#include "xbt/mmalloc/mmprivate.h"
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
"Logging specific to MC DPOR exploration");
}
static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
+
+ if(!xbt_dynar_is_empty(incomplete_communications_pattern))
+ xbt_die("Oh oh ...");
+
unsigned int cursor = 0, send_index = 0, recv_index = 0;
mc_comm_pattern_t comm1, comm2;
int comm_comparison = 0;
}
}
-static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){
mc_comm_pattern_t current_pattern;
unsigned int cursor = 0;
int index;
+ int completed = 0;
+ void *addr_pointed;
xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){
current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t);
- if(current_pattern->comm == pattern->comm){
- current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
- current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
- current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
- current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
+ if(current_pattern->comm == comm){
+ current_pattern->src_proc = comm->comm.src_proc->pid;
+ current_pattern->dst_proc = comm->comm.dst_proc->pid;
+ current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
+ current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
if(current_pattern->data_size == -1){
- current_pattern->data_size = pattern->comm->comm.src_buff_size;
+ current_pattern->data_size = *(comm->comm.dst_buff_size);
current_pattern->data = xbt_malloc0(current_pattern->data_size);
- memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
+ addr_pointed = *(void **)comm->comm.src_buff;
+ if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
+ memcpy(current_pattern->data, addr_pointed, current_pattern->data_size);
+ else
+ memcpy(current_pattern->data, comm->comm.src_buff, current_pattern->data_size);
}
- current_pattern->matched_comm = pattern->num;
- current_pattern->completed = 1;
xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
- return current_pattern->num;
+ completed++;
+ if(completed == 2)
+ return;
+ cursor--;
}
}
- return -1;
}
void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
mc_comm_pattern_t pattern = NULL;
pattern = xbt_new0(s_mc_comm_pattern_t, 1);
pattern->num = ++nb_comm_pattern;
- pattern->completed = 0;
pattern->data_size = -1;
+ void * addr_pointed;
if(call == 1){ // ISEND
pattern->comm = simcall_comm_isend__get__result(request);
pattern->type = SIMIX_COMM_SEND;
- if(pattern->comm->comm.dst_proc != NULL){
- pattern->matched_comm = complete_comm_pattern(list, pattern);
- pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
- pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
- pattern->completed = 1;
- }
pattern->src_proc = pattern->comm->comm.src_proc->pid;
pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
pattern->data_size = pattern->comm->comm.src_buff_size;
- pattern->data=xbt_malloc0(pattern->data_size);
- memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+ pattern->data = xbt_malloc0(pattern->data_size);
+ addr_pointed = *(void **)pattern->comm->comm.src_buff;
+ if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
+ memcpy(pattern->data, addr_pointed, pattern->data_size);
+ else
+ memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
}else{ // IRECV
pattern->comm = simcall_comm_irecv__get__result(request);
pattern->type = SIMIX_COMM_RECEIVE;
- if(pattern->comm->comm.src_proc != NULL){
- pattern->matched_comm = complete_comm_pattern(list, pattern);
- pattern->src_proc = pattern->comm->comm.src_proc->pid;
- pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
- pattern->completed = 1;
- pattern->data_size = pattern->comm->comm.src_buff_size;
- pattern->data=xbt_malloc0(pattern->data_size);
- memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
- }
pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
}
xbt_dynar_push(list, &pattern);
- if(!pattern->completed)
- xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
+ xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
}
mc_comm_pattern_t current_comm;
xbt_dynar_foreach(comms_pattern, cursor, current_comm){
if(current_comm->type == SIMIX_COMM_SEND)
- XBT_INFO("[(%lu) %s -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend");
+ XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend");
else
- XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv");
+ XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, current_comm->src_host, "iRecv");
}
}
XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used);
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
int cursor = 0, previous_cursor, next_cursor;
mc_visited_state_t state_test;
next_cursor++;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return -1;
}
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return cursor;
}
if(_sg_mc_visited == 0)
return -1;
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
mc_visited_state_t new_state = visited_state_new();
xbt_dynar_push(visited_states, &new_state);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return -1;
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_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return new_state->other_num;
}*/
xbt_dynar_insert_at(visited_states, cursor, &new_state);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return new_state->other_num;
}
cursor++;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return -1;
void MC_dpor_init()
{
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
mc_state_t initial_state = NULL;
smx_process_t process;
/* Create the initial state and push it into the exploration stack */
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
initial_state = MC_state_new();
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
MC_ignore_heap(simix_global->process_to_run->data, 0);
MC_ignore_heap(simix_global->process_that_ran->data, 0);
- MC_SET_RAW_MEM;
+ 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_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
else
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
int enabled = 0;
int interleave_size = 0;
int comm_pattern = 0;
+ smx_action_t current_comm;
while (xbt_fifo_size(mc_stack_safety) > 0) {
xbt_free(req_str);
}
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(dot_output != NULL)
req_str = MC_request_get_dot_output(req, value);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
if(mc_reduce_kind == e_mc_reduce_dpor){
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
char *key = bprintf("%lu", req->issuer->pid);
xbt_dict_remove(first_enabled_state, key);
xbt_free(key);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
+ /* TODO : handle test and testany simcalls */
if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
if(req->call == SIMCALL_COMM_ISEND)
comm_pattern = 1;
else if(req->call == SIMCALL_COMM_IRECV)
comm_pattern = 2;
+ else if(req->call == SIMCALL_COMM_WAIT)
+ comm_pattern = 3;
+ else if(req->call == SIMCALL_COMM_WAITANY)
+ comm_pattern = 4;
}
/* Answer the request */
SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
- MC_SET_RAW_MEM;
- if(comm_pattern != 0){
+ MC_SET_MC_HEAP;
+ if(comm_pattern == 1 || comm_pattern == 2){
if(!initial_state_safety->initial_communications_pattern_done)
get_comm_pattern(initial_communications_pattern, req, comm_pattern);
else
get_comm_pattern(communications_pattern, req, comm_pattern);
+ }else if(comm_pattern == 3){
+ current_comm = simcall_comm_wait__get__comm(req);
+ if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+ if(!initial_state_safety->initial_communications_pattern_done)
+ complete_comm_pattern(initial_communications_pattern, current_comm);
+ else
+ complete_comm_pattern(communications_pattern, current_comm);
+ }
+ }else if(comm_pattern == 4){
+ current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+ if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+ if(!initial_state_safety->initial_communications_pattern_done)
+ complete_comm_pattern(initial_communications_pattern, current_comm);
+ else
+ complete_comm_pattern(communications_pattern, current_comm);
+ }
}
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
comm_pattern = 0;
}
MC_wait_for_requests();
/* Create the new expanded state */
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
next_state = MC_state_new();
if(dot_output != NULL)
xbt_free(req_str);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
/* Let's loop again */
}
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
if(initial_state_safety->initial_communications_pattern_done){
MC_state_delete(state);
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
/* Check for deadlocks */
if(MC_deadlock_check()){
return;
}
- MC_SET_RAW_MEM;
+ 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
state that executed that previous request. */
while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
- if(mc_reduce_kind != e_mc_reduce_none){
+ if(mc_reduce_kind == e_mc_reduce_dpor){
req = MC_state_get_internal_request(state);
xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
if(state->system_state != NULL){
MC_restore_snapshot(state->system_state);
xbt_fifo_unshift(mc_stack_safety, state);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}else{
pos = xbt_fifo_size(mc_stack_safety);
item = xbt_fifo_get_first_item(mc_stack_safety);
}
MC_restore_snapshot(restored_state->system_state);
xbt_fifo_unshift(mc_stack_safety, state);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_replay(mc_stack_safety, pos);
}
}else{
xbt_fifo_unshift(mc_stack_safety, state);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_replay(mc_stack_safety, -1);
}
XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
MC_state_delete(state);
}
}
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
}
MC_print_statistics(mc_stats);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return;
}
}
void mc_dwarf_expression_init(mc_expression_t expression, size_t len, Dwarf_Op* ops) {
- if(expression->ops) {
- free(expression->ops);
- }
expression->lowpc = NULL;
expression->highpc = NULL;
expression->size = len;
}
void mc_dwarf_location_list_init_from_expression(mc_location_list_t target, size_t len, Dwarf_Op* ops) {
- if(target->locations) {
- mc_dwarf_location_list_clear(target);
- }
target->size = 1;
target->locations = (mc_expression_t) xbt_malloc(sizeof(s_mc_expression_t));
mc_dwarf_expression_init(target->locations, len, ops);
void MC_ignore_heap(void *address, size_t size){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
mc_heap_ignore_region_t region = NULL;
region = xbt_new0(s_mc_heap_ignore_region_t, 1);
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(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return;
}
if(current_region->address == address){
heap_ignore_region_free(region);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return;
}else if(current_region->address < address){
start = cursor + 1;
xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_remove_ignore_heap(void *address, size_t size){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
unsigned int cursor = 0;
int start = 0;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_ignore_global_variable(const char *name){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized");
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
/** \brief Ignore a local variable in a scope
void MC_ignore_local_variable(const char *var_name, const char *frame_name){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
if(strcmp(frame_name, "*") == 0)
frame_name = NULL;
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
MC_ignore_local_variable_in_object(var_name, frame_name, mc_libsimgrid_info);
if(frame_name!=NULL)
MC_ignore_local_variable_in_object(var_name, frame_name, mc_binary_info);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(stacks_areas == NULL)
stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
xbt_dynar_push(stacks_areas, ®ion);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_ignore(void *addr, size_t size){
- int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set= (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(mc_checkpoint_ignore == NULL)
mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
if(current_region->size == size){
checkpoint_ignore_region_free(region);
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return;
}else if(current_region->size < size){
start = cursor + 1;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
/******************************* Initialisation of MC *******************************/
void MC_init(){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
compare = 0;
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
MC_init_memory_map_info();
MC_init_debug_info();
/* Init parmap */
parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
/* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
MC_ignore_local_variable("e", "*");
}
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
}
void MC_do_the_modelcheck_for_real() {
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
if (mc_reduce_kind==e_mc_reduce_unset)
void MC_modelcheck_safety(void)
{
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
/* Check if MC is already initialized */
if (initial_state_safety)
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
/* Initialize statistics */
mc_stats = xbt_new0(s_mc_stats_t, 1);
if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
MC_init_dot_output();
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if(_sg_mc_visited > 0){
MC_init();
}else{
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
MC_init_memory_map_info();
MC_init_debug_info();
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
MC_dpor_init();
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
/* Save the initial state */
initial_state_safety = xbt_new0(s_mc_global_t, 1);
initial_state_safety->snapshot = MC_take_snapshot(0);
initial_state_safety->initial_communications_pattern_done = 0;
initial_state_safety->comm_deterministic = 1;
initial_state_safety->send_deterministic = 1;
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_dpor();
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
xbt_abort();
//MC_exit();
void MC_modelcheck_liveness(){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
MC_init();
/* mc_time refers to clock for each process -> ignore it for heap comparison */
MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
/* Initialize statistics */
mc_stats = xbt_new0(s_mc_stats_t, 1);
if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
MC_init_dot_output();
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_ddfs_init();
xbt_free(mc_time);
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
}
*/
void MC_replay(xbt_fifo_t stack, int start)
{
- int raw_mem = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem = (mmalloc_get_current_heap() == mc_heap);
int value, i = 1, count = 1;
char *req_str;
mc_state_t state;
smx_process_t process = NULL;
int comm_pattern = 0;
+ smx_action_t current_comm;
XBT_DEBUG("**** Begin Replay ****");
MC_restore_snapshot(initial_state_safety->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_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
start_item = xbt_fifo_get_last_item(stack);
}
}
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(mc_reduce_kind == e_mc_reduce_dpor){
xbt_dict_reset(first_enabled_state);
xbt_dynar_reset(incomplete_communications_pattern);
}
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
/* Traverse the stack from the state at position start and re-execute the transitions */
saved_req = MC_state_get_executed_request(state, &value);
if(mc_reduce_kind == e_mc_reduce_dpor){
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
char *key = bprintf("%lu", saved_req->issuer->pid);
xbt_dict_remove(first_enabled_state, key);
xbt_free(key);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
if(saved_req){
XBT_DEBUG("Replay: %s (%p)", req_str, state);
xbt_free(req_str);
}
- }
- if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
- if(req->call == SIMCALL_COMM_ISEND)
- comm_pattern = 1;
- else if(req->call == SIMCALL_COMM_IRECV)
- comm_pattern = 2;
- }
+ /* TODO : handle test and testany simcalls */
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+ if(req->call == SIMCALL_COMM_ISEND)
+ comm_pattern = 1;
+ else if(req->call == SIMCALL_COMM_IRECV)
+ comm_pattern = 2;
+ else if(req->call == SIMCALL_COMM_WAIT)
+ comm_pattern = 3;
+ else if(req->call == SIMCALL_COMM_WAITANY)
+ comm_pattern = 4;
+ }
- SIMIX_simcall_pre(req, value);
+ SIMIX_simcall_pre(req, value);
- if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
- MC_SET_RAW_MEM;
- if(comm_pattern != 0){
- get_comm_pattern(communications_pattern, req, comm_pattern);
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+ MC_SET_MC_HEAP;
+ if(comm_pattern == 1 || comm_pattern == 2){
+ get_comm_pattern(communications_pattern, req, comm_pattern);
+ }else if (comm_pattern == 3/* || comm_pattern == 4*/){
+ current_comm = simcall_comm_wait__get__comm(req);
+ if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+ complete_comm_pattern(communications_pattern, current_comm);
+ }
+ }else if (comm_pattern == 4/* || comm_pattern == 4*/){
+ current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+ if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+ complete_comm_pattern(communications_pattern, current_comm);
+ }
+ }
+ MC_SET_STD_HEAP;
+ comm_pattern = 0;
}
- MC_UNSET_RAW_MEM;
- comm_pattern = 0;
- }
- MC_wait_for_requests();
-
- count++;
-
- if(mc_reduce_kind == e_mc_reduce_dpor){
- MC_SET_RAW_MEM;
- /* Insert in dict all enabled processes */
- xbt_swag_foreach(process, simix_global->process_list){
- if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
- char *key = bprintf("%lu", process->pid);
- if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
- char *data = bprintf("%d", count);
- xbt_dict_set(first_enabled_state, key, data, NULL);
+
+ MC_wait_for_requests();
+
+ count++;
+
+ if(mc_reduce_kind == e_mc_reduce_dpor){
+ MC_SET_MC_HEAP;
+ /* Insert in dict all enabled processes */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+ char *key = bprintf("%lu", process->pid);
+ if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ }
+ xbt_free(key);
}
- xbt_free(key);
}
+ MC_SET_STD_HEAP;
}
- MC_UNSET_RAW_MEM;
}
/* Update statistics */
XBT_DEBUG("**** End Replay ****");
if(raw_mem)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
else
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
{
- initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
int value;
char *req_str;
/* 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_state_liveness->raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if(all_stack){
XBT_DEBUG("**** End Replay ****");
if(initial_state_liveness->raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
else
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_dump_stack_safety(xbt_fifo_t stack)
{
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
MC_show_stack_safety(stack);
mc_state_t state;
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
MC_state_delete(state);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
else
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_show_stack_safety(xbt_fifo_t stack)
{
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
int value;
mc_state_t state;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_show_deadlock(smx_simcall_t req)
void MC_dump_stack_liveness(xbt_fifo_t stack){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
mc_pair_t pair;
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
MC_pair_delete(pair);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
}
XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
}
XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
fprintf(dot_output, "}\n");
fclose(dot_output);
if (_sg_mc_send_determinism)
XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
}
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
void MC_assert(int prop)
void MC_automaton_load(const char *file){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
xbt_automaton_load(_mc_property_automaton,file);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
}
void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if (_mc_property_automaton == NULL)
_mc_property_automaton = xbt_automaton_new();
xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
if(raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
}
*/
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);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
int cursor = 0, previous_cursor, next_cursor;
mc_visited_pair_t pair_test;
next_cursor++;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return -1;
}
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return cursor;
}
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);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
mc_visited_pair_t pair = NULL;
pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
/*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_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
}*/
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;
+ MC_SET_STD_HEAP;
return NULL;
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return pair;
static void remove_acceptance_pair(int pair_num){
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
unsigned int cursor = 0;
mc_visited_pair_t pair_test = NULL;
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
/** \brief Checks whether a given state has already been visited by the algorithm.
if(_sg_mc_visited == 0)
return -1;
- int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
mc_visited_pair_t new_pair = NULL;
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return pair->other_num;
}*/
cursor = min;
MC_visited_pair_delete(pair_test);
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return new_pair->other_num;
}
}
}
if(!raw_mem_set)
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
return -1;
}
void MC_ddfs_init(void){
- initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+ initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
XBT_DEBUG("**************************************************");
XBT_DEBUG("Double-DFS init");
MC_ignore_heap(simix_global->process_to_run->data, 0);
MC_ignore_heap(simix_global->process_that_ran->data, 0);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
initial_state_liveness->snapshot = MC_take_snapshot(0);
initial_state_liveness->prev_pair = 0;
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
unsigned int cursor = 0;
xbt_automaton_state_t automaton_state;
xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
if(automaton_state->type == -1){ /* Initial automaton state */
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
initial_pair = MC_pair_new();
initial_pair->automaton_state = automaton_state;
xbt_fifo_unshift(mc_stack_liveness, initial_pair);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_ddfs();
if(cursor != 0){
MC_restore_snapshot(initial_state_liveness->snapshot);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
}
}
if(initial_state_liveness->raw_mem_set)
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
else
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
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;
+ MC_SET_STD_HEAP;
}else{
while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(dot_output != NULL){
if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
}
initial_state_liveness->prev_pair = current_pair->num;
}
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
/* Debug information */
if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
xbt_free(req_str);
}
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
if(dot_output != NULL){
initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
if(current_pair->search_cycle)
fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
}
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
MC_state_set_executed_request(current_pair->graph_state, req, value);
mc_stats->executed_transitions++;
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
prop_values = get_atomic_propositions_values();
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
int new_pair = 0;
if(new_pair)
MC_replay_liveness(mc_stack_liveness, 1);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
next_pair = MC_pair_new();
next_pair->graph_state = MC_state_new();
if(mc_stats->expanded_pairs%1000000 == 0)
XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
new_pair = 1;
if(new_pair)
MC_replay_liveness(mc_stack_liveness, 1);
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
next_pair = MC_pair_new();
next_pair->graph_state = MC_state_new();
if(mc_stats->expanded_pairs%1000000 == 0)
XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
new_pair = 1;
}
- MC_SET_RAW_MEM;
+ MC_SET_MC_HEAP;
xbt_dynar_free(&prop_values);
current_pair = xbt_fifo_shift(mc_stack_liveness);
if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
}
MC_pair_delete(current_pair);
- MC_UNSET_RAW_MEM;
+ MC_SET_STD_HEAP;
}
/* Pointers to each of the heap regions to use */
void *std_heap = NULL; /* memory erased each time the MC stuff rollbacks to the beginning. Almost everything goes here */
-void *raw_heap = NULL; /* memory persistent over the MC rollbacks. Only MC stuff should go there */
+void *mc_heap = NULL; /* memory persistent over the MC rollbacks. Only MC stuff should go there */
/* Initialize the model-checker memory subsystem */
-/* It creates the two heap regions: std_heap and raw_heap */
+/* It creates the two heap regions: std_heap and mc_heap */
void MC_memory_init()
{
/* Create the first region HEAP_OFFSET bytes after the heap break address */
#if defined HAVE_GNU_LD && !defined MMALLOC_WANT_OVERRIDE_LEGACY
/* use the system malloc for the model-checker data */
- raw_heap = NULL;
+ mc_heap = NULL;
#else
/* Create the second region a page after the first one ends + safety gap */
- raw_heap = xbt_mheap_new(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize);
- xbt_assert(raw_heap != NULL);
+ mc_heap = xbt_mheap_new_options(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize, 0);
+ xbt_assert(mc_heap != NULL);
#endif
}
MC_free_object_info(&mc_binary_info);
MC_free_object_info(&mc_libsimgrid_info);
- if (raw_heap)
- xbt_mheap_destroy(raw_heap);
+ if (mc_heap)
+ xbt_mheap_destroy(mc_heap);
}
#include "xbt/function_types.h"
#include "xbt/mmalloc.h"
#include "../simix/smx_private.h"
+#include "../xbt/mmalloc/mmprivate.h"
#include "xbt/automaton.h"
#include "xbt/hash.h"
#include "msg/msg.h"
size_t size;
}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
+inline static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
+ if(snapshot==NULL)
+ xbt_die("snapshot is NULL");
+ xbt_mheap_t heap = (xbt_mheap_t)snapshot->regions[0]->data;
+ return heap->breakval;
+}
+
mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
mc_snapshot_t MC_take_snapshot(int num_state);
void MC_restore_snapshot(mc_snapshot_t);
/* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */
extern void *std_heap;
-extern void *raw_heap;
+extern void *mc_heap;
/* FIXME: Horrible hack! because the mmalloc library doesn't provide yet of */
/* size_t bytes_free; /\* Byte total of chunks in the free list. *\/ */
/* }; */
-#define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap)
-#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
+#define MC_SET_MC_HEAP mmalloc_set_current_heap(mc_heap)
+#define MC_SET_STD_HEAP mmalloc_set_current_heap(std_heap)
/******************************* MEMORY MAPPINGS ***************************/
int num;
smx_action_t comm;
e_smx_comm_type_t type;
- int completed;
unsigned long src_proc;
unsigned long dst_proc;
const char *src_host;
char *rdv;
ssize_t data_size;
void *data;
- int matched_comm;
}s_mc_comm_pattern_t, *mc_comm_pattern_t;
extern xbt_dynar_t communications_pattern;
extern xbt_dynar_t incomplete_communications_pattern;
void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
/* *********** Sets *********** */
XBT_LOG_CONNECT(xbt);
XBT_LOG_CONNECT(graphxml_parse);
XBT_LOG_CONNECT(log);
-#if HAVE_MMALLOC
- XBT_LOG_CONNECT(mm_diff);
-#endif
XBT_LOG_CONNECT(module);
XBT_LOG_CONNECT(peer);
XBT_LOG_CONNECT(replay);
XBT_LOG_CONNECT(mc_memory);
XBT_LOG_CONNECT(mc_memory_map);
XBT_LOG_CONNECT(mc_request);
+ XBT_LOG_CONNECT(mc_diff);
#endif
/* msg */
#include "mmorecore.c"
#include "mm_legacy.c"
#include "mm_module.c"
-#include "mm_diff.c"
static char junkareas[MAX_JUNK_AREAS][JUNK_SIZE];
/* This version use mmalloc if there is a current heap, or the legacy implem if not */
-void *malloc(size_t n) {
+static void *malloc_or_calloc(size_t n, int setzero) {
xbt_mheap_t mdp = __mmalloc_current_heap;
void *ret;
#ifdef MM_LEGACY_VERBOSE
LOCK(mdp);
ret = mmalloc(mdp, n);
UNLOCK(mdp);
+ // This was already done by mmalloc:
+ if (mdp->options & XBT_MHEAP_OPTION_MEMSET) {
+ setzero = 0;
+ }
#ifdef MM_LEGACY_VERBOSE
if (!warned_mmalloc) {
fprintf(stderr,"Using mmalloc; enabling the model-checker in cmake may have a bad impact on your simulation performance\n");
warned_mmalloc = 1;
}
#endif
- } else {
- if (!real_malloc) {
+ } else if (!real_malloc) {
size_t needed_areas = n / JUNK_SIZE;
if(needed_areas * JUNK_SIZE != n) needed_areas++;
if (allocated_junk+needed_areas>=MAX_JUNK_AREAS) {
} else {
size_t i = allocated_junk;
allocated_junk += needed_areas;
- return junkareas[i];
+ ret = junkareas[i];
}
}
+ else {
#ifdef MM_LEGACY_VERBOSE
if (!warned_raw) {
fprintf(stderr,"Using system malloc after interception; you seem to be currently model-checking\n");
#endif
ret = real_malloc(n);
}
+ if (ret && setzero) {
+ memset(ret, 0, n);
+ }
return ret;
}
+void *malloc(size_t n)
+{
+ return malloc_or_calloc(n, 0);
+}
void *calloc(size_t nmemb, size_t size)
{
- void *ret = malloc(nmemb*size);
- memset(ret, 0, nmemb * size);
- return ret;
+ return malloc_or_calloc(nmemb*size, 1);
}
void *realloc(void *p, size_t s)
On failure returns NULL. */
xbt_mheap_t xbt_mheap_new(int fd, void *baseaddr)
+{
+ return xbt_mheap_new_options(fd, baseaddr, 0);
+}
+
+xbt_mheap_t xbt_mheap_new_options(int fd, void *baseaddr, int options)
{
struct mdesc mtemp;
xbt_mheap_t mdp;
mdp->base = mdp->breakval = mdp->top = baseaddr;
mdp->next_mdesc = NULL;
mdp->refcount = 1;
+ mdp->options = options;
/* If we have not been passed a valid open file descriptor for the file
to map to, then we go for an anonymous map */
if (__mmalloc_default_mdp == NULL) {
unsigned long mask = ~((unsigned long)xbt_pagesize - 1);
void *addr = (void*)(((unsigned long)sbrk(0) + HEAP_OFFSET) & mask);
- __mmalloc_default_mdp = xbt_mheap_new(-1, addr);
+ __mmalloc_default_mdp = xbt_mheap_new_options(-1, addr, XBT_MHEAP_OPTION_MEMSET);
/* Fixme? only the default mdp in protected against forks */
// This is mandated to protect the mmalloced areas through forks. Think of tesh.
// Nah, removing the mutex isn't a good idea either for tesh
/* Allocate memory from the heap. */
void *mmalloc(xbt_mheap_t mdp, size_t size) {
void *res= mmalloc_no_memset(mdp,size);
-// fprintf(stderr,"malloc(%zu)~>%p\n",size,res);
- memset(res,0,size);
+ if (mdp->options & XBT_MHEAP_OPTION_MEMSET) {
+ memset(res,0,size);
+ }
return res;
}
/* Spliting mmalloc this way is mandated by a trick in mrealloc, that gives
/* The version number of the mmalloc package that created this file. */
unsigned char version;
+ unsigned int options;
+
/* Some flag bits to keep track of various internal things. */
unsigned int flags;
void *breakval;
/* The end of the current memory region for this malloc heap. This is
- the first location past the end of mapped memory. */
+ the first location past the end of mapped memory.
+ Compared to breakval, this value is rounded to the next memory page.
+ */
void *top;