About ACM Software System Award

Gernot Heiser, University of New South Wales; Gerwin Klein, Proofcraft; Harvey Tuch, Google; Kevin Elphinstone, University of New South Wales; June Andronick, Proofcraft; David Cock, ETH Zurich; Philip Derrin, Qualcomm; Dhammika Elkaduwe, University of Peradeniya; Kai Engelhardt; Toby Murray, University of Melbourne; Rafal Kolanski, Proofcraft; Michael Norrish, Australian National University; Thomas Sewell, University of Cambridge; and Simon Winwood, Galois, receive the ACM Software System Award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, mechanically-checked proof of full functional correctness.

In 2009, the Software System Awardees presented the seL4 microkernel, which became the first ever industrial-strength, general-purpose operating system with formally proved implementation correctness. In subsequent years, the team further added proofs that seL4 enforces the core security properties of integrity and confidentiality, extended the proof to the binary code of the kernel, and performed the first sound and complete worst-case execution-time analysis of a protected mode OS.

The seL4 high-assurance microkernel has fundamentally changed the research community’s perception of what formal methods can accomplish: it showed that not only is it possible to complete a formal proof of correctness and security for an industrial-strength operating system but that this can be accomplished without compromising performance or generality. The continuously maintained and growing proofs on seL4 have helped to give rise to a new discipline of proof engineering—the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.

Xavier Leroy, Collège de France; Sandrine Blazy, University of Rennes 1, IRISA; Zaynah Dargaye, Nomadic Labs; Jacques-Henri Jourdan, CNRS, Laboratoire Méthodes Formelles; Michael Schmidt, AbsInt Angewandte Informatik; Bernhard Schommer, Saarland University, and AbsInt Angewandte Informatik GmbH; and Jean-Baptiste Tristan, Boston College, receive the ACM Software System Award for the development of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness.

CompCert, initiated in 2005, is a compiler for the C programming language and the first industrial-strength compiler with a mechanically checked proof of correctness. It can be used with most computer architectures including PowerPC, ARM, RISC-V and x86 (32 and 64 bits) architectures.

When it was introduced, CompCert represented a major advance over other production compilers, because it did not experience miscompilation issues since it is formally verified using machine-assisted mathematical proofs. The code it produces is proved to behave exactly as specified by the semantics of the source C program. This level of confidence in the correctness of the compilation process enables CompCert to meet the highest levels of software assurance.

Today, CompCert continues as a research project at Inria, the French National Institute for Research in Digital Science and Technology and is available under commercial and noncommercial licenses (source code openly available for noncommercial use). Other researchers build on CompCert, and multiple corporations use it for safety-critical applications.

Margo Seltzer, University of British Columbia; Mike Olson, formerly of Cloudera; and Keith Bostic, MongoDB, receive the ACM Software System Award for Berkeley DB, which was an early exemplar of the NoSQL movement and pioneered the “dual-license” approach to software licensing.

Since 1991, Berkeley DB has been a pervasive force underlying the modern internet: it is a part of nearly every POSIX or POSIX-like system, as well as the GNU standard C library (glibc) and many higher-level scripting languages. Berkeley DB was the transactional key/value store for a range of first- and second-generation internet services, including account management, mail and identity servers, online trading platforms and many other software-as-a-service platforms.

As an open source package, Berkeley DB is an invaluable teaching tool, allowing students to see under the hood of a tool that they have grown familiar with by use. The code is clean, well structured, and well documented—it had to be, as it was meant to be consumed and used by an unlimited number of software developers.

As originally created by Seltzer, Olson and Bostic, Berkeley DB was distributed as part of the University of California’s Fourth Berkeley Software Distribution. Seltzer and Bostic subsequently founded Sleepycat Software in 1996 to continue development of Berkeley DB and provide commercial support. Olson joined in 1997, and for 10 years, Berkeley DB was the de facto data store for major web infrastructure. As the first production quality, commercial key/value store, it helped launched the NoSQL movement; as the engine behind Amazon’s Dynamo and the University of Michigan’s SLAPD server, Berkeley DB helped move non-relational databases into the public eye.

