|Title:||A Programming Language Approach to Transactional Memory Consistency
|PDF - Revised||PHD-2015-13.revised.pdf|
|Abstract:||Transactional memory (TM) has been hailed as a paradigm for simplifying concurrent programming. It eases the task of writing concurrent applications by letting the programmer designate certain code blocks as atomic.
One of the main challenges in stating the correctness of TM systems is the need to provide guarantees on the system state observed by live transactions, i.e., those that have not yet committed or aborted. While several consistency conditions have been suggested for TM, they fall short of formalizing the intuitive semantics of atomic blocks, the interface through which a TM is used in a programming language. A TM consistency condition should be weak enough to allow flexibility in implementation, yet strong enough to disallow undesirable TM behavior, which can lead to run-time errors in live transactions. The latter feature is formalized by observational refinement between TM implementations, stating that properties of a program using a concrete TM implementation can be established by analyzing its behavior with an abstract TM, serving as a specification of the concrete one.
We show that Strong Transactional Memory Specification (STMS), a variant of Transactional Memory Specification 1 (TMS1), is necessary and sufficient for observational refinement for a programming language in which local variables are not rolled back upon an abort. We also show that TMS1 is necessary and sufficient for observational refinement for the common programming model in which local variables are rolled back upon a transaction abort. This makes STMS and TMS1 the weakest acceptable conditions for these programming models.
We show that STMS is prefix-closed, that is, every prefix of a STMS history is also STMS. We then show that under certain restrictions, STMS is limit-closed, i.e., the limit of any sequence of ever extending STMS histories is also STMS. Therefore, STMS is a safety property, and to prove that a TM implementation is STMS, it suffices to prove that all its finite histories are STMS. We also show that STMS is weaker than Opacity, a well-known consistency condition, and that under certain restrictions, STMS is equivalent to Opacity.
Our results suggest a new approach to evaluate and compare TM consistency conditions. They can also reduce the effort of proving that a TM implements its programming language interface correctly, by only requiring its developer to show that it satisfies the corresponding consistency condition.
|Copyright||The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information|
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2015/PHD/PHD-2015-13), rather than to the URL of the PDF or PS files directly. The latter URLs may change without notice.
To the list of the PHD technical reports of 2015
To the main CS technical reports page
Computer science department, Technion