Abstract
We explore in this paper the subtle correctness criterion of the absence of livelocks in parallel programs. The basic concepts underlying livelocks are formalized. A classification of livelocks into two types according to their causes of formation is introduced. Two techniques for proving the absence of livelocks are also presented. One is based on the notion of problem reduction; the other is an extension of the well-founded set method for proving termination in sequential programs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ashcroft, E. A.: Proving assertions about parallel programs. J. Comp. Sys. Sci., 10, 1 (Jan., 1975), 110–135.
Courtois, P. J., Heymans, F. and Parnas, D. L.: Concurrent control with "readers" and "writers." Comm. ACM, 14, 10 (Oct., 1971), 667–668.
Dijkstra, E. W.: Solution of a problem in concurrent programming control. Comm. ACM, 8, 9 (Sept., 1965), 569.
Dijkstra, E. W.: Hierarchical ordering of sequential processes. Acta Informatica, 1, 2(Oct., 1971), 115–138.
Floyd, R. W.: Assigning meanings to programs. Proc. Symp. in Applied Math., 19, American Math. Society (1967), 19–32.
Holt, R. C.: Comments on prevention of system deadlocks. Comm. ACM, 14, 1(Jan., 1971), 36–38.
Karp, R. M. and Miller R. E.: Parallel program schemata. J. Comp. Sys. Sci., 3(May, 1969), 147–195.
Keller, R. M.: Parallel program schemata and maximal parallelism. J. ACM, 20, 3(July, 1973), 514–537; and J. ACM, 20, 4(Oct., 1973), 696–710.
Keller, R. M.: A fundamental theorem of asynchronous parallel computation. Parallel Processing, T. Y. Feng (ed.), Springer-Verlag, Berlin (1975).
Keller, R. M.: Formal verification of parallel programs. Comm. ACM, 19, 7(July, 1976), 371–384.
Knuth, D. E.: Additional comments on a problem in concurrent programming control. Comm. ACM, 9, 5(May, 1966), 321–322.
Kwong, Y. S.: On reduction of asynchronous systems. Theoretical Computer Science, 5(1977), 25–50.
Kwong, Y. S.: On reductions and livelocks in asynchronous parallel computation. Ph.D. Dissertation, Dept. of Electrical Engineering and Computer Science, Princeton University, Princeton, N. J. 08540 (1978).
Kwong, Y. S.: Livelocks in parallel programs. Parts I and II. Technical reports 78-CS-15 & 16. Dept. of Applied Math., McMaster University (August, 1978).
Lamport, L.: Proving the correctness of multiprocess program. IEEE Trans. Software Engineering, SE-3, 2(March, 1977), 125–143.
van Lamsweerde, A. and Sintzoff, M.: Formal derivation of strongly correct parallel programs. Report R338, M.B.L.E. Research Laboratory, Brussel, Belgium (Oct., 1976).
Lipton, R. J.: Reduction: A method of proving properties of parallel programs. Comm. ACM, 18, 12(Dec., 1975), 717–721.
Rosen, B. K.: Correctness of parallel programs: The Church-Rosser approach. Theoretical Computer Science, 2(1976), 183–207.
Slutz, D.: The flow graph schemata model of parallel computation. Rep. MAC-TR-53 (Thesis), MIT project MAC (Sept., 1968).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kwong, Y.S. (1979). On the absence of livelocks in parallel programs. In: Kahn, G. (eds) Semantics of Concurrent Computation. Lecture Notes in Computer Science, vol 70. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022469
Download citation
DOI: https://doi.org/10.1007/BFb0022469
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09511-8
Online ISBN: 978-3-540-35163-4
eBook Packages: Springer Book Archive