Thread-Modular Reasoning for Heap-Manipulating Programs: Exploiting Pointer Race Freedom
Correctness of software artefacts has become a major requirement in software development processes for all sorts of systems. For parallel programs, however, testing becomes insufficient as it cannot observer all possible interleavings of threads. Hence, we employ model checking to automatically explore all behaviours of a concurrent system and thus allow proving its correctness. Today, a core problem of model checking efforts is the dynamically evolving heap in presence of low-level memory operations that stem from explicit memory management as known from C. Most approaches presently employ thread-modularity to handle an unbounded number of threads. The scalability of this methodology, however, suffers severely in the presence of explicit memory management. To overcome this limitation, a novel approach has been proposed which introduces a concept of ownership for explicitly managed memory if certain kinds of programming bugs, so-called pointer races, are absent. In the present thesis we extend an existing thread-modular analysis for concurrent data structures to integrate the novel notion of pointer race free programs. We show that relying on those programs is reasonable in the sense that even performance-critical non-blocking algorithms can be handled. Moreover, we substantiate the usefulness of this novel notion by providing experimental evidence for a speed-up of two orders of magnitude compared to classical thread-modular reasoning for explicit memory management.