Sequential to parallel buffer refinement
Andrew Kay, Peter Lupton · Formal Aspects of Computing · 1992
Abstract This paper is intended to solve a particular problem related to the refinement of a shared sequential buffer into a parallel collection of buffers arising from a study on the IBM CICS project. Using the notion of cooperating refinement we show that the two systems are equivalent from the users' points of view (except with respect to efficiency). This is achieved by constructing an interleaving for each possible sequence of commands which access the buffer. The induction used in the proof is non-standard, and makes the problem harder than it would at first seem. Further we show that the interleaving cannot be done ‘on the fly’, showing that in some other sense, the parallel collection is indeed superior, as intuition suggests.