A New Proof for the Undecidability of Context-Sensitive Synchronization-Sensitive Analysis

Concurrent interprocedural program analysis is an undecidable problem. To analysis concurrent interprocedural program, we need understand why the problem is undecidable. [1] proofs the undecidable problem via constructing a instance of PCP problem with three concurrent tasks. This paper constructs an instance of PCP problem of the concurrent interprocedural program analysis problem, but with only two concurrent tasks. The proof offers insights into the undecidable problem. It comes from interleaved patterns of procedural matching in a task, where at least one procedural matching comes from other concurrent task, whose procedural matching is projected to prior task through synchronization matching. A necessary condition of the undecidable problem is given as analysis result.