Pointer Race Freedom

TL;DR

This paper introduces a new concept of pointer race in concurrent programs, showing how verifying pointer race freedom under garbage collection can ensure safety in explicit memory management, with practical optimizations demonstrated.

Contribution

It defines pointer race freedom, proves its verification under garbage-collected semantics, and applies these results to optimize thread-modular analysis for explicit memory management.

Findings

Verification of pointer race freedom is sound under garbage collection.

Pointer race freedom verification can be performed under garbage-collected semantics.

Practical optimization yields up to two orders of magnitude speed-up.

Abstract

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 accessor's 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.