-
High-performance training and inference for deep equivariant interatomic potentials
Authors:
Chuin Wei Tan,
Marc L. Descoteaux,
Mit Kotak,
Gabriel de Miranda Nascimento,
Seán R. Kavanagh,
Laura Zichi,
Menghang Wang,
Aadit Saluja,
Yizhong R. Hu,
Tess Smidt,
Anders Johansson,
William C. Witt,
Boris Kozinsky,
Albert Musaelian
Abstract:
Machine learning interatomic potentials, particularly those based on deep equivariant neural networks, have demonstrated state-of-the-art accuracy and computational efficiency in atomistic modeling tasks like molecular dynamics and high-throughput screening. The size of datasets and demands of downstream workflows are growing rapidly, making robust and scalable software essential. This work presen…
▽ More
Machine learning interatomic potentials, particularly those based on deep equivariant neural networks, have demonstrated state-of-the-art accuracy and computational efficiency in atomistic modeling tasks like molecular dynamics and high-throughput screening. The size of datasets and demands of downstream workflows are growing rapidly, making robust and scalable software essential. This work presents a major overhaul of the NequIP framework focusing on multi-node parallelism, computational performance, and extensibility. The redesigned framework supports distributed training on large datasets and removes barriers preventing full utilization of the PyTorch 2.0 compiler at train time. We demonstrate this acceleration in a case study by training Allegro models on the SPICE 2 dataset of organic molecular systems. For inference, we introduce the first end-to-end infrastructure that uses the PyTorch Ahead-of-Time Inductor compiler for machine learning interatomic potentials. Additionally, we implement a custom kernel for the Allegro model's most expensive operation, the tensor product. Together, these advancements speed up molecular dynamics calculations on system sizes of practical relevance by up to a factor of 18.
△ Less
Submitted 22 April, 2025;
originally announced April 2025.
-
Message-Observing Sessions
Authors:
Ryan Kavanagh,
Brigitte Pientka
Abstract:
We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give M…
▽ More
We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.
△ Less
Submitted 7 March, 2024;
originally announced March 2024.
-
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
Authors:
Chuta Sano,
Ryan Kavanagh,
Brigitte Pientka
Abstract:
Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows…
▽ More
Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as session-typed languages.
△ Less
Submitted 21 September, 2023;
originally announced September 2023.
-
Fairness and Communication-Based Semantics for Session-Typed Languages
Authors:
Ryan Kavanagh
Abstract:
We give communication-based semantics and reasoning techniques for Polarized SILL, a rich session-typed programming language with general recursion. Its features include channel and code transmission, synchronous and asynchronous communication, and functional programming. Our contributions are distinguished by their faithfulness to the process abstraction, i.e., to the premise that communication i…
▽ More
We give communication-based semantics and reasoning techniques for Polarized SILL, a rich session-typed programming language with general recursion. Its features include channel and code transmission, synchronous and asynchronous communication, and functional programming. Our contributions are distinguished by their faithfulness to the process abstraction, i.e., to the premise that communication is the only observable phenomenon of processes. We give the first observed communication semantics that supports general recursion and code transmission. Observed communication semantics define the meaning of processes in terms of their observed communications. We use this observational semantics to define experiments on processes, and we give a communication-based testing equivalences framework for defining observational simulations and equivalences on processes. This framework captures several natural equivalences, and we show that one of these coincides with barbed congruence, the canonical notion of process equivalence.
Polarized SILL is defined using a substructural operational semantics based on multiset rewriting. To ensure that our contributions are well-defined in the presence of non-termination, we introduce fairness for multiset rewriting systems. We construct a fair scheduler, we give sufficient conditions for traces to be fair, and we study the effects of permutation on fair traces.
△ Less
Submitted 1 November, 2021; v1 submitted 2 April, 2021;
originally announced April 2021.
-
Substructural Observed Communication Semantics
Authors:
Ryan Kavanagh
Abstract:
Session-types specify communication protocols for communicating processes, and session-typed languages are often specified using substructural operational semantics given by multiset rewriting systems. We give an observed communication semantics for a session-typed language with recursion, where a process's observation is given by its external communications. To do so, we introduce fair executions…
▽ More
Session-types specify communication protocols for communicating processes, and session-typed languages are often specified using substructural operational semantics given by multiset rewriting systems. We give an observed communication semantics for a session-typed language with recursion, where a process's observation is given by its external communications. To do so, we introduce fair executions for multiset rewriting systems, and extract observed communications from fair process executions. This semantics induces an intuitively reasonable notion of observational equivalence that we conjecture coincides with semantic equivalences induced by denotational semantics, bisimulations, and barbed congruences for these languages.
△ Less
Submitted 31 August, 2020;
originally announced August 2020.
-
Parametrized Fixed Points on O-Categories and Applications to Session Types
Authors:
Ryan Kavanagh
Abstract:
O-categories generalize categories of domains to provide just the structure required to compute fixed points of locally continuous functors. Parametrized fixed points are of particular interest to denotational semantics and are often given by "dagger operations". We generalize existing techniques to define a functorial dagger operation on locally continuous functors between O-categories. We show t…
▽ More
O-categories generalize categories of domains to provide just the structure required to compute fixed points of locally continuous functors. Parametrized fixed points are of particular interest to denotational semantics and are often given by "dagger operations". We generalize existing techniques to define a functorial dagger operation on locally continuous functors between O-categories. We show that this dagger operation satisfies the Conway identities, a collection of identities used to axiomatize iteration theories. We study the behaviour of this dagger operation on natural transformations and consider applications to semantics of session-typed languages.
△ Less
Submitted 15 June, 2020;
originally announced June 2020.
-
A Domain Semantics for Higher-Order Recursive Processes
Authors:
Ryan Kavanagh
Abstract:
The polarized SILL programming language uniformly integrates functional programming and session-typed message-passing concurrency. It supports general recursion, asynchronous and synchronous communication, and higher-order programs that communicate channels and processes. We give polarized SILL a domain-theoretic semantics---the first denotational semantics for a language with this combination of…
▽ More
The polarized SILL programming language uniformly integrates functional programming and session-typed message-passing concurrency. It supports general recursion, asynchronous and synchronous communication, and higher-order programs that communicate channels and processes. We give polarized SILL a domain-theoretic semantics---the first denotational semantics for a language with this combination of features. Session types in polarized SILL denote pairs of domains of unidirectional communications. Processes denote continuous functions between these domains, and process composition is interpreted by a trace operator. We illustrate our semantics by validating expected program equivalences.
△ Less
Submitted 10 May, 2020; v1 submitted 5 February, 2020;
originally announced February 2020.
-
A denotational account of C11-style memory
Authors:
Ryan Kavanagh,
Stephen Brookes
Abstract:
We introduce a denotational semantic framework for shared-memory concurrent programs in a C11-style memory model. This denotational approach is an alternative to techniques based on "execution graphs" and axiomatizations, and it allows for compositional reasoning. Our semantics generalizes from traces (sequences of actions) to pomsets (partial orders of actions): instead of traces and interleaving…
▽ More
We introduce a denotational semantic framework for shared-memory concurrent programs in a C11-style memory model. This denotational approach is an alternative to techniques based on "execution graphs" and axiomatizations, and it allows for compositional reasoning. Our semantics generalizes from traces (sequences of actions) to pomsets (partial orders of actions): instead of traces and interleaving, we embrace "true" concurrency. We build on techniques from our prior work that gives a denotational semantics to SPARC TSO. We add support for C11's wider range of memory orderings, e.g., acquire-release and relaxed, and support for local variables and various synchronization primitives, while eliminating significant amounts of technical bookkeeping. Our approach features two main components. We first give programs a syntax-directed denotation in terms of sets of pomsets of memory actions. We then give a race-detecting executional interpretation of pomsets using footprints and a local view of state.
△ Less
Submitted 11 April, 2018;
originally announced April 2018.
-
A Denotational Semantics for SPARC TSO
Authors:
Ryan Kavanagh,
Stephen Brookes
Abstract:
The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We sho…
▽ More
The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We show that our denotational account is sound and complete relative to the axiomatic account, that is, that it captures exactly the behaviours permitted by the axiomatic account. Our compositional approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.
△ Less
Submitted 7 May, 2019; v1 submitted 2 November, 2017;
originally announced November 2017.
-
TANGO: Transparent heterogeneous hardware Architecture deployment for eNergy Gain in Operation
Authors:
Karim Djemame,
Django Armstrong,
Richard Kavanagh,
Jean-Christophe Deprez,
Ana Juan Ferrer,
David Garcia Perez,
Rosa Badia,
Raul Sirvent,
Jorge Ejarque,
Yiannis Georgiou
Abstract:
The paper is concerned with the issue of how software systems actually use Heterogeneous Parallel Architectures (HPAs), with the goal of optimizing power consumption on these resources. It argues the need for novel methods and tools to support software developers aiming to optimise power consumption resulting from designing, developing, deploying and running software on HPAs, while maintaining oth…
▽ More
The paper is concerned with the issue of how software systems actually use Heterogeneous Parallel Architectures (HPAs), with the goal of optimizing power consumption on these resources. It argues the need for novel methods and tools to support software developers aiming to optimise power consumption resulting from designing, developing, deploying and running software on HPAs, while maintaining other quality aspects of software to adequate and agreed levels. To do so, a reference architecture to support energy efficiency at application construction, deployment, and operation is discussed, as well as its implementation and evaluation plans.
△ Less
Submitted 4 March, 2016;
originally announced March 2016.
-
On Coupled Logical Bisimulation for the Lambda-Calculus
Authors:
Ryan Kavanagh,
Jean-Marie Madiot
Abstract:
We study coupled logical bisimulation (CLB) to reason about contextual equivalence in the lambda-calculus. CLB originates in a work by Dal Lago, Sangiorgi and Alberti, as a tool to reason about a lambda-calculus with probabilistic constructs. We adapt the original definition to the pure lambda-calculus. We develop the metatheory of CLB in call-by-name and in call-by-value, and draw comparisons wit…
▽ More
We study coupled logical bisimulation (CLB) to reason about contextual equivalence in the lambda-calculus. CLB originates in a work by Dal Lago, Sangiorgi and Alberti, as a tool to reason about a lambda-calculus with probabilistic constructs. We adapt the original definition to the pure lambda-calculus. We develop the metatheory of CLB in call-by-name and in call-by-value, and draw comparisons with applicative bisimulation (due to Abramsky) and logical bisimulation (due to Sangiorgi, Kobayashi and Sumii). We also study enhancements of the bisimulation method for CLB by developing a theory of up-to techniques for cases where the functional corresponding to bisimulation is not necessarily monotone.
△ Less
Submitted 10 October, 2014;
originally announced October 2014.
