Skip to content

Phase 1 of Integration of UDPOR: Adding UDPOR Constructs

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

Overview

This is the first of three or four (or perhaps more) PRs to come which will introduce an implementation of UDPOR into SimGrid. The first phase is to add all of the constructs that will be used by UDPOR and to test them heavily. The principle additions are as follows (note that some are not yet in existence):

  1. The Unfolding is the owner of all the events that UDPOR encounters and keeps alive. Each UdporChecker instance holds an instance of and Unfolding which it uses while exploring the event structure. UDPOR manipulates the Unfolding so as to guarantee that references to events that the Unfolding maintains are always valid.
  2. Events that are discovered in the unfolding are represented with the UnfoldingEvent class. Each UnfoldingEvent maintains the transition that UDPOR associates with it (which is important in future phases of UDPOR integration) as well as all of its immediate causes (viz. events such that if e' is an immediate cause of e, there is no event e'' where e causes e'' and e'' causes e'). It is sufficient to store the immediate causes since this implicitly stores the entire history with the event
  3. An EventSet is simple a set of events with some convenience methods.
  4. A Configuration is almost an EventSet, but it contains some convenience methods and maintains some extra information about the events in the collection.
  5. A History of a set of events is an "un-expanded" version of the events in the entire history. The History class contains convenience methods for determining e.g. whether an event is in the joined history of a set of events. The History will be more important with the implementation of K-partial alternatives in phase 3

Changes

Although the size of the diff is large, it should be noted that a large part of the diff can be attributed to the new classes that have been added (of which there are many) and their implementations, the test cases, and in removing the old udpor_globals.* files.

The primary changes can be summarized as follows:

  1. The UnfoldingChecker.cpp was given a big boost. Instead of lying empty, what now appears is effectively pseudocode for the UDPOR algorithm. Note the absence of implementations in many of the important functions. The implementations of these functions will form the basis of future MRs.
  2. A whole slew of files were added under src/mc/explo/udpor (a new directory), corresponding to the additions mentioned above and their unit tests
  3. ActorState now holds shared pointers to the transitions they own. These transitions will eventually be vended to events that UDPOR creates from the State objects UDPOR decides to visit. Since events potentially outlive the states that UDPOR keeps track of, events need to ensure that the transitions they hold a reference to stay valid.

What to focus on

Reviewers should primarily focus on the unit tests introduced for each of the constructs added and should scrutinize the implementations of all (but especially the commonly-used) methods (e.g. EventSet::contains()) that will appear in UDPOR everywhere. Note, however, the current absence of tests from some more esoteric functions such as History::get_event_diff_with(const Configuration&) const. I feel it is more reasonable to add tests for functions such as these along with the phase to which they correspond, especially if it turns out some of the functions will be removed in favor of others when more of the implementation is added. Further, to prevent the diff from becoming too large, I have decided to stop here for the moment unit testing the functions in the MR. Do point out, though, if more tests are needed for the functions which are clearly intended to be heavily tested in this phase.

More tests (for both new and previously-introduced constructs) will be added in the coming week along with each phase fear not.

Edited by Maxwell Pirtle

Merge request reports