FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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:

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.

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