An Operational Semantics for LogTMAn Operational Semantics for LogTMThis research was conducted by Ben Liblit.
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.
The full paper is available as a single PDF document. A suggested BibTeX citation record is also available.