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. */
7 #include "mc_private.h"
9 #include "xbt/mmalloc/mmprivate.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
12 "Logging specific to MC safety verification ");
14 xbt_dict_t first_enabled_state;
17 * \brief Initialize the DPOR exploration algorithm
19 void MC_pre_modelcheck_safety()
22 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
24 mc_state_t initial_state = NULL;
25 smx_process_t process;
27 /* Create the initial state and push it into the exploration stack */
31 if (_sg_mc_visited > 0)
33 xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
35 if (mc_reduce_kind == e_mc_reduce_dpor)
36 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
38 initial_state = MC_state_new();
42 XBT_DEBUG("**************************************************");
43 XBT_DEBUG("Initial state");
45 /* Wait for requests (schedules processes) */
46 MC_wait_for_requests();
50 /* Get an enabled process and insert it in the interleave set of the initial state */
51 xbt_swag_foreach(process, simix_global->process_list) {
52 if (MC_process_is_enabled(process)) {
53 MC_state_interleave_process(initial_state, process);
54 if (mc_reduce_kind != e_mc_reduce_none)
59 xbt_fifo_unshift(mc_stack, initial_state);
61 if (mc_reduce_kind == e_mc_reduce_dpor) {
62 /* To ensure the soundness of DPOR, we have to keep a list of
63 processes which are still enabled at each step of the exploration.
64 If max depth is reached, we interleave them in the state in which they have
65 been enabled for the first time. */
66 xbt_swag_foreach(process, simix_global->process_list) {
67 if (MC_process_is_enabled(process)) {
68 char *key = bprintf("%lu", process->pid);
69 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
70 xbt_dict_set(first_enabled_state, key, data, NULL);
81 /** \brief Model-check the application using a DFS exploration
82 * with DPOR (Dynamic Partial Order Reductions)
84 void MC_modelcheck_safety(void)
89 smx_simcall_t req = NULL, prev_req = NULL;
90 mc_state_t state = NULL, prev_state = NULL, next_state =
91 NULL, restored_state = NULL;
92 smx_process_t process = NULL;
93 xbt_fifo_item_t item = NULL;
94 mc_state_t state_test = NULL;
96 mc_visited_state_t visited_state = NULL;
99 while (xbt_fifo_size(mc_stack) > 0) {
101 /* Get current state */
103 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
105 XBT_DEBUG("**************************************************");
107 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
108 xbt_fifo_size(mc_stack), state, state->num,
109 MC_state_interleave_size(state), user_max_depth_reached,
110 xbt_dict_size(first_enabled_state));
112 /* Update statistics */
113 mc_stats->visited_states++;
115 /* If there are processes to interleave and the maximum depth has not been reached
116 then perform one step of the exploration algorithm */
117 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
118 && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
120 MC_LOG_REQUEST(mc_safety, req, value);
122 if (dot_output != NULL) {
124 req_str = MC_request_get_dot_output(req, value);
128 MC_state_set_executed_request(state, req, value);
129 mc_stats->executed_transitions++;
131 if (mc_reduce_kind == e_mc_reduce_dpor) {
133 char *key = bprintf("%lu", req->issuer->pid);
134 xbt_dict_remove(first_enabled_state, key);
139 /* Answer the request */
140 SIMIX_simcall_enter(req, value);
142 /* Wait for requests (schedules processes) */
143 MC_wait_for_requests();
145 /* Create the new expanded state */
148 next_state = MC_state_new();
150 if ((visited_state = is_visited_state()) == NULL) {
152 /* Get an enabled process and insert it in the interleave set of the next state */
153 xbt_swag_foreach(process, simix_global->process_list) {
154 if (MC_process_is_enabled(process)) {
155 MC_state_interleave_process(next_state, process);
156 if (mc_reduce_kind != e_mc_reduce_none)
161 if (_sg_mc_checkpoint
162 && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
163 next_state->system_state = MC_take_snapshot(next_state->num);
166 if (dot_output != NULL)
167 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
168 next_state->num, req_str);
172 if (dot_output != NULL)
173 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
174 visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
178 xbt_fifo_unshift(mc_stack, next_state);
180 if (mc_reduce_kind == e_mc_reduce_dpor) {
181 /* Insert in dict all enabled processes, if not included yet */
182 xbt_swag_foreach(process, simix_global->process_list) {
183 if (MC_process_is_enabled(process)) {
184 char *key = bprintf("%lu", process->pid);
185 if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
186 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
187 xbt_dict_set(first_enabled_state, key, data, NULL);
194 if (dot_output != NULL)
199 /* Let's loop again */
201 /* The interleave set is empty or the maximum depth is reached, let's back-track */
204 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
205 || visited_state != NULL) {
207 if (user_max_depth_reached && visited_state == NULL)
208 XBT_DEBUG("User max depth reached !");
209 else if (visited_state == NULL)
210 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
212 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);
214 if (mc_reduce_kind == e_mc_reduce_dpor) {
215 /* Interleave enabled processes in the state in which they have been enabled for the first time */
216 xbt_swag_foreach(process, simix_global->process_list) {
217 if (MC_process_is_enabled(process)) {
218 char *key = bprintf("%lu", process->pid);
220 (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
223 int cursor = xbt_fifo_size(mc_stack);
224 xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
225 if (cursor-- == enabled) {
226 if (!MC_state_process_is_done(state_test, process)
227 && state_test->num != state->num) {
228 XBT_DEBUG("Interleave process %lu in state %d",
229 process->pid, state_test->num);
230 MC_state_interleave_process(state_test, process);
241 XBT_DEBUG("There are no more processes to interleave. (depth %d)",
242 xbt_fifo_size(mc_stack) + 1);
248 /* Trash the current state, no longer needed */
249 xbt_fifo_shift(mc_stack);
250 MC_state_delete(state);
251 XBT_DEBUG("Delete state %d at depth %d", state->num,
252 xbt_fifo_size(mc_stack) + 1);
256 visited_state = NULL;
258 /* Check for deadlocks */
259 if (MC_deadlock_check()) {
260 MC_show_deadlock(NULL);
265 /* Traverse the stack backwards until a state with a non empty interleave
266 set is found, deleting all the states that have it empty in the way.
267 For each deleted state, check if the request that has generated it
268 (from it's predecesor state), depends on any other previous request
269 executed before it. If it does then add it to the interleave set of the
270 state that executed that previous request. */
272 while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
273 if (mc_reduce_kind == e_mc_reduce_dpor) {
274 req = MC_state_get_internal_request(state);
275 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
276 if (MC_request_depend
277 (req, MC_state_get_internal_request(prev_state))) {
278 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
279 XBT_DEBUG("Dependent Transitions:");
280 prev_req = MC_state_get_executed_request(prev_state, &value);
281 req_str = MC_request_to_string(prev_req, value);
282 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
284 prev_req = MC_state_get_executed_request(state, &value);
285 req_str = MC_request_to_string(prev_req, value);
286 XBT_DEBUG("%s (state=%d)", req_str, state->num);
290 if (!MC_state_process_is_done(prev_state, req->issuer))
291 MC_state_interleave_process(prev_state, req->issuer);
293 XBT_DEBUG("Process %p is in done set", req->issuer);
297 } else if (req->issuer ==
298 MC_state_get_internal_request(prev_state)->issuer) {
300 XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
301 MC_state_get_internal_request(prev_state)->call);
307 ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
308 req->call, req->issuer->pid, state->num,
309 MC_state_get_internal_request(prev_state)->call,
310 MC_state_get_internal_request(prev_state)->issuer->pid,
317 if (MC_state_interleave_size(state)
318 && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
319 /* We found a back-tracking point, let's loop */
320 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
321 xbt_fifo_size(mc_stack) + 1);
322 if (_sg_mc_checkpoint) {
323 if (state->system_state != NULL) {
324 MC_restore_snapshot(state->system_state);
325 xbt_fifo_unshift(mc_stack, state);
328 pos = xbt_fifo_size(mc_stack);
329 item = xbt_fifo_get_first_item(mc_stack);
331 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
332 if (restored_state->system_state != NULL) {
335 item = xbt_fifo_get_next_item(item);
339 MC_restore_snapshot(restored_state->system_state);
340 xbt_fifo_unshift(mc_stack, state);
342 MC_replay(mc_stack, pos);
345 xbt_fifo_unshift(mc_stack, state);
347 MC_replay(mc_stack, -1);
349 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
350 xbt_fifo_size(mc_stack));
353 XBT_DEBUG("Delete state %d at depth %d", state->num,
354 xbt_fifo_size(mc_stack) + 1);
355 MC_state_delete(state);
361 MC_print_statistics(mc_stats);