id: 04149590
dt: j
an: 04149590
au: Wing, Jeannette M.
ti: Verifying atomic data types.
so: Int. J. Parallel Program. 18, No.5, 315-357 (1989).
py: 1989
pu: Springer, New York, NY
la: EN
cc: 
ut: program verification; fault-tolerance; abstract data types; Atomic
    transactions; distributed systems
ci: 
li: doi:10.1007/BF01379184
ab: Summary: 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++$.
rv: