Proving monitors

ABSTRACT

Interesting scheduling and sequential properties of monitors can be proved by using state variables which record the monitors' history and by defining extended proof rules for their wait and signal operations. These two techniques are defined, discussed, and applied to examples to prove properties such as freedom from indefinitely repeated overtaking or unnecessary waiting, upper bounds on queue lengths, and historical behavior.

REFERENCES

• 1: Dijkstra, E.W. Hierarchical ordering of sequential processes. In Operating Systems Techniques, C.A.R. Hoare and R.H. Perrott (Eds.), Academic Press, 1972, pp. 72-93.
• 2: Per Brinch Hansen, Operating System Principles, Prentice Hall PTR, Upper Saddle River, NJ, 1973
• 3: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 4: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 5: Hoare, C.A.R. Proof of correctness of data representations. Acta Informatica I (1972), 271-281.
• 6: Lawrence Robinson , Karl N. Levitt , Peter G. Neumann , Ashok R. Saxena, On attaining reliable software for a secure operating system, Proceedings of the international conference on Reliable software, p.267-284, April 21-23, 1975, Los Angeles, California
• 7: Clint, M. Program proving: coroutines. Acta Informatica 2 (1973), 50-63.
• 8: John E. Hopcroft , Jeffrey D. Ullman, Formal languages and their relation to automata, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1969
• 9: Howard, J.H., and Alexander, W.P. Analyzing sequences of operations performed by programs. Program Test Methods, W.C. Hetzel (Ed.), Prentice-Hall, 1973, pp. 239-254.
• 10: William Preston Alexander, III, Analysis of sequencing in computer programs and systems., 1974
• 11: Zilles, S.N. Abstract specification for data types. Working paper, IBM Research, San Jose, Calif., 1975. Extracted from 1974 Project Mac Progress Report, MIT, Cambridge, Mass., 1975.
• 12: Barbara Liskov , Stephen Zilles, Specification techniques for data abstractions, Proceedings of the international conference on Reliable software, p.72-87, April 21-23, 1975, Los Angeles, California
• 13: D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
• 14: A. Nico Habermann, Synchronization of communicating processes, Proceedings of the third ACM symposium on Operating systems principles, p.80, October 18-20, 1971, Palo Alto, California, United States [doi>10.1145/800212.806503]
• 15: Michel Sintzoff , Axel Van Lamsweerde, Constructing correct and efficient concurrent programs, Proceedings of the international conference on Reliable software, p.319-326, April 21-23, 1975, Los Angeles, California
• 16: Toby J. Teorey , Tad B. Pinkerton, A comparative analysis of disk scheduling policies, Proceedings of the third ACM symposium on Operating systems principles, p.114, October 18-20, 1971, Palo Alto, California, United States [doi>10.1145/800212.806509]

INDEX TERMS

Keywords:
alarm clock, bounded buffer, concurrency, correctness, disk head, historical variables, monitors, proof rules, scheduling, semaphores