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 local reasoning about programs for which there exists a notion of dynamic ownership of heap parts by locks and threads. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., & Sagiv, M. (2007). Local reasoning for storable locks and threads. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4807 LNCS, pp. 19–37). Springer Verlag. https://doi.org/10.1007/978-3-540-76637-7_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
