From: Gabriel Corona Date: Mon, 23 Feb 2015 12:40:14 +0000 (+0100) Subject: [mc] Cross-process MC/safety implementation X-Git-Tag: v3_12~732^2~78 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e7c2b72c7328c4aade5049a3cc21603a9d27842c [mc] Cross-process MC/safety implementation --- diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh index 03f5d54f9b..b8a1ca278e 100644 --- a/examples/msg/mc/bugged1.tesh +++ b/examples/msg/mc/bugged1.tesh @@ -17,20 +17,20 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 > [ 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 diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh index 49619cea8f..cadf32f2ab 100644 --- a/examples/msg/mc/bugged2.tesh +++ b/examples/msg/mc/bugged2.tesh @@ -882,17 +882,17 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 > [ 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 diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c index 164047cfcb..e55a80cabf 100644 --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@ -17,12 +17,18 @@ #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; diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 6c787e15ad..6c06f80cc8 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -732,9 +732,12 @@ static s_mc_address_space_class_t mc_snapshot_class = { 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); @@ -830,6 +833,8 @@ void MC_restore_snapshot_fds(mc_snapshot_t snapshot) 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); diff --git a/src/mc/mc_client.c b/src/mc/mc_client.c index 62c57338bd..6b70c894f3 100644 --- a/src/mc/mc_client.c +++ b/src/mc/mc_client.c @@ -23,6 +23,7 @@ #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"); @@ -57,10 +58,8 @@ void MC_client_init(void) 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) @@ -69,6 +68,12 @@ 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) { @@ -76,13 +81,12 @@ void MC_client_handle_messages(void) 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) { @@ -93,15 +97,41 @@ void MC_client_handle_messages(void) 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(); + } +} diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h index f5d01a57bf..7f82c11769 100644 --- a/src/mc/mc_client.h +++ b/src/mc/mc_client.h @@ -22,11 +22,14 @@ void MC_client_init(void); 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 diff --git a/src/mc/mc_client_api.c b/src/mc/mc_client_api.c index fad7c0ffd8..f9d58db27c 100644 --- a/src/mc/mc_client_api.c +++ b/src/mc/mc_client_api.c @@ -23,14 +23,12 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, 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(); + } } } diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index aed01eebfe..1941949139 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -346,8 +346,8 @@ void MC_modelcheck_comm_determinism(void) && (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) { diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index bc9169d373..10f95d265a 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -106,7 +106,7 @@ void MC_init() 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)) { @@ -115,7 +115,10 @@ void MC_init_pid(pid_t pid, int socket) 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) */ @@ -201,12 +204,6 @@ void MC_init_pid(pid_t pid, int socket) } mmalloc_set_current_heap(heap); - - if (mc_mode == MC_MODE_CLIENT) { - // This will move somehwere else: - MC_client_handle_messages(); - } - } /******************************* Core of MC *******************************/ @@ -215,6 +212,10 @@ void MC_init_pid(pid_t pid, int socket) 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); @@ -241,40 +242,15 @@ static void MC_modelcheck_comm_determinism_init(void) 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); @@ -298,20 +274,39 @@ static void MC_modelcheck_liveness_init() 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); @@ -337,12 +332,15 @@ int MC_deadlock_check() 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 @@ -457,7 +455,7 @@ void MC_replay(xbt_fifo_t stack) /* 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); } @@ -543,7 +541,7 @@ void MC_replay_liveness(xbt_fifo_t stack) /* 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); } @@ -606,7 +604,7 @@ void MC_show_stack_safety(xbt_fifo_t stack) : (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); } @@ -653,7 +651,7 @@ void MC_show_stack_liveness(xbt_fifo_t stack) 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); } @@ -812,3 +810,14 @@ void MC_process_clock_add(smx_process_t process, double amount) { 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); +} diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c index f213822d98..051a1f40c1 100644 --- a/src/mc/mc_ignore.c +++ b/src/mc/mc_ignore.c @@ -121,7 +121,6 @@ static void MC_heap_region_ignore_send(mc_heap_ignore_region_t region) 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: diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 4d7c048ec0..c648c6739e 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -299,8 +299,8 @@ void MC_modelcheck_liveness() 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 */ diff --git a/src/mc/mc_model_checker.c b/src/mc/mc_model_checker.c index 9482e45f04..98aa299117 100644 --- a/src/mc/mc_model_checker.c +++ b/src/mc/mc_model_checker.c @@ -28,3 +28,14 @@ void MC_model_checker_delete(mc_model_checker_t mc) 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; +} diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index 0b07e8e71c..1dee19e398 100644 --- a/src/mc/mc_model_checker.h +++ b/src/mc/mc_model_checker.h @@ -40,13 +40,7 @@ struct s_mc_model_checker { 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() diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 250c77f117..fed2f4d562 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -152,6 +152,8 @@ uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks); */ void MC_dump_stacks(FILE* file); +void MC_report_assertion_error(void); + SG_END_DECL() #endif diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c index 4fad0cbade..e49a7e23dc 100644 --- a/src/mc/mc_process.c +++ b/src/mc/mc_process.c @@ -26,6 +26,7 @@ #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"); @@ -161,15 +162,14 @@ void MC_process_refresh_heap(mc_process_t process) 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, @@ -621,27 +621,15 @@ void MC_simcall_handle(smx_simcall_t req, int value) 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"); } diff --git a/src/mc/mc_protocol.c b/src/mc/mc_protocol.c index 28150330fd..c51979787b 100644 --- a/src/mc/mc_protocol.c +++ b/src/mc/mc_protocol.c @@ -19,6 +19,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic"); 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; @@ -47,7 +51,7 @@ int MC_protocol_hello(int socket) 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 { @@ -63,7 +67,63 @@ int MC_protocol_hello(int socket) 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 "?"; + } } diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h index f0100fd06b..b6507f4c57 100644 --- a/src/mc/mc_protocol.h +++ b/src/mc/mc_protocol.h @@ -47,6 +47,9 @@ typedef enum { 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 @@ -88,6 +91,12 @@ typedef struct s_mc_stack_region_message { 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]; @@ -98,7 +107,10 @@ typedef struct s_mc_register_symbol_message { 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() diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index a4bd9d96ae..8b79524bd5 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -17,6 +17,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc, 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) @@ -37,23 +38,20 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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) @@ -64,25 +62,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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; } @@ -95,25 +93,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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; @@ -143,69 +141,69 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) 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; @@ -230,8 +228,19 @@ static char *buff_size_to_string(size_t buff_size) } -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; @@ -298,11 +307,16 @@ char *MC_request_to_string(smx_simcall_t req, int value) 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) : "", @@ -318,11 +332,16 @@ char *MC_request_to_string(smx_simcall_t req, int value) 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); @@ -330,8 +349,8 @@ char *MC_request_to_string(smx_simcall_t req, int value) 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), @@ -479,18 +498,16 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx) 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; diff --git a/src/mc/mc_request.h b/src/mc/mc_request.h index 1bc9eb8d7f..a95ff3526f 100644 --- a/src/mc/mc_request.h +++ b/src/mc/mc_request.h @@ -13,8 +13,14 @@ 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); diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c index 3dea427d7c..01c1d6b071 100644 --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@ -12,6 +12,7 @@ #include "mc_private.h" #include "mc_record.h" #include "mc_smx.h" +#include "mc_client.h" #include "xbt/mmalloc/mmprivate.h" @@ -35,17 +36,14 @@ static int is_exploration_stack_state(mc_state_t current_state){ /** * \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("**************************************************"); @@ -57,6 +55,7 @@ void MC_pre_modelcheck_safety() 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); @@ -73,14 +72,12 @@ void MC_pre_modelcheck_safety() /** \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; @@ -103,8 +100,8 @@ void MC_modelcheck_safety(void) 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) { @@ -116,10 +113,11 @@ void MC_modelcheck_safety(void) 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 */ @@ -135,6 +133,7 @@ void MC_modelcheck_safety(void) 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); @@ -184,8 +183,8 @@ void MC_modelcheck_safety(void) /* 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; @@ -213,12 +212,12 @@ void MC_modelcheck_safety(void) 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); } @@ -268,3 +267,33 @@ void MC_modelcheck_safety(void) 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(); +} diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h index 183ebac313..52ca5dabbe 100644 --- a/src/mc/mc_safety.h +++ b/src/mc/mc_safety.h @@ -24,7 +24,6 @@ typedef enum { 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{ diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index 39b15da755..869dd75818 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -55,11 +55,9 @@ void s_mc_server::start() /* 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; @@ -126,6 +124,7 @@ void s_mc_server::resume(mc_process_t process) 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 @@ -138,7 +137,7 @@ void throw_socket_error(int fd) 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]; @@ -156,7 +155,7 @@ void s_mc_server::handle_events() 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()); @@ -169,7 +168,6 @@ void s_mc_server::handle_events() 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"); @@ -180,10 +178,8 @@ void s_mc_server::handle_events() 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"); @@ -194,7 +190,6 @@ void s_mc_server::handle_events() 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"); @@ -206,7 +201,6 @@ void s_mc_server::handle_events() 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"); @@ -236,11 +230,19 @@ void s_mc_server::handle_events() 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); @@ -252,7 +254,7 @@ void s_mc_server::handle_events() 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); @@ -260,6 +262,8 @@ void s_mc_server::handle_events() if (signalfd_pollfd->revents & POLLHUP) xbt_die("Signalfd hang up?"); } + + return true; } void s_mc_server::loop() @@ -327,3 +331,27 @@ void s_mc_server::on_signal(const struct signalfd_siginfo* info) 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; + } +} diff --git a/src/mc/mc_server.h b/src/mc/mc_server.h index a8ea31bcb3..b6677d98da 100644 --- a/src/mc/mc_server.h +++ b/src/mc/mc_server.h @@ -7,7 +7,15 @@ #ifndef MC_SERVER_H #define MC_SERVER_H +#include +#include + +#include +#include + #include + +#include "mc_process.h" SG_BEGIN_DECL() @@ -17,6 +25,9 @@ typedef struct s_mc_server s_mc_server_t, *mc_server_t; 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 @@ -33,7 +44,7 @@ public: void exit(); void resume(mc_process_t process); void loop(); - void handle_events(); + bool handle_events(); protected: void handle_signals(); void handle_waitpid(); diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h index 98a2c70a75..61baa7eb58 100644 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@ -200,6 +200,7 @@ typedef struct s_fd_infos{ 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; diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 0e0126b212..8e707b2f9d 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -14,12 +14,16 @@ #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; @@ -89,8 +93,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, { 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 @@ -140,7 +144,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, 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; @@ -167,103 +171,108 @@ smx_simcall_t MC_state_get_internal_request(mc_state_t state) 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; diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index d121fdbf73..409acb5774 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -29,6 +29,7 @@ #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"); @@ -76,8 +77,23 @@ static int do_parent(int socket, pid_t child) 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(); } @@ -107,7 +123,7 @@ int main(int argc, char** argv) 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) @@ -115,7 +131,7 @@ int main(int argc, char** argv) 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) { diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c index 29474e8500..fd7b9d93af 100644 --- a/src/simix/smx_global.c +++ b/src/simix/smx_global.c @@ -219,6 +219,7 @@ void SIMIX_global_init(int *argc, char **argv) mc_mode = MC_MODE_CLIENT; MC_client_init(); MC_client_hello(); + MC_client_handle_messages(); } else { mc_mode = MC_MODE_STANDALONE; } diff --git a/teshsuite/mc/replay/random_bug.c b/teshsuite/mc/replay/random_bug.c index 80bcf410eb..4b8613c747 100644 --- a/teshsuite/mc/replay/random_bug.c +++ b/teshsuite/mc/replay/random_bug.c @@ -6,9 +6,13 @@ #include +#include + #include #include +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[]) @@ -33,5 +37,5 @@ int main(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(); } diff --git a/teshsuite/mc/replay/random_bug.tesh b/teshsuite/mc/replay/random_bug.tesh index 1b79e51dc7..59e995b3e0 100644 --- a/teshsuite/mc/replay/random_bug.tesh +++ b/teshsuite/mc/replay/random_bug.tesh @@ -2,13 +2,13 @@ !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