Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Clarify that the issuer for a CommWait() action is that of the same actor
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Mon, 3 Apr 2023 09:42:38 +0000 (11:42 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Wed, 5 Apr 2023 08:39:59 +0000 (10:39 +0200)
commit8f411032939a18552d34cf9cf2398838ab5f12a0
tree193bdf174bb2bc2ad366754ecb7218f51d25356d
parent1a43705d13b6418986f3c87317b2ddf92c5c60fe
Clarify that the issuer for a CommWait() action is that of the same actor

The `CommWait()` transition, in the manner that SimGrid
handles communications, can be said to be "issued" by either
the sender or the receiver that are a part of the communication
under consideration. We favor that which is run by the same actor;
indeed, we require it as this point unless otherwise noted.

If it is possible for a `CommWait` to wait on a communication
whose identity cannot be traced back to an event that already
executed by the same actor, the model would have to change
when computing extension sets for CommWait(), specifically
when checking whether or not that transition is enabled
at a prior state
src/mc/explo/UdporChecker.cpp
src/mc/explo/udpor/EventSet.hpp
src/mc/explo/udpor/ExtensionSetCalculator.cpp