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

Placeholder

Organizational Units

Program

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

Citation

Endorsement

Review

Supplemented By

Referenced By

Copy Rights Note

0

Views

0

Downloads

View PlumX Details