Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add monotonically-increasing IDs for UnfoldingEvent
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Tue, 18 Apr 2023 08:17:51 +0000 (10:17 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 9 Jun 2023 07:58:43 +0000 (09:58 +0200)
commitaa013f7dd162e725e707dc8b191717562d541556
tree33c79231e9dc5222bd1296a2f67eb8111cdb1c46
parent8ae5f4cb7292df072ca7df70e5d4ff6791b04cdf
Add monotonically-increasing IDs for UnfoldingEvent

UDPOR is inherently non-deterministic in the
sense that multiple routes may exist that UDPOR
can follow from any given configuration. Correctness
and optimality are not affected by these results;
however, we seek for SimGrid to have a deterministic
execution on all platforms while running UDPOR.
Prior to this commit, arbitrarily the first event in
an unordered set was selected. But since the "first"
event in an unordered set is implementation-defined,
we seek to avoid leaving it up to the standard library's
ordering and define instead an ordering ourselves.

This motivates assigning a monotonically-increasing
ID to each newly-created event. Note that since
events may be created and then ultimately
destroyed after UDPOR realizes it has created a duplicate
event (which can happen when computing the extension
set of two configurations whose extension sets overlap),
events that exist in the unfolding need not contain
a contiguous range of IDs.

To provide a deterministic order, we must first process
the transitions that are enabled from any given state
in a determinstic order so that events are discovered
in a determinstic order. Furthermore, we must always
pick events from the intersection of en(C) and A in
a determinstic order. Here, we always pick events
with the smallest assigned ID first.
src/mc/explo/UdporChecker.cpp
src/mc/explo/udpor/EventSet.cpp
src/mc/explo/udpor/EventSet.hpp
src/mc/explo/udpor/ExtensionSetCalculator.cpp
src/mc/explo/udpor/UnfoldingEvent.cpp
src/mc/explo/udpor/UnfoldingEvent.hpp