Thu 18 Jul 2019 16:20 - 16:40 at Mancy - Concurrency and Parallelism Chair(s): Stephen Kell

One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.

Thu 18 Jul

Displayed time zone: Belfast change

15:40 - 17:00
Concurrency and ParallelismResearch Papers at Mancy
Chair(s): Stephen Kell University of Kent
15:40
20m
Research paper
DynaSOAr: A Parallel Memory Allocator for Object-oriented Programming on GPUs with Efficient Memory Access
Research Papers
Matthias Springer Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
DOI Pre-print Media Attached
16:00
20m
Research paper
Reliable State Machines: A Framework for Programming Reliable Cloud Services
Research Papers
Suvam Mukherjee Microsoft Research India, Nitin John Raj International Institute of Information Technology, Hyderabad, Krishnan Govindraj Microsoft Research, Pantazis Deligiannis Microsoft Research, Chandramouleswaran Ravichandran Microsoft Azure, Akash Lal Microsoft Research India, Aseem Rastogi Microsoft Research, Raja Krishnaswamy Microsoft Azure
DOI Media Attached
16:20
20m
Research paper
Transferring Obligations Through Synchronizations
Research Papers
Jafar Hamin imec-DistriNet, Depatrmant of Computer Science, KU Leuven, Belgium, Bart Jacobs KU Leuven
DOI Media Attached
16:40
20m
Research paper
Motion Session Types for Robotic InteractionsBrave New Idea
Research Papers
Rupak Majumdar MPI-SWS, Germany, Marcus Pirron MPI-SWS, Nobuko Yoshida Imperial College London, Damien Zufferey MPI-SWS
DOI Media Attached