Checking race freedom via linear programming

Research output: Contribution to journalArticle

2 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.

Original languageEnglish
Pages (from-to)1-10
Number of pages10
JournalACM SIGPLAN Notices
Volume43
Issue number6
Publication statusPublished - 2008 Jun
Externally publishedYes

Fingerprint

Linear programming
Static analysis
Joining
Synchronization

Keywords

  • Fractional Capabilities
  • Linear Programming

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Checking race freedom via linear programming. / Terauchi, Tachio.

In: ACM SIGPLAN Notices, Vol. 43, No. 6, 06.2008, p. 1-10.

Research output: Contribution to journalArticle

@article{de2edc33d23144aebcb7a5ac2b0e6c6c,
title = "Checking race freedom via linear programming",
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.",
keywords = "Fractional Capabilities, Linear Programming",
author = "Tachio Terauchi",
year = "2008",
month = "6",
language = "English",
volume = "43",
pages = "1--10",
journal = "SIGPLAN Notices (ACM Special Interest Group on Programming Languages)",
issn = "0362-1340",
publisher = "Association for Computing Machinery (ACM)",
number = "6",

}

TY - JOUR

T1 - Checking race freedom via linear programming

AU - Terauchi, Tachio

PY - 2008/6

Y1 - 2008/6

N2 - 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.

AB - 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.

KW - Fractional Capabilities

KW - Linear Programming

UR - http://www.scopus.com/inward/record.url?scp=67650088512&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=67650088512&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:67650088512

VL - 43

SP - 1

EP - 10

JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

SN - 0362-1340

IS - 6

ER -