Abstract Disjointness and Abstract Atomicity

Abstract. We look at approaches to specifying concurrent program modules based on disjointness (the abstraction that concurrent oper-ations act on disjoint resources) and atomicity (the abstraction that con-current operations occur at disjoint times). We illustrate the limitations of these approaches, and propose a novel approach, using atomic triples, that overcomes them. The specification and verification of concurrent program modules is a dif-ficult problem. When concurrent threads work with shared data, the resulting behaviour can be complex. Two abstractions provide useful simplifications: that operations effectively act at distinct times; and that operations effectively act on disjoint resources. Programmers work with sophisticated combinations of time and data abstractions. In contrast, existing reasoning techniques tend to be lim-ited to one or other abstraction. Consider the following implementation of a concurrent counter:3 function read(x) { r: = [x]; return r; function incr(x) { do { r: = [x]; b: = CAS(x, r, r + 1);} while (b = 0); function wkincr(x) { r: = [x]; [x]: = r + 1; The implementation provides an operation, read, that returns the current value of the counter, and two operations, incr and wkincr, that increment the value of the counter. The difference between incr and wkincr is that wkincr may not behave correctly if another thread is concurrently incrementing the counter (but is potentially faster otherwise4). 3 We assume that memory read, write and compare-and-swap (CAS) operations are atomic. 4 In a quick and dirty experiment, wkincr was around 60 % faster. 2 Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner Sequential Specification. How do we specify such a counter? A good start would be to give a sequential specification using Hoare triples, such as:{ C(x, n