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
Maxwell Pirtle [Mon, 6 Mar 2023 14:28:05 +0000 (15:28 +0100)]
Fix edge cases in variable_for_loop
Some tests were added which detected an off-by-one
error in the implementation logic of the variable_for_loop.
Subsequent commits will add more tests to the iterator
for further verification
Maxwell Pirtle [Mon, 6 Mar 2023 13:41:24 +0000 (14:41 +0100)]
Write LazyPowerSet in terms of iterator_wrapper
Maxwell Pirtle [Mon, 6 Mar 2023 13:01:48 +0000 (14:01 +0100)]
Add iterator_wrapping convenience container
The iterator_wrapping structure is a light-weight
container whose contents are traversed according
to the behavior of the iterator that it creates
when asked. The wrapping can only construct
a container around an iterator whose termination
condition can be succinctly represented with a
default-constructed argument. It is not always
the case that such a default-constructed iterator
represents the end, so this should be kept in made
(although this is generally the convention).
Creating an instance of a wrapping allows, e.g.,
for the traversal over a collection without explicit
need to construct the iterators/loop manually.
For example, a struct `Iterable` may define a method
`make_complicated_forward_iterator_over_me()`
that can be called and used inside e.g. an auto-based
for-loop. This helps with readability immensely.
Maxwell Pirtle [Mon, 6 Mar 2023 09:32:54 +0000 (10:32 +0100)]
Add first implementation of variable for-loop
Martin Quinson [Mon, 6 Mar 2023 09:50:07 +0000 (10:50 +0100)]
Fix clang build and make output more portable/predictible
Maxwell Pirtle [Fri, 3 Mar 2023 12:34:02 +0000 (13:34 +0100)]
Add computation for minimally reproducible sets
A minimally reproducible set of a configuration
is simply the smallest set of events whose
collective histories joint together cover every
event in the configuration. Effecively, it is
the maximal set of C whose history equals C.
The computation builds upon the maximal_subsets_iterator
introduced in a prior phase and exploits all of
the work that already went into computing the
subsets
Martin Quinson [Mon, 6 Mar 2023 08:05:55 +0000 (09:05 +0100)]
sthread: Add a way to verify accesses to non-reentrant data structures
The example is very fragile so far, segfaulting 2 times over 3 in
general, so don't activate it.
Martin Quinson [Mon, 6 Mar 2023 09:17:42 +0000 (10:17 +0100)]
Cosmetics in sthread output when not using SMPI
Arnaud Giersch [Mon, 6 Mar 2023 07:49:26 +0000 (08:49 +0100)]
Enable compile optimizations when tests will be run.
[ci-skip]
Arnaud Giersch [Sun, 5 Mar 2023 21:48:50 +0000 (22:48 +0100)]
Missing ']'
[ci-skip]
Arnaud Giersch [Sun, 5 Mar 2023 20:56:34 +0000 (21:56 +0100)]
Fix compilation error with clang 11.0.1.
Building CXX object CMakeFiles/simgrid.dir/src/mc/explo/udpor/maximal_subsets_iterator.cpp.o
In file included from .../src/mc/explo/udpor/maximal_subsets_iterator.cpp:1:
.../src/mc/explo/udpor/maximal_subsets_iterator.hpp:38:3: error: explicitly defaulted default constructor is implicitly deleted [-Werror,-Wdefaulted-function-deleted]
maximal_subsets_iterator() = default;
^
.../src/mc/explo/udpor/maximal_subsets_iterator.hpp:43:68: note: default constructor of 'maximal_subsets_iterator' is implicitly deleted because field 'config' of const-qualified type 'const std::optional<std::reference_wrapper<const Configuration>>' would not be initialized
const std::optional<std::reference_wrapper<const Configuration>> config;
^
1 error generated.
Arnaud Giersch [Sun, 5 Mar 2023 20:31:19 +0000 (21:31 +0100)]
Enable _GLIBCXX_DEBUG for one of the builds.
Also run the tests in this case.
Arnaud Giersch [Sun, 5 Mar 2023 16:35:16 +0000 (17:35 +0100)]
Sonar smells.
Martin Quinson [Sun, 5 Mar 2023 20:13:24 +0000 (20:13 +0000)]
Merge branch 'maximal-subset-search' into 'master'
Phase 3 of UDPOR Integration: Iteration Over Maximal Sets of a Configuration
See merge request simgrid/simgrid!135
Arnaud Giersch [Sun, 5 Mar 2023 14:32:32 +0000 (15:32 +0100)]
Don't clear flops_amount on ExecImpl::reset.
Fix failures where flops_amount is not defined anymore in ExecImpl::start
(found by building with CXXFLAGS=-D_GLIBCXX_DEBUG)
Arnaud Giersch [Sun, 5 Mar 2023 14:01:22 +0000 (15:01 +0100)]
Quick tests show that currentContainer is always empty at this point.
Arnaud Giersch [Sat, 4 Mar 2023 09:35:59 +0000 (10:35 +0100)]
Walking the stack in the forward direction gives the same result, but makes the code simpler.
Arnaud Giersch [Thu, 2 Mar 2023 21:14:38 +0000 (22:14 +0100)]
Simplify assertions.
Augustin Degomme [Sat, 4 Mar 2023 13:13:06 +0000 (14:13 +0100)]
try to use another mattermost action, as the main one is linux only (uses docker)
Augustin Degomme [Sat, 4 Mar 2023 12:10:51 +0000 (13:10 +0100)]
[ci-skpi] fix sending of messages, and do parallel testing on github action
Augustin Degomme [Sat, 4 Mar 2023 12:09:16 +0000 (13:09 +0100)]
assume mmap is not functional for us on macos>=11 as memory accesses are restricted by default
Augustin Degomme [Sat, 4 Mar 2023 10:51:11 +0000 (11:51 +0100)]
[ci skip] remove spurious line
Augustin Degomme [Sat, 4 Mar 2023 10:43:20 +0000 (11:43 +0100)]
add macos build to github action, untested
Augustin Degomme [Sat, 4 Mar 2023 10:42:56 +0000 (11:42 +0100)]
remove ns3 from ubuntu stable and github actions, as 3.35 is broken on 22.04
Martin Quinson [Fri, 3 Mar 2023 23:08:16 +0000 (00:08 +0100)]
Fix a useless change -- and go get some sleep
Martin Quinson [Fri, 3 Mar 2023 22:57:15 +0000 (23:57 +0100)]
Bump cmake to at least 3.12
- It's difficult to search for Python Development component before that version
- This version is available in Debian buster (oldstable)
Martin Quinson [Fri, 3 Mar 2023 22:50:05 +0000 (23:50 +0100)]
python3-dev is another dependency of the Python bindings
Martin Quinson [Fri, 3 Mar 2023 20:21:07 +0000 (21:21 +0100)]
Reindent -- almost no real change
Simply don't traverse an array if debug logs are disabled.
Arnaud Giersch [Fri, 3 Mar 2023 16:32:08 +0000 (17:32 +0100)]
Forgot to add c++17g to the "ignore" list.
[ci-ckip]
Martin Quinson [Fri, 3 Mar 2023 14:31:22 +0000 (15:31 +0100)]
fix MC + gcc builds
Martin Quinson [Fri, 3 Mar 2023 10:45:34 +0000 (11:45 +0100)]
Move the implem of a function out of the header to reduce issues
Martin Quinson [Thu, 2 Mar 2023 23:30:29 +0000 (00:30 +0100)]
Move the PageStore from ModelChecker to RemoteApp
Maxwell Pirtle [Fri, 3 Mar 2023 10:06:54 +0000 (11:06 +0100)]
Correct MANIFEST.in according to `make distcheck`
Maxwell Pirtle [Fri, 3 Mar 2023 08:00:25 +0000 (09:00 +0100)]
Filter events before performing iteration
A filter can be supplied to the maximal subset
iterator to remove events from consideration in
maximal subsets. Instead of needlessly processing
events that will never be considered, we can
instead remove those events at the beginning while
perserving the relative ordering among events that
we do actually care about. This both simplifies the
bookkeeper's code slightly and reduces the number
of times we need to invoke the filter function drastically
(once per event instead of multiple times per combination).
Martin Quinson [Thu, 2 Mar 2023 22:59:14 +0000 (23:59 +0100)]
Move the stats of visited_states count from ModelChecker to DFSExplorer where it belongs
Martin Quinson [Thu, 2 Mar 2023 22:48:01 +0000 (23:48 +0100)]
Move the dot_output from ModelChecker to Exploration