Static Analysis of Multi-Core Applications

Award Information
Agency:
Department of Defense
Branch
Defense Advanced Research Projects Agency
Amount:
$99,000.00
Award Year:
2007
Program:
SBIR
Phase:
Phase I
Contract:
W31P4Q-08-C-0171
Agency Tracking Number:
07SB2-0175
Solicitation Year:
2007
Solicitation Topic Code:
SB072-010
Solicitation Number:
2007.2
Small Business Information
GRAMMATECH, INC.
317 N. Aurora Street, Ithaca, NY, 14850
Hubzone Owned:
N
Socially and Economically Disadvantaged:
N
Woman Owned:
N
Duns:
603978321
Principal Investigator:
David Melski
VP of Research
(607) 273-7340
melski@grammatech.com
Business Contact:
Ray Teitelbaum
CEO and Chairman
(607) 273-7340
tt@grammatech.com
Research Institution:
n/a
Abstract
The goal of this project is to develop a static analysis tool that identifies program flaws that may arise when executing on a multi-core processor. In particular, we will target flaws that arise in lock-free algorithms. Concurrent programs are often plagued by race conditions on shared data. Lock-based solutions to this problem are conceptually simple and work reasonably well. However, they typically do not perform well for the fine-grained concurrency that is often needed on multi-core processors. As the number of processor cores increases, lock contention also increases and many processors are left idle. Lock-free algorithms achieve much greater processor utilization (and better performance) as the number of cores increases. However, lock-free algorithms are difficult to reason about. (To make matters worse, multi-core processors often use a relaxed memory model.) This project will focus on using bounded model checking in order to verify libraries that implement lock-free algorithms.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government