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
Funding
Bibliographic Details
- 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
Item Description
- Keywords:
- Pubs id:
-
pubs:572454
- UUID:
-
uuid:75e286e6-8ddb-4dc9-bf84-9cae949ac674
- Local pid:
- pubs:572454
- Deposit date:
- 2017-01-28
Terms of use
- Copyright holder:
- Springer Verlag
- Copyright date:
- 2016
- Notes:
- © Springer-Verlag Berlin Heidelberg 2016. Presented at TACAS 2016: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2-8 April 2016: Eindhoven, The Netherlands). This is the accepted manuscript version of the article. The final version is available online from Springer at: [10.1007/978-3-662-49674-9_30].
If you are the owner of this record, you can report an update to it here: Report update to this record