attempt reclaimer_none, Storage2 edits

Author: fhackett

omnilink/package.mill

@@ -50,21 +50,14 @@ def hppOverlay: T[PathRef] = Task:
   PathRef(overlay)
 end hppOverlay
 
-def staticOverlayUnsafe: T[PathRef] = Task.Source(os.sub / "static_overlay.nix")
+def staticOverlay: T[PathRef] = Task.Source(os.sub / "static_overlay.nix")
 
 def dependOnEntireModuleDir: T[Seq[PathRef]] = Task.Input:
   os.list(build.omnilink.moduleDir)
     .filterNot(_.last.contains(".duckdb")) // exclude for _severe_ perf reasons
     .map(PathRef(_))
 end dependOnEntireModuleDir
 
-def staticOverlay: T[PathRef] = Task:
-  dependOnEntireModuleDir()
-  // Nix has its own dedup method, hammering its caching
-  // on every change should be fine.
-  staticOverlayUnsafe()
-end staticOverlay
-
 def pkgs: T[PathRef] = Task:
   val file = Task.dest / "pkgs.nix"
   val contents = s"""

omnilink/setbench/package.mill

@@ -43,6 +43,12 @@ object `package` extends Module:
       "omnilink.setbench.workload.brown_ext_chromatic_delegateSingle_lf"
   end brown_ext_chromatic_delegateSingle_lf
 
+  object brown_ext_chromatic_delegateSingle_lf_noreclaim
+      extends SetBenchTracingConfigModule:
+    def nixName =
+      "omnilink.setbench.workload.brown_ext_chromatic_delegateSingle_lf_noreclaim"
+  end brown_ext_chromatic_delegateSingle_lf_noreclaim
+
   object brown_ext_chromatic_delegateSingle_lf_bug1
       extends SetBenchTracingConfigModule:
     def nixName =

omnilink/setbench/workload.nix

@@ -8,6 +8,7 @@
   ghUrl ? "git@github.com:ubc-systopia/augmented-chromatic-trees.git",
   ghRev,
   setbenchSubdir,
+  shouldReclaimMemory ? true,
 }:
 let
   setbenchSrc = builtins.fetchGit {
@@ -32,6 +33,7 @@ stdenv.mkDerivation {
     cmake
   ];
   env.SETBENCH_SUBDIR = setbenchSubdir;
+  env.SETBENCH_SHOULD_RECLAIM_MEMORY = shouldReclaimMemory;
   sourceRoot = "workload";
   postInstall = ''
     chmod a+x $out/bin/main

omnilink/setbench/workload/CMakeLists.txt

@@ -21,6 +21,9 @@ target_include_directories(main PRIVATE
   "../source/$ENV{SETBENCH_SUBDIR}"
 )
 target_link_libraries(main msgpack-cxx OmniLink::OmniLink)
+if($ENV{SETBENCH_SHOULD_RECLAIM_MEMORY})
+  target_compile_definitions(main PRIVATE SETBENCH_SHOULD_RECLAIM_MEMORY)
+endif()
 
 install(DIRECTORY ${PROJECT_BINARY_DIR}/main
   DESTINATION bin

omnilink/setbench/workload/main.cpp

@@ -23,7 +23,11 @@ thread_local int tid = 0;
 
 #include "adapter.h"
 
+#ifdef SETBENCH_SHOULD_RECLAIM_MEMORY
 using DataStructure = ds_adapter<int32_t, int32_t>;
+#else
+using DataStructure = ds_adapter<int32_t, int32_t, reclaimer_none<int32_t>>;
+#endif
 
 struct context_init_t {
     DataStructure& ds;

omnilink/static_overlay.nix

@@ -52,6 +52,11 @@ final: prev: {
         ghRev = "9a8c04ccdaefb2d4ab893367f7ff99a593d51aa6"; # main as of paper sub
         setbenchSubdir = "ds/brown_ext_chromatic_delegateSingle_lf";
       };
+      brown_ext_chromatic_delegateSingle_lf_noreclaim = final.callPackage ./setbench/workload.nix {
+        ghRev = "9a8c04ccdaefb2d4ab893367f7ff99a593d51aa6"; # main as of paper sub
+        setbenchSubdir = "ds/brown_ext_chromatic_delegateSingle_lf";
+        shouldReclaimMemory = false;
+      };
       brown_ext_chromatic_augment_lf_linbug1 = final.callPackage ./setbench/workload.nix {
         ghRev = "a99d464a7dd0e8958c2093b3143dc3f069803dc5";
         setbenchSubdir = "ds/brown_ext_chromatic_augment_lf";

omnilink/wiredtiger/MCStorage2.cfg

@@ -0,0 +1,17 @@
+SPECIFICATION RefinementSpec
+
+CONSTANTS
+    RC ="snapshot"
+    WC = "majority"
+
+    Keys = {k1, k2, k3}
+    MTxId = {t1, t2, t3}
+    Timestamps = {10, 20, 30}
+    Node = {"n"}
+    NoValue = NoValue
+
+CONSTRAINT StateConstraint
+
+PROPERTY IsRefinedByStorage
+
+SYMMETRY Symmetry

omnilink/wiredtiger/MCStorage2.tla

@@ -0,0 +1,15 @@
+---- MODULE MCStorage2 ----
+EXTENDS Storage2
+
+Storage == INSTANCE Storage
+
+IsRefinedByStorage ==
+    [][Next]_vars
+
+RefinementSpec ==
+    Storage!Init /\ [][Storage!Next]_vars
+
+StateConstraint ==
+    /\ Len(mlog["n"]) <= 3
+
+====

omnilink/wiredtiger/Storage.tla

@@ -81,7 +81,7 @@ LogEntries ==
 
 Logs == Seq(LogEntries)
 
-Max(S) == CHOOSE x \in S : \A y \in S : x >= y
+Max(S) == IF S = {} THEN 0 ELSE CHOOSE x \in S : \A y \in S : x >= y
 
 --------------------------------------------------------
 
@@ -92,9 +92,6 @@ CommitTimestamps(n) == {mlog[n][i].ts : i \in DOMAIN mlog[n]}
 
 ActiveReadTimestamps(n) == { IF ~mtxnSnapshots[n][tx]["active"] THEN 0 ELSE mtxnSnapshots[n][tx].ts : tx \in DOMAIN mtxnSnapshots[n]}
 
-\* Next timestamp to use for a transaction operation.
-NextTs(n) == Max(PrepareOrCommitTimestamps(n) \cup ActiveReadTimestamps(n)) + 1
-
 ActiveTransactions(n) == {tid \in MTxId : mtxnSnapshots[n][tid]["active"]}
 PreparedTransactions(n) == {tid \in ActiveTransactions(n) : mtxnSnapshots[n][tid].prepared}