Phase 1 of Integration of UDPOR: Adding UDPOR Constructs
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):
- The
Unfolding
is the owner of all the events that UDPOR encounters and keeps alive. EachUdporChecker
instance holds an instance of andUnfolding
which it uses while exploring the event structure. UDPOR manipulates theUnfolding
so as to guarantee that references to events that theUnfolding
maintains are always valid. - Events that are discovered in the unfolding are represented with the
UnfoldingEvent
class. EachUnfoldingEvent
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 ife'
is an immediate cause ofe
, there is no evente''
wheree
causese''
ande''
causese'
). It is sufficient to store the immediate causes since this implicitly stores the entire history with the event - An
EventSet
is simple a set of events with some convenience methods. - A
Configuration
is almost anEventSet
, but it contains some convenience methods and maintains some extra information about the events in the collection. - A
History
of a set of events is an "un-expanded" version of the events in the entire history. TheHistory
class contains convenience methods for determining e.g. whether an event is in the joined history of a set of events. TheHistory
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:
- 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. - 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 -
ActorState
now holds shared pointers to the transitions they own. These transitions will eventually be vended to events that UDPOR creates from theState
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.