Journal article icon

Journal article

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
More from this funder
Grant:
Task 2269.002
Publisher:
Springer Verlag Publisher's website
Journal:
Lecture Notes in Computer Science Journal website
Volume:
9636
Pages:
515-530
Publication date:
2016-04-09
Acceptance date:
2016-01-01
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
Source identifiers:
572454
Keywords:
Pubs id:
pubs:572454
UUID:
uuid:75e286e6-8ddb-4dc9-bf84-9cae949ac674
Local pid:
pubs:572454
Deposit date:
2017-01-28

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