arXiv subjects

M. Frans Kaashoek

Publications and source records attributed to M. Frans Kaashoek.

5 recordsLinked to original sources

arXiv2026

Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents

MachCSL is a framework for verifying system software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea behind MachCSL is to adapt concurrent separation logic, based on Iris, to reasoning about low-level hardware execution at the sub-instruction level: page-table translation, TLB, privilege levels, configuration registers, instruction fetch/decode/execute, traps and interrupts, DMA, shared memory, power failures, etc. Reasoning at this level of detail ensures that the system software correctly manages all of the hardware details. Verifying software at this low level of abstraction is tedious, but LLM-based agents are capable of reasoning about such low-level details. As a case study, we verify the xv6 OS kernel (6,657 lines of C and assembly code), which provides a traditional Unix system call interface (processes, file system, file descriptors, and preemptive scheduling) and has substantial internal concurrency (multi-core support with fine-grained locking, shared memory, interrupts, DMA, etc.). In the verification process, we uncovered 11 bugs in the xv6 implementation, as well as one bug in the Sail RISC-V semantics, and one bug in Sail's Lean extraction. The verification effort took us 102 days, including the time to develop the MachCSL framework. On top of the verified xv6 kernel, we prove a theorem about console-level behavior: e.g., if the user types echo hello world as input on the UART console, the only output the system can produce is hello world (if there are no crashes or other errors). This theorem covers both the kernel and the init, sh, echo, cat, grep, sync, and seccomp binaries in the initial file system image.

cs.LO↗

arXiv2026

Fast end-to-end cloud application cold-start with initscripts

Serverless functions are a popular way of deploying cloud applications. Because many of these functions are short- running and experience frequent cold-starts, start latencies often dominate their execution latency. Start latency can be broken down into two components: setup and initialization. Setup involves steps the cloud platform takes when starting an application, such as downloading its binary and creating an isolated execution environment. Initialization involves steps the application takes after it has started running but before it can do useful work, such as connecting to other services, coordinating to claim work, and downloading inputs. This paper contributes initscripts, which provide a script- able interface for developers to specify their application's initialization routine to the cloud platform. The platform can then run an application's initscript and reduce application start latency by overlapping setup and initialization steps. Once the application is up and running, the initscript bootstraps the application by transferring initialization results to it. Using initscripts, we were able to speed up cold-starts of several of the ServerlessBench Python applications by an average 1.67X with no modifications to the application. Initscripts also speed up start times for a serverless image recognition workload by 1.81X, and off-the-shelf microservices like etcd and memcached.

cs.DC↗

arXiv2023

Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)

Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including GroveKV, a realistic distributed multi-threaded key-value store. GroveKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. GroveKV achieves high performance (67-73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2x the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.

cs.LO↗

arXiv2020

Unnatural Language Processing: Bridging the Gap Between Synthetic and Natural Language Data

Large, human-annotated datasets are central to the development of natural language processing models. Collecting these datasets can be the most challenging part of the development process. We address this problem by introducing a general purpose technique for ``simulation-to-real'' transfer in language understanding problems with a delimited set of target behaviors, making it possible to develop models that can interpret natural utterances without natural training data. We begin with a synthetic data generation procedure, and train a model that can accurately interpret utterances produced by the data generator. To generalize to natural utterances, we automatically find projections of natural language utterances onto the support of the synthetic language, using learned sentence embeddings to define a distance metric. With only synthetic training data, our approach matches or outperforms state-of-the-art models trained on natural language data in several domains. These results suggest that simulation-to-real transfer is a practical framework for developing NLP applications, and that improved models for transfer might provide wide-ranging improvements in downstream tasks.

cs.CL↗

arXiv2018

A Revised and Verified Proof of the Scalable Commutativity Rule

This paper explains a flaw in the published proof of the Scalable Commutativity Rule (SCR), presents a revised and formally verified proof of the SCR in the Coq proof assistant, and discusses the insights and open questions raised from our experience proving the SCR.

cs.DC↗