Verifying atomic data types |
| |
Authors: | Jeannette M Wing |
| |
Affiliation: | (1) School of Computer Science, Carnegie Mellon University, 15213-3890 Pittsburgh, Pennsylvania |
| |
Abstract: | Atomic transactions are a widely-accepted technique for organizing computation in fault-tolerant distributed systems. In most languages and systems based on transactions, atomicity is implemented through atomic objects, typed data objects that provide their own synchronization and recovery. Hence, atomicity is the key correctness condition required of a data type implementation. This paper presents a technique for verifying the correctness of implementations of atomic data types. The significant aspect of this technique is the extension of Hoare's abstraction function to map to a set of sequences of abstract operations, not just to a single abstract value. We give an example of a proof for an atomic queue implemented in the programming language Avalon/C++. |
| |
Keywords: | Atomicity program verification fault-tolerance transactions distributed systems abstract data types |
本文献已被 SpringerLink 等数据库收录! |
|