David Harel (Weizmann Institute)
A Grand Challenge: Towards Full Reactive Modeling of a Multi-Cellular Animal
Sriram K. Rajamani (Microsoft Research)
Zing: Exploiting Program Structure for Model Checking Concurrent Software
Authors: Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof and
Model checking is a technique for finding bugs in systems by
systematically exploring their state spaces. We wish to extract sound
models from concurrent programs automatically and check the behaviors of
these models systematically. The ZING project is an effort to build a
flexible infrastructure to represent and model check abstractions of
large concurrent software.
To support automatic extraction of models from programs written in
common programming languages, ZING's modeling language supports three
facilities present in modern programming languages: (1) procedure calls
with a call-stack, (2) objects with dynamic allocation, and (3)
processes with dynamic creation, using both shared memory and message
passing for communication.
We believe that these three facilities capture the essence of model
checking modern concurrent software.
Building a scalable model-checker for such an expressive modeling
language is a huge challenge. ZING's modular architecture provides a
clear separation between the expressive semantics of the modeling
language, and a simple view of ZING programs as labeled transition
systems. This separation has allowed us to decouple the design of
efficient model checking algorithms from the complexity of supporting
rich constructs in the modeling language.
ZING's model checking algorithms have been designed to exploit existing
structural abstractions in concurrent programs such as processes and
procedure calls. We present two such novel techniques in the paper: (1)
compositional checking of ZING models for message-passing programs using
a conformance theory inspired by work in the process algebra community,
and (2) a new summarization algorithm, which enables ZING to reuse work
at procedure boundaries by extending interprocedural data-flow analysis
algorithms from the compiler community to analyze concurrent programs.
Steve Brookes (Carnegie-Mellon)
Peter O'Hearn (Queen Mary University of London)
Resources, Concurrency and Local Reasoning
Resource has always been a central concern in concurrent programming.
Often, a number of processes share access to system resources such as
memory, processor time, or network bandwidth, and
correct resource usage is essential for the overall working of a system.
In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked
the problem of resource control in their basic works on concurrent programming. In addition
to the use of synchronization mechanisms to provide protection from inconsistent
use, they stressed the importance of resource separation as a means
of controlling the complexity of process interactions and reducing the
possibility of time-dependent errors.
The intervening years have seen the development of resource-oriented logics such as linear logic and BI. This
work uses one such logic, separation logic (a species of BI), to revisit the problem of reasoning about resources in
imperative concurrent programs. We use the separating conjunction connective to partition the portions of state used by different processes. The resulting proof method is modular, in the sense that assertions make local remarks about the
resources used by program components, instead of global remarks about the entire system state.
The first part of the tutorial, by O'Hearn, describes the basic ideas, and illustrates it with programs that
transfer ownership of portions of state between processes. Examples include resource pools, efficient message
passing, and semaphores programs (where a semaphore is dynamically ``attached'' to a portion of state that it owns).
The second part of the tutorial, by Brookes, provides a foundation for the method using a denotational model. In addition to soundness, the model shows that any program that gets past the proof rules does not have a race condition, where different processes attempt to access the same portion of state without explicit synchronization.
Bengt Jonsson (Uppsala)
Regular Model Checking
Regular model checking is being developed for algorithmic verification
of several classes of infinite-state systems whose
configurations can be modeled as words over a finite alphabet.
parameterized systems consisting of an arbitrary number
of homogeneous finite-state processes connected in a linear or ring-formed
systems that operate on queues, stacks, integers,
and other linear data structures.
The main idea is to use
regular languages as the representation of sets of
finite-state transducers to describe transition relations.
In general, the verification problems considered are all undecidable, so
the work has consisted in developing semi-algorithms, and decidability
results for restricted cases.
This tutorial explains some of the work that has been performed so far,
some of its applications, and gives comparisons with other
frameworks for analyzing parameterized structures, such as shape analysis