The Theory of Distributed Systems group uses the mathematical Input/Output Automaton model to describe and reason about distributed algorithms. This model supports description of systems as interacting state machines. The TDS group has developed the IOA language, a programming and modeling language based on the I/O Automaton model, and is currently developing a suite of tools for IOA.

Several of our projects can use programming help this summer and in the future.

General requirements:
All the project require strong skills in Java programming and discrete math and an interest in distributed algorithms and programming languages and compilers.

1. Constructing a user interface for the IOA automatic code generator

The IOA code generator compiles IOA programs into Java code that runs on a network of workstations. Programs running on different workstations communicate with each other and also receive input from the external environment. The goal of this project is to write a graphical tool that makes it easy for the user to generate input to the system. The form of the input is instances of Java classes that implement the IOA data types, which include integers, strings, sets, maps, and nestings thereof. The tool should make it easy for the user to create instances of arbitrary data types. For example, the tool might read in an IOA program to determine which types of values it uses, and then present the user with a palette for constructing those data types. Once there is an instance of a data type (e.g., a set of integers), the user should be able to view and manipulate it (e.g. add an integer to the set). Challenging problems include designing the interface so the user can easily visualize and manipulate arbitrary nestings of data types, making the tool extensible to support user-defined data types, and putting these two together so that users can add new data types without having to write a lot of Swing code.

Requirements:
Fluent in Java, software engineering, Swing. Interested in user interface design and visualization, programming languages and compilers, distributed algorithms.

Contact person: Josh Tauber, josh@theory.lcs.mit.edu

2. Testing and maintaining the basic IOA analysis tools: the IOA simulator and theorem-prover

The basic analysis tools for IOA consist of a simulator, which includes facilities for simulating system descriptions at multiple levels of abstraction, and a connection to an interactive theorem-prover. The simulator is instrumented to produce output for Prof. Ernst's Daikon invariant discovery tool. The basic toolset is currently being tested by application to many distributed algorithm examples. Such testing is uncovering the need for many enhancements and fixes to the system. This project involves assisting with testing the tools and implementing the needed improvements. Such improvements may include, for example, fixing bugs, adding new data type definitions, and identifying and automating strategies to support the construction of proofs.

Requirements:
Excellent at Java programming, software engineering, discrete math. Interested in distributed algorithms, logic, programming languages and compilers.

Contact persons: Steve Garland, garland@larch.lcs.mit.edu, Dilsun Kirli, dilsun@theory.lcs.mit.edu

3. Improving the IOA simulator

The IOA language allows highly nondeterministic system descriptions. The main challenge involved in simulating IOA programs is resolving the nondeterministic choices. This project involves improving the IOA simulator by adding support for resolving nondeterminism.

Nondeterminism in IOA comes in two flavors: Explicit choices from a set of options, and implicit scheduling decisions. We would like help from a student in (a) adding support for certain standard scheduling policies, such as random choice, round-robin, or timing-based, and (b) adding support for choosing an element from a set, e.g., by defining default elements of data types.

Requirements:
Excellent at Java programming, software engineering, discrete math. Interested in distributed algorithms, programming languages and compilers.

Contact person: Dilsun Kirli, dilsun@theory.lcs.mit.edu

4. Enhancing the IOA language with support for timing analysis

The current IOA language allows description of distributed algorithms without any timing-dependence. We are interested in extending the language with constructs to express timing behavior, including and upper and lower bounds on times for various events, and program constructs such as timeouts. Various IOA tools, in particular, the simulator and the theorem-prover connection, must also be extended to handle the new constructs.

Requirements:
Excellent at discrete math, Java programming, programming languages and compilers. Interested in distributed algorithms.

Contact person: Dilsun Kirli, dilsun@theory.lcs.mit.edu