Phase 7 of UDPOR Integration: Add specialized `ex(C)` computation for `Comm*` transitions
Overview:
This PR introduces the specialized functions for computing extension sets of ex(C)
for the CommSend
, CommRecv
, and CommWait
transitions. This allows for UDPOR to be used against the simple examples that already exist in SimGrid and against which SimGrid’s DPOR implementation is tested. UDPOR should identify bugs in each of the programs for which it is known a bug exists. At the moment, though, UDPOR does not identify the bug in the example mc-bugged2
. Discovering why will take some time; and since the MR is already rather large, a fix should be introduced in a separate MR anyway.
Changes
The following changes are of primary concern:
- The method
simgrid::mc::State::execute_next()
now also returns a handle to the transition which executed containing the latest information about the action that was taken. This is important since UDPOR creates events and associates transitions to those events before they have executed and received any additional context. Once the transitions have executed, though, more information may have potentially been associated with them, and this must be reflected in events in the currentUnfolding
. Fortunately, we can perform this update “on the fly”: after extending the current configurationC
under consideration of UDPOR with an evente
, only the transition associated withe
’s need be updated. The justification follows from the fact that for any actorA
, there can exist at most one event whose associated transition is thej
th action taken by that actor. In other words, we know thate
ande
alone is the event that must be updated. - The
UdporChecker
now maintains a stack of states that it has visited in favor of only the current state of the configurationstateC
. This is needed to allow UDPOR to regenerate a prior state of theAppSide
before exploring an alternative. With an iterative version of UDPOR, the stack could be moved into a local variable theoretically. The functionality is very close to that which exists inDFSExplorer
. - The
Unfolding
now preserves all events that are added to it in favor of removing events permanently. Instead, it now performs some minor bookkeeping moving events between the two global setsU
andG
maintained by UDPOR. This change goes in tandem with that of the clean up phase of UDPOR (namelyRemove(e, C, D)
in the pseudocode). - Two bugs were fixed in other important methods used by UDPOR, viz. a) checking for compatibility (
Configuration::is_compatible_with()
andUnfoldingEvent::conflicts_with_any()
) which is used when computing alternatives, and b) checking for the immediate conflicts of some evente
in an unfolding (Unfolding::get_immediate_conflicts_of()
).
There is a still a long way to go before we’d have a functional version of UDPOR integrated into SimGrid, but this is a big step forward.