Programming distributed systems is already very challenging due to the presence of data races and deadlocks; bugs are difficult to detect and reproduce when they only arise in certain thread interleavings. The rise of modern distributed systems have introduced unique domain-specific challenges further complicating software development. Although program analysis tools exist for distributed systems, the most popular and usable tools are still centered around traditional programming languages. With the pervasive usage of distributed systems in software design, there is an urgent need for formal tools to help with the design, verification, and quantitative analysis of distributed software.

In response, this thesis designs novel resource-aware session types that serve as a sound and practical foundation for distributed systems with strong type-theoretic guarantees. Session types statically prescribe and enforce biirectional communication protocols for message-passing processes. However, they cannot express quantitative properties of a distributed system, such as energy consumption, latency, response time, and throughput. This thesis addresses this limitation by designing two extensions to express the work and span of parallel computation. To compute work, the key innovation was that messages and processes both carry an abstract notion of potential which is consumed to perform work. To compute span, the key innovation was to introduce operators from temporal logic to capture the timing of message exchanges. Resource-aware session types combine session types with work and span extensions allowing programmers to reason aboutboth qualitative and quantitative aspects of distributed systems.

The thesis further applies resource-aware session types to the blockchain domain. Blockchains allow execution of complex protocols between mutually distrusting parties through smart contracts. Programming smart contracts comes with unique challenges such as enforcing transaction protocols, computing their execution cost, and ensuring that assets are not accidentally duplicated or discarded. This thesis presents Nomos: a language for smart contracts based on resource-aware session types. Session types statically express contract protocols. Resource-aware types automatically infer the execution cost of transactions leveraging ideas from automatic amortized resource analysis. The built-in linear type system of session types provides a natural representation for assets ensuring that they are preserved across transactions. The Nomos type checker statically enforces the above requirements: protocols are enforced at runtime, bounds inferred are sound and precise, and assets used are neither duplicated nor discarded. Nomos also significantly develops the theory of programming languages: integrating session types with functional programming, linear-time type checking to prevent denial-of-service attacks, and an acquire-release discipline to rule out re-entrancy attacks. The thesis concludes with two complementary future directions: enhancing Nomos with refinement types for lightweight verification of smart contracts, and applying Nomos to other distributed domains e.g. cryptographic protocols.

152 pages

Thesis Committee:
Jan Hoffmann (Chair)
Frank Pfenning
Bryan Parno
Andrew Miller (University of Illinois Urbana-Champaign)
Shaz Qadeer (Facebook)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu