Data flow analysis of asynchronous systems using infinite abstract domains

DOI10.1007/978-3-030-72019-3_2zbMATH Open1473.68110arXiv2101.10233OpenAlexW3141564970MaRDI QIDQ2233447FDOQ2233447

Authors: Snigdha Athaiya, Raghavan Komondoor, K. Narayan Kumar 

Publication date: 18 October 2021

Abstract: Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This paper addresses the problem of precise data flow analysis for such systems. To obtain good precision, data flow analysis needs to somehow skip execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at run time. Existing data flow analysis techniques do elide a subset of such infeasible paths, but have the restriction that they admit only finite abstract analysis domains. In this paper we propose a generalization of these approaches to admit infinite abstract analysis domains, as such domains are commonly used in practice to obtain high precision. We have implemented our approach, and have analyzed its performance on a set of 14 benchmarks. On these benchmarks our tool obtains significantly higher precision compared to a baseline approach that does not elide any infeasible paths and to another baseline that elides infeasible paths but admits only finite abstract domains.

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

Recommendations

• Interprocedural analysis of asynchronous programs
• Bounded phase analysis of message-passing programs
• Data flow analysis of distributed communicating processes
• Automated analysis of asynchronously communicating systems
• Efficient dataflow analysis of logic programs

zbMATH Keywords

message-passing systemsdata flow analysis

Mathematics Subject Classification ID

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

Cites Work

• The octagon abstract domain
• Parallel program schemata
• Title not available (Why is that?)
• The Complexity of the Finite Containment Problem for Petri Nets
• On Communicating Finite-State Machines
• Precise interprocedural analysis through linear algebra
• The covering and boundedness problems for vector addition systems
• Verifying programs with unreliable channels
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• Well-structured transition systems everywhere!
• On the reachability problem for 5-dimensional vector addition systems
• A structure to decide reachability in Petri nets
• Context-Bounded Analysis of Concurrent Queue Systems
• Title not available (Why is that?)
• State space reduction using partial order techniques
• Monotone data flow analysis frameworks
• Title not available (Why is that?)
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• Title not available (Why is that?)
• Precise interprocedural dataflow analysis with applications to constant propagation
• An O(n log n) unidirectional distributed algorithm for extrema finding in a circle
• Interprocedural analysis of asynchronous programs
• Decidability Results for Well-Structured Transition Systems with Auxiliary Storage
• Analysis of recursively parallel programs
• Title not available (Why is that?)
• Data flow analysis of asynchronous systems using infinite abstract domains
• Well-structured pushdown systems
• Fencing off Go: liveness and safety for channel-based programming
• Effect-driven flow analysis
• Safety verification of asynchronous pushdown systems with shaped stacks
• Complexity analysis of the backward coverability algorithm for VASS
• Hyper-Ackermannian bounds for pushdown vector addition systems
• Verifying liveness for asynchronous programs

Cited In (4)

• Bounded phase analysis of message-passing programs
• A fully abstract trace model for dataflow and asynchronous networks
• Data flow analysis of asynchronous systems using infinite abstract domains
• Interprocedural analysis of asynchronous programs

This page was built for publication: Data flow analysis of asynchronous systems using infinite abstract domains

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