To order through AMS contact the AMS Customer Services Department, P.O. Box 6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard, Discover, and American Express orders call 1-800-321-4AMS.
You may also visit the AMS Bookstore and order directly from there. DIMACS does not distribute or sell these books.
Research in the last few decades on the connection between partial order semantics and interleaving semantics has resulted in a class of new verification techniques for distributed systems that are beginning to prove themselves to be of great practical value in routine industrial applications of formal verification techniques.
Much of the new work in this area is being pursued by people from quite distinct fields who rarely have an opportunity to meet and exchange ideas directly. These groups include, for instance, verification tool builders, logicians, semantic researchers, and process algebra specialists. The aim of the Workshop was to bring together researchers from these different disciplines.
The Workshop on Partial Order Methods in Verification, POMIV'96, was held during July 24-26, 1996, in the Computer Science Department of Princeton University, New Jersey
. The organizers invited twenty-five researchers representing different areas, including automata and formal languages, category theory, concurrency theory, logic, process algebra, program semantics, specification and verification, topology and trace theory. The Workshop focused on the following three main themes:
The talks in the Workshop focused on both the practical and the theoretical aspects of using partial order models.
This proceedings volume includes eighteen papers presented at POMIV'96. It also contains a lively e-mail debate, taking place between October 21 and November 19, 1990, via the concurrency mailing list, moderated at that time by Albert Meyer. It discusses the importance of the partial order dichotomy in modeling concurrency.
Some of the papers in this volume discuss partial order based semantic models such as event structures, pomsets, and traces. These permit expression of the causality relation between the events executed in a concurrent system. Their use allows the phenomena of concurrency and nondeterminism to be distinguished, an important distinction not drawn by interleaved semantics. Various specification formalisms allow the expression of properties based on partial order semantics, e.g., using classical and temporal logics, process algebras, or special automata.
The study of formalisms over partial orders has grown into an interesting research field of its own. Some of the papers presented in the conference focused on formal language research of trace theory, decision algorithms that are beneficial for automatic verification of concurrent programs, and a topological study of families of such languages and their connection with program specification. Such models were studied also with respect to automata theory, category theory and topology.
Various specification languages, such as classical logics (e.g., first and second order monadic logics), are used to express properties over partial order structures. Several papers also focused on new temporal logics designed for partial order models, aimed at specifying the behavior of concurrent programs. Other works study the issues of expressiveness and axiomatizability of such formalisms.
Automated verification tools based on automata theory and partial order reduction techniques are beginning to gain acceptance as effective tools for distributed system design. The success of partial order techniques in the domain of software verification may be compared to the success of BDDs (binary decision diagrams) in the domain of hardware verification. They are used to alleviate the state space explosion in automatically verifying concurrent programs. Unlike many other problem domains, any improvement in our understanding of this area can translate almost immediately into improvements of industrial practice.
Using partial order reduction techniques, it has become possible to analyze larger problem sizes, which did not lend themselves to automatic verification before. The simplicity of the principles behind these methods suggests that they can be integrated into any state-based automatic verification tool. Such practical methods have already been integrated into various model-checking tools, allowing more efficient checking of bigger systems. New results, reported in this volume, show how such methods can preserve specifications given in various formalisms, including linear and branching temporal logic properties and various process algebras.
The talks given in the Workshop included many new results and state-of-the-art techniques. We expect this volume to be an important resource on research done in the area of modeling, specifying, and verifying concurrent systems in general, and the theory of partial orders in formal methods in particular.
The Workshop included two social events: a reception, held in the Prospect Gardens building at Princeton University on July 23rd, and a Workshop dinner, held at the computer science building on July 25th. Pictures taken at the Workshop dinner can be found in the Internet Web page:
POMIV'96 was sponsored by the ONR (Office of Naval Research), AT&T, and Lucent Technologies. It was run under the Special Year on Logic and Algorithms (SYLA), organized by DIMACS-Center for Discrete Mathematics and Computer Science.
Local arrangements were made by Sandy Barbu of the Computer Science Department, Princeton University, Princeton, New Jersey.
The organizers would like to thank Sandy for her hard work in helping to arrange this event. We would like to thank the invited speakers, the participants, and the sponsors.
The Problem. Enhancing the reliability of concurrent systems is an increasingly important and challenging problem for information technology today. The problem is more serious than for sequential systems for two reasons. First, the possible interactions in a computer network are far more complex than for a traditional stand-alone sequential program. Second, one little bug may ruin the whole day not just of an individual computer user but an entire community, many of whom need not even be directly involved with computers.
With increasing system complexity, whether concurrent or sequential, come increasing costs of system failure. The widespread outage of the telephone system on the U.S. east coast in January 1991 dramatically testified to the expensive havoc that one tiny programming error could wreak, as did the $475 million Pentium chip division bug, and the recent $5 billion crash of the Ariane 5 rocket.
Expectations. It is unreasonable to expect to eliminate all errors, even catastrophic ones, but any improvements in software technology that will reduce their frequency and severity are well worth the effort. If each $ 1 00 million invested in enhanced system reliability avoided one billion-dollar catastrophe, the rate of return on this investment would be a thousand percent even without counting the savings from the many lesser bugs that would also have been avoided.
Given the magnitude of the software reliability problem, the software industry should not put all its eggs in one basket, but instead aggressively explore all reasonable alternatives.
The Verification Option. One alternative that has strong support from a large segment of the software engineering community is verification, the application of logic to the efficient search of the entire space of possible behaviors. No tool can hope for perfection, and logic is no exception. What logic accomplishes is not the infallibility popularly attributed to it, but rather the efficient search of combinatorially large or even infinite state spaces for all the known types of bugs in a practical amount of time. No methodology comes near the efficacy of logic in that role, particularly in the case of infinite search spaces where mathematical induction permits seeking out in finite time every nook and cranny that may hide a known type of bug.
One weakness of logic is that it cannot guarantee to recognize bugs of a kind not anticipated by the axioms of the logical system. For this and other reasons logic should be viewed as just one player on a team whose overall goal is improved reliability. Logic has proved a valuable player in this role on many documented occasions, fully justifying its continued support and growth.
Logic works best when understood as a discipline for manipulating not just symbols (proof theory) but also facts about some world (model theory). To the latter end one develops a mathematical model of that world, and evaluates the soundness of the proof system relative to that model. The model must be faithful to the world, yet simple enough to permit the soundness of the logic to be assessed.
What is concurrency? A burning problem in program verification today is how to model the world of concurrent systems. The excellent models of sequential behavior that have evolved during the past thirty years of sequential program verification do not adequately reflect the nature of a concurrent universe. Only when one imagines each and every event in the universe lining up to take its turn can one confidently apply any of the sequential models. A variety of "testing scenarios" reveals situations where sequential models yield a visibly wrong answer and hence an unsound logic. These scenarios have spurred interest in true concurrency as it has come to be called; namely, in modeling concurrency in a way that is faithful to all currently understood modes of interaction of system components, particularly those beyond the reach of sequential models.
Two concurrency models. There are two basic approaches to true concurrency: state based and event based. The state based approach as the standard model for sequential behavior has the advantage of familiarity. In this model, the passage from sequential to concurrent behavior is accompanied by an increase in structural complexity of the transition system. The basic additional structure required is a higher-dimensional filling in of the spaces between the "commuting squares" characteristic of the state diagrams of concurrent systems. While this structure is most simply realized directly by geometric means, a number of more or less equivalent ways of achieving essentially the same effects have been proposed by the concurrency community in the past decade or so.
The event-based approach models behavior in terms of occurrence of events. A system, or any of its components, is modeled as the set of all events the system is capable of performing, usually infinite in practice. Pure concurrency, with no synchronous behavior, interference, or other interaction, is simply the set of events itself with no additional structure. The many ways in which system components can interact, whether cooperating synchronously (communication), competing for shared resources that forbid simultaneous access (mutual exclusion), or inhibiting one another's occurrence altogether (conflict), are modeled by equipping the event set with structure consisting of constraints formally expressing those interactions. Note the change in direction here: with states structure increases with increasing independence while with events it increases with increasing interaction, the opposite of independence.
Just as physics needs both waves and particles to model the physical universe, so does computer science need both state-based and event-based models of true concurrency.
Partial Orders. The focus of this Workshop is on the concurrent structures supporting the event-based approach, the basic such structure being the partial order. Total order semantics views each execution of a concurrent system as a sequence of events, where actions executed concurrently appear according to some arbitrary order. Partial order semantics allows events to appear either ordered or unordered, disallowing causality cycles, e.g., action A happens before action B, which happens before action C, which happens before A.
Total order semantics, also called interleaving semantics, is traditionally considered easier to work with as it lends itself to simple representations, e.g., with finite state machines. Until recently partial order semantics had not been widely applied in practical verification due to a lack of maturity in the methodology of its use and a shortage of suitable tools for verification based on partial orders.
Continuing research into partial order semantics has improved this situation in recent years, and the partial order approach can now reasonably be looked to as a viable extension of total order semantics. Since total orders are a special case of partial orders, the move to the latter has freed verification system builders to employ new methods without having to abandon those sequential methods that have proved useful in concurrent verification. These new methods are now starting to show worthwhile efficiency gains in the exploration of state spaces.
Doron Peled, Vaughan Pratt, Gerard Holzmann
Murray Hill, NJ and Palo
Alto, CA.
Foreword ix Preface xi Prefix function view of states and events ANTONI MAZURKIEWICZ 1 Elements of an automata theory over partial orders WOLFGANG THOMAS 25 Algebraic manipulations and vector languages M. W. SHIELDS 41 Refinement with global equivalence proofs in temporal logic SHMUEL KATZ 59 A complete axiomatization of a first-order temporal logic over trace systems WOJCIECH PENCZEK AND MARIAN SREBRNY 79 Interleaved progress, concurrent progress, and local progress W. REISIG 99 Teams can see pomsets GORDON PLOTKIN AND VAUGHAN PRATT 117 Presheaves as transition systems GLYNN WINSKEL AND MOGENs NIELSEN 129 On topological hierarchies of temporal properties CHRISTEL BAIER AND MARTA KWIATKOWSKA 141 Linear time temporal logics over Mazurkiewicz traces MADHAVAN MUKUND AND P. S. THIAGARAJAN 171 A solution of an interleaving decision problem by a partial order technique ALBERT R. MEYER AND ALEXANDER RABINOVICH 203 Stubborn set methods for process algebras ANTTI VALMARI 213 Paxtial order reduction: Linear and branching temporal logics and process algebras DORON PELED 233 History dependent verification for partial order systems UGO MONTANARI AND MARCO PISTORE 259 Transition systems with independence and multi-arcs THOMAS T. HILDEBRANDT AND VLADIMIRO SASSONE 273 On the costs and benefits of using partial-order methods for the verification of concurrent systems PATRICE GODEFROID 289 Partial order verification with PEP EIKE BEST 305 Rapide: A language and toolset for simulation of distributed systems by partial orderings of events DAVID C. LUCKHAM 329 Debate '90: An electronic discussion on true concurrency 359
Index of Volumes
DIMACS Homepage