Publication: Moving around: Lipton's reduction for TSO - (Regular submission)
Program
KU-Authors
KU Authors
Co-Authors
Sezgin, Ali
Publication Date
Language
Embargo Status
Journal Title
Journal ISSN
Volume Title
Alternative 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).
Source
Publisher
Springer International Publishing Ag
Subject
Computer Science, Artificial intelligence, Software engineering
Citation
Has Part
Source
Verified Software: Theories, Tools, and Experiments
Book Series Title
Edition
DOI
10.1007/978-3-319-29613-5_10