Skip to content

Phase 5 of UDPOR Integration: Implementing Conflict Checks

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

Overview

This MR adds the ability to determine conflicts and immediate conflicts between events from an unfolding. The MR also fills in more of the UnfoldingChecker's implementation in preparation for the next phase (which is to determine when some action is enabled at a configuration config(K) for some maximal set K)

Changes

The changes can be summarized as follows:

  1. Several methods were implemented for UnfoldingEvent, most importantly UnfoldingEvent::conflicts_with(const UnfoldingEvent *) and UnfoldingEvent::immediately_conflicts_with(const UnfoldingEvent *). Another important method, UnfoldingEvent::conflicts_with(const Configuration&), was also implemented that is used to preserve the invariant that a configuration is conflict-free. Prior to this MR, we only enforced that configurations be causally closed.
  2. Most of the important parts for computing the extension set using brute force were added to UnfoldingChecker. What's missing is the computation of the (albeit important) condition which decides whether some action is enabled at a configuration config(K) for some maximal set of events K of configuration C.
  3. The maximal_subsets_iterator now has a parameter that can limit the size of the subsets that are visited in the search. This would be useful when determining conflicts; for now, we stick with variable_for_loop for simplicity, but the code is there for the future.

Note: A large portion of the diff can be attributed to the changes made in the the unit test files

Future Changes

What remains is at the same time a lot of work and not a lot of work. The phases thus far have laid the "foundation" that we will quickly begin to build off of as more parts of UDPOR are implemented. At this point, we must

  1. determine when two events are semantically equivalent (==)
  2. compute K-partial alternatives as outlined in the paper "Quasi-Optimal UDPOR"
  3. compute the set Q_CD which determines which events need to stay
  4. regenerate states (almost trivial: we can use the same code from DFSExplorer)
  5. potentially add state equivalence checks to UDPOR to allow search over cyclic state spaces as described in section 5 of the UDPOR paper (would be difficult and would be added in as a last step)
  6. add more unit tests for everything

It's actually quite manageable, and sooner rather than later a "rough draft" of UDPOR will exist in SimGrid.

Merge request reports