-
-
Notifications
You must be signed in to change notification settings - Fork 187
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Java 21 causes TLC's BufferedRandomAccessFileTest and OffHeapDiskFPSetTest to fail #835
Comments
I'm looking at putting together a fix for this. I'm very impressed with the quality and clarity of tlaplus/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.java Line 55 in 7fcaceb
But, in reality, "The offset may be set beyond the end of the file". In JDK<21, I think fixing this issue will require relaxing the invariant that tlaplus/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.java Line 72 in 7fcaceb
|
@lemmy I discovered something else interesting while testing my changes. The tests include: @Test
public void testReadSeek() throws IOException {
final File tmpFile = File.createTempFile("BufferedRandomAccessFileTest_testReadSeek", ".bin");
tmpFile.deleteOnExit();
final java.io.RandomAccessFile raf = new BufferedRandomAccessFile(tmpFile, "rw");
raf.setLength(BufferedRandomAccessFile.BuffSz + 1L);
raf.seek(1);
for (int i = 0; i < BufferedRandomAccessFile.BuffSz / 8; i++) {
assertEquals(0L, raf.readLong());
}
raf.close();
} That test checks that
Do you know if any clients of |
I've reviewed the different fingerprint sets to refresh my memory. I recall that the |
This commit makes major alterations to `BufferedRandomAccessFile` to bring it in line with the general `RandomAccessFile` contract: - Invariant V1 has been strengthened to include a contract for the `length` field. - Invariants V2-V5 have been altered to account for cases where `curr > length`, which the `RandomAccessFile` contract allows. - Additionally, invariant V5 has been adjusted to clarify that `dirty=true` does not imply that there are unflushed bytes. The implication is only one-way: if there are unflushed bytes, then `dirty=true`. - The `hi` and `maxHi` fields have been removed. These largely duplicate information that can be quickly recomputed, meaning they add additional complexity to the class invariants. Without those fields, invariant V6 can be removed. - The `close()` method now closes the underlying file descriptor even if `flush()` throws an exception. Due to the complexity of this change, I have added a TLA+ specification for `BufferedRandomAccessFile` to enable model checking of its design. To ensure that the code is correct, this commit also adds a substantial amount of test infrastructure: - Several new regression tests have been added. These are a little cryptic because they were randomly generated, but they do reflect true behaviors of the `RandomAccessFile` contract. - A fuzz test has been added. This test ensures that many sequences of random operations behave correctly. It also minimizes failures so they can be easily converted to regression tests. This commit also makes some whitespace and formatting adjustments. Fixes #835. I have verified that the tests now pass under Java 21.
This commit makes major alterations to `BufferedRandomAccessFile` to bring it in line with the general `RandomAccessFile` contract: - Invariant V1 has been strengthened to include a contract for the `length` field. - Invariants V2-V5 have been altered to account for cases where `curr > length`, which the `RandomAccessFile` contract allows. - Additionally, invariant V5 has been adjusted to clarify that `dirty=true` does not imply that there are unflushed bytes. The implication is only one-way: if there are unflushed bytes, then `dirty=true`. - The `hi` and `maxHi` fields have been removed. These largely duplicate information that can be quickly recomputed, meaning they add additional complexity to the class invariants. Without those fields, invariant V6 can be removed. - The `close()` method now closes the underlying file descriptor even if `flush()` throws an exception. Due to the complexity of this change, I have added a TLA+ specification for `BufferedRandomAccessFile` to enable model checking of its design. To ensure that the code is correct, this commit also adds a substantial amount of test infrastructure: - Several new regression tests have been added. These are a little cryptic because they were randomly generated, but they do reflect true behaviors of the `RandomAccessFile` contract. - A fuzz test has been added. This test ensures that many sequences of random operations behave correctly. It also minimizes failures so they can be easily converted to regression tests. This commit also makes some whitespace and formatting adjustments. Fixes #835. I have verified that the tests now pass under Java 21. Signed-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>
Some methods such as
tlc2.util.BufferedRandomAccessFile#readLong
that used to throwIOException
have started to throwArrayIndexOutOfBoundsExceptions
.The text was updated successfully, but these errors were encountered: