Programming Languages and Analysis and Verification get-together December 2022
Tuesday 6th December 2022, starting at 12:00PM in lecture theatre 311.
This event is open to everyone (PhD students, RAs, faculty and admin staff) who identifies with the department’s Programming Languages and Analysis and Verification themes.
What is it? Following on from our fun gathering in May, this get-together is once again for everyone (PhD students, RAs and faculty) who identifies with one/both of the above themes.
What’s the aim? To get to know each other better across research groups, and especially to welcome PhD students and RAs who started recently.
What will it involve? Welcome lunch, followed by a programme of informal talks and discussions, and dinner in the evening. The main idea is to have a lot of time to talk to and get to know each other better.
Is it for me? If you believe your work relates to one of these themes, then it’s for you. I expect that most attendees will be PhD students or postdocs of academics who are part of these themes, but we are aiming to be inclusive of others in the department whose work is related.
PROGRAMME
12:00-13:00 Lunch
13:00-13:20 Lightning talks and introductions.
13:20-13:40 Sam Coward, Circuits and Systems, Department of Electrical and Electronic Engineering (EEE). E-Graphs for Exploration: All Implementations are Equal But Some are More Equal Than Others.
Around since the 1970's, e-graphs are not a new data structure, but in recent years they've taken aim at exploration and optimization problems. Providing a compact representation of equivalent designs and a complete history of the design space explored, they've proved useful in a range of domains. To date researchers have used e-graphs to automate numerical stability analysis, datapath hardware design, rewrite rule synthesis and much more. In this talk I hope to raise awareness of e-graphs and potentially discover new applications from the audience!
13:40-14:00 Sacha Ayoun and Nat Karmios, Verified Software Group. Gillian – Debugging, C, Rust.
Gillian is a multi-language platform for symbolic analysis. It allows for three kinds of analysis : Whole-program symbolic testing, Compositional verification based on Separation Logic, and Bi-Abduction, in the style of Infer Pulse. In this talk, we’ll show the latest improvements to the user experience of Gillian, how we got students to use it, and what it could mean for the future of verification for programs written using the Rust programming language.
14:00-14:20 Oisin Kidney, Functional Programming Group. Equations for Algebraic Effects.
Algebraic effects are a standard formalism for describing programs and their effect systems, but up until now formalisations of algebraic effects have lacked the ability to properly express equations over the algebraic structures they describe. This work uses some new tools to fully formalise the theories of programs with a wide array of algebraic effects.
14:20-14:30 - Luke Cheeseman, SLURP. When Concurrency Strikes.
Concurrent programming has been ubiquitously adopted to utilise the great potential provided by modern hardware. A multitude of concurrency paradigms have been proposed, often with the aim to offer atomicity, data-race freedom, flexible coordination across different resources, deadlock freedom, ordering guarantees, ease of programming, and efficient implementation. We believe that so far, none of these paradigms have reached the sweet-spot in the design that satisfies all these requirements. We introduce Behaviour-Oriented Concurrency (BoC), a paradigm that enables asynchronously creating atomic and ordered units of work with exclusive access to a collection of independent resources. We argue that BoC satisfies all the requirements from above. We argue the applicability of this paradigm through concurrency challenges, and show that our C++ implementation is efficient, achieving almost perfect scaling in system-level experiments.
14:30-15:00 Herbert Wiklicky, Department of Computing. Challenges of Quantum Programming.
Quantum computation is one of the most intriguing developments regarding hardware we might have to face in future. This will lead to new models and frameworks underlying programming. At the moment we have first experimental realisations of systems with a few ideal qubits or slightly larger collections of noisy qubits. Quantum communication (Key Distribution, Teleportation) is a realistic proposition already now. The particular nature of these quantum devices requires us to reconsider our underlying assumptions on what programming constructs idioms are required in order to implement quantum algorithms as well as their verification. The aim is a personal review of some of these aspects (e.g. computational state, entanglement, measurements, noise and error correction, quantum logics, etc.).
15:00-15:30 Coffee break
15:30-16:20 Breakout session, overseen by Paul Kelly, Department of Computing
16:20-16:40 Marios Kogias, Large Scale Data and Systems (LSDS) Group. Datacenter Systems: A Great Opportunity for System and PL Co-design.
In this talk I will go through the main research challenges and opportunities in building datacenter systems that can provide tail-tolerance, fault-tolerance, and confidentiality guarantees. I will particularly focus on the need for interplay between systems and PL research and showcase my experience with that through 2 projects. Enclosure (ASPLOS21) is a new programming language construct for library isolation that provides a developer with fine-grain control over the resources that a library can access, even for libraries with complex inter-library dependencies. Concord (under submission) is a runtime for microsecond-scale RPCs that eliminates the need for hardware interrupts for scheduling using compiler passes to enforce a precise cooperative scheduling mechanism.
16:40-17:00 Arindam Sharma, Software Reliability Group (SRG). Patch Analysis using Modular Product Programs.
Software testing is key to the reliability of software systems. Consequently, most software systems usually spend a lot of time in maintenance phase where small patches are applied to the existing software. Hence testing these software patches is important. One way of doing it is by combining the pre- and post-patched versions into a single program, called a product program and thereby using the existing tools that work on a single program for patch testing.
17:00-18:30: Free time
18:30- Dinner at a local restaurant
Regitration is now closed, but if you want to attend and have not yet registered, please email Teresa [email protected] or Ally Donaldson [email protected] before Friday 2nd December.
May 2022: Programming Languages and Analysis and Verification get-together
Tuesday, 17th May 2022
An event open to everyone (PhD students, RAs, faculty and admin staff) who identifies with the department’s Programming Languages and Analysis and Verification themes.
LIGHTNING TALKS PARTICIPANTS INFO: (in alphabetical order)
(to add of amend these, or If you have any questions about the event, please email Teresa [email protected] )
George Bisbas, George is a final year PhD student working with Professor Paul Kelly on the Devito project. His research is focused on Domain-Specific Languages and compilers for High-Performance Computing. More specifically, George aims to automate cache-related optimizations such as temporal blocking in order to accelerate the solution of Partial-Differential Equations through the finite-difference method.
Cristian Cadar is a Professor in DoC, where he leads the Software Reliability Group. His research interests span the areas of software engineering, computer systems and software security, with a focus on building practical techniques for improving the reliability and security of software systems.
David Davies, Functional Programming Group. David is a 1st year PhD student supervised by Steffen van Bakel and Nick Wu. He is interested in dependent type theory and classical logic, and λ-calculi that can capture continuations (and cause effects), as well as implementing these into programming languages. He is happy to chat about these things and Haskell.
Alastair Donaldson, Multicore Programming Group. Ally is a Professor in DoC, interested in programming languages, testing and verification. Currently he mainly works on the reliability of programming language implementations, which includes automated randomised testing of compilers, and using formal techniques to make programming language specifications more precise.
Philippa Gardner, Verified Software group. Philippa is a Professor in DoC, and her research focusses on program specification and verification. Her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, and is currently developing the Gillian platform for building symbolic analysis tools for real-world programming languages such as C and JavaScript, which unifies classical symbolic execution, semi-automatic verification based on separation logic, and automatic compositional testing based on bi-abduction.
Dan Iorga is a final year PhD student working with Alastair Donaldson and John Wickerson. His research interests are in testing, verification, and specification design of shared-memory multicore systems, especially heterogeneous CPU/FPGA systems.
Jordy Ruiz is a Research Associate at DoC, where he works in the Software Reliability Group (SRG). Jordy’s current research work revolves around symbolic execution and static analysis of programs, namely working on the Chopper tool in order to automate the selection of skipped code regions. Besides that, Jordy’s research interests include abstract interpretation, binary code analysis, mathematical abstractions and (formal) proofs.
Omar Tahir, Custom Computing Group and Functional Programming Group. Omar is a first-year PhD student under the supervision of Wayne Luk and Nick Wu. His research lies in the intersection between functional programming and digital design, in particular using algebraic effects to assist in designing and analysing hardware. Among other things, he is also interested in computer architecture, fractal geometry and theorem proving.
Jamie Willis, Jamie is a PhD student in his 3rd year at Imperial supervised by Nicolas Wu in the Functional Programming Group. He is interested in making parser combinators into the obvious tool of choice for writing parsers in the functional world (as well as bringing these concepts to the wider community). To make this possible, he makes use of a principled meta-programming technique called staging. He is more than happy to discuss anything about parsing and parser combinators, meta-programming (and how to battle with static and dynamic domain-specific information), and also all things Haskell and Scala.
PROGRAMME TALKS
Symbolic Execution and KLEE at the Software Reliability Group, Martin Nowack. Abstract: At the Software Reliability Group, symbolic execution is a vital research topic. With KLEE at its heart, we maintain and continue to develop a symbolic execution engine well known across academia and industry. This talk will provide a short introduction to symbolic execution and a brief overview of some of our group’s past and continuing research in this context.
A Brief Introduction to the Mobility Reading Group, Adam Barwell. Abstract: The Mobility Reading Group aims to improve the reliability and correctness of concurrent and distributed systems via behavioural type systems. In this talk, I will give a brief introduction as to who we are, the problems that motivate us, and what we are currently working on.
Advances in Automated Compiler Testing, Karine Even Mendoza. Abstract: The critical role of compilers, which underpin all deployed software practically, has led to a great deal of interest in techniques for automated compiler testing, with a surge of interest in this topic over the last decade. Compiler fuzzing has been extremely effective and led to hundreds of bugs reported in critical compiler infrastructures such as LLVM and GCC. However, compilers are starting to become relatively immune to such fuzzers, which can no longer find many compiler bugs as a decade ago. In this talk, I will present techniques for more intensive compiler testing, which we have applied on top of existing fuzzers such as Csmith and LibFuzzer and which have led to a contribution of test cases to the Clang/LLVM test suite and many new bug reports in mature compilers as LLVM and GCC and in static code analysers as Frama-c.
Panel discussion: Careers and mentorship in Programming Languages and Analysis & Verification. Karine Even Mendoza, Paul Kelly, Azalea Raad, Nick Wu.
Logical and Algebraic Foundations for Verification, Daniele Nantes Sobrinho. Abstract: I will briefly present the last contributions I was involved in, both in algebraic developments for automated reasoning and logical foundations for verification techniques for message-passing programs based on behavioral type systems. Also, I would like to discuss (informally) some possible connections between this theoretical work and the applied research conducted by the Verified Software group, and the prospects for future work.
Validating the (Memory) Persistency Semantics of Intel-x86 Architecture, Vasileios Klimis. Abstract: Memory persistency models prescribe the order Non-Volatile Memory (NVM) `writes’ become durable. This allows programmers to reason about guarantees on recovery-correctness. We consider the problem of validating empirically the formalisation of the persistency semantics of programs interfacing with NVM. To explore recoverability behaviour with respect to durability and ordering in normal operation (instead of simulating power-loss crashes while the workload is running), we monitor the DDR4 bus traffic in real time by interposing a monitoring object between CPU and main memory in the DDR bus. By conducting validity litmus tests on several examples of persistent programs, we judge the goodness of the Px86 (‘persistent x86’) model and confirm that the assumptions underlying the model are justifiable.
Towards temporal blocking as part of Devito: The Devito DSL and compiler framework and on-going work towards automated temporal blocking, George Bisbas. Abstract: This talk presents (a) Devito, a Domain-Specific Language and compiler for optimised stencil computation (e.g., finite differences, image processing, machine learning) from a high-level symbolic abstraction and (b) our work in enhancing its available built-in optimisations. Devito’s DSL builds on top of SymPy, is rich enough to describe real-world problems and is actively used in production codes (e.g. seismic and medical imaging). Users can write partial differential equations in a symbolic language, and Devito’s compiler employs automated code generation through just-in-time compilation to generate and execute optimised kernels on various computer platforms. These optimisations, which are very tedious and complex to apply by hand, are automatically applied by Devito. The separation of concerns among disciplines helps to increase productivity and helps scientists focus on modelling their domain problems. My work aims to raise the performance bar by enhancing Devito’s optimisations with temporal blocking. Temporal blocking is an advanced cache optimisation technique, proven to be beneficial for stencils but very complicated to apply manually.
When Concurrency Strikes, Luke Cheeseman. Abstract: Concurrent programming has been ubiquitously adopted to utilise the great potential provided by modern hardware. A multitude of concurrency paradigms have been proposed, often with the aim to offer atomicity, data-race freedom, flexible coordination across different resources, deadlock freedom, ordering guarantees, ease of programming, and efficient implementation. We believe that so far, none of these paradigms have reached the sweet-spot in the design that satisfies all these requirements.
We introduce Behaviour-Oriented Concurrency (BoC), a paradigm that enables asynchronously creating atomic and ordered units of work with exclusive access to a collection of independent resources. We argue that BoC satisfies all the requirements from above. We argue the applicability of this paradigm through concurrency challenges, and show that our C++ implementation is efficient, achieving almost perfect scaling in system-level experiments.
Verified software, verified hardware, verified everything, Andreas Lööw. Abstract: In this talk I briefly outline some challenges involved in building so-called verified stacks, that is, computer systems with proofs of correctness all the way from the system’s application software down to, and including, the hardware implementation of the system. Among other things, I describe a verified stack built using hardware development tools I have developed and the CakeML compiler. The stack is capable of running the CakeML compiler on top of itself; all proofs were developed in, and checked by, the HOL4 interactive theorem prover and covers the whole stack all the way down to the Verilog implementation of the verified processor at the bottom of the stack.
Parsley: A Staged Parser Combinator Story, Jamie Willis. Abstract: In this talk I will be discussing the general ideas behind the work I do in my PhD, which is to help improve the viability of parser combinators for parsing tasks more commonly reserved for parser generators or hand-written parsers. I will discuss briefly both what parser combinators are, and how I use staged meta-programming to accomplish my goals at a high-level.
