An Operational Semantics for LogTM

Abstract

We present a formal operational semantics for LogTM, a hardware-based nested transactional memory system. We define the proper execution of programs written in a small assembly language that includes memory accesses, nested closed and open transactions, partial rollback, commit and abort handlers, thread spawning, and escape actions. This is a working document, intended to reflect and codify the current best understanding of LogTM's operation in both common and corner cases. This formal semantics serves as a reference companion to other published discussions of LogTM, and specifically corresponds to the system described in "Supporting Nested Transactional Memory in LogTM" by Moravan et al.