An Operational Semantics for LogTM

File(s)
Date
2006Author
Liblit, Ben
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
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.
Permanent Link
http://digital.library.wisc.edu/1793/60516Type
Technical Report
Citation
TR1571