From 114948db2d558f1be1481dea89be75166201461f Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 19 Oct 2012 10:20:21 +0200 Subject: [PATCH 1/1] model-checker : New public functions to take a snapshot and compare two snapshots from user application using new simcalls (simcall_mc_snapshot and simcall_mc_compare_snapshots) --- include/simgrid/modelchecker.h | 2 ++ include/simgrid/simix.h | 4 ++++ src/mc/mc_checkpoint.c | 6 ++++++ src/mc/mc_compare.c | 5 +++++ src/mc/mc_request.c | 14 +++++++++++++- src/simix/smx_smurf.c | 12 ++++++++++++ src/simix/smx_smurf_private.h | 12 ++++++++++++ src/simix/smx_user.c | 26 ++++++++++++++++++++++++++ 8 files changed, 80 insertions(+), 1 deletion(-) diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 52b2ed7f2d..d5f8bca700 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -21,6 +21,8 @@ extern int _surf_do_model_check; /* please don't use directly: we inline MC_is_a XBT_PUBLIC(void) MC_assert(int); XBT_PUBLIC(int) MC_random(int min, int max); XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct); +XBT_PUBLIC(void *) MC_snapshot(void); +XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2); #else diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h index bc7dc42466..121b2ccc13 100644 --- a/include/simgrid/simix.h +++ b/include/simgrid/simix.h @@ -467,6 +467,10 @@ XBT_PUBLIC(xbt_dict_t) SIMIX_asr_get_properties(const char *name); /************************** AS router simcalls ***************************/ XBT_PUBLIC(xbt_dict_t) simcall_asr_get_properties(const char *name); +/************************** MC simcalls **********************************/ +XBT_PUBLIC(void *) simcall_mc_snapshot(void); +XBT_PUBLIC(int) simcall_mc_compare_snapshots(void *s1, void *s2); + /************************** New API simcalls **********************************/ /* TUTORIAL: New API */ /******************************************************************************/ diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 0703b1744c..6f53924dee 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -614,3 +614,9 @@ static void snapshot_stack_free(mc_snapshot_stack_t s){ void snapshot_stack_free_voidp(void *s){ snapshot_stack_free((mc_snapshot_stack_t) * (void **) s); } + +void *MC_snapshot(void){ + + return simcall_mc_snapshot(); + +} diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 083301b17f..0b20726e00 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -407,3 +407,8 @@ static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void * return nb_diff; } +int MC_compare_snapshots(void *s1, void *s2){ + + return simcall_mc_compare_snapshots(s1, s2); + +} diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index ec73bfd36f..50c7cd226a 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -239,6 +239,16 @@ char *MC_request_to_string(smx_simcall_t req, int value) } break; + case SIMCALL_MC_SNAPSHOT: + type = xbt_strdup("MC_SNAPSHOT"); + args = '\0'; + break; + + case SIMCALL_MC_COMPARE_SNAPSHOTS: + type = xbt_strdup("MC_COMPARE_SNAPSHOTS"); + args = '\0'; + break; + default: THROW_UNIMPLEMENTED; } @@ -271,7 +281,9 @@ int MC_request_is_visible(smx_simcall_t req) || req->call == SIMCALL_COMM_WAIT || req->call == SIMCALL_COMM_WAITANY || req->call == SIMCALL_COMM_TEST - || req->call == SIMCALL_COMM_TESTANY; + || req->call == SIMCALL_COMM_TESTANY + || req->call == SIMCALL_MC_SNAPSHOT + || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS; } int MC_request_is_enabled(smx_simcall_t req) diff --git a/src/simix/smx_smurf.c b/src/simix/smx_smurf.c index 973dd82155..f3ebc520f7 100644 --- a/src/simix/smx_smurf.c +++ b/src/simix/smx_smurf.c @@ -1,6 +1,7 @@ #include "smx_private.h" #include "xbt/fifo.h" #include "xbt/xbt_os_thread.h" +#include "../mc/mc_private.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_smurf, simix, "Logging specific to SIMIX (SMURF)"); @@ -557,6 +558,17 @@ void SIMIX_simcall_pre(smx_simcall_t simcall, int value) SIMIX_simcall_answer(simcall); break; + case SIMCALL_MC_SNAPSHOT: + simcall->mc_snapshot.s = MC_take_snapshot_liveness(); + SIMIX_simcall_answer(simcall); + break; + + case SIMCALL_MC_COMPARE_SNAPSHOTS: + simcall->mc_compare_snapshots.result = + snapshot_compare(simcall->mc_compare_snapshots.snapshot1, simcall->mc_compare_snapshots.snapshot2); + SIMIX_simcall_answer(simcall); + break; + case SIMCALL_NONE: THROWF(arg_error,0,"Asked to do the noop syscall on %s@%s", SIMIX_process_get_name(simcall->issuer), diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h index adff451ced..2009207771 100644 --- a/src/simix/smx_smurf_private.h +++ b/src/simix/smx_smurf_private.h @@ -98,6 +98,8 @@ SIMCALL_ENUM_ELEMENT(SIMCALL_FILE_STAT), \ SIMCALL_ENUM_ELEMENT(SIMCALL_FILE_UNLINK),\ SIMCALL_ENUM_ELEMENT(SIMCALL_FILE_LS),\ SIMCALL_ENUM_ELEMENT(SIMCALL_ASR_GET_PROPERTIES), \ +SIMCALL_ENUM_ELEMENT(SIMCALL_MC_SNAPSHOT), \ +SIMCALL_ENUM_ELEMENT(SIMCALL_MC_COMPARE_SNAPSHOTS), \ /* ****************************************************************************************** */ \ /* TUTORIAL: New API */ \ /* ****************************************************************************************** */ \ @@ -607,6 +609,16 @@ typedef struct s_smx_simcall { xbt_dict_t result; } asr_get_properties; + struct{ + void *s; + } mc_snapshot; + + struct{ + void *snapshot1; + void *snapshot2; + int result; + } mc_compare_snapshots; + /* ****************************************************************************************** */ /* TUTORIAL: New API */ /* ****************************************************************************************** */ diff --git a/src/simix/smx_user.c b/src/simix/smx_user.c index a6415b50ab..84ce825d17 100644 --- a/src/simix/smx_user.c +++ b/src/simix/smx_user.c @@ -1651,6 +1651,32 @@ xbt_dict_t simcall_file_ls(const char* mount, const char* path) return simcall->file_ls.result; } +void *simcall_mc_snapshot(void) +{ + smx_simcall_t simcall = SIMIX_simcall_mine(); + simcall->call = SIMCALL_MC_SNAPSHOT; + + SIMIX_simcall_push(simcall->issuer); + + return simcall->mc_snapshot.s; +} + +int simcall_mc_compare_snapshots(void *s1, void *s2){ + + smx_simcall_t simcall = SIMIX_simcall_mine(); + simcall->call = SIMCALL_MC_COMPARE_SNAPSHOTS; + simcall->mc_compare_snapshots.snapshot1 = s1; + simcall->mc_compare_snapshots.snapshot2 = s2; + + if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */ + simcall->mc_compare_snapshots.result = -1; + + SIMIX_simcall_push(simcall->issuer); + + return simcall->mc_compare_snapshots.result; +} + + /* ****************************************************************************************** */ /* TUTORIAL: New API */ /* All functions for simcall */ -- 2.20.1