Pi演算的资源使用分析
Resource Usage Analysis for the Pi-Calculus
摘要:
我们提出了一个基于类型的资源使用分析的-演算扩展资源创建/访问原语。资源使用分析的目标是静态地检查程序是否以有效的方式访问资源,如文件和内存。我们的类型系统是一个扩展以前的行为类型系统的演算,并可以保证安全属性,没有无效的访问被执行,以及必要的访问(如关闭操作的文件)最终执行,除非程序发散的属性。为使程序员从编写复杂类型注释的负担中解脱出来,本文还开发了一个完善的类型系统类型推断算法。基于该算法,我们已经实现了一个原型的资源使用分析器的演算。据作者所知,我们是第一个基于类型的资源使用分析,处理一个表达并发语言,如pi演算。
英文摘要:
We propose a type-based resource usage analysis for the π-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a program accesses resources such as files and memory in a valid manner. Our type system is an extension of previous behavioral type systems for the π-calculus, and can guarantee the safety property that no invalid access is performed, as well as the property that necessary accesses (such as the close operation for a file) are eventually performed unless the program diverges. A sound type inference algorithm for the type system is also developed to free the programmer from the burden of writing complex type annotations. Based on the algorithm, we have implemented a prototype resource usage analyzer for the π-calculus. To the authors' knowledge, ours is the first type-based resource usage analysis that deals with an expressive concurrent language like the pi-calculus.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。