Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 18:30 - 18:45 at VMCAI - Concurrent and Distributed Systems Chair(s): Dana Drachsler Cohen

Correctness verification of a concurrent history is challenging and has been proven to be an NP-complete problem. The reason that verifying correctness cannot be solved in polynomial time is a consequence of the way correctness is defined. Traditional correctness conditions require a concurrent history to be equivalent to a legal sequential history. The worst case number of legal sequential histories for a concurrent history is O(n!) with respect to n methods invoked. Existing correctness verification tools improve the time complexity by either reducing the size of the possible legal sequential histories or improving the efficiency of generating the possible legal sequential histories. Further improvements to the time complexity of correctness verification can be achieved by changing the way correctness of concurrent programs is defined. In this paper, we present the first methodology to recast the correctness conditions in literature to be defined in vector space. The concurrent histories are represented as a set of method call vectors, and correctness is defined as properties over the set of vectors. The challenge with defining correctness in vector space is accounting for method call ordering and data structure semantics. We solve this challenge by incorporating a priority assignment scheme to the values of the method call vectors. Using our new definitions of concurrent correctness, we design a dynamic analysis tool that checks the correctness of concurrent data structures in O(n^2) with respect to n method calls, a significant improvement over O(n!) time required to analyze legal sequential histories. We showcase our dynamic analysis tool by using it to check the correctness of a variety of queues, stacks, and hashmaps.

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler Cohen Technion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina Peterson University of Central Florida, Victor Cook University of Central Florida, Damian Dechev University of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Mehdi Naouar University of Freiburg, Andreas Podelski University of Freiburg, Germany, Claus Schätzle University of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Informal Systems Inc, Josef Widder Informal Systems, Florian Zuleger Vienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie Bertrand INRIA Rennes, Marijana Lazic Technical University of Munich, Josef Widder Informal Systems
Media Attached