Sciweavers

Share
APLAS
2007
ACM

Local Reasoning for Storable Locks and Threads

9 years 5 months ago
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.
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rin
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where APLAS
Authors Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
Comments (0)
books