Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)
Venue
Mathematical Foundations of Programming Semantics (MFPS) 2015
Publication date
Jun 2015
Identifiers
Authors
- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
Abstract
The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.