1 /* Copyright (c) 2008-2014. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
10 #include "mc_request.h"
11 #include "mc_safety.h"
12 #include "mc_private.h"
13 #include "mc_record.h"
15 #include "mc_client.h"
17 #include "xbt/mmalloc/mmprivate.h"
21 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
22 "Logging specific to MC safety verification ");
24 static int is_exploration_stack_state(mc_state_t current_state){
27 mc_state_t stack_state;
28 for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
29 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
30 if(snapshot_compare(stack_state, current_state) == 0){
31 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
39 * \brief Initialize the DPOR exploration algorithm
41 static void MC_pre_modelcheck_safety()
43 if (_sg_mc_visited > 0)
44 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
46 mc_state_t initial_state = MC_state_new();
48 XBT_DEBUG("**************************************************");
49 XBT_DEBUG("Initial state");
51 /* Wait for requests (schedules processes) */
52 MC_wait_for_requests();
54 /* Get an enabled process and insert it in the interleave set of the initial state */
55 smx_process_t process;
56 MC_EACH_SIMIX_PROCESS(process,
57 if (MC_process_is_enabled(process)) {
58 MC_state_interleave_process(initial_state, process);
59 if (mc_reduce_kind != e_mc_reduce_none)
64 xbt_fifo_unshift(mc_stack, initial_state);
68 /** \brief Model-check the application using a DFS exploration
69 * with DPOR (Dynamic Partial Order Reductions)
71 static void MC_modelcheck_safety_main(void)
75 smx_simcall_t req = NULL;
76 mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
77 xbt_fifo_item_t item = NULL;
78 mc_visited_state_t visited_state = NULL;
80 while (xbt_fifo_size(mc_stack) > 0) {
82 /* Get current state */
83 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
85 XBT_DEBUG("**************************************************");
87 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
88 xbt_fifo_size(mc_stack), state, state->num,
89 MC_state_interleave_size(state), user_max_depth_reached);
91 /* Update statistics */
92 mc_stats->visited_states++;
94 /* If there are processes to interleave and the maximum depth has not been reached
95 then perform one step of the exploration algorithm */
96 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
97 && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
99 req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
100 XBT_DEBUG("Execute: %s", req_str);
103 if (dot_output != NULL) {
104 req_str = MC_request_get_dot_output(req, value);
107 MC_state_set_executed_request(state, req, value);
108 mc_stats->executed_transitions++;
110 // TODO, bundle both operations in a single message
111 // MC_execute_transition(req, value)
113 /* Answer the request */
114 MC_simcall_handle(req, value);
115 MC_wait_for_requests();
117 /* Create the new expanded state */
118 next_state = MC_state_new();
120 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
121 MC_show_non_termination();
125 if ((visited_state = is_visited_state(next_state)) == NULL) {
127 /* Get an enabled process and insert it in the interleave set of the next state */
128 smx_process_t process = NULL;
129 MC_EACH_SIMIX_PROCESS(process,
130 if (MC_process_is_enabled(process)) {
131 MC_state_interleave_process(next_state, process);
132 if (mc_reduce_kind != e_mc_reduce_none)
137 if (dot_output != NULL)
138 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
142 if (dot_output != NULL)
143 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
147 xbt_fifo_unshift(mc_stack, next_state);
149 if (dot_output != NULL)
152 /* Let's loop again */
154 /* The interleave set is empty or the maximum depth is reached, let's back-track */
157 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
159 if (user_max_depth_reached && visited_state == NULL)
160 XBT_DEBUG("User max depth reached !");
161 else if (visited_state == NULL)
162 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
164 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
168 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
172 /* Trash the current state, no longer needed */
173 xbt_fifo_shift(mc_stack);
174 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
175 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
177 visited_state = NULL;
179 /* Check for deadlocks */
180 if (MC_deadlock_check()) {
181 MC_show_deadlock(NULL);
185 /* Traverse the stack backwards until a state with a non empty interleave
186 set is found, deleting all the states that have it empty in the way.
187 For each deleted state, check if the request that has generated it
188 (from it's predecesor state), depends on any other previous request
189 executed before it. If it does then add it to the interleave set of the
190 state that executed that previous request. */
192 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
193 if (mc_reduce_kind == e_mc_reduce_dpor) {
194 req = MC_state_get_internal_request(state);
195 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
196 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
197 if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
198 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
199 XBT_DEBUG("Dependent Transitions:");
200 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
201 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
202 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
204 prev_req = MC_state_get_executed_request(state, &value);
205 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
206 XBT_DEBUG("%s (state=%d)", req_str, state->num);
210 if (!MC_state_process_is_done(prev_state, issuer))
211 MC_state_interleave_process(prev_state, issuer);
213 XBT_DEBUG("Process %p is in done set", req->issuer);
217 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
219 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
224 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
225 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
226 req->call, issuer->pid, state->num,
227 MC_state_get_internal_request(prev_state)->call,
228 previous_issuer->pid,
235 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
236 /* We found a back-tracking point, let's loop */
237 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
238 xbt_fifo_unshift(mc_stack, state);
240 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
243 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
244 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
249 MC_print_statistics(mc_stats);
253 void MC_modelcheck_safety(void)
255 if(_sg_mc_termination)
256 mc_reduce_kind = e_mc_reduce_none;
257 else if (mc_reduce_kind == e_mc_reduce_unset)
258 mc_reduce_kind = e_mc_reduce_dpor;
260 if (_sg_mc_termination)
261 XBT_INFO("Check non progressive cycles");
263 XBT_INFO("Check a safety property");
264 MC_wait_for_requests();
266 XBT_DEBUG("Starting the safety algorithm");
270 /* Create exploration stack */
271 mc_stack = xbt_fifo_new();
273 MC_pre_modelcheck_safety();
275 /* Save the initial state */
276 initial_global_state = xbt_new0(s_mc_global_t, 1);
277 initial_global_state->snapshot = MC_take_snapshot(0);
279 MC_modelcheck_safety_main();