Formalizing and checking thread refinement for data-race-free execution models
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 ter...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Published: |
Springer Verlag
2016
|
| _version_ | 1797076204821413888 |
|---|---|
| author | Poetzl, D Kroening, D |
| author_facet | Poetzl, D Kroening, D |
| author_sort | Poetzl, D |
| collection | OXFORD |
| description | 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 in more cases and leads to more efficient and simpler procedures for refinement checking. We develop the theory for the SC for- DRF execution model (using locks for synchronization), and show that its application in compiler testing yields speedups of on average more than two orders of magnitude compared to a previous approach. |
| first_indexed | 2024-03-07T00:00:49Z |
| format | Journal article |
| id | oxford-uuid:75e286e6-8ddb-4dc9-bf84-9cae949ac674 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:00:49Z |
| publishDate | 2016 |
| publisher | Springer Verlag |
| record_format | dspace |
| spelling | oxford-uuid:75e286e6-8ddb-4dc9-bf84-9cae949ac6742022-03-26T20:12:16ZFormalizing and checking thread refinement for data-race-free execution modelsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:75e286e6-8ddb-4dc9-bf84-9cae949ac674Symplectic Elements at OxfordSpringer Verlag2016Poetzl, DKroening, DWhen 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 in more cases and leads to more efficient and simpler procedures for refinement checking. We develop the theory for the SC for- DRF execution model (using locks for synchronization), and show that its application in compiler testing yields speedups of on average more than two orders of magnitude compared to a previous approach. |
| spellingShingle | Poetzl, D Kroening, D Formalizing and checking thread refinement for data-race-free execution models |
| title | Formalizing and checking thread refinement for data-race-free execution models |
| title_full | Formalizing and checking thread refinement for data-race-free execution models |
| title_fullStr | Formalizing and checking thread refinement for data-race-free execution models |
| title_full_unstemmed | Formalizing and checking thread refinement for data-race-free execution models |
| title_short | Formalizing and checking thread refinement for data-race-free execution models |
| title_sort | formalizing and checking thread refinement for data race free execution models |
| work_keys_str_mv | AT poetzld formalizingandcheckingthreadrefinementfordataracefreeexecutionmodels AT kroeningd formalizingandcheckingthreadrefinementfordataracefreeexecutionmodels |