int coordinator(int argc, char *argv[])
{
-
int CS_used = 0;
msg_task_t task = NULL, answer = NULL;
xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
int main(int argc, char *argv[])
{
-
MSG_init(&argc, argv);
-
char **options = &argv[1];
- MSG_config("model-check/property","promela_bugged1_liveness");
MC_automaton_new_propositional_symbol_pointer("r", &r);
MC_automaton_new_propositional_symbol_pointer("cs", &cs);
const char* platform_file = options[0];
const char* application_file = options[1];
-
+
MSG_create_environment(platform_file);
+
MSG_function_register("coordinator", coordinator);
MSG_function_register("client", raw_client);
MSG_launch_application(application_file);
+
MSG_main();
return 0;
! expect signal SIGABRT
! timeout 20
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
+> [ 0.000000] (0:@) Pair 23 already reached (equal to pair 11) !
> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
> [ 0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
> [ 0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:@) Expanded pairs = 22
-> [ 0.000000] (0:@) Visited pairs = 20
-> [ 0.000000] (0:@) Executed transitions = 20
-> [ 0.000000] (0:@) Counter-example depth : 21
-
+> [ 0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) Expanded pairs = 23
+> [ 0.000000] (0:@) Visited pairs = 21
+> [ 0.000000] (0:@) Executed transitions = 21
+> [ 0.000000] (0:@) Counter-example depth : 22
! expect signal SIGABRT
! timeout 60
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
+> [ 0.000000] (0:@) Pair 23 already reached (equal to pair 11) !
> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 0.000000] (0:@) | ACCEPTANCE CYCLE |
> [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
> [ 0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
> [ 0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
> [ 0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:@) Expanded pairs = 22
-> [ 0.000000] (0:@) Visited pairs = 20
-> [ 0.000000] (0:@) Executed transitions = 20
-> [ 0.000000] (0:@) Counter-example depth : 21
+> [ 0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:@) Expanded pairs = 23
+> [ 0.000000] (0:@) Visited pairs = 21
+> [ 0.000000] (0:@) Executed transitions = 21
+> [ 0.000000] (0:@) Counter-example depth : 22
! expect signal SIGABRT
! timeout 90
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (0:@) Visited pairs = 201
> [ 0.000000] (0:@) Executed transitions = 207
> [ 0.000000] (0:@) Counter-example depth : 51
-
! expect signal SIGABRT
! timeout 90
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
MSG_init(&argc, argv);
- MSG_config("model-check/property","promela_bugged2_liveness");
MC_automaton_new_propositional_symbol_pointer("cs", &cs);
MSG_create_environment("../msg_platform.xml");
{ \
xbt_running_ctx_t *__xbt_ex_ctx_ptr = __xbt_running_ctx_fetch(); \
int __ex_cleanup = 0; \
- __ex_mctx_t *__ex_mctx_en; \
__ex_mctx_t __ex_mctx_me; \
- __ex_mctx_en = __xbt_ex_ctx_ptr->ctx_mctx; \
+ __ex_mctx_t * __ex_mctx_en = __xbt_ex_ctx_ptr->ctx_mctx; \
__xbt_ex_ctx_ptr->ctx_mctx = &__ex_mctx_me; \
if (__ex_mctx_save(&__ex_mctx_me)) { \
if (1)
#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", "*");
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_init();
+ }
}
else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
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();
+ }
}
}
#include "mc_private.h"
#include "mc_record.h"
#include "mc_smx.h"
+#include "mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
}
}
-void MC_pre_modelcheck_liveness(void) {
+static void MC_modelcheck_liveness_main(void);
+static void MC_pre_modelcheck_liveness(void)
+{
initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
mc_pair_t initial_pair = NULL;
smx_process_t process;
+ // TODO, fix this
+ MC_wait_for_requests();
MC_wait_for_requests();
MC_SET_MC_HEAP;
MC_SET_STD_HEAP;
- MC_modelcheck_liveness();
+ MC_modelcheck_liveness_main();
if (initial_global_state->raw_mem_set)
MC_SET_MC_HEAP;
}
-void MC_modelcheck_liveness()
+static void MC_modelcheck_liveness_main(void)
{
smx_process_t process = NULL;
mc_pair_t current_pair = NULL;
/* Update current state in buchi automaton */
_mc_property_automaton->current_state = current_pair->automaton_state;
- XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)",
+ XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %d, pair_num = %d, requests = %d)",
current_pair->depth, current_pair->search_cycle,
- MC_state_interleave_size(current_pair->graph_state), current_pair->num);
+ MC_state_interleave_size(current_pair->graph_state), current_pair->num,
+ current_pair->requests);
if (current_pair->requests > 0) {
} /* End of while(xbt_fifo_size(mc_stack) > 0) */
}
+
+void MC_modelcheck_liveness(void)
+{
+ XBT_DEBUG("Starting the liveness algorithm");
+ xbt_assert(mc_mode == MC_MODE_SERVER);
+ _sg_mc_liveness = 1;
+
+ 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);
+
+}
mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
void MC_visited_pair_delete(mc_visited_pair_t p);
-void MC_pre_modelcheck_liveness(void);
void MC_modelcheck_liveness(void);
void MC_show_stack_liveness(xbt_fifo_t stack);
void MC_dump_stack_liveness(xbt_fifo_t stack);
return;
}
}
+
+void MC_server_loop(mc_server_t server)
+{
+ server->loop();
+}
void MC_server_wait_client(mc_process_t process);
void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value);
+void MC_server_loop(mc_server_t server);
+
SG_END_DECL()
#ifdef __cplusplus
static mc_visited_state_t visited_state_new()
{
mc_process_t process = &(mc_model_checker->process);
- mc_visited_state_t new_state = NULL;
- new_state = xbt_new0(s_mc_visited_state_t, 1);
+ mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
MC_process_get_heap(process)->heaplimit,
MC_process_get_malloc_info(process));
mc_server = new s_mc_server(child, socket);
mc_server->start();
MC_init_pid(child, socket);
-
- 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;
- MC_do_the_modelcheck_for_real();
- }
-
- else {
- mc_server->loop();
- }
-
+ MC_do_the_modelcheck_for_real();
mc_server->shutdown();
mc_server->exit();
}
MSG_mailbox_put_with_timeout(msg_mailbox_t mailbox, msg_task_t task,
double timeout)
{
- xbt_ex_t e;
msg_error_t ret = MSG_OK;
simdata_task_t t_simdata = NULL;
msg_process_t process = MSG_process_self();
p_simdata->waiting_task = task;
+ xbt_ex_t e;
/* Try to send it by calling SIMIX network layer */
TRY {
smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simix call */