#include "src/mc/mc_protocol.h"
#include "src/mc/Client.hpp"
+#include "src/mc/mc_request.h"
// We won't need those once the separation MCer/MCed is complete:
#include "src/mc/mc_ignore.h"
-#include "src/mc/mc_private.h" // MC_deadlock_check()
#include "src/mc/mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
case MC_MESSAGE_DEADLOCK_CHECK:
{
- int result = MC_deadlock_check();
+ // Check deadlock:
+ bool deadlock = false;
+ smx_process_t process;
+ if (xbt_swag_size(simix_global->process_list)) {
+ deadlock = true;
+ xbt_swag_foreach(process, simix_global->process_list)
+ if (simgrid::mc::process_is_enabled(process)) {
+ deadlock = false;
+ break;
+ }
+ }
+
+ // Send result:
s_mc_int_message_t answer;
answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
- answer.value = result;
+ answer.value = deadlock;
if (channel_.send(answer))
xbt_die("Could not send response");
}
return;
}
+bool ModelChecker::checkDeadlock()
+{
+ int res;
+ if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
+ xbt_die("Could not check deadlock state");
+ s_mc_int_message_t message;
+ ssize_t s = mc_model_checker->process().getChannel().receive(message);
+ if (s == -1)
+ xbt_die("Could not receive message");
+ if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
+ xbt_die("%s received unexpected message %s (%i, size=%i) "
+ "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(message.type), (int) message.type, (int) s,
+ (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
+ );
+ return message.value != 0;
+}
+
}
}
mc_model_checker->wait_client(mc_model_checker->process());
}
void exit(int status);
+
+ bool checkDeadlock();
+
private:
void setup_ignore();
bool handle_message(char* buffer, ssize_t size);
visited_state = nullptr;
/* Check for deadlocks */
- if (MC_deadlock_check()) {
+ if (mc_model_checker->checkDeadlock()) {
MC_show_deadlock(nullptr);
return SIMGRID_MC_EXIT_DEADLOCK;
}
//xbt_abort();
}
-#if HAVE_MC
-int MC_deadlock_check()
-{
- if (mc_mode == MC_MODE_SERVER) {
- int res;
- if ((res = mc_model_checker->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
- xbt_die("Could not check deadlock state");
- s_mc_int_message_t message;
- ssize_t s = mc_model_checker->process().getChannel().receive(message);
- if (s == -1)
- xbt_die("Could not receive message");
- if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
- xbt_die("%s received unexpected message %s (%i, size=%i) "
- "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
- MC_mode_name(mc_mode),
- MC_message_type_name(message.type), (int) message.type, (int) s,
- (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
- );
- return message.value;
- }
-
- bool deadlock = false;
- smx_process_t process;
- if (xbt_swag_size(simix_global->process_list)) {
- deadlock = true;
- xbt_swag_foreach(process, simix_global->process_list)
- if (simgrid::mc::process_is_enabled(process)) {
- deadlock = false;
- break;
- }
- }
- return deadlock;
-}
-#endif
-
/**
* \brief Re-executes from the state at position start all the transitions indicated by
* a given model-checker stack.
XBT_PRIVATE extern int user_max_depth_reached;
-XBT_PRIVATE int MC_deadlock_check(void);
XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
XBT_PRIVATE void MC_replay_liveness(xbt_fifo_t stack);
XBT_PRIVATE void MC_show_deadlock(smx_simcall_t req);
visited_state = nullptr;
/* Check for deadlocks */
- if (MC_deadlock_check()) {
+ if (mc_model_checker->checkDeadlock()) {
MC_show_deadlock(nullptr);
return SIMGRID_MC_EXIT_DEADLOCK;
}