Actually, read()=0 is not an issue in the AppSide

it simply means that the checker closed the socket on its side, so we
should quit ASAP without complaining.

Fix some easy sonar smells

const-ness, try_emplace, attribute noreturn, ...

The most important one is the TransitionObjectAccess one, where a
field in the subclass was hiding a field of the same name in the
superclass. Maybe the bug I was experiencing in that area was related.

Fix two sonar bugs

- don't throw from the destructor
- don't slice objects (downcast objects instead of downcasting
  references). I suspect that this one is a false positive but the
  tests still pass this way so let's go.

Change an example to take its platform file from the command line if provided

Merge branch 'udpor-phase6' into 'master'

Phase 6 of UDPOR Integration: Add `K`-partial alternatives computation + clean up phase

See merge request simgrid/simgrid!139

jenkins::Flags if you run the tests, be verbose on errors [no-ci]

Make sure that the dtor of CheckerSide actually kills the application and waits for it

Fix the liveness tests when the reforks are compiled in but not activated

Manually handle the memory associated to the libevent events

The previous version with std::unique_ptr resulted in segfaults errors
reported by valgrind, and I fail to get it right.

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.

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.

Address minor comments in MR review

Remove empty Comb.cpp

Add documentation for Comb data structure

The Comb data structure lacked documentation
prior to this commit. Since it plays a pretty
important role in the computation of `K`-partial
alternatives, it was given a more extensive
explanation to ensure that it was used properly.

cosmetics

Move more of the CheckerSide creation logic to the object constructor

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.

Differ the creation of the RemoteProcessMemory to when we have enough information

Better responsabilities splitup between CheckerSide and RemoteProcessMemory

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.

Finally kill the now empty ModelChecker class

Move the memory handling of RemoteProcessMemory singleton from ModelChecker to CheckerSide

Move handle_message from ModelChecker to RemoteProcessMemory

Move handle_waitpid from ModelChecker to RemoteProcessMemory

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.

Gosh, how many calls to that global were there?

Kill a now unused class in mc

Remove some more usage of mc_model_checker in Region and snapshoting logic

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.

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

Fix make distcheck

Fix MC+clang builds

Reduce a bit the adherance of handle_waitpid to ModelChecker

Merge branch 'master' into 'master'

First step for guided state

See merge request simgrid/simgrid!141

Move DPOR and sleep set algorithm from backtrack to run procedure

Merge branch 'master' of https://framagit.org/simgrid/simgrid

Replace todo direct access with consider methods; guided or not

BasicGuide handle next_transition if asked to

Merge CheckerSide::start() intp the constructor

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.

Move the checker_side_ from the ModelChecker to the RemoteApp

with an axe.

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.

Add GuidedState abstract class; move ActorState management

Simplify Channel::receive by handling non-blocking recv separately

A few calls to mc_model_checker less by passing more parameters

Move handle_simcall from ModelChecker to RemoteApp

Merge branch 'master' into 'master'

Add reference to parent state

See merge request simgrid/simgrid!140

Add reference to parent state: only use this creation in DFSexplorer

Fix test in k-partial alternatives step five

The fifth step in the K-partial alternatives
actually has three possible alternatives that
can be selected instead of only one. UDPOR
would still pick e7 next regardless, but more
than one outcome is possible.

Missing include.

Decrease required version for nlohmann_json; add to jenkins/project_description.sh.

Version 3.7.0 is available in debian/buster-backports.

Remove unused code in Comb.cpp + fix MANIFEST.in

Add full example for K-partial alternatives

Useless guards.

Apply "smpi/buffering" when MC_record_replay_is_active too.

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

Make it compile with all warnings enabled

Document a future cleanup to do when we bump cmake version

Move alternative computation to Configuration for testing

Add semantic equivalence to UnfoldingEvent

Two UnfoldingEvents are considered to be equivalent
if they have the same associated action (same actor,
type, and times_considered) and the same immediate history.
Semantic equivalence is required since any given
event may appear in the extension set of several configurations
that UDPOR decides to explore, and thus we must be able
to determine if a newly-computed event has already been
seen before

Add comments in K-partial alternatives computation

The computation of k-partial alternatives was added in
a prior commit. This commit implements the function
`Configuration::is_compatible_with(const History&)`
which is used during the computation of K-partial alternatives
to determine which events go with which spikes.

Note: The implementation that currently exists for
K-partial alternatives is a first go at an implementation
of the algorithm. There are clear spots within the computation
where performance may be improved with some more clever ideas.
For now, we're working towards a proof-of-concept: we can
optimize more heavily later

Remove comments about non-existent support for smpi/privatization in MC.

[ci-skip]

Really check the privatization option in the MCed SMPI app.

Add first go at implementation of K-partial alternatives

The algorithm for computing K-partial alternatives was
added in this commit. It doesn't look super clean
at this point, nor is the code as efficient as it
could be, but it certainly is a first go at an
implementation for K-partial alternatives. Subsequent
commits will attempt to clean up the code and will
implement a version of `Configuration::is_compatible_with()`
which currently remains unimplemented

Inform if JSON lib is found.

Test for JSON before using it

Cosmetics

fix make distcheck

Merge branch 'master' into 'master'

Add wfformat json DAG loader and DAG doc

See merge request simgrid/simgrid!137

Add wfformat json DAG loader and DAG doc

Add Comb data structure for K-partial alternatives

Add clean up phase to UDPOR

The last part of processing during UDPOR
involves removing events from the unfolding
which are no longer needed. The events in
the unfolding which must be preserved are outlined
in the UDPOR paper and are labeled Q_CDU.

Correctly protect tests property settings, bummer

Give the remote_process_memory to the mc::State constructor

This way, we rely a bit less on the ugly mc_model_checker singleton.

Move another function of ModelChecker to RemoteProcessMemory

Move another function out of ModelChecker

Move a function from ModelChecker to Exploration

move wait_for_requests() from ModelChecker to RemoteApp

Inline a function in ModelChecker

Move one method from ModelChecker to Exploration

Move 2 functions from mc::ModelChecker to mc::RemoteApp

Make the sendsend tests at least fail fast to not hinder my workflow

MC: rename remote/RemoteProcess to sosp/RemoteProcessMemory

Clean leftovers

MC: stop reading maxpid in memory, but ask it over the network instead

One use less of the global mc_model_checker

This seems to reduce the amount of failure, but I don't know why :(

Not sure I know what I'm doing here :(

Fix build with -D_GLIBCXX_DEBUG [-Werror=range-loop-construct].

Fix assert: min and max are both included in interval for MC_random.

[ci-skip]

Merge branch 'udpor-phase5' into 'master'

Phase 5 of UDPOR Integration: Implementing Conflict Checks

See merge request simgrid/simgrid!138

Try to avoid a segfault on assert message

This is an attempt to fix https://framagit.org/simgrid/simgrid/-/issues/118

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.

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.

re-fixed assert message with up-to-date configuration option name

Assert message fix

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

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)

Add src/.../udpor/udpor_tests_private.hpp to CMake

Eager mode is for the first case only (thx adegomme).

[ci-skip]

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)