Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : fix (again ..) DPOR for iSend/iRecv and Wait communications
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 13 Jun 2013 07:21:52 +0000 (09:21 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 13 Jun 2013 09:49:41 +0000 (11:49 +0200)
commit0f40cfec58fb170c3378cc63e83cb0a878552970
treef13193b8683d9137292e88370d06cd6ab0c3fecf
parent4d6e2bb1c86ba6092fc69e61582c223100ee98a9
model-checker : fix (again ..) DPOR for iSend/iRecv and Wait communications

- add rdv_cpy in s_smx_action_t structure. comm.rdv is used for
  garbage collection and set to NULL when the communication matches
  with another communication already pushed and waiting in the
  mailbox.
- iSend/iRecv and Wait communications are independant if the
  communications are not in the same mailbox. Otherwise, the
  iSend/iRecv communication process issuer must be different of the
  src_proc or dst_proc of the Wait communication, or, src_buff and
  dst_buff of the communications must be different.
src/mc/mc_request.c
src/simix/smx_network.c
src/simix/smx_private.h