[TYPES] static analyses for shared resource accesses in multi-threaded systems

[Nels Beckman]

Hello Austin,

What you are describing sounds quite a bit like my thesis research.
This work could best be described as "static typestate checking for
multi-threaded OO programs." Our analysis, which is presented as a
type system, uses aliasing permissions, from Kevin Bierhoff's thesis
work but inspired by Boyland's fractional permissions, to approximate
thread-sharedness. There are various permission kinds, such as unique,
immutable, and shared, which permit or prohibit modification through a
program references, and which allow for quite a bit of flexibility in
aliasing.

We track the state of an object in an object protocol statically, but
discard the object state (to simulate thread interleaving) when the
permission to an object indicates the object may be concurrently
modified.

The best reference is from OOPSLA 2008:
N. Beckman, K. Bierhoff, J. Aldrich. Verifying Correct Usage of Atomic
Blocks and Typestate. In Proceedings of ACM SIGPLAN International
Conference on Object-Oriented Programming, Systems, Languages, and
Applications 2008 (OOPSLA '08) Nashville, TN, USA. October 19-23,
2008.
http://doi.acm.org/10.1145/1449764.1449783

This paper used atomic blocks as the means of mutual exclusion,
although we have recently extended the system to support synchronized
blocks as well.

Additionally, we've implemented our approach as a static analysis for
Java called Plural. That tool is available, open source, on Google
code:
http://code.google.com/p/pluralism/

Thanks a lot,
Nels

--
--------------------------------------
Nels Beckman
Carnegie Mellon University
nbeckman at cs.cmu.edu
http://www.nelsbeckman.com