2006 International Conference on Parallel Architectures and Compilation Techniques (PACT) (2006)
Seattle, WA, USA
Sept. 16, 2006 to Sept. 20, 2006
DOI Bookmark: http://doi.ieeecomputersociety.org/
Chaiyasit Manovit , Sun Microsystems, Sunnyvale, CA, USA
Sudheendra Hangal , Magic Lamp Software, Bangalore, India
Hassan Chafi , Stanford University, Stanford, CA, USA
Austen McDonald , Stanford University, Stanford, CA, USA
Christos Kozyrakis , Stanford University, Stanford, CA, USA
Kunle Olukotun , Stanford University, Stanford, CA, USA
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.
Specification, Transactional memory, Testing, Verification
C. Manovit, S. Hangal, H. Chafi, A. McDonald, C. Kozyrakis and K. Olukotun, "Testing implementations of transactional memory," 2006 International Conference on Parallel Architectures and Compilation Techniques (PACT), Seattle, WA, USA, 2006, pp. 134-143.