Skip to content

Phase 6 of UDPOR Integration: Add `K`-partial alternatives computation + clean up phase

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

Overview

This MR introduces the computation of K-partial alternatives into the UnfoldingChecker. This is a big step forward in integrating UDPOR into SimGrid as the algorithm is effectively split into first a) figuring out how we can extend the current configuration and b) which among those possible extensions should be searched. The latter is determined through computing alternatives. Since computing alternatives has been proven to be NP-complete, the concept of partial alternatives, which sacrifices optimality in favor of computing "what should I do next?" in a polynomial amount of time, was implemented as described in "Quasi-Optimal DPOR" by Nguyen et al.

At this point, alternatives are computed without any specialized data structures (i.e. they are computed strictly using the unfolding and configuration at hand). More advanced techniques exist for programs that have a limited set of transitions (as discussed in "Quasi-Optimal DPOR"). This technique would have to be extended to all the transitions that SimGrid supports and would introduce quite a bit more complexity. We leave that as a future addition (or an exercise for the reader if some future reader is attempting to implement it now...)

Changes

The primary changes are to Configuration.cpp, Configuration_tests.cpp, and UnfoldingEvent.cpp:

  1. Computation of alternatives was moved into Configuration.cpp to allow for unit-testing. It's imperative that we compute alternatives properly since UDPOR is heavily reliant on their correctness. Note there are not currently tests for computing partial alternatives — only full alternatives are tested. We'd need to work out an example of the tree that should be searched by hand by something such as SDPOR to verify that things are truly working properly. For now, we test it a bit indirectly through the correctness of computing full alternatives (which is just a special case where you check all events of D).

  2. A walkthrough of each call made to Alt(C, D + {e}) in the example given in the UDPOR paper has been added to Configuration_tests.cpp which tests that alternatives are computed correctly at each step. There are 11 such calls as shown in the following diagram: examples

  3. The "clean up" phase (Remove(e, C, D) in the pseudocode) of UDPOR was implemented. There are some performance improvements I can see being made in the future (e.g. if we kept around what each event causes instead of only what each is caused by, we could eliminate all events in the Causes(D) right off the bat). For now, we add the implementation to match the pseudocode as closely as possible

  4. Checking for equality between two UnfoldingEvents was added. This will be more important in the next phase.

Note that there is currently no way to dynamically adjust between the optimal variant of UDPOR and the suboptimal variant using partial alternatives. It would be a trivial configuration parameter to UDPOR that could be exposed to end users in the future if desired.

Future Changes

  1. Although I originally planned to add in extension set computations before computing alternatives, I began working on alternatives first while getting a bit stuck attempting to compute the extension sets without knowledge of the specific transition. I have some more ideas on this front, but it looks like we're going to dive straight into writing the specialized functions for computing the extension sets.

  2. Afterwards, we'll need to do a little reorganizing with how we keep around states in the UnfoldingChecker to ensure the application-side always reflects what the checker believes is the current state. This shouldn't be difficult.

There are a couple of other steps here and there; but after we've added computations for ex(C), we'll be very close to something that works.

Hypothetical Future Changes

  1. I was thinking about adding a nice print-out of the Unfolding similar to what is done with git log --oneline --graph for debugging purposes. This would help enormously with debugging should UDPOR miss a trace and would make for some pretty pictures of event structures. It could be quite complicated though, so we'll have to weigh the benefits of doing this.

  2. Potentially we want to write an iterative version of UDPOR. This could also be difficult, although dpu works iteratively which could give us some inspiration.

Merge request reports