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

diff --git a/MANIFEST.in b/MANIFEST.in
index 4418185..0863de7 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2220,6 +2220,8 @@ include src/mc/explo/udpor/StateManager.cpp
 include src/mc/explo/udpor/StateManager.hpp
 include src/mc/explo/udpor/UnfoldingEvent.cpp
 include src/mc/explo/udpor/UnfoldingEvent.hpp
+include src/mc/explo/udpor/Unfolding.cpp
+include src/mc/explo/udpor/Unfolding.hpp
 include src/plugins/ProducerConsumer.cpp
 include src/plugins/chaos_monkey.cpp
 include src/plugins/file_system/s4u_FileSystem.cpp

diff --git a/src/mc/explo/udpor/Unfolding.cpp b/src/mc/explo/udpor/Unfolding.cpp
new file mode 100644 (file)
index 0000000..68fff48
--- /dev/null
+++ b/src/mc/explo/udpor/Unfolding.cpp
@@ -0,0 +1,36 @@
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/Unfolding.hpp"
+
+#include <stdexcept>
+
+namespace simgrid::mc::udpor {
+
+void Unfolding::remove(UnfoldingEvent* e)
+{
+  if (e == nullptr) {
+    throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL");
+  }
+  this->global_events_.erase(e);
+}
+
+void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
+{
+  UnfoldingEvent* handle = e.get();
+  auto loc               = this->global_events_.find(handle);
+  if (loc == this->global_events_.end()) {
+    // This is bad: someone wrapped the raw event address twice
+    // in two different unique ptrs and attempted to
+    // insert it into the unfolding...
+    throw std::invalid_argument("Attempted to insert an unfolding event owned twice."
+                                "This will result in a  double free error and must be fixed.");
+  }
+
+  // Map the handle to its owner
+  this->global_events_[handle] = std::move(e);
+}
+
+} // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/Unfolding.hpp b/src/mc/explo/udpor/Unfolding.hpp
new file mode 100644 (file)
index 0000000..471e043
--- /dev/null
+++ b/src/mc/explo/udpor/Unfolding.hpp
@@ -0,0 +1,42 @@
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved.          */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
+#define SIMGRID_MC_UDPOR_UNFOLDING_HPP
+
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/udpor_forward.hpp"
+
+#include <memory>
+#include <unordered_map>
+
+namespace simgrid::mc::udpor {
+
+class Unfolding {
+private:
+  /**
+   * @brief All of the events that are currently are a part of the unfolding
+   *
+   * @invariant Each unfolding event maps itself to the owner of that event,
+   * i.e. the unique pointer that owns the address. The Unfolding owns all
+   * of the addresses that are referenced by EventSet instances and Configuration
+   * instances. UDPOR guarantees that events are persisted for as long as necessary
+   */
+  std::unordered_map<UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
+
+public:
+  Unfolding()                       = default;
+  Unfolding& operator=(Unfolding&&) = default;
+  Unfolding(Unfolding&&)            = default;
+
+  void remove(UnfoldingEvent* e);
+  void insert(std::unique_ptr<UnfoldingEvent> e);
+
+  size_t size() const { return this->global_events_.size(); }
+  bool empty() const { return this->global_events_.empty(); }
+};
+
+} // namespace simgrid::mc::udpor
+#endif

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index b47df34..0746dc4 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -533,6 +533,8 @@ set(MC_SRC
   src/mc/explo/udpor/StateManager.hpp
   src/mc/explo/udpor/UnfoldingEvent.cpp
   src/mc/explo/udpor/UnfoldingEvent.hpp
+  src/mc/explo/udpor/Unfolding.cpp
+  src/mc/explo/udpor/Unfolding.hpp
   
   src/mc/inspect/DwarfExpression.cpp
   src/mc/inspect/DwarfExpression.hpp