The geometry of semaphore programs

ABSTRACT

Synchronization errors in concurrent programs are notoriously difficult to find and correct. Deadlock, partial deadlock, and unsafeness are conditions that constitute such errors. A model of concurrent semaphore programs based on multidimensional, solid geometry is presented. While previously reported geometric models are restricted to two-process mutual exclusion problems, the model described here applies to a broader class of synchronization problems. The model is shown to be exact for systems composed of an arbitrary, yet fixed number of concurrent processes, each consisting of a straight line sequence of arbitrarily ordered semaphore operations.

REFERENCES

• 1: Scott David Carson, Geometric models of concurrent programs, 1984
• 2: Edmund Clarke, Jr., Synthesis of Resource Invariants for Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.338-358, July 1980 [doi>10.1145/357103.357109]
• 3: E. G. Coffman , M. Elphick , A. Shoshani, System Deadlocks, ACM Computing Surveys (CSUR), v.3 n.2, p.67-78, June 1971 [doi>10.1145/356586.356588]
• 4: DIJRSTRA, E.W. Co-operating sequential processes. In Programming Languages, F. Genuys, Ed. Academic Press, New York, 1968, 43-110.
• 5: HASERMAr~N, A.N. Path expressions. Tech. Rep., Dept. of Computer Science, Carnegie-Mellon Univ., Pittsburgh, Pa., June 1975.
• 6: Richard C. Holt, Some Deadlock Properties of Computer Systems, ACM Computing Surveys (CSUR), v.4 n.3, p.179-196, Sept. 1972 [doi>10.1145/356603.356607]
• 7: KELLER, R.M. Generalized Petri nets as models for system verification. Tech. Rep., Computer Science Dept., Univ. of Utah, Salt Lake City, 1977.
• 8: LIPSKI, W., AND PAPADIMITRIOU, C.H. A fast algorithm for testing for safety and detecting deadlocks in locked transaction systems. J. A/g. 2, 3 (Sept. 1981), 211-226.
• 9: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 10: PAPAD1MITRIOU, C. H. Concurrency control by locking. SIAM J. Comput. 12, 2 (May 1983), 215-226.
• 11: YA~NAKAKIS, M., PAPADIMITRIOU, C. H., AND KUNG, H. T. Locking policies: Safety and freedom from deadlock. In Proceedings of the 20th FOCS (San Juan, P.R., Oct. 29-31, 1979). IEEE, New York, 1979, 286-297.

INDEX TERMS

Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Synchronization; Concurrency; Mutual exclusion; Deadlocks

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Graph algorithms

General Terms:
Algorithms, Theory