Publication:
Moving around: Lipton's reduction for TSO - (Regular submission)

Placeholder

Departments

School / College / Institute

Program

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

item.page.datauri

Link

Rights

Copyrights Note

Endorsement

Review

Supplemented By

Referenced By

0

Views

0

Downloads

View PlumX Details