Implementing and Evaluating a Model Checker for Transactional Memory Systems

Abstract—Transactional Memory (TM) is a promising technique that addresses the difficulty of parallel programming. Since TM takes responsibility for all concurrency control, TM systems are highly vulnerable to subtle correctness errors. Due to the difficulty of fully proving the correctness of TM systems, many of them are used without any formal correctness guarantees. This paper presents ChkTM, a flexible model checking environment to verify the correctness of various TM systems. ChkTM aims to model TM systems close to the implementation level to reveal as many potential bugs as possible. For example, ChkTM accurately models the version control mechanism in timestampbased software TMs (STMs). In addition, ChkTM can flexibly model TM systems that use additional hardware components or support nested parallelism. Using ChkTM, we model several TM systems including a widely-used industrial STM (TL2), a hybrid TM (SigTM) that uses hardware signatures, and an STM (NesTM) that supports ...

• Type: Conference
• Year: 2010
• Where: ICECCS
• Authors: Woongki Baek, Nathan Grasso Bronson, Christos Kozyrakis, Kunle Olukotun
• Keywords: Correctness, Hardware, ICECCS 2010, TM Systems, Various Tm Systems