Phase 5 of UDPOR Integration: Implementing Conflict Checks
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:
- Several methods were implemented for
UnfoldingEvent
, most importantlyUnfoldingEvent::conflicts_with(const UnfoldingEvent *)
andUnfoldingEvent::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. - 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 configurationconfig(K)
for some maximal set of eventsK
of configurationC
. - 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 withvariable_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
- determine when two events are semantically equivalent (
==
) - compute K-partial alternatives as outlined in the paper "Quasi-Optimal UDPOR"
- compute the set
Q_CD
which determines which events need to stay - regenerate states (almost trivial: we can use the same code from
DFSExplorer
) - 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)
- 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.