/* 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 <assert.h>
+
#include <simgrid/simix.h>
#include "mc_base.h"
#include "mc_process.h"
#include "mc_model_checker.h"
#include "mc_protocol.h"
+#include "mc_smx.h"
+#include "mc_server.h"
#endif
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
void MC_wait_for_requests(void)
{
+ if (mc_mode == MC_MODE_SERVER) {
+ MC_server_wait_client(&mc_model_checker->process);
+ return;
+ }
+
smx_process_t process;
smx_simcall_t req;
unsigned int iter;
#ifdef HAVE_MC
s_smx_synchro_t temp_synchro;
#endif
- smx_mutex_t mutex = NULL;
switch (req->call) {
case SIMCALL_NONE:
}
return (act->comm.src_proc && act->comm.dst_proc);
- case SIMCALL_COMM_WAITANY:
- /* Check if it has at least one communication ready */
+ case SIMCALL_COMM_WAITANY: {
+#ifdef HAVE_MC
+ // Read dynar:
+ s_xbt_dynar_t comms;
+ MC_process_read_simple(&mc_model_checker->process,
+ &comms, simcall_comm_waitany__get__comms(req), sizeof(comms));
+ // Read dynar buffer:
+ assert(comms.elmsize == sizeof(act));
+ size_t buffer_size = comms.elmsize * comms.used;
+ char buffer[buffer_size];
+ MC_process_read_simple(&mc_model_checker->process,
+ buffer, comms.data, sizeof(buffer));
+#endif
+
+#ifdef HAVE_MC
+ for (index = 0; index < comms.used; ++index) {
+ memcpy(&act, buffer + comms.elmsize * index, sizeof(act));
+#else
xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+#endif
#ifdef HAVE_MC
// Fetch from MCed memory:
return TRUE;
}
return FALSE;
+ }
- case SIMCALL_MUTEX_LOCK:
- mutex = simcall_mutex_lock__get__mutex(req);
+ 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);
+#ifdef HAVE_MC
+ // TODO, *(mutex->owner) :/
+ return MC_smx_resolve_process(mutex->owner)->pid ==
+ MC_smx_resolve_process(req->issuer)->pid;
+#else
+ return mutex->owner->pid == req->issuer->pid;
+#endif
+ }
default:
/* The rest of the requests are always enabled */