A Resource-Sensitive Framework for Concurrent Programs
This 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 another process. 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.
