Pass include and library directories to try_compile.

Fix usage of option --cfg=path in tesh files.

Most of them reference a non-existent directory: examples/smpi/msg/.
Remove them.

Use the option in tests from basic-parsing-test.

Make distcheck

MC: Reap all zombie childs to avoid them to accumulate

Remove the timings of another ns3 test to help older ns3 versions

Allow ns3 to be idempotent if correctly patched

Rename `remove()` method on `Unfolding`

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

Make use of the sets `G` and `U` with `Unfolding`

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

Fix bug with immediate conflict detection

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...

Improve the logging level of that message that is relatively important

these ns3 tests need an 'output sort' directive :(

Regenerate tesh files (one more time).

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()."

Cosmetics.

Rename MC_NEED_PTRACE -> SIMGRID_MC_NEED_PTRACE for consistency.

Centralize definitions for the name of environment variables used by the MC.

Sonar smells; remove redundant mentions of std::shared_ptr<State>.

Fix make distcheck, stupid bummer

Enforce the ns3 timings for the latest version of ns3, and just execute older versions

Fix conflict detection between configs + history

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

Add first round of debug logging to UDPOR

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

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).

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...

Add extension set computations without type casts

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.

Additionally, some Sonar errors were fixed.

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

Add comment on state restoration in UnfoldingChecker

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.

Replace switch statement with map of handlers

Add skeleton implementation for ex(C) for CommSend

Add skeleton implementations to ExtensionSetCalculator

Add ExtensionSetCalculator files

Add test case for tracking latest events/transitions

Add dependency between same actor for tests

It doesn't make sense to say that two
transitions executed by the same actor are
independent; indeed, it would lead to unexpected
results when testing whether or not a configuration
were properly tracking the "most recent" event
for each actor, as is done in subsequent commits

Begin tracking latest events for each actor

Computing specialized extensions for each transition
type frequently requires knowing the "latest" event
that some given actor is associated with in some
configuration (denoted `preEvt(C, a)`). We now track
this information as new events are added and pre-compute
the information when constructing a configuration with
a set of events using once again our favorite topological
ordering function.

Subsequent commits will introduce some unit tests to
ensure that the Configuration is tracking the new events
appropriately.

Make strsignal(SIGSEGV) return the same string across all architectures

Use the fast SOCK_SEQPACKET where available

Maybe SOCK_SEQPACKET is not faster than SOCK_STREAM per se, I don't
know, but streams force us to re-bufferize the data that we receive in
excess, leading to many useless data copies.

Make the MC protocol work on top of STREAM sockets

MacOSX does not have AF_UNIX + SOCK_SEQPACKET so we need SOCK_STREAM
for that architecture. I'll make it SEQPACKET on Linux+FreeBSD and
STREAM on Mac in the next commit, but I wanted to code and debug the
SOCK_STREAM version locally.

The problem with the SOCK_STREAM version is that messages are not
segmented anymore: each recv() gets everything that got posted on the
socket already, so I have to implement a buffer in which I can
reinject the extraneous bytes received, so that they can be used in
the next recv(). The real fun begins when I have half of the expected
message in buffer and the other half must be taken from the network.

Or even better: the second half was not posted yet so reading from the
network is blocking for ever. This can happen when I receive any
message in a 512-bytes buffer, but I already had a full but shorter
message in buffer. I have to try reading from the socket with the
DONT_WAIT flag, detect that there is nothing to read, and use the
buffer content only.

Regenerate tesh files.

Use a multiset to handle opened states, and ensures a reproductible order on different systems.

From cppreference: The order of the elements that compare equivalent is the order of insertion and does not change.
 (since C++11)

An integer seems good enough to handle priorities, and is not subject to rounding errors.

Don't die at compilation when activating stateless MC on non-ptrace architectures

Remove a file generated by cmake

Ensure in tests that the ns3 timings remain unchanged

Revert "Treat ECONNRESET like a normal connection close."

This reverts commit 2fbcc71ab230e6a05e64189f6bd7c49c1df31907.

It was erroneously pushed before testing. Sorry for the noise.
[ci-skip]

Treat ECONNRESET like a normal connection close.

Also return immediately with EAGAIN, or handle_message() will fail with size == -1.

Kill another override-to-same-content

Cosmetics in cmake

- use ON/OFF instead of 1/0
- display all MC related options together
- mark some crufy variables as advanced to hide them

Don't override a method to the same content

Don't use ucontextes on Apple hosts

Cast a printf parameter to please MacOS X

Disable MC stateful API when not running in MC

