SOUND, PRECISE AND EFFICIENT STATIC RACE DETECTION FOR MULTI-THREADED PROGRAMS

dc.contributor.advisorHicks, Michaelen_US
dc.contributor.advisorFoster, Jeffreyen_US
dc.contributor.authorPratikakis, Polyviosen_US
dc.contributor.departmentComputer Scienceen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.date.accessioned2008-10-11T05:53:02Z
dc.date.available2008-10-11T05:53:02Z
dc.date.issued2008-08-21en_US
dc.description.abstractMultithreaded programming is increasingly relevant due to the growing prevalence of multi-core processors. Unfortunately, the non-determinism in parallel processing makes it easy to make mistakes but difficult to detect them, so that writing concurrent programs is considered very difficult. A data race, which happens when two threads access the same memory location without synchronization is a common concurrency error, with potentially disastrous consequences. This dissertation presents Locksmith, a tool for automatically finding data races in multi-threaded C programs by analyzing their source code. Locksmith uses a collection of static analysis techniques to reason about program properties, including a novel effect system to compute memory locations that are shared between threads, a system for inferring ``guarded-by'' correlations between locks and memory locations, and a novel analysis of data structures using existential types. We present the main analyses in detail and give formal proofs to support their soundness. We discuss the implementation of each analysis in Locksmith, present the problems that arose when extending it to the full C programming language, and discuss some alternative solutions. We provide extensive measurements for the precision and performance of each analysis and compare alternative techniques to find the best combination.en_US
dc.format.extent1497819 bytes
dc.format.mimetypeapplication/pdf
dc.identifier.urihttp://hdl.handle.net/1903/8627
dc.language.isoen_US
dc.subject.pqcontrolledComputer Scienceen_US
dc.titleSOUND, PRECISE AND EFFICIENT STATIC RACE DETECTION FOR MULTI-THREADED PROGRAMSen_US
dc.typeDissertationen_US

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
umi-umd-5743.pdf
Size:
1.43 MB
Format:
Adobe Portable Document Format