Improving thread-modular abstract interpretation

DOI10.1007/978-3-030-88806-0_18MaRDI QIDQ2145342zbMATH OpenOpenAlexFDO

Authors Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani

Publication date 17 June 2022

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

zbMATH Keywords

collecting trace semanticsconcurrent systemsglobal invariantsside-effectsthread-modular abstract interpretation

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Min'e's approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks.

Recommendations

• Relational thread-modular static value analysis by abstract interpretation
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Thread-Modular Verification Is Cartesian Abstract Interpretation
• scientific article; zbMATH DE number 2087567
• Thread-modular counterexample-guided abstraction refinement

Cites work

• A semantics for concurrent separation logic
• Communicating state transition systems for fine-grained concurrent resources
• Computer Aided Verification
• Dataflow analysis for datarace-free programs
• Fast and Accurate Static Data-Race Detection for Concurrent Programs
• scientific article; zbMATH DE number 6712238 (Why is no real title available?)
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Relational thread-modular abstract interpretation under relaxed memory models
• Relational thread-modular static value analysis by abstract interpretation
• Resources, concurrency, and local reasoning
• Static analysis of run-time errors in embedded real-time parallel C programs
• Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
• Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
• Time, clocks, and the ordering of events in a distributed system

Cited in

(4)

• Relational thread-modular static value analysis by abstract interpretation
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• scientific article; zbMATH DE number 1955854 (Why is no real title available?)
• Clustered relational thread-modular abstract interpretation with local traces

Describes a project that uses

Uses Software

• Goblint

This page was built for publication: Improving thread-modular abstract interpretation

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