Paper Info
Title
Verifying concurrent memory reclamation algorithms with grace
Abstract
Memory management is one of the most complex aspects of modern concurrent algorithms, and various techniques proposed for it--such as hazard pointers, read-copy-update and epoch-based reclamation--have proved very challenging for formal reasoning. In this paper, we show that different memory reclamation techniques actually rely on the same implicit synchronisation pattern, not clearly reflected in the code, but only in the form of assertions used to argue its correctness. The pattern is based on the key concept of a grace period, during which a thread can access certain shared memory cells without fear that they get deallocated. We propose a modular reasoning method, motivated by the pattern, that handles all three of the above memory reclamation techniques in a uniform way. By explicating their fundamental core, our method achieves clean and simple proofs, scaling even to realistic implementations of the algorithms without a significant increase in proof complexity. We formalise the method using a combination of separation logic and temporal logic and use it to verify example instantiations of the three approaches to memory reclamation.
Year
DOI
Venue
2013
10.1007/978-3-642-37036-6_15
ESOP
Keywords
Field
DocType
modular reasoning method,different memory reclamation technique,memory reclamation technique,memory reclamation,certain shared memory cell,concurrent memory reclamation algorithm,memory management,implicit synchronisation pattern,separation logic,formal reasoning,epoch-based reclamation
Separation logic,Programming language,Shared memory,Computer science,Critical section,Correctness,Algorithm,Theoretical computer science,Memory management,Hazard pointer,Proof complexity,Temporal logic
Conference
Volume
ISSN
Citations 
7792
0302-9743
17
PageRank 
References 
Authors
0.74
12
3
Name
Order
Citations
PageRank
Alexey Gotsman143928.62
Noam Rinetzky242130.69
Hongseok Yang32313115.85