{"id":307574,"date":"2007-09-12T17:00:59","date_gmt":"2007-09-13T00:00:59","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=307574"},"modified":"2016-10-18T22:28:19","modified_gmt":"2016-10-19T05:28:19","slug":"indian-team-applies-rigor-solving-software-challenges","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/indian-team-applies-rigor-solving-software-challenges\/","title":{"rendered":"Indian Team Applies Rigor to Solving Software Challenges"},"content":{"rendered":"

By Rob Knies, Managing Editor, Microsoft Research<\/em><\/p>\n

For Sriram Rajamani, the opportunity to work on improving software performance for Microsoft Research has been a productive, rewarding experience.<\/p>\n

And getting a chance to do so while stationed in his native India has been a rare privilege.<\/p>\n

Rajamani (opens in new tab)<\/span><\/a>, a senior researcher for Microsoft Research India (opens in new tab)<\/span><\/a> who heads the Rigorous Software Engineering (opens in new tab)<\/span><\/a> (RSE) group, has an extensive history of making the process of software development more robust, and his move from Microsoft Research Redmond (opens in new tab)<\/span><\/a> back to India two years ago provided a more faceted perspective on that effort.<\/p>\n

\u201cThe particular significance the group has in the Indian context is because a large portion of the Indian IT economy is about building software,\u201d he says. \u201cIndia as a country is exposed to much more of the software life cycle than anybody else, and that\u2019s a good test bed to study the whole cycle.\u201d<\/p>\n

At the same time, the RSE efforts can help lift computer-science research in the subcontinent to world-class levels.<\/p>\n

\u201cMost people in India don\u2019t have access to the research methods of the Western world,\u201d Rajamani says. \u201cThey don\u2019t have money to travel to conferences. They don\u2019t publish in world-class conferences. To use a metaphor, they never compete in the Olympics.<\/p>\n

\u201cBecause we are there, we give them a venue to compete in the world Olympics. People want to be the best that they can be. Our India lab gives Indian researchers an opportunity to compete in the Olympics, which they never had before.\u201d<\/p>\n

While based in Redmond, Rajamani managed the Software Productivity Tools team. He moved to Microsoft Research India, located in Bangalore, and instituted RSE in September 2005. The group is charged with bringing vigor and formality to software-engineering efforts.<\/p>\n

\u201cSoftware engineering is the process of building software, including things like design, coding, implementation, testing, and validation\u2014the whole shebang of building software,\u201d he says. \u201cThe goal of our group is to bring rigorous techniques that help the entire spectrum.\u201d<\/p>\n

Two years on, it appears that RSE has made significant traction.<\/p>\n

\u201cIt\u2019s going well,\u201d Rajamani says. \u201cWe have recruited good people. We have a few really good projects off the ground. Our papers are getting into good conferences. Technology coming out of our group is getting into Microsoft products.\u201d<\/p>\n

By external measures, too, the team is making its presence felt. In 2006, a paper entitled SYNERGY: A New Algorithm for Property Checking<\/em> (opens in new tab)<\/span><\/a>\u2014co-authored by Bhargav Gulavani of the Indian Institute of Technology [IIT], Bombay; Thomas Henzinger of Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne; and Microsoft Research India\u2019s Yamini Kannan, Aditya Nori (opens in new tab)<\/span><\/a>, and Rajamani\u2014was named the best paper of the fifth joint meeting of the European Software Engineering Conference and the Association of Computing Machinery\u2019s SIGSOFT Symposium on the Foundations of Software Engineering. This year, another RSE paper, Programming Asynchronous Layers with CLARITY<\/em>, was short-listed for the same award.<\/p>\n

Understanding Code<\/h2>\n

The SYNERGY paper represented work on one of the RSE team\u2019s three areas of focus: code understanding. The project from which the paper stemmed, called Yogi (opens in new tab)<\/span><\/a>, aims to build a scalable software-property checker by direct analysis of program binaries, using a new algorithm for property checking that combines software testing with verification.<\/p>\n

\u201cCode-understanding tools take code and try to give information to the programmer about problems,\u201d Rajamani explains, \u201cgetting an understanding about the root cause of an error in a simpler way. We want to make that process easier, to find bugs before they reach the customer.\u201d<\/p>\n

While in Redmond, Rajamani worked with colleague Tom Ball (opens in new tab)<\/span><\/a> on a project called SLAM (opens in new tab)<\/span><\/a>, which used static analysis to compare real code with a mathematical model to attempt to identify potential bugs. Yogi tries to take that effort a step further by using a couple of different techniques.<\/p>\n

\u201cSLAM is a static-analysis tool, which means that it never runs a program, it inspects a program and tries to understand it,\u201d Rajamani says. \u201cA lot of people have been building testing tools. Some of them run a program and observe what happens. Others use static analysis, which, without running the program, tries to construct a model of what the program should do and to analyze what it actually does.<\/p>\n

\u201cWith Yogi, we came up with a new algorithm that combines both of those things. Tools like SLAM, they\u2019ll find all bugs of a particular kind, but when they find a bug, you\u2019re not really sure if it\u2019s a true bug or not. When they find what appears to be an error, it\u2019s only a possible error. But they get good coverage.<\/p>\n

\u201cOn the other hand,\u201d he continues, \u201ctesting tools run the program for a few scenarios, and they define real bugs, but if you test the program for 10 days and you haven\u2019t found anything, you don\u2019t have a guarantee. Testing tries to hit the set of bugs in a program from below. Verification starts from above. We thought it was natural to combine both the projects, which is why we started Yogi. The idea has been very well received.\u201d<\/p>\n

Configuration Control<\/h2>\n

Another RSE focus is configuration analysis, examining the effect metadata\u2014such as access-control policies, registries, and deployment details\u2014on how programs perform.<\/p>\n

\u201cEvery file you own has permissions on who can read them, who can write them, who can execute them,\u201d Rajamani states. \u201cThere are many others in your computer. They\u2019re everywhere.<\/p>\n

\u201cHow does somebody know that they have set all these permissions correctly? That\u2019s an interesting question.\u201d<\/p>\n

To pursue answers, the RSE team developed Netra, a tool to identify potential configuration errors. The tool has been adopted by the Secure Windows Initiative (opens in new tab)<\/span><\/a>, and its effect is far-reaching.<\/p>\n

\u201cWhen Microsoft ships a product,\u201d Rajamani says, \u201cit first is run through a security audit: All the configurations, all the information they touch, all the files they create, all the DLLs they create \u2026 are they configured correctly? Netra is used to do that check.\u201d<\/p>\n

Clarity For Developers<\/h2>\n

The third RSE concern is with software design, an informal process that has lacked a mechanism to record design and architectural decisions that would enable them to be managed, along with code, as a project evolves. Enterprise applications, in particular, could benefit from such an approach, and, the RSE Web site declares, \u201cAllowing software engineers to operate at higher levels of abstraction will improve the productivity of the industry as a whole.\u201d<\/p>\n

\u201cIf you were to write code differently,\u201d Rajamani asks, \u201ccould you avoid a certain number of bugs from ever even happening? Design is about things that happen before coding even starts\u2014the methodology used to write the code: Was it the right one?\u201d<\/p>\n

The Clarity project, a new programming language developed by Rajamani in collaboration with Joseph Joy, development manager for Microsoft Research India, is designed to address such issues, many of which result from the challenges in writing operating-system code able to cope with a bombardment of asynchronous, concurrent requests.<\/p>\n

\u201cWe thought about a new way by which we can think about these things,\u201d Rajamani says, \u201cso that, from a programmer\u2019s perspective, [such a flood of concurrent requests] will look sequential.<\/p>\n

\u201cTypically, you do certain things, and then you might have to wait for somebody else to finish, and then you have to do certain things. When you wait for somebody else to finish, the context just goes away. You get a request, you want to do something, you wait for somebody else to finish, and then, when you resume, you have to reload your context, and that\u2019s a very hard thing to do.<\/p>\n

\u201cWe came up with a way that, when you wait for somebody else to finish, you can logically keep your state the same way. This simplifies the programmer\u2019s job.\u201d<\/p>\n

Smart People<\/h2>\n

As should be obvious, such work requires the talents of exceptional researchers, able to conceptualize the software-engineering process at a lofty level of abstraction, then transform their observations and hypotheses into tools that work in real life. When it comes to the RSE team, Rajamani extols the individuals\u2019 contributions with excited exuberance. A brief synopsis:<\/p>\n