Attribute "printf" for ModelChecker::dot_output.

Don't throw an exception from destructor.

boost::circular_buffer_space_optimized::pop_back() may throw std::bad_alloc

C++17 is required since commit d5718258083be61d600e55b70915ccca43666e0f.

Reduce depth of nested statements

Don't give write permissions to others with mkdir.

Use "std::vector" instead of C-style array (sonar).

Avoid to send/receive zero-size messages.

There seems to be something broken with them on freebsd.

Update tesh file.

(follows commit 9b1267b59e70deb98dbf69b1231f597ed292aaaf)

Misc cosmetics for sonar.

Remove temporary object (sonar).

Declare functions "const" (sonar).

Make parameters pointer/reference-to-const (sonar).

Kill redundant blank lines (codefactor.io)

[ci-skip]

[ci-skip] try to help gcovr find files (it needs to be run in the same dir as gcc)

MC: apply some sonar advices

Fix the fixme (inline templated struct).

Unused include.

remove spurious debug message and warning

update teshes

multiple attemps to tune behavior of read/write_all

fix mpi_file set/get view to set shared pointer properly and return disp

update file pointer to match shared one after shared calls when needed

seek and other calls must use number of elements and not bytes displacement

update teshes as there are now more seek calls

smpi io: restore position after calls which should not modify it (add seek calls which are not ideal but harmless)

s4u filesystem: correctly update size of files when changed

intercept getpid call in SMPI, to provide internal PID instead of same of for all processes.

implement MPI_File_get_type_extent, MPI_File_s/get_atomicity, MPI_File_get_byte_offset

filesystem, correctly update file size when seeking past it

Don't test statequality: it's ~15h w/o DPOR and hard to optimize

Correctly disable DPOR when StateEq reduction is enabled

Add the teshfiles to the archive even when MC is disabled

Add tests of state equality reduction and nodpor for DFS explo

kill a parameter that is always true

mc:DFSExplo: cosmetics in the backtracking

Merge mc_safety.hpp into DFSExplorer class

Useless cosmetics while trying to understand that code

Integrate the (WIP) hashing logic in the Snapshot object

Small cleanups in mc::Snapshot

Finish the removal of mc::api by moving the last bits to the side

I would prefer to directly kill the templated structure, but I fail to
write a correct comparison lambda because it's used over a
std::vector<std::unique_ptr<simgrid::mc::VisitedState>>

All my attempts lead to either "no conversion to std::unique_ptr<VisitedState>",
or an error saying that I try to copy a unique_ptr when my lambda
takes unique_ptr as a parameter.

Please someone better at C++ than I am, please kill it.

Move mc:api::get_remote_heap_bytes() to RemoteProcess

Convert simgrid::mc::snapshot_equal() into Snapshot::operator==()

Also inline 2 more functions from mc::api

Move the dot_output global into ModelChecker

Make the RemoteApp a field of the Exploration, and sanitize initialization

Simplify the MC initialization code

only 3 more functions to go in mc::api

Kill another mc::api function

Pass the remote app as a parameter to all exploration signals

When we'll have reforks in the future, the remote app may change
during the exploration, so we don't want to seal the current remote
app in the callback closure. We want to use the fresh one instead.

Kill 2 more functions from mc::api

Move the automaton from mc::api to Liveness. An ugly trick is needed :(

See the comment in Liveness.hpp for the full details on that trick.

log_state has nothing to do in RemoteApp, it belongs to the exploration

Sanitize MC finalization process and inline a function

Kill mc::api::get_remote_app()

Kill another function of mc::api

Kill an unimplemented declaration

Convert Api::get_maxpid() into RemoteApp::get_maxpid()

The patch is a bit complex because RemoteApp is not a singleton, and
because I converted some pointers to references on the way.

Merge an initialization function into the constructor

Rename mc::Session into mc::api::RemoteApp

[ci-skip] activate ccache on sanitizer builds

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

Ensure that the verified application still works if get_max_consider() is not called at a given depth

This can happen after a backtrack: the Checker already knows how many
times this can be considered, but the App was reset in between so it
forgot.

So, make get_max_consider() const, and do the initialization in the
observer constructor, where it belongs. Too bad for the tiny little
tiny loss of performance compared to the lazy initialization.

[ci-skip] Flags - let's see if this trailing whitespace was breaking everything..

[ci-skip] use ccache on flags build as well.
Restrict build to two nodes with enough disk space, as it's expected to be costly

Kill a now useless variable

sanitize things around FINALIZE_REPLY despite my laziness as it seems to break on FreeBSD

Fix SMPI builds by reintroducing a killed MC function that it actually use

MC further cleanups (let it compile, this time)

MC: rename a file to sort out the mess

And now cleanup the App-side of cruft that was needed for Checker to read actor informations

Finally kill mc::RemoteProcess::actors(). We now communicate the data over the wire instead of reading it directly

Give read access to a private field

inline a function, kill a file

Well the last rogue call to RemoteProcess::actors() was easy actually

try to hide something under the rug for now

remove useless field

fix build for clang <15

Liveness: rename graph_state -> app_state and automaton_state -> prop_state

further reduce the amount of call sites for RemoteProcess::actors()

small cosmetics to not spread unrelated logic all around the file

MC: make it clear that we only have the info about the ready-to-run actors in a given mc::State

This is very similar to the exploration algorithm in Simix, but that's
still counter-intuitive when you try to understand the code.

Let's hope that writting it this way will help me not falling into
that trap anymore :)

