Work Analysis with Resource-Aware Session Types

Authors: Ankush Das, Jan Hoffmann and Frank Pfenning

Paper Information

Title:Work Analysis with Resource-Aware Session Types
Authors:Ankush Das, Jan Hoffmann and Frank Pfenning
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:concurrency and distributed computation, formal aspects of program analysis, linear logic, programming language semantics, type systems

ABSTRACT. While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this article presents an analysis for statically deriving worst-case bounds on the total work performed by message-passing processes. To decompose interacting processes into components that can be analyzed in isolation, the analysis is based on novel resource-aware session types, which describe protocols and resource contracts for inter-process communication. A key innovation is that both messages and processes carry potential to share and amortize cost while communicating. To symbolically express resource usage in a setting without static data structures and intrinsic sizes, resource contracts describe bounds that are functions of interactions between processes. Resource-aware session types combine standard binary session types and type-based amortized resource analysis in a linear type system. This type system is formulated for a core session-type calculus of the language SILL and proved sound with respect to a multiset-based operational cost semantics that tracks the total number of messages that are exchanged in a system. The effectiveness of the analysis is demonstrated by analyzing standard examples from amortized analysis and the literature on session types and by a comparative performance analysis of different concurrent programs implementing the same interface.

Talk:Jul 10 11:40 (Session 54E)