Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of github.com:simgrid/simgrid into dev_11
authorEhsan Azimi <eazimi@ehsan.irisa.fr>
Thu, 26 Nov 2020 08:46:43 +0000 (09:46 +0100)
committerEhsan Azimi <eazimi@ehsan.irisa.fr>
Thu, 26 Nov 2020 08:46:43 +0000 (09:46 +0100)
1  2 
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp
src/mc/mc_base.cpp
src/mc/mc_state.cpp
src/mc/mc_state.hpp

@@@ -171,20 -171,19 +173,19 @@@ void CommunicationDeterminismChecker::d
  
  /********** Non Static functions ***********/
  
- void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_mc_call_type_t call_type,
-                                                        int backtracking)
+ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, CallType call_type, int backtracking)
  {
 -  const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
 +  const smx_actor_t issuer = mcapi::get().mc_smx_simcall_get_issuer(request);
    const mc::PatternCommunicationList& initial_pattern          = initial_communications_pattern[issuer->get_pid()];
    const std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer->get_pid()];
  
    auto pattern   = std::make_unique<PatternCommunication>();
    pattern->index = initial_pattern.index_comm + incomplete_pattern.size();
  
-   if (call_type == MC_CALL_TYPE_SEND) {
+   if (call_type == CallType::SEND) {
      /* Create comm pattern */
      pattern->type      = PatternCommunicationType::send;
 -    pattern->comm_addr = static_cast<kernel::activity::CommImpl*>(simcall_comm_isend__getraw__result(request));
 +    pattern->comm_addr = mcapi::get().get_pattern_comm_addr(request);
  
      Remote<kernel::activity::CommImpl> temp_synchro;
      mc_model_checker->get_remote_simulation().read(temp_synchro, remote(pattern->comm_addr));
@@@ -404,14 -394,14 +404,14 @@@ void CommunicationDeterminismChecker::r
      smx_simcall_t req        = &issuer->simcall_;
  
      /* TODO : handle test and testany simcalls */
-     e_mc_call_type_t call = MC_get_call_type(req);
-     mcapi::get().handle_simcall(state->transition_);
+     CallType call = MC_get_call_type(req);
+     mc_model_checker->handle_simcall(state->transition_);
      MC_handle_comm_pattern(call, req, req_num, 1);
 -    mc_model_checker->wait_for_requests();
 +    mcapi::get().mc_wait_for_requests();
  
      /* Update statistics */
 -    mc_model_checker->visited_states++;
 -    mc_model_checker->executed_transitions++;
 +    mcapi::get().mc_inc_visited_states();
 +    mcapi::get().mc_inc_executed_trans();
    }
  }
  
@@@ -443,12 -433,12 +443,12 @@@ void CommunicationDeterminismChecker::r
  
        std::string req_str;
        if (dot_output != nullptr)
 -        req_str = request_get_dot_output(req, req_num);
 +        req_str = mcapi::get().request_get_dot_output(req, req_num);
  
 -      mc_model_checker->executed_transitions++;
 +      mcapi::get().mc_inc_executed_trans();
  
        /* TODO : handle test and testany simcalls */
-       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
+       CallType call = CallType::NONE;
        if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
          call = MC_get_call_type(req);
  
Simple merge
@@@ -197,13 -191,13 +196,13 @@@ void SafetyChecker::backtrack(
      stack_.pop_back();
      if (reductionMode_ == ReductionMode::dpor) {
        smx_simcall_t req = &state->internal_req_;
-       if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
+       if (req->call_ == simix::Simcall::MUTEX_LOCK || req->call_ == simix::Simcall::MUTEX_TRYLOCK)
          xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
  
 -      const kernel::actor::ActorImpl* issuer = MC_smx_simcall_get_issuer(req);
 +      const kernel::actor::ActorImpl* issuer = mcapi::get().mc_smx_simcall_get_issuer(req);
        for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
          State* prev_state = i->get();
 -        if (request_depend(req, &prev_state->internal_req_)) {
 +        if (mcapi::get().request_depend(req, &prev_state->internal_req_)) {
            if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
              XBT_DEBUG("Dependent Transitions:");
              int value              = prev_state->transition_.argument_;
Simple merge
Simple merge
Simple merge