Force the use of sleep sets with ODPOR

GitHub action: update to actions/checkout@v3

Adjust tesh tests according to changes in deps.

A number of tests were affected by the previous
additions that labeled transitions executed by
the same actor as dependent. The appropriate
modifications were made to the expected outputs
and a "sanity" check was performed before making
them

Mark transitions run by the same actor as dependent

This commit adds a missing component to a number of
transition classes. Transitions that are executed by
the same actor are inherently dependent; but only the
RandomTransition actually checked for this case! This
caused ODPOR to search traces incorrectly under the
assumption that transitions which were actually
dependent were independent

Fix subtle bug in ~_E computation

The computation for the action ~_E requires
that we compute whether `p` is independent with
some sequence of transitions `w` after an
execution `E`. The algorithm for computing
whether an equivalent trace was found works
to iteratively eliminate events from the
equivalent sequence, leaving behind only
the remaining "bits" that are needed for
insertion into a wakeup tree.

The bug involved a typo of `w` for `w_now`
:( :( which broke everything :/

add python bindings for operations

Add remaining handlers to ReversibleRaceCalculator

This commit adds handlers for each type of transition
to ReversibleRaceCalculator which, as the name suggests,
determines whether a reversible race exists between two
events e1 and e2 based on the type of transition found
at e2. The full semantics have not been added for each
type of transition and will need to be added in the future

Resolve misconception with ODPOR pseudocode impl.

Like the SDPOR implementation before it, the ODPOR
implementation suffered from a similar fault in its
implementation. Determining whether an insertion was
necessary into a wakeup tree for some point in the
past requires determining whether the sleep set and
the set of weak initials overlap one another. If
their intersection is the empty set, THEN we attempt
to insert an actor. The prior implementation attempted
to find the first such actor that was not contained
in the sleep set, but this is semantically different

Resolve misconception with SDPOR pseudocode impl.

This commits fixes a semantics mismatch between
the implementation and the pseudocode in SDPOR.
The trouble was that we didn't stop searching
for an initial when we noticed that ANY initial
was contained in the backtrack set; instead, we
simply searched until we found ANY initial contained
OUTSIDE OF the backtrack set. The latter is not
equivalent to the former, so SDPOR was doing
more work than necessary.

A similar implementation issue is also present in
ODPOR which will be resolved in due time.

Fix subtle bug in Execution regeneration in DFSExplorer

Prior to this commit, during state regeneration,
we had used the state's `get_transition_out()`
method to refill the `Execution` instance bound
to DFSExplorer (`execution_seq_`). The trouble
is that this is an **unstable** source of truth:
it should not be trusted to regenerate an execution.
Instead, the `get_transition_in()` method should
be used on the state which follows. Intuitively,
both methods should be equivalent, which is why
the bug was overlooked for so long. Now that the
execution is correct and that SDPOR/ODPOR are
based on the correct sources of truth, things
are moving along more nicely and the two algorithms
appear to behave more sanely.

In addition to the above bug fix, this commit adds
a return value to the `insert()` function of the
`WakeupTree` class. This extra information is used
in debug logs to get a better idea of what ODPOR
is doing during its insertion. Similar debug information
will be added to SDPOR in subsequent phases.

Keep pointers to transitions instead of slices

Prior to this commit, sleep sets contained slices

Fix two minor bugs in the ODPOR implementation

This commit fixes the following two bugs:

1. When seeding a wakeup tree for the first
time, we forgot to add a `break` statement
to ensure that only one such enabled thread
were placed into the wakeup tree. Before
all such enabled threads were inserted which
amounted to what would have been a brute-force
search :(.

2. When determining whether a sequence is a
candidate for insertion into a wakeup tree,
we may need to check, for all enabled actors
in a given state, whether those actors'
next steps are independent with the sequence
theretofore constructed. This additional
step peforms the work needed to check whether
those actors are contained in the set of
*weak* initials. The method corresponds
to line 6 of the pseudocode of the ODPOR algorithm

Please Sonar and scan-build.

Make ASan ignore more odr-violations.

Fix some sonar issues in includes, after upgrade to c++17.

Disable implicit conversions in nlohmann/json.

See https://github.com/nlohmann/json#implicit-conversions

Add reversible race implementations for Comm actions

Add reversible race calculator

Determining whether or not a race between
two events is reversible is a critical component
of ODPOR. It turns out that we need to specialize
the race detection to the action types themselves.
Knowing the types of the transitions will help us
determine whether the race is reversible.

Add non-trivial insertion test

move handling of remote disks to platform parsing.
they should be accessible without having to load the filesystem plugin.
only the notion of mounting point really pertains to the plugin

add accessors

Specialize the Activity on_veto, on_suspend and on_resume in AnyActivity to ease the matching

Hide a bit an internal method (make it protected)

easy cleanup

Give the on_this_ variant to all VM signals

Sort the signals on the plugin page

+ also fix some documentation errors

Rename Resource::on_state_change to Resource::on_onoff for sake of clarity

Use the right version for the deprecate macro

Give the _this_ variants to the Link signals

Ignore ASan warnings about odr-violation with Activity_T::on_completion.

These are false positives IIUC.

[ci-skip]

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

Various cleanups in the Host signals

- Add a on_this_*_cb variant to the Host signals
- Rename Activity::on_{suspended,resumed} for symmetry with Actor signals
- Change kernel::activity::CpuAction::on_state_change to s4u::Host::on_exec_state_change

Remove global variables in PageStore_test too (mimic Snapshot_test).

Use C++17 features: std::scoped_lock and structured bindings.

Use the "_t" and "_v" version of type traits.

Compact namespaces.

C++17 support is now required for public headers too.

Update ChangeLog, FindSimGrid.cmake, and sonar-project.properties.

Add tests for initials and independence for Execution

add Io operations and an example

Add first round of execution independence tests

This commit adds the first set of tests for
checking whether a particular transition `t` is
independent with an extension `w` of an execution
sequence `E`. This is needed to determine whether
the transition `t` satisfies condition (2) of the
procedure outlined in the ODPOR paper for testing
whether `v ~_[E] w` holds between two sequences

another try to please clang

try to solve the -Wundefined-var-template thing with clang

allow operation to execute more than one function at start and end

add missing override

have a on_completion per activity type to save users some dynamic_cast-based filtering

Add instance signals for all Disk signals

Add instance signals for all Actor signals

no need to save all ns3 sink points

Rename cfg 'ns3/TcpModel' to 'ns3/UdpModel'

Test that setting ns3 TCP models actually work

cosmetics in the ChangeLog

 allow activities launched by maestro to be instrumented

throw on_send and on_receive signals when doing a host-to-host Comm
this is needed by instrumentation

allow to set tracing category in STARTING state

Add test for removing the first single-process subtree

This commit adds the first test checking whether
removing the first single-process node from the
tree produces the correct results, viz. that the
resulting tree is the same as before save for the
missing branch

Begin adding tests for subtree rooting

Add detailed stress test for WakeupTree

This commit introduces an edge case wherein
a "different looking sequence" ultimately is
already accounted for by a sequence contained
in the tree that "eventually could be made to
look like it" (viz. such that `~_E` holds
between the two sequences). Other stress tests
will be added for the other methods on the
WakeupTree and the Execution to test their
correctness. There is a long way to go

Begin first round of in-depth tests for WakeupTree

Explicitly capture required scope variables (sonar).

Get rid of global variables for snapshot tests.

Also fix some sonar issues.

Add first "working" version of ODPOR

This commit introduces the first version of
ODPOR which detects a bug using the example
programs found in SimGrid's test suite! There
is still work to be done (e.g. dealing with
transitions that have multiple possible
paths of execution such as MCRandom() will
be non-trivial to resolve).

The key adjustments in this commit are
to the WakeupTree structure itself. Gone
are the days when each node in the tree
maintained a sequence of transitions to
execute; instead, each node contains only
a single transition, and its the paths between
a node and the root that describe the partial
executions that ODPOR needs to explore.
This resulted from a misconception I had about
the structure of wakeup trees. When an insertion
is made, potentially a *chain* of leaf nodes
are added into the tree. This ensures we always
have a single-process branch to pick (which
is what we expected) and greatly improves the
readability of some of the methods found in
State.cpp related to ODPOR

fix example photovoltaic

add photovoltaic plugin

Add tests before changes to WakeupTree structure

Reduce scope for variables.

Don't shadow outer variables.

Use plain pointers instead of references to pointer.

Add some strategies and fix the semantics of Max/MinMatch

Add first round of extensive docs to ODPOR methods

Add test files for WakeupTree

Add explicit ODPOR clean-up phase to DFSExplorer

ODPOR requires that we remove elements from the
wakeup tree and add elements to the sleep sets
at state in the execution only AFTER we've
completed fully the recursive exploration of the
space pointed towards by the wakeup trees; i.e.,
we only remove subtrees and add to the sleep sets
when we're walking back UP the state stack looking
for a point to recontinue the execution.

Add ODPOR "backtracking" logic

Add ODPOR extension computation (lines 4-6)

ODPOR asks us to compute, for each reversible
race in the current maximal execution `E`,
whether some subsequence `v` of events
extending a prefix `E'` of `E` should be
inserted into a wakeup tree.

There's a few subtle details that should
be noted in this computation. ODPOR asks
us to compute `notdep(e, E)`, which means
possibly looking at events that occur
*after* `e'` and THEN adding `proc(e')`.
The subtlety lies in the fact that the
actual transition associated with `e'`
must be added AFTER all of the others.
We got lucky with SDPOR since next_E_p
was already in the last position and
thus required no special treatment. With
ODPOR, we have to be more careful.

Even more subtle is the observation that
any events in `notdep(e, E)` can neither
affect the enabledness of `e'` nor can
`e'` affect the enabledness of any of
those events, or else if they do
affect the enabledness of `e'` they
will necessarily be contained "between"
`e` and `e'`

Use `std::shared_ptr<Transition>` for Execution

Prior to this commit, the `Execution` class
maintained raw pointers to the transitions
maintained by the stack used in DFSExplorer.
Instead, we opt for the execution to contain
a collection of shared pointers to facilitate
the creation of partial executions

Add ODPOR race detection phase rough-draft

ODPOR is decoposed into two parts: the "passive"
observer phase, where ODPOR selects search points
based on the work it did before to fill in its
wakeup trees, and the active race-detection phase,
where ODPOR looks at all reversible races in an
execution and performs the work to determine if
new traces need be searched. This commit adds
in an outline for the latter phase. Note that
there is still much work to be done with respect
to the race detection -- we still need to implement
the partial execution function for example.

Likewise, handling the issue of multiple execution
possibilities for a given process will be particularly
tricky.

Add boolean check for wakeup tree initialization

While not great, one way to prevent the wakeup
tree from continuing to add elements after it
has already done so when empty is to add a
boolean flag that's checked to prevent the
addition. For now, we'll live with it

Automatically remove nodes from parents

After removing a node from a WakeupTree,
we need to be careful to also have any references
to the node removed, viz. that held onto the
parent of the node in the list of children.
This commit adds a back reference to the
parent node of a given WakeupTreeNode to
allow removal from the parent when destroyed.

Additionally, some bugs were fixed for creating
subtrees and removing subtrees (we forgot to remove
the root for example)

Add tree pruning/subtree methods to State

ODPOR requires that we can remove a
subtree from a wakeup tree as we continue
the exploration. Further, we must also be
able to create a subtree from a given
wakeup tree. The functionality for those
methods has already been added; this commit
instead introduces the management of wakeup
trees specifically in the context of ODPOR
exploration.

Add skeleton for expansion phase of ODPOR

Add logic for subtree node removal

ODPOR also mandates that subtrees be removed
from a wakeup tree after having finished searching
"in the direction" of the subtree. This commit
adds a method to WakeupTree which, given a handle
to a node in the tree, removes the subtree rooted at
that node.

Finish post-order travesal with WakeupTreeIterator

The WakeupTreeIterator is now full implemented:
we now properly add nodes to the top of the
stack in reverse order, resulting in a post-order
traversal as desired.

One subtlety arose with the implementation: the
root node is not contained in the list of any
other node in the tree. To handle this issue,
a "fake" list managed by the iterator was added
into which the root is placed at construction-time.
This prevents us from needing to change any of the
logic, and we can simply treat the root as any other
node in the traversal

Add logic for subtree extraction from wakeup trees

Extracting a subtree from a wakeup tree is required
for ODPOR to continue its search and to pass information
down to the other paths that ODPOR decides to visit.
Extracting a copy of a subtree is difficult as it
requires a deep copy of the tree, making sure
that references to any nodes in the tree that is copied
are copied appropriately. One additional subtlety is that
the subtree can only be taken with respect to single-process
branches and, further, that that process is removed from
each descendant of the node that contains the single process.

Add complicated computation of v ~_E w to Execution

The relation `v ~_E w` is used when traversing
a WakeupTree to determine is an "equivalent"
execution is already noted in the tree. This commit
adds the first "working" implementation of
several components to this process, viz.

1. Assuming that iteration has been implemented
(which is to come in future commits), the WakeupTree
now implements the `insert_E(v, B)` operation, where
`B` refers to the tree instance itself.

2. The `Execution` class can now determine what
is needed to complete the `insert()` operation,
specifically determining first if a) two sequences
`v` and `w` are related by `v ~_E w` and b)
what the smallest sequence `w'` is such that
`w [= v.w'`. The latter computation uses the neat
observation that (w / v) is the smallest such
sequence (viz. removing anything in `w` that's in
`v` "one at a time") and computes this value as
it is in the process of determining whether the
`~_E` relation noted holds

