On analysis of deadlock and blocking freeness in isomorphic module systems

This paper is about efficiently analyzing deadlock and blocking for systems consisting of isomorphic modules instantiated from a template. By refining the template, our approach captures essential interactions among modules and efficiently determine whether a system of an arbitrary number of modules is deadlock free or blocking free, while avoid their explicit synchronization. When the answer is negative, our approach identifies the largest module number, up to which the system satisfies each of these properties.