Specifying Weak Sets

13 years 8 months ago

Download www.cs.cmu.edu

nt formal speci cations 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 willingto tolerate and to understand the tradeo between providing strong consistency guarantees and implementing weak sets e ciently. Our speci cation 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 speci cations were instrumentalin u...

Jeannette M. Wing, David C. Steere

Real-time Traffic