Download Research Tools
Collaboration can be a great catalyst for new ideas. Whether working with colleagues from down the hall or a team from another continent, we have found that working together strengthens our ideas. A prime example is the Barcelona Supercomputing Centre – Microsoft Research Centre in Barcelona, Spain. Microsoft Research Cambridge began collaborating with the Barcelona Supercomputing Center (BSC) in 2006. We formalized the relationship with the establishment of the BSC – Microsoft Research Centre in January 2008. The Centre focuses on the design and interaction of future microprocessors and software for the mobile and desktop market segments.
The BSC – Microsoft Research Centre is home to a talented group of students who are working towards their PhDs and who bring their creativity and enthusiasm to tackle tomorrow’s problems. “I am very happy that the Centre is a model of open research,” said Centre director Mateo Valero. “We share our findings with the community and all of our software and applications are available for download at our website.”
The program has an extremely young team with more than 15 PhD candidates, Valero explained. Leading the student group was Ferad Zyulkyarov, who is at the forefront of Transactional Memory (TM) research. Working under the supervision of Valero, and his colleagues Osman Unsal and Adrián Cristal, Zyulkyarov investigated how this new approach to multi-core programming could make software development much easier for future computer architectures.
Ferad Zyulkyarov defends his thesis in Barcelona
A Different Point of View
Previous TM research had focused on evaluating and improving TM implementations. Zyulkyarov took a unique approach to the problem, looking at it from the programmer’s point of view. As part of his thesis, Zyulkyarov developed one of the first real-world TM applications: a rewrite of the Quake Game Server that replaced traditional memory locks with TM atomic blocks. This makes life much easier for the programmer, potentially transforming multi-core software development for the future.
Zyulkyarov encountered some obstacles during his project. For example, he had to develop a better debugger and profiling support, neither of which existed before he created them. When he reviewed the performance of the core server code, Zyulkyarov could see the potential for TM. There is still some optimization work to be done, but the potential is there.
During the project, Zyulkyarov collaborated closely with Tim Harris, senior researcher, Systems and Networking Group, Microsoft Research Cambridge. Harris is proud of the work Zyulkyarov accomplished during their time together. “It’s great to see Ferad’s work come to fruition,” Harris said. “He’s made substantial contributions to the development of programming tools for using TM, and I hope that we’ll now be able to apply these ideas to other parts of the multi-core challenge.”
The First of Many PhDs from Barcelona
The first of the 15 students to receive his PhD, and now at Intel, Zyulkyarov is just one example of the young talent being fostered through the BSC – Microsoft Research Centre, driving the industry to tackle some of its most challenging problems. “In the five years since we have started, the Centre has matured quite a lot, and this is the first fruit of the collaboration with BSC and Microsoft Research,” Valero said, adding he is especially grateful to Harris for serving as Ferad’s mentor. “I know that more [success stories] will follow soon,” he added.
I am very glad—thinking back to my first visit to BSC five years ago—in seeing how far we came. This is the result of all the energy and enthusiasm we have all put together in the enterprise. This is only the first of a successful series of PhD awards, which we will see taking place in the next few years.
—Fabrizio Gagliardi, Director, Microsoft Research Connections EMEA (Europe, the Middle East, and Africa)
Each year, Microsoft Research awards competitive grants to computer science academics through the Software Engineering Innovation Foundation (SEIF). In the first grant round, conducted in 2010, Professor David Notkin and his colleagues at the University of Washington were the recipients of one of the 12 awards for their proposal, “Speculation and Continuous Validation for Software Development,” which resulted in the project, “Crystal: Precise and Unobtrusive Conflict Warnings.” I’m pleased to announce that the achievements of Notkin and his colleagues are being recognized this month with an ACM SIGSOFT Distinguished Paper Award. The award will be presented at the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE) in Szeged, Hungary (September 5–9, 2011). I’d like to share some of this exceptional research with you today.
(From left to right) Reid Holmes, David Notkin, Judith Bishop, Michael Ernst, Yuriy Brun
About the Crystal Project
Collaborative development of large software projects can be hampered when conflicts arise because developers have created inconsistent copies of a shared file, Notkin explains. The Crystal approach is designed to help developers identify and resolve inconsistencies early, before those conflicts become severe—and before relevant changes fade from the developers’ memories. The Crystal paper presents three outcomes of the project:
Notkin’s study spans nine open-source systems totaling 3.4 million lines of code. The conflict data is derived from 550,000 development versions of the system. The complete paper, which goes into great detail on all three points, plus other research that was conducted as part of the project, is available to read online.
The SEIF grants are just one way through which we continue to strengthen our support for outstanding university software engineering programs. These grants are intended to stimulate research in all aspects of software engineering, with an aim to cultivate interest in Microsoft Research tools and technologies. They also strengthen our ties to the university community.
In fact, one of the postgraduate students who worked on Notkin’s Crystal project, Kıvanç Muşlu, came to work for us as an intern. He was jointly mentored by Christian Bird and Tom Zimmermann of the Research in Software Engineering group (RiSE) and me. During his internship, Muşlu explored how Crystal’s principles could be expanded for use in a full industrial context. The testbed was the full Bing development history. The result of his work, a new tool called Beacon, will be deployed to Microsoft product groups in the near future. Like Crystal, Beacon can alert developers when code they are writing will conflict with changes to another branch of the code. By using Microsoft Lync, it can quickly put the developers of the two sections of code in touch so that they can resolve the conflict. The challenge was to make the system work in real time with the enormous number of files and developers involved in a system like Bing. We look forward to seeing more from Muşlu in the future.
—Judith Bishop, Director of Computer Science, Microsoft Research Connections
Building verifiably reliable and trustworthy software is one of the ultimate objectives of software engineering. With this goal in mind, academics, scientists, and researchers gathered in Shanghai, China, for the second Verified Software Workshop and Summer School. The event, which took place from August 23 to 31, 2012, attracted approximately 250 faculty and student attendees from more than 70 universities and research institutes and nearly a dozen countries across the Asia Pacific region and beyond.
World-class scientists and researchers—from Asia, Europe, and North America—provided the latest insights into verification theory, practice, and tools.
Co-sponsored by Microsoft Research Asia and East China Normal University, the event explored new directions and emerging opportunities in verified software research, with 21 keynote presentations by world-class scientists and researchers—from Asia, Europe, and North America—providing the latest insights into verification theory, practice, and tools. Especially notable among the prominent presenters were the workshop co-chairs: Professor Tony Hoare, the 1980 Turing Award winner and a principal researcher at Microsoft Research Cambridge, who gave the opening speech, titled, “Algebra Unifies Theories of Programming”; and Professor Jifeng He of East China Normal University and a member of the of the Chinese Academy of Sciences, who delivered a keynote on “A Clock-Based Framework for Modeling Hybrid Systems.”
The event began with a two-day workshop at East China Normal University that included inspiring lectures from technical and academic leaders. A broad and comprehensive workshop, it featured in-depth talks on such topics as detection of concurrency bugs, safe programming of asynchronous interaction, pervasive model checking, analysis and verification of multiple programs, automation of program verification, concurrent software verification, software analytics and its application, and modeling and verification of hybrid systems.
A five-day summer school of intense training followed the workshop. Students were treated to lectures focusing on the theoretical nature of concurrency and separation logic. One particular highlight was the hybrid systems session, which taught the KeYmaera logical analysis approach in a single day’s time. In addition, a step-by-step tool session provided attendees with valuable hands-on practice and an in-depth learning experience.
The event was popular with both students and presenters. Summing up the benefits of the event, one student said, “I acquired cutting-edge research and tools in [the] verification software field, and also had the opportunity to exchange my ideas with innovative peers and academic leads from across the world.”
Capturing the perspective of the experienced researcher, co-chair Tony Hoare praised the event and laid out his goals for such venues, saying, “We hope to expand the opportunities for industrial application of mature academic research, and to encourage the next generation of advanced researchers to continue the pursuit of deep and interesting questions in areas of the software industry.”
Professor Tony Hoare, the 1980 Turing Award winner and a principal researcher at Microsoft Research Cambridge, gave the opening speech, titled, “Algebra Unifies Theories of Programming."
Co-chair Jifeng He added, “We have achieved a lot in [the] verified software field with everyone’s great effort, but there is always more work to do. With this event, we hoped to not only inspire our young talent but also provide researchers and faculties worldwide with the advantage of exchanging ideas.”
Lolan Song, the senior director of Microsoft Research Asia, spoke of the company’s objectives in sponsoring such events, observing that “We hold this event in order to advance the state of the art in software and present a great opportunity for academics, researchers, and students in this area to share and exchange ideas. Also, we hope to identify and cultivate worldwide top talent in verified software areas and build up cadres of experienced users to support eventual use of the tools in the industry.” She also expressed the gratitude of Microsoft Research Asia for the assistance and participation of colleagues from Microsoft Research Cambridge, Microsoft Research Redmond, and Microsoft Research India.
—Kangping Liu, University Relations Manager, Microsoft Research Connections Asia