Add skeleton of implementation for tree insertion

The `insert` method on a Wakeup tree is an
essential component of the ODPOR algorithm.
Tree insertion guides the ODPOR algorithm
towards the unique, unsearched traces of the
state space. Insertion is based heavily on the
correctness of computing the `~` relation over
a given execution. Subsequent commits will fill
in this method as well as several others that
will be needed to implement that functionality

Add WakeupTreeIterator and WakeupTree skeletons

Add more docmentation for get_first_sdpor_initial()

A very important function at the center of SDPOR
was missing significant context that would help
a reader understand what exactly was going on
with the function. What makes the situation tricky
is the fact that the pseudocode's implementation
is blended into several lines and computed "on the
fly" rather than fully.

Suprious brace (fix non-linux builds).

Define master_socket_name only once, and embed it with the request to fork.

Try harder not to fail with stale sockets after several runs.

* on linux, prefer abstract unix sockets that are automatically removed
* otherwise, remove possible stale socket before bind

The default destructor should be fine.

Add more documentation to ClockVector/Execution

Add unit tests for ClockVector

Fix MANIFEST.in

We should note that the Execution that's a part of
both ODPOR and SDPOR is now contained in DFSExplorer
even in stateless execution. This will likely eventually
be true also for ODPOR; hence, the ODPOR sources
have been added to the SRC_MC_STATELESS portion as
needed

