Paper Info
Title
Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models (Extended Version)
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 theories of valid optimizations 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 the state of threads at synchronization operations, and show that it provides several advantages: it supports more optimizations, 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 a compiler testing setting leads to large performance improvements.
Year
Venue
Field
2015
CoRR
Program code,Synchronization,Programming language,Computer science,Parallel computing,Compiler,Thread (computing),Execution model,Thread safety,Syntax
DocType
Volume
Citations 
Journal
abs/1510.07171
0
PageRank 
References 
Authors
0.34
11
2
Name
Order
Citations
PageRank
Daniel Poetzl1704.04
Daniel Kroening23084187.60