Dynamic Checking of Safe Concurrent Memory Access using Shared Ownership

TL;DR

This paper introduces a formal shared ownership model for dynamically checking safe concurrent memory access, improving correctness verification in shared-memory programming.

Contribution

It presents a novel formal model and methodology for automatically detecting unsafe memory accesses in concurrent programs using shared ownership.

Findings

Model is proven free from data races

Effective in detecting unsafe accesses during simulation

Demonstrated on various synchronization mechanisms

Abstract

In shared-memory concurrent programming, shared resources can be protected using synchronization mechanisms such as monitors or channels. The connection between these mechanisms and the resources they protect is, however, only given implicitly; this makes it difficult both for programmers to apply the mechanisms correctly and for compilers to check that resources are properly protected. This paper presents a mechanism to automatically check that shared memory is accessed properly, using a methodology called shared ownership. In contrast to traditional ownership, shared ownership offers more flexibility by permitting multiple owners of a resource. On the basis of this methodology, we define an abstract model of resource access that provides operations to manage data dependencies, as well as sharing and transfer of access privileges. The model is rigorously defined using a formal semantics, and shown to be free from data races. This property can be used to detect unsafe memory accesses when simulating the model together with the execution of a program. The expressiveness and efficiency of the approach is demonstrated on a variety of programs using common synchronization mechanisms.