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. */
8 #include "mc_request.h"
10 #include "mc_private.h"
11 #include "mc_record.h"
13 #include "xbt/mmalloc/mmprivate.h"
15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
16 "Logging specific to MC safety verification ");
18 xbt_dict_t first_enabled_state;
21 * \brief Initialize the DPOR exploration algorithm
23 void MC_pre_modelcheck_safety()
26 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
28 mc_state_t initial_state = NULL;
29 smx_process_t process;
31 /* Create the initial state and push it into the exploration stack */
35 if (_sg_mc_visited > 0)
37 xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
39 if (mc_reduce_kind == e_mc_reduce_dpor)
40 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
42 initial_state = MC_state_new();
46 XBT_DEBUG("**************************************************");
47 XBT_DEBUG("Initial state");
49 /* Wait for requests (schedules processes) */
50 MC_wait_for_requests();
54 /* Get an enabled process and insert it in the interleave set of the initial state */
55 xbt_swag_foreach(process, simix_global->process_list) {
56 if (MC_process_is_enabled(process)) {
57 MC_state_interleave_process(initial_state, process);
58 if (mc_reduce_kind != e_mc_reduce_none)
63 xbt_fifo_unshift(mc_stack, initial_state);
65 if (mc_reduce_kind == e_mc_reduce_dpor) {
66 /* To ensure the soundness of DPOR, we have to keep a list of
67 processes which are still enabled at each step of the exploration.
68 If max depth is reached, we interleave them in the state in which they have
69 been enabled for the first time. */
70 xbt_swag_foreach(process, simix_global->process_list) {
71 if (MC_process_is_enabled(process)) {
72 char *key = bprintf("%lu", process->pid);
73 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
74 xbt_dict_set(first_enabled_state, key, data, NULL);
85 /** \brief Model-check the application using a DFS exploration
86 * with DPOR (Dynamic Partial Order Reductions)
88 void MC_modelcheck_safety(void)
93 smx_simcall_t req = NULL, prev_req = NULL;
94 mc_state_t state = NULL, prev_state = NULL, next_state =
95 NULL, restored_state = NULL;
96 smx_process_t process = NULL;
97 xbt_fifo_item_t item = NULL;
98 mc_state_t state_test = NULL;
100 mc_visited_state_t visited_state = NULL;
103 while (xbt_fifo_size(mc_stack) > 0) {
105 /* Get current state */
107 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
109 XBT_DEBUG("**************************************************");
111 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
112 xbt_fifo_size(mc_stack), state, state->num,
113 MC_state_interleave_size(state), user_max_depth_reached,
114 xbt_dict_size(first_enabled_state));
116 /* Update statistics */
117 mc_stats->visited_states++;
119 /* If there are processes to interleave and the maximum depth has not been reached
120 then perform one step of the exploration algorithm */
121 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
122 && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
124 MC_LOG_REQUEST(mc_safety, req, value);
126 if (dot_output != NULL) {
128 req_str = MC_request_get_dot_output(req, value);
132 MC_state_set_executed_request(state, req, value);
133 mc_stats->executed_transitions++;
135 if (mc_reduce_kind == e_mc_reduce_dpor) {
137 char *key = bprintf("%lu", req->issuer->pid);
138 xbt_dict_remove(first_enabled_state, key);
143 /* Answer the request */
144 SIMIX_simcall_handle(req, value);
146 /* Wait for requests (schedules processes) */
147 MC_wait_for_requests();
149 /* Create the new expanded state */
152 next_state = MC_state_new();
154 if ((visited_state = is_visited_state()) == NULL) {
156 /* Get an enabled process and insert it in the interleave set of the next state */
157 xbt_swag_foreach(process, simix_global->process_list) {
158 if (MC_process_is_enabled(process)) {
159 MC_state_interleave_process(next_state, process);
160 if (mc_reduce_kind != e_mc_reduce_none)
165 if (_sg_mc_checkpoint
166 && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
167 next_state->system_state = MC_take_snapshot(next_state->num);
170 if (dot_output != NULL)
171 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
172 next_state->num, req_str);
176 if (dot_output != NULL)
177 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
178 visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
182 xbt_fifo_unshift(mc_stack, next_state);
184 if (mc_reduce_kind == e_mc_reduce_dpor) {
185 /* Insert in dict all enabled processes, if not included yet */
186 xbt_swag_foreach(process, simix_global->process_list) {
187 if (MC_process_is_enabled(process)) {
188 char *key = bprintf("%lu", process->pid);
189 if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
190 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
191 xbt_dict_set(first_enabled_state, key, data, NULL);
198 if (dot_output != NULL)
203 /* Let's loop again */
205 /* The interleave set is empty or the maximum depth is reached, let's back-track */
208 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
209 || visited_state != NULL) {
211 if (user_max_depth_reached && visited_state == NULL)
212 XBT_DEBUG("User max depth reached !");
213 else if (visited_state == NULL)
214 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
216 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);
218 if (mc_reduce_kind == e_mc_reduce_dpor) {
219 /* Interleave enabled processes in the state in which they have been enabled for the first time */
220 xbt_swag_foreach(process, simix_global->process_list) {
221 if (MC_process_is_enabled(process)) {
222 char *key = bprintf("%lu", process->pid);
224 (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
227 int cursor = xbt_fifo_size(mc_stack);
228 xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
229 if (cursor-- == enabled) {
230 if (!MC_state_process_is_done(state_test, process)
231 && state_test->num != state->num) {
232 XBT_DEBUG("Interleave process %lu in state %d",
233 process->pid, state_test->num);
234 MC_state_interleave_process(state_test, process);
245 XBT_DEBUG("There are no more processes to interleave. (depth %d)",
246 xbt_fifo_size(mc_stack) + 1);
252 /* Trash the current state, no longer needed */
253 xbt_fifo_shift(mc_stack);
254 MC_state_delete(state);
255 XBT_DEBUG("Delete state %d at depth %d", state->num,
256 xbt_fifo_size(mc_stack) + 1);
260 visited_state = NULL;
262 /* Check for deadlocks */
263 if (MC_deadlock_check()) {
264 MC_show_deadlock(NULL);
269 /* Traverse the stack backwards until a state with a non empty interleave
270 set is found, deleting all the states that have it empty in the way.
271 For each deleted state, check if the request that has generated it
272 (from it's predecesor state), depends on any other previous request
273 executed before it. If it does then add it to the interleave set of the
274 state that executed that previous request. */
276 while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
277 if (mc_reduce_kind == e_mc_reduce_dpor) {
278 req = MC_state_get_internal_request(state);
279 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
280 if (MC_request_depend
281 (req, MC_state_get_internal_request(prev_state))) {
282 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
283 XBT_DEBUG("Dependent Transitions:");
284 prev_req = MC_state_get_executed_request(prev_state, &value);
285 req_str = MC_request_to_string(prev_req, value);
286 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
288 prev_req = MC_state_get_executed_request(state, &value);
289 req_str = MC_request_to_string(prev_req, value);
290 XBT_DEBUG("%s (state=%d)", req_str, state->num);
294 if (!MC_state_process_is_done(prev_state, req->issuer))
295 MC_state_interleave_process(prev_state, req->issuer);
297 XBT_DEBUG("Process %p is in done set", req->issuer);
301 } else if (req->issuer ==
302 MC_state_get_internal_request(prev_state)->issuer) {
304 XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
305 MC_state_get_internal_request(prev_state)->call);
311 ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
312 req->call, req->issuer->pid, state->num,
313 MC_state_get_internal_request(prev_state)->call,
314 MC_state_get_internal_request(prev_state)->issuer->pid,
321 if (MC_state_interleave_size(state)
322 && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
323 /* We found a back-tracking point, let's loop */
324 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
325 xbt_fifo_size(mc_stack) + 1);
326 if (_sg_mc_checkpoint) {
327 if (state->system_state != NULL) {
328 MC_restore_snapshot(state->system_state);
329 xbt_fifo_unshift(mc_stack, state);
332 pos = xbt_fifo_size(mc_stack);
333 item = xbt_fifo_get_first_item(mc_stack);
335 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
336 if (restored_state->system_state != NULL) {
339 item = xbt_fifo_get_next_item(item);
343 MC_restore_snapshot(restored_state->system_state);
344 xbt_fifo_unshift(mc_stack, state);
346 MC_replay(mc_stack, pos);
349 xbt_fifo_unshift(mc_stack, state);
351 MC_replay(mc_stack, -1);
353 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
354 xbt_fifo_size(mc_stack));
357 XBT_DEBUG("Delete state %d at depth %d", state->num,
358 xbt_fifo_size(mc_stack) + 1);
359 MC_state_delete(state);
365 MC_print_statistics(mc_stats);