Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 17:15 - 17:30 at VMCAI - Hyperproperties Chair(s): Grigory Fedyukovich

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory FedyukovichFlorida State University
17:00 - 17:15
Compositional Model Checking for Multi-Properties
Ohad GoudsmidDepartment of Computer Science, The Technion, Orna GrumbergTechnion – Israel Institute of Technology, Sarai SheinvaldDepartment of Software Engineering, ORT Braude College of Engineering
Media Attached
17:15 - 17:30
Decomposing Data Structure Commutativity Proofs with mn-Differencing
Eric KoskinenStevens Institute of Technology, Kshitij BansalGoogle
Media Attached