|
December 2009
A paper by Professor Sriram Sankaranarayanan
was the recipient of the
ACM SIGSOFT
Distinguished Paper Award.
The award was presented at the
24th ACM/IEEE International Conference on Automated Software Engineering (ASE 2009)
held recently in Auckland, New Zealand.
The paper, titled
Symbolic Deadlock Analysis in Concurrent Libraries and their Clients,
was written with co-authors
Jyotirmoy Deshmukh and E. Allen Emerson,
both of the University of Texas at Austin:
Methods in object-oriented concurrent libraries hide internal synchronization
details. However, information hiding may result in clients causing thread
safety violations by invoking methods in an unsafe manner. Given such a
library, we present a technique for inferring interface contracts that specify
permissible concurrent method calls and patterns of aliasing among method
arguments, such that the derived contracts guarantee deadlock free execution
for the methods in the library. The contracts also help client developers by
documenting required assumptions about the library methods. Alternatively,
the contracts can be statically enforced in the client code to detect potential
deadlocks in the client. Our technique combines static analysis with a symbolic
encoding for tracking lock dependencies, allowing us to synthesize contracts
using a SMT solver. Our prototype tool analyzes over a million lines of code
for some widely-used Java libraries within an hour, thus demonstrating its
scalability and efficiency. Furthermore, the contracts inferred by our approach
have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have
been a part of bug-reports filed by users and developers of the client code.
ACM SIGSOFT encourages SIGSOFT-sponsored conferences to designate a number of
accepted papers for ACM SIGSOFT Distinguished Paper Awards for the conference.
The award is given to approximately fifteen papers annually and was given to
two papers at ASE 2009.
|
