CAREER: Design, Applications, and Foundations of Safe, Low-Level Programming Languages

职业：安全、低级编程语言的设计、应用和基础

• 批准号: 9875536
• 负责人: John Morrisett
• 金额: $ 20.5万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-03-01 至 2004-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9875536&HistoricalAwards=false
• 关键词: CAREER; Design; Applications; Foundations; Safe

9875536 J. Gregory MorrisettWe are examining the design, applications, and foundations of low-level, but safe programming languages. The goal is as in C, to give programmers (and compilers) the option of tight control over instructions and memory management, but as with high-level languages such as Java or SML, provide the abstraction and safety mechanisms needed to engineer large systems. In particular, we are exploring type systems that support the elimination of unnecessary dynamic tests, provide manual control over data layout, and give fine-grained control over the [de]allocation of memory objects, all without sacrificing the safety guarantees of high-level languages. We expect that the type systems for these low-level languages will have a number of compelling benefits. First, a programmer unsatisfied with automatically generated code or automatic memory managers will have the facilities to hand-optimize the code. As long as the resulting code continues to type-check, the programmer can be assured that the code is still safe. Second, typed low-level languages can serve as compiler intermediate or target languages. Here, the types can be used to support advanced optimizations, to ensure that compilation invariants are maintained, and to support security in extensible systems. Finally, typed low-level languages can serve as safe "glue" between high-level language systems and low-level services, such as runtime systems, operating systems, or hardware devices, thereby providing an evolutionary path from legacy software to next-generation systems.

9875536 J. Gregory Morrisett我们正在研究低级但安全的编程语言的设计，应用程序和基础。 其目标与C语言一样，为程序员（和编译器）提供对指令和内存管理的严格控制，但与Java或SML等高级语言一样，提供了设计大型系统所需的抽象和安全机制。 特别是，我们正在探索支持消除不必要的动态测试的类型系统，提供对数据布局的手动控制，并对内存对象的分配进行细粒度控制，所有这些都不会牺牲高级语言的安全保证。 我们期望这些低级语言的类型系统将有许多令人信服的好处。 首先，不满意自动生成代码或自动内存管理器的程序员将有工具手动优化代码。 只要生成的代码继续进行类型检查，程序员就可以确信代码仍然是安全的。 第二，类型化的低级语言可以作为编译器的中间语言或目标语言。 在这里，类型可用于支持高级优化，确保维护编译不变量，并支持可扩展系统中的安全性。 最后，类型化的低级语言可以作为高级语言系统和低级服务（如运行时系统、操作系统或硬件设备）之间的安全“粘合剂”，从而提供从遗留软件到下一代系统的进化路径。