Local Reasoning for Storable Locks and Threads

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 local reasoning about programs for which there exists a notion of dynamic ownership of heap parts by locks and threads.

slides.pdf
PDF file
paper.pdf
PDF file

In  Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

TypeInproceedings
Pages19-37
Volume4807
SeriesLecture Notes in Computer Science
ISBN978-3-540-76636-0

Previous Versions

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local Reasoning for Storable Locks and Threads, Microsoft Research, April 2007.

> Publications > Local Reasoning for Storable Locks and Threads