Synchronization of communicating processes

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.

REFERENCES

• 1: Dijkstra, E.W. Cooperating sequential processes. In Programming Languages, F. Genuys, Ed., Academic Press, New York, 1968, pp. 43-112.
• 2: Edsger W. Dijkstra, The structure of the “THE”-multiprogramming system, Communications of the ACM, v.11 n.5, p.341-346, May 1968 [doi>10.1145/363095.363143]
• 3: Parnas, D.L Information distribution aspects of design methodology. Report, Dep. Computer Sci., Carnegie-Mellon U., Pittsburgh, Pa., Feb. 1971.
• 4: J. H. Saltzer, TRAFFIC CONTROL IN A MULTIPLEXED COMPUTER, Massachusetts Institute of Technology, Cambridge, MA, 1966
• 5: C. Bétourné , J. Boulenger , J. Ferrié , C. Kaiser , S. Krakowiak , J. Mossière, Process management and resource sharing in the multiaccess system in ESOPE, Communications of the ACM, v.13 n.12, p.727-733, Dec. 1970 [doi>10.1145/362814.362821]
• 6: Michael J. Spier , Elliott I. Organick, The multics interprocess communication facility, Proceedings of the second symposium on Operating systems principles, October 20-22, 1969, Princeton, New Jersey [doi>10.1145/961053.961086]
• 7: E. W. Dijkstra, Solution of a problem in concurrent programming control, Communications of the ACM, v.8 n.9, p.569, Sept. 1965 [doi>10.1145/365559.365617]
• 8: Habermann, A.N. An operating system modeled as a set of interacting processes. Ann. Princeton Conf. on Computer Sci. and Syst., March 1971.

INDEX TERMS

Keywords:
multiprogramming, parallel programming, process communication, process scheduling, program correctness