Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)
Venue
Electr. Notes Theor. Comput. Sci., vol. 319, pp. 3–18
Publication Year
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.