Using transformations to verify parallel programs
- 113 Downloads
We argue that the verification of parallel programs can be considerably simplified by using program transformations. We illustrate this approach by proving correctness of two parallel programs under the assumption of fairness: asynchronous fixed point computation and parallel zero search.
KeywordsParallel Program Parallel Composition Proper State Fair Termination Program Transformation
Unable to display preview. Download preview PDF.
- E. Ashcroft and Z. Manna, Formalization of properties of parallel programs, Machine Intelligence 6, pp. 17–41, 1971.Google Scholar
- K.R. Apt and E.-R. Olderog, Proof rules and transformations dealing with fairness, Science of Computer Programming 3, pp. 65–100, 1983.Google Scholar
- R.J.R. Back, A method for refining atomicity in parallel algorithms, Lecture Notes in Computer Science 366, Springer-Verlag, 1989.Google Scholar
- M. Chandy and J. Misra, A Foundation of Parallel Program Design, Addison-Wesley, 1988.Google Scholar
- E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM 18, pp. 453–457, 1975.Google Scholar
- L. Flon and N. Suzuki, The total correctness of parallel programs, SIAM Journal of Computing, pp. 227–246, 1978.Google Scholar
- N. Francez, Fairness, Springer-Verlag, 1986.Google Scholar
- M.C.B.Hennessy and G.D. Plotkin, Full abstraction for a simple programming language, Lecture Notes in Computer Science 74, Springer-Verlag, 1979.Google Scholar
- L. Lamport, Proving the correctness of multiprocess programs, IEEE Transactions on Software Engineering SE-3:2, pp.125–143, 1977.Google Scholar
- R. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM 18, pp. 717–721, 1975.Google Scholar
- E. R. Olderog and K. R. Apt, Fairness in parallel programs, the transformational approach, ACM TOPLAS 10, pp. 420–455, 1988.Google Scholar