Name
Abstract | ||
|---|---|---|
A significant problem of lock-free concurrent data structures in an environment without garbage collection is to ensure safe memory reclamation of objects that are removed from the data structure. An elegant solution to this problem is Michael's hazard pointers method. The formal verification of concurrent algorithms with hazard pointers is yet challenging. This work presents a mechanized proof of the major correctness and progress aspects of a lock-free stack with hazard pointers. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-23283-1_16 | ICTAC |
Keywords | Field | DocType |
hazard pointers method,hazard pointer,elegant solution,lock-free concurrent data structure,significant problem,major correctness,data structure,concurrent algorithm,garbage collection,formal verification | Data structure,Programming language,Non-blocking algorithm,Computer science,Correctness,Hazard pointer,Concurrent algorithm,Garbage collection,Concurrent data structure,Formal verification | Conference |
Citations | PageRank | References |
11 | 0.59 | 11 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bogdan Tofan | 1 | 86 | 4.93 |
| Gerhard Schellhorn | 2 | 769 | 56.43 |
| Wolfgang Reif | 3 | 915 | 95.46 |