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
/************************** 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 */
/******************************************************************************/
void snapshot_stack_free_voidp(void *s){
snapshot_stack_free((mc_snapshot_stack_t) * (void **) s);
}
+
+void *MC_snapshot(void){
+
+ return simcall_mc_snapshot();
+
+}
return nb_diff;
}
+int MC_compare_snapshots(void *s1, void *s2){
+
+ return simcall_mc_compare_snapshots(s1, s2);
+
+}
}
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;
}
|| 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)
#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)");
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),
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 */ \
/* ****************************************************************************************** */ \
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 */
/* ****************************************************************************************** */
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 */