Sleepycat Software pioneered the “dual-license” model of software licensing: use and redistribution in Open Source applications was always free, and companies could choose a commercial license for support or to distribute Berkeley DB as part of proprietary packages. This model pointed the way for a number of other open source companies, and this innovation has been widely adopted in open source communities. The open source Berkeley DB release includes all the features of the complete commercial version, and developers building prototypes with open source releases suffer no delay when transitioning to a proprietary product that embeds Berkeley DB.

In summary, Berkeley DB has been one of the most useful, powerful, reliable, and long-lived software packages. The longevity of Berkeley DB’s contribution is particularly impressive in an industry with frequent software system turnover.

ACM named Paul Mockapetris recipient of the ACM Software System Award for development of the Domain Name System (DNS), which provides the worldwide distributed directory service that is an essential component of the functionality of the global internet.

When the internet was first deployed in the early 1980s, the online community relied on a centrally-managed directory that matched human-friendly host names to numerical IP addresses of computers on the network. As the internet began to grow more rapidly, maintaining a single centralized host directory became slow and unwieldy, necessitating a new scalable architecture. To address this need, in 1983, Mockapetris designed and built the Domain Name System (DNS), creating the associated query protocol, a server implementation, and initial root servers. Taken together, these components provided the first stable operational DNS system.

When Mockapetris initially designed the DNS, the number of name lookups to establish the associated IP address were in the few thousands per day. Today, while still employing the core components that Mockapetris introduced 37 years ago, the DNS manages 350 million separately-managed domains, and responds to several tens of billions of queries each day.

DNS serves as a foundation for dozens of other applications, including email and web addresses. The Universal Resource Locator (URL) and Universal Resource Identifier (URI)—core components the World Wide Web—rely on domain names as introduced in the DNS system. While many of the new features of the DNS have been added by others, the ability of Mockapetris’s original design to incorporate these updates is a testament to his work.

ACM named Gerald C. Combs recipient of the ACM Software System Award for for creating the Wireshark network protocol analyzer, an essential tool for nearly anyone who designs, deploys, analyzes and troubleshoots the wide range of network protocols that tie the internet together, and for continued leadership of the international Wireshark developer community.

Combs started Wireshark as an open source project in 1997 under the name Ethereal. The software quickly became the most commonly used system for visually analyzing network protocol traffic. Before the advent of Ethereal and Wireshark, protocol analyzers were expensive, dedicated pieces of hardware that were only available to large institutions. The creation of an open source network protocol analyzer democratized access to network protocol analysis. It also enabled people to learn about network protocols, as they were able to visualize the traffic on their own networks. In addition, Wireshark has also had significant influence on the areas of network engineering and cybersecurity. Engineers who work alongside security experts in financial institutions and other high-profile businesses make extensive use of Wireshark in their ongoing fight against cybercrime.

Combs, who serves as Director of Open Source Projects at Riverbed Technology, has continued to work on the Wireshark code. He spent 20 years guiding the open source community that has developed around the software and leading SharkFest, an annual educational conference focused on sharing knowledge, experience and best practices among the Wireshark developer and user communities.

The ACM Software System Award is presented to an institution or individual(s) recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. The Software System Award carries a prize of $35,000. Financial support for the Software System Award is provided by IBM.

ACM named Fernando Pérez, Brian E. Granger, Min Ragan-Kelley, Paul Ivanov, Thomas Kluyver, Jason Grout, Matthias Bussonnier, Damián Avila, Steven Silvester, Jonathan Frederic, Kyle Kelley, Jessica Hamrick, Carol Willing, Sylvain Corlay and Peter Parente (members of the Project Jupyter Steering Council), recipients of the ACM Software System Award for Project Jupyter, a broad collaboration that develops open source tools for interactive computing, with a language-agnostic design. These tools, which include IPython, the Jupyter Notebook and JupyterHub, have become a de facto standard for data analysis in research, education, journalism and industry. Jupyter has broad impact across domains and use cases. Today more than 2,000,000 Jupyter notebooks are on GitHub, each a distinct instance of a Jupyter application—covering a range of uses from technical documentation to course materials, books and academic publications.

Jupyter has also gained wide industry adoption. Since 2015, Jupyter-based products have been released by several companies including Google (Cloud DataLab), Microsoft (AzureML, HDInsight), Intel (Trusted Analytics Platform), and IBM (IBM Watson Studio). Bloomberg and Anaconda Inc. have partnered with Project Jupyter to develop the next-generation web interface, JupyterLab.

