Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add class for eventual "happens-before" computations
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Mon, 24 Apr 2023 12:55:12 +0000 (14:55 +0200)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 12 May 2023 13:58:22 +0000 (15:58 +0200)
commit9d23bfe5e8febe2b55c45e7fcd72d50644fac6ca
treeabf9a663b9615465e82f1bf30d81d2a653fe601f
parent68701a14f6323155ceb9a0af8e82679cd10fe8ae
Add class for eventual "happens-before" computations

Computing the "happens-before" relation over
a sequence of executions is an important step
in determining whether or not DPOR (and SDPOR
alike) needs to add a backtracking point.
This commit introduces the "ClockVector"
class which acts effectively as a light
wrapping around an `unordered_map` mapping
actor ids to integer values.

The essential component of the ClockVector
class is that its contents are "implicit"
in the sense that actors for which no
value is explicitly contained in the map
are assigned to the value `0` by default.
This allows clock vectors to be flexible
enough to support the creation of new
actors and the enabling/disabling of old
actors as they come and go.
MANIFEST.in
src/mc/api/ClockVector.cpp [new file with mode: 0644]
src/mc/api/ClockVector.hpp [new file with mode: 0644]
tools/cmake/DefinePackages.cmake