#ifdef HAVE_MC
#include "mc_process.h"
#include "mc_model_checker.h"
+#include "mc_protocol.h"
#endif
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
{
unsigned int index = 0;
smx_synchro_t act = 0;
+#ifdef HAVE_MC
+ s_smx_synchro_t temp_synchro;
+#endif
switch (req->call) {
case SIMCALL_NONE:
case SIMCALL_COMM_WAIT:
/* FIXME: check also that src and dst processes are not suspended */
act = simcall_comm_wait__get__comm(req);
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+
if (simcall_comm_wait__get__timeout(req) >= 0) {
/* 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. */
case SIMCALL_COMM_WAITANY:
/* Check if it has at least one communication ready */
- xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act)
+ xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+
if (act->comm.src_proc && act->comm.dst_proc)
return TRUE;
+ }
return FALSE;
+ case SIMCALL_MUTEX_LOCK: {
+ smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
+#ifdef HAVE_MC
+ s_smx_mutex_t temp_mutex;
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_mutex, mutex, sizeof(temp_mutex),
+ MC_PROCESS_INDEX_ANY);
+ mutex = &temp_mutex;
+ }
+#endif
+ if(mutex->owner == NULL)
+ return TRUE;
+ else
+ return (mutex->owner->pid == req->issuer->pid);
+ }
+
default:
/* The rest of the requests are always enabled */
return TRUE;
|| req->call == SIMCALL_COMM_TEST
|| req->call == SIMCALL_COMM_TESTANY
|| req->call == SIMCALL_MC_RANDOM
+ || req->call == SIMCALL_MUTEX_LOCK
#ifdef HAVE_MC
|| req->call == SIMCALL_MC_SNAPSHOT
|| req->call == SIMCALL_MC_COMPARE_SNAPSHOTS