Octocurious

Christina O'Donnell

REPLS and Kent Concurrency Workshop 2024 Roundup

July 25, 2024

On 18th-19th July 2024, the Univeristy of Kent hosted the 15th South of England Regional Programming Language Seminar, a regular informal meeting open to all interested in the semantics and implementation of new programming languages. This year it was jointly held with the Concurrency Workshop which aims to bring together researchers who are working thon the theory of concurrency and related areas. You can see the conference page here.

This was my first time attending either series and my second computer science conference I’ve ever been to, so I came in knowing no one and having no idea what to expect. My plan has been to go into conferences with a notebook and an aim to scribble down as much as possible while watching the talk. In particular I like to write down all the keywords and phrases that pop up to later look up.

Although many of the talks went over my head, I did find myself understanding bits of them and engaging by asking the odd question. My plan is to revise the topics that I found most interesting and to give myself a glancing understanding of the other topics, just so I can know vaguely what they are when they come up in future.

The rest of this post enumerates, the papers, giving a brief description with definitions for each one.

Unfortunately I only noted down the speaker’s name and not the additional contributors to each talk.

The titles of the talks were:

REPLS #

  • Modular Effective Programs
  • Algebraic effects with parameters and their handlers
  • A Logical Framework for Locally Cartesian Closed Categories
  • A Mixed Linear and Graded Logic: Proofs, Terms, and Models
  • Semantics for Nondeterministic Logic Programming via Mutually Exclusive Choice
  • Compositional imprecise probability
  • CPS or Direct Style? Why not both?
  • David Turner, 1946–2023
  • Semantics of Remote Direct Memory Access
  • IsaBIL: A Framework for Verifying (In)correctness of Binaries

Kent Concurrency Workshop #

  • Program Analysis for the People
  • Abstract hardware catches concrete bugs
  • Limitations of Concurrency on the Web
  • Invariants || concurrency
  • Mix Testing: Specifying and Testing ABI Compatibility Of C/C++ Atomics Implementations
  • Semi-automatic efficient granularity control
  • Completeness of Asynchronous Session Tree Subtyping in Coq
  • Non-Linear Communication via Graded Modal Session Types
  • TOASTER - A Toolchain for Generating Erlang Stubs with Inline Runtime Monitors from Timeout Asynchronous Session Types

You can see the list of talks on the conference page.

Modular Effective Programs #

by Nicolas Wu (Imperial College London)

Nicolas Wu discussed effect handlers, which are programming constructs that allow you to define and limit side effects. These effects include operations like changing state, handling exceptions, or introducing randomness. They matter for “pure” functional programming because they allow us to reason about what a particular function can and can’t do, enabling optimizations, control of determinism and more. Wu presented recent work on a Haskell library for higher-order algebraic effects, which provides a flexible interface for combining effects. This work supplants prior work on monad transformers which is a type contructor that turns one monad into another.

Definitions:

  • Effect Handlers: Tools to manage operations that affect the state or behavior of a program.
  • Side Effects: Operations that interact with the state of a program outside its local environment.
  • Monad Transformers: Structures that combine multiple computational contexts in the form of monads.

Algebraic effects with parameters and their handlers #

by Jesse Sigal (University of Edinburgh) joint work with:

Jesse Sigal introduced Paella, an Idris library for algebraic effects and handlers using Kripke semantics, which deal with possible worlds and their relationships. The library can manage effects involving dynamic allocation, such as creating and using reference cells. Implemented in the dependently-typed language Idris 2, it aims to improve mutable-to-immutable data transformation, thread scheduling, and constraint solving.

You can find the slides to this talk here.

Definitions:

  • Algebraic Effects: A way to represent operations that can have different effects depending on their context.
  • Kripke Semantics: A framework for modeling possible worlds and their interactions.
  • Dependent Types: A logic where types can depend on values.

A Logical Framework for Locally Cartesian Closed Categories #

by Zhixuan Yang (Imperial College London)

Zhixuan Yang talked about a logical framework that supports higher-order abstract syntax and equational axioms. This framework helps study type theories, which are formal systems categorizing types of data and their interactions. Yang sketched out the categorical semantics (mathematical structures that describe logical systems) for this framework.

Definitions:

A Mixed Linear and Graded Logic: Proofs, Terms, and Models #

by Tori Vollmer (University of Kent)

Tori Vollmer presented a framework combining graded modal logics with linear logic. This framework decomposes graded modalities into adjunctions and actions, providing a sequent calculus, proof theory, and categorical model. The work highlights shared principles between linear logic and graded modal logics.

