Work analysis with resource-aware session types

DOI10.1145/3209108.3209146MaRDI QIDQ5145303zbMATHOpenAlexFDO

Authors Ankush Das, Jan Hoffmann, Frank Pfenning

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1712.08310

zbMATH Keywords

resource analysissession typestype systems

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Resource Usage Analysis for the Pi-Calculus
• Verification, Model Checking, and Abstract Interpretation
• Type-based amortized resource analysis with integers and arrays
• Type-based amortized resource analysis with integers and arrays
• Automatic Static Cost Analysis for Parallel Programs

Cited in

(9)

• Types for complexity of parallel computation in pi-calculus
• Two decades of automatic amortized resource analysis
• Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination
• Session Types with Arithmetic Refinements
• Analysing parallel complexity of term rewriting
• Types and Effects for Resource Usage Analysis
• scientific article; zbMATH DE number 7471698 (Why is no real title available?)
• A calculus for modeling floating authorizations
• Nested session types

This page was built for publication: Work analysis with resource-aware session types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145303)