Verification of Transactional Memory in POWER8
Allon Adir, Dave Goodman, Daniel Hershcovich, Oz Hershkovitz, Bryan Hickerson, Karen Holtz, Wisam Kadry, Anatoly Koyfman, John M. Ludden, Charles Meissner, Amir Nahir, Randall R. Pratt, Mike Schiffli, Brett St. Onge, Brian W. Thompto, Elena Tsanko, Avi Ziv · 2014
Transactional memory is a promising mechanism for synchronizing concurrent programs that eliminates locks at the expense of hardware complexity. Transactional memory is a hard feature to verify. First, transactions comprise several instructions that must be observed as a single global atomic operation. In addition, there are many reasons a transaction can fail. This results in a high level of non-determinism which must be tamed by the verification methodology. This paper describes the innovation that was applied to tools and methodology in pre-silicon simulation, acceleration and post-silicon in order to verify transactional memory in the IBM POWER8 processor core.