Hi Chris,
I had forgotten that I had written a spec of serializability in that
paper. The other one I mentioned is better because (a) it uses a
separate queue for each process, which seems to correspond more
closely to an implementation, and (b) it's in TLA+. But it's the same
idea. I don't know what transactions over multi-version objects are,
so I don't know if the same approach will work.
Using an auxiliary variable when showing that one spec refines another
need not be a cheat. It is sometimes necessary. (See the paper "The
Existence of Refinement Mappings" by Martin Abadi and me.
Abstraction always requires creativity. In general, it's best to
write the simplest, clearest spec you can. It's certainly better to
add history variables to the implementation rather than modifying the
spec to avoid them. Prophecy variable are mindboggling enough that
I'd recommend trying to modify the spec to avoid them if you can.
Leslie