Testing implementations of transactional memory

ABSTRACT

Transactional memory is an attractive design concept for scalable multiprocessors because it offers efficient lock-free synchronization and greatly simplifies parallel software. Given the subtle issues involved with concurrency and atomicity, however, it is important that transactional memory systems be carefully designed and aggressively tested to ensure their correctness. In this paper, we propose an axiomatic framework to model the formal specification of a realistic transactional memory system which may contain a mix of transactional and non-transactional operations. Using this framework and extensions to analysis algorithms originally developed for checking traditional memory consistency, we show that the widely practiced pseudo-random testing methodology can be effectively applied to transactional memory systems. Our testing methodology was successful in finding previously unknown bugs in the implementation of TCC, a transactional memory system. We study two flavors of the underlying analysis algorithm, one incomplete and the other complete, and show that the complete algorithm while being theoretically intractable is very efficient in practice.

REFERENCES

• 1: Sarita V. Adve , Mark D. Hill , Barton P. Miller , Robert H. B. Netzer, Detecting data races on weak memory systems, Proceedings of the 18th annual international symposium on Computer architecture, p.234-243, May 27-30, 1991, Toronto, Ontario, Canada
• 2: C. Scott Ananian , Krste Asanovic , Bradley C. Kuszmaul , Charles E. Leiserson , Sean Lie, Unbounded Transactional Memory, Proceedings of the 11th International Symposium on High-Performance Computer Architecture, p.316-327, February 12-16, 2005 [doi>10.1109/HPCA.2005.41]
• 3: B. Bentley and R. Gray. Validating the Intel Pentium 4 processor. Intel Technology Journal, (Q1):8, Feb. 2001.
• 4: Phillip B. Gibbons , Ephraim Korach, Testing Shared Memories, SIAM Journal on Computing, v.26 n.4, p.1208-1244, Aug. 1997 [doi>10.1137/S0097539794279614]
• 5: Lance Hammond , Brian D. Carlstrom , Vicky Wong , Ben Hertzberg , Mike Chen , Christos Kozyrakis , Kunle Olukotun, Programming with transactional coherence and consistency (TCC), Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 6: Lance Hammond , Vicky Wong , Mike Chen , Brian D. Carlstrom , John D. Davis , Ben Hertzberg , Manohar K. Prabhu , Honggo Wijaya , Christos Kozyrakis , Kunle Olukotun, Transactional Memory Coherence and Consistency, Proceedings of the 31st annual international symposium on Computer architecture, p.102, June 19-23, 2004, München, Germany
• 7: Sudheendra Hangal , Durgam Vahia , Chaiyasit Manovit , Juin-Yeu Joseph Lu, TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model, Proceedings of the 31st annual international symposium on Computer architecture, p.114, June 19-23, 2004, München, Germany
• 8: Maurice Herlihy , J. Eliot B. Moss, Transactional memory: architectural support for lock-free data structures, Proceedings of the 20th annual international symposium on Computer architecture, p.289-300, May 16-19, 1993, San Diego, California, United States
• 9: R. Hosabettu. SPARC V9 atomic transaction. Sun Microsystems internal document, Feb. 2003.
• 10: J. M. Ludden, W. Roesner, G. M. Heiling, J. R. Reysa, J. R. Jackson, et al. Functional verification of the POWER4 microprocessor and POWER4 multiprocessor system. IBM Journal of Research and Development, 46(1):53--76, 2002.
• 11: S. T. Mangelsdorf, R. P. Gratias, R. M. Blumberg, and R. Bhatia. Functional verification of the HP PA 8000 processor. Hewlett-Packard Journal, Aug. 1997.
• 12: Chaiyasit Manovit , Sudheendra Hangal, Efficient algorithms for verifying memory consistency, Proceedings of the seventeenth annual ACM symposium on Parallelism in algorithms and architectures, July 18-20, 2005, Las Vegas, Nevada, USA [doi>10.1145/1073970.1074011]
• 13: C. Manovit and S. Hangal. Completely verifying memory consistency of test program executions. In HPCA'06: Proceedings of the 12th International Symposium on High-Performance Computer Architecture, 2006.
• 14: S. Mehta , S. Ahmed , S. Al-Ashari , D. Chen , C. Dev , S. Cokmez , P. Desai , R. Eltejaein , P. Fu , J. Gee , T. Granvold , A. Iyer , K. Lin , G. Maturana , D. McConn , H. Mohammed , J. Mostoufi , A. Moudgal , S. Nori , N. Parveen , G. Peterson , M. Splain , T. Yu, Verification of the UltraSPARC microprocessor, Proceedings of the 40th IEEE Computer Society International Conference, p.452, March 05-09, 1995
• 15: M. Moir. Hybrid transactional memory, Jul 2005. Unpublished manuscript.
• 16: K. E. Moore, J. Bobba, M. J. Moravan, et al. LogTM: Log-based transactional memory. In HPCA'06: Proceedings of the 12th International Symposium on High-Performance Computer Architecture, 2006.
• 17: Christos H. Papadimitriou, The serializability of concurrent database updates, Journal of the ACM (JACM), v.26 n.4, p.631-653, Oct. 1979 [doi>10.1145/322154.322158]
• 18: Ravi Rajwar , Maurice Herlihy , Konrad Lai, Virtualizing Transactional Memory, Proceedings of the 32nd annual international symposium on Computer Architecture, p.494-505, June 04-08, 2005
• 19: Nir Shavit , Dan Touitou, Software transactional memory, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.204-213, August 20-23, 1995, Ottowa, Ontario, Canada [doi>10.1145/224964.224987]
• 20: A. Shriraman, V. Marathe, S. Dwarkadas, et al. Hardware acceleration of software transactional memory. Technical Report UR CSD;TR 887, Dept. of Computer Science, University of Rochester, Dec. 2005.
• 21: P. S. Sindhu, J.-M. Frailong, and M. Cekleov. Formal specification of memory models. Technical Report CSL-91-11, Xerox Palo Alto Research Center, Dec. 1991.
• 22: Scott Taylor , Michael Quinn , Darren Brown , Nathan Dohm , Scot Hildebrandt , James Huggins , Carl Ramey, Functional verification of a multiple-issue, out-of-order, superscalar Alpha processor—the DEC Alpha 21264 microprocessor, Proceedings of the 35th annual conference on Design automation, p.638-643, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277208]
• 23: Min Xu , Rastislav Bodík , Mark D. Hill, A serializability violation detector for shared-memory server programs, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA

INDEX TERMS

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

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Systems specification methodology

General Terms:
Algorithms, Verification

Keywords:
specification, testing, transactional memory, verification