Martin Quinson [Mon, 20 Mar 2023 22:27:39 +0000 (23:27 +0100)]
Do not initialize the App's memory introspection if it's not needed
Reforks are still not activated in this code, as the DFS constructor
pretends that it needs memory introspection when it does not. The
version activating reforks is currently commented here, if you want to
play with it.
Things seem more or less working with this change. Known issues:
- liveness checking is killed by a out-of-bounds access to a vector
while handling the property automaton. This is the case even when
reforks are not activated, making this change improper for the
master branch.
- The checker is not very good at killing the application in refork
mode, and many processes remain around until after they are
abandoned by their checker.
I'm not sure of whether they only consume memory or whether they
also burn the CPU in an active loop. In both cases, this is ...
suboptimal.
This point is OK when not activating reforks.
- valgrind reports some sort of double free on the libevent's events.
I fail to get the std::unique_ptr thing right. See next commit.
Martin Quinson [Mon, 20 Mar 2023 16:09:17 +0000 (17:09 +0100)]
Put everything in position to re-fork the verified App
If you pass "need_memory_introspection = false" to the Exploration
constructor, then the application is re-forked systematically instead
of taking snapshot that are then restored.
But it's still in progress, in the sense that the memory is still
introspected even if we don't need it. The network protocol still
needs to be changed so that the memory info are asked only if
"need_memory_introspection = true" and not otherwise.
For the time being, using reforks is very memory intensive for some
reason, and my computers gets to its knees when running the tests.
Until after the OOM killer saves me by cleaning stuff.
Martin Quinson [Sun, 19 Mar 2023 20:15:10 +0000 (21:15 +0100)]
cosmetics
Martin Quinson [Sun, 19 Mar 2023 20:07:00 +0000 (21:07 +0100)]
Move more of the CheckerSide creation logic to the object constructor
Martin Quinson [Sun, 19 Mar 2023 18:45:39 +0000 (19:45 +0100)]
MC: disable Address Space Layout Randomization in the application
This will allow to re-fork the application on restore without
invalidating all the metadata we accumulated in the previous
exploration traces.
Martin Quinson [Sun, 19 Mar 2023 15:18:05 +0000 (16:18 +0100)]
Differ the creation of the RemoteProcessMemory to when we have enough information
Martin Quinson [Sun, 19 Mar 2023 14:57:19 +0000 (15:57 +0100)]
Better responsabilities splitup between CheckerSide and RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 14:20:23 +0000 (15:20 +0100)]
Move methods not related to Memory out of RemoteProcessMemory
Now that ModelChecker is gone, it's time to move to the next step of cleanup.
The goal is that CheckerSide is in charge of the interaction with the
application process and RemoteProcessMemory is in charge of its memory.
Right now, RemoteProcessMemory does a bit more, as it stores the pid
and whether or not the application process is running.
This is bad because we want to make RemoteProcessMemory optional, only
used when we need to introspect the application memory (liveness
checking, non-progression checking, etc), so that we can run the app
in valgrind when we don't need to introspect its memory (safety
checking without non-progression checking).
I know I just moved this chunks of code from ModelChecker to
RemoteProcessMemory to now move it further, and I'm sorry for the
noise, but this code drives me nuts and I need to clean it step by step.
Martin Quinson [Sun, 19 Mar 2023 14:01:44 +0000 (15:01 +0100)]
Finally kill the now empty ModelChecker class
Martin Quinson [Sun, 19 Mar 2023 13:50:37 +0000 (14:50 +0100)]
Move the memory handling of RemoteProcessMemory singleton from ModelChecker to CheckerSide
Martin Quinson [Sun, 19 Mar 2023 13:29:05 +0000 (14:29 +0100)]
Move handle_message from ModelChecker to RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 12:54:23 +0000 (13:54 +0100)]
Move handle_waitpid from ModelChecker to RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 11:46:57 +0000 (12:46 +0100)]
Make a global singleton of Exploration, to kill ModelChecker
Having global singletons is far from optimal, but it's a bit like the
EngineImpl singleton in the model-checker process.
This will allow to kill the ModelChecker class which responsabilities
were split between RemoteApp and Exploration.
Martin Quinson [Sun, 19 Mar 2023 11:15:58 +0000 (12:15 +0100)]
Gosh, how many calls to that global were there?
Martin Quinson [Sun, 19 Mar 2023 11:09:07 +0000 (12:09 +0100)]
Kill a now unused class in mc
Martin Quinson [Sun, 19 Mar 2023 09:58:20 +0000 (10:58 +0100)]
Remove some more usage of mc_model_checker in Region and snapshoting logic
Martin Quinson [Sun, 19 Mar 2023 09:10:34 +0000 (10:10 +0100)]
Another use of mc_model_checker disapears. In Snapshot.equals.
I guess that this could be done in a better way, as noted in the
comment.
Martin Quinson [Sun, 19 Mar 2023 08:52:48 +0000 (09:52 +0100)]
another mc_model_checker call location disappears
I postponned this one a lot because it's impacting non-MC code, but at
the end it went smoothly
Martin Quinson [Sun, 19 Mar 2023 08:13:06 +0000 (09:13 +0100)]
Fix make distcheck
Martin Quinson [Sat, 18 Mar 2023 21:49:00 +0000 (22:49 +0100)]
Fix MC+clang builds
Martin Quinson [Sat, 18 Mar 2023 20:49:57 +0000 (21:49 +0100)]
Reduce a bit the adherance of handle_waitpid to ModelChecker
Martin Quinson [Sat, 18 Mar 2023 21:21:14 +0000 (21:21 +0000)]
Merge branch 'master' into 'master'
First step for guided state
See merge request simgrid/simgrid!141
mlaurent [Sat, 18 Mar 2023 14:58:43 +0000 (15:58 +0100)]
Move DPOR and sleep set algorithm from backtrack to run procedure
mlaurent [Sat, 18 Mar 2023 13:48:00 +0000 (14:48 +0100)]
Merge branch 'master' of https://framagit.org/simgrid/simgrid
mlaurent [Sat, 18 Mar 2023 13:46:53 +0000 (14:46 +0100)]
Replace todo direct access with consider methods; guided or not
mlaurent [Sat, 18 Mar 2023 13:05:13 +0000 (14:05 +0100)]
BasicGuide handle next_transition if asked to
Martin Quinson [Sat, 18 Mar 2023 11:21:30 +0000 (12:21 +0100)]
Merge CheckerSide::start() intp the constructor
Martin Quinson [Sat, 18 Mar 2023 11:05:09 +0000 (12:05 +0100)]
Better split of responsabilities between CheckerSide and RemoteApp
Define in CheckerSide the callbacks that are used in there, instead of
defining it in the RemoteApp and passing it along to the CheckerSide.
Let's be optimistic: this code is every day a bit less messy.
Martin Quinson [Sat, 18 Mar 2023 10:58:55 +0000 (11:58 +0100)]
Move the checker_side_ from the ModelChecker to the RemoteApp
with an axe.
Martin Quinson [Sat, 18 Mar 2023 10:25:53 +0000 (11:25 +0100)]
One usage of mc_model_checker less
I had to reduce the const-ness of the RemoteProcessMemory variable in
Snapshot::operator==() because getting the heap modifies the
RemoteMemory object. Sorry sonar.
mlaurent [Sat, 18 Mar 2023 10:14:35 +0000 (11:14 +0100)]
Add GuidedState abstract class; move ActorState management
Martin Quinson [Fri, 17 Mar 2023 22:02:27 +0000 (23:02 +0100)]
Simplify Channel::receive by handling non-blocking recv separately
Martin Quinson [Fri, 17 Mar 2023 21:23:09 +0000 (22:23 +0100)]
A few calls to mc_model_checker less by passing more parameters
Martin Quinson [Fri, 17 Mar 2023 21:13:40 +0000 (22:13 +0100)]
Move handle_simcall from ModelChecker to RemoteApp
Martin Quinson [Fri, 17 Mar 2023 21:42:38 +0000 (21:42 +0000)]
Merge branch 'master' into 'master'
Add reference to parent state
See merge request simgrid/simgrid!140
mlaurent [Fri, 17 Mar 2023 15:55:22 +0000 (16:55 +0100)]
Add reference to parent state: only use this creation in DFSexplorer
Arnaud Giersch [Thu, 16 Mar 2023 10:58:11 +0000 (11:58 +0100)]
Missing include.
Arnaud Giersch [Thu, 16 Mar 2023 10:46:41 +0000 (11:46 +0100)]
Decrease required version for nlohmann_json; add to jenkins/project_description.sh.
Version 3.7.0 is available in debian/buster-backports.
Arnaud Giersch [Wed, 15 Mar 2023 14:25:52 +0000 (15:25 +0100)]
Useless guards.
Arnaud Giersch [Wed, 15 Mar 2023 14:17:52 +0000 (15:17 +0100)]
Apply "smpi/buffering" when MC_record_replay_is_active too.
Martin Quinson [Wed, 15 Mar 2023 22:54:52 +0000 (23:54 +0100)]
Sanitize how we know the current MC mode
This can be either NONE, AppSide, CheckerSide or Replay.
Also, further reduce how often we use the mc_model_checker singleton
Martin Quinson [Wed, 15 Mar 2023 22:23:03 +0000 (23:23 +0100)]
Make it compile with all warnings enabled
Martin Quinson [Wed, 15 Mar 2023 21:55:45 +0000 (22:55 +0100)]
Document a future cleanup to do when we bump cmake version
Arnaud Giersch [Tue, 14 Mar 2023 15:51:08 +0000 (16:51 +0100)]
Remove comments about non-existent support for smpi/privatization in MC.
[ci-skip]
Arnaud Giersch [Tue, 14 Mar 2023 15:34:28 +0000 (16:34 +0100)]
Really check the privatization option in the MCed SMPI app.
Arnaud Giersch [Tue, 14 Mar 2023 08:24:44 +0000 (09:24 +0100)]
Inform if JSON lib is found.
Martin Quinson [Mon, 13 Mar 2023 23:43:27 +0000 (00:43 +0100)]
Test for JSON before using it
Martin Quinson [Mon, 13 Mar 2023 23:43:04 +0000 (00:43 +0100)]
Cosmetics
Martin Quinson [Mon, 13 Mar 2023 21:47:12 +0000 (22:47 +0100)]
fix make distcheck
Fred Suter [Mon, 13 Mar 2023 21:12:47 +0000 (21:12 +0000)]
Merge branch 'master' into 'master'
Add wfformat json DAG loader and DAG doc
See merge request simgrid/simgrid!137
Adrien [Mon, 13 Mar 2023 21:12:47 +0000 (21:12 +0000)]
Add wfformat json DAG loader and DAG doc
Martin Quinson [Mon, 13 Mar 2023 09:34:06 +0000 (10:34 +0100)]
Correctly protect tests property settings, bummer
Martin Quinson [Mon, 13 Mar 2023 09:07:07 +0000 (10:07 +0100)]
Give the remote_process_memory to the mc::State constructor
This way, we rely a bit less on the ugly mc_model_checker singleton.
Martin Quinson [Sun, 12 Mar 2023 23:05:42 +0000 (00:05 +0100)]
Move another function of ModelChecker to RemoteProcessMemory
Martin Quinson [Sun, 12 Mar 2023 22:59:42 +0000 (23:59 +0100)]
Move another function out of ModelChecker
Martin Quinson [Sun, 12 Mar 2023 22:52:33 +0000 (23:52 +0100)]
Move a function from ModelChecker to Exploration
Martin Quinson [Sun, 12 Mar 2023 22:31:40 +0000 (23:31 +0100)]
move wait_for_requests() from ModelChecker to RemoteApp
Martin Quinson [Sun, 12 Mar 2023 22:10:10 +0000 (23:10 +0100)]
Inline a function in ModelChecker
Martin Quinson [Sun, 12 Mar 2023 22:05:06 +0000 (23:05 +0100)]
Move one method from ModelChecker to Exploration
Martin Quinson [Sun, 12 Mar 2023 21:57:25 +0000 (22:57 +0100)]
Move 2 functions from mc::ModelChecker to mc::RemoteApp
Martin Quinson [Sun, 12 Mar 2023 21:35:53 +0000 (22:35 +0100)]
Make the sendsend tests at least fail fast to not hinder my workflow
Martin Quinson [Sun, 12 Mar 2023 21:16:16 +0000 (22:16 +0100)]
MC: rename remote/RemoteProcess to sosp/RemoteProcessMemory
Martin Quinson [Sun, 12 Mar 2023 20:50:18 +0000 (21:50 +0100)]
Clean leftovers
Martin Quinson [Sat, 11 Mar 2023 00:05:31 +0000 (01:05 +0100)]
MC: stop reading maxpid in memory, but ask it over the network instead
Martin Quinson [Fri, 10 Mar 2023 22:44:05 +0000 (23:44 +0100)]
One use less of the global mc_model_checker
Martin Quinson [Fri, 10 Mar 2023 22:34:07 +0000 (23:34 +0100)]
This seems to reduce the amount of failure, but I don't know why :(
Not sure I know what I'm doing here :(
Arnaud Giersch [Sun, 12 Mar 2023 15:16:23 +0000 (16:16 +0100)]
Fix build with -D_GLIBCXX_DEBUG [-Werror=range-loop-construct].
Arnaud Giersch [Fri, 10 Mar 2023 16:08:07 +0000 (17:08 +0100)]
Fix assert: min and max are both included in interval for MC_random.
[ci-skip]
Martin Quinson [Fri, 10 Mar 2023 21:25:15 +0000 (21:25 +0000)]
Merge branch 'udpor-phase5' into 'master'
Phase 5 of UDPOR Integration: Implementing Conflict Checks
See merge request simgrid/simgrid!138
Martin Quinson [Fri, 10 Mar 2023 18:48:33 +0000 (19:48 +0100)]
Try to avoid a segfault on assert message
This is an attempt to fix https://framagit.org/simgrid/simgrid/-/issues/118
Maxwell Pirtle [Fri, 10 Mar 2023 10:15:36 +0000 (11:15 +0100)]
Add first test for immediate conflicts edge case
Detecting immediate conflicts is much more subtle
than detecting conflicts in general. The subtlety
lies in the fact that the collection of events
in the shared history of the two events under
consideration must itself be a valid configuration:
in other words, the events would not be considered
to be in immediate conflict if somewhere in their
history lies a conflict.
Maxwell Pirtle [Fri, 10 Mar 2023 09:06:33 +0000 (10:06 +0100)]
Add first batch of tests for conflict detection among events
Detecting conflicts among a collection of events
is super critical to the proper functioning of
UDPOR (it is primarily used to compute en(C) for
a given configuration). Testing conflicts among
events in an event structure is very important.
Subsequent commits and MRs will continue to add
tests for detecting conflicts among collections
of events.
Detecting immediate conflicts is also critical
when it comes to determining which events UDPOR
decides to keep around after continuing its search.
Immediate conflicts are more subtle and should be
tested with great care.
Henri Casanova [Thu, 9 Mar 2023 19:08:18 +0000 (09:08 -1000)]
re-fixed assert message with up-to-date configuration option name
Henri Casanova [Thu, 9 Mar 2023 18:45:19 +0000 (08:45 -1000)]
Assert message fix
Maxwell Pirtle [Thu, 9 Mar 2023 14:34:25 +0000 (15:34 +0100)]
Add implementation for immediate conflicts
Two events are said to be in immediate conflict
if they are conflicting but if the removal of
either event from their shared history would
result in a conflict-free set. That is, if
the only conflict among the set of events in
the history of the two events `e` and `e'`
is between `e` and `e'`, then `e` and `e'`
are in immediate conflict
Maxwell Pirtle [Thu, 9 Mar 2023 14:19:07 +0000 (15:19 +0100)]
Require conflict-freedom in is_valid_configuration
The method `EventSet::is_valid_configuration()`
was missing the condition that the set of events
need also be free of conflicts (in addition to
being causally closed)
Maxwell Pirtle [Thu, 9 Mar 2023 13:18:56 +0000 (14:18 +0100)]
Add src/.../udpor/udpor_tests_private.hpp to CMake
Arnaud Giersch [Thu, 9 Mar 2023 13:18:32 +0000 (14:18 +0100)]
Eager mode is for the first case only (thx adegomme).
[ci-skip]
Maxwell Pirtle [Thu, 9 Mar 2023 13:08:27 +0000 (14:08 +0100)]
Add test to verify topological ordering of EventSet
The topological ordering was moved into EventSet
in a prior commit since it is useful to order
events in an EventSet that reside outside of a
Configuration. This commit adds a stress test
that verifies that the topological orderings
of all possible subsets of a collection of
events obey the topological ordering invariant
after being ordered (in both directions)
Arnaud Giersch [Thu, 9 Mar 2023 10:36:49 +0000 (11:36 +0100)]
Improve doc for smpi/buffering.
Describe the behavior like for smpi/send-is-detached-thresh.
Arnaud Giersch [Wed, 8 Mar 2023 22:15:18 +0000 (23:15 +0100)]
Fix asserts for when received size is 0 (message type is invalid).
Arnaud Giersch [Wed, 8 Mar 2023 15:36:45 +0000 (16:36 +0100)]
Depreciate unused functions s4u::Comm::copy_{buffer,pointer}_callback().
Arnaud Giersch [Wed, 8 Mar 2023 15:36:13 +0000 (16:36 +0100)]
Inline s4u::Comm::copy_pointer_callback which is the default callback.
Maxwell Pirtle [Wed, 8 Mar 2023 14:27:43 +0000 (15:27 +0100)]
Begin filling in computations of ex(C) and en(C)
This commit introduces the first steps towards
computing ex(C) and en(C) using many of the
additions of the previous phases. An important
part of the computation is so far missing, however,
viz. the determination of whether or not an action
`a` is enabled at some point in the past. We'll
need to decipher what's going on in tiny_simgrid
to fully determine what to do here; for now, we
simply ignore adding an event entirely and just
say that `a` was disabled at all points in the past.
Arnaud Giersch [Wed, 8 Mar 2023 14:09:13 +0000 (15:09 +0100)]
Depreciate ForcefulKillException::try_n_catch().
It was used by the Java bindings.
Arnaud Giersch [Wed, 8 Mar 2023 13:23:00 +0000 (14:23 +0100)]
Obvious typo.
Maxwell Pirtle [Wed, 8 Mar 2023 13:11:39 +0000 (14:11 +0100)]
Fix logic for mutual conflict between two events
Prior to this commit, detecting whether two
events were in conflict involved looking at all
of the events with respect to all others. However,
you must instead *only* look at how the event `e`
and `e'` relate to the other event's history:
we wouldn't care if some other event is in conflict
with `e'` if `e` is not that event
Maxwell Pirtle [Wed, 8 Mar 2023 12:12:00 +0000 (13:12 +0100)]
Add conflict-free invariant check to Configuration
When adding events to a configuration, we want to
ensure that the configuration remains both a)
causally closed and b) conflict-free. The latter
required that the tests be modified as they effectively
assumed that the transitions associated with each
event were independent of one another. Since the
`Transition` base class is dependent by default, this
was at odds with the assumptions
Arnaud Giersch [Wed, 8 Mar 2023 10:23:17 +0000 (11:23 +0100)]
Use #include <...> for foreign header files.
Files in teshsuite/smpi/mpich3-test/ were not considered.
Maxwell Pirtle [Wed, 8 Mar 2023 10:18:50 +0000 (11:18 +0100)]
Add preliminary tests for checking event conflicts
Maxwell Pirtle [Wed, 8 Mar 2023 08:13:15 +0000 (09:13 +0100)]
Add conflict detection to EventSet
Detecting whether or not a collection of events
are in conflict important for computing en(C)
and for K-partial alternatives. We simply
follow the definition of conflicts. More
esoteric methods may exist that are faster,
but for now let's keep it simple: we can always
add those in later incrementally
Martin Quinson [Wed, 8 Mar 2023 00:10:15 +0000 (00:10 +0000)]
Merge branch 'udpor-phase4' into 'master'
Phase 4 of UDPOR Integration: Variable For-loop
See merge request simgrid/simgrid!136
Maxwell Pirtle [Tue, 7 Mar 2023 13:36:03 +0000 (14:36 +0100)]
Add ability to restrict maximum subset size
This commit adds the ability to restrict the
size of the maximal subsets that are produced
by the maximal_subsets_iterator. This filtering
significantly reduces the number of subsets that
need to be searched in more complicated graphs.
The advantage of adding the filtering directly
to the maximal_subsets_iterator over using a
higher-order iterator such as boost::filter_iterator
is that branches can be pruned immediately. Since
the maximal_subsets_iterator performs its search
in depth-first order, something like
boost::filter_iterator, while technically equivalent,
would have to actually perform the iteration over
entire branches that are otherwise useless due to
their size.
Searching maximal subsets of a restricted size is
useful when determining conflicts between sets of
events: we want to look at pairs of maximal events
Maxwell Pirtle [Tue, 7 Mar 2023 13:05:01 +0000 (14:05 +0100)]
Add asserts for Configuration vs EventSet
This commit adds two asserts to ensure that
traversing a configuration is equivalent to
traversing the events of that configuration.
That is, the assertions check that a configuration
can effectively be treated as a set of events
when it comes to traversal of maximal sets and
computing a topological ordering
Maxwell Pirtle [Tue, 7 Mar 2023 12:48:29 +0000 (13:48 +0100)]
Allow iteration over maximal subsets of an EventSet
The maximal_subsets_iterator was updated to allow
traversal over the subsets of events of some set `E`
which are maximal (i.e. causally-free). It is a
simple addition which extends the power of the iterator
to EventSets more generally (as opposed to strictly
for Configurations)
Maxwell Pirtle [Tue, 7 Mar 2023 12:41:41 +0000 (13:41 +0100)]
Move topological ordering to EventSet
The events of an EventSet can be ordered
topologically by considering them as part
of the configuration containing the histories
of all events in the set. The trick is to
ignore adding in an event into the ordering
if the event is not contained in the original
set itself
Maxwell Pirtle [Tue, 7 Mar 2023 09:05:45 +0000 (10:05 +0100)]
Rename `EventSet::is_maximal_event_set()`
The method `is_maximal_event_set()` was renamed
to simply `is_maximal()`, since the question is
already being asked about some event set (i.e.
the `_event_set` bit is redundant)
Maxwell Pirtle [Tue, 7 Mar 2023 08:10:58 +0000 (09:10 +0100)]
Add some basic tests for variable_for_loop
Some tests were added to confirm that the
variable_for_loop iterator behaved as expected.
Arnaud Giersch [Mon, 6 Mar 2023 15:16:49 +0000 (16:16 +0100)]
Fixes in docs/source/tuto_* (untested).
Maxwell Pirtle [Mon, 6 Mar 2023 15:13:50 +0000 (16:13 +0100)]
Write maximal_subsets_iterator_wrapper with xbt utils