Spatial Logics for Distributed Systems

Wide-area distributed systems require new paradigms for computation and interaction. For example, such systems must be based on the asynchronous interaction of autonomous and loosely-connected entities, as opposed to the familiar synchronous interaction of closely-coupled objects. This is now very well understood: new computing paradigms are actively being developed, both practically and theoretically. Autonomy, security, and privacy, are now major concerns, in addition to the traditional concerns of correctness and efficiency. Type safety, until very recently an academic luxury, has now become a staple of the security of distributed systems. Concurrency can no longer be ignored or hidden in dark corners. Various kinds of novel program analyses are being actively investigated.

Even program logics (another academic luxury) may now find new and critical uses. Wide-area distribution implies that interfaces must be established to unprecedented degrees, and autonomy implies that such interfaces must be specified and agreed to by untrusting partners. In the same way that interaction primitives are changing, we believe that program logics must change too. Distribution means that it is important to know where things are happening. Security means it is important to know where things are kept. Privacy means it is important to know where things are known. Therefore, we must be able to discuss the where of a logical property, in contrast (or in addition to) the when of temporal logics, the how of intuitionistic logics, and the whether of classical logics.

We call "spatial logic" a logic where a property can describes a spatial component of a larger system. This idea may be quite general and applied in various ways. As a start, we have concretely investigated spatial logics for specific calculi of distributed systems. The spatial aspect is most obvious for calculi that have built-in notions of locations where processes reside. But, in retrospect, the idea can be usefully applied also to familiar calculi of concurrency (in fact, it is necessary to do so, before considering fancier calculi). For example, the hiding operator of pi-calculus can be seen as restricting the location of a name (e.g. for privacy), and therefore has a spatial aspect that can be exploited by appropriate logical operators. More strikingly, the familiar parallel composition operator has an obvious flavor of spatial separation that can be exploited by logical operators that had so far been largely overlooked.

In this lecture we discuss the new view of computing arising from wide-area distributed systems, and the implications that have eventually led us to consider new logical properties. We hope that our point of view will be helpful in developing new forms of analysis and new tools for taming the needs of wide-area distributed computing.

(Reflecting work with Andy Gordon, Microsoft Research Cambridge, and Luis Caires, FCT/UNL Lisbon)