This is a better fix for the null-dereference found by the sanitizers
since 2 nights. Instead of hiding the problem on these builds (as done
in previous commit), fix it for every builds.

MC stateful API is only needed when stateful MC is compiled in

Don't use CLOEXEC

In one case (Checker->App), we were removing it after setup so we
don't need it.

In the other case (App->App), it was just to be tiddy but it's not
really useful: Forking applications are barely supported anyway.

Ensure that the clang optimizer does not swallow the segfault I'm expecting

Instead of actually dereferencing the null pointer (which drives the
static analyzers nuts), simply send myself a SIGSEGV.

Ignore empty replay path + hide a global (to avoid init fiasco)

I was observing that the model_checking_mode global did not had the
same value when compiling with or without optimizations.

Maybe I had a sort of race condition on model_checking_mode during
initialization, or maybe the config element of the replay path was
either called before or after the initialization of the library, thus
replacing the model_checking_mode to REPLAY even if it was supposed to
be APP_SIDE in my case.

It's fixed now, but I'm not completely sure of which of these change
was the right one (probably the replay path). Both seem legit, so commit both.

More logs around the configuration of the MC variants

Really diplay cmake parameters in the jenkins logs

Jenkins: display cmake parameters in the logs

Option model-checking OFF by default

Don't qwack when the default empty string is passed as a replay path

Revert "Also valgrind childs in CI, to valgrind MC apps"

This is already done in Tests.cmake (note so in my_valgrind.pl)

This reverts commit ee681140d428f4adb2cbfde207a04a4fc5a84b95.

Fix an initialization race around the AppSide

Fix make distcheck

Also valgrind childs in CI, to valgrind MC apps

Only compile stateless MC when libevent is found

Rename SIMGRID_HAVE_MC into SIMGRID_HAVE_STATEFUL_MC (so that MC can be optional again)

Fix non-MC builds when MC-only dependencies are missing

Compile the safe part of MC in default mode too

Safety properties (with no checkpointing) are not requiring anything
weird nowadays. Liveness properties, communication determinism and
state-equality reductions are not considered safe as they still need
some memory introspection black magic.

Try to please the ultramodern clang running on FreeBSD by properly giving a copy operator to the abstract class too

We should stop using the copy operator, and use a nice and clean
clone() call instead. Mathieu's on it.

Fix doc on how to select the compiler before compiling

Merge branch 'master' into 'master'

Guiding Backtrack in DFSExplorer

See merge request simgrid/simgrid!143

[gitlab-ci] Run "make distcheck-configure" for merge requests.

Allow to skip some stages of "make distcheck".

Now:
* "make distcheck-archive" only checks the archive
* "make distcheck-configure" also runs cmake et checks the file MANIFEST.in
* "make distcheck" depends on the previous stages, and runs the full build+install+tests

Correctly select the clang compiler on gitlab CI

Gitlab CI: Use clang on modelchecker builds, for MRs

Fix clang builds

Add a small implementation note in MC

Merge branch 'master' into 'master'

Add battery plugin and fix DAG doc

See merge request simgrid/simgrid!142

Add battery plugin and fix DAG doc

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

Rename guide as strategy and fix counter-example display with recipe

Replace state copy with recipe: list of transition to replay a state

Cosmetics (help project_description.sh) [ci-skip].

[jenkins] Remove stale sockets from simgrid-mc.

Add missing file

Change opened states for a priority queue

Abide by both compiler warnings

Now handle random transition and multiple times transitions

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

Activate the stdobject test now that it works

Don't set a really short timeout on sendsend now that this test works

Revert "Revalidate tesh files now that safety checking is based on reforks"

We can revert this, as we don't re-initialize again and again the
application in refork mode. Instead, we fork a pre-initialized app.

This reverts commit b2a9ee8e090af818cca9e72cd0e44fa1b91586b0.

Implement reforks by forking the application, to save the app exec time

Instead of forking from the checker and exec()ing the application, we
now fork+exec an application that we use as a proxy to the real
application process.

When we need a new application process, we fork it from the proxy,
which is much faster as it's already initialized.

The extra complexity is when the socket closes abruptly on the Checker
side, which means that the application died. We cannot waitpid() on
the app directly, as it's our grandchild. So, we have to ask the proxy
to do the waitpid for us and return the status.

Allow up to 30 elements in ENUM_CLASS

memset 0 the memory that is sent over the network

MC protocol: rename INITIAL_ADDRESSES msg to NEED_MEMINFO

Actually, now that the appside is not ptraced, there is no point killing it

Closing the socket is enough; it will exit on its self.

Also, there is no point waitpid()ing it, as the libevent loop is
already doing so.