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"
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 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
203 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
204 if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
205 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
206 XBT_DEBUG("Dependent Transitions:");
207 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
208 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
209 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
211 prev_req = MC_state_get_executed_request(state, &value);
212 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
213 XBT_DEBUG("%s (state=%d)", req_str, state->num);
217 if (!MC_state_process_is_done(prev_state, issuer))
218 MC_state_interleave_process(prev_state, issuer);
220 XBT_DEBUG("Process %p is in done set", req->issuer);
224 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
226 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
231 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
232 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
233 req->call, issuer->pid, state->num,
234 MC_state_get_internal_request(prev_state)->call,
235 previous_issuer->pid,
242 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
243 /* We found a back-tracking point, let's loop */
244 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
245 xbt_fifo_unshift(mc_stack, state);
247 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
250 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
251 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
257 XBT_INFO("No property violation found.");
258 MC_print_statistics(mc_stats);
259 exit(SIMGRID_EXIT_SUCCESS);
262 static void MC_modelcheck_safety_init(void)
264 if(_sg_mc_termination)
265 mc_reduce_kind = e_mc_reduce_none;
266 else if (mc_reduce_kind == e_mc_reduce_unset)
267 mc_reduce_kind = e_mc_reduce_dpor;
269 if (_sg_mc_termination)
270 XBT_INFO("Check non progressive cycles");
272 XBT_INFO("Check a safety property");
273 MC_wait_for_requests();
275 XBT_DEBUG("Starting the safety algorithm");
279 /* Create exploration stack */
280 mc_stack = xbt_fifo_new();
282 MC_pre_modelcheck_safety();
284 /* Save the initial state */
285 initial_global_state = xbt_new0(s_mc_global_t, 1);
286 initial_global_state->snapshot = MC_take_snapshot(0);