Martin Quinson [Thu, 27 Apr 2023 13:41:03 +0000 (15:41 +0200)]
Lazily compute the recipe of a state, on need only
This will be useful when leveraging intermediate states during
backtracks. In that case, we need to compute partial recipes, up to
the advanced restaure point.
Martin Quinson [Thu, 27 Apr 2023 11:48:19 +0000 (13:48 +0200)]
MC: give each state an incoming transition too
Using the parent's outgoing transition is not reliable anymore now
that we don't always explore the tree in order, but rather following
the exploration strategies.
Martin Quinson [Mon, 17 Apr 2023 08:01:01 +0000 (10:01 +0200)]
sonar fixes
- Undefined return value (that would happen on a platform without any host)
- Local variable shadowing
- Automatic memory management
- const, explicit, etc.
Since the events aren't ever removed from the
Unfolding and are instead simply displaced,
we change the name of the method to better
reflect what is going on
The `Unfolding` class in UDPOR previously discarded
all events from `U` when they were no longer needed.
Technically, UDPOR moves those events into a set `G`
which can be used to do more interesting things
in the future (e.g. to model check cyclic state spaces).
Furthermore, there are some subtlties it seems in
fully destroying the contents of an event after it has
been discovered, viz. with dealing with what to do when
a previous extension set contains such a deleted event
Detecting immediate conflicts for an event is
important as part of the clean up phase of
UDPOR. There was a typo that gave incorrect
results for the actual conflicts that were
detected which was resolved.
NOTE: There is still a problem with event
deletion. The issue is that previous configurations
will contain references to events which have been
deleted in the extension set which is computed
for them (ex(C)). I'm not quite sure how to
handle this at the moment...
Examine all opened_states_ to find the best candidate.
We cannot use a std::multiset, nor a std::priority_queue as before since
the value for the priority may change, even for states already stored in
opeened_states_.
Citing mlaurent:
"Le problème c'est que dans run() la partie gestion de "persistent set" peut
modifier des acteurs de State déjà dans opened_states_ en les passant à Todo.
Et ça, ça peut modifier la valeur renvoyée par next_transition_guided()."
The computation of K-partial alternatives requires
that we can determine whether or not `[e] + C`
for some event `e` is a valid configuration. There
was a subtlety in the code prior to the this commit
that caused UDPOR to incorrectly compute whether
or not `[e] + C` was a valid configuration. Specifically,
it was not sufficient to look at the difference between
the event's history and the events in the configuration
and checking *dependency*. You have to check *conflicts*:
it's possible that two events are dependent in a configuration
but are related to each other causally (and thus would
not be in conflict with one another)
Fix dynamic_cast<> typo for computation for CommRecv
There was a type check in the incremental computation
of extension sets for CommRecv that incorrectly cast
the value to a CommSend instead. I suppose this gave
us some undefined behavior as UDPOR correctly identified
the bug in some cases but not in other cases.
With the small fix, UDPOR now correctly identifies
the assertion failure in all cases in mc-failed-assertion.
Clarify that the issuer for a CommWait() action is that of the same actor
The `CommWait()` transition, in the manner that SimGrid
handles communications, can be said to be "issued" by either
the sender or the receiver that are a part of the communication
under consideration. We favor that which is run by the same actor;
indeed, we require it as this point unless otherwise noted.
If it is possible for a `CommWait` to wait on a communication
whose identity cannot be traced back to an event that already
executed by the same actor, the model would have to change
when computing extension sets for CommWait(), specifically
when checking whether or not that transition is enabled
at a prior state
Several XBT_DEBUG() statements were added throughout
the functions in UdporChecker to better understand
the evolution of UDPOR in the context of SimGrid.
Several `to_string()` statements were added where
appropriate to aid in the visualization of the
unfolding structure. Until we potentially add
a more complicated tree-drawing algorithm to SimGrid
that can render the unfolding structure systematically,
this is the best we have
Maxwell Pirtle [Tue, 28 Mar 2023 11:44:12 +0000 (13:44 +0200)]
Intermediate commit to prove that UDPOR functions
This commit returns a const_cast<>-ed UnfoldingEvent
from the intersection of the sets A and ex(C) in
the Unfolding. We use this work around currently as
there is no way currently to distinguish between a
set of events and a set of constant events with
EventSet. To do so would require a number of changes
and probably a class that would be entirely duplicated
and more difficult to read without the help of e.g.
a template (which itself is not always the easiest to
read).
Maxwell Pirtle [Mon, 27 Mar 2023 11:37:08 +0000 (13:37 +0200)]
Fill in implementation of CommWait before large changes
This commit adds the implementation of the extension
set computation before larger changes are added into
the UDPOR implementation.
What was discovered is that events hold stale references
to the transitions that they own. As UDPOR executes
actors in its quest to search the unfolding of the
application, the transitions that are executed are
potentially updated with additional information
*after* they have been executed. We'll need a way
to figure out how to manage this without causing an
absolute mess...
Maxwell Pirtle [Fri, 24 Mar 2023 10:21:13 +0000 (11:21 +0100)]
Add first steps for ex(C) for CommWait
Computing the extension sets of a `CommWait`
action turns out to be a bit more involved than
I anticipated. In particular, we must determine
whether or not the transition is enabled at
some point in the past. This requires us to
find the event which created the communication
on which the `CommWait` waits and perform a
couple checks on that event. The current implementation
is not complete and is missing several important
steps, but it's a step in the right direction.
Maxwell Pirtle [Thu, 23 Mar 2023 08:19:08 +0000 (09:19 +0100)]
Move state stack management to member on UnfoldingChecker
Instead of passing around the variable `state_stack`
in a number of arguments in the UnfoldingChecker,
we moved the stack into a member on the class. This
also allows us to give a textual trace of what UDPOR
is searching much in the same way as is done with
DFSExplorer
Maxwell Pirtle [Wed, 22 Mar 2023 08:33:07 +0000 (09:33 +0100)]
Track the current sequence of states with UDPOR
Prior to this commit, we only tracked the "current"
state that was visited by the program. This is not
sufficient however: we must also keep track of the
sequence of states that UDPOR visited to *generate*
the configuration it is currently looking at. This
is required since we need to be able to generate
a fresh remote process when UDPOR decides to re-explore
a configuration `C` in its second recursive call
if it determines that an alternative exists. The
state regeneration is very similar (practically
identical) to that which is performed in the DFSChecker.