Specifying Weak Sets
David C. Steere and Jeannette M. Wing
Abstract
We present formal specifcations 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 specifcations were instrumental in understanding
the design space, and we are currently implementing the most permissive
of the specifcations in several types of Unix systems.