Local Reasoning for Storable Locks and Threads

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv

Abstract

We present a resource-oriented program logic that is able to reason about concurrent heap-manipulating programs with unbounded numbers of dynamically-allocated locks and threads. The logic is inspired by concurrent separation logic, but handles these more realistic concurrency primitives. We demonstrate that the proposed logic allows for local reasoning about programs that exhibit a high degree of information hiding in their locking mechanisms. Soundness is proved using a novel thread-local fixed-point semantics.

Details

Publication typeTechReport
NumberMSR-TR-2007-39
Pages33
InstitutionMicrosoft Research
PublisherMicrosoft Research
> Publications > Local Reasoning for Storable Locks and Threads