多线程多态类型汇编语言死锁检测的类型推断
Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
摘要：
我们以前开发了一个多态类型系统和类型检查器的多线程锁为基础的多态类型汇编语言（MIL），确保良好的类型程序不会遇到竞争条件。本文扩展了这样的工作，考虑到死锁。扩展类型系统验证是否以正确的顺序获取了锁。为此，我们需要一种带有注释的语言来指定锁定顺序。我们提出了一个算法来推断注释，而不是要求程序员（或编译器的后端）专门注释每个新引入的锁。其结果是一个类型检查器，其输入语言与以前一样是非修饰的，但它进一步检查程序是否免于死锁。
英文摘要：
We previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type system verifies that locks are acquired in the proper order. Towards this end we require a language with annotations that specify the locking order. Rather than asking the programmer (or the compiler's backend) to specifically annotate each newly introduced lock, we present an algorithm to infer the annotations. The result is a type checker whose input language is non-decorated as before, but that further checks that programs are exempt from deadlocks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
