Decomposing Data Structure Commutativity Proofs with mn-Differencing
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.
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
17:00 - 17:30
|Compositional Model Checking for Multi-Properties|
Ohad Goudsmid Department of Computer Science, The Technion, Orna Grumberg Technion – Israel Institute of Technology, Sarai Sheinvald Department of Software Engineering, ORT Braude College of EngineeringMedia Attached
|Decomposing Data Structure Commutativity Proofs with mn-Differencing|