51³Ô¹ÏÍø

ACM SIGPLAN Conference on Programming Language Design and Implementation

Members of the Department of Computing have had three papers accepted at the , widely regarded as one of the two most prestigious conferences in the field Programming Languages. (It even has its own this year!)

The papers are (in alphabetical order):

• , by Kyeongmin Cho (KAIST, Korea), Sung-Hwan Lee (Seoul National University, Korea), Azalea Raad (51³Ô¹ÏÍø), and Jeehoon Kang (KAIST, Korea)
• , by Alastair F. Donaldson (51³Ô¹ÏÍø), Paul Thomson (Google), Vasyl Teliman (National Technical University, Ukraine), Stefano Milizia (51³Ô¹ÏÍø), André Perez Maselco (Federal University of ABC, Brazil), and Antoni Karpi?ski (Warsaw University of Technology, Poland)
• , by David Castro-Perez (University of Kent, 51³Ô¹ÏÍø), Francisco Ferreira (51³Ô¹ÏÍø), Lorenzo Gheri (51³Ô¹ÏÍø), and Nobuko Yoshida (51³Ô¹ÏÍø)

"Revamping Hardware Persistency Models", by Cho, Lee, Raad and Kang, is a collaboration between 51³Ô¹ÏÍø 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. and .

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

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 programming language, which is at the heart of the modern GPU programming model. and .

“Zooid: a DSL for Certified Multiparty Computation”, by Castro-Perez (Kent and 51³Ô¹ÏÍø), Ferreira, Gheri and Yoshida (51³Ô¹ÏÍø) 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) [, ], 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.  , and associated artifact on and . 

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