Wed 18 Jan 2023 11:35 - 12:00 at Grand Ballroom A - Automated Verification Chair(s): Michael Greenberg

There is a wide variety of message-passing communication models, ranging from synchronous "rendez-vous" communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the network, and a few classes of orders of message delivery (FIFO, causally ordered) have been identified in the early days of distributed computing. For local-scale message-passing applications, e.g., running on a single machine, the communication model may be determined by the actual implementation of message buffers and by how FIFO queues are used. While large-scale communication models, such as causal ordering, are defined by logical axioms, local-scale models are often defined by an operational semantics. In this work, we connect these two approaches, and we present a unified hierarchy of communication models encompassing both large-scale and local-scale models, based on their concurrent behaviors. We also show that all the communication models we consider can be axiomatized in the monadic second order logic, and may therefore benefit from several bounded verification techniques based on bounded special treewidth.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:45 - 12:00
Automated VerificationPOPL at Grand Ballroom A
Chair(s): Michael Greenberg Stevens Institute of Technology
10:45
25m
Talk
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
POPL
Michalis Kokologiannakis MPI-SWS, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS
DOI
11:10
25m
Talk
Stratified Commutativity in Verification Algorithms for Concurrent ProgramsVirtual
POPL
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg
DOI
11:35
25m
Talk
A Partial Order View of Message-Passing Communication Models
POPL
Cinzia Di Giusto Université Côte d'Azur; CNRS, Davide Ferre' Université Côte d'Azur; CNRS, Laetitia Laversa Université Côte d'Azur; CNRS, Etienne Lozes Université Côte d'Azur; CNRS
DOI