SHF: SMALL: Practical Linear Types for Safe Protocols

软件错误经常出现，因为程序的一个组件没有正确地遵循一个定义良好的协议来访问一些有状态资源。常见的例子包括程序误用了操作系统提供的资源句柄，错误地多次释放相同的内存或其他资源，或者未能正确顺序调用复杂的程序模块。这种违反协议的行为会导致软件崩溃或意想不到的行为，可能会带来灾难性的后果。该项目的目标是开发编程语言技术，使软件开发人员能够方便地描述有状态的协议资源。该技术将在设计时通过静态检查程序是否适当地遵循所需的协议来发现此类错误，从而排除广泛的软件缺陷。新的语言机制将是通用的、实用的，并且适用于从内存管理到传统协议实现的各种应用程序。研究人员将创建一个编译器基础架构原型，并通过机器检查的类型稳健性证明来确定方法的正确性。该项目的主要影响是开发技术，以帮助在软件设计生命周期的早期消除此类编程错误，从而降低构建正确、可靠的软件的成本。

Software errors frequently arise because a component of the program doesnot correctly follow a well-defined protocol for accessing some statefulresource. Common examples include programs that misuse resource handlesprovided by the operating system, incorrectly deallocate the same memoryor other resource multiple times, or fail to properly sequence calls toa complex program module. Such protocol violations lead to softwarecrashes or unintended behavior, potentially with disastrousconsequences.The project objective is to develop programming language technology toallows software developers to conveniently describe protocols overstateful resources. This technology will uncover such bugs at designtime by statically checking whether the program is appropriatelyfollowing the desired protocols, thereby ruling out the wide class ofsoftware flaws. The new language mechanisms will be general purpose,practical, and suitable for use in a wide variety of applicationsranging from memory management to traditional protocol implementation.The researchers will create a compiler infrastructure prototype andestablish the correctness of the approach by a machine-checked proof oftype soundness. The primary broader impact of the project is thedevelopment of technology to help eliminate such programming errorsearly in the software-design life cycle to decrease the cost of buildingcorrect, reliable software.