Behavioral Contracts for Concurrent and Message-Passing Programs

Welcome to the home page of the Behave! project, a research effort within the Software Productivity Tools Research group at Microsoft Research, on checking behavioral properties of concurrent, message-passing programs. This page contains information about:

 

Background and approach

Concurrent, asynchronous, message-passing programming is becoming increasingly important. However, such programs are notoriously hard to design and test. The goal of the Behave!  project is to build tools for checking behavioral properties (like deadlock freedom, invariant checking, message understood properties) of  asynchronous message-passing programs. We want to do this by directly analyzing source code written in an asynchronous programming language.

In hardware and protocol design, behavioral properties are checked by manually constructing models of the system as communicating finite state machines, and using a model checker to algorithmically explore the state space of the model. Three main issues arise when applying model checking to distributed message-passing software:

  1. Expressiveness. Unlike hardware, message-passing software tends to be more difficult to model as communicating state machines. The difficulty stems from typical, dynamic high-level programming features, including procedural abstraction (stack), dynamically created memory references (heap), references and communication channels that are sent as messages.
  2. State explosion. State explosion is a major limitation, and severely limits the size of models that can be checked automatically. Abstraction (throwing away irrelevant information about the system and simplifying it) and composition (dividing the model checking problem into parts) are the only ways to deal with state explosion on large programs
  3. Specification. Both abstraction and composition require user assistance in the form of specifications. User input needs to be integrated with the source code tightly. Otherwise, there is no way way to check for consistency between user input and source code, and maintain this consistency as the source code evolves.

Our general approach is to use a behavioral type system, both for specifying properties and for directing the extraction of models from the source code. Using behavioral type specifications, or contracts, model checking is performed compositionally. In the most general form, types are CCS processes, and subtyping is a simulation relation on CCS processes, as exemplified in our behavioral type theory for the Pi-calculus.

  • Special focus has been on checking that message-passing programs are stuck-free. Stuck-freedom formalizes the property that a communicating system cannot deadlock waiting for messages that are never sent or send messages that are never received. In our application, programmers write contracts, which are interfaces that specify the externally visible message-passing behavior of the program. Stuck-freedom is ensured by checking that an implementation conforms to its contract using a model checker. If you think of a contract as a behavioral type, you can think of stuck-freedom as the associated notion of type safety. We have developed a theory of stuck-free conformance for CCS processes. We have implemented a conformance checker in the software model checker Zing, and we have applied it in model checking distributed programs.
  • Powered by model checking: we rely on research and technology from the Zing project at MSR, which develops a state-of-the-art-and-beyond concurrent software model checker.

    • People

    The people involved in the Behave! project are:

  • Jim Larus    (Microsoft Research, Software Productivity Tools Group)
  • Sriram Rajamani    (Microsoft Research, Software Productivity Tools Group)                                  
  • Jakob Rehof    (Microsoft Research, Software Productivity Tools Group)
    •

    Papers  

    Links to papers and technical reports from the Behave! project:

    Copyright notice:
    These papers have been accepted for publication, and the copyright of each paper has been transferred to the publisher of the conference/journal in which that paper will appear. Copyright is retained by the publisher, notwithstanding that these works are offered here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each publisher's copyright, as stated in the copyright notice on each preprint. In particular, these works may not be further duplicated or reposted without the explicit permission of the copyright holder.

           Sriram K. Rajamani and Jakob Rehof
           Proceedings CAV 02, International Conference on Computer Aided Verification
           Abstract

     

    Talks

    Talks related to the Behave! project:

     

     homepage