Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Anne Gardner · Electronic Notes in Theoretical Computer Science · 2015
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.