1 /* Copyright (c) 2008-2015. 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"
18 #include "xbt/mmalloc/mmprivate.h"
22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
23 "Logging specific to MC safety verification ");
27 static int is_exploration_stack_state(mc_state_t current_state){
30 mc_state_t stack_state;
31 for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
32 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
33 if(snapshot_compare(stack_state, current_state) == 0){
34 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
41 static void MC_modelcheck_safety_init(void);
44 * \brief Initialize the DPOR exploration algorithm
46 static void MC_pre_modelcheck_safety()
48 if (_sg_mc_visited > 0)
49 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
51 mc_state_t initial_state = MC_state_new();
53 XBT_DEBUG("**************************************************");
54 XBT_DEBUG("Initial state");
56 /* Wait for requests (schedules processes) */
57 MC_wait_for_requests();
59 /* Get an enabled process and insert it in the interleave set of the initial state */
60 smx_process_t process;
61 MC_EACH_SIMIX_PROCESS(process,
62 if (MC_process_is_enabled(process)) {
63 MC_state_interleave_process(initial_state, process);
64 if (mc_reduce_kind != e_mc_reduce_none)
69 xbt_fifo_unshift(mc_stack, initial_state);
73 /** \brief Model-check the application using a DFS exploration
74 * with DPOR (Dynamic Partial Order Reductions)
76 void MC_modelcheck_safety(void)
78 MC_modelcheck_safety_init();
82 smx_simcall_t req = NULL;
83 mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
84 xbt_fifo_item_t item = NULL;
85 mc_visited_state_t visited_state = NULL;
87 while (xbt_fifo_size(mc_stack) > 0) {
89 /* Get current state */
90 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
92 XBT_DEBUG("**************************************************");
94 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
95 xbt_fifo_size(mc_stack), state, state->num,
96 MC_state_interleave_size(state), user_max_depth_reached);
98 /* Update statistics */
99 mc_stats->visited_states++;
101 /* If there are processes to interleave and the maximum depth has not been reached
102 then perform one step of the exploration algorithm */
103 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
104 && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
106 req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
107 XBT_DEBUG("Execute: %s", req_str);
110 if (dot_output != NULL) {
111 req_str = MC_request_get_dot_output(req, value);
114 MC_state_set_executed_request(state, req, value);
115 mc_stats->executed_transitions++;
117 // TODO, bundle both operations in a single message
118 // MC_execute_transition(req, value)
120 /* Answer the request */
121 MC_simcall_handle(req, value);
122 MC_wait_for_requests();
124 /* Create the new expanded state */
125 next_state = MC_state_new();
127 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
128 MC_show_non_termination();
129 exit(SIMGRID_EXIT_NON_TERMINATION);
132 if ((visited_state = is_visited_state(next_state)) == NULL) {
134 /* Get an enabled process and insert it in the interleave set of the next state */
135 smx_process_t process = NULL;
136 MC_EACH_SIMIX_PROCESS(process,
137 if (MC_process_is_enabled(process)) {
138 MC_state_interleave_process(next_state, process);
139 if (mc_reduce_kind != e_mc_reduce_none)
144 if (dot_output != NULL)
145 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
149 if (dot_output != NULL)
150 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
154 xbt_fifo_unshift(mc_stack, next_state);
156 if (dot_output != NULL)
159 /* Let's loop again */
161 /* The interleave set is empty or the maximum depth is reached, let's back-track */
164 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
166 if (user_max_depth_reached && visited_state == NULL)
167 XBT_DEBUG("User max depth reached !");
168 else if (visited_state == NULL)
169 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
171 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);
175 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
179 /* Trash the current state, no longer needed */
180 xbt_fifo_shift(mc_stack);
181 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
182 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
184 visited_state = NULL;
186 /* Check for deadlocks */
187 if (MC_deadlock_check()) {
188 MC_show_deadlock(NULL);
189 exit(SIMGRID_EXIT_DEADLOCK);
192 /* Traverse the stack backwards until a state with a non empty interleave
193 set is found, deleting all the states that have it empty in the way.
194 For each deleted state, check if the request that has generated it
195 (from it's predecesor state), depends on any other previous request
196 executed before it. If it does then add it to the interleave set of the
197 state that executed that previous request. */
199 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
200 if (mc_reduce_kind == e_mc_reduce_dpor) {
201 req = MC_state_get_internal_request(state);
202 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
203 xbt_die("Mutex is currently not supported with DPOR, "
204 "use --cfg=model-check/reduction:none");
205 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
206 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
207 if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
208 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
209 XBT_DEBUG("Dependent Transitions:");
210 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
211 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
212 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
214 prev_req = MC_state_get_executed_request(state, &value);
215 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
216 XBT_DEBUG("%s (state=%d)", req_str, state->num);
220 if (!MC_state_process_is_done(prev_state, issuer))
221 MC_state_interleave_process(prev_state, issuer);
223 XBT_DEBUG("Process %p is in done set", req->issuer);
227 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
229 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
234 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
235 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
236 req->call, issuer->pid, state->num,
237 MC_state_get_internal_request(prev_state)->call,
238 previous_issuer->pid,
245 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
246 /* We found a back-tracking point, let's loop */
247 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
248 xbt_fifo_unshift(mc_stack, state);
250 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
253 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
254 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
260 XBT_INFO("No property violation found.");
261 MC_print_statistics(mc_stats);
262 exit(SIMGRID_EXIT_SUCCESS);
265 static void MC_modelcheck_safety_init(void)
267 if(_sg_mc_termination)
268 mc_reduce_kind = e_mc_reduce_none;
269 else if (mc_reduce_kind == e_mc_reduce_unset)
270 mc_reduce_kind = e_mc_reduce_dpor;
272 if (_sg_mc_termination)
273 XBT_INFO("Check non progressive cycles");
275 XBT_INFO("Check a safety property");
276 MC_wait_for_requests();
278 XBT_DEBUG("Starting the safety algorithm");
282 /* Create exploration stack */
283 mc_stack = xbt_fifo_new();
285 MC_pre_modelcheck_safety();
287 /* Save the initial state */
288 initial_global_state = xbt_new0(s_mc_global_t, 1);
289 initial_global_state->snapshot = MC_take_snapshot(0);