Calvin Loncaric


GitHub | LinkedIn

Hello! I am a computer scientist.

Today I work at Oracle Cloud Infrastructure with Chris Newcombe doing formal verification for distributed systems. I am also a maintainer for the TLA+ language and tools.

In the past I got a PhD at the University of Washington, where I focused on program synthesis: turning complex programming tasks into simple ones by having the computer write some (or all) of the code automatically. I worked with the programming languages and software engineering group under Michael Ernst.

Blog Posts and Notes

Nitpicky Coding Advice: Use Dataflow and Types for Preconditions
July 2024
One suggestion for mitigating sequential coupling.
Misadventures Recompiling the Java Ecosystem from Source
November 2023
Something is rotten in the state of Maven.
Everything is a Distributed System: Client-Side Consistency During Website Deployments
July 2023
Website deployments run concurrently with visitors' browsers.
The Live Migration Problem
January 2023
Upgrading an existing system in-place is much harder than writing a new one.
You Can't Not Crash (or: Segfaults Shouldn't be Scary)
October 2021
Even the power of full formal verification can't prevent your programs from crashing. This is about learning to live with it.
How to Durably Write a File on POSIX Systems
July 2021
It is remarkably difficult to create a file and also be certain it will surive a power outage.
Arbitrary Choice in SMT-LIB
October 2020
An operator to choose an aribirary value satisfying a predicate can be very useful.
InterruptedException
April 2019
In Java, lots of standard library methods throw InterruptedException. How should programs respond to this exception?
Grokking Unix Permissions
March 2017
If you collaborate with others on a shared filesystem, you will invariably run into permissions problems. Read this to understand why and what you can do about it.

Research

Data Structure Synthesis

High-performance data structures are at the heart of many applications. In our PLDI 2016 paper we describe how to generate complex data structure implementations from high-level specifications. Cozy (our implementation of these techniques) is available online.

Our more recent ICSE 2018 paper improves Cozy by widening the class of data structures it can handle and generalizing the synthesis algorithm to require fewer hard-coded heuristics.

People: Michael Ernst, Emina Torlak, Zhen Zhang, Andrew Tran, David Grant, Haoming Liu, and Daniel Perelman.

Formal Verification of a Neutron Therapy Machine

My group applied formal verification techniques to the Clinical Neutron Therapy System at the UW Medical Center. The CNTS is used for actual cancer treatments, so we want a high degree of confidence that all the code is correct!

Verifying all the CNTS code is challenging since it is built on many different technologies. Our SNAPL 2015 paper describes the need to combine many disparate verification strategies into a cohesive piece of evidence. In our CAV 2016 paper we describe how we actually achieved this for (parts of) CNTS.

People: Jon Jacky, Stuart Pernsteiner, Zach Tatlock, Emina Torlak, Michael Ernst, Dan Grossman, and Xi Wang.

Type Error Diagnosis

Many developers have horror stories of struggling to diagnose type errors in type-inferred languages like ML and Haskell. Recent research promises far more accurate error messages, but the techniques are difficult to implement and slow to run.

Our OOPSLA 2016 paper describes how to achieve comparable quality at substantially lower run-time cost. Even better, our technique can be implemented with only small modifications to a compiler's existing type inference algorithm!

There is also a tech report on this research that expands some details in the OOPSLA paper. In particular, Appendix C gives advice for compiler writers and future researchers. Note that this is my own version of the paper and has not been peer-reviewed. (Last updated 10 October, 2016.)

Our code and evaluation materials are available on request.

People: Satish Chandra, Cole Schlesinger, and Manu Sridharan.

Other Projects

PPPL
August 2021
The Persistent Parallel Programming Language: a language without sequential execution or volatile memory.
Many-SMT
February 2021
An SMT-LIB frontend that runs multiple solvers in parallel.
Angelic Minesweeper
August 2020
Minesweeper, but without any guessing.
EzPSL
January 2020
A pseudocode language that compiles to TLA+ for model checking.
Generator to Iterator Converter
February 2017
Compiles Python-style generator functions to Java-style iterators.
Sketch to UI converter
June 2015
Computer vision class project to convert hand-drawn sketches into user interface code (e.g. HTML).
Coq Plugin for Sublime Text 3
May 2014
A plugin for interacting with the proof assistant Coq in the Sublime text editor.
Marching Tetrahedrons
April 2012
A clean implementation of the marching tetrahedrons algorithm for rendering implicit surfaces.
Mini Lang
February 2012
A language with only three operations.