diff --git a/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java index f4d8f9f86abc0cba8ec4a0ee8a1a141782eeb787..cc84b78fa149cdeee2dfbcd3bc27a3288526aabb 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 d78d75bb5cc421e9a85f21964b311dd21d18ea8a..3d724c0ddac363de753e78c6a2a302350dcb7f51 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++) {