The ACM Software System Award is presented to an institution or individual(s) recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. The Software System Award carries a prize of $35,000. Financial support for the Software System Award is provided by IBM.

Mahadev Satyanarayanan, Michael L. Kazar, Robert N. Sidebotham, David A. Nichols, Michael J. West, John H. Howard, Alfred Z. Spector and Sherri M. Nichols were honored for developing the Andrew File System (AFS). AFS was the first distributed file system designed for tens of thousands of machines, and pioneered the use of scalable, secure and ubiquitous access to shared file data. To achieve the goal of providing a common shared file system used by large networks of people, AFS introduced novel approaches to caching, security, management and administration. AFS is still in use today as both an open source system and as the file system in commercial applications. It has also inspired several cloud-based storage applications.

The 2016 Software System Award recipients designed and built the Andrew File System in the 1980s while working as a team at the Information Technology Center (ITC), a partnership between Carnegie Mellon University and IBM. Many other universities soon integrated AFS before it was introduced as a commercial application. Many of this year’s recipients also contributed to two foundational AFS papers: The ITC Distributed File System: Principles and Design, published in Proceedings of ACM SOSP 1985 and Scale and Performance in a Distributed File System, published in Proceedings of ACM SOSP 1987.

The ACM Software System Award is presented to an institution or individual(s) recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. The Software System Award carries a prize of $35,000. Financial support for the Software System Award is provided by IBM.

ACM announced the recipients of four prestigious technical awards:  ACM Grace Murray Hopper Award, ACM Paris Kanellakis Theory and Practice Award, ACM-AAAI Allen Newell Award, and ACM Software System Award. These innovators were selected by their peers for making significant contributions that enable the computing field to solve real-world challenges. The awards reflect achievements in cryptography, network coding systems, computer-human interaction, and software systems. The 2015 recipients will be formally honored at the ACM Awards Banquet on June 11 in San Francisco.

Richard Stallman, recipient of the ACM Software System Award for the development and leadership of GCC (GNU Compiler Collection), which has enabled extensive software and hardware innovation, and has been a lynchpin of the free software movement. A compiler is a computer program that takes the source code of another program and translates it into machine code that a computer can run directly. GCC compiles code in various programming languages, including Ada, C, C++, Cobol, Java, and FORTRAN. It produces machine code for many kinds of computers, and can run on Unix and GNU/Linux systems as well as others.

GCC was developed for the GNU operating system, which includes thousands of programs from various projects, including applications, libraries, tools such as GCC, and even games. Most importantly, the GNU system is entirely free (libre) software, which means users are free to run all these programs, to study and change their source code, and to redistribute copies with or without changes. GNU is usually used with the kernel, Linux. Stallman has previously been recognized with ACM’s Grace Murray Hopper Award.

Mach, a pioneering operating system used as the basis for later operating systems, has won the 2014 ACM Software System Award. The lead developers, Rick Rashid and Avie Tevanian, created a system that advanced the state of operating systems and led to practical, widespread adoption. Mach-based operating systems are used by hundreds of millions of people 30 years after the project began. 

The Mach operating system, a DARPA-funded research project at Carnegie Mellon University conducted from 1983-1992, was based on innovative approaches to virtual memory management and microkernel architecture. Under the leadership of Rashid and Tevanian, Mach established a foundation for later operating systems on personal computers, tablets, and mobile phones. Rashid founded Microsoft Research in 1991, and is Vice President and Chief Technology Officer for Microsoft Applications and Services Group. Tevanian, formerly of Apple Inc., is Managing Director of Elevation Partners, a private equity firm.

Mach’s influence reflects both significant commercial acceptance and substantial contributions to the concept of operating systems. For example, Mach’s portability and performance attributes made it possible for Apple to rely extensively on it in their operating systems for their devices.

The Mach kernel forms the heart of the Apple iOS and OS X systems. Mach was at the core of NeXT’s operating system, which Apple acquired and subsequently used as the basis of OS X and iOS. Mach’s influence can also be traced to operating systems such as GNU Hurd, and UNIX systems OSF/1, Digital Unix, and Tru64 Unix.