Warning: DiskFPSet.mergeNewEntries: xxx is already on disk with hangup

following. Use double precision when calculating `tblScalingFactor` to avoid rounding issues in `Indexer#getIdx`. These rounding issues can lead to critical errors, such as the largest fingerprints being incorrectly mapped to lower indices instead of the highest index. This problem occurs intermittently for specific ranges of positions within the interval `(0, Integer.MAX_VALUE)`. Part of Github issue #1112 #1112 [Bug][TLC] Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Jan 16, 2025 · 11c1711 · 11c1711
1 parent ad438c1
commit 11c1711
Show file tree

Hide file tree

Showing 3 changed files with 75 additions and 2 deletions.
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java
@@ -610,7 +610,7 @@ public Indexer(final long positions, final int fpBits) {
 		public Indexer(final long positions, final int fpBits, final long maxFingerprint) {
 			this.positions = positions;
 			// (position-1L) because array is zero indexed.
-			this.tblScalingFactor = (positions - 1L) / ((maxFingerprint - minFingerprint) * 1f);
+			this.tblScalingFactor = (positions - 1L) / ((maxFingerprint - minFingerprint) * 1d);
 		}
 
 		protected long getIdx(final long fp) {

diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/fp/LongArraysTest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/fp/LongArraysTest.java
@@ -622,8 +622,8 @@ public void test7() {
 		final List<Long> expected = new ArrayList<Long>();
 		expected.add(1L);
 		expected.add(0L);
-		expected.add(4L);
 		expected.add(0L);
+		expected.add(4L);
 		expected.add(6L);
 		expected.add(0L);
 		expected.add(0L);

diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/fp/OffHeapIndexerTest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/fp/OffHeapIndexerTest.java
@@ -122,6 +122,79 @@ public void testRescale299() throws RemoteException {
 		Assert.assertEquals(0, indexer.getIdx((0xFFFFFFFFFFFFFFFFL >>> fpBits), (int)positions+1));
 	}
 
+	@Test
+	public void testRescaleMany() throws RemoteException {
+		for (int fpBits = 1; fpBits < 3; fpBits++) {
+			final long maxFP = 0xFFFFFFFFFFFFFFFFL >>> fpBits;
+			for (long p = 1L; p < Integer.MAX_VALUE; p++) {
+				final Indexer indexer = new OffHeapDiskFPSet.Indexer(p, fpBits);
+
+				// indexer spreads over all positions
+				Assert.assertEquals(0, indexer.getIdx(1));
+				Assert.assertEquals(p - 1, indexer.getIdx(maxFP));
+
+				// Correctly wraps around when end of array is reached
+				Assert.assertEquals(0, indexer.getIdx(maxFP, 1));
+				// Correctly wraps around when end of array is reached twice
+				Assert.assertEquals(0, indexer.getIdx(maxFP, (int) p + 1));
+			}
+		}
+	}
+
+	@Test
+	public void testRescale1_2013265920() throws RemoteException {
+		final int fpBits = 1;
+		final long positions = 2013265920L; // -XX:MaxDirectMemorySize=30720M as in Github issue #1112
+
+		final Indexer indexer = new OffHeapDiskFPSet.Indexer(positions, fpBits);
+
+		// indexer spreads over all positions
+		Assert.assertEquals(0, indexer.getIdx(1));
+		final long maxFP = 0xFFFFFFFFFFFFFFFFL >>> fpBits;
+		Assert.assertEquals(positions - 1, indexer.getIdx(maxFP));
+
+		// Correctly wraps around when end of array is reached
+		Assert.assertEquals(0, indexer.getIdx(maxFP, 1));
+		// Correctly wraps around when end of array is reached twice
+		Assert.assertEquals(0, indexer.getIdx(maxFP, (int) positions + 1));
+	}
+
+	@Test
+	public void testRescale1_1207959552() throws RemoteException {
+		final int fpBits = 1;
+		final long positions = 1207959552L;
+
+		final Indexer indexer = new OffHeapDiskFPSet.Indexer(positions, fpBits);
+
+		// indexer spreads over all positions
+		Assert.assertEquals(0, indexer.getIdx(1));
+		final long maxFP = 0xFFFFFFFFFFFFFFFFL >>> fpBits;
+		Assert.assertEquals(positions - 1, indexer.getIdx(maxFP));
+
+		// Correctly wraps around when end of array is reached
+		Assert.assertEquals(0, indexer.getIdx(maxFP, 1));
+		// Correctly wraps around when end of array is reached twice
+		Assert.assertEquals(0, indexer.getIdx(maxFP, (int) positions + 1));
+	}
+
+	@Test
+	public void testShift1_268435456() throws RemoteException {
+		final int fpBits = 1;
+		final long positions = 268435456L;
+
+		final Indexer indexer = new OffHeapDiskFPSet.BitshiftingIndexer(positions, fpBits);
+
+		// indexer spreads over all positions
+		Assert.assertEquals(0, indexer.getIdx(1));
+		long maxFP = 0xFFFFFFFFFFFFFFFFL >>> fpBits;
+		Assert.assertEquals(positions - 1, indexer.getIdx(maxFP));
+
+		// Correctly wraps around when end of array is reached
+		Assert.assertEquals(0, indexer.getIdx(maxFP, 1));
+		// Correctly wraps around when end of array is reached twice
+		Assert.assertEquals(0, indexer.getIdx(maxFP, (int) positions + 1));
+	}
+
 	@Test
 	public void testRescaleMaximum() throws RemoteException {
 		final int fpBits = 1;