Summary
A method is described for deriving concurrent programs which are consistent with the problem specifications and free from deadlock and from starvation. The programs considered are expressed by nondeterministic repetitive selections of pairs of synchronizing conditions and subsequent actions. An iterative, convergent calculus is developed for synthesizing the invariant and synchronizing conditions which guarantee strong correctness. These conditions are constructed as limits of recurrences associated with the specifications and the actions. An alternative method for deriving starvationfree programs by use of auxiliary variables is also given. The applicability of the techniques presented is discussed through various examples; their use for verification purposes is illustrated as well.
Similar content being viewed by others
References
Burstall, R.: Program proving as hand simulation with a little induction. Proc. IFIP Congress 1974, Stockholm, pp. 308–312. Amsterdam: North Holland 1974
de Bakker, J.W., de Roever, W.P.: A calculus for recursive program schemes. In: Automata, Languages and Programming 1 (M. Nivat, ed.), pp. 167–196. Amsterdam: North Holland 1973
Devillers, R.E., Lauer, P.E.: A general mechanism for avoiding starvation with distributed control. Information Processing Lett. 7, 156–158 (1978)
Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informat. 1, 115–138 (1971)
Dijkstra, E.W.: A class of allocation strategies inducing bounded delays only. Proc. SJCC 1972, pp. 933–936. Montvale, N.J.: AFIPS Press 1972
Dijkstra, E.W.: A Discipline of Programming. Englewood Cliffs, N.J.: Prentice Hall, 1976
Dijkstra, E.W.: Two starvation-free solutions of a general exclusion problem. Report EWD 625, Burroughs-Nuenen, The Netherlands 1977
Flon, L., Suzuki, N.: Nondeterminism and the correctness of parallel programs. In: Formal Description of Programming Concepts (E.J. Neuhold, ed.), pp. 589–605. Amsterdam: North Holland 1978
Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. Applied Maths., Vol. 19, Aspects of Computer Science, pp. 19–32. New York: American Mathematical Society 1967
Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informat. 9, 133–157 (1978)
Holt, R.C.: Comment on prevention of system deadlocks. Comm. ACM 14, 36–38 (1971)
Keller, R.M.: Formal verification of parallel programs. Comm. ACM 19, 371–384 (1976)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Soft. Eng. SE-3, 125–143 (1977)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informat. 6, 319–340 (1976)
Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence (B. Meltzer and D. Michie, eds.), Vol. 5, pp. 59–78. Edinburgh: University Press 1969
Sintzoff, M.: Eliminating blind alleys from backtrack programs. In: Automata, Languages and Programming 3 (S. Michaelson and R. Milner, eds.), pp. 531–557. Edinburgh: University Press 1976
Sintzoff, M.: Inventing program construction rules. In: Constructing Quality Software (P.G. Hibbard and S.A. Schuman, eds.), pp. 471–501. Amsterdam: North Holland 1978
Sintzoff, M.: Ensuring correctness by arbitrary postfixed-points. In: 7th Symposium on Mathematical Foundations of Computer Science (J. Winkowski, ed.), Lecture Notes in Computer Science, Vol. 64, pp. 484–492. Berlin-Heidelberg-New York: Springer 1978
Sintzoff, M., van Lamsweerde, A.: Constructing correct and efficient concurrent programs. Proceedings ACM-IEEE International Conference on Reliable Software 1975, Los Angeles. Sigplan Notices 10, 319–326 (1975)
van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct parallel programs. MBLE Res. Lab., Brussels, Report R 338, October 1976
van Lamsweerde, A.: From verifying termination to guaranteeing it: a case study. In: Formal Description of Programming Concepts (E.J. Neuhold, ed.), pp. 609–620. Amsterdam: North Holland 1978
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
van Lamsweerde, A., Sintzoff, M. Formal derivation of strongly correct concurrent programs. Acta Informatica 12, 1–31 (1979). https://doi.org/10.1007/BF00264015
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF00264015