A Resource-Sensitive Semantic Framework for Concurrent Programs

0429505 Stephen D.BrookesCMUA资源敏感的并发程序框架这个项目将开发一个踪迹理论的指称语义框架和一种并发形式的分离逻辑，用于对共享访问可变状态的并发程序的行为进行组合推理。这样的程序很普遍，例如在Java应用程序中。指针很难推理，而并发性使问题变得更加困难。与以前的模型不同，我们的语义将检测竞争的可能性，例如一个进程试图写入另一个进程使用的一段状态。种族导致不可预测的、可能是不可复制的行为，我们的语义学将把可能的种族视为灾难。这种语义将用于验证逻辑和改进设计正确的无竞争并行程序的方法。

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.