Skip to content

Phase 7 of UDPOR Integration: Add specialized `ex(C)` computation for `Comm*` transitions

Maxwell Pirtle requested to merge maxwellpirtle/simgrid:udpor-phase7 into master

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:

  1. 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 current Unfolding. Fortunately, we can perform this update “on the fly”: after extending the current configuration C under consideration of UDPOR with an event e, only the transition associated with e’s need be updated. The justification follows from the fact that for any actor A, there can exist at most one event whose associated transition is the jth action taken by that actor. In other words, we know that e and e alone is the event that must be updated.
  2. The UdporChecker now maintains a stack of states that it has visited in favor of only the current state of the configuration stateC. This is needed to allow UDPOR to regenerate a prior state of the AppSide 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 in DFSExplorer.
  3. 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 sets U and G maintained by UDPOR. This change goes in tandem with that of the clean up phase of UDPOR (namely Remove(e, C, D) in the pseudocode).
  4. Two bugs were fixed in other important methods used by UDPOR, viz. a) checking for compatibility (Configuration::is_compatible_with() and UnfoldingEvent::conflicts_with_any()) which is used when computing alternatives, and b) checking for the immediate conflicts of some event e 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.

Merge request reports