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. */
12 #include <xbt/dynar.h>
14 #include <xbt/sysdep.h>
16 #include "src/mc/mc_state.h"
17 #include "src/mc/mc_request.h"
18 #include "src/mc/mc_safety.h"
19 #include "src/mc/mc_private.h"
20 #include "src/mc/mc_record.h"
21 #include "src/mc/mc_smx.h"
22 #include "src/mc/mc_client.h"
23 #include "src/mc/mc_exit.h"
25 #include "src/xbt/mmalloc/mmprivate.h"
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
30 "Logging specific to MC safety verification ");
34 static int is_exploration_stack_state(mc_state_t current_state){
37 mc_state_t stack_state;
38 for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
39 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
40 if(snapshot_compare(stack_state, current_state) == 0){
41 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
48 static void MC_modelcheck_safety_init(void);
51 * \brief Initialize the DPOR exploration algorithm
53 static void MC_pre_modelcheck_safety()
55 if (_sg_mc_visited > 0)
56 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
58 mc_state_t initial_state = MC_state_new();
60 XBT_DEBUG("**************************************************");
61 XBT_DEBUG("Initial state");
63 /* Wait for requests (schedules processes) */
64 mc_model_checker->wait_for_requests();
66 /* Get an enabled process and insert it in the interleave set of the initial state */
67 for (auto& p : mc_model_checker->process().simix_processes())
68 if (MC_process_is_enabled(&p.copy)) {
69 MC_state_interleave_process(initial_state, &p.copy);
70 if (mc_reduce_kind != e_mc_reduce_none)
74 xbt_fifo_unshift(mc_stack, initial_state);
78 /** \brief Model-check the application using a DFS exploration
79 * with DPOR (Dynamic Partial Order Reductions)
81 int MC_modelcheck_safety(void)
83 MC_modelcheck_safety_init();
85 char *req_str = nullptr;
87 smx_simcall_t req = nullptr;
88 mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
89 xbt_fifo_item_t item = nullptr;
90 mc_visited_state_t visited_state = nullptr;
92 while (xbt_fifo_size(mc_stack) > 0) {
94 /* Get current state */
95 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
97 XBT_DEBUG("**************************************************");
99 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
100 xbt_fifo_size(mc_stack), state, state->num,
101 MC_state_interleave_size(state), user_max_depth_reached);
103 /* Update statistics */
104 mc_stats->visited_states++;
106 /* If there are processes to interleave and the maximum depth has not been reached
107 then perform one step of the exploration algorithm */
108 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
109 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
111 req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
112 XBT_DEBUG("Execute: %s", req_str);
115 if (dot_output != nullptr) {
116 req_str = MC_request_get_dot_output(req, value);
119 MC_state_set_executed_request(state, req, value);
120 mc_stats->executed_transitions++;
122 // TODO, bundle both operations in a single message
123 // MC_execute_transition(req, value)
125 /* Answer the request */
126 MC_simcall_handle(req, value);
127 mc_model_checker->wait_for_requests();
129 /* Create the new expanded state */
130 next_state = MC_state_new();
132 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
133 MC_show_non_termination();
134 return SIMGRID_MC_EXIT_NON_TERMINATION;
137 if ((visited_state = is_visited_state(next_state)) == nullptr) {
139 /* Get an enabled process and insert it in the interleave set of the next state */
140 for (auto& p : mc_model_checker->process().simix_processes())
141 if (MC_process_is_enabled(&p.copy)) {
142 MC_state_interleave_process(next_state, &p.copy);
143 if (mc_reduce_kind != e_mc_reduce_none)
147 if (dot_output != nullptr)
148 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
152 if (dot_output != nullptr)
153 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
157 xbt_fifo_unshift(mc_stack, next_state);
159 if (dot_output != nullptr)
162 /* Let's loop again */
164 /* The interleave set is empty or the maximum depth is reached, let's back-track */
167 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
169 if (user_max_depth_reached && visited_state == nullptr)
170 XBT_DEBUG("User max depth reached !");
171 else if (visited_state == nullptr)
172 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
174 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);
178 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
182 /* Trash the current state, no longer needed */
183 xbt_fifo_shift(mc_stack);
184 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
185 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
187 visited_state = nullptr;
189 /* Check for deadlocks */
190 if (MC_deadlock_check()) {
191 MC_show_deadlock(nullptr);
192 return SIMGRID_MC_EXIT_DEADLOCK;
195 /* Traverse the stack backwards until a state with a non empty interleave
196 set is found, deleting all the states that have it empty in the way.
197 For each deleted state, check if the request that has generated it
198 (from it's predecesor state), depends on any other previous request
199 executed before it. If it does then add it to the interleave set of the
200 state that executed that previous request. */
202 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
203 if (mc_reduce_kind == e_mc_reduce_dpor) {
204 req = MC_state_get_internal_request(state);
205 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
206 xbt_die("Mutex is currently not supported with DPOR, "
207 "use --cfg=model-check/reduction:none");
208 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
209 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
210 if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
211 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
212 XBT_DEBUG("Dependent Transitions:");
213 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
214 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
215 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
217 prev_req = MC_state_get_executed_request(state, &value);
218 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
219 XBT_DEBUG("%s (state=%d)", req_str, state->num);
223 if (!MC_state_process_is_done(prev_state, issuer))
224 MC_state_interleave_process(prev_state, issuer);
226 XBT_DEBUG("Process %p is in done set", req->issuer);
230 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
232 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
237 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
238 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
239 req->call, issuer->pid, state->num,
240 MC_state_get_internal_request(prev_state)->call,
241 previous_issuer->pid,
248 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
249 /* We found a back-tracking point, let's loop */
250 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
251 xbt_fifo_unshift(mc_stack, state);
253 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
256 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
257 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
263 XBT_INFO("No property violation found.");
264 MC_print_statistics(mc_stats);
265 return SIMGRID_MC_EXIT_SUCCESS;
268 static void MC_modelcheck_safety_init(void)
270 if(_sg_mc_termination)
271 mc_reduce_kind = e_mc_reduce_none;
272 else if (mc_reduce_kind == e_mc_reduce_unset)
273 mc_reduce_kind = e_mc_reduce_dpor;
275 if (_sg_mc_termination)
276 XBT_INFO("Check non progressive cycles");
278 XBT_INFO("Check a safety property");
279 mc_model_checker->wait_for_requests();
281 XBT_DEBUG("Starting the safety algorithm");
285 /* Create exploration stack */
286 mc_stack = xbt_fifo_new();
288 MC_pre_modelcheck_safety();
290 /* Save the initial state */
291 initial_global_state = xbt_new0(s_mc_global_t, 1);
292 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);