Checking race freedom via linear programming

Tachio Terauchi*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

26 Citations (Scopus)

Abstract

We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs. copyright

Original languageEnglish
Title of host publicationPLDI'08
Subtitle of host publicationProceedings of the 2008 SIGPLAN Conference on Programming Language Design and Implementation
Pages1-10
Number of pages10
DOIs
Publication statusPublished - 2008
Externally publishedYes
Event2008 ACM SIGPLAN Conference on Programming Language Design and Implementation 2008, PLDI'08 - Tucson, AZ, United States
Duration: 2007 Jun 72007 Jun 13

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other2008 ACM SIGPLAN Conference on Programming Language Design and Implementation 2008, PLDI'08
Country/TerritoryUnited States
CityTucson, AZ
Period07/6/707/6/13

Keywords

  • Fractional capabilities
  • Linear programming

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Checking race freedom via linear programming'. Together they form a unique fingerprint.

Cite this