TY - GEN
T1 - Clustered Relational Thread-Modular Abstract Interpretation with Local Traces
AU - Schwarz, Michael
AU - Saan, Simmo
AU - Seidl, Helmut
AU - Erhard, Julian
AU - Vojdani, Vesal
N1 - Publisher Copyright:
© 2023, The Author(s).
PY - 2023
Y1 - 2023
N2 - We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables – given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.
AB - We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables – given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.
KW - clusters
KW - collecting local trace semantics
KW - concurrency
KW - dynamic thread creation
KW - thread-modular relational abstract interpretation
UR - http://www.scopus.com/inward/record.url?scp=85161450943&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-30044-8_2
DO - 10.1007/978-3-031-30044-8_2
M3 - Conference contribution
AN - SCOPUS:85161450943
SN - 9783031300431
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 28
EP - 58
BT - Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Proceedings
A2 - Wies, Thomas
PB - Springer Science and Business Media Deutschland GmbH
T2 - 32nd European Symposium on Programming, ESOP 2023, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023
Y2 - 22 April 2023 through 27 April 2023
ER -