Conference item icon

Conference item

Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models

Abstract:

When optimizing a thread in a concurrent program (either done manually or by the compiler), it must be guaranteed that the resulting thread is a refinement of the original thread. Most definitions of refinement are formulated in terms of valid syntactic transformations on the program code, or in terms of valid transformations on thread execution traces. We present a new theory formulated instead in terms of state transitions between synchronization operations. Our new method shows refinement ...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
  • (Accepted manuscript, pdf, 362.6KB)
Publisher copy:
10.1007/978-3-662-49674-9_30

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Publisher:
Springer Verlag Publisher's website
Host title:
Tools and Algorithms for the Construction and Analysis of Systems
Publication date:
2016-04-09
DOI:
ISSN:
0302-9743
Source identifiers:
581538
Pubs id:
pubs:581538
UUID:
uuid:8793e851-566c-4120-8aa9-54ebc05526aa
Local pid:
pubs:581538
Deposit date:
2016-01-09

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP