Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of github.com:simgrid/simgrid into dev_11
[simgrid.git] / src / mc / checker / CommunicationDeterminismChecker.hpp
1 /* Copyright (c) 2016-2020. The SimGrid Team. All rights reserved.          */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "src/mc/VisitedState.hpp"
7 #include "src/mc/checker/Checker.hpp"
8 #include "src/mc/mc_comm_pattern.hpp"
9
10 #include <string>
11 #include <vector>
12
13 #ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
14 #define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
15
16 namespace simgrid {
17 namespace mc {
18
19 class XBT_PRIVATE CommunicationDeterminismChecker : public Checker {
20 public:
21   explicit CommunicationDeterminismChecker(Session& session);
22   ~CommunicationDeterminismChecker() override;
23   void run() override;
24   RecordTrace get_record_trace() override;
25   std::vector<std::string> get_textual_trace() override;
26
27 private:
28   void prepare();
29   void real_run();
30   void log_state() override;
31   void deterministic_comm_pattern(int process, const PatternCommunication* comm, int backtracking);
32   void restoreState();
33
34 public:
35   // These are used by functions which should be moved in CommunicationDeterminismChecker:
36   void get_comm_pattern(smx_simcall_t request, CallType call_type, int backtracking);
37   void complete_comm_pattern(RemotePtr<kernel::activity::CommImpl> comm_addr, unsigned int issuer, int backtracking);
38
39 private:
40   /** Stack representing the position in the exploration graph */
41   std::list<std::unique_ptr<State>> stack_;
42   VisitedStates visited_states_;
43   unsigned long expanded_states_count_ = 0;
44
45   bool initial_communications_pattern_done = false;
46   bool recv_deterministic                  = true;
47   bool send_deterministic                  = true;
48   char *send_diff = nullptr;
49   char *recv_diff = nullptr;
50 };
51 } // namespace mc
52 } // namespace simgrid
53
54 #endif
55