Definitions:

  • Graded Modal Logic: A class of modal logic with modalities that can be quantified by integers to require that they must be used by at least that number of times.
  • Linear Logic: A class of logics where variables are treated as resources that must be used exactly once.
  • Sequent Calculus: A formal system for constructuing proofs in logic.

Semantics for Nondeterministic Logic Programming via Mutually Exclusive Choice #

by Michael Arntzenius (RelationalAI)

Michael Arntzenius discussed combining logical constraints with nondeterministic choices in logic programming, which is useful in areas like procedural content generation for video games. He introduced “finite-choice logic programming,” where rules can have multiple, mutually exclusive conclusions. This mutual exclusion is modeled using posets (partially ordered sets), where elements are incompatible if they have no upper bound. A bounded-complete poset ensures every compatible subset has a least upper bound. By constructing a complete lattice on mutually exclusive subsets, the semantics form a monotone map, and its least fixed point identifies minimal models of programs. Arntzenius also hinted at an implementation strategy inspired by this denotational semantics. This work is in collaboration with Robert J. Simmons and Chris Martens.

Definitions:

  • Nondeterministic Choice: Making a choice without a deterministic rule, potentially leading to multiple possible outcomes.
  • Poset (Partially Ordered Sets): Mathematical structures where some elements are comparable.
  • Bounded-Complete Poset: A poset where every bounded subset has a least upper bound.
  • Complete Lattice: A structure where every subset has both a least upper bound and a greatest lower bound.
  • Monotone map: A function that preserves the order of elements.
  • Denotational Semantics: A methodology for giving mathematical meaning to programming languages.

Compositional imprecise probability #

by Jack Liell-Cock (University of Oxford)

Jack Liell-Cock discussed models for imprecise probability. Imprecise probability is a precise term, not to be conflated with the simple lack of measurement prescision, is a method of modelling of Knightian uncertainty using convex regions. Knightian uncertainty refers to uncertainty that can’t be quantified, such as an unfair coin that you don’t know how much it is biased by. The goal is to support all kinds of composition, using graded monads to name and manage nondeterministic choices. This approach provides a fully compositional model for imprecise probability, improving upon existing monad-based methods.

Definitions:

  • Knightian uncertainty: A lack of any quantifiable knowledge about some possible occurrence, as opposed to the presence of quantifiable risk.
  • Imprecise Probability: A way to handle uncertainty in probability distributions.
  • Graded Monads: Structures that manage different levels of computation or effects.

CPS or Direct Style? Why not both? #

by Teodoro Freund (Huawei UK R&D)*

Teodoro Freund discussed combining CPS and direct style approaches for asynchronous functions, common in modern programming languages. He explored scenarios where each approach is beneficial and presented early results on dynamically switching between them, considering the trade-offs involved.

Continuation Passing Style (CPS): a style of programming in which control is passed explicitly in the form of a continuation.

David Turner, 1946–2023 #

by Simon Thompson (University of Kent)

Simon Thompson provided an appreciation of David Turner’s work and legacy, highlighting his contributions to programming languages and theoretical computer science at Kent. Turner’s influence continues in the PLAS group today.

He is best known for developing three programming languges SASL, Kent Recursive Calculator, and Miranda. Introducing lazy evaluation, combinator graph reduction, and polymorphic types in a functional programming language, having a strong influence on Haskell.

Semantics of Remote Direct Memory Access #

by Guillaume Ambal (Imperial College London)

Guillaume Ambal presented formal models for RDMA on x86-TSO machines, providing a foundation for specifying concurrent RDMA program behaviors. The models have been reviewed by NVIDIA and validated through extensive testing, aiming to support language-level models and verification techniques for RDMA systems.

Definitions:

  • RDMA (Remote Direct Memory Access): Technology allowing direct memory access between computers without involving their operating systems.
  • x86-TSO (Total Store Order): A memory consistency model for the x86 architecture.

IsaBIL: A Framework for Verifying (In)correctness of Binaries #

by Matthew Griffin (Imperial College London)

Matthew Griffin introduced IsaBIL, a binary analysis framework built within the Isabelle/HOL proof assistant and based on the Binary Analysis Platform (BAP). IsaBIL formalizes BAP’s intermediate language, BIL, and integrates it with Hoare logic for proving correctness and O’Hearn’s logic for proving incorrectness. It supports a wide range of languages, toolchains, and target architectures, and can be used even without source code. IsaBIL uses Isabelle locales for modular and extensible binary analysis, offering high-level reasoning rules and proof tactics to optimize verification.

