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

fix the instructions on how to use local installs of python bindings

Fix the liveness tests by ignoring the Comm ID memory that breaks the state equality detection

Revalidate the tesh files after the recent MC depends change

Do not consider the memory addresses in MC depends function

There is no use for that, and it makes depends system-dependent.

MC: Give an ID to comms to not use their pointer value, that can be reused over time

Not doing so made the dependency architecture- and system- dependent:
if a pointer address got reused for another comm, that would have
impacted the depends() result on the MC side.

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

add a get_unique_data to Extendable and test it in one example

Explain the relevant PYTHONPATH when installing from source

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

A few spelling mistakes and many replacements: [Ss]imgrid -> SimGrid.

[ci-skip]

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

Revalidate the MC tesh files after the recent changes in the depend of wait and send

re-add --help-coll to the doc now that it's implemented

Fix missing fortran import

Respect member order according to the initialisation order

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

Fix test stats according to current dependency relation

Complete "smpirun -help" [ci-skip]

Another unw_accessor forgotten in previous commit.

Fix error: missing initializer for member unw_accessors::ptrauth_insn_mask

Seen with some version of libunwind.

Implement smpirun --help-coll.

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

Add function call and full location in checker-side transitions

Tiny doc improvement

improve the doc of how to select the right algorithm

Disable s4u-mc-bugged1-liveness-visited-ucontext only.

Sorry for the noise [ci-skip]

Disable liveness model-checking tests outside Linux.

It seems to fall in an infinite loop under FreeBSD for example.

[ci-skip]

Sometimes the expansion may work and the memory address should stay the same.

Merge branch 'udpor-phase8' into 'master'

Add `ex(C)` computations for remaining primitives

See merge request simgrid/simgrid!147

Only compute extensions for enabled events

Add events with implicit bottom event

A bug was caught whereby events of the
form MUTEX* were not added properly
when following the pseudocode directly.
The problem is that SimGrid does not
explicitly represent the "bottom" event
with which every event in an unfolding is
implicitly dependent; instead, events are
simply processed without it. The implication
is such that technically, all events would
have the "previously-executed event" as
the bottom event if it was the first action taken
by the actor in the configuration, while SimGrid
will return a `std::nullopt_t` if no such
action has been taken.

The solution is very simple: we simply
add the event without any dependencies
(representing the root event) if the
previous event can't be found for the
action. This is the case in the
other pseudocode that exists, but
is a bit more subtle when readingh the
pseudocode for mutexes

Add partial implementation for MutexWait/MutexTest

The full implementation for computing extension
sets for MutexWait and MutexTest was *almost*
added in this commit. Again, though, we need to
be able to determine dependecies in the context
of mutex transitions which implies we need to
be have more information from the application side.
This work will be added in subsequent commits

Add ex(C) computation for mutex lock/unlock

The pseudcode for computing the incremental
portion of the extension set for the transitions
MUTEX_ASYNC_LOCK and MUTEX_UNLOCK were partially
added. What's importantly missing is one key
element of detecting dependencies in the specific
configuration context between a MUTEX_UNLOCK and
a MUTEX_WAIT. This will also prove to be an issue
when implementing the corresponding function for
MUTEX_WAIT.

Add tentative implementation of CommTest ex(C) pseudocode

Reorder loop processing in CommWait ex(C) comp

Add "working" UDPOR on small examples with CommWait independence

In forcing each CommWait transition to be
independent with all other CommWait transitions as
assumed in The Anh Pham's thesis, UDPOR appears to
correctly identify the errors in the few programs
that are used to test SimGrid's model checking
component.

Add ex(C) example with a small program

Incorporating extension set computations into
unit tests is rather difficult, as it requires
effectively enumerating each step followed by
UDPOR during one of its computations. This
commit adds one such expansion for a very simple
program with two threads each running two actions,
resulting in a single Mazurkiewicz trace.

More tests will be added with more actors
as a stress test for the more elaborate conditions
checked for when computing extension sets for
CommWait

Add monotonically-increasing IDs for UnfoldingEvent

UDPOR is inherently non-deterministic in the
sense that multiple routes may exist that UDPOR
can follow from any given configuration. Correctness
and optimality are not affected by these results;
however, we seek for SimGrid to have a deterministic
execution on all platforms while running UDPOR.
Prior to this commit, arbitrarily the first event in
an unordered set was selected. But since the "first"
event in an unordered set is implementation-defined,
we seek to avoid leaving it up to the standard library's
ordering and define instead an ordering ourselves.

