Specifying Weak Sets
Authors: Jeannette M. Wing and David Steere
Appears in Proceedings of the International Conference
on Distributed Computing Systems, June 1995.
The full text of this paper is here (in
PostScript).
Abstract
We present formal specifications of a new abstraction, weak
sets, which can be used to alleviate
high latencies when retrieving data from a wide-area information system like
the World Wide Web. In the presence of failures, concurrency, and
distribution, clients performing queries may observe behavior that is
inconsistent with the stringent semantic requirements of mathematical
sets. For example, an element retrieved and returned to the client
may be subsequently deleted before the query terminates. We chose to
specify formally the behavior of weak sets because we wanted to
understand the varying degrees of inconsistency clients might be
willing to tolerate and to understand the tradeoff between providing
strong consistency guarantees and implementing weak sets efficiently.
Our specification assertion language uses a novel construct that lets
us model reachability explicitly; with it, we can distinguish
between the existence of an object and its accessibility.
These specifications were instrumental in understanding the design space,
and we are currently implementing the most permissive of the
specifications in several types of Unix systems.