An Operational Semantics for LogTM

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.

Download this report (PDF)

Return to tech report index