Work analysis with resource-aware session types

DOI10.1145/3209108.3209146zbMATH Open1497.68111arXiv1712.08310OpenAlexW2963595697MaRDI QIDQ5145303FDOQ5145303

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)

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.

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

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

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)

Cited In (10)

• Analysing parallel complexity of term rewriting
• Types and Effects for Resource Usage Analysis
• Nested session types
• A calculus for modeling floating authorizations
• Types for complexity of parallel computation in pi-calculus
• Two decades of automatic amortized resource analysis
• ElixirST: a session-based type system for elixir modules
• Title not available (Why is that?)
• Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination
• Session Types with Arithmetic Refinements

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)