Maxwell Pirtle [Mon, 20 Feb 2023 12:38:02 +0000 (13:38 +0100)]
Add first batch of tests for UDPOR
This commit adds tests for the UDPOR constructs
that will be used when UDPOR is finally implemented.
UDPOR will rely heavily on the correctness of
the methods herein and hereafter (in subsequent
commits) tested, so it is important that each function
be tested to the maximum extent possible
Maxwell Pirtle [Fri, 17 Feb 2023 12:59:59 +0000 (13:59 +0100)]
"Finalize" interface to UnfoldingEvent
The interface to the UnfoldingEvent was carried over
from the previous implementation of UDPOR in the
"tiny_simgrid" repository. However, the implementation
needed to be adjusted to better suit how SimGrid is
going to implement UDPOR. Instead of holding a string
tag identifying a transition, each UnfoldingEvent now
directly holds a reference to the transition from the
state prior.
This caused some changes to need to be made in the
UdporChecker.cpp. These changes have moved the pseudocode
of UDPOR one large step closer to the actual implementation
that will be brought to life over the next few weeks
Maxwell Pirtle [Fri, 17 Feb 2023 10:47:50 +0000 (11:47 +0100)]
Allow actor transitions to be shared
Transitions that were stored in `ActorState`
prior to this commit were stored as `std::unique_ptr`
instances. But UDPOR events need to hold
references to the transitions that they are
"associated with". While UDPOR will discard events
at the appropriate time, we want to make sure the
reference to the transition in some `ActorState`
(ultimately in some `State` instance) remains
valid event after UDPOR discard the State object.
This could e.g. be helpful while debugging
Maxwell Pirtle [Thu, 16 Feb 2023 09:32:42 +0000 (10:32 +0100)]
Add Unfolding data structure
The Unfolding data structure is used to
house all of the events UDPOR needs to maintain
as it searches through the unfolding. The
Unfolding may eventually also be used to store
and maintain state, although this technically
only needs to be delegated to the checker itself
as it performs its exploration
Maxwell Pirtle [Thu, 16 Feb 2023 09:10:01 +0000 (10:10 +0100)]
Add implementations for EventSet + Configurations
Maxwell Pirtle [Thu, 16 Feb 2023 08:10:23 +0000 (09:10 +0100)]
Add xbt_assert() for state handle overflow
With the StateManager, the current implementation
vends out integer handles that are referred to by
each UnfoldingEvent to map it to the appropriate
State.
A better API, however, may be to have a each event
manage its own state. We should verify first that
each UnfoldingEvent object corresponds to a unique
State object, but this may be the best option
Maxwell Pirtle [Tue, 14 Feb 2023 14:04:40 +0000 (15:04 +0100)]
Use std::unordered_set instead of std::set for EventSet
The ordering of the events in the set does not
matter in an EventSet. The std::unordered_set construct
is thus a better fit (std::set orders its elements).
While this disallows the use of the nice functions
in the standard library for forming unions etc.,
it is trivial to implement the functions `make_union()`
etc.
Maxwell Pirtle [Tue, 14 Feb 2023 13:53:44 +0000 (14:53 +0100)]
Move UDPOR constructs out of udpor_global.cpp
The udpor_global.hpp/cpp have been removed in
favor of seperate files for the primary
constructs that will be used in UDPOR. The source
files have been adjusted as necessary to allow
for a complete compilation
Maxwell Pirtle [Tue, 14 Feb 2023 13:20:10 +0000 (14:20 +0100)]
Add `udpor` directory under `mc/explo`
The `udpor` directory was created to better
house/separate all of the functionality that will
eventually be required by the UDPOR algorithm.
Currently, the files are not used as part of the
compilation process. Subsequent commits will remove
the `udpor_global.cpp` file and adjust the compilation
as necessary
Maxwell Pirtle [Tue, 14 Feb 2023 12:57:40 +0000 (13:57 +0100)]
Remove currently unused methods from udpor_globals
The udpor_globals.cpp file contained many currently
unused functions that were remove with this commit.
Subsequent commits will move the globals into more
relevant files under `explo`
Maxwell Pirtle [Tue, 14 Feb 2023 12:21:43 +0000 (13:21 +0100)]
Add minor clean ups
Maxwell Pirtle [Tue, 7 Feb 2023 14:04:09 +0000 (15:04 +0100)]
Add implementation for state management
Maxwell Pirtle [Tue, 7 Feb 2023 12:47:05 +0000 (13:47 +0100)]
Add incomplete implementations of udpor_globals.cpp
The classes EventSet, Configuration, and StateManager
have implementations added in order to allow SimGrid
to link properly. Future commits will provide actual
implementations for many of the TODOs that remain
Maxwell Pirtle [Mon, 6 Feb 2023 15:13:31 +0000 (16:13 +0100)]
Add `udpor` namespace
Maxwell Pirtle [Mon, 6 Feb 2023 14:30:44 +0000 (15:30 +0100)]
Begin porting implementation from tiny_simgrid
More of the structure of the current implementation
of the UDPOR algorithm was imported into SimGrid
with minor alterations to better fit the EventSet
class paradigm, along with some other cleaning up.
The next phase will be two-fold:
1. Importantly, state management will need to be
added into SimGrid. This shouldn't be too difficult,
assuming that we can follow a similar strategy as
The Pham had in tiny_simgrid of mapping State
objects to state id's and using those ids to later
manipulate the state. In SimGrid, the state will be
be used to manipulate the remote process to which
the Exploration has access, instead of manipulating
what's effectively a dummy object
2. Implementing most of the TODO functions
in EventSet etc. This functionality will come
in future commits.
Eventually, we'll want to make an iterative version
of UDPOR to prevent stack overflows, as it is likely
that the unfoldings of programs of any significant size
can get quite deep. For now, though, this is not
strictly necessary to get a first draft implemented
Maxwell Pirtle [Mon, 6 Feb 2023 10:54:40 +0000 (11:54 +0100)]
Add methods between EventSet and Configuration
The distinction between a Configuration and an
EventSet is a subtle one. Indeed, a configuration
in UDPOR is merely a set. There may be the opportunity
perhaps even to replace the Configuration class
with a typedef, although this may not be possible or
improve readability.
Maxwell Pirtle [Mon, 6 Feb 2023 08:37:54 +0000 (09:37 +0100)]
Convert EventSet into class from typedef
The EventSet object was simply typedef-ed to
a std::deque<UnfoldingEvent *>. While this
worked, it caused a lot of the code in tiny-simgrid
to be a bit more difficult to read since it
required the use of a more C-like idiom of passing
`this` as an explicit argument in EvtSetTools.
Effectively, the idea to absorb all of the EvtSetTools
methods into the EventSet class directly. This will
give a more natural C++ (instead of C) look to the
resulting code in the UDPOR algorithm
Arnaud Giersch [Mon, 20 Feb 2023 09:37:04 +0000 (10:37 +0100)]
Revert "Upgrade embedded xxhash (-> v0.8.1)."
It doesn't compile on arm64
This reverts commit
4127fe802ff334591a6ba5b315190523fc2a660e.
Arnaud Giersch [Mon, 20 Feb 2023 09:25:44 +0000 (09:25 +0000)]
Merge branch 'fix-probe' into 'master'
Send actor action probes one at a time
See merge request simgrid/simgrid!131
Maxwell Pirtle [Mon, 20 Feb 2023 08:41:16 +0000 (09:41 +0100)]
Send actor action probes one at a time
To avoid the scenario whereby the AppSide
delivers a message larger than the maximum
datagram side allowed by the application,
we instead send a single message for each actor.
This prevents us from needing to complicate the
sending logic in Channel.cpp, which would have
been made more complicated should we have wanted
to send variable-sized messages between the
checker and the application side
Martin Quinson [Sun, 19 Feb 2023 21:34:31 +0000 (22:34 +0100)]
Remove more occurences of 'surf' with uppercases
Martin Quinson [Sun, 19 Feb 2023 15:09:01 +0000 (16:09 +0100)]
Document that surf is gone
Arnaud Giersch [Sun, 19 Feb 2023 14:48:56 +0000 (15:48 +0100)]
Upgrade embedded xxhash (-> v0.8.1).
Taken from
https://github.com/RedSpah/xxhash_cpp/commit/
d21e37c34c4ad4ad562e4ec01ec036e342c422e3
Arnaud Giersch [Sun, 19 Feb 2023 14:37:48 +0000 (15:37 +0100)]
Upgrade embedded catch2 (-> v2.13.10).
Taken from
https://github.com/catchorg/Catch2/releases/tag/v2.13.10
Martin Quinson [Sun, 19 Feb 2023 14:45:51 +0000 (15:45 +0100)]
Finally kill surf_interface.hpp watched_host was actually useless
Martin Quinson [Sun, 19 Feb 2023 11:53:23 +0000 (12:53 +0100)]
rename another file with had 'surf' in its name
Martin Quinson [Sun, 19 Feb 2023 11:49:24 +0000 (12:49 +0100)]
Kill a file with 'surf' in its name, and further empty surf_interface.cpp
Martin Quinson [Sun, 19 Feb 2023 11:21:55 +0000 (12:21 +0100)]
Rework a comment (to remove 'surf')
Arnaud Giersch [Sun, 19 Feb 2023 08:37:22 +0000 (09:37 +0100)]
Rework compile optimizations for MC.
Arnaud Giersch [Sun, 19 Feb 2023 06:27:24 +0000 (07:27 +0100)]
Missing includes.
Arnaud Giersch [Sun, 19 Feb 2023 06:20:34 +0000 (07:20 +0100)]
Move -Wno-unused-local-typedefs to common flags.
It's supported by Clang too, and needed with at least ns-3.31.
Martin Quinson [Sat, 18 Feb 2023 21:48:39 +0000 (22:48 +0100)]
kill src/simix
Martin Quinson [Sat, 18 Feb 2023 21:44:30 +0000 (22:44 +0100)]
Move the non-deprecated bits of simix to kernel::actor::Simcall
Martin Quinson [Sat, 18 Feb 2023 20:49:57 +0000 (21:49 +0100)]
Kill src/include
The -Isrc/include makes it difficult to recognize in the source which
\#include takes a public header and which one is a private header.
Plus, move the third-party headers to a specific directory.
Martin Quinson [Sat, 18 Feb 2023 20:21:56 +0000 (21:21 +0100)]
reduce the amount of header includes in headers, to speedup recompilation
Martin Quinson [Sat, 18 Feb 2023 19:10:28 +0000 (20:10 +0100)]
Merge branch 'master' of framagit.org:simgrid/simgrid
Martin Quinson [Sat, 18 Feb 2023 18:37:22 +0000 (19:37 +0100)]
Remove an obsolete cmake warning
Martin Quinson [Sat, 18 Feb 2023 18:28:37 +0000 (19:28 +0100)]
Move some content of surf_interface to a new math_utils.h
Arnaud Giersch [Sat, 18 Feb 2023 18:04:03 +0000 (19:04 +0100)]
Update path.
Error also seen with clang 11 and ns3.31.
Martin Quinson [Sat, 18 Feb 2023 17:45:08 +0000 (18:45 +0100)]
Move the files related to the platform parsing to kernel/xml
Martin Quinson [Sat, 18 Feb 2023 17:32:11 +0000 (18:32 +0100)]
move a symbol declaration out of surf_interface.hpp
Martin Quinson [Sat, 18 Feb 2023 17:25:55 +0000 (18:25 +0100)]
CMake requires ns3 v3.28+, so don't work around a bug in v3.27
Martin Quinson [Sat, 18 Feb 2023 17:23:50 +0000 (18:23 +0100)]
Move the ns3 helper files to kernel/models/ns3
Martin Quinson [Sat, 18 Feb 2023 16:59:53 +0000 (17:59 +0100)]
Move the surf tesh tests with the other models' ones
Martin Quinson [Sat, 18 Feb 2023 16:31:27 +0000 (17:31 +0100)]
Remove some more occurence of 'surf' in comments and such
Arnaud Giersch [Sat, 18 Feb 2023 16:42:44 +0000 (17:42 +0100)]
Misc Sonar issues.
Arnaud Giersch [Sat, 18 Feb 2023 16:39:33 +0000 (17:39 +0100)]
Various cleanups.
Martin Quinson [Sat, 18 Feb 2023 16:21:27 +0000 (17:21 +0100)]
Further rename the identifiers of flexml to simgrid_parse_*
Martin Quinson [Sat, 18 Feb 2023 10:48:52 +0000 (11:48 +0100)]
Change the namespace of flexml-generated parser from surfxml to simgrid_parse
Martin Quinson [Sat, 18 Feb 2023 10:32:21 +0000 (11:32 +0100)]
Two more references of the surf/precision option name
Martin Quinson [Sat, 18 Feb 2023 10:07:33 +0000 (11:07 +0100)]
Remove surf from the content from the examples of simulated filesystems
Martin Quinson [Sat, 18 Feb 2023 09:38:38 +0000 (10:38 +0100)]
Rename ActivityImpl::surf_action_ to ActivityImpl::model_action_
Martin Quinson [Fri, 17 Feb 2023 22:02:54 +0000 (23:02 +0100)]
Move HostImpl to kernel/resource with its friends
Martin Quinson [Fri, 17 Feb 2023 21:31:02 +0000 (22:31 +0100)]
move the models to the right directory (empty src/surf a bit)
The remaining parts of src/surf need to be cleaned before being moved
Also, remove almost all #include "surf_interface.hpp"
Martin Quinson [Thu, 16 Feb 2023 23:05:18 +0000 (00:05 +0100)]
Allow precision/bmf as a synonym to bmf/precision
Martin Quinson [Thu, 16 Feb 2023 23:01:45 +0000 (00:01 +0100)]
Rename option maxmin/precision to precision/work-amount for clarity
Martin Quinson [Thu, 16 Feb 2023 22:44:37 +0000 (23:44 +0100)]
Rename option "surf/precision" to "precision/timing" for clarity.
Martin Quinson [Thu, 16 Feb 2023 22:39:54 +0000 (23:39 +0100)]
Rename sg_surf_precision to sg_precision_timing for clarity
Martin Quinson [Thu, 16 Feb 2023 22:31:53 +0000 (23:31 +0100)]
Use surf_precision as a value for PMPI_Wtick
the unit of maxmin_precision is in flops or bytes (that's an amount of
work) while the unit of surf_precision is in seconds (that's a time).
Martin Quinson [Thu, 16 Feb 2023 16:48:10 +0000 (17:48 +0100)]
doc: add a little graph about the host energy plugin
Martin Quinson [Thu, 16 Feb 2023 21:13:41 +0000 (21:13 +0000)]
Merge branch 'fix-mc-tests' into 'master'
Fix root node edge case for `State` instance
See merge request simgrid/simgrid!129
Maxwell Pirtle [Thu, 16 Feb 2023 14:51:37 +0000 (15:51 +0100)]
Initialize uninitialized transition for root state
The transition in the root state was uninitialized
and this appears to have caused the last of the remaining
issues with the test suite. Of course, reading from the
uninitialized pointer `transition_` is bound to cause
a bunch of problems...
Maxwell Pirtle [Thu, 16 Feb 2023 12:11:07 +0000 (13:11 +0100)]
Fix root-node edge cases for states
Martin Quinson [Thu, 16 Feb 2023 10:05:59 +0000 (11:05 +0100)]
fix MC+gcc builds
Martin Quinson [Thu, 16 Feb 2023 09:52:21 +0000 (10:52 +0100)]
CI: build the model-checker on framagit, to test the MRs
Martin Quinson [Thu, 16 Feb 2023 08:45:47 +0000 (09:45 +0100)]
fix the build (but not all tests) of MC
Martin Quinson [Wed, 15 Feb 2023 23:59:31 +0000 (23:59 +0000)]
Merge branch 'actor-comms' into 'master'
Serialize pending transitions when responding to `ACTOR_STATUS` messages on the application side
See merge request simgrid/simgrid!127
Martin Quinson [Wed, 15 Feb 2023 23:49:30 +0000 (00:49 +0100)]
properly deal with network/optim (end of the ModuleGroup cleanup)
The network/optim was abusing the model description mechanism, because
it was introduced before the options could be restricted to a list of
values. That's a pretty old cruft :)
Moreover, the config mechanism (probably) allowed network/optim:TI but then
ignored it silently. Not nice for the users.
Martin Quinson [Wed, 15 Feb 2023 23:31:13 +0000 (00:31 +0100)]
Kill a now useless file
Martin Quinson [Wed, 15 Feb 2023 23:26:24 +0000 (00:26 +0100)]
Cosmetics around the creation of the VM model
Martin Quinson [Wed, 15 Feb 2023 23:21:52 +0000 (00:21 +0100)]
Further factorization: introduce ModuleGroup::init_from_flag_value()
Martin Quinson [Wed, 15 Feb 2023 23:15:19 +0000 (00:15 +0100)]
15 years later, I finally managed to kill host/model:compound
Martin Quinson [Wed, 15 Feb 2023 22:41:33 +0000 (23:41 +0100)]
Objectif the disk model
Martin Quinson [Wed, 15 Feb 2023 22:31:53 +0000 (23:31 +0100)]
There is no way these names are empty, bc we give a default value
Martin Quinson [Wed, 15 Feb 2023 22:22:10 +0000 (23:22 +0100)]
Objectifies the host models
Martin Quinson [Wed, 15 Feb 2023 22:00:50 +0000 (23:00 +0100)]
factorize the flags of models and plugins
Martin Quinson [Wed, 15 Feb 2023 16:38:27 +0000 (17:38 +0100)]
docs: fix a sphinx formatting error
Martin Quinson [Wed, 15 Feb 2023 16:24:12 +0000 (17:24 +0100)]
Objectifies the CPU model
Martin Quinson [Wed, 15 Feb 2023 15:51:00 +0000 (16:51 +0100)]
Allow to add a disk to a host after a load_platform from xml
Fix https://github.com/simgrid/simgrid/issues/383
Maxwell Pirtle [Wed, 15 Feb 2023 09:55:14 +0000 (10:55 +0100)]
Add note about resetting `times_considered`
Resetting `times_considered` after multiple
serializations of a particular transition are performed
to give the checker all exections of an actor
that can perform multiple actions. There was concern
that this value would have to be "reset" to the
original value after the serialization, since the latter
modifies the simcall's observer's internal state.
However, no reset is actually needed as each
SIMCALL_EXECUTE message that the checker sends to the
application-side comes equipped with the latest
`times_considered`, and thus preparation will be
performed correctly before execution.
Maxwell Pirtle [Wed, 15 Feb 2023 09:50:16 +0000 (10:50 +0100)]
Replace pending transition with latest execution
The `State::execute_next(aid_t)` method was
adjusted to use the newest copy of the transition
that was executed by an actor in lieu of the
copy of the transition that was previously stored
by the actor, as more information may be gained
during the execution of a transition.
Martin Quinson [Wed, 15 Feb 2023 09:00:22 +0000 (10:00 +0100)]
fix pip build
Martin Quinson [Wed, 15 Feb 2023 08:30:06 +0000 (09:30 +0100)]
Convert the network models to the new plugin-like mechanism
Martin Quinson [Tue, 14 Feb 2023 20:12:10 +0000 (21:12 +0100)]
Objectify the model containers
This should allow further cleanups in the near future, where models
are handled as the plugins already are: no shotgun design anymore with
the registration, and everything about a given model contained in a
single file.
Martin Quinson [Sun, 12 Feb 2023 22:22:10 +0000 (23:22 +0100)]
Move the surf log categories elsewhere
Martin Quinson [Sat, 11 Feb 2023 23:25:30 +0000 (00:25 +0100)]
Remove multiarch from the doc: it was never tested, and 32b is soon gone
Martin Quinson [Sat, 11 Feb 2023 23:24:29 +0000 (00:24 +0100)]
Document the fact that 32bits is gone
Maxwell Pirtle [Tue, 14 Feb 2023 08:06:24 +0000 (09:06 +0100)]
Fix condition for XBT_DECLARE_ENUM_CLASS
The condition for the `is_valid_##EnumType`
was updated. Previously, is was missing the edge
case where `raw_value >= 0`
Arnaud Giersch [Mon, 13 Feb 2023 15:09:47 +0000 (16:09 +0100)]
Reduce scope for variables.
Arnaud Giersch [Mon, 13 Feb 2023 15:04:25 +0000 (16:04 +0100)]
Simplify initialization of the root log category.
Arnaud Giersch [Mon, 13 Feb 2023 08:49:37 +0000 (09:49 +0100)]
For Sonar.
Arnaud Giersch [Sat, 11 Feb 2023 18:25:25 +0000 (19:25 +0100)]
Define context related globals as static members of Context.
Arnaud Giersch [Sat, 11 Feb 2023 10:45:54 +0000 (11:45 +0100)]
Make global variables "const".
Even if it has no importance, take the special values from smpi.h
Maxwell Pirtle [Mon, 13 Feb 2023 09:48:20 +0000 (10:48 +0100)]
Finalize passing transitions during model checking
Transitions are now serialized and sent to the
checker side whenever a new State instance is
created (when the ACTOR_STATUS message is sent
by the checker). Transition serialization is the
first step before the work on the UDPOR branch(es)
can be integrated into Mc SimGrid.
Martin Quinson [Sat, 11 Feb 2023 23:11:57 +0000 (00:11 +0100)]
move the flatifier functions to the s4u::Engine, for public consumption
Martin Quinson [Sat, 11 Feb 2023 19:17:10 +0000 (20:17 +0100)]
Add a Link::get_concurrency_limit and use it in the flatifier
Martin Quinson [Sat, 11 Feb 2023 18:34:46 +0000 (19:34 +0100)]
Flatifier: make a function returning a std::string instead of using printf
Martin Quinson [Fri, 10 Feb 2023 22:30:50 +0000 (23:30 +0100)]
flatifier: cosmetics + display the real name of the root zone
Martin Quinson [Fri, 10 Feb 2023 18:39:45 +0000 (19:39 +0100)]
Fix attribution
Martin Quinson [Sun, 29 Jan 2023 16:20:16 +0000 (17:20 +0100)]
Document recent changes