Publication: Moving around: Lipton's reduction for TSO - (Regular submission)
Program
KU-Authors
KU Authors
Co-Authors
Sezgin, Ali
Advisor
Publication Date
2016
Language
English
Type
Conference proceeding
Journal Title
Journal ISSN
Volume Title
Abstract
We generalize Lipton's reduction theory, hitherto limited to SC, for TSO programs. We demonstrate the use of our theory by specifying the conditions under which a particular write is SC-like (i.e. placing a fence immediately after the write does not constrain the behavior of the overall program) and a library implementation can be safely used (i.e. compositionality). Our theory is complete: a program has only SC behaviors iff there is a proof that establishes that every write in the program is SC-like. We adapt the notion of program abstraction to TSO analysis via our theory. We define precisely what is meant by abstraction, and propose a methodology by which one can obtain via abstraction SC summaries of a program which may have non-SC behaviors. Finally, we show how checking whether a write instruction is SC-like can be mechanized. We describe a transformation in which the execution of each thread of the original program (under TSO) is simulated by the execution of two tightly coupled threads in the new program (under SC).
Description
Source:
Verified Software: Theories, Tools, and Experiments
Publisher:
Springer International Publishing Ag
Keywords:
Subject
Computer Science, Artificial intelligence, Software engineering