Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix a MC serialization bug around WaitAny
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 2 Jul 2023 13:29:04 +0000 (15:29 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 2 Jul 2023 13:37:37 +0000 (15:37 +0200)
commita41a7f329f4931c404907ccf78a390b274780275
tree53d58b9ffa8db9384dea28f6dc13e8f87d8074c7
parent989e6d7e4cb105760aff9acce9ac2d26de2f793d
Fix a MC serialization bug around WaitAny

The individual wait activities that are embeeded in a WaitAny or
TestAny do not have any call_location associated, as the call_location
is associated to the observer, not the activity. The previous code was
thus not serializing the call location of all those activities while
serializing them, but it's a pity because the Checker code deserialize
these call_location in any case. This was resulting in the beginning
of the next transition to be used as location, naturally breaking the
deserialization afterward.

Instead, the call location of the TestAny or WaitAny is now used for
each and every wait activities embedded in the *Any call. This may
challenge the MC implementation, but it sounds like a sensible idea:
In such case, the location of the embedded wait IS the one of the
englobing TestAny or WaitAny call.

In some sense, that's very close to how we handle the timeout that is
given by the englobing call, not the embedded ones, in such situation.
src/kernel/actor/CommObserver.cpp
src/mc/transition/TransitionAny.cpp
src/mc/transition/TransitionComm.cpp