Have you ever faced a situation where your device or software application did not work properly and caused your computer to hang, freeze, or even crash at the most inopportune of moments? Have you wondered why things don't just work, instead of causing you heartburn? Venkatesh-Prasad Ranganath, G. Ramalingam, and Kapil Vaswani, researchers in the Rigorous Software Engineering group at Microsoft Research India, are trying to solve the problem of applications and devices interacting undesirably with the operating system.
"Today, building software and applications is akin to building a car. There are many parts built by different companies that go into the car, and all of these have to work together properly for the car to run," says Ranganath while explaining Tark, a project focusing on software-incompatibility issues. "Specifically, the car manufacturer and various part vendors have to agree on how their parts will interact and affect only these interactions; failing to do so by making unjustified assumptions based on observations can cause unforeseen failures in a car and inconvenience to the end user."
Given the number of devices and software from different vendors used in a computer, software development faces a similar challenge.
"Today's pace of technology evolution makes software compatibility an even more important and challenging problem," says Ramalingam. "Anyone developing a new or updated part must ensure that it works correctly with older systems as well as future systems. It thus becomes critical to have 'contracts' between different parts of the software that govern the behavior of those parts."
Ramalingam draws an analogy with traffic rules to explain what he means by a 'contract': Traffic typically flows smoothly when everyone follows the traffic rules. But if even one person violates a single traffic rule, it can lead to a cascading series of events that result in chaos or serious accidents. Similarly, products built from many parts might stop functioning because one part somewhere in the product violates a rule.
"A large fraction of computer crashes," Ranganath says, "are caused by third-party device drivers that do not adhere to the required protocol, underlining the importance of defining these 'contracts.' "
Current software development suffers from two related problems.
- First, contracts and rules tend to be stated informally in documentation.
- Second, there is no formal, comprehensive verification that software components satisfy the appropriate rules.
Over the last decade, the research community has made significant advances in software-verification technology. Software-verification tools can check whether a software component follows a given contract and can help identify potential incompatibility issues early on, when developers write code, rather than have these problems manifest themselves at a later stage, when users use the product.
"However, there is a catch to using software-verification tools," Ramalingam says. "The rules must be stated in a formal language that the tools understand. It is not enough to have documentation in English, as is the common practice today."
The team is building a tool to infer rules that govern the interaction of applications with the Windows operating system.
"The goal of Tark," Ramalingam says, "is to find these rules using data-mining techniques."
Tark mines rules that govern an application-programming interface (API). The technology is intended for use with APIs, such as the Windows API, for which many correct or mostly correct clients already exist. It first creates traces of events that occur when client applications access a particular type of resource and creates a database of such traces. It then looks for correlations and patterns among the events and extracts those with high statistical support and confidence as rules.
Tark is not error-free -- hence the name "Tark," which means "conjecture" or "guess" in Sanskrit -- because not all programs may interact in the correct manner.
"What we are doing may boil down to speculation, because it is statistical," Ranganath says. "We are trying to come up with what are likely rules, but there is no guarantee they will be true because they are based on observations. We expect human experts to look at the candidate rules inferred by our tool to validate or correct them.
"But we can assume that, by and large, most programs use any particular resource in a correct manner. There may be variations in how the programs work, but overall, certain patterns will emerge whenever the contract constrains the programs' behavior."
It is possible to mine rules in a static manner, by looking at the structure of the program and using it to approximate the behavior of the program, or in a dynamic manner, by registering events at run time.
Once the rules are expressed formally, they can be incorporated into diagnostic tools such as the Static Driver Verifier, which checks whether a program can violate any of the specified rules.
"Automatic verification tools," Ranganath says, "can identify scenarios where the program may fail to follow a rule."
Earlier, these rules had not been laid down formally, making it difficult to use such verification tools. But now, with the work of Ramalingam, Ranganath, and Vaswani, life for the programmer could become easier, and there might be fewer crashes and incompatibility issues for computer users.
