A Resource-Sensitive Semantic Framework for Concurrent Programs

点击翻译按钮获取中文摘要

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.