4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
5 "Logging specific to algorithms for liveness properties verification");
7 xbt_dynar_t initial_pairs = NULL;
8 xbt_fifo_t reached_pairs;
9 xbt_dynar_t successors = NULL;
10 extern mc_snapshot_t initial_snapshot;
12 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
14 XBT_DEBUG("Compare snapshot");
16 if(s1->num_reg != s2->num_reg){
17 XBT_DEBUG("Different num_reg");
24 for(i=0 ; i< s1->num_reg ; i++){
26 if(s1->regions[i]->size != s2->regions[i]->size){
27 XBT_DEBUG("Different size of region");
31 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
32 XBT_DEBUG("Different start addr of region");
36 if(s1->regions[i]->type != s2->regions[i]->type){
37 XBT_DEBUG("Different type of region");
42 if(s1->regions[i]->type == 0){
43 if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
44 XBT_DEBUG("Different heap (mmalloc_compare)");
48 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
49 XBT_DEBUG("Different memcmp for data in libsimgrid or program");
61 int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
64 if(xbt_fifo_size(reached_pairs) == 0){
72 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
74 /* Get values of propositional symbols */
75 unsigned int cursor = 0;
76 xbt_propositional_symbol_t ps = NULL;
77 xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
78 int (*f)() = ps->function;
80 xbt_dynar_push_as(prop_ato, int, res);
86 xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs);
87 mc_pair_reached_t pair_test = NULL;
89 while(i < xbt_fifo_size(reached_pairs)){
91 pair_test = (mc_pair_reached_t) xbt_fifo_get_item_content(item);
93 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
94 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
95 if(snapshot_compare(s, pair_test->system_state) == 0){
102 item = xbt_fifo_get_next_item(item);
114 void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
119 mc_pair_reached_t pair = NULL;
120 pair = xbt_new0(s_mc_pair_reached_t, 1);
121 pair->automaton_state = st;
122 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
123 pair->system_state = sn;
125 /* Get values of propositional symbols */
126 unsigned int cursor = 0;
127 xbt_propositional_symbol_t ps = NULL;
128 xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
129 int (*f)() = ps->function;
131 xbt_dynar_push_as(pair->prop_ato, int, res);
134 xbt_fifo_unshift(reached_pairs, pair);
141 void MC_pair_delete(mc_pair_t pair){
142 xbt_free(pair->graph_state->proc_status);
143 xbt_free(pair->graph_state);
144 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
150 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
154 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
155 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
156 return (left_res || right_res);
160 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
161 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
162 return (left_res && right_res);
166 int res = MC_automaton_evaluate_label(a, l->u.exp_not);
171 unsigned int cursor = 0;
172 xbt_propositional_symbol_t p = NULL;
173 xbt_dynar_foreach(a->propositional_symbols, cursor, p){
174 if(strcmp(p->pred, l->u.predicat) == 0){
175 int (*f)() = p->function;
195 /********************* Double-DFS stateless *******************/
197 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
198 xbt_free(pair->graph_state->proc_status);
199 xbt_free(pair->graph_state);
200 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
204 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
205 mc_pair_stateless_t p = NULL;
206 p = xbt_new0(s_mc_pair_stateless_t, 1);
207 p->automaton_state = st;
210 mc_stats_pair->expanded_pairs++;
214 void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
216 XBT_DEBUG("**************************************************");
217 XBT_DEBUG("Double-DFS stateless init");
218 XBT_DEBUG("**************************************************");
220 mc_pair_stateless_t mc_initial_pair = NULL;
221 mc_state_t initial_graph_state = NULL;
222 smx_process_t process;
224 MC_wait_for_requests();
228 initial_graph_state = MC_state_pair_new();
229 xbt_swag_foreach(process, simix_global->process_list){
230 if(MC_process_is_enabled(process)){
231 MC_state_interleave_process(initial_graph_state, process);
235 reached_pairs = xbt_fifo_new();
236 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
237 //snapshot = xbt_new0(s_mc_snapshot_t, 1);
239 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
240 MC_take_snapshot_liveness(initial_snapshot, prgm);
244 unsigned int cursor = 0;
247 xbt_dynar_foreach(a->states, cursor, state){
248 if(state->type == -1){
251 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
252 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
256 MC_restore_snapshot(initial_snapshot);
260 MC_ddfs_stateless(a, 0, 0, prgm);
263 if(state->type == 2){
266 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
267 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
270 set_pair_reached(a, state, initial_snapshot);
273 MC_restore_snapshot(initial_snapshot);
277 MC_ddfs_stateless(a, 1, 0, prgm);
286 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm){
288 smx_process_t process;
289 mc_pair_stateless_t current_pair = NULL;
290 mc_snapshot_t snapshot = NULL;
292 if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
296 MC_replay_liveness(mc_stack_liveness_stateless, 0);
297 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
298 xbt_swag_foreach(process, simix_global->process_list){
299 if(MC_process_is_enabled(process)){
300 MC_state_interleave_process(current_pair->graph_state, process);
305 /* Get current pair */
306 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
308 /* Update current state in buchi automaton */
309 a->current_state = current_pair->automaton_state;
312 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
313 XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
315 mc_stats_pair->visited_pairs++;
318 mc_state_t next_graph_state = NULL;
319 smx_req_t req = NULL;
322 xbt_transition_t transition_succ;
323 unsigned int cursor = 0;
326 mc_pair_stateless_t next_pair = NULL;
327 mc_pair_stateless_t pair_succ;
329 if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
331 if(current_pair->requests > 0){
333 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
335 /* Debug information */
336 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
337 req_str = MC_request_to_string(req, value);
338 XBT_DEBUG("Execute: %s", req_str);
342 MC_state_set_executed_request(current_pair->graph_state, req, value);
344 /* Answer the request */
345 SIMIX_request_pre(req, value);
347 /* Wait for requests (schedules processes) */
348 MC_wait_for_requests();
353 /* Create the new expanded graph_state */
354 next_graph_state = MC_state_pair_new();
356 /* Get enabled process and insert it in the interleave set of the next graph_state */
357 xbt_swag_foreach(process, simix_global->process_list){
358 if(MC_process_is_enabled(process)){
359 MC_state_interleave_process(next_graph_state, process);
363 xbt_dynar_reset(successors);
369 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
371 res = MC_automaton_evaluate_label(a, transition_succ->label);
373 if(res == 1){ // enabled transition in automaton
375 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
376 xbt_dynar_push(successors, &next_pair);
384 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
386 res = MC_automaton_evaluate_label(a, transition_succ->label);
388 if(res == 2){ // true transition in automaton
390 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
391 xbt_dynar_push(successors, &next_pair);
398 if(xbt_dynar_length(successors) == 0){
400 next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
401 xbt_dynar_push(successors, &next_pair);
407 xbt_dynar_foreach(successors, cursor, pair_succ){
409 if(search_cycle == 1){
411 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
414 snapshot = xbt_new0(s_mc_snapshot_t, 1);
415 MC_take_snapshot_liveness(snapshot, prgm);
418 if(reached(a, pair_succ->automaton_state, snapshot) == 1){
420 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
422 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
423 XBT_INFO("| ACCEPTANCE CYCLE |");
424 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
425 XBT_INFO("Counter-example that violates formula :");
426 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
427 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
428 MC_print_statistics_pairs(mc_stats_pair);
433 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
435 set_pair_reached(a, pair_succ->automaton_state, snapshot);
443 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
445 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
448 snapshot = xbt_new0(s_mc_snapshot_t, 1);
449 MC_take_snapshot_liveness(snapshot, prgm);
452 set_pair_reached(a, pair_succ->automaton_state, snapshot);
461 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
464 MC_ddfs_stateless(a, search_cycle, 0, prgm);
466 /* Restore system before checking others successors */
467 if(cursor != (xbt_dynar_length(successors) - 1))
468 MC_replay_liveness(mc_stack_liveness_stateless, 1);
472 if(MC_state_interleave_size(current_pair->graph_state) > 0){
473 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
474 MC_replay_liveness(mc_stack_liveness_stateless, 0);
479 }else{ /*No request to execute, search evolution in Büchi automaton */
483 /* Create the new expanded graph_state */
484 next_graph_state = MC_state_pair_new();
486 xbt_dynar_reset(successors);
492 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
494 res = MC_automaton_evaluate_label(a, transition_succ->label);
496 if(res == 1){ // enabled transition in automaton
498 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
499 xbt_dynar_push(successors, &next_pair);
507 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
509 res = MC_automaton_evaluate_label(a, transition_succ->label);
511 if(res == 2){ // true transition in automaton
513 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
514 xbt_dynar_push(successors, &next_pair);
521 if(xbt_dynar_length(successors) == 0){
523 next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
524 xbt_dynar_push(successors, &next_pair);
530 xbt_dynar_foreach(successors, cursor, pair_succ){
532 if(search_cycle == 1){
534 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
537 snapshot = xbt_new0(s_mc_snapshot_t, 1);
538 MC_take_snapshot_liveness(snapshot, prgm);
541 if(reached(a, pair_succ->automaton_state, snapshot) == 1){
543 XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
545 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
546 XBT_INFO("| ACCEPTANCE CYCLE |");
547 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
548 XBT_INFO("Counter-example that violates formula :");
549 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
550 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
551 MC_print_statistics_pairs(mc_stats_pair);
556 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
558 set_pair_reached(a, pair_succ->automaton_state, snapshot);
566 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){
569 snapshot = xbt_new0(s_mc_snapshot_t, 1);
570 MC_take_snapshot_liveness(snapshot, prgm);
573 set_pair_reached(a, pair_succ->automaton_state, snapshot);
582 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
585 MC_ddfs_stateless(a, search_cycle, 0, prgm);
587 /* Restore system before checking others successors */
588 if(cursor != xbt_dynar_length(successors) - 1)
589 MC_replay_liveness(mc_stack_liveness_stateless, 1);
596 if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
597 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle);
599 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
604 xbt_fifo_shift(mc_stack_liveness_stateless);
605 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
606 xbt_fifo_shift(reached_pairs);
609 MC_free_snapshot(snapshot);
612 MC_pair_stateless_delete(current_pair);
614 /* FIXME : free memory (pair, snapshot)*/