From f6d8d2887c6d27a88f70455e07c5e2a8cdeb171d Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Mon, 11 May 2015 09:41:04 +0200
Subject: [PATCH] [Documentation] Move documentation where it belongs
---
tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java | 13 +++++++++++++
tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java | 11 -----------
2 files changed, 13 insertions(+), 11 deletions(-)
diff --git a/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java
index f4d8f9f86..cc84b78fa 100644
--- a/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java
@@ -39,6 +39,19 @@ public class LSBDiskFPSet extends HeapBasedDiskFPSet {
int cnt = (int) tblCnt.get();
Assert.check(cnt > 0, EC.GENERAL);
+ // Why not sort this.tbl in-place rather than doubling memory
+ // requirements by copying to clone array and subsequently sorting it?
+ // - disk written fps are marked disk written by changing msb to 1
+ // - next time such a fp from the in-memory this.tlb is converted on the
+ // fly back and again used to do an in-memory lookup
+ //
+ // - this.tbl bucket assignment (hashing) is done on least significant bits,
+ // which makes in-place sort with overlay index infeasible
+ // - erasing this.tbl means we will loose the in-memory cache completely until it fills up again
+ // - new fps overwrite disk flushed fps in-memory
+ // see MSBDiskFPSet for an implementation that doesn't have the
+ // requirement to sort in a clone array.
+
// copy table contents into a buffer array buff; do not erase tbl
buff = new long[cnt];
int idx = 0;
diff --git a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
index d78d75bb5..3d724c0dd 100644
--- a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
@@ -71,17 +71,6 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
*/
protected void prepareTable() {
- // Why not sort this.tbl in-place rather than doubling memory
- // requirements by copying to clone array and subsequently sorting it?
- // - disk written fps are marked disk written by changing msb to 1
- // - next time such a fp from the in-memory this.tlb is converted on the
- // fly back and again used to do an in-memory lookup
- //
- // - this.tbl bucket assignment (hashing) is done on least significant bits,
- // which makes in-place sort with overlay index infeasible
- // - erasing this.tbl means we will loose the in-memory cache completely until it fills up again
- // - new fps overwrite disk flushed fps in-memory
-
// copy table contents into a buffer array buff; do not erase tbl, but 1
// msb of each fp to indicate it has been flushed to disk
for (int j = 0; j < tbl.length; j++) {
--
GitLab