From 199b029b33b5b9fbe1eacb50828914f3b38bde2f Mon Sep 17 00:00:00 2001 From: mquinson Date: Wed, 5 May 2010 23:15:21 +0000 Subject: [PATCH] Add the model-checker to the build tree. It's not used yet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@7701 48e7efb5-ca39-0410-a469-dd3cf9ba447f --- buildtools/Cmake/src/CMakeDefinePackages.txt | 11 + src/Makefile.am | 8 +- src/mc/README | 9 + src/mc/mc_checkpoint.c | 23 ++ src/mc/mc_dfs.c | 150 ++++++++++ src/mc/mc_dpor.c | 195 +++++++++++++ src/mc/mc_global.c | 287 +++++++++++++++++++ src/mc/mc_memory.c | 183 ++++++++++++ src/mc/mc_transition.c | 104 +++++++ src/mc/memory_map.c | 125 ++++++++ src/mc/private.h | 154 ++++++++++ src/xbt/log.c | 1 + 12 files changed, 1249 insertions(+), 1 deletion(-) create mode 100644 src/mc/README create mode 100644 src/mc/mc_checkpoint.c create mode 100644 src/mc/mc_dfs.c create mode 100644 src/mc/mc_dpor.c create mode 100644 src/mc/mc_global.c create mode 100644 src/mc/mc_memory.c create mode 100644 src/mc/mc_transition.c create mode 100644 src/mc/memory_map.c create mode 100644 src/mc/private.h diff --git a/buildtools/Cmake/src/CMakeDefinePackages.txt b/buildtools/Cmake/src/CMakeDefinePackages.txt index dd6419e0db..9b717659f5 100755 --- a/buildtools/Cmake/src/CMakeDefinePackages.txt +++ b/buildtools/Cmake/src/CMakeDefinePackages.txt @@ -327,6 +327,16 @@ ${PROJECT_DIRECTORY}/src/bindings/ruby/rb_msg_task.c ${PROJECT_DIRECTORY}/src/bindings/ruby/rb_application_handler.c ) +set(MC_SRC + ${PROJECT_DIRECTORY}/src/mc/mc_memory.c + ${PROJECT_DIRECTORY}/src/mc/mc_checkpoint.c + ${PROJECT_DIRECTORY}/src/mc/memory_map.c + ${PROJECT_DIRECTORY}/src/mc/mc_global.c + ${PROJECT_DIRECTORY}/src/mc/mc_dfs.c + ${PROJECT_DIRECTORY}/src/mc/mc_dpor.c + ${PROJECT_DIRECTORY}/src/mc/mc_transition.c +) + set(install_bins ${PROJECT_DIRECTORY}/src/smpi/smpicc ${PROJECT_DIRECTORY}/src/smpi/smpirun @@ -510,6 +520,7 @@ set(simgrid_sources ${GRAS_COMMON_SRC} ${GRAS_SG_SRC} ${AMOK_SRC} + ${MC_SRC} ) ### Gras Lib sources diff --git a/src/Makefile.am b/src/Makefile.am index 9cbfb1427e..0ff1ac69b5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -345,6 +345,12 @@ AMOK_SRC= \ amok/Bandwidth/bandwidth.c amok/Bandwidth/saturate.c \ amok/PeerManagement/peermanagement.c +MC_SRC= \ + mc/mc_memory.c mc/mc_checkpoint.c \ + mc/memory_map.c mc/mc_global.c \ + mc/mc_dfs.c mc/mc_dpor.c \ + mc/mc_transition.c + ############################## # Deal with optional modules # ############################## @@ -364,7 +370,7 @@ lib_LTLIBRARIES= libsimgrid.la libgras.la libsmpi.la gras_sources=$(XBT_SRC) $(GRAS_COMMON_SRC) $(GRAS_RL_SRC) $(AMOK_SRC) simgrid_sources=$(XBT_SRC) $(SURF_SRC) $(GTNETS_USED) \ - $(SIMIX_SRC) $(MSG_SRC) $(SIMDAG_SRC) \ + $(SIMIX_SRC) $(MC_SRC) $(MSG_SRC) $(SIMDAG_SRC) \ $(GRAS_COMMON_SRC) $(GRAS_SG_SRC) $(AMOK_SRC) \ $(TRACING_SRC) diff --git a/src/mc/README b/src/mc/README new file mode 100644 index 0000000000..e2c38da1fc --- /dev/null +++ b/src/mc/README @@ -0,0 +1,9 @@ +This file lists the issues to solve to achieve a the full integration of the MC branch: +- Model-checker entry point: + Up to now, the main function of each user API has to be modified to call MC_modelcheck instead of SIMIX_solve. + It would be nice to have a command line option like --model-check to determine the right behaviour. + +- Memory managment routines: + Because mc_memory.c redefines malloc, calloc, realloc and free, now even the simulator is going to use + the mmalloc library. This is no good because it is far slower than GNU's malloc, so some black magic should be + used to link against one library or the other depending on the mode choosed by the user. diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c new file mode 100644 index 0000000000..5abffdad14 --- /dev/null +++ b/src/mc/mc_checkpoint.c @@ -0,0 +1,23 @@ +#include "private.h" + +void MC_take_snapshot(mc_snapshot_t snapshot) +{ +/* Save the heap! */ + snapshot->heap_size = MC_save_heap(&(snapshot->heap)); + +/* Save data and bss that */ + snapshot->data_size = MC_save_dataseg(&(snapshot->data)); +} + +void MC_restore_snapshot(mc_snapshot_t snapshot) +{ + MC_restore_heap(snapshot->heap, snapshot->heap_size); + MC_restore_dataseg(snapshot->data, snapshot->data_size); +} + +void MC_free_snapshot(mc_snapshot_t snapshot) +{ + xbt_free(snapshot->heap); + xbt_free(snapshot->data); + xbt_free(snapshot); +} diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c new file mode 100644 index 0000000000..af28bba7c0 --- /dev/null +++ b/src/mc/mc_dfs.c @@ -0,0 +1,150 @@ +#include "private.h" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, + "Logging specific to MC DFS exploration"); + + +void MC_dfs_init() +{ + mc_transition_t trans = NULL; + mc_state_t initial_state = NULL; + xbt_setset_cursor_t cursor = NULL; + + MC_SET_RAW_MEM; + initial_state = MC_state_new(); + /* Add the state data structure for the initial state */ + xbt_fifo_unshift(mc_stack, initial_state); + MC_UNSET_RAW_MEM; + + DEBUG0("**************************************************"); + DEBUG0("Initial state"); + + /* Schedule all the processes to detect the transitions from the initial state */ + MC_schedule_enabled_processes(); + + MC_SET_RAW_MEM; + xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions); + xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){ + if(trans->type == mc_wait + && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){ + xbt_setset_set_remove(initial_state->enabled_transitions, trans); + } + } + + /* Fill the interleave set of the initial state with all enabled transitions */ + xbt_setset_add(initial_state->interleave, initial_state->enabled_transitions); + + /* Update Statistics */ + mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions); + + MC_UNSET_RAW_MEM; +} + +/** + * \brief Perform the model-checking operation using a depth-first search exploration + * + * It performs the model-checking operation by executing all possible scheduling of the communication actions + * \return The time spent to execute the simulation or -1 if the simulation ended + */ +void MC_dfs(void) +{ + mc_transition_t trans = NULL; + mc_state_t current_state = NULL; + mc_state_t next_state = NULL; + xbt_setset_cursor_t cursor = NULL; + + while(xbt_fifo_size(mc_stack) > 0){ + DEBUG0("**************************************************"); + + /* FIXME: Think about what happens if there are no transitions but there are + some actions on the models. (ex. all the processes do a sleep(0) in a round). */ + + /* Get current state */ + current_state = (mc_state_t) + xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + + /* If there are transitions to execute and the maximun depth has not been reached + then perform one step of the exploration algorithm */ + if(xbt_setset_set_size(current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){ + + DEBUG3("Exploration detph=%d (state=%p)(%d transitions)", xbt_fifo_size(mc_stack), + current_state, xbt_setset_set_size(current_state->interleave)); + + /* Update statistics */ + mc_stats->visited_states++; + mc_stats->executed_transitions++; + + /* Choose a transition to execute from the interleave set of the current state, + and create the data structures for the new expanded state in the exploration + stack. */ + MC_SET_RAW_MEM; + trans = xbt_setset_set_extract(current_state->interleave); + + /* Define it as the executed transition of this state */ + current_state->executed_transition = trans; + + next_state = MC_state_new(); + xbt_fifo_unshift(mc_stack, next_state); + MC_UNSET_RAW_MEM; + + DEBUG1("Executing transition %s", trans->name); + SIMIX_process_schedule(trans->process); + + /* Do all surf's related black magic tricks to keep all working */ + MC_execute_surf_actions(); + + /* Schedule every process that got enabled due to the executed transition */ + MC_schedule_enabled_processes(); + + /* Calculate the enabled transitions set of the next state: + -add the transition sets of the current state and the next state + -remove the executed transition from that set + -remove all the transitions that are disabled (mc_wait only) + -use the resulting set as the enabled transitions of the next state */ + MC_SET_RAW_MEM; + xbt_setset_add(next_state->transitions, current_state->transitions); + xbt_setset_set_remove(next_state->transitions, trans); + xbt_setset_add(next_state->enabled_transitions, next_state->transitions); + xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){ + if(trans->type == mc_wait + && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){ + xbt_setset_set_remove(next_state->enabled_transitions, trans); + } + } + + /* Fill the interleave set of the new state with all enabled transitions */ + xbt_setset_add(next_state->interleave, next_state->enabled_transitions); + MC_UNSET_RAW_MEM; + + /* Update Statistics */ + mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions); + + /* Let's loop again */ + + /* The interleave set is empty or the maximum depth is reached, let's back-track */ + }else{ + DEBUG0("There are no more actions to run"); + + MC_SET_RAW_MEM; + xbt_fifo_shift(mc_stack); + MC_state_delete(current_state); + + /* Go backwards in the stack until we find a state with transitions in the interleave set */ + while(xbt_fifo_size(mc_stack) > 0 && (current_state = (mc_state_t)xbt_fifo_shift(mc_stack))){ + if(xbt_setset_set_size(current_state->interleave) == 0){ + MC_state_delete(current_state); + }else{ + xbt_fifo_unshift(mc_stack, current_state); + DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack)); + MC_replay(mc_stack); + MC_UNSET_RAW_MEM; + /* Let's loop again */ + break; + } + } + } + } + MC_UNSET_RAW_MEM; + /* We are done, show the statistics and return */ + MC_print_statistics(mc_stats); +} \ No newline at end of file diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c new file mode 100644 index 0000000000..88992b91aa --- /dev/null +++ b/src/mc/mc_dpor.c @@ -0,0 +1,195 @@ +/* Copyright (c) 2008 Martin Quinson, Cristian Rosa. + All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "private.h" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, + "Logging specific to MC DPOR exploration"); + +/** + * \brief Initialize the DPOR exploration algorithm + */ +void MC_dpor_init() +{ + mc_state_t initial_state = NULL; + mc_transition_t trans = NULL; + xbt_setset_cursor_t cursor = NULL; + + /* Create the initial state and push it into the exploration stack */ + MC_SET_RAW_MEM; + initial_state = MC_state_new(); + xbt_fifo_unshift(mc_stack, initial_state); + MC_UNSET_RAW_MEM; + + /* Schedule all the processes to detect the transitions of the initial state */ + DEBUG0("**************************************************"); + DEBUG0("Initial state"); + MC_schedule_enabled_processes(); + + MC_SET_RAW_MEM; + xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions); + xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){ + if(trans->type == mc_wait + && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){ + xbt_setset_set_remove(initial_state->enabled_transitions, trans); + } + } + + /* Fill the interleave set of the initial state with an enabled process */ + trans = xbt_setset_set_choose(initial_state->enabled_transitions); + if(trans) + xbt_setset_set_insert(initial_state->interleave, trans); + MC_UNSET_RAW_MEM; + + trans->refcount++; + + /* Update Statistics */ + mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions); +} + + +/** + * \brief Perform the model-checking operation using a depth-first search exploration + * with Dynamic Partial Order Reductions + */ +void MC_dpor(void) +{ + mc_transition_t trans = NULL; + mc_state_t current_state = NULL; + mc_state_t next_state = NULL; + xbt_setset_cursor_t cursor = NULL; + + while(xbt_fifo_size(mc_stack) > 0){ + + DEBUG0("**************************************************"); + + /* FIXME: Think about what happen if there are no transitions but there are + some actions on the models. (ex. all the processes do a sleep(0) in a round). */ + + /* Get current state */ + current_state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + + /* If there are transitions to execute and the maximun depth has not been reached + then perform one step of the exploration algorithm */ + if(xbt_setset_set_size(current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){ + + DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack), + current_state, xbt_setset_set_size(current_state->interleave), + xbt_setset_set_size(current_state->enabled_transitions)); + + xbt_setset_foreach(current_state->enabled_transitions, cursor, trans){ + DEBUG1("\t %s", trans->name); + } + + /* Update statistics */ + mc_stats->visited_states++; + mc_stats->executed_transitions++; + + /* Choose a transition to execute from the interleave set of the current + state, and create the data structures for the new expanded state in the + exploration stack. */ + MC_SET_RAW_MEM; + trans = xbt_setset_set_extract(current_state->interleave); + next_state = MC_state_new(); + xbt_fifo_unshift(mc_stack, next_state); + + /* Add the transition in the done set of the current state */ + xbt_setset_set_insert(current_state->done, trans); + trans->refcount++; + + /* Set it as the executed transition of the current state */ + current_state->executed_transition = trans; + MC_UNSET_RAW_MEM; + + /* Execute the selected transition by scheduling it's associated process. + Then schedule every process that got ready to run due to the execution + of the transition */ + DEBUG1("Executing transition %s", trans->name); + SIMIX_process_schedule(trans->process); + MC_execute_surf_actions(); /* Do surf's related black magic */ + MC_schedule_enabled_processes(); + + /* Calculate the enabled transitions set of the next state: + -add the transition sets of the current state and the next state + -remove the executed transition from that set + -remove all the transitions that are disabled (mc_wait only) + -use the resulting set as the enabled transitions of the next state */ + MC_SET_RAW_MEM; + xbt_setset_add(next_state->transitions, current_state->transitions); + xbt_setset_set_remove(next_state->transitions, trans); + xbt_setset_add(next_state->enabled_transitions, next_state->transitions); + xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){ + if(trans->type == mc_wait + && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){ + xbt_setset_set_remove(next_state->enabled_transitions, trans); + } + } + + /* Choose one transition to interleave from the enabled transition set */ + trans = xbt_setset_set_choose(next_state->enabled_transitions); + if(trans) + xbt_setset_set_insert(next_state->interleave, trans); + MC_UNSET_RAW_MEM; + + /* Update Statistics */ + mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions); + + /* Let's loop again */ + + /* The interleave set is empty or the maximum depth is reached, let's back-track */ + }else{ + DEBUG0("There are no more transitions to interleave."); + + mc_transition_t q = NULL; + xbt_fifo_item_t item = NULL; + mc_state_t state = NULL; + + //MC_show_stack(mc_stack); + + /* Trash the current state, no longer needed */ + MC_SET_RAW_MEM; + xbt_fifo_shift(mc_stack); + MC_state_delete(current_state); + + /* 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 transition that has generated it + (from it's predecesor state), depends on any other previous transition + executed before it. If it does then add it to the interleave set of the + state that executed that previous transition. */ + while((current_state = xbt_fifo_shift(mc_stack)) != NULL){ + q = current_state->executed_transition; + xbt_fifo_foreach(mc_stack, item, state, mc_state_t){ + if(MC_transition_depend(q, state->executed_transition)){ + DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q); + xbt_setset_foreach(state->enabled_transitions, cursor, trans){ + if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){ + DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans); + xbt_setset_set_insert(state->interleave, trans); + break; + } + } + if(trans) + break; + } + } + if(xbt_setset_set_size(current_state->interleave) > 0){ + /* We found a back-tracking point, let's loop */ + xbt_fifo_unshift(mc_stack, current_state); + DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack)); + MC_replay(mc_stack); + MC_UNSET_RAW_MEM; + break; + }else{ + MC_state_delete(current_state); + } + } + } + } + DEBUG0("We are done"); + /* We are done, show the statistics and return */ + MC_print_statistics(mc_stats); +} \ No newline at end of file diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c new file mode 100644 index 0000000000..97e3e2a235 --- /dev/null +++ b/src/mc/mc_global.c @@ -0,0 +1,287 @@ +#include "../surf/surf_private.h" +#include "../simix/private.h" +#include "xbt/fifo.h" +#include "private.h" + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, + "Logging specific to MC (global)"); + +/* MC global data structures */ +mc_snapshot_t initial_snapshot = NULL; +xbt_fifo_t mc_stack = NULL; +xbt_setset_t mc_setset = NULL; +mc_stats_t mc_stats = NULL; +char mc_replay_mode = FALSE; + +/** + * \brief Initialize the model-checker data structures + */ +void MC_init(int method) +{ + /* Check if MC is already initialized */ + if(initial_snapshot) + return; + + /* Initialize the data structures that must be persistent across every + iteration of the model-checker (in RAW memory) */ + MC_SET_RAW_MEM; + + /* Initialize statistics */ + mc_stats = xbt_new0(s_mc_stats_t, 1); + mc_stats->state_size = 1; + + /* Create exploration stack */ + mc_stack = xbt_fifo_new(); + + /* Create the container for the sets */ + mc_setset = xbt_setset_new(20); + + switch(method){ + case 0: + MC_dfs_init(); + break; + case 1: + MC_dpor_init(); + break; + default: + break; + } + + /* Save the initial state */ + MC_SET_RAW_MEM; + initial_snapshot = xbt_new(s_mc_snapshot_t,1); + MC_take_snapshot(initial_snapshot); + MC_UNSET_RAW_MEM; +} + +void MC_modelcheck(int method){ + + MC_init(method); + + switch(method){ + case 0: + MC_dfs(); + break; + case 1: + MC_dpor(); + break; + default: + break; + } +} + + +/** + * \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) +{ + xbt_fifo_item_t item; + mc_state_t state; + mc_transition_t trans; + + DEBUG0("**** Begin Replay ****"); + + /* Restore the initial state */ + MC_restore_snapshot(initial_snapshot); + + mc_replay_mode = TRUE; + + MC_UNSET_RAW_MEM; + + /* 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)){ + + state = (mc_state_t) xbt_fifo_get_item_content(item); + trans = state->executed_transition; + + /* Update statistics */ + mc_stats->visited_states++; + mc_stats->executed_transitions++; + + DEBUG1("Executing transition %s", trans->name); + SIMIX_process_schedule(trans->process); + + /* Do all surf's related black magic tricks to keep all working */ + MC_execute_surf_actions(); + + /* Schedule every process that got enabled due to the executed transition */ + MC_schedule_enabled_processes(); + } + mc_replay_mode = FALSE; + DEBUG0("**** End Replay ****"); +} + +/** + * \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(xbt_fifo_t stack) +{ + mc_state_t state; + mc_transition_t trans; + + MC_SET_RAW_MEM; + while( (state = (mc_state_t)xbt_fifo_pop(stack)) != NULL ){ + trans = state->executed_transition; + if(trans) + INFO1("%s", trans->name); + + MC_state_delete(state); + } + MC_UNSET_RAW_MEM; +} + +void MC_show_stack(xbt_fifo_t stack) +{ + mc_state_t state; + mc_transition_t trans; + xbt_fifo_item_t item; + + INFO0("==========================="); + for(item=xbt_fifo_get_last_item(stack); + (item?(state=(mc_state_t)(xbt_fifo_get_item_content(item))):(NULL)); \ + item=xbt_fifo_get_prev_item(item)){ + trans = state->executed_transition; + if(trans){ + INFO1("%s", trans->name); + } + } +} + + +/** + * \brief Schedules all the process that are ready to run + * As a side effect it performs some clean-up required by SIMIX + */ +void MC_schedule_enabled_processes(void) +{ + smx_process_t process; + + //SIMIX_process_empty_trash(); + + /* Schedule every process that is ready to run due to an finished action */ + while ((process = xbt_swag_extract(simix_global->process_to_run))) { + DEBUG2("Scheduling %s on %s", process->name, process->smx_host->name); + SIMIX_process_schedule(process); + } +} + +/******************************** States **************************************/ + +/** + * \brief Creates a state data structure used by the exploration algorithm + */ +mc_state_t MC_state_new(void) +{ + mc_state_t state = NULL; + + state = xbt_new0(s_mc_state_t, 1); + state->transitions = xbt_setset_new_set(mc_setset); + state->enabled_transitions = xbt_setset_new_set(mc_setset); + state->interleave = xbt_setset_new_set(mc_setset); + state->done = xbt_setset_new_set(mc_setset); + state->executed_transition = NULL; + + mc_stats->expanded_states++; + + return state; +} +/** + * \brief Deletes a state data structure + * \param trans The state to be deleted + */ +void MC_state_delete(mc_state_t state) +{ + /*if(state->executed_transition) + MC_transition_delete(state->executed_transition);*/ + xbt_setset_destroy_set(state->transitions); + xbt_setset_destroy_set(state->enabled_transitions); + xbt_setset_destroy_set(state->interleave); + xbt_setset_destroy_set(state->done); + + xbt_free(state); +} + +/************************** SURF Emulation ************************************/ + +/* Dirty hack, we manipulate surf's clock to simplify the integration of the + model-checker */ +extern double NOW; + +/** + * \brief Executes all the actions at every model + */ +void MC_execute_surf_actions(void) +{ + unsigned int iter; + surf_action_t action = NULL; + surf_model_t model = NULL; + smx_action_t smx_action = NULL; + + /* Execute all the actions in every model */ + xbt_dynar_foreach(model_list, iter, model){ + while ((action = xbt_swag_extract(model->states.running_action_set))){ + /* FIXME: timeouts are not calculated correctly */ + if(NOW >= action->max_duration){ + surf_action_state_set(action, SURF_ACTION_DONE); + smx_action = action->data; + DEBUG5("Resource [%s] (%d): Executing RUNNING action \"%s\" (%p) MaxDuration %lf", + model->name, xbt_swag_size(model->states.running_action_set), + smx_action->name, smx_action, action->max_duration); + + /* Copy the transfered data of the completed network actions */ + /* FIXME: be carefull it might not be an action of the network model */ + if(smx_action && smx_action->data != NULL) + SIMIX_network_copy_data((smx_comm_t)smx_action->data); + + if(smx_action) + SIMIX_action_signal_all(smx_action); + } + } + /*FIXME: check if this is always empty or not */ + while ((action = xbt_swag_extract(model->states.failed_action_set))) { + smx_action = action->data; + DEBUG4("Resource [%s] (%d): Executing FAILED action \"%s\" (%p)", + model->name, xbt_swag_size(model->states.running_action_set), + smx_action->name, smx_action); + if (smx_action) + SIMIX_action_signal_all(smx_action); + } + } + /* That's it, now go one step deeper into the model-checking process! */ + NOW += 0.5; /* FIXME: Check time increases*/ +} + +/****************************** Statistics ************************************/ +void MC_print_statistics(mc_stats_t stats) +{ + INFO1("State space size ~= %lu", stats->state_size); + INFO1("Expanded states = %lu", stats->expanded_states); + INFO1("Visited states = %lu", stats->visited_states); + INFO1("Executed transitions = %lu", stats->executed_transitions); + INFO1("Expanded / Visited = %lf", + (double)stats->visited_states / stats->expanded_states); + /*INFO1("Exploration coverage = %lf", + (double)stats->expanded_states / stats->state_size);*/ +} + +/************************* Assertion Checking *********************************/ +void MC_assert(int prop) +{ + if(!prop){ + INFO0("**************************"); + INFO0("*** PROPERTY NOT VALID ***"); + INFO0("**************************"); + INFO0("Counter-example execution trace:"); + MC_dump_stack(mc_stack); + MC_print_statistics(mc_stats); + xbt_abort(); + } +} + diff --git a/src/mc/mc_memory.c b/src/mc/mc_memory.c new file mode 100644 index 0000000000..7f9aa05e4e --- /dev/null +++ b/src/mc/mc_memory.c @@ -0,0 +1,183 @@ +#include +#include +#include "mc/mc.h" +#include "xbt/sysdep.h" +#include "private.h" +#include "xbt/log.h" +#include +#define _GNU_SOURCE + +extern char *basename (__const char *__filename); + +#define HEAP_OFFSET 20480000 /* Safety gap from the heap's break adress */ +#define STD_HEAP_SIZE 20480000 /* Maximum size of the system's heap */ + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc, + "Logging specific to MC (memory)"); + +/* Pointers to each of the heap regions to use */ +void *std_heap; +void *raw_heap; +void *actual_heap; + +/* Pointers to the begining and end of the .data and .bss segment of libsimgrid */ +/* They are initialized once at memory_init */ +void *libsimgrid_data_addr_start = NULL; +size_t libsimgrid_data_size = 0; + +/* Initialize the model-checker memory subsystem */ +/* It creates the heap regions and set the default one */ +void MC_memory_init() +{ +/* Create the first region HEAP_OFFSET bytes after the heap break address */ + std_heap = mmalloc_attach(-1, (char *)sbrk(0) + HEAP_OFFSET); + xbt_assert(std_heap != NULL); + +/* Create the sencond region a page after the first one ends */ +/* FIXME: do not hardcode the page size to 4096 */ + raw_heap = mmalloc_attach(-1, (char *)(std_heap) + STD_HEAP_SIZE + 4096); + xbt_assert(raw_heap != NULL); + + MC_SET_RAW_MEM; + +/* Get the start address and size of libsimgrid's data segment */ +/* CAVEAT: Here we are assuming several things, first that get_memory_map() */ +/* returns an array with the maps sorted from lower addresses to higher */ +/* ones. Second, that libsimgrid's data takes ONLY ONE page. */ + int i; + char *libname, *tmp; + + /* Get memory map */ + memory_map_t maps; + maps = get_memory_map(); + + for(i=0; i < maps->mapsize; i++){ + + if(maps->regions[i].inode != 0){ + + tmp = xbt_strdup(maps->regions[i].pathname); + libname = basename(tmp); + + if( strncmp("libsimgrid.so.2.0.0", libname, 18) == 0 && maps->regions[i].perms & MAP_WRITE){ + libsimgrid_data_addr_start = maps->regions[i].start_addr; + libsimgrid_data_size = (size_t)((char *)maps->regions[i+1].end_addr - (char *)maps->regions[i].start_addr); + xbt_free(tmp); + break; + } + xbt_free(tmp); + } + } + + xbt_assert0(libsimgrid_data_addr_start != NULL, + "Cannot determine libsimgrid's .data segment address"); + + MC_UNSET_RAW_MEM; +} + +/* Finish the memory subsystem */ +void MC_memory_exit() +{ + mmalloc_detach(std_heap); + mmalloc_detach(raw_heap); + actual_heap = NULL; +} + +void *malloc(size_t n) +{ + void *ret = mmalloc(actual_heap, n); + + DEBUG2("%zu bytes were allocated at %p",n, ret); + return ret; +} + +void *calloc(size_t nmemb, size_t size) +{ + size_t total_size = nmemb * size; + void *ret = mmalloc(actual_heap, total_size); + +/* Fill the allocated memory with zeroes to mimic calloc behaviour */ + memset(ret,'\0', total_size); + + DEBUG2("%zu bytes were mallocated and zeroed at %p",total_size, ret); + return ret; +} + +void *realloc(void *p, size_t s) +{ + void *ret = NULL; + + if (s) { + if (p) + ret = mrealloc(actual_heap, p,s); + else + ret = malloc(s); + } else { + if (p) { + free(p); + } + } + + DEBUG2("%zu bytes were reallocated at %p",s,ret); + return ret; +} + +void free(void *p) +{ + DEBUG1("%p was freed",p); + xbt_assert(actual_heap != NULL); + return mfree(actual_heap, p); +} + +/* FIXME: Horrible hack! because the mmalloc library doesn't provide yet of */ +/* an API to query about the status of a heap, we simply call mmstats and */ +/* because I now how does structure looks like, then I redefine it here */ + +struct mstats + { + size_t bytes_total; /* Total size of the heap. */ + size_t chunks_used; /* Chunks allocated by the user. */ + size_t bytes_used; /* Byte total of user-allocated chunks. */ + size_t chunks_free; /* Chunks in the free list. */ + size_t bytes_free; /* Byte total of chunks in the free list. */ + }; + +extern struct mstats mmstats(void *); + +/* Copy std_heap to "to_heap" allocating the required space for it */ +size_t MC_save_heap(void **to_heap) +{ + size_t heap_size = mmstats(std_heap).bytes_total; + + *to_heap = calloc(heap_size, 1); + + xbt_assert(*to_heap != NULL); + + memcpy(*to_heap, std_heap, heap_size); + + return heap_size; +} + +/* Copy the data segment of libsimgrid to "data" allocating the space for it */ +size_t MC_save_dataseg(void **data) +{ + *data = calloc(libsimgrid_data_size, 1); + memcpy(*data, libsimgrid_data_addr_start, libsimgrid_data_size); + return libsimgrid_data_size; +} + +/* Restore std_heap from "src_heap" */ +void MC_restore_heap(void *src_heap, size_t size) +{ + memcpy(std_heap, src_heap, size); +} + +/* Restore the data segment of libsimgrid from "src_data" */ +void MC_restore_dataseg(void *src_data, size_t size) +{ + memcpy(libsimgrid_data_addr_start, src_data, size); +} + + + + + diff --git a/src/mc/mc_transition.c b/src/mc/mc_transition.c new file mode 100644 index 0000000000..4e5c95d349 --- /dev/null +++ b/src/mc/mc_transition.c @@ -0,0 +1,104 @@ +#include "private.h" + +/** + * \brief Create a model-checker transition and add it to the set of avaiable + * transitions of the current state, if not running in replay mode. + * \param process The process who wants to perform the transition + * \param comm The type of then transition (comm_send, comm_recv) +*/ +mc_transition_t MC_create_transition(mc_trans_type_t type, smx_process_t p, smx_rdv_t rdv, smx_comm_t comm) +{ + mc_state_t current_state = NULL; + char *type_str = NULL; + + if(!mc_replay_mode){ + MC_SET_RAW_MEM; + mc_transition_t trans = xbt_new0(s_mc_transition_t, 1); + trans->refcount = 1; + + /* Generate a string for the "type" */ + switch(type){ + case mc_isend: + type_str = bprintf("iSend"); + break; + case mc_irecv: + type_str = bprintf("iRecv"); + break; + case mc_wait: + type_str = bprintf("Wait"); + break; + case mc_waitany: + type_str = bprintf("WaitAny"); + break; + default: + xbt_die("Invalid transition type"); + } + + trans->name = bprintf("[%s][%s] %s (%p)", p->smx_host->name, p->name, type_str, trans); + xbt_free(type_str); + + trans->type = type; + trans->process = p; + trans->rdv = rdv; + trans->comm = comm; + /* Push it onto the enabled transitions set of the current state */ + current_state = (mc_state_t) + xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + xbt_setset_set_insert(current_state->transitions, trans); + MC_UNSET_RAW_MEM; + return trans; + } + return NULL; +} + +/** + * \brief Associate a communication to a transition + * \param trans The transition + * \param comm The communication + */ +void MC_transition_set_comm(mc_transition_t trans, smx_comm_t comm) +{ + if(trans) + trans->comm = comm; + return; +} + +/** + * \brief Deletes a transition + * \param trans The transition to be deleted + */ +void MC_transition_delete(mc_transition_t trans) +{ + /* Only delete it if there are no references, otherwise decrement refcount */ + if(--trans->refcount == 0){ + xbt_free(trans->name); + xbt_free(trans); + } +} + +/** + * \brief Determine if two transitions are dependent + * \param t1 a transition + * \param t2 a transition + * \return TRUE if \a t1 and \a t2 are dependent. FALSE otherwise. + */ +int MC_transition_depend(mc_transition_t t1, mc_transition_t t2) +{ + /* The semantics of SIMIX network operations implies that ONLY transitions + of the same type, in the same rendez-vous point, and from different processes + are dependant, except wait transitions that are always independent */ + if( t1->type == mc_wait + || t2->type == mc_wait + || t1->process == t2->process + || t1->type != t2->type + || t1->rdv != t2->rdv) + return FALSE; + else + return TRUE; +} + + + + + + diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c new file mode 100644 index 0000000000..fb91333798 --- /dev/null +++ b/src/mc/memory_map.c @@ -0,0 +1,125 @@ +#define _GNU_SOURCE +#include "private.h" +#include + +memory_map_t get_memory_map(void) +{ + FILE *fp; /* File pointer to process's proc maps file */ + char *line = NULL; /* Temporal storage for each line that is readed */ + ssize_t read; /* Number of bytes readed */ + size_t n = 0; /* Amount of bytes to read by getline */ + memory_map_t ret = NULL; /* The memory map to return */ + +/* The following variables are used during the parsing of the file "maps" */ + s_map_region memreg; /* temporal map region used for creating the map */ + char *lfields[6], *tok, *endptr; + int i; + +/* Open the actual process's proc maps file and create the memory_map_t */ +/* to be returned. */ + fp = fopen("/proc/self/maps","r"); + + if(!fp) + xbt_abort(); + + ret = xbt_new0(s_memory_map_t,1); + + /* Read one line at the time, parse it and add it to the memory map to be returned */ + while((read = getline(&line, &n, fp)) != -1) { + + /* Wipeout the new line character */ + line[read - 1] = '\0'; + + /* Tokenize the line using spaces as delimiters and store each token */ + /* in lfields array. We expect 5 tokens/fields */ + lfields[0] = strtok(line, " "); + + for(i=1; i < 6 && lfields[i - 1] != NULL; i++){ + lfields[i] = strtok(NULL, " "); + } + + /* Check to see if we got the expected amount of columns */ + if(i < 6) + xbt_abort(); + + /* Ok we are good enough to try to get the info we need */ + /* First get the start and the end address of the map */ + tok = strtok(lfields[0], "-"); + if(tok == NULL) + xbt_abort(); + + memreg.start_addr = (void *)strtoul(tok, &endptr, 16); + /* Make sure that the entire string was an hex number */ + if(*endptr != '\0') + xbt_abort(); + + tok = strtok(NULL, "-"); + if(tok == NULL) + xbt_abort(); + + memreg.end_addr = (void *)strtoul(tok, &endptr, 16); + /* Make sure that the entire string was an hex number */ + if(*endptr != '\0') + xbt_abort(); + + /* Get the permissions flags */ + if(strlen(lfields[1]) < 4) + xbt_abort(); + + memreg.perms = 0; + + for(i=0; i<3; i++) + if(lfields[1][i] != '-') + memreg.perms |= 1 << i; + + if(lfields[1][4] == 'p') + memreg.perms |= MAP_PRIV; + + else if (lfields[1][4] == 's') + memreg.perms |= MAP_SHARED; + + /* Get the offset value */ + memreg.offset = (void *)strtoul(lfields[2], &endptr, 16); + /* Make sure that the entire string was an hex number */ + if(*endptr != '\0') + xbt_abort(); + + /* Get the device major:minor bytes */ + tok = strtok(lfields[3], ":"); + if(tok == NULL) + xbt_abort(); + + memreg.dev_major = (char)strtoul(tok, &endptr, 16); + /* Make sure that the entire string was an hex number */ + if(*endptr != '\0') + xbt_abort(); + + tok = strtok(NULL, ":"); + if(tok == NULL) + xbt_abort(); + + memreg.dev_minor = (char)strtoul(tok, &endptr, 16); + /* Make sure that the entire string was an hex number */ + if(*endptr != '\0') + xbt_abort(); + + /* Get the inode number and make sure that the entire string was a long int*/ + memreg.inode = strtoul(lfields[4], &endptr, 10); + if(*endptr != '\0') + xbt_abort(); + + /* And finally get the pathname */ + memreg.pathname = xbt_strdup(lfields[5]); + + /* Create space for a new map region in the region's array and copy the */ + /* parsed stuff from the temporal memreg variable */ + ret->regions = xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1)); + memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg)); + ret->mapsize++; + } + + if(line) + free(line); + + return ret; +} diff --git a/src/mc/private.h b/src/mc/private.h new file mode 100644 index 0000000000..56a10029da --- /dev/null +++ b/src/mc/private.h @@ -0,0 +1,154 @@ +/* $Id: private.h 5497 2008-05-26 12:19:15Z cristianrosa $ */ + +/* Copyright (c) 2007 Arnaud Legrand, Bruno Donnassolo. + All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef MC_PRIVATE_H +#define MC_PRIVATE_H + +#include +#include "mc/mc.h" +#include "mc/datatypes.h" +#include "xbt/fifo.h" +#include "xbt/setset.h" +#include "xbt/config.h" +#include "xbt/function_types.h" +#include "mmalloc.h" +#include "../simix/private.h" + +/****************************** Snapshots ***********************************/ + +/*typedef struct s_mc_process_checkpoint { + xbt_checkpoint_t machine_state; Here we save the cpu + stack +} s_mc_process_checkpoint_t, *mc_process_checkpoint_t;*/ + +typedef struct s_mc_snapshot { + size_t heap_size; + size_t data_size; + void* data; + void* heap; + +} s_mc_snapshot_t, *mc_snapshot_t; + +extern mc_snapshot_t initial_snapshot; + +size_t MC_save_heap(void **); +void MC_restore_heap(void *, size_t); + +size_t MC_save_dataseg(void **); +void MC_restore_dataseg(void *, size_t); + +void MC_take_snapshot(mc_snapshot_t); +void MC_restore_snapshot(mc_snapshot_t); +void MC_free_snapshot(mc_snapshot_t); + +/********************************* MC Global **********************************/ + +/* Bound of the MC depth-first search algorithm */ +#define MAX_DEPTH 1000 + +extern char mc_replay_mode; + +void MC_show_stack(xbt_fifo_t stack); +void MC_dump_stack(xbt_fifo_t stack); +void MC_execute_surf_actions(void); +void MC_replay(xbt_fifo_t stack); +void MC_schedule_enabled_processes(void); +void MC_dfs_init(void); +void MC_dpor_init(void); +void MC_dfs(void); +void MC_dpor(void); + +/******************************* Transitions **********************************/ +typedef struct s_mc_transition{ + XBT_SETSET_HEADERS; + char* name; + unsigned int refcount; + mc_trans_type_t type; + smx_process_t process; + smx_rdv_t rdv; + smx_comm_t comm; /* reference to the simix network communication */ +} s_mc_transition_t; + +void MC_transition_delete(mc_transition_t); +int MC_transition_depend(mc_transition_t, mc_transition_t); + +/******************************** States **************************************/ +typedef struct mc_state{ + xbt_setset_set_t transitions; + xbt_setset_set_t enabled_transitions; + xbt_setset_set_t interleave; + xbt_setset_set_t done; + mc_transition_t executed_transition; +} s_mc_state_t, *mc_state_t; + +extern xbt_fifo_t mc_stack; +extern xbt_setset_t mc_setset; + +mc_state_t MC_state_new(void); +void MC_state_delete(mc_state_t); + +/****************************** Statistics ************************************/ +typedef struct mc_stats{ + unsigned long state_size; + unsigned long visited_states; + unsigned long expanded_states; + unsigned long executed_transitions; +}s_mc_stats_t, *mc_stats_t; + +extern mc_stats_t mc_stats; + +void MC_print_statistics(mc_stats_t); + +/********************************** MEMORY ******************************/ +/* The possible memory modes for the modelchecker are standard and raw. */ +/* Normally the system should operate in std, for switching to raw mode */ +/* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */ + +extern void *actual_heap; +extern void *std_heap; +extern void *raw_heap; +extern void *libsimgrid_data_addr_start; +extern size_t libsimgrid_data_size; + +#define MC_SET_RAW_MEM actual_heap = raw_heap +#define MC_UNSET_RAW_MEM actual_heap = std_heap + +/******************************* MEMORY MAPPINGS ***************************/ +/* These functions and data structures implements a binary interface for */ +/* the proc maps ascii interface */ + +#define MAP_READ 1 << 0 +#define MAP_WRITE 1 << 1 +#define MAP_EXEC 1 << 2 +#define MAP_SHARED 1 << 3 +#define MAP_PRIV 1 << 4 + +/* Each field is defined as documented in proc's manual page */ +typedef struct s_map_region { + + void *start_addr; /* Start address of the map */ + void *end_addr; /* End address of the map */ + int perms; /* Set of permissions */ + void *offset; /* Offset in the file/whatever */ + char dev_major; /* Major of the device */ + char dev_minor; /* Minor of the device */ + unsigned long inode; /* Inode in the device */ + char *pathname; /* Path name of the mapped file */ + +} s_map_region; + +typedef struct s_memory_map { + + s_map_region *regions; /* Pointer to an array of regions */ + int mapsize; /* Number of regions in the memory */ + +} s_memory_map_t, *memory_map_t; + +memory_map_t get_memory_map(void); + + +#endif diff --git a/src/xbt/log.c b/src/xbt/log.c index b75511005a..e4e7a7d037 100644 --- a/src/xbt/log.c +++ b/src/xbt/log.c @@ -517,6 +517,7 @@ XBT_LOG_NEW_CATEGORY(xbt, "All XBT categories (simgrid toolbox)"); XBT_LOG_NEW_CATEGORY(surf, "All SURF categories"); XBT_LOG_NEW_CATEGORY(msg, "All MSG categories"); XBT_LOG_NEW_CATEGORY(simix, "All SIMIX categories"); +XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); XBT_LOG_NEW_CATEGORY(bindings, "All bindings categories"); XBT_LOG_NEW_DEFAULT_SUBCATEGORY(log, xbt, -- 2.20.1