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, 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 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
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
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...
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.
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 [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.
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.
Maxwell Pirtle [Wed, 1 Feb 2023 13:52:53 +0000 (14:52 +0100)]
Add patch for arm64 Ubuntu 22.04 in UnwindContext
The `mcontext_t` struct on Ubuntu 22.04
running on arm64 is missing the `fregs`
field. This causes a compilation failure
in `src/mc/inspect/mc_unw.cpp` since the
code there assumes the field exists on
linux-arm64.
This commit adds a new CMake variable
SIMGRID_PROCESSOR_arm64 to account for
the additional architecture more
explicitly and to better fit the context
surrounding the code where the fix was made