Publication Details
Pointer Race Freedom
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Meyer Roland (UNIKL)
Wolf Sebastian (UNIKL)
pointer race
pointer race freedom
garbage collecting semantics
memory managed semantics
thread modular reasoning
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessors control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of up to two orders of magnitude.
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessors control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of up to two orders of magnitude.
@INPROCEEDINGS{FITPUB11065, author = "Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k and Roland Meyer and Sebastian Wolf", title = "Pointer Race Freedom", pages = "393--412", booktitle = "Verification, Model Checking, and Abstract Interpretation (VMCAI)", series = "Lecture Notes in Computer Science", volume = 9583, year = 2016, location = "Berlin, DE", publisher = "Springer Verlag", ISBN = "978-3-662-49121-8", doi = "10.1007/978-3-662-49122-5\_19", language = "english", url = "https://www.fit.vut.cz/research/publication/11065" }