Automatic generation of deadlock detection algorithms for a family of microarchitecture description languages of communication fabrics

摘要

In the multi-core era, ensuring deadlock freedom of communication fabrics is an important challenge. Intel proposed xMAS, a microarchitecture description language (MaDL), to support the formal modelling and verification of communication fabrics. The xMAS language is restricted to eight basic primitives. Using this restriction, an efficient deadlock detection technique has been defined. This technique is tailored to the eight primitives, which are not sufficient to model many realistic designs. We ex­hibit two primitives, namely, an adaptive switch and a synchron­ization barrier, that cannot be expressed or analyzed using the current xMAS language and tools. Our main contribution is to automatically generate an efficient deadlock detection algorithm tailored to a given set of primitives. We define a set of core primitives and extension mechanisms for user-defined primitives. This creates a family of MaDL's together with a family of tailored and efficient deadlock detection algorithms. We prove that the automatically generated algorithms are correct by construction, i.e., they correctly detect deadlocks in all fabrics defined in the language for which they are generated. These algorithms handle message dependencies, counters, virtual channels, parametric buffer sizes, and many other aspects of micro-architectural models. The effectiveness of our approach is demonstrated on models with adaptive switches and synchronization barriers. Our approach automatically provides efficient deadlock detection for a large family of MaDL's.