Type of Talk: UTCS Colloquium

Speaker/Affiliation: Roma

n Manevish/ UCLA

Date/ Time: July 10, 2009, 2:00-3:25pm

Locati

on: TAY 3.128

Host: Keshav Pingali

Talk Title: Partially Disjunct

ive Shape Analysis

Talk Abstract:

Abstract: Modern programs rely
significantly on the use of dynamically-allocated linked data structures.
Shape-analysis algorithms statically analyze a program to determine inform

ation about these data structures, e.g, "does variable x point to an acyc

lic list?", "can variables x and y reach the same object via pointer trave

rsals?". The algorithms are conservative (sound), i.e., the discovered i

nformation is true for every input, and thus can be applied for different

uses, e.g., for program verification,
optimization, parallelization,
etc.

Disjunctive shape analyses operate by abstracting the concrete s

tores into (bounded) shape graphs. At control flow join points, the shape
graphs are merged by using disjunctions (set union), which leads to an ex

ponential explosion in the number of shape graphs. In concurrent programs t

his problem is even more acute due to the blow up in the control flow of di

fferent threads.

This talk presents sound abstraction techniques aimed
at taming the size of the state space by abstracting disjunctions, as wel

l as soundly approximating program statements. These techniques were imple

mented and used to prove properties of sequential programs and concurrent p

rograms with fine-grained parallelism. The analyses were used to prove a v

ariety of challenging properties, e.g., linearizability of concurrent dat

a structure implementations.