Reduce the amount of MC locations reading the memory of the App

We still read the remote memory, but (almost) only when creating a new
State representing that state of the App. The goal is then to get
those info through message passing instead of through memory reading.
That should help reducing the bizarre things done by the MC, maybe
allowing to run the App in valgrind or so.

As a side effect, the exploration code becomes much more readable by
using the info from the mc::State instead of invocking low-level
things to retrive those info.

ignore new deprecation warning on freebsd

use ccache for main ci build.
It should be available on every builder, so skip detection phase. Will be added if/when needed

Fix RST formatting + one URL in Release_Notes.rst

If there is no LOCK in mmalloc anymore, then there is no need for atfork

Remove the need of pthread_mutex in mmalloc, to allow its use with sthread

Historically, mmalloc was used in all case when MC was activated at
build time (even if MC was not involved at runtime), forcing this
protection against race conditions for e.g. parallel simulations.

But nowadays, mmalloc is only activated at runtime in the verified
application. In other runtime setups, mmalloc uses the libc's malloc
implem instead of itself (that's why we use dlsym in the
initialization of mmalloc, to find the replacement).

So, removing this code should have no impact whatsoever.
Only maybe speeding up the verification a tiny bit.

And now, sthread becomes usable in conjunction with Mc Simgrid!!!

Given the current poor coverage of the pthread API, we can't verify
any useful program, but at least we have a valid (and rather robust)
prototype of such a verification tool.

Stick to dwarf-4 for MC builds.

TODO: add support for dwarf-5

Kill useless complexity in mmalloc: one of the dlsym

dlsym is not necessary to retrieve the LD_PRELOAD-injected symbol.

The killed code was intended to be used in libsimgrid, trying to
detect when libsgmalloc was already in memory to use that copy
instead. But that's useless: LD_PRELOAD ensures that the copy of the
injected version is the only existing one in the process.

In addition, that may resolve stability issues that my previous commit
didn't solve as nicely on the build daemons than on my laptop with gcc.

Allow dlsym to call free() on memory that is allocated before mmalloc init

dlsym obviously uses malloc, but we use dlsym while initializing
mmalloc, so we have a static buffer somewhere to give the required
memory to dlsym while mmalloc is not ready to serve. That's old.

Now, since the recent change in mmalloc, dlsym seems to not only
malloc some memory, but it also frees some of the obtained memory.
This commit detects when this happens and react gracefully (by
ignoring the free on that memory) instead of verbosely dying.

more protection for non linux builds

Disable mmap privatization if MUSL is detected, as it segfaults and we don't really care.
Hack a way of detecting musl, which is not really ideal but should work.

Another attempt at PRELOADing mmalloc (WIP)

Try to have mmalloc both in the simgrid library (for the regular use)
and also as an external library that can be LD_PRELOADed before
sthread too.

We'll have two copies of the library when actually preloading it in
sthread, but in this case, we use dlsym(RTDL_NEXT) to find the first
loaded symbol in memory to have only one mheap in the process.

It still segfault when launching a sthread code within simgrid-mc as
follows:
   bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=lib/libsgmalloc.so:lib/libsthread.soexamples/sthread/pthread-mutex-simple
but at least it should fix the breakage found on FreeBSD.

Merge branch 'adegomme-master-patch-16995' into 'master'

SMPI/replay: Fix issue with recv of size =0.

See merge request simgrid/simgrid!116

SMPI/replay: Fix issue with recv of size =0.
Negative values can be used to trigger a probe in case of unknown receive size, but 0 is a legit value.

Merge branch 'support-sendrecv-ti' into 'master'

Quick and dirty support of SendRecv in time-independent traces

See merge request simgrid/simgrid!115

Fix build error due to clang-format reordering the headers

Split mmalloc in a separate library

The idea is to allow to preload mmalloc before sthread, that must come
before simgrid itself.

Further small simplifications to mmalloc, killing dead code

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

Separate mmalloc from xbt

This is too bad that we cannot THROW on double free anymore, but we'll
have to live with it if we want to move mmalloc to libsthread.so