Formalizing and checking thread refinement for data-race-free execution models

Journal article

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.

Authors: Poetzl, D; Kroening, D

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer Verlag
• Journal: Lecture Notes in Computer Science
• Volume: 9636
• Pages: 515-530
• Publication date: 2016-04-09
• Acceptance date: 2016-01-01
• DOI: 10.1007/978-3-662-49674-9_30
• EISSN: 1611-3349
• ISSN: 0302-9743
• Keywords: Conference Proceeding; cs.PL