A serialization graph construction for nested transactions

ABSTRACT

This paper makes three contributions. First, we present a proof technique that offers system designers the same ease of reasoning about nested transaction systems as is given by the classical theory for systems without nesting, and yet can be used to verify that a system satisfies the robust “user view” definition of correctness of [10]. Second, as applications of the technique, we verify the correctness of Moss' read/write locking algorithm for nested transactions, and of an undo logging algorithm that has not previously been presented or proved for nested transaction systems. Third, we make explicit the assumptions used for this proof technique, assumptions that are usually made implicitly in the classical theory, and therefore we clarify the type of system for which the classical theory itself can reliably be used.

REFERENCES

• 1: James Aspnes , Alan Fekete , Nancy A. Lynch , Michael Merritt , William E. Weihl, A Theory of Timestamp-Based Concurrency Control for Nested Transactions, Proceedings of the 14th International Conference on Very Large Data Bases, p.431-444, August 29-September 01, 1988
• 2: Catriel Beeri , Philip A. Bernstein , Nathan Goodman, A model for concurrency in nested transactions systems, Journal of the ACM (JACM), v.36 n.2, p.230-269, April 1989 [doi>10.1145/62044.62046]
• 3: Philip A. Bernstein , Vassco Hadzilacos , Nathan Goodman, Concurrency control and recovery in database systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
• 4: A. Fekete , N. Lynch , M. Merrit , W. Weihl, Nested transactions and read-write locking, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.97-111, March 23-25, 1987, San Diego, California, United States [doi>10.1145/28659.28669]
• 5: A. Fekete, N. Lynch, M. Merritt, and W. Weihl. Commutativity-based locking for nested transactions. Technical Memo MIT/LCS/TM-370.b, Massachusetts Institute Technology, Laboratory for Computer Science, August 1989. To appear in JCSS.
• 6: Kenneth J. Goldman , Nancy A. Lynch, Quorum consensus in nested transaction systems, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.27-41, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41843]
• 7: Thanasis Hadzilacos , Vassos Hadzilacos, Transaction synchronisation in object bases, Proceedings of the seventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.193-200, March 1988, Austin, Texas, United States [doi>10.1145/308386.308438]
• 8: Maurice Herlihy , Nancy Lynch , Michael Merritt , William Weihl, On the correctness of orphan management algorithms, Journal of the ACM (JACM), v.39 n.4, p.881-930, Oct. 1992 [doi>10.1145/146585.146616]
• 9: Barbara Liskov, Distributed programming in Argus, Communications of the ACM, v.31 n.3, p.300-312, March 1988 [doi>10.1145/42392.42399]
• 10: Nancy Lynch , Michael Merritt, Introduction to the theory of nested transactions, Proceedings on International conference on database theory, p.278-305, December 1986, Rome, Italy
• 11: N. Lynch , M. Merritt , W. Weihl , A. Fekete, A theory of atomic transactions, Lecture notes in computer science on ICDT '88, p.41-71, October 1988, Bruges, Belgium
• 12: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 13: E. B. Moss, NESTED TRANSACTIONS: AN APPROACH TO RELIABLE DISTRIBUTED COMPUTING, Massachusetts Institute of Technology, Cambridge, MA, 1981
• 14: Christos Papadimitriou, The theory of database concurrency control, Computer Science Press, Inc., New York, NY, 1986
• 15: A. Spector and K. Swedlow. Guide to the Camelot distributed transaction facility: Release 1, October 1987. Available from Carnegie Mellon University, Pittsburgh, PA.
• 16: W. E. Weihl, The impact of recovery on concurrency control, Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.259-269, March 1989, Philadelphia, Pennsylvania, United States [doi>10.1145/73721.73748]
• 17: W. E. Weihl, Local atomicity properties: modular concurrency control for abstract data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.2, p.249-282, April 1989 [doi>10.1145/63264.63518]
• 18: W. E. Weihl, SPECIFICATION AND IMPLEMENTATION OF ATOMIC DATA TYPES, Massachusetts Institute of Technology, Cambridge, MA, 1984

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.4 Systems
          Subjects: Transaction processing

General Terms:
Algorithms, Design, Management, Performance, Reliability, Theory, Verification