A class of synchronization systems that permit the use of large atomic blocks

ABSTRACT

This paper revisits the formal justification of a common practice used in formal and informal reasoning about distributed systems: considering certain sections of code to be implicitly atomic. This practice is extremely useful as it allows distributed and concurrent programs to be developed, tested, and verified with large atomic blocks, yet executed with a much finer granularity of parallelism for efficiency. We expose the elements on which this practice is based and characterize the synchronization systems for which this practice is valid. Unlike previous justifications for this practice, our approach is based on a weakest precondition semantics. Owing to the generality of our model of computation, the result is applicable to both distributed-memory and shared-memory systems.

REFERENCES

• 1: {1} R. J. R. Back. On correct refinements of programs. Journal of Computer and System Sciences, 23:49-68, 1981.
• 2: Ralph-Johan Back, A Method for Refining Atomicity in Parallel Algorithms, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.199-216, June 12-16, 1989
• 3: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 4: {4} Edsger W. Dijkstra and C. S. Scholten. Termination detection for diffusing computations. Information Processing Letters, 11(1):1-4, August 1980.
• 5: Edsger W. Dijkstra , Carel S. Scholten, Predicate calculus and program semantics, Springer-Verlag New York, Inc., New York, NY, 1990
• 6: Thomas W. Doeppner, Jr., Parallel program correctness through refinement, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.155-169, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512965]
• 7: {7} Leslie Lamport. A theorem on atomicity in distributed algorithms. Distributed Computing , 4(2):59-68, 1990.
• 8: Leslie Lamport , Fred B. Schneider, Pretending Atomicity, Cornell University, Ithaca, NY, 1989
• 9: Harry R. Lewis , Christos H. Papadimitriou , Christos Papadimitriou, Elements of the Theory of Computation, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 10: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 11: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 12: Jayadev Misra , K. M. Chandy, Termination Detection of Diffusing Computations in Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.1, p.37-43, Jan. 1982 [doi>10.1145/357153.357156]
• 13: Carroll Morgan, The specification statement, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.403-419, July 1988 [doi>10.1145/44501.44503]
• 14: Joseph M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, v.9 n.3, p.287-306, December 1, 1987 [doi>10.1016/0167-6423(87)90011-6]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency

Additional Classification:
  B. Hardware
  B.3 MEMORY STRUCTURES
      B.3.2 Design Styles
          Subjects: Shared memory

  D. Software
  D.4 OPERATING SYSTEMS
      D.4.2 Storage Management
          Subjects: Distributed memories

General Terms:
Design, Measurement, Theory