可组合的描述符泄露类型检查

Compositional Type Checking of Descriptor Leaking

应用程序通过操作系统的系统调用对文件描述符进行操作并管理文件资源。如果应用程序对资源描述符的管理出现错误并发生描述符泄漏,会严重影响系统的可用性。据此,提出了一种检查程序是否会导致描述符泄漏的类型系统,给出了描述符操作方法的语义和类型约束,证明了类型系统的可靠性定理。此外,还初步讨论了该类型系统在并发程序下的扩展。

Programs manage files, as a kind of resource, using system calls provided by operating systems to manipulate file descriptors. The availability of the system will be significantly degenerated if programs deal with file descriptors ar- bitrarily. We proposed a type system to check whether a program leaks some resource （typically, file） descriptors. We defined semantics for descriptor-related operations in sequential programs, and proved that the type system is sound with respect to our semantics. In addition, the extension of this type system with concurrent semantics was discussed.