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