Abstract={Separation logic has been successful at verifying that pro- grams do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.}
}
...
...
@@ -491,6 +493,8 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
Year={2011},
Month={October},
Pages={845--864},
url={http://doi.acm.org/10.1145/2048066.2048131},
doi={10.1145/2048066.2048131},
Abstract={Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is in- sufficient for reasoning about indexes that are accessed con- currently.
We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, how- ever, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and BLink trees. The complexity of these algorithms, in particular the BLink tree algorithm, can be completely hidden from the client?s view by our abstract specification.}
...
...
@@ -503,6 +507,8 @@ We present an abstract specification for concurrent indexes. We verify several r
Abstract={To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concur- rent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
Building on separation logic with concurrent abstract predicates (CAP), we introduce TaDA, a program logic which combines the benefits of abstract atomicity and abstract disjointness. We give several examples: an atomic lock module, a CAP example with a twist, which cannot be done using linearisability; an atomic MCAS module implemented using our lock module, a classic linearisability example which cannot be done us- ing CAP; and a double-ended queue module implemented using MCAS.}
...
...
@@ -515,6 +521,8 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
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.}
