Sciweavers

Share
ICECCS
2010
IEEE

Implementing and Evaluating a Model Checker for Transactional Memory Systems

10 years 4 months ago
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 ...
Woongki Baek, Nathan Grasso Bronson, Christos Kozy
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where ICECCS
Authors Woongki Baek, Nathan Grasso Bronson, Christos Kozyrakis, Kunle Olukotun
Comments (0)
books