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

[Austin Anderson]

I would be interested to know if there is any existing work on static
analyses to guarantee that threads in a multi-threaded system access some
shared resources (such as state) according to some access policy. I have
become interested in such a problem from reading about session typing, which
is an analogous analysis used to guarantee that threads in a multi-threaded
system communicate according to a specific protocol. Session typing makes
several assumptions, however, e.g. a global communications queue with
temporal ordering, which seem to be inappropriate for non-message-passing
systems. It would, I think, be possible to apply the analyses used in
session typing if we made use of a global read/write queue, but I think this
is too much of a restriction for most shared state paradigms.

Hence I am looking for analyses which guarantee that resources in a
multi-threaded environment are accessed according to a protocol, in a system
where we can have interleaving of actions. I am primarily interested in
approaches which are purely static and do not involve model checking. One
approach which I have already discovered which does make use of model
checking is the thesis:

Typed Static Analysis for Concurrent, Policy-Based, Resource Access Control
Nicholas Nguyen
University of Sussex

Any suggestions would be much appreciated.

Austin Anderson
University of Southampton