About 📖

I'm a PhD student in the Systopia and Software Practices labs at the University of British Columbia. My interests relate to programming language design, implementation, and formally modeling systems. I usually target domains that are challenging to program, like concurrent and distributed systems, compilers, interpreters. Often, I work with TLA+.

Models don't need to be one-off, isolated artifacts. With a precise enough model, we can automatically generate an implementation. We can also cross-check real executions against our models, to see if we modeled what the implementation actually does. See below for specific projects, talks, and peer-reviewed publications.

Contact 📡

E-Mail 📧 ≝ [email protected] Github

≝ https://www.github.com/fhackett

Recent Projects 🛠️

OmniLink [ArXiv]: Tool for validating traces of concurrent implementations against high-level specifications in TLA+. We combine TLA+ trace validation and linearizability checking, and extend the combination with a substep linearizability formalism. The resulting validator can check runtime traces with over 500k events against complex TLA+ specifications, and has been evaluated on WiredTiger, Balanced Augmented Trees, and ConcurrentQueue. Collaboration with Yuanhao Wei at UBC and A. Jesse Jiryu Davis at MongoDB.
Specula: Building models requires significant expertise, and can be tedious. This is a barrier to adoption, and limits their usefulness in practice. Specula uses LLMs to infer TLA+ models from implementation code, which can then be used to detect design issues that can neither be detected by existing manual analysis, nor regular LLM bug finding. To mitigate a range of possible hallucinations, the generated models are both model checked and validated against runtime implementation traces, with validation feedback looped back into the LLM generation process. Collaboration with Emilie Ma and several excellent collaborators from Nanjing University and the University of Illinois Urbana-Champaign. Emilie leads the UBC side of the project.
Forja: Current tooling for the TLA+ ecosystem is monolithic, and not well suited for extension. Research projects will usually fork the existing TLA+ tools, and the prototyped changes will be left behind as the main branch evolves. Forja is a mechanism for specifying, rewriting, and validating abstract syntax trees, which we are prototyping as a means to enhance and cross-validate existing tools in the TLA+ space.
PGo: Compiler from distributed system specifications into implementations, translating TLA+ based Modular PlusCal specifications into Go. We used it to build a Raft-based key-value store which outperformed other specification-compiled implementations. There remain open questions about how to go beyond known limitations of specification compilation, and the DCal project, when I return to it, aims to explore some possibilities there. We also used PGo to prototype TraceLink, an automatic instrumentation layer for performing trace validation of systems built with PGo, and a precursor to OmniLink.