DoC members have three papers accepted at ACM SIGPLAN Conference

ACM SIGPLAN Conference on Programming Language Design and Implementation

Members of the Department of Computing have had three papers accepted at the ACM SIGPLAN Conference on Programming Language Design and Implementation, widely regarded as one of the two most prestigious conferences in the field Programming Languages. (It even has its own promotional song this year!)

The papers are (in alphabetical order):

• Revamping Hardware Persistency Models, by Kyeongmin Cho (KAIST, Korea), Sung-Hwan Lee (Seoul National University, Korea), Azalea Raad (Imperial College London), and Jeehoon Kang (KAIST, Korea)
• Test-Case Reduction and Deduplication Almost for Free with Transformation-Based Compiler Testing, by Alastair F. Donaldson (Imperial College London), Paul Thomson (Google), Vasyl Teliman (National Technical University, Ukraine), Stefano Milizia (Imperial College London), André Perez Maselco (Federal University of ABC, Brazil), and Antoni Karpi?ski (Warsaw University of Technology, Poland)
• Zooid: a DSL for Certified Multiparty Computation, by David Castro-Perez (University of Kent, Imperial College London), Francisco Ferreira (Imperial College London), Lorenzo Gheri (Imperial College London), and Nobuko Yoshida (Imperial College London)

"Revamping Hardware Persistency Models", by Cho, Lee, Raad and Kang, is a collaboration between Imperial College (Azalea Raad) and colleagues at KAIST, South Korea. It proposes a novel approach for specifying hardware persistency models, including those of the ubiquitous Intel-x86 (desktop) and ARMv8 (mobile) architectures. In doing so, this work identifies and fixes several weaknesses in existing semantics of Intel and ARM persistency. Check out the paper and associated artifacts.

“Test-Case Reduction and Deduplication Almost for Free with Transformation-Based Compiler Testing” is based on work that Donaldson (Imperial College) undertook with long-term collaborator Thomson when Donaldson held a joint appointment between Imperial and Google. It is a collaboration with Google interns Milizia (an Imperial undergraduate) and Karpi?ski, as well as with Teliman and Perez Maselco who worked on the project via Google Summer of Code.

The paper describes a new approach to automatically finding bugs in compiles - the software components that turn human-written programs into machine code - with a specific focus on compilers for graphics processing units (GPUs). It introduces the spirv-fuzz tool, an automated tester of compilers for the SPIR-V programming language, which is at the heart of the modern Vulkan GPU programming model. Check out the paper and associated artifact.

“Zooid: a DSL for Certified Multiparty Computation”, by Castro-Perez (Kent and Imperial), Ferreira, Gheri and Yoshida (Imperial) addresses the problem of designing and implementing distributed systems. Distributed systems are challenging to design and implement, yet they are commonplace and part of our everyday life online, especially now that so many aspects are mediated by web services, like conference management systems, messaging software and booking services.

This work applies Multiparty Session Types (MPST) [POPL08, JACM], which allow to specify and implement distributed protocols ensuring that all participants comply the choreographic protocol without deadlock and livelock. The work proposes first to set the foundational theory of MPST in solid ground by mechanising the metatheory of MPST in the Coq proof assistant.

The main result of this part is a formal proof of the trace equivalence of the behaviours of the global specification and the local views of all the participants. In Zooid, the mechanisation provides value beyond the proof document, by building a certified domain specific language for implementing distributed systems. The Zooid design builds on top of the formal proofs, a language to implement processes that are guaranteed to behave according to the protocol, in a type-safe and deadlock-free way.  Check out the paper, and associated artifact on Github and Zenodo. 

A tutorial for Zooid will be given by the authors at the upcoming workshop VEST’21 (July 2021) at ICALP’21.