Data flow analysis of asynchronous systems using infinite abstract domains

DOI10.1007/978-3-030-72019-3_2MaRDI QIDQ2233447zbMATH OpenOpenAlexFDO

Authors Snigdha Athaiya, Raghavan Komondoor, K. Narayan Kumar

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

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

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)

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.

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

Cites work

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

Cited in

(4)

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

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)