Integrate SDPOR into `model-check/reduction` flag

SDPOR and ODPOR can be used as part of the
DFSExplorer (ODPOR should integrate with some
minor details in the DFS implementation, but that's
for a later PR). This commit replaces the simple
`with_dpor` boolean flag used to control the
reduction with the more precise `ReductionMode`
that is newly extracted from within `DFSExplorer`
and is instead made "public"

Add more documentation to essential SDPOR methods

Modify tesh suite expectations with changes to dependencies

Fix ObjectAccess dependency check

The ObjectAccess transition should defer
dependency computation to the ActorJoin action.
Previously, it only decided dependency by
simply checking if the `other` transition
were simply another object access on the
same object

Fix subtlety with SDPOR/ODPOR initials

Computing initials for SDPOR/ODPOR requires
extending a search with respect to
a prefix of an execution. Previously, events
added to the extension were referred to by
their location within the larger execution
from which the prefix was taken. The problem
is that the new events need to be referred
to by their position relative to the
*extension* of the prefix; otherwise,
asking about "happens-before" in the extension
while using their handles in the full execution
will give incorrect results

Fix two off-by-one errors with clock vectors

Two errors were identified with managing clock
vectors in the Execution class. The index
assigned to the new transition was previously
`size() + 1` when it should have read `size()`.
Furthermore, the loop for checking "happens-between"
events excluded event 0. Both issues are now resolved
and a test with a race at the beginning was added
as verification

Mark `ActorJoin` dependent with `target_`

The `ActorJoin` transition was previously
labeled as independent with all other
transitions, including those of the actor
upon which the join acted. However, this
assumption was faulty: the join action is
instead dependent with ANY transition executed
by the actor joined upon, as the action
BECOMES enabled only as soon as the last action
run by the actor is executed.