Context-Sensitive Synchronization-Sensitive Analysis is Undecidable

This paper illustrates one source of difficulty in statically analyzing concurrent programs. In the realm of static interprocedural analysis, one talks of context-sensitive analyses: these are analyses that are precise with respect to calling-context, in a formally defined way. In a concurrent program that contains synchronization constructs, one can similarly define the notion of synchronization-sensitive analyses: these are analyses that are precise with respect to the synchronization structure of the program. Efficiene context-sensitive analysis algorithms have been developed for a number of analysis problems. Intraprocedural synchronization-sensitive analyses can be expensive (they are known to be NP-hard), but it is straight forward to show that they are possible for a number of analysis problems. In this paper we address the problem of interprocedural analysis of concurrent programs. Specifically, we show that context-sensitive and synchronization-sensitive analysis is impossible even for the simplest of analysis problems.