-
- /* Fork an mc's slave exploration process and wait for it. */
- /* The forked process will explore a trace until:
- - a back-tracking point is found (it sets mc_expl_ctl to MC_explore)
- - there are no more states to explore (it sets mc_expl_ctl to MC_STOP)
- - a property is invalid (or dead-lock)
- */
- while(*mc_exp_ctl == MC_EXPLORE){
- if((pid = fork())){
- waitpid(pid, &status, 0);
- mmalloc_detach(raw_heap);
- raw_heap = mmalloc_attach(raw_heap_fd, (char*)(std_heap) + STD_HEAP_SIZE + getpagesize());
-
- if (WIFSIGNALED(status)) {
- INFO1("killed by signal %d\n", WTERMSIG(status));
- break;
- }else if (WIFSTOPPED(status)) {
- INFO1("stopped by signal %d\n", WSTOPSIG(status));
- break;
- }else if (WIFCONTINUED(status)) {
- INFO0("continued\n");
- break;
- }
-
- if(*mc_exp_ctl == MC_DEADLOCK){
- INFO0("**************************");
- INFO0("*** DEAD-LOCK DETECTED ***");
- INFO0("**************************");
- MC_dump_stack(mc_stack);
- MC_print_statistics(mc_stats);
- break;
- }
-
- }else{
- /* if mc_stack is empty then create first state, otherwise replay */
- if(xbt_fifo_size(mc_stack) == 0)
- MC_dpor_init();
- else
- MC_replay(mc_stack);
-
- MC_dpor();
- MC_memory_exit();
- break;
- }
- }
-
- /* If we are the mc's master process then exit */
- if(pid)
- MC_exit();