---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/BufferedRandomAccessFile.tla
---
\* Copyright (c) 2024, Oracle and/or its affiliates.
----------------------- MODULE BufferedRandomAccessFile ------------------------
\* This is a model-checkable specification for BufferedRandomAccessFile.java.
\* It covers the core fields as well as the seek, read, write, flush, and
\* setLength operations.
\*
\* There are three major correctess conditions:
\*
\* (1) the internal invariants V1-V5 should hold
\* (2) the behavior should refine a general RandomAccessFile
\* (3) each operation should refine its RandomAccessFile counterpart
\*
\* Readers will probably want to start with the general RandomAccessFile spec
\* before reading this one.
EXTENDS Naturals, Sequences, TLC, Common
CONSTANT BuffSz
VARIABLES
\* in-memory variables (BufferedRandomAccessFile class fields)
dirty,
length,
curr,
lo,
buff,
diskPos,
\* the underlying file
file_content,
file_pointer
vars == <<
dirty, length, curr, lo, buff, diskPos,
file_content, file_pointer >>
TypeOK ==
/\ dirty \in BOOLEAN
/\ length \in Offset
/\ curr \in Offset
/\ lo \in Offset
/\ buff \in Array(SymbolOrArbitrary, BuffSz)
/\ diskPos \in Offset
/\ file_content \in ArrayOfAnyLength(SymbolOrArbitrary)
/\ ArrayLen(file_content) <= MaxOffset
/\ file_pointer \in Offset
--------------------------------------------------------------------------------
\* Internal invariants (copied from comment in BufferedRandomAccessFile.java)
RelevantBufferContent ==
ArraySlice(buff, 0, Min(BuffSz, length - lo))
LogicalFileContent == \* denoted c(f) in .java file
IF ArrayLen(RelevantBufferContent) > 0
THEN WriteToFile(file_content, lo, RelevantBufferContent)
ELSE file_content
DiskF(i) == \* denoted disk(f)[i] in .java file
IF i >= 0 /\ i < ArrayLen(file_content)
THEN ArrayGet(file_content, i)
ELSE ArbitrarySymbol
BufferedIndexes == lo..(Min(lo + BuffSz, length) - 1)
Inv1 ==
\* /\ f.closed == closed(f) \* close() not described in this spec
\* /\ f.curr == curr(f) \* by definition; see `file_pointer <- curr` in refinement mapping below
/\ length = ArrayLen(LogicalFileContent)
/\ diskPos = file_pointer
\* Inv2 is a bit special. Most methods restore it just before they return. It
\* is generally restored by calling `restoreInvariantsAfterIncreasingCurr()`.
\* But, that behavior is difficult to model in straight TLA+ because each
\* method may modify variables multiple times. So instead, this spec treats
\* Inv2 as a precondition for the methods and verifies that it is always
\* restored by calling `restoreInvariantsAfterIncreasingCurr()`.
\* See `Inv2CanAlwaysBeRestored` below.
Inv2 ==
/\ lo <= curr
/\ curr < lo + BuffSz
Inv3 ==
\A i \in BufferedIndexes:
ArrayGet(LogicalFileContent, i) = ArrayGet(buff, i - lo)
Inv4 ==
\A i \in 0..(length - 1):
i \notin BufferedIndexes =>
ArrayGet(LogicalFileContent, i) = DiskF(i)
Inv5 ==
(\E i \in BufferedIndexes: DiskF(i) /= ArrayGet(buff, i - lo)) =>
dirty
--------------------------------------------------------------------------------
\* Behavior
Init ==
/\ dirty = FALSE
/\ length = 0
/\ curr = 0
/\ lo = 0
/\ buff \in Array({ArbitrarySymbol}, BuffSz)
/\ diskPos = 0
/\ file_pointer = 0
/\ file_content = EmptyArray
FlushBuffer ==
/\ dirty
/\ LET len == Min(length - lo, BuffSz) IN
/\ IF len > 0
THEN LET diskPosA == lo IN \* super.seek(this.lo)
/\ file_content' = WriteToFile(file_content, diskPosA, ArraySlice(buff, 0, len))
/\ file_pointer' = diskPosA + len
/\ diskPos' = lo + len
ELSE
UNCHANGED << diskPos, file_pointer, file_content >>
/\ dirty' = FALSE
/\ UNCHANGED << length, curr, lo, buff >>
\* Helper for Seek (not a full action):
\* - reads lo'
\* - constrains diskPos', file_pointer', and buff'
FillBuffer ==
LET diskPosA == lo' IN
/\ buff' = MkArray(BuffSz, [i \in 0..BuffSz |->
LET fileOffset == diskPosA + i IN
IF fileOffset < ArrayLen(file_content)
THEN ArrayGet(file_content, fileOffset)
ELSE ArbitrarySymbol])
/\ file_pointer' = Min(diskPosA + BuffSz, ArrayLen(file_content))
/\ diskPos' = Min(diskPosA + BuffSz, ArrayLen(file_content))
Seek(pos) ==
/\ curr' = pos
/\ IF pos < lo \/ pos >= (lo + BuffSz) THEN
/\ ~dirty \* call to FlushBuffer
/\ lo' = (pos \div BuffSz) * BuffSz
/\ FillBuffer
ELSE
UNCHANGED << lo, diskPos, file_pointer, buff >>
/\ UNCHANGED << dirty, length, file_content >>
SetLength(newLength) ==
/\ file_content' = TruncateOrExtendFile(file_content, newLength)
/\ IF ArrayLen(file_content) > newLength /\ file_pointer > newLength
THEN file_pointer' = newLength
ELSE file_pointer' \in Offset
/\ length' = newLength
/\ diskPos' = file_pointer'
/\ IF curr > newLength
THEN curr' = newLength
ELSE UNCHANGED curr
\* In reality the buffer doesn't change---but some of its bytes might no
\* longer be relevant and have to be marked as arbitrary.
/\ buff' = MkArray(BuffSz, [i \in 0..(BuffSz - 1) |->
IF lo + i < newLength
THEN ArrayGet(buff, i)
ELSE ArbitrarySymbol])
/\ UNCHANGED << dirty, lo >>
Read1(byte) ==
/\ Inv2
/\ curr < length
/\ byte = ArrayGet(buff, curr - lo)
/\ curr' = curr + 1
/\ UNCHANGED << lo, diskPos, buff, file_pointer, dirty, file_content, length >>
Write1(byte) ==
/\ curr + 1 <= MaxOffset \* bound model checking
/\ Inv2
/\ buff' = ArraySet(buff, curr - lo, byte)
/\ curr' = curr + 1
/\ dirty' = TRUE
/\ length' = Max(length, curr')
/\ UNCHANGED << lo, diskPos, file_pointer, file_content >>
Read(data) ==
LET numReadableWithoutSeeking == Min(lo + BuffSz, length) - curr IN
/\ Inv2
/\ numReadableWithoutSeeking >= 0
/\ LET
numToRead == Min(ArrayLen(data), numReadableWithoutSeeking)
buffOff == curr - lo
IN
/\ data = ArraySlice(buff, buffOff, buffOff + numToRead)
/\ curr' = curr + numToRead
/\ UNCHANGED << buff, dirty, diskPos, file_content, file_pointer, length, lo >>
\* The `write()` method is composed of repeated calls to `writeAtMost()`, so
\* verifying that the latter maintains all our invariants should be sufficient.
WriteAtMost(data) ==
LET
numWriteableWithoutSeeking == Min(ArrayLen(data), lo + BuffSz - curr)
buffOff == curr - lo
IN
/\ Inv2
/\ curr + numWriteableWithoutSeeking <= MaxOffset
/\ buff' = ArrayConcat(ArrayConcat(
ArraySlice(buff, 0, buffOff),
ArraySlice(data, 0, numWriteableWithoutSeeking)),
ArraySlice(buff, buffOff + numWriteableWithoutSeeking, ArrayLen(buff)))
/\ dirty' = TRUE
/\ curr' = curr + numWriteableWithoutSeeking
/\ length' = Max(length, curr')
/\ UNCHANGED << lo, diskPos, file_content, file_pointer >>
Next ==
\/ FlushBuffer
\/ \E offset \in Offset:
\/ Seek(offset)
\/ SetLength(offset)
\/ \E symbol \in SymbolOrArbitrary:
\/ Read1(symbol)
\/ Write1(symbol)
\/ \E len \in 1..MaxOffset: \E data \in Array(SymbolOrArbitrary, len):
\/ WriteAtMost(data)
\/ Read(data)
Spec == Init /\ [][Next]_vars
--------------------------------------------------------------------------------
\* Refinement of general RandomAccessFile
RAF == INSTANCE RandomAccessFile WITH
file_content <- LogicalFileContent,
file_pointer <- curr
Safety == RAF!Spec
\* Ensure that the various actions behave according to their abstract specifications.
FlushBufferCorrect == [][FlushBuffer => UNCHANGED RAF!vars]_vars
SeekCorrect == [][\A offset \in Offset: Seek(offset) => RAF!Seek(offset)]_vars
SetLengthCorrect == [][\A offset \in Offset: SetLength(offset) => RAF!SetLength(offset)]_vars
SeekEstablishesInv2 == [][\A offset \in Offset: Seek(offset) => Inv2']_vars
Write1Correct == [][\A symbol \in SymbolOrArbitrary: Write1(symbol) => RAF!Write(SeqToArray(<<symbol>>))]_vars
Read1Correct == [][\A symbol \in SymbolOrArbitrary: Read1(symbol) => RAF!Read(SeqToArray(<<symbol>>))]_vars
WriteAtMostCorrect == [][\A len \in 1..MaxOffset: \A data \in Array(SymbolOrArbitrary, len): WriteAtMost(data) => \E written \in 1..len: RAF!Write(ArraySlice(data, 0, written))]_vars
ReadCorrect == [][\A len \in 1..MaxOffset: \A data \in Array(SymbolOrArbitrary, len): Read(data) => RAF!Read(data)]_vars
\* Inv2 is a precondition for many actions; it should always be possible to
\* restore Inv2 by execuing `restoreInvariantsAfterIncreasingCurr()`. That
\* method calls `seeek(curr)`, which is composed of a FlushBuffer followed by a
\* Seek, or just a Seek.
\*
\* To ensure that `restoreInvariantsAfterIncreasingCurr()` works as expected
\* (without using the \cdot action composition operator), we'll verify a few
\* things:
\* - dirty => ENABLED FlushBuffer
\* - FlushBuffer => ~dirty'
\* - ~dirty => ENABLED Seek(curr)
\* - Seek(curr) => Inv2'
\* Together, those properties ensure that it is always possible to restore Inv2
\* by taking a FlushBuffer action (if necessary) followed by a Seek(curr)
\* action.
FlushBufferPossibleWhenDirty == dirty => ENABLED FlushBuffer
FlushBufferMakesProgress == [][FlushBuffer => ~dirty']_vars
SeekCurrPossibleWhenNotDirty == ~dirty => ENABLED Seek(curr)
SeekCurrRestoresInv2 == [][Seek(curr) => Inv2']_vars
Inv2CanAlwaysBeRestored ==
/\ []FlushBufferPossibleWhenDirty
/\ FlushBufferMakesProgress
/\ []SeekCurrPossibleWhenNotDirty
/\ SeekCurrRestoresInv2
--------------------------------------------------------------------------------
\* Model checking helper definitions
Symmetry == Permutations(Symbols)
Alias == [
\* constants
BuffSz |-> BuffSz,
MaxOffset |-> MaxOffset,
\* regular vars
dirty |-> dirty,
length |-> length,
curr |-> curr,
lo |-> lo,
buff |-> buff,
diskPos |-> diskPos,
file_content |-> file_content,
file_pointer |-> file_pointer,
\* abstract vars
abstract_contents |-> LogicalFileContent]
================================================================================
--------------------------- MODULE RandomAccessFile ----------------------------
\* Specification of Java's RandomAccessFile class.
\*
\* A RandomAccessFile offers single-threaded access to some on-disk data
\* (`file_content`) and has an internal "pointer" or "cursor" (`file_pointer`).
\* Clients can move the pointer to an arbitrary position, or the client can
\* read or write data linearly from its current position, which simultaneously
\* advances the pointer.
\*
\* The core operations are:
\* - seek (to move the pointer)
\* - setLength (to resize the data)
\* - read (to copy bytes from disk to memory)
\* - write (to copy bytes from memory to disk)
\*
\* There are some cases where the general RandomAccessFile contract does not
\* define the data contents, for instance when extending the file using
\* setLength. In this spec, undefined bytes in the file are explicitly marked
\* with `ArbitrarySymbol`. While not entirely accurate, that choice simplifies
\* many definitions, since there is no need to nondeterministically choose
\* contents for the file. It also (incidentally) reduces state space explosion
\* during model checking.
EXTENDS Naturals, Sequences, Common
VARIABLES
file_content,
file_pointer
vars == << file_content, file_pointer >>
TypeOK ==
/\ file_content \in ArrayOfAnyLength(SymbolOrArbitrary)
/\ ArrayLen(file_content) <= MaxOffset
/\ file_pointer \in Offset
Init ==
/\ file_content = EmptyArray
/\ file_pointer = 0
Seek(new_offset) ==
/\ new_offset \in Offset
/\ file_pointer' = new_offset
/\ UNCHANGED << file_content >>
SetLength(new_length) ==
/\ file_content' = TruncateOrExtendFile(file_content, new_length)
\* The pointer's behavior is very strange. Per RandomAccessFile docs [1]:
\* > If the present length of the file as returned by the length method is
\* > greater than the newLength argument then the file will be truncated.
\* > In this case, if the file offset as returned by the getFilePointer
\* > method is greater than newLength then after this method returns the
\* > offset will be equal to newLength.
\*
\* The docs say NOTHING else about the file pointer. So, we can assume
\* that there are no other formal restrictions on its behavior.
\*
\* [1]: https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/io/RandomAccessFile.html#setLength(long)
/\ IF ArrayLen(file_content) > new_length /\ file_pointer > new_length
THEN file_pointer' = new_length
ELSE file_pointer' \in Offset
Read(output) ==
/\ output = ArraySlice(file_content, file_pointer, Min(file_pointer + ArrayLen(output), ArrayLen(file_content)))
/\ file_pointer' = file_pointer + ArrayLen(output)
/\ UNCHANGED << file_content >>
Write(data) ==
/\ file_pointer + ArrayLen(data) <= MaxOffset
/\ file_content' = WriteToFile(file_content, file_pointer, data)
/\ file_pointer' = file_pointer + ArrayLen(data)
Next ==
\/ \E offset \in Offset:
\/ Seek(offset)
\/ SetLength(offset)
\/ \E len \in 1..MaxOffset: \E data \in Array(SymbolOrArbitrary, len):
\/ Write(data)
\/ Read(data)
Spec == Init /\ [][Next]_vars
================================================================================
-------------------------------- MODULE Common ---------------------------------
\* This module contains constants and definitions common to both
\* RandomAccessFile and BufferedRandomAccessFile.
EXTENDS Naturals, Sequences
CONSTANTS
Symbols, \* data stored in the file (in reality there are 256 symbols: bytes 0x00 to 0xFF)
ArbitrarySymbol, \* special token for an arbitrary symbol (to reduce the need for nondeterministic choice)
MaxOffset \* the highest possible offset (in reality this is 2^63 - 1)
\* The set of legal offsets
Offset == 0..MaxOffset
\* The set of things that can appear at an offset in a file
SymbolOrArbitrary == Symbols \union {ArbitrarySymbol}
\* Minimum and maximum of two numbers
Min(a, b) == IF a <= b THEN a ELSE b
Max(a, b) == IF a <= b THEN b ELSE a
\* Definitions for 0-indexed arrays (as opposed to TLA+ 1-indexed sequences).
\* A major goal of the BufferedRandomAccessFile spec is to prevent off-by-one
\* errors in the implementation; therefore it should use 0-indexed arrays like
\* Java.
\*
\* The definitions are deliberately crafted so that the usual sequence
\* operators do NOT work on them; this is to help avoid accidental mixing of
\* sequences and arrays.
ArrayOfAnyLength(T) == [elems: Seq(T)]
Array(T, len) == [elems: [1..len -> T]]
ConstArray(len, x) == [elems |-> [i \in 1..len |-> x]]
MkArray(len, f) == [elems |-> [i \in 1..len |-> f[i - 1]]]
EmptyArray == [elems |-> <<>>]
ArrayLen(a) == Len(a.elems)
ArrayToSeq(a) == a.elems
SeqToArray(seq) == [elems |-> seq]
ArrayGet(a, i) == a.elems[i + 1]
ArraySet(a, i, x) == [a EXCEPT !.elems[i + 1] = x]
ArraySlice(a, startInclusive, endExclusive) == [elems |-> SubSeq(a.elems, startInclusive + 1, endExclusive)]
ArrayConcat(a1, a2) == [elems |-> a1.elems \o a2.elems]
\* General contract of the file `write()` call: extend the file with
\* ArbitrarySymbols if necessary, then overlay some `data_to_write` at the
\* given offset.
WriteToFile(file, offset, data_to_write) ==
LET
file_len == ArrayLen(file)
data_len == ArrayLen(data_to_write)
length == Max(file_len, offset + data_len)
IN
MkArray(
length,
[i \in 0..(length - 1) |->
CASE i < offset -> IF i < file_len THEN ArrayGet(file, i) ELSE ArbitrarySymbol
[] i >= offset /\ i < offset + data_len -> ArrayGet(data_to_write, i - offset)
[] i >= offset + data_len -> ArrayGet(file, i)])
\* General contract of the file `setLength()` call: truncate the file or fill
\* it with ArbitrarySymbol to reach the desired length.
TruncateOrExtendFile(file, new_length) ==
IF new_length > ArrayLen(file)
THEN ArrayConcat(file, ConstArray(new_length - ArrayLen(file), ArbitrarySymbol))
ELSE ArraySlice(file, 0, new_length)
================================================================================