Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
3ed4e6ceb1a737d44b26e2407e20d406b51d46ac
[simgrid.git] / src / mc / mc_state.cpp
1 /* Copyright (c) 2008-2015. The SimGrid Team.
2  * All rights reserved.                                                     */
3
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. */
6
7 #include <assert.h>
8
9 #include <xbt/log.h>
10 #include <xbt/sysdep.h>
11
12 #include "src/simix/smx_private.h"
13 #include "src/mc/mc_state.h"
14 #include "src/mc/mc_request.h"
15 #include "src/mc/mc_private.h"
16 #include "src/mc/mc_comm_pattern.h"
17 #include "src/mc/mc_smx.h"
18 #include "src/mc/mc_xbt.hpp"
19
20 using simgrid::mc::remote;
21
22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
23                                 "Logging specific to MC (state)");
24
25 /**
26  * \brief Creates a state data structure used by the exploration algorithm
27  */
28 simgrid::mc::State* MC_state_new()
29 {
30   simgrid::mc::State* state = new simgrid::mc::State();
31   std::memset(&state->internal_comm, 0, sizeof(state->internal_comm));
32   std::memset(&state->internal_req, 0, sizeof(state->internal_req));
33   std::memset(&state->executed_req, 0, sizeof(state->executed_req));
34
35   state->max_pid = MC_smx_get_maxpid();
36   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
37   state->num = ++mc_stats->expanded_states;
38   /* Stateful model checking */
39   if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
40     state->system_state = simgrid::mc::take_snapshot(state->num);
41     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
42       MC_state_copy_incomplete_communications_pattern(state);
43       MC_state_copy_index_communications_pattern(state);
44     }
45   }
46   return state;
47 }
48
49 namespace simgrid {
50 namespace mc {
51
52 State::State()
53 {
54   std::memset(&this->internal_comm, 0, sizeof(this->internal_comm));
55   std::memset(&this->internal_req, 0, sizeof(this->internal_req));
56   std::memset(&this->executed_req, 0, sizeof(this->executed_req));
57 }
58
59 State::~State()
60 {
61   xbt_free(this->index_comm);
62   xbt_free(this->incomplete_comm_pattern);
63   xbt_free(this->proc_status);
64 }
65
66 }
67 }
68
69 void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process)
70 {
71   assert(state);
72   state->proc_status[process->pid].state = MC_INTERLEAVE;
73   state->proc_status[process->pid].interleave_count = 0;
74 }
75
76 void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process)
77 {
78   if (state->proc_status[process->pid].state == MC_INTERLEAVE)
79     state->proc_status[process->pid].state = MC_DONE;
80 }
81
82 unsigned int MC_state_interleave_size(simgrid::mc::State* state)
83 {
84   unsigned int i, size = 0;
85   for (i = 0; i < state->max_pid; i++)
86     if ((state->proc_status[i].state == MC_INTERLEAVE)
87         || (state->proc_status[i].state == MC_MORE_INTERLEAVE))
88       size++;
89   return size;
90 }
91
92 int MC_state_process_is_done(simgrid::mc::State* state, smx_process_t process)
93 {
94   return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE;
95 }
96
97 void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req,
98                                    int value)
99 {
100   state->executed_req = *req;
101   state->req_num = value;
102
103   /* The waitany and testany request are transformed into a wait or test request over the
104    * corresponding communication action so it can be treated later by the dependence
105    * function. */
106   switch (req->call) {
107   case SIMCALL_COMM_WAITANY: {
108     state->internal_req.call = SIMCALL_COMM_WAIT;
109     state->internal_req.issuer = req->issuer;
110     smx_synchro_t remote_comm;
111     read_element(mc_model_checker->process(),
112       &remote_comm, remote(simcall_comm_waitany__get__comms(req)),
113       value, sizeof(remote_comm));
114     mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
115     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
116     simcall_comm_wait__set__timeout(&state->internal_req, 0);
117     break;
118   }
119
120   case SIMCALL_COMM_TESTANY:
121     state->internal_req.call = SIMCALL_COMM_TEST;
122     state->internal_req.issuer = req->issuer;
123
124     if (value > 0) {
125       smx_synchro_t remote_comm;
126       read_element(mc_model_checker->process(),
127         &remote_comm, remote(simcall_comm_testany__get__comms(req)),
128         value, sizeof(remote_comm));
129       mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
130     }
131
132     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
133     simcall_comm_test__set__result(&state->internal_req, value);
134     break;
135
136   case SIMCALL_COMM_WAIT:
137     state->internal_req = *req;
138     mc_model_checker->process().read_bytes(&state->internal_comm ,
139       sizeof(state->internal_comm), remote(simcall_comm_wait__get__comm(req)));
140     simcall_comm_wait__set__comm(&state->executed_req, &state->internal_comm);
141     simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
142     break;
143
144   case SIMCALL_COMM_TEST:
145     state->internal_req = *req;
146     mc_model_checker->process().read_bytes(&state->internal_comm,
147       sizeof(state->internal_comm), remote(simcall_comm_test__get__comm(req)));
148     simcall_comm_test__set__comm(&state->executed_req, &state->internal_comm);
149     simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
150     break;
151
152   case SIMCALL_MC_RANDOM: {
153     state->internal_req = *req;
154     int random_max = simcall_mc_random__get__max(req);
155     if (value != random_max)
156       for (auto& p : mc_model_checker->process().simix_processes()) {
157         mc_procstate_t procstate = &state->proc_status[p.copy.pid];
158         const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
159         if (p.copy.pid == issuer->pid) {
160           procstate->state = MC_MORE_INTERLEAVE;
161           break;
162         }
163       }
164     break;
165   }
166
167   default:
168     state->internal_req = *req;
169     break;
170   }
171 }
172
173 smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value)
174 {
175   *value = state->req_num;
176   return &state->executed_req;
177 }
178
179 smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state)
180 {
181   return &state->internal_req;
182 }
183
184 static inline smx_simcall_t MC_state_get_request_for_process(
185   simgrid::mc::State* state, int*value, smx_process_t process)
186 {
187   mc_procstate_t procstate = &state->proc_status[process->pid];
188
189   if (procstate->state != MC_INTERLEAVE
190       && procstate->state != MC_MORE_INTERLEAVE)
191       return nullptr;
192   if (!simgrid::mc::process_is_enabled(process))
193     return nullptr;
194
195   switch (process->simcall.call) {
196
197       case SIMCALL_COMM_WAITANY:
198         *value = -1;
199         while (procstate->interleave_count <
200               read_length(mc_model_checker->process(),
201                 remote(simcall_comm_waitany__get__comms(&process->simcall)))) {
202           if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
203               procstate->interleave_count++)) {
204             *value = procstate->interleave_count - 1;
205             break;
206           }
207         }
208
209         if (procstate->interleave_count >=
210             simgrid::mc::read_length(mc_model_checker->process(),
211               simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))
212           procstate->state = MC_DONE;
213
214         if (*value != -1)
215           return &process->simcall;
216
217         break;
218
219       case SIMCALL_COMM_TESTANY: {
220         unsigned start_count = procstate->interleave_count;
221         *value = -1;
222         while (procstate->interleave_count <
223                 read_length(mc_model_checker->process(),
224                   remote(simcall_comm_testany__get__comms(&process->simcall))))
225           if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
226               procstate->interleave_count++)) {
227             *value = procstate->interleave_count - 1;
228             break;
229           }
230
231         if (procstate->interleave_count >=
232             read_length(mc_model_checker->process(),
233               remote(simcall_comm_testany__get__comms(&process->simcall))))
234           procstate->state = MC_DONE;
235
236         if (*value != -1 || start_count == 0)
237           return &process->simcall;
238
239         break;
240       }
241
242       case SIMCALL_COMM_WAIT: {
243         smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
244         s_smx_synchro_t act;
245         mc_model_checker->process().read_bytes(
246           &act, sizeof(act), remote(remote_act));
247         if (act.comm.src_proc && act.comm.dst_proc)
248           *value = 0;
249         else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
250               && act.comm.detached == 1)
251           *value = 0;
252         else
253           *value = -1;
254         procstate->state = MC_DONE;
255         return &process->simcall;
256       }
257
258       case SIMCALL_MC_RANDOM:
259         if (procstate->state == MC_INTERLEAVE)
260           *value = simcall_mc_random__get__min(&process->simcall);
261         else if (state->req_num < simcall_mc_random__get__max(&process->simcall))
262           *value = state->req_num + 1;
263         procstate->state = MC_DONE;
264         return &process->simcall;
265
266       default:
267         procstate->state = MC_DONE;
268         *value = 0;
269         return &process->simcall;
270   }
271   return nullptr;
272 }
273
274 smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value)
275 {
276   for (auto& p : mc_model_checker->process().simix_processes()) {
277     smx_simcall_t res = MC_state_get_request_for_process(state, value, &p.copy);
278     if (res)
279       return res;
280   }
281   return nullptr;
282 }