Reasoning about Data Structures, Concurrency, and Resources

关于数据结构、并发性和资源的推理

• 批准号: 0541021
• 负责人: John Reynolds
• 金额: --
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-04-15 至 2010-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541021&HistoricalAwards=false
• 关键词: Reasoning; about; Data; Structures; Concurrency

Abstract0541021John C. ReynoldsCarnegie Mellon UniversityReasoning about Shared Structure and ConcurrencyThe specification and verification of computer programs is investigated, along with the semantics needed to insure the soundness of verification. Of specific interest are:Separation Logic, which treats programs employing shared mutable data structures or shared-variable concurrency. The goal is to extend the logic to high-level languages using safe type systems and automaticstorage reclamation, and also to machine-level languages permitting pointers to code to be embedded within data structures.Grainless Semantics, which treats shared-variable concurrency without imposing any default level of atomic operations, by regarding race conditions (i.e., simultaneous access to the same storage by concurrentprocesses) as catastrophic events. The goal is to simplify the understanding of programs by avoiding useless distinctions between programs with unacceptable behavior.The intellectual merit of this research is that it will substantially increase the domain of discourse of separation logic, and facilitate soundness arguments for this and other logics for shared-variableconcurrency.The broader impact is that it will become easier to avoid errors in an important class of useful but difficult computer programs. Eventually, it should be possible to automate proof-checking in the logic so thatprograms in this class can be accompanied by machine-checkable proofs of their correctness.

Abstract0541021约翰·雷诺兹卡内基梅隆大学关于共享结构和并发性的推理研究了计算机程序的规范和验证，以及确保验证健全性所需的语义。 特别感兴趣的是：分离逻辑，它处理使用共享可变数据结构或共享变量并发的程序。 目标是使用安全类型系统和自动存储回收将逻辑扩展到高级语言，以及允许将代码指针嵌入数据结构中的机器级语言。无粒度语义，它处理共享变量并发而不强加任何原子操作的默认级别，通过将竞争条件（即并发进程同时访问同一存储）视为灾难性事件。 目标是通过避免具有不可接受行为的程序之间的无用区别来简化对程序的理解。这项研究的智力价值在于它将大大增加分离逻辑的讨论领域，并促进该逻辑和其他共享逻辑的合理性论证。 - 变量并发。更广泛的影响是，在一类重要的有用但困难的计算机程序中避免错误将变得更加容易。 最终，应该可以在逻辑中自动进行校对检查，以便此类程序可以附有机器可检查的正确性证明。