Reasoning about Data Structures, Concurrency, and Resources

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

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.