PRL Seminars

Abstract

An event structure is an abstract model of an execution of a distributed system. It contains all the information usually represented in a "message sequence diagram" and from its primitives we may define Lamport's causal ordering of events. The Logic of Events is a constructive logic where the propositions are about event structures and the realizers of these propositions are abstract distributed programs, called distributed message automata. The definition of this logic in Nuprl is now fairly elegant -- there are six axioms for event structures and nine rules for realizing propositions. In the first part of the seminar, I will go over the logic and present a simple example of deriving a program from a specification. In the second part, I will discuss a newer result. We have defined a class of expressions, reminiscent of regular expressions, called ESP (event structure patterns), and given them a precise meaning as event structure propositions. Every ESP expression is realizable (this is the new resut) and so they form a new set of compoonents for building distributed systems.