This motivates assigning a monotonically-increasing
ID to each newly-created event. Note that since
events may be created and then ultimately
destroyed after UDPOR realizes it has created a duplicate
event (which can happen when computing the extension
set of two configurations whose extension sets overlap),
events that exist in the unfolding need not contain
a contiguous range of IDs.

To provide a deterministic order, we must first process
the transitions that are enabled from any given state
in a determinstic order so that events are discovered
in a determinstic order. Furthermore, we must always
pick events from the intersection of en(C) and A in
a determinstic order. Here, we always pick events
with the smallest assigned ID first.

Expand sanity-check tests for CommSend/CommRecv transitions

A very, very basic test was added to ensure that
the most trivial program was treated correctly.
More tests will be added which will make for more
interesting scenarios. The difficulty lies with
creating the unfolding itself: there's no better
way than to do so manually and to follow along
with where UDPOR would take us...

Add preliminary basic tests for ex(C) computation

Testing the correctness of the computation for
extension sets is critical, as extension sets
guide the entire UDPOR search. Unfortunately it
is also very difficult to create tests for computing
the extension sets...

Factorize common code to cancel actions when a resource is turned off.

Merge branch 'master' into 'master'

Enhancing guiding strategies for McSimGrid

See merge request simgrid/simgrid!161

Fix CI tests

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

Better strategy documentation

Buffers should not be considered by CommWaitTransition::depends.

Update tesh files accordingly.

Use xbt::random instead of rand and srand

Better warning message for max-depth

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

Remove unused parameters (sonar).

Connect the right signal.

Declare functions "const" (sonar).

Another round of pointer-to-const for sonar.

Use xbt_die instead of xbt_assert(false).

Disable maybe throwing move constructor (sonar).

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

Sort MANIFEST.in.

[ci-skip]

Few more CI tesh fixing

Fix stat order for CI tests

Fix build without MC.

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

Fix Manifest.in

Clang-tidy: readability-qualified-auto.

Also add const qualifiers to pointers and references when possible.

Define classes with "class".

Postpone the destruction of Task::current_activity_.

Fixes heap-use-after-free spotted by ASan and valgrind.

Various cleanups in Task plugin.

* reduce number of calls to simcall_answered
* use xbt::signal for the "on_this_*" signals
* reduce scope for static member "inited"
* remove intrusive_ptr_* function for derived classes

Add factorisation for strategy and Use dynamic over static cast

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

Install package non-interactively on CI

Another struct/class mismatch between forward declaration and actual use

Enable the ODPOR/SDPOR tests in default builds also

Please clang by not defaulting a constructor that it will delete

odpor_tests_private.hpp:24:3: error: explicitly defaulted default constructor is implicitly deleted [-Werror,-Wdefaulted-function-deleted]
  DependentIfSameValueAction() = default;
    ^
odpor_tests_private.hpp:21:13: note: default constructor of 'DependentIfSameValueAction' is implicitly deleted because field 'value' of const-qualified type 'const int' would not be initialized
  const int value;
            ^

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

Fix stat missorder at the end of DFSexplorer

Cosmetics: whitespace cleanup (codefactor.io).

Call CommImpl::set_iface(nullptr) as soon as the comm is finished, and make TSan happy with s4u-app-masterworkers-parallel tests.

Merge branch 'fix-sonar-task' into 'master'

Fix sonar task

See merge request simgrid/simgrid!160

more sonar fix

fix sonar warnings

Merge branch 'odpor-clean-ups' into 'master'

Address Comments/Errors from ODPOR/SDPOR Integration

See merge request simgrid/simgrid!159

Fix RuntimeError: pybind11::handle::inc_ref() PyGILState_Check() failure.

See commit 2c2d94471739d82e9cbd370711f73377e0b17717 for details.

CI pages: try to use the Debian version of the python packages

Remove a test that was indended to show that this branch is never used

Complete missing docs for WakeupTreeNode

Add more documentation and fix forward declaration

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

Fix few typos and add random seed intializer

Use Debian:12 for our build deps

Merge branch 'rename-operation-task' into 'master'

rename operation to task

See merge request simgrid/simgrid!158

Merge branch 'odpor-implementation' into 'master'

Introduce SDPOR and ODPOR into Simgrid

See merge request simgrid/simgrid!154

fire on_start for one-sided communication instead of on_send/recv

add Comm::on_this_send and Comm::on_this_recv

[no-ci] indicate which methods and signals are static in the doc

[no-ci] precise which methods of the Actor class are static

This should be fixed now.

A deleted Comm cannot be a valid iface anymore.

rename operation to task. rename execute to fire.

properly remove the old signals and prevent MC to fire Comm::on_this_completion

react to the proper signals