Definitions:

Program Analysis for the People #

by Peter O’Hearn (University College London and Lacework)

Peter O’Hearn shared his journey applying mathematical logic and static analysis at Facebook. He discussed the challenges and successes of deploying program analysis tools in real-world environments, which led to many bugs being fixed before production. O’Hearn emphasized the importance of adapting theoretical knowledge to practical needs and highlighted the intellectual growth from moving between theory and practice.

Definitions:

  • Static Analysis: The process of analyzing code without executing it.
  • Program Analysis Tools: Software tools that help identify bugs and improve code quality.

Abstract hardware catches concrete bugs #

by Thomas Fourier1 (University of Cambridge)

Thomas Fourier introduced a technique to detect bugs from insufficient virtual-memory synchronization. The technique involves a relaxed-memory checker for Arm-A virtual memory, which runs during conventional testing to identify synchronization issues. This method has been used to find bugs in Google’s pKVM hypervisor for Android.

Definitions:

  • Virtual Memory Synchronization: Coordination of safe memory access in a virtual memory system.
  • Relaxed-Memory Checker: A tool to check memory consistency in relaxed-memory models.
  • Hypervisor: The system responsible for creating and runs virtual machines at the operating system level.

Limitations of Concurrency on the Web #

by Conrad Watt (University of Cambridge)

Conrad Watt explored the constraints on shared memory concurrency on the Web platform, which restricts certain atomic operations and synchronization primitives. He discussed challenges in compiling languages like C++ and Rust to WebAssembly and highlighted efforts to expand Web concurrency capabilities.

Definitions:

Invariants || concurrency #

by Cliff Jones (Newcastle University)

Cliff Jones emphasized the importance of abstract objects and data type invariants in formal methods for concurrent software. He discussed the use of rely/guarantee conditions and data reification to manage concurrency and liveness, drawing on recent research with Alan Burns on real-time scheduling.

Definitions:

Mix Testing: Specifying and Testing ABI Compatibility Of C/C++ Atomics Implementations #

by Luke Geeson (University College London)

Luke Geeson introduced mix testing to find compiler bugs related to ABI compatibility in concurrent programs. The technique involves separately compiling components and testing their composition. His tool, atomic-mixer, identified several new bugs in LLVM and GCC. This work has contributed to specifying an atomics ABI for Armv8.

Definitions:

Semi-automatic efficient granularity control #

by Vitaly Aksenov (University of London)

Vitaly Aksenov discussed techniques for controlling granularity in parallel computing systems, using an oracle-guided scheduling algorithm. Implemented in C++ as an extension of Cilk, this method matches the performance of hand-tuned codes, eliminating the need for manual optimization.

Definitions:

Completeness of Asynchronous Session Tree Subtyping in Coq #

by Burak Ekici (University of London)

Burak Ekici presented the first formalization of asynchronous subtyping in multiparty session types using Coq. By transforming session types into session trees and establishing a refinement relation, Ekici demonstrated the effectiveness of the formalization through verified subtyping schemas and reduced rules for inductive negation.

Definitions:

  • Asynchronous Subtyping: A type system that allows reordering of actions in concurrent programming.
  • Coq: A formal proof management system.

Non-Linear Communication via Graded Modal Session Types #

by Danielle Marshall (University of Glasgow)

Danielle Marshall explained how graded modal types can introduce controlled non-linearity in session types, enabling various concurrency behaviors. Using the Granule programming language, Marshall showcased a core calculus and operational model, highlighting the integration of graded modal session-typed primitives.

Definitions:

TOASTER - A Toolchain for Generating Erlang Stubs with Inline Runtime Monitors from Timeout Asynchronous Session Types #

by Jonah Pears (University of Kent)

Jonah Pears presented TOAST, a theory of asynchronous session types with timeouts, and its implementation in TOASTER. The tool generates Erlang stubs with inline runtime monitors, ensuring deadlock-free asynchronous communication with timeouts. A live demonstration showcased TOAST’s practical applications.

Definitions:

  • Session Types: Type systems ensuring safe and correct implementation of protocols.
  • Erlang: A programming language used for building concurrent systems.

Conclusion #

Did I get all those definitions right? If you were involved in the talks I summarised above, did I portray your work correctly? Do you want to hear more about any of these topics?

Let me know at christina@octocurious.com!

Thanks to all the people involved in this conference for being so welcoming to me. I eagerly await the next one!

  1. I was unable to find a homepage for Thomas Fourier. ↩︎