A Resource-Sensitive Semantic Framework for Concurrent Programs

并发程序的资源敏感语义框架

• 批准号: 0429505
• 负责人: Stephen Brookes
• 金额: $ 30万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-05-01 至 2009-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0429505&HistoricalAwards=false
• 关键词: Resource; Sensitive; Semantic; Framework; Concurrent

0429505Stephen D. BrookesCMUA Resource-Sensitive Framework for Concurrent ProgramsThis project will develop a trace-theoretic denotational semantic framework and a concurrent form of separation logic, for compositional reasoning about the behavior of concurrent programs which share access to mutable state. Such programs are widespread, for instance in Java applications. Pointers are difficult to reason about, and concurrency makes the problem harder. Unlike previous models, our semantics will detect the potential for races, such as an attempt by one process to write on a piece of state used by anotherprocess. Races cause unpredictable, possibly irreproducible, behavior, and our semantics will treat a possible race as a catastrophe. This semantics will be used in validating logics and advancing methodologies for the design of correct race-free parallel programs.

0429505斯蒂芬·D. BrookesCMUA Resource-Sensitive Framework for Concurrent Programs这个项目将开发一个跟踪理论的指称语义框架和一个并发形式的分离逻辑，用于对共享可变状态访问的并发程序的行为进行组合推理。 这样的程序很普遍，例如在Java应用程序中。指针很难推理，并发性使问题更难解决。 与以前的模型不同，我们的语义将检测到潜在的竞争，如一个进程试图写在一块状态使用另一个进程。竞争导致不可预测的，可能是不可复制的行为，我们的语义将把可能的竞争视为灾难。这种语义将被用于验证逻辑和先进的方法，正确的种族免费并行程序的设计。