From e5fe78c52b6f55df1e88fea24c09189958ec1f5e Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Sat, 9 May 2015 12:34:07 +0200
Subject: [PATCH] [Bugfix] Stop NoSuchElementException during distributed
 modelchecking.

TLCIterator#getLast does not return the last element when the largest
fingerprint that is *not* on disk fails to be in the last non-null
bucket. This case however, is perfectly valid. Its likelyhood is
increased when checkpointing is enabled. Then the buckets are flushed in
shorter intervals causing a higher chance that the last bucket has only
on-disk fingerprints in it when getLast() is called.
---
 tlatools/src/tlc2/tool/fp/DiskFPSet.java      |  8 ++-
 tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java   | 30 +++++---
 .../tlc2/tool/fp/DummyFPSetConfiguration.java |  4 ++
 .../test/tlc2/tool/fp/MSBDiskFPSetTest2.java  | 68 ++++++++++++++++++-
 4 files changed, 98 insertions(+), 12 deletions(-)

diff --git a/tlatools/src/tlc2/tool/fp/DiskFPSet.java b/tlatools/src/tlc2/tool/fp/DiskFPSet.java
index 276a9b9eb..a6bc57708 100644
--- a/tlatools/src/tlc2/tool/fp/DiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/DiskFPSet.java
@@ -745,7 +745,13 @@ public abstract class DiskFPSet extends FPSet implements FPSetStatistic {
 	 * @see tlc2.tool.fp.FPSet#checkFPs()
 	 */
 	public final double checkFPs() throws IOException {
-		flusher.flushTable(); // No need for any lock here
+		// It seems pointless to acquire the locks when checkFPs is only
+		// executed after model checking has finished. Sill lock the disk
+		// fingerprint sets though. Acquiring the locks is cheap.
+		rwLock.acquireAllLocks();
+		flusher.flushTable();
+		rwLock.releaseAllLocks();
+
 		RandomAccessFile braf = new BufferedRandomAccessFile(
 				this.fpFilename, "r");
 		long fileLen = braf.length();
diff --git a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
index 7442e0107..d78d75bb5 100644
--- a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
@@ -110,7 +110,7 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
 		protected void mergeNewEntries(RandomAccessFile inRAF, RandomAccessFile outRAF) throws IOException {
 			final long buffLen = tblCnt.get();
 			final TLCIterator itr = new TLCIterator(tbl);
-	
+
 			// Precompute the maximum value of the new file
 			long maxVal = itr.getLast();
 			if (index != null) {
@@ -295,18 +295,28 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
 			int len = buff.length - 1;
 			long[] bucket = buff[len];
 
-			// find last bucket containing elements, buff elements might be null if
-			// no fingerprint for such an index has been added to the DiskFPSet
-			while (bucket == null) {
+			// Walk from the end of buff to the beginning. Each bucket that is
+			// found and non-null (null if no fingerprint for such an index has
+			// been added to the DiskFPSet) is checked for a valid fingerprint.
+			// A fp is valid iff it is larger zero. A zero fingerprint slot
+			// indicates an unoccupied slot, while a negative one corresponds to
+			// a fp that has already been flushed to disk.
+			while (len > 0) {
 				bucket = buff[--len];
-			}
-			
-			// find last element > 0 in bucket
-			for (int i = bucket.length - 1; i >= 0 ;i--) {
-				if (bucket[i] > 0) {
-					return bucket[i];
+
+				// Find last element > 0 in bucket (negative elements have already
+				// been flushed to disk, zero indicates an unoccupied slot).
+				if (bucket != null) {
+					for (int i = bucket.length - 1; i >= 0; i--) {
+						if (bucket[i] > 0) {
+							return bucket[i];
+						}
+					}
 				}
 			}
+			// At this point we have scanned the complete buff, but haven't
+			// found a single fingerprint that hasn't been flushed to disk
+			// already.
 			throw new NoSuchElementException();
 		}
 		
diff --git a/tlatools/test/tlc2/tool/fp/DummyFPSetConfiguration.java b/tlatools/test/tlc2/tool/fp/DummyFPSetConfiguration.java
index 9ec82cbeb..4d7a26d8a 100644
--- a/tlatools/test/tlc2/tool/fp/DummyFPSetConfiguration.java
+++ b/tlatools/test/tlc2/tool/fp/DummyFPSetConfiguration.java
@@ -14,4 +14,8 @@ public class DummyFPSetConfiguration extends FPSetConfiguration {
 		// which unit tests might have to tear down.
 		return memoryInBytes;
 	}
+	
+	public void setMemoryInFingerprintCnt(int numberOfFingerprints) {
+		this.memoryInBytes = numberOfFingerprints * FPSet.LongSize;
+	}
 }
diff --git a/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java b/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
index 660109d0b..3a8b45495 100644
--- a/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
+++ b/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
@@ -1,10 +1,14 @@
 // Copyright (c) 2012 Markus Alexander Kuppe. All rights reserved.
 package tlc2.tool.fp;
 
+import java.io.IOException;
 import java.rmi.RemoteException;
+import java.util.NoSuchElementException;
+
+import tlc2.tool.fp.MSBDiskFPSet.TLCIterator;
 
 public class MSBDiskFPSetTest2 extends AbstractHeapBasedDiskFPSetTest {
-	
+
 	/* (non-Javadoc)
 	 * @see tlc2.tool.fp.HeapBasedDiskFPSetTest#getDiskFPSet(tlc2.tool.fp.FPSetConfiguration)
 	 */
@@ -25,4 +29,66 @@ public class MSBDiskFPSetTest2 extends AbstractHeapBasedDiskFPSetTest {
 	protected long getUpperLimit() {
 		return 1L << 31;
 	}
+	
+	public void testGetLast() throws IOException {
+		final MSBDiskFPSet msbDiskFPSet = getMSBDiskFPSet();
+		
+		// Add the largest possible fingerprint into the fpset. It will end up
+		// in the largest bucket. Check that the MSB iterator returns it.
+		final long highFP = 1L << 62;
+		msbDiskFPSet.put(highFP);
+		TLCIterator tlcIterator = new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+		assertEquals(highFP, tlcIterator.getLast());
+		
+		// Flush the set to disk (simulating e.g. a checkpoint), a new iterator
+		// won't find the element anymore because it intentionally only searches
+		// for elements that are *not* on disk.
+		msbDiskFPSet.flusher.flushTable();
+		new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+		try {
+			tlcIterator.getLast();
+		} catch (NoSuchElementException e) {
+			// This exception is expected.
+			
+			// Now add the smallest possible element into the set. It will end
+			// up in the smallest bucket.
+			final long lowFP = 1;
+			msbDiskFPSet.put(lowFP);
+			// check that the iterator finds it as the last element.
+			tlcIterator = new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+			assertEquals(lowFP, tlcIterator.getLast());
+			return;
+		}
+		fail();
+	}
+
+	/*
+	 * Try to get the last element with no elements in the set.
+	 */
+	public void testGetLastNoBuckets() throws IOException {
+		final MSBDiskFPSet msbDiskFPSet = getMSBDiskFPSet();
+		
+
+		TLCIterator tlcIterator = new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+		try {
+			tlcIterator.getLast();
+		} catch (NoSuchElementException e) {
+			return;
+		}
+		fail();
+	}
+
+	private MSBDiskFPSet getMSBDiskFPSet() throws RemoteException, IOException {
+		// Create an MSBDiskFPSet usable in this unit test with memory allocated
+		// to store 100 fingerprints.
+		final DummyFPSetConfiguration fpSetConfig = new DummyFPSetConfiguration();
+		fpSetConfig.setMemoryInFingerprintCnt(100);
+		assertEquals(100, fpSetConfig.getMemoryInFingerprintCnt());
+		
+		final String filename = getClass().getName() + System.currentTimeMillis();
+
+		final MSBDiskFPSet msbDiskFPSet = (MSBDiskFPSet) getDiskFPSet(fpSetConfig);
+		msbDiskFPSet.init(1, System.getProperty("java.io.tmpdir"), filename);
+		return msbDiskFPSet;
+	}
 }
-- 
GitLab