Ernie writes,
Note that while you can specify strict serializability in TLA, it
requires use of temporal existential quantification, which you won't
be able to check with TLC unless you can provide a suitable witness.
I'm puzzled by this. If you don't want to limit what you can express
to simple properties, you have to be able to specify one system by a
more abstract system. And writing a philosophically correct spec of
that form requires variable hiding, which is represented in TLA by
temporal existential quantification. So it's not just
serializability; you can't even specify a FIFO queue in TLA without
temporal quantification. Clearly this isn't a practical issue, and
surely Ernie realizes this.
My guess is that Ernie thinks serializability is a special case, and
it requires a spec that's quite unlike a FIFO queue spec. He is both
wrong and right about this. There is a simple way to specify
serializability in TLA+ whose state involves only a collection of FIFO
queues (one for each process) and a central memory. And it has simple
fairness conditions on its action. But he's right that although in
practice it's not fundamentally different from a FIFO queue spec, it's
fundamentally different from the FIFO queue spec because it's not
machine closed. That difference arises because serializability is an
inherently weird spec--as evidenced by the fact that an implementation
that can predict the future can return a value for a read that hasn't
yet been written. It could allow weird behaviors in circumstances in
which it would be possible to infer some future behavior by a process.
Anyway, the spec is in the Lazy Caching paper:
Leslie