TY - GEN
T1 - Decomposing Data Structure Commutativity Proofs with mn -Differencing
AU - Koskinen, Eric
AU - Bansal, Kshitij
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - Commutativity of data structure methods is of ongoing interest in contexts such as parallelizing compilers, transactional memory, speculative execution and software scalability. Despite this interest, we lack effective theories and techniques to aid commutativity verification. In this paper, we introduce a novel decomposition to improve the task of verifying method-pair commutativity conditions from data structure implementations. The key enabling insight—called mn -differencing—defines the precision necessary for an abstraction to be fine-grained enough so that commutativity of method implementations in the abstract domain entails commutativity in the concrete domain, yet can be less precise than what is needed for full-functional correctness. We incorporate this decomposition into a proof rule, as well as an automata-theoretic reduction for commutativity verification. Finally, we discuss our simple proof-of-concept implementation and experimental results showing that mn -differencing leads to more scalable commutativity verification of some simple examples.
AB - Commutativity of data structure methods is of ongoing interest in contexts such as parallelizing compilers, transactional memory, speculative execution and software scalability. Despite this interest, we lack effective theories and techniques to aid commutativity verification. In this paper, we introduce a novel decomposition to improve the task of verifying method-pair commutativity conditions from data structure implementations. The key enabling insight—called mn -differencing—defines the precision necessary for an abstraction to be fine-grained enough so that commutativity of method implementations in the abstract domain entails commutativity in the concrete domain, yet can be less precise than what is needed for full-functional correctness. We incorporate this decomposition into a proof rule, as well as an automata-theoretic reduction for commutativity verification. Finally, we discuss our simple proof-of-concept implementation and experimental results showing that mn -differencing leads to more scalable commutativity verification of some simple examples.
UR - http://www.scopus.com/inward/record.url?scp=85101582954&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85101582954&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-67067-2_5
DO - 10.1007/978-3-030-67067-2_5
M3 - Conference contribution
AN - SCOPUS:85101582954
SN - 9783030670665
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 81
EP - 103
BT - Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Proceedings
A2 - Henglein, Fritz
A2 - Shoham, Sharon
A2 - Vizel, Yakir
T2 - 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021
Y2 - 17 January 2021 through 19 January 2021
ER -