05275785

a

05275785 Gotsman, Alexey Berdine, Josh Cook, Byron Rinetzky, Noam Sagiv, Mooly Local reasoning for storable locks and threads. Shao, Zhong (ed.), Programming languages and systems. 5th Asian symposium, APLAS 2007, Singapore, November 29--December 1, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-76636-0/pbk). Lecture Notes in Computer Science 4807, 19-37 (2007). 2007 Berlin: Springer EN

doi:10.1007/978-3-540-76637-7_3

Summary: 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.