A. Nico Habermann
Abstract
Formalization of a well-defined synchronization mechanism can be used to prove that concurrently running processes of a system communicate correctly. This is demonstrated for a system consisting of many sending processes which deposit messages in a buffer and many receiving processes which remove messages from that buffer. The formal description of the synchronization mechanism makes it very easy to prove that the buffer will neither overflow nor underflow, that senders and receivers will never operate on the same message frame in the buffer nor will they run into a deadlock.
- 1 Dijkstra, E.W. Cooperating sequential processes. In Programming Languages, F. Genuys, Ed., Academic Press, New York, 1968, pp. 43-112.Google Scholar
- 2 Dijkstra, E.W. The structure of the "THE"-- multiprogramming system. Comm. ACM 11, 5 (May 1968), 341-346. Google ScholarDigital Library
- 3 Parnas, D.L Information distribution aspects of design methodology. Report, Dep. Computer Sci., Carnegie-Mellon U., Pittsburgh, Pa., Feb. 1971.Google Scholar
- 4 Saltzer, J.H. Traffic control in a multiplexed computer system (Th.). Rep. MAC-TR-30, Proj. MAC, MIT, Cambridge, Mass., 1966. Google ScholarDigital Library
- 5 Botourno, C., et al. Process management and resource sharing in the multiaccess system "ESOPE." Comm. ACM 13, 12 (Dec. 1970), 727-733. Google ScholarDigital Library
- 6 Spier, M.J., and Organick, E.I. The multics interprocess communication facility. Proc. Second Symp. on Oper. Syst. Princ., ACM, New York, 1971, pp. 83-91. Google ScholarDigital Library
- 7 Dijkstra, E.W. Solution of a problem in concurrent programming control. Comm. ACM 8, 9 (Sept. 1965), 569. Google ScholarDigital Library
- 8 Habermann, A.N. An operating system modeled as a set of interacting processes. Ann. Princeton Conf. on Computer Sci. and Syst., March 1971.Google Scholar
Recommendations
Synchronization of communicating processes
Formalization of a well-defined synchronization mechanism can be used to prove that concurrently running processes of a system communicate correctly. This is demonstrated for a system consisting of many sending processes which deposit messages in a ...
Synchronization of communicating processes
SOSP '71: Proceedings of the third ACM symposium on Operating systems principlesThis paper appears in the March, 1972, issue of the Communications of the ACM. Its abstract is reproduced below.
Formalization of a well-defined synchronization mechanism can be used to prove that concurrently running processes of a system communicate ...
The nucleus of a multiprogramming system
This paper describes the philosophy and structure of a multi-programming system that can be extended with a hierarchy of operating systems to suit diverse requirements of program scheduling and resource allocation. The system nucleus simulates an ...
Comments