Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add events with implicit bottom event
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Mon, 24 Apr 2023 07:01:59 +0000 (09:01 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 9 Jun 2023 08:01:51 +0000 (10:01 +0200)
commit1d2749010b8bc3bd6338abed1c4cbc2fdd9a8895
tree3b63bbd1075c2cdce366b36d90874ee997e75e99
parenta4961b3040827fe40c55635a0790a30008c2b054
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
src/mc/explo/UdporChecker.cpp
src/mc/explo/udpor/ExtensionSetCalculator.cpp
src/mc/transition/TransitionComm.cpp