Transactional Semantics with Zombies
Michael Lee Scott · 2014
Different formal models of transactional memory are re-quired at different levels of the system stack. This paper focuses on the run-time level, where the semantics of in-dividual operations (start, read, write, try-commit) govern the interactions between the compiler and the TM sys-tem. For sandboxing TM systems, which allow a doomed transaction (a “zombie”) to continue for some time be-yond an inconsistent read, run-time–level semantics can-not be captured by opacity as currently defined: we need a formal model of zombie execution. 1