> [ 0.000000] (2:client@HostB) Sent!
> [ 0.000000] (3:client@HostC) Sent!
> [ 0.000000] (2:client@HostB) Sent!
-> [ 0.000000] (1:server@HostA) **************************
-> [ 0.000000] (1:server@HostA) *** PROPERTY NOT VALID ***
-> [ 0.000000] (1:server@HostA) **************************
-> [ 0.000000] (1:server@HostA) Counter-example execution trace:
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(2)HostB (client)] iSend(src=(2)HostB (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(2)HostB (client)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) [(4)HostD (client)] iSend(src=(4)HostD (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(4)HostD (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) Expanded states = 22
-> [ 0.000000] (1:server@HostA) Visited states = 56
-> [ 0.000000] (1:server@HostA) Executed transitions = 52
+> [ 0.000000] (0:@) **************************
+> [ 0.000000] (0:@) *** PROPERTY NOT VALID ***
+> [ 0.000000] (0:@) **************************
+> [ 0.000000] (0:@) Counter-example execution trace:
+> [ 0.000000] (0:@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(2)HostB (client)] iSend(src=(2)HostB (client), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(1)HostA (server)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(2)HostB (client)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) [(4)HostD (client)] iSend(src=(4)HostD (client), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(1)HostA (server)] Wait(comm=(verbose only) [(4)HostD (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) Expanded states = 22
+> [ 0.000000] (0:@) Visited states = 56
+> [ 0.000000] (0:@) Executed transitions = 52
> [ 0.000000] (1:server@HostA) Received 2
> [ 0.000000] (3:client@HostC) Send 2!
> [ 0.000000] (1:server@HostA) Received 2
-> [ 0.000000] (1:server@HostA) **************************
-> [ 0.000000] (1:server@HostA) *** PROPERTY NOT VALID ***
-> [ 0.000000] (1:server@HostA) **************************
-> [ 0.000000] (1:server@HostA) Counter-example execution trace:
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (1:server@HostA) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
-> [ 0.000000] (1:server@HostA) Expanded states = 461
-> [ 0.000000] (1:server@HostA) Visited states = 2271
-> [ 0.000000] (1:server@HostA) Executed transitions = 2117
+> [ 0.000000] (0:@) **************************
+> [ 0.000000] (0:@) *** PROPERTY NOT VALID ***
+> [ 0.000000] (0:@) **************************
+> [ 0.000000] (0:@) Counter-example execution trace:
+> [ 0.000000] (0:@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [ 0.000000] (0:@) Expanded states = 461
+> [ 0.000000] (0:@) Visited states = 2271
+> [ 0.000000] (0:@) Executed transitions = 2117
#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;
mc_snapshot_t MC_take_snapshot(int num_state)
{
+ XBT_DEBUG("Taking snapshot %i", num_state);
+
mc_process_t mc_process = &mc_model_checker->process;
mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
snapshot->process = mc_process;
+ snapshot->num_state = num_state;
snapshot->address_space.address_space_class = &mc_snapshot_class;
snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
void MC_restore_snapshot(mc_snapshot_t snapshot)
{
+ XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
+
const bool use_soft_dirty = _sg_mc_sparse_checkpoint
&& _sg_mc_soft_dirty
&& MC_process_is_self(&mc_model_checker->process);
#include "mc_ignore.h"
#include "mc_model_checker.h"
#include "mc_private.h" // MC_deadlock_check()
+#include "mc_smx.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
void MC_client_hello(void)
{
- XBT_DEBUG("Greeting the MC server");
if (MC_protocol_hello(mc_client->fd) != 0)
xbt_die("Could not say hello the MC server");
- XBT_DEBUG("Greeted the MC server");
}
void MC_client_send_message(void* message, size_t size)
xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type);
}
+void MC_client_send_simple_message(int type)
+{
+ if (MC_protocol_send_simple_message(mc_client->fd, type))
+ xbt_die("Could not send message %i", type);
+}
+
void MC_client_handle_messages(void)
{
while (1) {
char message_buffer[MC_MESSAGE_LENGTH];
size_t s;
- if ((s = recv(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) == -1)
+ if ((s = MC_receive_message(mc_client->fd, &message_buffer, sizeof(message_buffer), 0)) == -1)
xbt_die("Could not receive commands from the model-checker");
- XBT_DEBUG("Receive message from model-checker");
s_mc_message_t message;
if (s < sizeof(message))
- xbt_die("Message is too short");
+ xbt_die("Received message is too small");
memcpy(&message, message_buffer, sizeof(message));
switch (message.type) {
answer.type = MC_MESSAGE_DEADLOCK_CHECK_REPLY;
answer.value = result;
if (MC_protocol_send(mc_client->fd, &answer, sizeof(answer)))
- xbt_die("Could nor send response");
+ xbt_die("Could not send response");
}
break;
case MC_MESSAGE_CONTINUE:
return;
+ case MC_MESSAGE_SIMCALL_HANDLE:
+ {
+ s_mc_simcall_handle_message_t message;
+ if (s != sizeof(message))
+ xbt_die("Unexpected size for SIMCALL_HANDLE");
+ memcpy(&message, message_buffer, sizeof(message));
+ smx_process_t process = SIMIX_process_from_PID(message.pid);
+ if (!process)
+ xbt_die("Invalid pid %lu", (unsigned long) message.pid);
+ SIMIX_simcall_handle(&process->simcall, message.value);
+ }
+ return;
+
default:
- xbt_die("Unexpected message from model-checker %i", message.type);
+ xbt_die("%s received unexpected message %s (%i)",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(message.type),
+ message.type
+ );
}
}
}
+
+void MC_client_main_loop(void)
+{
+ while (1) {
+ MC_protocol_send_simple_message(mc_client->fd, MC_MESSAGE_WAITING);
+ MC_client_handle_messages();
+ MC_wait_for_requests();
+ }
+}
void MC_client_hello(void);
void MC_client_handle_messages(void);
void MC_client_send_message(void* message, size_t size);
+void MC_client_send_simple_message(int type);
#ifdef HAVE_MC
void MC_ignore(void* addr, size_t size);
#endif
+void MC_client_main_loop(void);
+
SG_END_DECL()
#endif
void MC_assert(int prop)
{
if (MC_is_active() && !prop) {
- XBT_INFO("**************************");
- XBT_INFO("*** PROPERTY NOT VALID ***");
- XBT_INFO("**************************");
- XBT_INFO("Counter-example execution trace:");
- MC_record_dump_path(mc_stack);
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
- xbt_abort();
+ if (mc_mode == MC_MODE_STANDALONE) {
+ MC_report_assertion_error();
+ } else {
+ MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
+ MC_client_handle_messages();
+ }
}
}
&& (req = MC_state_get_request(state, &value))
&& (visited_state == NULL)) {
- req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Execute: %s", req_str);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
if (dot_output != NULL) {
MC_init_pid(getpid(), -1);
}
-void MC_init_pid(pid_t pid, int socket)
+static void MC_init_mode(void)
{
if (mc_mode == MC_MODE_NONE) {
if (getenv(MC_ENV_SOCKET_FD)) {
mc_mode = MC_MODE_STANDALONE;
}
}
+}
+void MC_init_pid(pid_t pid, int socket)
+{
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
}
mmalloc_set_current_heap(heap);
-
- if (mc_mode == MC_MODE_CLIENT) {
- // This will move somehwere else:
- MC_client_handle_messages();
- }
-
}
/******************************* Core of MC *******************************/
static void MC_modelcheck_comm_determinism_init(void)
{
MC_init();
+ if (mc_mode == MC_MODE_CLIENT) {
+ // This will move somehwere else:
+ MC_client_handle_messages();
+ }
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mmalloc_set_current_heap(heap);
}
-static void MC_modelcheck_safety_init(void)
-{
- _sg_mc_safety = 1;
-
- MC_init();
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_safety();
-
- MC_SET_MC_HEAP;
- /* Save the initial state */
- initial_global_state = xbt_new0(s_mc_global_t, 1);
- initial_global_state->snapshot = MC_take_snapshot(0);
- MC_SET_STD_HEAP;
-
- MC_modelcheck_safety();
-
- mmalloc_set_current_heap(heap);
-
- xbt_abort();
- //MC_exit();
-}
-
static void MC_modelcheck_liveness_init()
{
_sg_mc_liveness = 1;
MC_init();
+ if (mc_mode == MC_MODE_CLIENT) {
+ // This will move somehwere else:
+ MC_client_handle_messages();
+ }
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
void MC_do_the_modelcheck_for_real()
{
+ MC_init_mode();
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
XBT_INFO("Check communication determinism");
mc_reduce_kind = e_mc_reduce_none;
MC_modelcheck_comm_determinism_init();
- } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
+ }
+
+ else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
if(_sg_mc_termination){
XBT_INFO("Check non progressive cycles");
mc_reduce_kind = e_mc_reduce_none;
- }else{
- XBT_INFO("Check a safety property");
+ } else {
+ if (mc_reduce_kind == e_mc_reduce_unset)
+ mc_reduce_kind = e_mc_reduce_dpor;
+ else {
+ _sg_mc_safety = 1;
+ mc_reduce_kind = e_mc_reduce_dpor;
+ if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+ XBT_INFO("Check a safety property");
+ MC_modelcheck_safety();
+ }
+ else {
+ // Most of this is not needed:
+ MC_init();
+ // Main event loop:
+ MC_client_main_loop();
+ }
+ }
}
- MC_modelcheck_safety_init();
- } else {
+ }
+
+ else {
if (mc_reduce_kind == e_mc_reduce_unset)
mc_reduce_kind = e_mc_reduce_none;
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_MESSAGE_DEADLOCK_CHECK)))
xbt_die("Could not check deadlock state");
s_mc_int_message_t message;
- ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message));
+ ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0);
if (s == -1)
xbt_die("Could not receive message");
else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
- xbt_die("Unexpected message, expected MC_MESSAGE_DEADLOCK_CHECK_REPLY %i %i vs %i %i",
- (int) s, (int) message.type, (int) sizeof(message), (int) 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)
);
}
else
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
XBT_DEBUG("Replay: %s (%p)", req_str, state);
xbt_free(req_str);
}
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
xbt_free(req_str);
}
: (NULL)); item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(state, &value);
if (req) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(pair->graph_state, &value);
if (req && req->call != SIMCALL_NONE) {
- req_str = MC_request_to_string(req, value);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
XBT_INFO("%s", req_str);
xbt_free(req_str);
}
{
mc_time[process->pid] += amount;
}
+
+void MC_report_assertion_error(void)
+{
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ XBT_INFO("Counter-example execution trace:");
+ MC_record_dump_path(mc_stack);
+ MC_dump_stack_safety(mc_stack);
+ MC_print_statistics(mc_stats);
+}
message.region = *region;
if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
xbt_die("Could not send ignored region to MCer");
- XBT_DEBUG("Sent ignored region to the model-checker");
}
// MCed:
MC_SET_STD_HEAP;
}
- char* req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Execute: %s", req_str);
+ char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
/* Set request as executed */
MC_process_clear(&mc->process);
xbt_dict_free(&mc->hosts);
}
+
+unsigned long MC_smx_get_maxpid(void)
+{
+ if (mc_mode == MC_MODE_STANDALONE)
+ return simix_process_maxpid;
+
+ unsigned long maxpid;
+ MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
+ &maxpid, sizeof(maxpid));
+ return maxpid;
+}
mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
void MC_model_checker_delete(mc_model_checker_t mc);
-
-static inline
-int MC_smx_get_maxpid(void)
-{
- // Currently we use the same variable in STANDALONE and in SERVER mode:
- return simix_process_maxpid;
-}
+unsigned long MC_smx_get_maxpid(void);
SG_END_DECL()
*/
void MC_dump_stacks(FILE* file);
+void MC_report_assertion_error(void);
+
SG_END_DECL()
#endif
#include "mc_snapshot.h"
#include "mc_ignore.h"
#include "mc_smx.h"
+#include "mc_server.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
"MC process information");
void MC_process_refresh_malloc_info(mc_process_t process)
{
assert(!MC_process_is_self(process));
- if (!process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP)
+ if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP))
MC_process_refresh_heap(process);
// Refresh process->heapinfo:
size_t malloc_info_bytesize =
(process->heap->heaplimit + 1) * sizeof(malloc_info);
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- process->heap_info = (malloc_info*) realloc(process->heap_info,
- malloc_info_bytesize);
+ process->heap_info = realloc(process->heap_info, malloc_info_bytesize);
mmalloc_set_current_heap(heap);
MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
return;
}
- MC_process_smx_refresh(&mc_model_checker->process);
-
unsigned i;
mc_smx_process_info_t pi = NULL;
xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
- smx_process_t p = (smx_process_t) pi->address;
if (req == &pi->copy.simcall) {
- smx_simcall_t real_req = &p->simcall;
- // TODO, use a remote call
- SIMIX_simcall_handle(real_req, value);
+ MC_server_simcall_handle(&mc_model_checker->process, pi->copy.pid, value);
return;
}
}
- // Check (remove afterwards):
- xbt_dynar_foreach_ptr(mc_model_checker->process.smx_process_infos, i, pi) {
- smx_process_t p = (smx_process_t) pi->address;
- if (req == &p->simcall)
- xbt_die("The real simcall was passed. We expected the local copy.");
- }
-
xbt_die("Could not find the request");
}
int MC_protocol_send(int socket, void* message, size_t size)
{
+ XBT_DEBUG("Protocol [%s] send %s",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(*(e_mc_message_type*) message));
+
while (send(socket, message, size, 0) == -1) {
if (errno == EINTR)
continue;
message.type = MC_MESSAGE_NONE;
size_t s;
- while ((s = recv(socket, &message, sizeof(message), 0)) == -1) {
+ while ((s = MC_receive_message(socket, &message, sizeof(message), 0)) == -1) {
if (errno == EINTR)
continue;
else {
return 0;
}
-ssize_t MC_receive_message(int socket, void* message, size_t size)
+ssize_t MC_receive_message(int socket, void* message, size_t size, int options)
+{
+ int res = recv(socket, message, size, options);
+ if (res != -1) {
+ XBT_DEBUG("Protocol [%s] received %s",
+ MC_mode_name(mc_mode),
+ MC_message_type_name(*(e_mc_message_type*) message));
+ }
+ return res;
+}
+
+const char* MC_message_type_name(e_mc_message_type type)
{
- return recv(socket, message, size, 0);
+ switch(type) {
+ case MC_MESSAGE_NONE:
+ return "NONE";
+ case MC_MESSAGE_HELLO:
+ return "HELLO";
+ case MC_MESSAGE_CONTINUE:
+ return "CONTINUE";
+ case MC_MESSAGE_IGNORE_HEAP:
+ return "IGNORE_HEAP";
+ case MC_MESSAGE_UNIGNORE_HEAP:
+ return "UNIGNORE_HEAP";
+ case MC_MESSAGE_IGNORE_MEMORY:
+ return "IGNORE_MEMORY";
+ case MC_MESSAGE_STACK_REGION:
+ return "STACK_REGION";
+ case MC_MESSAGE_REGISTER_SYMBOL:
+ return "REGISTER_SYMBOL";
+ case MC_MESSAGE_DEADLOCK_CHECK:
+ return "DEADLOCK_CHECK";
+ case MC_MESSAGE_DEADLOCK_CHECK_REPLY:
+ return "DEADLOCK_CHECK_REPLY";
+ case MC_MESSAGE_WAITING:
+ return "WAITING";
+ case MC_MESSAGE_SIMCALL_HANDLE:
+ return "SIMCALL_HANDLE";
+ case MC_MESSAGE_ASSERTION_FAILED:
+ return "ASSERTION_FAILED";
+ default:
+ return "?";
+ }
+}
+
+const char* MC_mode_name(e_mc_mode_t mode)
+{
+ switch(mode) {
+ case MC_MODE_NONE:
+ return "NONE";
+ case MC_MODE_STANDALONE:
+ return "STANDALONE";
+ case MC_MODE_CLIENT:
+ return "CLIENT";
+ case MC_MODE_SERVER:
+ return "SERVER";
+ default:
+ return "?";
+ }
}
MC_MESSAGE_REGISTER_SYMBOL,
MC_MESSAGE_DEADLOCK_CHECK,
MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+ MC_MESSAGE_WAITING,
+ MC_MESSAGE_SIMCALL_HANDLE,
+ MC_MESSAGE_ASSERTION_FAILED,
} e_mc_message_type;
#define MC_MESSAGE_LENGTH 512
s_stack_region_t stack_region;
} s_mc_stack_region_message_t, *mc_stack_region_message_t;
+typedef struct s_mc_simcall_handle_message {
+ e_mc_message_type type;
+ unsigned long pid;
+ int value;
+} s_mc_simcall_handle_message_t, *mc_simcall_handle_message;
+
typedef struct s_mc_register_symbol_message {
e_mc_message_type type;
char name[128];
int MC_protocol_send(int socket, void* message, size_t size);
int MC_protocol_send_simple_message(int socket, int type);
int MC_protocol_hello(int socket);
-ssize_t MC_receive_message(int socket, void* message, size_t size);
+ssize_t MC_receive_message(int socket, void* message, size_t size, int options);
+
+const char* MC_message_type_name(e_mc_message_type type);
+const char* MC_mode_name(e_mc_mode_t mode);
SG_END_DECL()
static char *pointer_to_string(void *pointer);
static char *buff_size_to_string(size_t size);
+// Those are MC_state_get_internal_request(state)
int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
{
if (mc_reduce_kind == e_mc_reduce_none)
if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
return FALSE;
- // Read object from MCed memory:
- s_smx_synchro_t synchro1, synchro2;
+ // Those are internal requests, we do not need indirection
+ // because those objects are copies:
+ smx_synchro_t synchro1, synchro2;
if (r1->call == SIMCALL_COMM_WAIT) {
- MC_process_read_simple(&mc_model_checker->process, &synchro1,
- simcall_comm_wait__get__comm(r1), sizeof(synchro1));
+ synchro1 = simcall_comm_wait__get__comm(r1);
}
if (r2->call == SIMCALL_COMM_WAIT) {
- MC_process_read_simple(&mc_model_checker->process, &synchro2,
- simcall_comm_wait__get__comm(r2), sizeof(synchro2));
+ synchro2 = simcall_comm_wait__get__comm(r2);
}
if (r1->call == SIMCALL_COMM_TEST) {
- MC_process_read_simple(&mc_model_checker->process, &synchro1,
- simcall_comm_test__get__comm(r1), sizeof(synchro1));
+ synchro1 = simcall_comm_test__get__comm(r1);
}
if (r2->call == SIMCALL_COMM_TEST) {
- MC_process_read_simple(&mc_model_checker->process, &synchro2,
- simcall_comm_test__get__comm(r2), sizeof(synchro2));
+ synchro2 = simcall_comm_test__get__comm(r2);
}
if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
simcall_comm_irecv__get__rdv(r1);
- if (rdv != synchro2.comm.rdv_cpy
+ if (rdv != synchro2->comm.rdv_cpy
&& simcall_comm_wait__get__timeout(r2) <= 0)
return FALSE;
- if ((r1->issuer != synchro2.comm.src_proc)
- && (r1->issuer != synchro2.comm.dst_proc)
+ if ((r1->issuer != synchro2->comm.src_proc)
+ && (r1->issuer != synchro2->comm.dst_proc)
&& simcall_comm_wait__get__timeout(r2) <= 0)
return FALSE;
if ((r1->call == SIMCALL_COMM_ISEND)
- && (synchro2.comm.type == SIMIX_COMM_SEND)
- && (synchro2.comm.src_buff !=
+ && (synchro2->comm.type == SIMIX_COMM_SEND)
+ && (synchro2->comm.src_buff !=
simcall_comm_isend__get__src_buff(r1))
&& simcall_comm_wait__get__timeout(r2) <= 0)
return FALSE;
if ((r1->call == SIMCALL_COMM_IRECV)
- && (synchro2.comm.type == SIMIX_COMM_RECEIVE)
- && (synchro2.comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
+ && (synchro2->comm.type == SIMIX_COMM_RECEIVE)
+ && (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
&& simcall_comm_wait__get__timeout(r2) <= 0)
return FALSE;
}
SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) :
simcall_comm_irecv__get__rdv(r2);
- if (rdv != synchro1.comm.rdv_cpy
+ if (rdv != synchro1->comm.rdv_cpy
&& simcall_comm_wait__get__timeout(r1) <= 0)
return FALSE;
- if ((r2->issuer != synchro1.comm.src_proc)
- && (r2->issuer != synchro1.comm.dst_proc)
+ if ((r2->issuer != synchro1->comm.src_proc)
+ && (r2->issuer != synchro1->comm.dst_proc)
&& simcall_comm_wait__get__timeout(r1) <= 0)
return FALSE;
if ((r2->call == SIMCALL_COMM_ISEND)
- && (synchro1.comm.type == SIMIX_COMM_SEND)
- && (synchro1.comm.src_buff !=
+ && (synchro1->comm.type == SIMIX_COMM_SEND)
+ && (synchro1->comm.src_buff !=
simcall_comm_isend__get__src_buff(r2))
&& simcall_comm_wait__get__timeout(r1) <= 0)
return FALSE;
if ((r2->call == SIMCALL_COMM_IRECV)
- && (synchro1.comm.type == SIMIX_COMM_RECEIVE)
- && (synchro1.comm.dst_buff !=
+ && (synchro1->comm.type == SIMIX_COMM_RECEIVE)
+ && (synchro1->comm.dst_buff !=
simcall_comm_irecv__get__dst_buff(r2))
&& simcall_comm_wait__get__timeout(r1) <= 0)
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT
&& (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
- && (synchro1.comm.src_proc == NULL || synchro1.comm.dst_proc == NULL))
+ && (synchro1->comm.src_proc == NULL || synchro1->comm.dst_proc == NULL))
return FALSE;
if (r2->call == SIMCALL_COMM_WAIT
&& (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST)
- && (synchro2.comm.src_proc == NULL || synchro2.comm.dst_proc == NULL))
+ && (synchro2->comm.src_proc == NULL || synchro2->comm.dst_proc == NULL))
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
- && synchro1.comm.src_buff == synchro2.comm.src_buff
- && synchro2.comm.dst_buff == synchro2.comm.dst_buff)
+ && synchro1->comm.src_buff == synchro2->comm.src_buff
+ && synchro2->comm.dst_buff == synchro2->comm.dst_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
- && synchro1.comm.src_buff != NULL
- && synchro1.comm.dst_buff != NULL
- && synchro2.comm.src_buff != NULL
- && synchro2.comm.dst_buff != NULL
- && synchro1.comm.dst_buff != synchro2.comm.src_buff
- && synchro1.comm.dst_buff != synchro2.comm.dst_buff
- && synchro2.comm.dst_buff != synchro1.comm.src_buff)
+ && synchro1->comm.src_buff != NULL
+ && synchro1->comm.dst_buff != NULL
+ && synchro2->comm.src_buff != NULL
+ && synchro2->comm.dst_buff != NULL
+ && synchro1->comm.dst_buff != synchro2->comm.src_buff
+ && synchro1->comm.dst_buff != synchro2->comm.dst_buff
+ && synchro2->comm.dst_buff != synchro1->comm.src_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_TEST &&
(simcall_comm_test__get__comm(r1) == NULL
- || synchro1.comm.src_buff == NULL
- || synchro1.comm.dst_buff == NULL))
+ || synchro1->comm.src_buff == NULL
+ || synchro1->comm.dst_buff == NULL))
return FALSE;
if (r2->call == SIMCALL_COMM_TEST &&
(simcall_comm_test__get__comm(r2) == NULL
- || synchro2.comm.src_buff == NULL
- || synchro2.comm.dst_buff == NULL))
+ || synchro2->comm.src_buff == NULL
+ || synchro2->comm.dst_buff == NULL))
return FALSE;
if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && synchro1.comm.src_buff == synchro2.comm.src_buff
- && synchro1.comm.dst_buff == synchro2.comm.dst_buff)
+ && synchro1->comm.src_buff == synchro2->comm.src_buff
+ && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && synchro1.comm.src_buff == synchro2.comm.src_buff
- && synchro1.comm.dst_buff == synchro2.comm.dst_buff)
+ && synchro1->comm.src_buff == synchro2->comm.src_buff
+ && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && synchro1.comm.src_buff != NULL
- && synchro1.comm.dst_buff != NULL
- && synchro2.comm.src_buff != NULL
- && synchro2.comm.dst_buff != NULL
- && synchro1.comm.dst_buff != synchro2.comm.src_buff
- && synchro1.comm.dst_buff != synchro2.comm.dst_buff
- && synchro2.comm.dst_buff != synchro1.comm.src_buff)
+ && synchro1->comm.src_buff != NULL
+ && synchro1->comm.dst_buff != NULL
+ && synchro2->comm.src_buff != NULL
+ && synchro2->comm.dst_buff != NULL
+ && synchro1->comm.dst_buff != synchro2->comm.src_buff
+ && synchro1->comm.dst_buff != synchro2->comm.dst_buff
+ && synchro2->comm.dst_buff != synchro1->comm.src_buff)
return FALSE;
if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && synchro1.comm.src_buff != NULL
- && synchro1.comm.dst_buff != NULL
- && synchro2.comm.src_buff != NULL
- && synchro2.comm.dst_buff != NULL
- && synchro1.comm.dst_buff != synchro2.comm.src_buff
- && synchro1.comm.dst_buff != synchro2.comm.dst_buff
- && synchro2.comm.dst_buff != synchro1.comm.src_buff)
+ && synchro1->comm.src_buff != NULL
+ && synchro1->comm.dst_buff != NULL
+ && synchro2->comm.src_buff != NULL
+ && synchro2->comm.dst_buff != NULL
+ && synchro1->comm.dst_buff != synchro2->comm.src_buff
+ && synchro1->comm.dst_buff != synchro2->comm.dst_buff
+ && synchro2->comm.dst_buff != synchro1->comm.src_buff)
return FALSE;
return TRUE;
}
-char *MC_request_to_string(smx_simcall_t req, int value)
+char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t request_type)
{
+ bool use_remote_comm;
+ switch(request_type) {
+ case MC_REQUEST_SIMIX:
+ use_remote_comm = true;
+ break;
+ case MC_REQUEST_EXECUTED:
+ case MC_REQUEST_INTERNAL:
+ use_remote_comm = false;
+ break;
+ }
+
const char* type = NULL;
char *args = NULL;
p = pointer_to_string(remote_act);
s_smx_synchro_t synchro;
- MC_process_read_simple(&mc_model_checker->process, &synchro,
- remote_act, sizeof(synchro));
-
- smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
+ smx_synchro_t act;
+ if (use_remote_comm) {
+ MC_process_read_simple(&mc_model_checker->process, &synchro,
+ remote_act, sizeof(synchro));
+ act = &synchro;
+ } else
+ act = remote_act;
+
+ smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
src_proc ? src_proc->pid : 0,
src_proc ? MC_smx_process_get_host_name(src_proc) : "",
case SIMCALL_COMM_TEST: {
smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
s_smx_synchro_t synchro;
- MC_process_read_simple(&mc_model_checker->process, &synchro,
- remote_act, sizeof(synchro));
+ smx_synchro_t act;
+ if (use_remote_comm) {
+ MC_process_read_simple(&mc_model_checker->process, &synchro,
+ remote_act, sizeof(synchro));
+ act = &synchro;
+ } else
+ act = remote_act;
char* p;
- if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
+ if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
type = "Test FALSE";
p = pointer_to_string(remote_act);
args = bprintf("comm=%s", p);
type = "Test TRUE";
p = pointer_to_string(remote_act);
- smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
+ smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
src_proc->pid,
MC_smx_process_get_name(src_proc),
break;
case SIMCALL_COMM_WAITANY: {
- smx_synchro_t act;
MC_process_read_dynar_element(
- &mc_model_checker->process, &act, simcall_comm_waitany__get__comms(req),
- idx, sizeof(act));
+ &mc_model_checker->process, &remote_act, simcall_comm_waitany__get__comms(req),
+ idx, sizeof(remote_act));
}
break;
case SIMCALL_COMM_TESTANY: {
- s_smx_synchro_t act;
MC_process_read_dynar_element(
- &mc_model_checker->process, &act, simcall_comm_testany__get__comms(req),
- idx, sizeof(act));
+ &mc_model_checker->process, &remote_act, simcall_comm_testany__get__comms(req),
+ idx, sizeof(remote_act));
}
break;
SG_BEGIN_DECL()
+typedef enum e_mc_request_type {
+ MC_REQUEST_SIMIX,
+ MC_REQUEST_EXECUTED,
+ MC_REQUEST_INTERNAL,
+} e_mc_request_type_t;
+
int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
-char* MC_request_to_string(smx_simcall_t req, int value);
+char* MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t type);
unsigned int MC_request_testany_fail(smx_simcall_t req);
/*int MC_waitany_is_enabled_by_comm(smx_req_t req, unsigned int comm);*/
int MC_request_is_visible(smx_simcall_t req);
#include "mc_private.h"
#include "mc_record.h"
#include "mc_smx.h"
+#include "mc_client.h"
#include "xbt/mmalloc/mmprivate.h"
/**
* \brief Initialize the DPOR exploration algorithm
*/
-void MC_pre_modelcheck_safety()
+static void MC_pre_modelcheck_safety()
{
- mc_state_t initial_state = NULL;
- smx_process_t process;
-
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
if (_sg_mc_visited > 0)
visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
- initial_state = MC_state_new();
+ mc_state_t initial_state = MC_state_new();
MC_SET_STD_HEAP;
XBT_DEBUG("**************************************************");
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
+ smx_process_t process;
MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(initial_state, process);
/** \brief Model-check the application using a DFS exploration
* with DPOR (Dynamic Partial Order Reductions)
*/
-void MC_modelcheck_safety(void)
+static void MC_modelcheck_safety_main(void)
{
-
char *req_str = NULL;
int value;
- smx_simcall_t req = NULL, prev_req = NULL;
+ smx_simcall_t req = NULL;
mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
- smx_process_t process = NULL;
xbt_fifo_item_t item = NULL;
mc_visited_state_t visited_state = NULL;
if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
&& (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
- char* req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Execute: %s", req_str);
+ req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
if (dot_output != NULL) {
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
+ // TODO, bundle both operations in a single message
+ // MC_execute_transition(req, value)
+
/* Answer the request */
MC_simcall_handle(req, value);
-
- /* Wait for requests (schedules processes) */
MC_wait_for_requests();
/* Create the new expanded state */
if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get an enabled process and insert it in the interleave set of the next state */
+ smx_process_t process = NULL;
MC_EACH_SIMIX_PROCESS(process,
if (MC_process_is_enabled(process)) {
MC_state_interleave_process(next_state, process);
/* Trash the current state, no longer needed */
xbt_fifo_shift(mc_stack);
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
MC_SET_STD_HEAP;
if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
- prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = MC_request_to_string(prev_req, value);
+ smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
+ req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
xbt_free(req_str);
prev_req = MC_state_get_executed_request(state, &value);
- req_str = MC_request_to_string(prev_req, value);
+ req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
XBT_DEBUG("%s (state=%d)", req_str, state->num);
xbt_free(req_str);
}
return;
}
+
+void MC_modelcheck_safety(void)
+{
+ XBT_DEBUG("Starting the safety algorithm");
+ xbt_assert(mc_mode == MC_MODE_SERVER);
+
+ _sg_mc_safety = 1;
+
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+ /* Create exploration stack */
+ mc_stack = xbt_fifo_new();
+
+ MC_SET_STD_HEAP;
+
+ MC_pre_modelcheck_safety();
+
+ MC_SET_MC_HEAP;
+ /* Save the initial state */
+ initial_global_state = xbt_new0(s_mc_global_t, 1);
+ initial_global_state->snapshot = MC_take_snapshot(0);
+ MC_SET_STD_HEAP;
+
+ MC_modelcheck_safety_main();
+
+ mmalloc_set_current_heap(heap);
+
+ xbt_abort();
+ //MC_exit();
+}
extern e_mc_reduce_t mc_reduce_kind;
-void MC_pre_modelcheck_safety(void);
void MC_modelcheck_safety(void);
typedef struct s_mc_visited_state{
/* Wait for the target process to initialize and exchange a HELLO messages
* before trying to look at its memory map.
*/
- XBT_DEBUG("Greeting the MC client");
int res = MC_protocol_hello(socket);
if (res != 0)
throw std::system_error(res, std::system_category());
- XBT_DEBUG("Greeted the MC client");
// Block SIGCHLD (this will be handled with accept/signalfd):
sigset_t set;
int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE);
if (res)
throw std::system_error(res, std::system_category());
+ process->cache_flags = (e_mc_process_cache_flags_t) 0;
}
static
throw std::system_error(error, std::system_category());
}
-void s_mc_server::handle_events()
+bool s_mc_server::handle_events()
{
char buffer[MC_MESSAGE_LENGTH];
struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
if (socket_pollfd->revents) {
if (socket_pollfd->revents & POLLIN) {
- ssize_t size = recv(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
+ ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
if (size == -1 && errno != EAGAIN)
throw std::system_error(errno, std::system_category());
case MC_MESSAGE_IGNORE_HEAP:
{
- XBT_DEBUG("Received ignored region");
s_mc_ignore_heap_message_t message;
if (size != sizeof(message))
xbt_die("Broken messsage");
break;
}
-
case MC_MESSAGE_UNIGNORE_HEAP:
{
- XBT_DEBUG("Received unignored region");
s_mc_ignore_memory_message_t message;
if (size != sizeof(message))
xbt_die("Broken messsage");
case MC_MESSAGE_IGNORE_MEMORY:
{
- XBT_DEBUG("Received ignored memory");
s_mc_ignore_memory_message_t message;
if (size != sizeof(message))
xbt_die("Broken messsage");
case MC_MESSAGE_STACK_REGION:
{
- XBT_DEBUG("Received stack area");
s_mc_stack_region_message_t message;
if (size != sizeof(message))
xbt_die("Broken messsage");
break;
}
+ case MC_MESSAGE_WAITING:
+ return false;
+
+ case MC_MESSAGE_ASSERTION_FAILED:
+ MC_report_assertion_error();
+ xbt_abort();
+ break;
+
default:
xbt_die("Unexpected message from model-checked application");
}
- return;
+ return true;
}
if (socket_pollfd->revents & POLLERR) {
throw_socket_error(socket_pollfd->fd);
if (signalfd_pollfd->revents) {
if (signalfd_pollfd->revents & POLLIN) {
this->handle_signals();
- return;
+ return true;
}
if (signalfd_pollfd->revents & POLLERR) {
throw_socket_error(signalfd_pollfd->fd);
if (signalfd_pollfd->revents & POLLHUP)
xbt_die("Signalfd hang up?");
}
+
+ return true;
}
void s_mc_server::loop()
break;
}
}
+
+void MC_server_wait_client(mc_process_t process)
+{
+ mc_server->resume(process);
+ while (mc_model_checker->process.running) {
+ if (!mc_server->handle_events())
+ return;
+ }
+}
+
+void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value)
+{
+ s_mc_simcall_handle_message m;
+ memset(&m, 0, sizeof(m));
+ m.type = MC_MESSAGE_SIMCALL_HANDLE;
+ m.pid = pid;
+ m.value = value;
+ MC_protocol_send(mc_model_checker->process.socket, &m, sizeof(m));
+ process->cache_flags = (e_mc_process_cache_flags_t) 0;
+ while (mc_model_checker->process.running) {
+ if (!mc_server->handle_events())
+ return;
+ }
+}
#ifndef MC_SERVER_H
#define MC_SERVER_H
+#include <stdint.h>
+#include <stdbool.h>
+
+#include <sys/signalfd.h>
+#include <sys/types.h>
+
#include <xbt/misc.h>
+
+#include "mc_process.h"
SG_BEGIN_DECL()
extern mc_server_t mc_server;
+void MC_server_wait_client(mc_process_t process);
+void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value);
+
SG_END_DECL()
#ifdef __cplusplus
void exit();
void resume(mc_process_t process);
void loop();
- void handle_events();
+ bool handle_events();
protected:
void handle_signals();
void handle_waitpid();
struct s_mc_snapshot {
mc_process_t process;
+ int num_state;
s_mc_address_space_t address_space;
size_t heap_bytes_used;
mc_mem_region_t* snapshot_regions;
#include "mc_comm_pattern.h"
#include "mc_smx.h"
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
+ "Logging specific to MC (state)");
+
/**
* \brief Creates a state data structure used by the exploration algorithm
*/
mc_state_t MC_state_new()
{
mc_state_t state = xbt_new0(s_mc_state_t, 1);
+
state->max_pid = MC_smx_get_maxpid();
state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
state->system_state = NULL;
{
state->executed_req = *req;
state->req_num = value;
+
smx_process_t process = NULL;
- mc_procstate_t procstate = NULL;
/* The waitany and testany request are transformed into a wait or test request over the
* corresponding communication action so it can be treated later by the dependence
int random_max = simcall_mc_random__get__max(req);
if (value != random_max) {
MC_EACH_SIMIX_PROCESS(process,
- procstate = &state->proc_status[process->pid];
+ mc_procstate_t procstate = &state->proc_status[process->pid];
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
if (process->pid == issuer->pid) {
procstate->state = MC_MORE_INTERLEAVE;
return &state->internal_req;
}
-smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
+static inline smx_simcall_t MC_state_get_request_for_process(
+ mc_state_t state, int*value, smx_process_t process)
{
- smx_process_t process = NULL;
- mc_procstate_t procstate = NULL;
- unsigned int start_count;
- smx_synchro_t act = NULL;
-
- MC_EACH_SIMIX_PROCESS(process,
- procstate = &state->proc_status[process->pid];
-
- if (procstate->state != MC_INTERLEAVE
- && procstate->state != MC_MORE_INTERLEAVE)
- continue;
- if (!MC_process_is_enabled(process))
- continue;
-
- switch (process->simcall.call) {
- case SIMCALL_COMM_WAITANY:
- *value = -1;
- while (procstate->interleave_count <
- MC_process_read_dynar_length(&mc_model_checker->process,
- simcall_comm_waitany__get__comms(&process->simcall))) {
- if (MC_request_is_enabled_by_idx
- (&process->simcall, procstate->interleave_count++)) {
- *value = procstate->interleave_count - 1;
- break;
- }
- }
+ mc_procstate_t procstate = &state->proc_status[process->pid];
- if (procstate->interleave_count >=
- MC_process_read_dynar_length(&mc_model_checker->process,
- simcall_comm_waitany__get__comms(&process->simcall)))
- procstate->state = MC_DONE;
-
- if (*value != -1)
- return &process->simcall;
+ if (procstate->state != MC_INTERLEAVE
+ && procstate->state != MC_MORE_INTERLEAVE)
+ return NULL;
+ if (!MC_process_is_enabled(process))
+ return NULL;
- break;
+ switch (process->simcall.call) {
- case SIMCALL_COMM_TESTANY:
- start_count = procstate->interleave_count;
- *value = -1;
- while (procstate->interleave_count <
- MC_process_read_dynar_length(&mc_model_checker->process,
- simcall_comm_testany__get__comms(&process->simcall))) {
- if (MC_request_is_enabled_by_idx
- (&process->simcall, procstate->interleave_count++)) {
- *value = procstate->interleave_count - 1;
- break;
- }
- }
-
- if (procstate->interleave_count >=
+ case SIMCALL_COMM_WAITANY:
+ *value = -1;
+ while (procstate->interleave_count <
MC_process_read_dynar_length(&mc_model_checker->process,
- simcall_comm_testany__get__comms(&process->simcall)))
- procstate->state = MC_DONE;
-
- if (*value != -1 || start_count == 0)
- return &process->simcall;
-
- break;
-
- case SIMCALL_COMM_WAIT:
- act = simcall_comm_wait__get__comm(&process->simcall);
-
- if (act->comm.src_proc && act->comm.dst_proc) {
- *value = 0;
- } else {
- if (act->comm.src_proc == NULL && act->comm.type == SIMIX_COMM_READY
- && act->comm.detached == 1)
- *value = 0;
- else
- *value = -1;
+ simcall_comm_waitany__get__comms(&process->simcall))) {
+ if (MC_request_is_enabled_by_idx
+ (&process->simcall, procstate->interleave_count++)) {
+ *value = procstate->interleave_count - 1;
+ break;
}
+ }
+
+ if (procstate->interleave_count >=
+ MC_process_read_dynar_length(&mc_model_checker->process,
+ simcall_comm_waitany__get__comms(&process->simcall)))
procstate->state = MC_DONE;
+
+ if (*value != -1)
return &process->simcall;
- break;
+ break;
- case SIMCALL_MC_RANDOM:
- if (procstate->state == MC_INTERLEAVE)
- *value = simcall_mc_random__get__min(&process->simcall);
- else {
- if (state->req_num < simcall_mc_random__get__max(&process->simcall))
- *value = state->req_num + 1;
+ case SIMCALL_COMM_TESTANY: {
+ unsigned start_count = procstate->interleave_count;
+ *value = -1;
+ while (procstate->interleave_count <
+ MC_process_read_dynar_length(&mc_model_checker->process,
+ simcall_comm_testany__get__comms(&process->simcall))) {
+ if (MC_request_is_enabled_by_idx
+ (&process->simcall, procstate->interleave_count++)) {
+ *value = procstate->interleave_count - 1;
+ break;
}
+ }
+
+ if (procstate->interleave_count >=
+ MC_process_read_dynar_length(&mc_model_checker->process,
+ simcall_comm_testany__get__comms(&process->simcall)))
procstate->state = MC_DONE;
+
+ if (*value != -1 || start_count == 0)
return &process->simcall;
- break;
- default:
- procstate->state = MC_DONE;
+ break;
+ }
+
+ case SIMCALL_COMM_WAIT: {
+ smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
+ s_smx_synchro_t act;
+ MC_process_read_simple(&mc_model_checker->process,
+ &act, remote_act, sizeof(act));
+ if (act.comm.src_proc && act.comm.dst_proc) {
*value = 0;
- return &process->simcall;
- break;
+ } else {
+ if (act.comm.src_proc == NULL && act.comm.type == SIMIX_COMM_READY
+ && act.comm.detached == 1)
+ *value = 0;
+ else
+ *value = -1;
+ }
+ procstate->state = MC_DONE;
+ return &process->simcall;
+ }
+
+ case SIMCALL_MC_RANDOM:
+ if (procstate->state == MC_INTERLEAVE)
+ *value = simcall_mc_random__get__min(&process->simcall);
+ else {
+ if (state->req_num < simcall_mc_random__get__max(&process->simcall))
+ *value = state->req_num + 1;
+ }
+ procstate->state = MC_DONE;
+ return &process->simcall;
- }
+ default:
+ procstate->state = MC_DONE;
+ *value = 0;
+ return &process->simcall;
+ }
+ return NULL;
+}
+
+smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
+{
+ smx_process_t process = NULL;
+ MC_EACH_SIMIX_PROCESS(process,
+ smx_simcall_t res = MC_state_get_request_for_process(state, value, process);
+ if (res)
+ return res;
);
return NULL;
#include "mc_protocol.h"
#include "mc_server.h"
#include "mc_model_checker.h"
+#include "mc_safety.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
mc_server = new s_mc_server(child, socket);
mc_server->start();
MC_init_pid(child, socket);
- mc_server->resume(&mc_model_checker->process);
- mc_server->loop();
+
+ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
+ mc_server->loop();
+ }
+
+ else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
+ if (mc_reduce_kind == e_mc_reduce_unset)
+ mc_reduce_kind = e_mc_reduce_dpor;
+ XBT_INFO("Check a safety property");
+ MC_wait_for_requests();
+ MC_modelcheck_safety();
+ }
+
+ else {
+ mc_server->loop();
+ }
+
mc_server->shutdown();
mc_server->exit();
}
if (argc < 2)
xbt_die("Missing arguments.\n");
- bool server_mode = false;
+ bool server_mode = true;
char* env = std::getenv("SIMGRID_MC_MODE");
if (env) {
if (std::strcmp(env, "server") == 0)
else if (std::strcmp(env, "standalone") == 0)
server_mode = false;
else
- XBT_WARN("Unrecognised value for SIMGRID_MC_MODE (server/standalone)");
+ xbt_die("Unrecognised value for SIMGRID_MC_MODE (server/standalone)");
}
if (!server_mode) {
mc_mode = MC_MODE_CLIENT;
MC_client_init();
MC_client_hello();
+ MC_client_handle_messages();
} else {
mc_mode = MC_MODE_STANDALONE;
}
#include <stdio.h>
+#include <xbt/log.h>
+
#include <msg/msg.h>
#include <simgrid/modelchecker.h>
+XBT_LOG_NEW_DEFAULT_CATEGORY(random_bug, "Application");
+
/** An (fake) application with a bug occuring for some random values
*/
static int app(int argc, char *argv[])
MSG_function_register("app", &app);
MSG_create_environment(argv[1]);
MSG_launch_application(argv[2]);
- return (int) MSG_main();
+ return MSG_main();
}
!expect signal SIGABRT
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1
> [ 0.000000] (0:@) Check a safety property
-> [ 0.000000] (1:app@Tremblay) **************************
-> [ 0.000000] (1:app@Tremblay) *** PROPERTY NOT VALID ***
-> [ 0.000000] (1:app@Tremblay) **************************
-> [ 0.000000] (1:app@Tremblay) Counter-example execution trace:
-> [ 0.000000] (1:app@Tremblay) Path = 1/3;1/4
-> [ 0.000000] (1:app@Tremblay) [(1)Tremblay (app)] MC_RANDOM(3)
-> [ 0.000000] (1:app@Tremblay) [(1)Tremblay (app)] MC_RANDOM(4)
-> [ 0.000000] (1:app@Tremblay) Expanded states = 27
-> [ 0.000000] (1:app@Tremblay) Visited states = 68
-> [ 0.000000] (1:app@Tremblay) Executed transitions = 46
+> [ 0.000000] (0:@) **************************
+> [ 0.000000] (0:@) *** PROPERTY NOT VALID ***
+> [ 0.000000] (0:@) **************************
+> [ 0.000000] (0:@) Counter-example execution trace:
+> [ 0.000000] (0:@) Path = 1/3;1/4
+> [ 0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(3)
+> [ 0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(4)
+> [ 0.000000] (0:@) Expanded states = 27
+> [ 0.000000] (0:@) Visited states = 68
+> [ 0.000000] (0:@) Executed transitions = 46
