while(i < maps->mapsize){
r = maps->regions[i];
if (maps->regions[i].pathname != NULL){
- if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){
- size_t diff = (char*)reg->start_addr - (char*)r.start_addr;
- void *segment = malloc(reg->size + diff);
- XBT_DEBUG("Size of segment : %zu", sizeof(segment));
- memcpy((char *)segment + diff, reg->data, reg->size);
- memcpy(r.start_addr, segment, sizeof(segment));
- XBT_DEBUG("Memcpy region ok");
- break;
- }
+ if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){
+ size_t diff = (char*)reg->start_addr - (char*)r.start_addr;
+ void *segment = malloc(reg->size + diff);
+ XBT_DEBUG("Size of segment : %zu", sizeof(segment));
+ memcpy((char *)segment + diff, reg->data, reg->size);
+ memcpy(r.start_addr, segment, sizeof(segment));
+ XBT_DEBUG("Memcpy region ok");
+ break;
+ }
}
i++;
}
if ((reg.prot & PROT_WRITE)){
if (maps->regions[i].pathname == NULL){
if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one)
- MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+ MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
}
} else {
if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
} else {
- if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
- MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
- }
- }
+ if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
+ MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+ }
+ }
}
}
i++;
MC_UNSET_RAW_MEM;
/* FIXME: Update Statistics
- mc_stats->state_size +=
- xbt_setset_set_size(initial_state->enabled_transitions); */
+ mc_stats->state_size +=
+ xbt_setset_set_size(initial_state->enabled_transitions); */
}
XBT_DEBUG("**************************************************");
XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
- xbt_fifo_size(mc_stack_safety_stateless), state,
- MC_state_interleave_size(state));
+ xbt_fifo_size(mc_stack_safety_stateless), state,
+ MC_state_interleave_size(state));
/* Update statistics */
mc_stats->visited_states++;
MC_UNSET_RAW_MEM;
/* FIXME: Update Statistics
- mc_stats->state_size +=
- xbt_setset_set_size(next_state->enabled_transitions);*/
+ mc_stats->state_size +=
+ xbt_setset_set_size(next_state->enabled_transitions);*/
/* Let's loop again */
/* Debug information */
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
- req_str = MC_request_to_string(req, value);
- //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
- XBT_DEBUG("Execute: %s",req_str);
- xbt_free(req_str);
+ req_str = MC_request_to_string(req, value);
+ //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
+ XBT_DEBUG("Execute: %s",req_str);
+ xbt_free(req_str);
}
MC_state_set_executed_request(current_state->graph_state, req, value);
/* Get an enabled process and insert it in the interleave set of the next graph_state */
xbt_swag_foreach(process, simix_global->process_list){
- if(MC_process_is_enabled(process)){
- MC_state_interleave_process(next_graph_state, process);
- break;
- }
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(next_graph_state, process);
+ break;
+ }
}
next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
MC_SET_RAW_MEM;
while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
- req = MC_state_get_internal_request(current_state->graph_state);
- xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
+ req = MC_state_get_internal_request(current_state->graph_state);
+ xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
XBT_DEBUG("Dependent Transitions:");
if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
MC_state_interleave_process(prev_state->graph_state, req->issuer);
- } else {
+ } else {
XBT_DEBUG("Process %p is in done set", req->issuer);
- }
+ }
break;
}
}
- if(MC_state_interleave_size(current_state->graph_state)){
- MC_restore_snapshot(current_state->system_state);
- xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
- MC_UNSET_RAW_MEM;
- break;
- }
+ if(MC_state_interleave_size(current_state->graph_state)){
+ MC_restore_snapshot(current_state->system_state);
+ xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
+ XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
+ MC_UNSET_RAW_MEM;
+ break;
+ }
}
MC_UNSET_RAW_MEM;
void MC_init_safety_stateful(void){
- /* Check if MC is already initialized */
+ /* Check if MC is already initialized */
if (initial_snapshot)
return;
XBT_DEBUG("Creating stack");
- /* Create exploration stack */
+ /* Create exploration stack */
mc_stack_liveness = xbt_fifo_new();
MC_UNSET_RAW_MEM;
xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
req = &process->simcall;
if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
- SIMIX_simcall_pre(req, 0);
+ SIMIX_simcall_pre(req, 0);
}
}
}
* \brief Re-executes from the initial state all the transitions indicated by
* a given model-checker stack.
* \param stack The stack with the transitions to execute.
-*/
+ */
void MC_replay(xbt_fifo_t stack)
{
int value;
if(pair->requests > 0){
- saved_req = MC_state_get_executed_request(state, &value);
- //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+ saved_req = MC_state_get_executed_request(state, &value);
+ //XBT_DEBUG("SavedReq->call %u", saved_req->call);
- if(saved_req != NULL){
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
- req = &saved_req->issuer->simcall;
- //XBT_DEBUG("Req->call %u", req->call);
+ if(saved_req != NULL){
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ req = &saved_req->issuer->simcall;
+ //XBT_DEBUG("Req->call %u", req->call);
- /* Debug information */
- if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
- req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+ xbt_free(req_str);
+ }
- }
+ }
- SIMIX_simcall_pre(req, value);
- MC_wait_for_requests();
+ SIMIX_simcall_pre(req, value);
+ MC_wait_for_requests();
}
depth++;
/* Traverse the stack from the initial state and re-execute the transitions */
for (item = xbt_fifo_get_last_item(stack);
- item != xbt_fifo_get_first_item(stack);
- item = xbt_fifo_get_prev_item(item)) {
+ item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
state = (mc_state_t) pair->graph_state;
if(pair->requests > 0){
- saved_req = MC_state_get_executed_request(state, &value);
- //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+ saved_req = MC_state_get_executed_request(state, &value);
+ //XBT_DEBUG("SavedReq->call %u", saved_req->call);
- if(saved_req != NULL){
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
- req = &saved_req->issuer->simcall;
- //XBT_DEBUG("Req->call %u", req->call);
+ if(saved_req != NULL){
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ req = &saved_req->issuer->simcall;
+ //XBT_DEBUG("Req->call %u", req->call);
- /* Debug information */
- if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
- req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+ xbt_free(req_str);
+ }
- }
+ }
- SIMIX_simcall_pre(req, value);
- MC_wait_for_requests();
+ SIMIX_simcall_pre(req, value);
+ MC_wait_for_requests();
}
depth++;
* \brief Dumps the contents of a model-checker's stack and shows the actual
* execution trace
* \param stack The stack to dump
-*/
+ */
void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
{
mc_state_t state;
XBT_INFO("**************************");
XBT_INFO("Locked request:");
/*req_str = MC_request_to_string(req);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);*/
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);*/
XBT_INFO("Counter-example execution trace:");
MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
}
XBT_INFO("**************************");
XBT_INFO("Locked request:");
/*req_str = MC_request_to_string(req);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);*/
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);*/
XBT_INFO("Counter-example execution trace:");
MC_show_stack_safety_stateful(mc_stack_safety_stateful);
}
MC_show_stack_safety_stateful(stack);
/*MC_SET_RAW_MEM;
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+ while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
MC_state_delete(state);
MC_UNSET_RAW_MEM;*/
}
req = MC_state_get_executed_request(pair->graph_state, &value);
if(req){
if(pair->requests>0){
- req_str = MC_request_to_string(req, value);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
}else{
- XBT_INFO("End of system requests but evolution in Büchi automaton");
+ XBT_INFO("End of system requests but evolution in Büchi automaton");
}
}
}
XBT_INFO("Visited states = %lu", stats->visited_states);
XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
XBT_INFO("Expanded / Visited = %lf",
- (double) stats->visited_states / stats->expanded_states);
+ (double) stats->visited_states / stats->expanded_states);
/*XBT_INFO("Exploration coverage = %lf",
- (double)stats->expanded_states / stats->state_size); */
+ (double)stats->expanded_states / stats->state_size); */
}
void MC_print_statistics_pairs(mc_stats_pair_t stats)
XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
//XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
XBT_INFO("Expanded / Visited = %lf",
- (double) stats->visited_pairs / stats->expanded_pairs);
+ (double) stats->visited_pairs / stats->expanded_pairs);
/*XBT_INFO("Exploration coverage = %lf",
- (double)stats->expanded_states / stats->state_size); */
+ (double)stats->expanded_states / stats->state_size); */
}
void MC_assert(int prop)
}
xbt_automaton_t MC_create_automaton(const char *file){
- return xbt_create_automaton(file);
+ MC_SET_RAW_MEM;
+ xbt_automaton_t a = xbt_create_automaton(file);
+ MC_UNSET_RAW_MEM;
+ return a;
}
for(i=0 ; i< s1->num_reg ; i++){
if(s1->regions[i]->type != s2->regions[i]->type){
- XBT_INFO("Different type of region");
- errors++;
+ XBT_INFO("Different type of region");
+ errors++;
}
switch(s1->regions[i]->type){
- case 0:
+ case 0:
if(s1->regions[i]->size != s2->regions[i]->size){
- XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- errors++;
+ XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- errors++;
+ XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
}
if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
- XBT_INFO("Different heap (mmalloc_compare)");
- errors++;
+ XBT_INFO("Different heap (mmalloc_compare)");
+ errors++;
}
break;
case 1 :
if(s1->regions[i]->size != s2->regions[i]->size){
- XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- errors++;
+ XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- errors++;
+ XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
}
if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- XBT_INFO("Different memcmp for data in libsimgrid");
- errors++;
+ XBT_INFO("Different memcmp for data in libsimgrid");
+ errors++;
}
break;
case 2 :
if(s1->regions[i]->size != s2->regions[i]->size){
- XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
- errors++;
+ XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+ errors++;
}
if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
- XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
- errors++;
+ XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+ errors++;
}
if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
- XBT_INFO("Different memcmp for data in program");
- errors++;
+ XBT_INFO("Different memcmp for data in program");
+ errors++;
}
break;
default:
xbt_dynar_foreach(reached_pairs, cursor, pair_test){
XBT_INFO("Pair reached #%d", pair_test->nb);
if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
- //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
- //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
- //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
- if(snapshot_compare(pair_test->system_state, sn) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
+ //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
+ //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
+ if(snapshot_compare(pair_test->system_state, sn) == 0){
- MC_free_snapshot(sn);
- xbt_dynar_reset(prop_ato);
- xbt_free(prop_ato);
- MC_UNSET_RAW_MEM;
- return 1;
- }
- /* }
- }else{
- XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
- }*/
- }else{
- XBT_INFO("Different values of propositional symbols");
- }
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ /* }
+ }else{
+ XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
+ }*/
+ }else{
+ XBT_INFO("Different values of propositional symbols");
+ }
}else{
- XBT_INFO("Different automaton state");
+ XBT_INFO("Different automaton state");
}
}
int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */
- xbt_dict_cursor_t cursor_dict = NULL;
- char *key;
- char *data;
- smx_rdv_t rdv1, rdv2;
- xbt_fifo_item_t item1, item2;
- smx_action_t action1, action2;
- xbt_fifo_item_t item_req1, item_req2;
- smx_simcall_t req1, req2;
- int i=0;
- int j=0;
-
- xbt_dict_foreach(d1, cursor_dict, key, data){
- rdv1 = (smx_rdv_t)data;
- rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
- if(rdv2 == NULL){
- XBT_INFO("Rdv point unknown");
- return 1;
- }else{
- if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
- XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
- return 1;
- }else{
+ xbt_dict_cursor_t cursor_dict = NULL;
+ char *key;
+ char *data;
+ smx_rdv_t rdv1, rdv2;
+ xbt_fifo_item_t item1, item2;
+ smx_action_t action1, action2;
+ xbt_fifo_item_t item_req1, item_req2;
+ smx_simcall_t req1, req2;
+ int i=0;
+ int j=0;
+
+ xbt_dict_foreach(d1, cursor_dict, key, data){
+ rdv1 = (smx_rdv_t)data;
+ rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
+ if(rdv2 == NULL){
+ XBT_INFO("Rdv point unknown");
+ return 1;
+ }else{
+ if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
+ XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
+ return 1;
+ }else{
- XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo));
+ XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo));
- item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);
- item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
+ item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);
+ item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
- while(i<xbt_fifo_size(rdv1->comm_fifo)){
- action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
- action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
+ while(i<xbt_fifo_size(rdv1->comm_fifo)){
+ action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
+ action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
- if(action1->type != action2->type){
- XBT_INFO("Different type of action");
- return 1;
- }
+ if(action1->type != action2->type){
+ XBT_INFO("Different type of action");
+ return 1;
+ }
- if(action1->state != action2->state){
- XBT_INFO("Different state of action");
- return 1;
- }
+ if(action1->state != action2->state){
+ XBT_INFO("Different state of action");
+ return 1;
+ }
- if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
- XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
- return 1;
- }else{
+ if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
+ XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
+ return 1;
+ }else{
- item_req1 = xbt_fifo_get_first_item(action1->simcalls);
- item_req2 = xbt_fifo_get_first_item(action2->simcalls);
+ item_req1 = xbt_fifo_get_first_item(action1->simcalls);
+ item_req2 = xbt_fifo_get_first_item(action2->simcalls);
- while(j<xbt_fifo_size(action1->simcalls)){
+ while(j<xbt_fifo_size(action1->simcalls)){
- req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
- req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
+ req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
+ req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
- if(req1->call != req2->call){
- XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
- return 1;
- }
- if(req1->issuer->pid != req2->issuer->pid){
- XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
- return 1;
- }
-
- item_req1 = xbt_fifo_get_next_item(item_req1);
- item_req2 = xbt_fifo_get_next_item(item_req2);
- j++;
+ if(req1->call != req2->call){
+ XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
+ return 1;
+ }
+ if(req1->issuer->pid != req2->issuer->pid){
+ XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
+ return 1;
+ }
+
+ item_req1 = xbt_fifo_get_next_item(item_req1);
+ item_req2 = xbt_fifo_get_next_item(item_req2);
+ j++;
- }
- }
-
- switch(action1->type){
- case 0: /* execution */
- case 1: /* parallel execution */
- if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
- return 1;
- break;
- case 2: /* comm */
- if(action1->comm.type != action2->comm.type)
- return 1;
- //XBT_INFO("Type of comm : %d", action1->comm.type);
+ }
+ }
+
+ switch(action1->type){
+ case 0: /* execution */
+ case 1: /* parallel execution */
+ if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
+ return 1;
+ break;
+ case 2: /* comm */
+ if(action1->comm.type != action2->comm.type)
+ return 1;
+ //XBT_INFO("Type of comm : %d", action1->comm.type);
- switch(action1->comm.type){
- case 0: /* SEND */
- if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
- return 1;
- if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
- return 1;
- break;
- case 1: /* RECEIVE */
- if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
- return 1;
- if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
- return 1;
- break;
- case 2: /* READY */
- if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
- return 1;
- if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
- return 1;
- if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
- return 1;
- if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
- return 1;
- break;
- case 3: /* DONE */
- if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
- return 1;
- if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
- return 1;
- if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
- return 1;
- if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
- return 1;
- break;
+ switch(action1->comm.type){
+ case 0: /* SEND */
+ if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
+ return 1;
+ if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
+ return 1;
+ break;
+ case 1: /* RECEIVE */
+ if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
+ return 1;
+ if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
+ return 1;
+ break;
+ case 2: /* READY */
+ if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
+ return 1;
+ if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
+ return 1;
+ if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
+ return 1;
+ if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
+ return 1;
+ break;
+ case 3: /* DONE */
+ if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
+ return 1;
+ if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
+ return 1;
+ if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
+ return 1;
+ if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
+ return 1;
+ break;
- } /* end of switch on type of comm */
+ } /* end of switch on type of comm */
- if(action1->comm.refcount != action2->comm.refcount)
- return 1;
- if(action1->comm.detached != action2->comm.detached)
- return 1;
- if(action1->comm.rate != action2->comm.rate)
- return 1;
- if(action1->comm.task_size != action2->comm.task_size)
- return 1;
- if(action1->comm.src_buff != action2->comm.src_buff)
- return 1;
- if(action1->comm.dst_buff != action2->comm.dst_buff)
- return 1;
- if(action1->comm.src_data != action2->comm.src_data)
- return 1;
- if(action1->comm.dst_data != action2->comm.dst_data)
- return 1;
+ if(action1->comm.refcount != action2->comm.refcount)
+ return 1;
+ if(action1->comm.detached != action2->comm.detached)
+ return 1;
+ if(action1->comm.rate != action2->comm.rate)
+ return 1;
+ if(action1->comm.task_size != action2->comm.task_size)
+ return 1;
+ if(action1->comm.src_buff != action2->comm.src_buff)
+ return 1;
+ if(action1->comm.dst_buff != action2->comm.dst_buff)
+ return 1;
+ if(action1->comm.src_data != action2->comm.src_data)
+ return 1;
+ if(action1->comm.dst_data != action2->comm.dst_data)
+ return 1;
- break;
- case 3: /* sleep */
- if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
- return 1;
- break;
- case 4: /* synchro */
+ break;
+ case 3: /* sleep */
+ if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
+ return 1;
+ break;
+ case 4: /* synchro */
- break;
- default:
- break;
- }
-
- item1 = xbt_fifo_get_next_item(item1);
- item2 = xbt_fifo_get_next_item(item2);
- i++;
- }
- }
- }
- }
-
- return 0;
+ break;
+ default:
+ break;
+ }
+
+ item1 = xbt_fifo_get_next_item(item1);
+ item2 = xbt_fifo_get_next_item(item2);
+ i++;
+ }
+ }
+ }
+ }
+
+ return 0;
}
/*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
- xbt_dict_cursor_t cursor_dict = NULL;
- char *key;
- char *data;
- xbt_fifo_item_t item;
- smx_action_t action;
+ xbt_dict_cursor_t cursor_dict = NULL;
+ char *key;
+ char *data;
+ xbt_fifo_item_t item;
+ smx_action_t action;
- xbt_dict_foreach(rdv_points, cursor_dict, key, data){
+ xbt_dict_foreach(rdv_points, cursor_dict, key, data){
smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
new_rdv->name = strdup(((smx_rdv_t)data)->name);
new_rdv->comm_fifo = xbt_fifo_new();
xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
- smx_action_t a = xbt_new0(s_smx_action_t, 1);
- memcpy(a, action, sizeof(s_smx_action_t));
- xbt_fifo_push(new_rdv->comm_fifo, a);
- XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
- if(action->type==2)
- XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
+ smx_action_t a = xbt_new0(s_smx_action_t, 1);
+ memcpy(a, action, sizeof(s_smx_action_t));
+ xbt_fifo_push(new_rdv->comm_fifo, a);
+ XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
+ if(action->type==2)
+ XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
}
//new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
- for(j=0 ; j< sn->num_reg ; j++){
- if(hash_regions[j] != pair_test->hash_regions[j]){
- region_diff++;
- }
- }
- if(region_diff == 0){
- MC_free_snapshot(sn);
- xbt_dynar_reset(prop_ato);
- xbt_free(prop_ato);
- MC_UNSET_RAW_MEM;
- return 1;
- }else{
- XBT_INFO("Different snapshot");
- }
- }else{
- XBT_INFO("Different values of propositional symbols");
- }
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ for(j=0 ; j< sn->num_reg ; j++){
+ if(hash_regions[j] != pair_test->hash_regions[j]){
+ region_diff++;
+ }
+ }
+ if(region_diff == 0){
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }else{
+ XBT_INFO("Different snapshot");
+ }
+ }else{
+ XBT_INFO("Different values of propositional symbols");
+ }
}else{
- XBT_INFO("Different automaton state");
+ XBT_INFO("Different automaton state");
}
region_diff = 0;
xbt_dynar_foreach(visited_pairs, cursor, pair_test){
if(pair_test->search_cycle == sc) {
- if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
- if(snapshot_compare(pair_test->system_state, sn) == 0){
+ if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ if(snapshot_compare(pair_test->system_state, sn) == 0){
- MC_free_snapshot(sn);
- xbt_dynar_reset(prop_ato);
- xbt_free(prop_ato);
- MC_UNSET_RAW_MEM;
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
- return 1;
+ return 1;
+ }else{
+ XBT_INFO("Different snapshot");
+ }
+ }else{
+ XBT_INFO("Different values of propositional symbols");
+ }
+ }else{
+ XBT_INFO("Different automaton state");
+ }
}else{
- XBT_INFO("Different snapshot");
- }
- }else{
- XBT_INFO("Different values of propositional symbols");
- }
- }else{
- XBT_INFO("Different automaton state");
- }
- }else{
- XBT_INFO("Different value of search_cycle");
+ XBT_INFO("Different value of search_cycle");
}
}
xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
if(pair_test->search_cycle == sc) {
- if(automaton_state_compare(pair_test->automaton_state, st) == 0){
- if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
- for(j=0 ; j< sn->num_reg ; j++){
- if(hash_regions[j] != pair_test->hash_regions[j]){
- region_diff++;
+ if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ for(j=0 ; j< sn->num_reg ; j++){
+ if(hash_regions[j] != pair_test->hash_regions[j]){
+ region_diff++;
+ }
+ }
+ if(region_diff == 0){
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }else{
+ //XBT_INFO("Different snapshot");
+ }
+ }else{
+ //XBT_INFO("Different values of propositional symbols");
+ }
+ }else{
+ //XBT_INFO("Different automaton state");
}
- }
- if(region_diff == 0){
- MC_free_snapshot(sn);
- xbt_dynar_reset(prop_ato);
- xbt_free(prop_ato);
- MC_UNSET_RAW_MEM;
- return 1;
}else{
- //XBT_INFO("Different snapshot");
- }
- }else{
- //XBT_INFO("Different values of propositional symbols");
- }
- }else{
- //XBT_INFO("Different automaton state");
- }
- }else{
- //XBT_INFO("Different value of search_cycle");
+ //XBT_INFO("Different value of search_cycle");
}
region_diff = 0;
int_f_void_t f;
xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
if(strcmp(p->pred, l->u.predicat) == 0){
- f = (int_f_void_t)p->function;
- return (*f)();
+ f = (int_f_void_t)p->function;
+ return (*f)();
}
}
return -1;
MC_UNSET_RAW_MEM;
if(cursor != 0){
- MC_restore_snapshot(initial_snapshot_liveness);
- MC_UNSET_RAW_MEM;
+ MC_restore_snapshot(initial_snapshot_liveness);
+ MC_UNSET_RAW_MEM;
}
MC_ddfs(0);
}else{
if(state->type == 2){
- MC_SET_RAW_MEM;
- mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
- xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+ xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
+ MC_UNSET_RAW_MEM;
- set_pair_reached(state);
- //set_pair_reached_hash(state);
+ set_pair_reached(state);
+ //set_pair_reached_hash(state);
- if(cursor != 0){
- MC_restore_snapshot(initial_snapshot_liveness);
- MC_UNSET_RAW_MEM;
- }
+ if(cursor != 0){
+ MC_restore_snapshot(initial_snapshot_liveness);
+ MC_UNSET_RAW_MEM;
+ }
- MC_ddfs(1);
+ MC_ddfs(1);
}
}
while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
- /* Debug information */
+ /* Debug information */
- req_str = MC_request_to_string(req, value);
- XBT_INFO("Execute: %s", req_str);
- xbt_free(req_str);
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("Execute: %s", req_str);
+ xbt_free(req_str);
- MC_state_set_executed_request(current_pair->graph_state, req, value);
+ MC_state_set_executed_request(current_pair->graph_state, req, value);
- /* Answer the request */
- SIMIX_simcall_pre(req, value);
+ /* Answer the request */
+ SIMIX_simcall_pre(req, value);
- /* Wait for requests (schedules processes) */
- MC_wait_for_requests();
+ /* Wait for requests (schedules processes) */
+ MC_wait_for_requests();
- MC_SET_RAW_MEM;
+ MC_SET_RAW_MEM;
- /* Create the new expanded graph_state */
- next_graph_state = MC_state_pair_new();
+ /* Create the new expanded graph_state */
+ next_graph_state = MC_state_pair_new();
- /* Get enabled process and insert it in the interleave set of the next graph_state */
- xbt_swag_foreach(process, simix_global->process_list){
- if(MC_process_is_enabled(process)){
- MC_state_interleave_process(next_graph_state, process);
- }
- }
+ /* Get enabled process and insert it in the interleave set of the next graph_state */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(next_graph_state, process);
+ }
+ }
- xbt_dynar_reset(successors);
+ xbt_dynar_reset(successors);
- MC_UNSET_RAW_MEM;
+ MC_UNSET_RAW_MEM;
- cursor= 0;
- xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+ cursor= 0;
+ xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
- res = MC_automaton_evaluate_label(transition_succ->label);
+ res = MC_automaton_evaluate_label(transition_succ->label);
- if(res == 1){ // enabled transition in automaton
- MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
- xbt_dynar_push(successors, &next_pair);
- MC_UNSET_RAW_MEM;
- }
+ if(res == 1){ // enabled transition in automaton
+ MC_SET_RAW_MEM;
+ next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ xbt_dynar_push(successors, &next_pair);
+ MC_UNSET_RAW_MEM;
+ }
- }
+ }
- cursor = 0;
+ cursor = 0;
- xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+ xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
- res = MC_automaton_evaluate_label(transition_succ->label);
+ res = MC_automaton_evaluate_label(transition_succ->label);
- if(res == 2){ // true transition in automaton
- MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
- xbt_dynar_push(successors, &next_pair);
- MC_UNSET_RAW_MEM;
- }
+ if(res == 2){ // true transition in automaton
+ MC_SET_RAW_MEM;
+ next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ xbt_dynar_push(successors, &next_pair);
+ MC_UNSET_RAW_MEM;
+ }
- }
+ }
- cursor = 0;
+ cursor = 0;
- xbt_dynar_foreach(successors, cursor, pair_succ){
+ xbt_dynar_foreach(successors, cursor, pair_succ){
- if(search_cycle == 1){
+ if(search_cycle == 1){
- if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
+ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
- if(reached(pair_succ->automaton_state)){
- //if(reached_hash(pair_succ->automaton_state)){
+ if(reached(pair_succ->automaton_state)){
+ //if(reached_hash(pair_succ->automaton_state)){
- XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
+ XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
- 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_pairs(mc_stats_pair);
- exit(0);
+ 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_pairs(mc_stats_pair);
+ exit(0);
- }else{
+ }else{
- XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+ XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- set_pair_reached(pair_succ->automaton_state);
- //set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
- XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness, pair_succ);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
- MC_ddfs(search_cycle);
+ MC_ddfs(search_cycle);
- }
+ }
- }else{
+ }else{
- if(!visited_hash(pair_succ->automaton_state, search_cycle)){
- //if(!visited(pair_succ->automaton_state, search_cycle)){
+ if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+ //if(!visited(pair_succ->automaton_state, search_cycle)){
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness, pair_succ);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
- MC_ddfs(search_cycle);
+ MC_ddfs(search_cycle);
- }else{
+ }else{
- XBT_INFO("Next pair already visited ! ");
+ XBT_INFO("Next pair already visited ! ");
- }
+ }
- }
+ }
- }else{
+ }else{
- if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+ XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- set_pair_reached(pair_succ->automaton_state);
- //set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
- search_cycle = 1;
+ search_cycle = 1;
- XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
- }
+ }
- if(!visited_hash(pair_succ->automaton_state, search_cycle)){
- //if(!visited(pair_succ->automaton_state, search_cycle)){
+ if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+ //if(!visited(pair_succ->automaton_state, search_cycle)){
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness, pair_succ);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
- MC_ddfs(search_cycle);
+ MC_ddfs(search_cycle);
- }else{
+ }else{
- XBT_INFO("Next pair already visited ! ");
+ XBT_INFO("Next pair already visited ! ");
- }
+ }
- }
+ }
- /* Restore system before checking others successors */
- if(cursor != (xbt_dynar_length(successors) - 1))
- MC_replay_liveness(mc_stack_liveness, 1);
+ /* Restore system before checking others successors */
+ if(cursor != (xbt_dynar_length(successors) - 1))
+ MC_replay_liveness(mc_stack_liveness, 1);
- }
+ }
- if(MC_state_interleave_size(current_pair->graph_state) > 0){
- XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
- MC_replay_liveness(mc_stack_liveness, 0);
- }
+ if(MC_state_interleave_size(current_pair->graph_state) > 0){
+ XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
+ MC_replay_liveness(mc_stack_liveness, 0);
+ }
}
cursor= 0;
xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
- res = MC_automaton_evaluate_label(transition_succ->label);
+ res = MC_automaton_evaluate_label(transition_succ->label);
- if(res == 1){ // enabled transition in automaton
- MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
- xbt_dynar_push(successors, &next_pair);
- MC_UNSET_RAW_MEM;
- }
+ if(res == 1){ // enabled transition in automaton
+ MC_SET_RAW_MEM;
+ next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ xbt_dynar_push(successors, &next_pair);
+ MC_UNSET_RAW_MEM;
+ }
}
xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
- res = MC_automaton_evaluate_label(transition_succ->label);
+ res = MC_automaton_evaluate_label(transition_succ->label);
- if(res == 2){ // true transition in automaton
- MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
- xbt_dynar_push(successors, &next_pair);
- MC_UNSET_RAW_MEM;
- }
+ if(res == 2){ // true transition in automaton
+ MC_SET_RAW_MEM;
+ next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+ xbt_dynar_push(successors, &next_pair);
+ MC_UNSET_RAW_MEM;
+ }
}
xbt_dynar_foreach(successors, cursor, pair_succ){
- if(search_cycle == 1){
+ if(search_cycle == 1){
- if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
+ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
- if(reached(pair_succ->automaton_state)){
- //if(reached_hash(pair_succ->automaton_state)){
+ if(reached(pair_succ->automaton_state)){
+ //if(reached_hash(pair_succ->automaton_state)){
- XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
+ XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
- 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_pairs(mc_stats_pair);
- exit(0);
-
- }else{
-
- XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+ 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_pairs(mc_stats_pair);
+ exit(0);
+
+ }else{
+
+ XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
- set_pair_reached(pair_succ->automaton_state);
- //set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
- XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness, pair_succ);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
- MC_ddfs(search_cycle);
+ MC_ddfs(search_cycle);
- }
+ }
- }else{
+ }else{
- if(!visited_hash(pair_succ->automaton_state, search_cycle)){
- //if(!visited(pair_succ->automaton_state, search_cycle)){
+ if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+ //if(!visited(pair_succ->automaton_state, search_cycle)){
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness, pair_succ);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
- MC_ddfs(search_cycle);
+ MC_ddfs(search_cycle);
- }else{
+ }else{
- XBT_INFO("Next pair already visited ! ");
+ XBT_INFO("Next pair already visited ! ");
- }
- }
+ }
+ }
- }else{
+ }else{
- if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- set_pair_reached(pair_succ->automaton_state);
- //set_pair_reached_hash(pair_succ->automaton_state);
+ set_pair_reached(pair_succ->automaton_state);
+ //set_pair_reached_hash(pair_succ->automaton_state);
- search_cycle = 1;
+ search_cycle = 1;
- XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
- //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+ XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
- }
+ }
- if(!visited_hash(pair_succ->automaton_state, search_cycle)){
- //if(!visited(pair_succ->automaton_state, search_cycle)){
+ if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+ //if(!visited(pair_succ->automaton_state, search_cycle)){
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness, pair_succ);
- MC_UNSET_RAW_MEM;
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+ MC_UNSET_RAW_MEM;
- MC_ddfs(search_cycle);
+ MC_ddfs(search_cycle);
- }else{
+ }else{
- XBT_INFO("Next pair already visited ! ");
+ XBT_INFO("Next pair already visited ! ");
- }
+ }
- }
+ }
- /* Restore system before checking others successors */
- if(cursor != xbt_dynar_length(successors) - 1)
- MC_replay_liveness(mc_stack_liveness, 1);
+ /* Restore system before checking others successors */
+ if(cursor != xbt_dynar_length(successors) - 1)
+ MC_replay_liveness(mc_stack_liveness, 1);
}
return FALSE;
if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
- && r2->call == SIMCALL_COMM_WAIT){
+ && r2->call == SIMCALL_COMM_WAIT){
if(r2->comm_wait.comm->comm.rdv == NULL)
return FALSE;
}
if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
- && r1->call == SIMCALL_COMM_WAIT){
+ && r1->call == SIMCALL_COMM_WAIT){
if(r1->comm_wait.comm->comm.rdv != NULL)
return FALSE;
* isend/irecv call is not stored in a buffer used in the
* test call. */
if( (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
- && r2->call == SIMCALL_COMM_TEST)
+ && r2->call == SIMCALL_COMM_TEST)
return FALSE;
/* FIXME: the following rule assumes that the result of the
* isend/irecv call is not stored in a buffer used in the
* test call.*/
if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
- && r1->call == SIMCALL_COMM_TEST)
+ && r1->call == SIMCALL_COMM_TEST)
return FALSE;
if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND
- && r1->comm_isend.rdv != r2->comm_isend.rdv)
+ && r1->comm_isend.rdv != r2->comm_isend.rdv)
return FALSE;
if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV
- && r1->comm_irecv.rdv != r2->comm_irecv.rdv)
+ && r1->comm_irecv.rdv != r2->comm_irecv.rdv)
return FALSE;
if(r1->call == SIMCALL_COMM_WAIT && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
return FALSE;
if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
- && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
- && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
+ && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
+ && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
return FALSE;
if(r1->call == SIMCALL_COMM_TEST &&
- (r1->comm_test.comm == NULL
- || r1->comm_test.comm->comm.src_buff == NULL
- || r1->comm_test.comm->comm.dst_buff == NULL))
+ (r1->comm_test.comm == NULL
+ || r1->comm_test.comm->comm.src_buff == NULL
+ || r1->comm_test.comm->comm.dst_buff == NULL))
return FALSE;
if(r2->call == SIMCALL_COMM_TEST &&
- (r2->comm_test.comm == NULL
- || r2->comm_test.comm->comm.src_buff == NULL
- || r2->comm_test.comm->comm.dst_buff == NULL))
+ (r2->comm_test.comm == NULL
+ || r2->comm_test.comm->comm.src_buff == NULL
+ || r2->comm_test.comm->comm.dst_buff == NULL))
return FALSE;
if(r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
- && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
+ && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
+ && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
return FALSE;
if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
- && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)
+ && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
+ && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && r1->comm_wait.comm->comm.src_buff != NULL
- && r1->comm_wait.comm->comm.dst_buff != NULL
- && r2->comm_test.comm->comm.src_buff != NULL
- && r2->comm_test.comm->comm.dst_buff != NULL
- && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
- && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
- && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
+ && r1->comm_wait.comm->comm.src_buff != NULL
+ && r1->comm_wait.comm->comm.dst_buff != NULL
+ && r2->comm_test.comm->comm.src_buff != NULL
+ && r2->comm_test.comm->comm.dst_buff != NULL
+ && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
+ && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
+ && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && r1->comm_test.comm->comm.src_buff != NULL
- && r1->comm_test.comm->comm.dst_buff != NULL
- && r2->comm_wait.comm->comm.src_buff != NULL
- && r2->comm_wait.comm->comm.dst_buff != NULL
- && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
- && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
- && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
- return FALSE;
+ && r1->comm_test.comm->comm.src_buff != NULL
+ && r1->comm_test.comm->comm.dst_buff != NULL
+ && r2->comm_wait.comm->comm.src_buff != NULL
+ && r2->comm_wait.comm->comm.dst_buff != NULL
+ && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
+ && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
+ && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
+ return FALSE;
return TRUE;
size_t size = 0;
switch(req->call){
- case SIMCALL_COMM_ISEND:
- type = xbt_strdup("iSend");
- p = pointer_to_string(req->comm_isend.src_buff);
- bs = buff_size_to_string(req->comm_isend.src_buff_size);
- args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs);
- break;
- case SIMCALL_COMM_IRECV:
- size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
- type = xbt_strdup("iRecv");
- p = pointer_to_string(req->comm_irecv.dst_buff);
- bs = buff_size_to_string(size);
- args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs);
- break;
- case SIMCALL_COMM_WAIT:
- act = req->comm_wait.comm;
- if(value == -1){
- type = xbt_strdup("WaitTimeout");
- p = pointer_to_string(act);
- args = bprintf("comm=%p", p);
- }else{
- type = xbt_strdup("Wait");
- p = pointer_to_string(act);
- args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
- act->comm.src_proc ? act->comm.src_proc->pid : 0,
- act->comm.src_proc ? act->comm.src_proc->name : "",
- act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
- act->comm.dst_proc ? act->comm.dst_proc->name : "");
- }
- break;
- case SIMCALL_COMM_TEST:
- act = req->comm_test.comm;
- if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){
- type = xbt_strdup("Test FALSE");
- p = pointer_to_string(act);
- args = bprintf("comm=%s", p);
- }else{
- type = xbt_strdup("Test TRUE");
- p = pointer_to_string(act);
- args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
- act->comm.src_proc->pid, act->comm.src_proc->name,
- act->comm.dst_proc->pid, act->comm.dst_proc->name);
- }
- break;
-
- case SIMCALL_COMM_WAITANY:
- type = xbt_strdup("WaitAny");
- p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t));
- args = bprintf("comm=%s (%d of %lu)", p,
- value+1, xbt_dynar_length(req->comm_waitany.comms));
- break;
-
- case SIMCALL_COMM_TESTANY:
- if(value == -1){
- type = xbt_strdup("TestAny FALSE");
- args = xbt_strdup("-");
- }else{
- type = xbt_strdup("TestAny");
- args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
- }
- break;
-
- default:
- THROW_UNIMPLEMENTED;
+ case SIMCALL_COMM_ISEND:
+ type = xbt_strdup("iSend");
+ p = pointer_to_string(req->comm_isend.src_buff);
+ bs = buff_size_to_string(req->comm_isend.src_buff_size);
+ args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs);
+ break;
+ case SIMCALL_COMM_IRECV:
+ size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
+ type = xbt_strdup("iRecv");
+ p = pointer_to_string(req->comm_irecv.dst_buff);
+ bs = buff_size_to_string(size);
+ args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs);
+ break;
+ case SIMCALL_COMM_WAIT:
+ act = req->comm_wait.comm;
+ if(value == -1){
+ type = xbt_strdup("WaitTimeout");
+ p = pointer_to_string(act);
+ args = bprintf("comm=%p", p);
+ }else{
+ type = xbt_strdup("Wait");
+ p = pointer_to_string(act);
+ args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
+ act->comm.src_proc ? act->comm.src_proc->pid : 0,
+ act->comm.src_proc ? act->comm.src_proc->name : "",
+ act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
+ act->comm.dst_proc ? act->comm.dst_proc->name : "");
+ }
+ break;
+ case SIMCALL_COMM_TEST:
+ act = req->comm_test.comm;
+ if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){
+ type = xbt_strdup("Test FALSE");
+ p = pointer_to_string(act);
+ args = bprintf("comm=%s", p);
+ }else{
+ type = xbt_strdup("Test TRUE");
+ p = pointer_to_string(act);
+ args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
+ act->comm.src_proc->pid, act->comm.src_proc->name,
+ act->comm.dst_proc->pid, act->comm.dst_proc->name);
+ }
+ break;
+
+ case SIMCALL_COMM_WAITANY:
+ type = xbt_strdup("WaitAny");
+ p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t));
+ args = bprintf("comm=%s (%d of %lu)", p,
+ value+1, xbt_dynar_length(req->comm_waitany.comms));
+ break;
+
+ case SIMCALL_COMM_TESTANY:
+ if(value == -1){
+ type = xbt_strdup("TestAny FALSE");
+ args = xbt_strdup("-");
+ }else{
+ type = xbt_strdup("TestAny");
+ args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
+ }
+ break;
+
+ default:
+ THROW_UNIMPLEMENTED;
}
str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
int MC_request_is_visible(smx_simcall_t req)
{
return req->call == SIMCALL_COMM_ISEND
- || req->call == SIMCALL_COMM_IRECV
- || req->call == SIMCALL_COMM_WAIT
- || req->call == SIMCALL_COMM_WAITANY
- || req->call == SIMCALL_COMM_TEST
- || req->call == SIMCALL_COMM_TESTANY;
+ || req->call == SIMCALL_COMM_IRECV
+ || req->call == SIMCALL_COMM_WAIT
+ || req->call == SIMCALL_COMM_WAITANY
+ || req->call == SIMCALL_COMM_TEST
+ || req->call == SIMCALL_COMM_TESTANY;
}
int MC_request_is_enabled(smx_simcall_t req)
switch (req->call) {
- case SIMCALL_COMM_WAIT:
- /* FIXME: check also that src and dst processes are not suspended */
+ case SIMCALL_COMM_WAIT:
+ /* FIXME: check also that src and dst processes are not suspended */
+
+ /* If it has a timeout it will be always be enabled, because even if the
+ * communication is not ready, it can timeout and won't block.
+ * On the other hand if it hasn't a timeout, check if the comm is ready.*/
+ if(req->comm_wait.timeout >= 0){
+ return TRUE;
+ }else{
+ act = req->comm_wait.comm;
+ return (act->comm.src_proc && act->comm.dst_proc);
+ }
+ break;
- /* If it has a timeout it will be always be enabled, because even if the
- * communication is not ready, it can timeout and won't block.
- * On the other hand if it hasn't a timeout, check if the comm is ready.*/
- if(req->comm_wait.timeout >= 0){
+ case SIMCALL_COMM_WAITANY:
+ /* Check if it has at least one communication ready */
+ xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
+ if (act->comm.src_proc && act->comm.dst_proc){
return TRUE;
- }else{
- act = req->comm_wait.comm;
- return (act->comm.src_proc && act->comm.dst_proc);
}
- break;
-
- case SIMCALL_COMM_WAITANY:
- /* Check if it has at least one communication ready */
- xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
- if (act->comm.src_proc && act->comm.dst_proc){
- return TRUE;
- }
- }
- return FALSE;
- break;
+ }
+ return FALSE;
+ break;
- default:
- /* The rest of the request are always enabled */
- return TRUE;
+ default:
+ /* The rest of the request are always enabled */
+ return TRUE;
}
}
switch (req->call) {
- case SIMCALL_COMM_WAIT:
- /* FIXME: check also that src and dst processes are not suspended */
- act = req->comm_wait.comm;
- return (act->comm.src_proc && act->comm.dst_proc);
- break;
+ case SIMCALL_COMM_WAIT:
+ /* FIXME: check also that src and dst processes are not suspended */
+ act = req->comm_wait.comm;
+ return (act->comm.src_proc && act->comm.dst_proc);
+ break;
- case SIMCALL_COMM_WAITANY:
- act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
- return (act->comm.src_proc && act->comm.dst_proc);
- break;
+ case SIMCALL_COMM_WAITANY:
+ act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
+ return (act->comm.src_proc && act->comm.dst_proc);
+ break;
- case SIMCALL_COMM_TESTANY:
- act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
- return (act->comm.src_proc && act->comm.dst_proc);
- break;
+ case SIMCALL_COMM_TESTANY:
+ act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
+ return (act->comm.src_proc && act->comm.dst_proc);
+ break;
- default:
- return TRUE;
+ default:
+ return TRUE;
}
}
Contributed by Fred Fish at Cygnus Support. fnf@cygnus.com
-This file is part of the GNU C Library.
+ This file is part of the GNU C Library.
-The GNU C Library is free software; you can redistribute it and/or
-modify it under the terms of the GNU Library General Public License as
-published by the Free Software Foundation; either version 2 of the
-License, or (at your option) any later version.
+ The GNU C Library is free software; you can redistribute it and/or
+ modify it under the terms of the GNU Library General Public License as
+ published by the Free Software Foundation; either version 2 of the
+ License, or (at your option) any later version.
-The GNU C Library is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
-Library General Public License for more details.
+ The GNU C Library is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ Library General Public License for more details.
-You should have received a copy of the GNU Library General Public
-License along with the GNU C Library; see the file COPYING.LIB. If
-not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
-Boston, MA 02111-1307, USA. */
+ You should have received a copy of the GNU Library General Public
+ License along with the GNU C Library; see the file COPYING.LIB. If
+ not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
+ Boston, MA 02111-1307, USA. */
#include <sys/types.h>
#include <fcntl.h> /* After sys/types.h, at least for dpx/2. */
else if (sbuf.st_size > 0) {
/* We were given an valid file descriptor on an open file, so try to remap
- it into the current process at the same address to which it was previously
- mapped. It naturally have to pass some sanity checks for that.
+ it into the current process at the same address to which it was previously
+ mapped. It naturally have to pass some sanity checks for that.
- Note that we have to update the file descriptor number in the malloc-
- descriptor read from the file to match the current valid one, before
- trying to map the file in, and again after a successful mapping and
- after we've switched over to using the mapped in malloc descriptor
- rather than the temporary one on the stack.
+ Note that we have to update the file descriptor number in the malloc-
+ descriptor read from the file to match the current valid one, before
+ trying to map the file in, and again after a successful mapping and
+ after we've switched over to using the mapped in malloc descriptor
+ rather than the temporary one on the stack.
- Once we've switched over to using the mapped in malloc descriptor, we
- have to update the pointer to the morecore function, since it almost
- certainly will be at a different address if the process reusing the
- mapped region is from a different executable.
+ Once we've switched over to using the mapped in malloc descriptor, we
+ have to update the pointer to the morecore function, since it almost
+ certainly will be at a different address if the process reusing the
+ mapped region is from a different executable.
- Also note that if the heap being remapped previously used the mmcheckf()
- routines, we need to update the hooks since their target functions
- will have certainly moved if the executable has changed in any way.
- We do this by calling mmcheckf() internally.
+ Also note that if the heap being remapped previously used the mmcheckf()
+ routines, we need to update the hooks since their target functions
+ will have certainly moved if the executable has changed in any way.
+ We do this by calling mmcheckf() internally.
- Returns a pointer to the malloc descriptor if successful, or NULL if
- unsuccessful for some reason. */
+ Returns a pointer to the malloc descriptor if successful, or NULL if
+ unsuccessful for some reason. */
struct mdesc newmd;
struct mdesc *mdptr = NULL, *mdptemp = NULL;
if (lseek(fd, 0L, SEEK_SET) != 0)
- return NULL;
+ return NULL;
if (read(fd, (char *) &newmd, sizeof(newmd)) != sizeof(newmd))
- return NULL;
+ return NULL;
if (newmd.headersize != sizeof(newmd))
- return NULL;
+ return NULL;
if (strcmp(newmd.magic, MMALLOC_MAGIC) != 0)
- return NULL;
+ return NULL;
if (newmd.version > MMALLOC_VERSION)
- return NULL;
+ return NULL;
newmd.fd = fd;
if (__mmalloc_remap_core(&newmd) == newmd.base) {
- mdptr = (struct mdesc *) newmd.base;
- mdptr->fd = fd;
- if(!mdptr->refcount){
- sem_init(&mdptr->sem, 0, 1);
- mdptr->refcount++;
- }
+ mdptr = (struct mdesc *) newmd.base;
+ mdptr->fd = fd;
+ if(!mdptr->refcount){
+ sem_init(&mdptr->sem, 0, 1);
+ mdptr->refcount++;
+ }
}
/* Add the new heap to the linked list of heaps attached by mmalloc */
mdptemp = __mmalloc_default_mdp;
while(mdptemp->next_mdesc)
- mdptemp = mdptemp->next_mdesc;
+ mdptemp = mdptemp->next_mdesc;
LOCK(mdptemp);
mdptemp->next_mdesc = mdptr;
mdp = mdp->next_mdesc;
LOCK(mdp);
- mdp->next_mdesc = (struct mdesc *)mbase;
+ mdp->next_mdesc = (struct mdesc *)mbase;
UNLOCK(mdp);
}
}
/** Terminate access to a mmalloc managed region by unmapping all memory pages
- associated with the region, and closing the file descriptor if it is one
- that we opened.
+ associated with the region, and closing the file descriptor if it is one
+ that we opened.
- Returns NULL on success.
+ Returns NULL on success.
- Returns the malloc descriptor on failure, which can subsequently be used
- for further action, such as obtaining more information about the nature of
- the failure.
+ Returns the malloc descriptor on failure, which can subsequently be used
+ for further action, such as obtaining more information about the nature of
+ the failure.
- Note that the malloc descriptor that we are using is currently located in
- region we are about to unmap, so we first make a local copy of it on the
- stack and use the copy. */
+ Note that the malloc descriptor that we are using is currently located in
+ region we are about to unmap, so we first make a local copy of it on the
+ stack and use the copy. */
void *xbt_mheap_destroy(xbt_mheap_t mdp)
{
__mmalloc_default_mdp = xbt_mheap_new(-1, addr);
/* Fixme? only the default mdp in protected against forks */
res = xbt_os_thread_atfork(mmalloc_fork_prepare,
- mmalloc_fork_parent, mmalloc_fork_child);
+ mmalloc_fork_parent, mmalloc_fork_child);
if (res != 0)
THROWF(system_error,0,"xbt_os_thread_atfork() failed: return value %d",res);
}
static size_t pagesize;
#define PAGE_ALIGN(addr) (void*) (((long)(addr) + pagesize - 1) & \
- ~(pagesize - 1))
+ ~(pagesize - 1))
/* Return MAP_PRIVATE if MDP represents /dev/zero. Otherwise, return
MAP_SHARED. */
#define MAP_PRIVATE_OR_SHARED(MDP) (( MDP -> flags & MMALLOC_ANONYMOUS) \
- ? MAP_PRIVATE \
+ ? MAP_PRIVATE \
: MAP_SHARED)
/* Return MAP_ANONYMOUS if MDP uses anonymous mapping. Otherwise, return 0 */
#define MAP_IS_ANONYMOUS(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \
- ? MAP_ANONYMOUS \
- : 0)
+ ? MAP_ANONYMOUS \
+ : 0)
/* Return -1 if MDP uses anonymous mapping. Otherwise, return MDP->FD */
#define MAP_ANON_OR_FD(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \
- ? -1 \
- : (MDP) -> fd)
+ ? -1 \
+ : (MDP) -> fd)
/* Get core for the memory region specified by MDP, using SIZE as the
amount to either add to or subtract from the existing region. Works
*/
typedef struct {
int type; /* 0: busy large block
- >0: busy fragmented (fragments of size 2^type bytes)
- <0: free block */
+ >0: busy fragmented (fragments of size 2^type bytes)
+ <0: free block */
union {
/* Heap information for a busy block. */
struct {
/* Change the size of a block allocated by `mmalloc'.
Copyright 1990, 1991 Free Software Foundation
- Written May 1989 by Mike Haertel. */
+ Written May 1989 by Mike Haertel. */
/* Copyright (c) 2010. The SimGrid Team.
* All rights reserved. */
if ((char *) ptr < (char *) mdp->heapbase || BLOCK(ptr) > mdp->heapsize) {
printf
- ("FIXME. Ouch, this pointer is not mine, refusing to proceed (another solution would be to malloc it instead of reallocing it, see source code)\n");
+ ("FIXME. Ouch, this pointer is not mine, refusing to proceed (another solution would be to malloc it instead of reallocing it, see source code)\n");
result = mmalloc(mdp, size);
abort();
return result;
/* The new size is smaller; return excess memory to the free list. */
//printf("(%s) return excess memory...",xbt_thread_self_name());
for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++)
- mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here
+ mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here
mdp->heapinfo[block + blocks].busy_block.size
- = mdp->heapinfo[block].busy_block.size - blocks;
+ = mdp->heapinfo[block].busy_block.size - blocks;
mfree(mdp, ADDRESS(block + blocks));
mdp->heapinfo[block].busy_block.size = blocks;