- /* FIXME: the following rule assumes that the result of the
- * isend/irecv call is not stored in a buffer used in the
- * test call.*/
- /*if( (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
- && r1->call == SIMCALL_COMM_TEST)
- return FALSE; */
-
- if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND
- && simcall_comm_isend__get__rdv(r1) != simcall_comm_isend__get__rdv(r2))
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV
- && simcall_comm_irecv__get__rdv(r1) != simcall_comm_irecv__get__rdv(r2))
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_WAIT
- && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
- && (synchro1->comm.src_proc == NULL || synchro1->comm.dst_proc == NULL))
- return FALSE;
-
- if (r2->call == SIMCALL_COMM_WAIT
- && (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST)
- && (synchro2->comm.src_proc == NULL || synchro2->comm.dst_proc == NULL))
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
- && synchro1->comm.src_buff == synchro2->comm.src_buff
- && synchro2->comm.dst_buff == synchro2->comm.dst_buff)
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
- && synchro1->comm.src_buff != NULL
- && synchro1->comm.dst_buff != NULL
- && synchro2->comm.src_buff != NULL
- && synchro2->comm.dst_buff != NULL
- && synchro1->comm.dst_buff != synchro2->comm.src_buff
- && synchro1->comm.dst_buff != synchro2->comm.dst_buff
- && synchro2->comm.dst_buff != synchro1->comm.src_buff)
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_TEST &&
- (simcall_comm_test__get__comm(r1) == NULL
- || synchro1->comm.src_buff == NULL
- || synchro1->comm.dst_buff == NULL))
- return FALSE;
-
- if (r2->call == SIMCALL_COMM_TEST &&
- (simcall_comm_test__get__comm(r2) == NULL
- || synchro2->comm.src_buff == NULL
- || synchro2->comm.dst_buff == NULL))
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && synchro1->comm.src_buff == synchro2->comm.src_buff
- && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && synchro1->comm.src_buff == synchro2->comm.src_buff
- && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && synchro1->comm.src_buff != NULL
- && synchro1->comm.dst_buff != NULL
- && synchro2->comm.src_buff != NULL
- && synchro2->comm.dst_buff != NULL
- && synchro1->comm.dst_buff != synchro2->comm.src_buff
- && synchro1->comm.dst_buff != synchro2->comm.dst_buff
- && synchro2->comm.dst_buff != synchro1->comm.src_buff)
- return FALSE;
-
- if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && synchro1->comm.src_buff != NULL
- && synchro1->comm.dst_buff != NULL
- && synchro2->comm.src_buff != NULL
- && synchro2->comm.dst_buff != NULL
- && synchro1->comm.dst_buff != synchro2->comm.src_buff
- && synchro1->comm.dst_buff != synchro2->comm.dst_buff
- && synchro2->comm.dst_buff != synchro1->comm.src_buff)
- return FALSE;
-
- return TRUE;
+ if (r1->call_ == SIMCALL_COMM_WAIT && (r2->call_ == SIMCALL_COMM_WAIT || r2->call_ == SIMCALL_COMM_TEST) &&
+ (synchro1->src_actor_.get() == nullptr || synchro1->dst_actor_.get() == nullptr))
+ return false;
+
+ if (r1->call_ == SIMCALL_COMM_TEST &&
+ (simcall_comm_test__get__comm(r1) == nullptr || synchro1->src_buff_ == nullptr || synchro1->dst_buff_ == nullptr))
+ return false;
+
+ if (r1->call_ == SIMCALL_COMM_TEST && r2->call_ == SIMCALL_COMM_WAIT && synchro1->src_buff_ == synchro2->src_buff_ &&
+ synchro1->dst_buff_ == synchro2->dst_buff_)
+ return false;
+
+ if (r1->call_ == SIMCALL_COMM_WAIT && r2->call_ == SIMCALL_COMM_TEST && synchro1->src_buff_ != nullptr &&
+ synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr && synchro2->dst_buff_ != nullptr &&
+ synchro1->dst_buff_ != synchro2->src_buff_ && synchro1->dst_buff_ != synchro2->dst_buff_ &&
+ synchro2->dst_buff_ != synchro1->src_buff_)
+ return false;
+
+ return true;
+}
+
+// Those are internal_req
+bool request_depend(smx_simcall_t req1, smx_simcall_t req2)
+{
+ if (req1->issuer_ == req2->issuer_)
+ return false;
+
+ /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */
+ if ((req1->call_ == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) ||
+ (req2->call_ == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0))
+ return true;
+
+ if (req1->call_ != req2->call_)
+ return request_depend_asymmetric(req1, req2) && request_depend_asymmetric(req2, req1);
+
+ // Those are internal requests, we do not need indirection
+ // because those objects are copies:
+ simgrid::kernel::activity::CommImpl* synchro1 = MC_get_comm(req1);
+ simgrid::kernel::activity::CommImpl* synchro2 = MC_get_comm(req2);
+
+ switch (req1->call_) {
+ case SIMCALL_COMM_ISEND:
+ return simcall_comm_isend__get__mbox(req1) == simcall_comm_isend__get__mbox(req2);
+ case SIMCALL_COMM_IRECV:
+ return simcall_comm_irecv__get__mbox(req1) == simcall_comm_irecv__get__mbox(req2);
+ case SIMCALL_COMM_WAIT:
+ if (synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_)
+ return false;
+ if (synchro1->src_buff_ != nullptr && synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr &&
+ synchro2->dst_buff_ != nullptr && synchro1->dst_buff_ != synchro2->src_buff_ &&
+ synchro1->dst_buff_ != synchro2->dst_buff_ && synchro2->dst_buff_ != synchro1->src_buff_)
+ return false;
+ return true;
+ default:
+ return true;
+ }
+}
+
+}