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);
118 MC_state_set_executed_request(state, req, value);
119 mc_stats->executed_transitions++;
121 // TODO, bundle both operations in a single message
122 // MC_execute_transition(req, value)
124 /* Answer the request */
125 MC_simcall_handle(req, value);
126 mc_model_checker->wait_for_requests();
128 /* Create the new expanded state */
129 next_state = MC_state_new();
131 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
132 MC_show_non_termination();
133 return SIMGRID_MC_EXIT_NON_TERMINATION;
136 if ((visited_state = is_visited_state(next_state)) == nullptr) {
138 /* Get an enabled process and insert it in the interleave set of the next state */
139 for (auto& p : mc_model_checker->process().simix_processes())
140 if (MC_process_is_enabled(&p.copy)) {
141 MC_state_interleave_process(next_state, &p.copy);
142 if (mc_reduce_kind != e_mc_reduce_none)
146 if (dot_output != nullptr)
147 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
149 } else if (dot_output != nullptr)
150 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
153 xbt_fifo_unshift(mc_stack, next_state);
155 if (dot_output != nullptr)
158 /* Let's loop again */
160 /* The interleave set is empty or the maximum depth is reached, let's back-track */
163 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
165 if (user_max_depth_reached && visited_state == nullptr)
166 XBT_DEBUG("User max depth reached !");
167 else if (visited_state == nullptr)
168 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
170 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);
173 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
175 /* Trash the current state, no longer needed */
176 xbt_fifo_shift(mc_stack);
177 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
178 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
180 visited_state = nullptr;
182 /* Check for deadlocks */
183 if (MC_deadlock_check()) {
184 MC_show_deadlock(nullptr);
185 return SIMGRID_MC_EXIT_DEADLOCK;
188 /* Traverse the stack backwards until a state with a non empty interleave
189 set is found, deleting all the states that have it empty in the way.
190 For each deleted state, check if the request that has generated it
191 (from it's predecesor state), depends on any other previous request
192 executed before it. If it does then add it to the interleave set of the
193 state that executed that previous request. */
195 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
196 if (mc_reduce_kind == e_mc_reduce_dpor) {
197 req = MC_state_get_internal_request(state);
198 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
199 xbt_die("Mutex is currently not supported with DPOR, "
200 "use --cfg=model-check/reduction:none");
201 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
202 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
203 if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
204 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
205 XBT_DEBUG("Dependent Transitions:");
206 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
207 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
208 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
210 prev_req = MC_state_get_executed_request(state, &value);
211 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
212 XBT_DEBUG("%s (state=%d)", req_str, state->num);
216 if (!MC_state_process_is_done(prev_state, issuer))
217 MC_state_interleave_process(prev_state, issuer);
219 XBT_DEBUG("Process %p is in done set", req->issuer);
223 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
225 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
230 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
231 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
232 req->call, issuer->pid, state->num,
233 MC_state_get_internal_request(prev_state)->call,
234 previous_issuer->pid,
241 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
242 /* We found a back-tracking point, let's loop */
243 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
244 xbt_fifo_unshift(mc_stack, state);
246 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
249 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
250 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
256 XBT_INFO("No property violation found.");
257 MC_print_statistics(mc_stats);
258 return SIMGRID_MC_EXIT_SUCCESS;
261 static void MC_modelcheck_safety_init(void)
263 if(_sg_mc_termination)
264 mc_reduce_kind = e_mc_reduce_none;
265 else if (mc_reduce_kind == e_mc_reduce_unset)
266 mc_reduce_kind = e_mc_reduce_dpor;
268 if (_sg_mc_termination)
269 XBT_INFO("Check non progressive cycles");
271 XBT_INFO("Check a safety property");
272 mc_model_checker->wait_for_requests();
274 XBT_DEBUG("Starting the safety algorithm");
278 /* Create exploration stack */
279 mc_stack = xbt_fifo_new();
281 MC_pre_modelcheck_safety();
283 /* Save the initial state */
284 initial_global_state = xbt_new0(s_mc_global_t, 1);
285 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);