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: | Conference item |
| Published: |
Springer Verlag
2016
|
| _version_ | 1797080047918514176 |
|---|---|
| author | Kroening, D Poetzl, D |
| author_facet | Kroening, D Poetzl, D |
| author_sort | Kroening, 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 SCfor-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:54:32Z |
| format | Conference item |
| id | oxford-uuid:8793e851-566c-4120-8aa9-54ebc05526aa |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:54:32Z |
| publishDate | 2016 |
| publisher | Springer Verlag |
| record_format | dspace |
| spelling | oxford-uuid:8793e851-566c-4120-8aa9-54ebc05526aa2022-03-26T22:11:35ZFormalizing and Checking Thread Refinement for Data-Race-Free Execution ModelsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:8793e851-566c-4120-8aa9-54ebc05526aaSymplectic Elements at OxfordSpringer Verlag2016Kroening, DPoetzl, 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 SCfor-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 | Kroening, D Poetzl, 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 kroeningd formalizingandcheckingthreadrefinementfordataracefreeexecutionmodels AT poetzld formalizingandcheckingthreadrefinementfordataracefreeexecutionmodels |