Research

Main Project: Orc — Structured Concurrency

I'm in the research group of Prof. W. Cook and Prof. J. Misra, investigating "computational orchestration" — specifically the model of programming languages and distributed computing embodied by Orc.

Orc uses four "combinators" to express concurrency. (Surprisingly, the familiar fork–join construct is not one of them.) These four combinators form an simple but very expressive system for structuring concurrent work. Using Orc's combinators has been called "structured concurrent programming", drawing an analogy to structured programming's replacement of unmethodical use of goto and if statements with systematic control statements. [An interesting historical note: We do this work in Dijkstra's former office.]

One can think of a continuum of types of parallelism, from processor instruction-level parallelism at the fine-grained end, to loosely-coupled cross-organization human process concurrency at the course-grained end of the continuum. Orc addresses the needs at the middle-to-course part of the continuum, by providing language semantics for developers to easily use services such as wide-area distributed services (for example, Web services) and address the resulting reliability and timing concerns.

I contribute to the Orc project in two ways: 1) generally, helping further the overall Orc program of work, and 2) my specific problems.

My most significant "general" contribution so far is the Orc language plug-in for the Eclipse Integrated Development Environment. (Also available via EPIC, the Eclipse Plugin Central.)

Updating Executing Orc Programs

A specific problem that I am working on currently is updating running Orc programs. A large class of envisioned Orc applications are long-running processes, such as workflow procedures. These processes can be expensive to shut down to update the program. For example, if a workflow job representing an insurance claim has been in progress for weeks, it would be very undesirable to restart it because the claims handling rules have been updated. Migration of running instances from an old version to a new version of the program without restarting would prevent this. This work investigates a "safe" manner to transfer executing threads with minimal backtracking or other compensating actions. (This problem has also been called dynamic software updating, hot swapping, and online upgrading.)

Small Projects (term projects)

Currently in progress: Probabilistic Robot Control.

Draft Problem Statement: Robot behaviors are often designed using a set of states, with transition conditions among them, i.e. a finite state machine. The transition conditions often depend on uncertain inputs. Thus, transitions could fire incorrectly or fail to fire. This necessitates complicating the behavior design with additional transitions to "back out" of states judged to be erroneous.

Further, current robotic systems maintain probabilistic models of their environment. Deterministic state transitions are a mismatch for these models in that they require a single datum to be extracted from the probabilistic models to use as an input to the state transition decision. For example, when using a particle filter for the current robot pose, a single value is typically chosen to use as a basis for action decisions. In some sense, this "throws away" the advantages of tracking multiple hypotheses in the particle filter.

In this work, we seek to carry the probabilistic models into behavior decision making, insofar as it is possible. Clearly, a robot cannot choose to move to two different places at once, but not all decisions are mutually exclusive. For example, a robot could move its head to visually scan for objects while walking to a target location.

Currently in progress: Secure Information Flow Control in the Orc Concurrent Programming Language.

Draft Problem Statement: A secure information flow analysis of the Orc language, aimed at answering:

What are the various channels that information could flow among expressions in Orc (by design and covertly), under standard Orc semantics?

To what extent can an secure information flow policy be enforced in standard Orc with appropriate security extensions?

How does concurrency change the secure information flow problem or solution, if at all?

Can a policy be implemented reasonably that is more practical than strict noninterference?

Beyond the pure Orc semantic model, are there aspects of the implementation of the Orc compiler or runtime engine that affect the information flows?

Isolation of Untrusted Application Installers

(Isolation from the rest of the system, using the Alcatraz/Etrace work at Stony Brook University as a basis.)

Paper: Total Installation Awareness, with Robert Grant, Dec 2008. (PDF format, 602 kB)

Abstract: Users often install applications from untrusted sources. Alcatraz is a system that provides isolation of a system from potentially untrustworthy user programs. However, we find performance and functionality concerns with Alcatraz. Nevertheless, Alcatraz demonstrates the feasibility of one-way isolation of user programs. During a port of Alcatraz to a modern commodity operating system, Mac OS X, we observe that the various security goals present in such a system can be at odds with each other. This conflict impedes implementation of features such as isolation. We propose an alternative that preserves system adaptability properties while still serving the trusted platform needs of DRM. A substantially different approach to implementing one-way isolation appears feasible, and is left for future work.

Some Other Interests

I love many areas of computer science, but I've got two areas that are at the forefront of my interests at the moment:

Providing system facilities (either OS APIs or programming language features) for parallelism (fine-grained or cluster) that are natural/easy for developers and powerful/general for many irregular problems. This question lies somewhere between the programming languages and operating systems areas of CS.
Augmenting human's ability to reason logically with automated support for non-mathematical problems. We have reasonably powerful techniques to prove logical and mathematical assertions. How can we take some of this rigor and apply it to broader classes of questions? This problem crosses between a number of CS areas, including formal methods, knowledge representation, and HCI.

Other Views on Research

R. Hamming's Bellcore talk "You & Your Research" [700 kB PDF].