Type-Based Analysis of Linear Communications

This chapter presents a tool called Hypha for the type-based analysis of processes that communicate on linear channels. We describe the specification language used to model the systems under analysis (Section 9.1) followed by the typing rules on which the tool is based in order to verify two properties of systems, deadlock freedom and lock freedom (Section 9.2). In the final part of the chaper we illustrate the expressiveness and the limitations of the tool discussing a number of examples inspired by representative communication patterns using in parallel computing (Section 9.3) and then discuss closely related work (Section 9.4). The tool can be downloaded from the author’s home page, the type system has been described by Padovani [18] and the corresponding reconstruction algorithms by Padovani et al. [19, 20]