* under the terms of the license (GNU LGPL) which comes with this package. */
#include <string.h>
+#include <stdint.h>
#include "mc_base.h"
#include "xbt/fifo.h"
#include "xbt/automaton.h"
#include "xbt/dict.h"
+#include "mc_server.h"
#ifdef HAVE_MC
#include <libunwind.h>
MC_SET_STD_HEAP;
- if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination) {
+ if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
/* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
MC_ignore_local_variable("e", "*");
MC_ignore_local_variable("__ex_cleanup", "*");
/******************************* 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);
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_comm_determinism();
-
- MC_SET_MC_HEAP;
- initial_global_state = xbt_new0(s_mc_global_t, 1);
- initial_global_state->snapshot = MC_take_snapshot(0);
- initial_global_state->initial_communications_pattern_done = 0;
- initial_global_state->recv_deterministic = 1;
- initial_global_state->send_deterministic = 1;
- initial_global_state->recv_diff = NULL;
- initial_global_state->send_diff = NULL;
-
- MC_SET_STD_HEAP;
-
- MC_modelcheck_comm_determinism();
-
- mmalloc_set_current_heap(heap);
-}
-
-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);
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- /* Create the initial state */
- initial_global_state = xbt_new0(s_mc_global_t, 1);
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_liveness();
-
- /* We're done */
- MC_print_statistics(mc_stats);
- xbt_free(mc_time);
-
- mmalloc_set_current_heap(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();
+ // TODO, move this part in the MCer process
+ if (mc_mode == MC_MODE_SERVER)
+ MC_server_loop(mc_server);
+ else {
+ XBT_INFO("Check communication determinism");
+ mc_reduce_kind = e_mc_reduce_none;
+ MC_modelcheck_comm_determinism();
+ }
}
else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
- if(_sg_mc_termination){
- XBT_INFO("Check non progressive cycles");
+ if(_sg_mc_termination)
mc_reduce_kind = e_mc_reduce_none;
- } 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();
- }
- }
+ else if (mc_reduce_kind == e_mc_reduce_unset)
+ mc_reduce_kind = e_mc_reduce_dpor;
+ _sg_mc_safety = 1;
+ if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+ if (_sg_mc_termination)
+ XBT_INFO("Check non progressive cycles");
+ else
+ XBT_INFO("Check a safety property");
+ MC_wait_for_requests();
+ MC_modelcheck_safety();
+ }
+ else {
+ // Most of this is not needed:
+ MC_init();
+ // Main event loop:
+ MC_client_main_loop();
}
}
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_automaton_load(_sg_mc_property_file);
- MC_modelcheck_liveness_init();
+ if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+ XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
+ MC_automaton_load(_sg_mc_property_file);
+ MC_modelcheck_liveness();
+ } else {
+ MC_init();
+ MC_client_main_loop();
+ }
}
}
unw_word_t off;
do {
const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?";
+#if defined(__x86_64__)
+ unw_word_t rip = 0;
+ unw_word_t rsp = 0;
+ unw_get_reg(&c, UNW_X86_64_RIP, &rip);
+ unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
+ fprintf(file, " %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
+ nframe, name, rip, rsp);
+#else
fprintf(file, " %i: %s\n", nframe, name);
+#endif
++nframe;
} while(unw_step(&c));