Decomposing Data Structure Commutativity Proofs with mn -Differencing

Eric Koskinen, Kshitij Bansal

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Proceedings
EditorsFritz Henglein, Sharon Shoham, Yakir Vizel
Pages81-103
Number of pages23
DOIs
StatePublished - 2021
Event22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 - Copenhagen, Denmark
Duration: 17 Jan 202119 Jan 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12597 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021
Country/TerritoryDenmark
CityCopenhagen
Period17/01/2119/01/21

Fingerprint

Dive into the research topics of 'Decomposing Data Structure Commutativity Proofs with mn -Differencing'. Together they form a unique fingerprint.

Cite this