Peterson’s algorithm Total correctness proof in IPCL

A.A. Zhygallo

Abstract


The total correctness of the Peterson’s Algorithm has been proved. States and transitions were fixed by the program. Runtime environment considered is interleaving concurrency with shared memory. Invariant of the program was constructed. All reasoning provided in terms of Method for software properties proof in Interleaving Parallel Compositional Languages (IPCL). Conclusions about adequacy of the Method usage for such a kind of tasks (thanks to flexibility of composition-nominative platform) and its practicality as well as ease of use for real-world systems have been made based on this and other author’s works.

Problems in programming 2016; 2-3: 113-118


Keywords


Peterson’s algorithm; mutual exclusion; software total correctness; formal verification; liveness property; concurrent program; interleaving; IPCL; composition-nominative languages

Full Text:

PDF

References


PANCHENKO, T. (2006) Compositional Methods for Software Systems Specification and Verification (PhD Thesis), Kyiv, 177 p.

OWICKI S., GRIES D. (1976) An Axiomatic Proof Technique for Parallel Programs. Acta Informatica, Vol. 6, № 4, pp. 319-340.

https://doi.org/10.1007/BF00268134

XU Q., de ROEVER W.-P., HE J. (1997) The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs. Formal Aspects of Computing, Vol. 9, № 2, pp. 149-174.

https://doi.org/10.1007/BF01211617

LAMPORT L. (1993) Verification and Specification of Concurrent Programs. A Decade of Concurrency, deBakker J., deRoever W., Rozenberg G. (eds.), Berlin: Springer-Verlag, Vol. 803, pp. 347-374.

https://doi.org/10.1007/3-540-58043-3_23

PANCHENKO, T. (2004) The Methodology for Program Properties Proof in Compositional Languages IPCL. In Proceedings of the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2004), Kyiv, pp. 62-67.

TANENBAUM, A.S. (2008) Modern operating systems, 3Ed. Upper Saddle River, NJ: Pearson Prentice Hall, 1104 p.

PETERSON, G.L. (1981) Myths About the Mutual Exclusion Problem. Information Processing Letters, 12(3), pp. 115-116.

https://doi.org/10.1016/0020-0190(81)90106-X

ZHYGALLO A., OSTAPOVSKA Yu., PANCHENKO T. (2015) Peterson's Algorithm for Mutual Exclusion Correctness Proof in IPCL. Bulletin of Taras Shevchenko National University of Kyiv. Series: Physical & Mathematical Sciences, N 4.

REDKO, V. (1978) Compositions of Programs and Composition Programming. Programming, 5, pp. 3-24.

REDKO, V. (1979) Foundation of Composition Programming. Programming, 3, pp. 3-13.

NIKITCHENKO, N. (1998) A Composition Nominative Approach to Program Semantics. Technical Report IT-TR: 1998-020. Technical Univer-sity of Denmark. 103 p.

PANCHENKO, T. (2008) The Method for Program Properties Proof in Compositional Nominative Languages IPCL. Problems of Programming. 1. pp. 3-16.




DOI: https://doi.org/10.15407/pp2016.02-03.113

Refbacks

  • There are currently no refbacks.