Welcome to Fluid
Building a Programmer-Oriented Approach to Software Assurance and Evolution
If you're looking for
, click
here
Information about our project is below, but here are some quick links:
- The Fluid team
- The Fluid publications
- An Introduction to declaring design intent in Fluid for lock-based concurrency.
- A poster summarizing the project's objectives and prototype tool from OOPSLA '03
- A gallery of Fluid prototype tools (screenshots)
The Fluid Project is focused on creating practicable tools for programmers to assure and evolve real programs. We focus on "mechanical" program properties that tend to defy traditional testing and inspection regimes. These are properties with a non-local character, in that there may be no single place in the code where they are manifest, and they may involve non-determinism.
We have explored properties including:
- race conditions and locking policies,
- unique references and other programmer-significant aliasing properties,
- effects,
- appropriate typing,
- realtime threading policies, and
- single-threading policies.
These properties bear significantly on code safety, security, API compliance, and other attributes of dependability.
Composable static semantic program analyses are used to assure consistency of code and programmer expressed "low-level" models of design intent. Thus a failure to achieve assurance can indicate an error in the model, an error in the code, or an insufficiently precise analysis.
In order to facilitate experimentation, our prototype tool is presented as a seemingly benign plug-in in the widely adopted Eclipse IDE for Java. Case studies have identified numerous concurrency and other anomalies in production code drawn from a variety of sources, including government, industry, and open source.
We are guided in our design by a set of principles related to practicability. Specifically:
- Incrementality and early gratification. Any increment of effort we ask programmers to undertake should yield a generally immediate reward in the form of bug finding, assurance creation, guidance in evolution, or model expression.
- Familiar expression. Properties should be expressed tersely and using terminology already familiar to programmers.
- Cut points and composability. Components can be assured separately, and the assurances linked into chains of evidence.
The principle of incrementality suggests that partial chains are valuable in that they can assist in localizing attention when there are problems.
The Fluid Project team acknowledges primary support through the High Dependability Computing Program (HDCP) from NASA cooperative agreement NCC-2-1298. Work on the Fluid Tool has been funded entirely through NASA and previous contracts with DARPA and NSF. The team appreciates a grant from IBM Corporation specifically for work involving the Eclipse open source IDE. The team also appreciates support from Carnegie Mellon CyLab specifically for work on open source software quality and empirical work on case studies.