From Data Types to Session Types---A Basis for Concurrency and Distribution

We aim to solve computing's most pressing problem - concurrency and distribution - by adapting one of computing's most successful concepts - the data type. Data types codify the structure of data; session types codify the structure of communication. Session types will enable a revolution in the development of concurrent and distributed software, making it cheaper to construct and maintain, and more reliable.

Concurrency and distribution are computing's most pressing problem: unless we discover a way to routinely and reliably build concurrent and distributed systems, a half century of unprecedented technical progress will draw to a close. We are approaching the 50th anniversary of Moore's Law, the observation that component counts and clock speeds double every 18 months. No exponential improvement can continue forever, and recently this rule has changed: clock speeds now remain fixed while the number of processors doubles, so exploitation of concurrency is essential. Meanwhile, everyone now has a computer in their pocket, and these computers depend crucially on communication to achieve their function. We inhabit a world of web applications, cloud services, and mobile apps: society increasingly depends on a technological infrastructure of concurrent and distributed systems.

Programming concurrent and distributed systems is notoriously difficult. Many solutions are based on shared memory, which requires the programmer to reason about every possible interleaving by which many processors access a common resource. Shared memory scales only to a certain point; it is not appropriate for programming the server farms that drive the web or for mobile applications. The most successful solutions so far appear to be those that replace shared memory with communication as the central structuring technique. Communication usually centres around the notion of a protocol, a series of operations in a specific order. However, direct support for protocols at the language level has been lacking, as compared with data types.

The data type is one of computing's most successful concepts. Data types appear from the oldest programming language to the newest, and cover concepts ranging from a single byte to organised tables containing information on customers and orders. Types act as the fundamental unit of compositionality: the first thing a programmer writes or reads about each method is its data type, and type discipline guarantees that each call of a method matches its definition. Data types play a central role in all aspects of software, from architectural design to interactive development environments to efficient compilation.

The analogue of the data type for concurrency and distribution is the session type. A session type codifies the notion of a protocol. Session types build on data types, as data types specify the lowest level of data exchange, upon which more complex protocols are built. Just as type discipline matches use and definition of a method, so session types ensure consistency between the two ends of a communication.

We expect session types to play a role in all aspects of software. Today, architects discuss the high-level structure of a system in terms of its types, but must resort to informal notions of protocol to describe communication; in future, they will describe communication in terms of session types. Today, programmers use tools that let them search for methods and modules based on their type, and give immediate feedback if their program violates type discipline, but must resort to informal notions of protocol when coding communications; in future, they will search for components based on their session type, and get immediate feedback if their program violates session type discipline. Today, software tools exploit types to optimise code, but cannot exploit the informal notions of protocol to optimise communication; in future, communication middleware will exploit session types to support efficient messaging.

The programme is intended to establish a radically new programming methodology centring on session types, and design and build languages, tools and runtimes to enable their use by the standard software practice, as well as establishing theoretical foundations. This will have a far reaching impact on computing practice and on quality of software, in the short term (3 years), medium term (6 years) and long term (10 years and beyond).

(1) Who will benefit from this research?

In the short term, the beneficiaries will be the partners of this programme and those closely associated with them, including the web service and cloud computing platform from Amazon (Amazon Web Services, AWS), Qualit-E of Cognizant which provides defect analysis for large-scale enterprise software, large-scale E-Science infrastructure for ocean sciences and climate change (Ocean Observatories Initiative, OOI), Savara and other open-source projects in Red Hat, and VMware, a primary provider of cloud infrastructure. Each of them is a cutting edge engineering enterprise which centres on concurrency and distribution, and will directly benefit from our research accomplishments. This in turn will lead to a broader impact: for
example, AWS is one of the most widely used public web services with global user base, while OOI is a distributed observatory providing information from global oceans, which is vital for climate change.

In the medium term, our programming methodologies, languages and tools will become widely known outside of our partners, accompanying concrete usage scenarios. At this point, the ideas and tools will start to spread rapidly among aspiring engineers, including architects, analysts and programmers alike.

In the longer term, after the programme produces all of its key deliverables, their values will become appreciated among most software developers and all key personnel in IT divisions of cutting edge corporations. The time will be ripe for standardisation efforts for session-type-based technologies regarding e.g. quality assurance of components' behaviour and development process. These standardisations as well as the technologies themselves will have fundamental effects on all areas of computing and society, including citizens depending on ICT infrastructures for lifeline support.

(2) How will they benefit from this research?

The partners of this programme will benefit from their direct collaboration, and early access to the ideas, languages and tools, and will continue to be at the forefront of the software technologies exploiting the results of this collaboration.

For the adoption beyond our partners, the partners themselves will become one of the most effective channels. While new technologies in software often take time to become widely adopted, we believe that the urgency of working with concurrency and distribution will have an accelerating effect in the adoption of better and more powerful technologies. Once software developers start to use the session-type-based technologies from the programme, including programming languages and tools, developers and enterprises will quickly notice their benefits and will start to build development practice for their teams and organisations. This will also lead to the creation of a market for a new generation of software tools and methodologies.

In the long term, the effects will reach the public through two means. First, our provision of programming methods suited to concurrency and distribution will make it possible for new and versatile software products and services to appear and be used in public services. Second, improved safety and robustness of these software products will provide a higher quality of public service in the technological infrastructure that uses them.