Rework BufferedRandomAccessFile

[Calvin-L]

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.

[lemmy]

Impressive!

[IamfromSpace]

It is interesting to me that most of these functions are about Arrays. Even WriteToFile and ExtendFile are relatively easy make generic array operations, maybe OverlapAt and TruncateOrExtendWith, where both take a placeholder as an argument. It may simply be worth making this an Array module, and then Common stays more focused on the spec itself WriteToFile(file, offset, data_to_write) == Array.Overlap(file, data_to_write, offset, ArbitarySymbol) (I have no idea why I felt compelled to reverse arguments).

I suppose, otherwise I was going to suggest that we add brief documentation on what the semantics of WriteToFile and ExtendFile were, but in many ways something like ExtendFile == Array.TurncateOrExtendWith(file, new_length, ArbitrarySymbol) does this for you.

[IamfromSpace]

I am probably overthinking these utility functions, but it struck me that maybe the most intuitive implementation involves slice & concat.

TruncateOrExtend(a, T, len) == IF len > ArrayLen(a) THEN ArrayConcat(a, Array(T, len - ArrayLen(a))) ELSE ArraySlice(a, 0, len)

OverlayAt(a1, a2, T, i) == ArrayConcat(TruncateOrExtend(a2, T, i), a2)

[lemmy]

Should any of those utility operators be contributed as an Array module to our CommunityModules?

[Calvin-L]

I added some simple documentation to these operators.

but it struck me that maybe the most intuitive implementation involves slice & concat

I agree that the current definitions are a little ugly. I wrote them after one or two failed attempts to come up with simpler definitions.

The ones you've given are certainly cleaner than my early attempts, and I will adopt your definition for TruncateOrExtend. But I might keep the definition I wrote for WriteToFile. The equivalent definition in terms of other operators is actually fairly cryptic (your definition for OverlayAt needs to include the portion of the contents after the written data if the contents were not written at the end of the array):

WriteToFile(file, offset, data_to_write) ==
    ArrayConcat(ArrayConcat(
        TruncateOrExtendFile(file, offset),
        data_to_write),
        ArraySlice(file, offset + ArrayLen(data_to_write), ArrayLen(file)))

Should any of those utility operators be contributed as an Array module to our CommunityModules?

Yes! I'll look into doing that soon.

[IamfromSpace]

your definition for OverlayAt needs to include the portion of the contents after the written data if the contents were not written at the end of the array

Whoops! Easy to make things simpler if you forget the critical parts 😆

[IamfromSpace]

Just wanted to say that I have absolutely found it useful to have a spec of the class for review, and especially as a refinement.

[lemmy]

This spec could also be referenced at tlaplus/examples

[Calvin-L]

Thanks a ton @IamfromSpace for the feedback!

I think I've addressed all the major comments so far.

[IamfromSpace]

These updates look great! For the sake of thoroughness I still have a few comments coming through on tests, but nothing of real concern. Just wrapped up the unit tests, but it's taking me a bit longer to digest the fuzzing file :)

[IamfromSpace]

Alrighty, that's 100% everything from me :) I think there's some test comments that are worth a look over, but there's certainly no deal-breakers in there, so I've got the approval on there now. Not sure if the repo is configured to reset on changes or not, but if so, I'll keep it active for any commits that come in.

Nice work on this!

[lemmy]

I won't have time to review this PR anytime soon and I don't want to be a bottleneck. Given @IamfromSpace's review, I feel confident about this PR. @Calvin-L, feel free to merge or consider inviting additional reviewers at the TLA+ Community Meeting in two weeks. Reviewing the spec offers a great opportunity for those unfamiliar with or not fond of Java to contribute to the TLA+ tools.