Parallel & Distributed Operating Systems Group

Past & present projects at PDOS

Current projects

Armada: verifying concurrent storage systems
Armada is a Coq framework for verifying concurrent storage systems. It supports verifying systems written in Go by translating them to Coq to complete the proof using Armada.
Biscuit: An OS kernel in a high-level language

Biscuit is a monolithic, POSIX-subset operating system kernel in Go for x86-64 CPUs. We wrote it to study the performance trade-offs of using a high-level language with garbage collection to implement a kernel with a common style of architecture.

Noria: data-flow for web applications
Noria is an attempt at designing a database specifically tailored for web applications, providing automatic caching, safe and effortless schema migrations, and native support for reactive use.

Past projects

Secure web-application databases
The goal of this line of research is to apply cryptographic techniques practically to secure web application databases and provide strong guarantees against realistic adversaries.
Scalable file system

ScaleFS is a highly scalable file system for the sv6 operating system. The aim is to achieve scalability over many cores and disks.

CSPEC: Concurrency verification with movers
CSPEC is a framework in the Coq proof assistant for proving concurrent software correct using movers. The idea behind movers is to reduce the number of concurrent interleavings the programmer needs to consider. We've used CSPEC to prove a concurrent mail server correct which involves lock-free concurrency control with the file system.
FSCQ: File-system verification
FSCQ is the first file system with a machine-checkable proof (in the Coq proof assistant) that its implementation meets its specification and whose specification includes behavior under crashes.
Multicore scalability

We build and investigate software systems for multicore computers. We have analyzed and fixed scalability problems in existing software, such as the Linux kernel, and built scalable software from scratch, such as RadixVM and the Corey kernel. To facilitate this work and help identify scalability bottlenecks on multicore computers we have built analysis tools, like DProf.

Amber: User-centric cloud storage
A project to collect a users' data in a common, federated storage, to give users control over their data's storage and facilitate better sharing among applications through the use of global, cross-cloud queries.
Chord: Fully decentralized peer-to-peer systems

The Chord project explored how to build scalable, robust distributed systems using peer-to-peer ideas. The basis for much of our work is the Chord distributed hash lookup primitive. Chord is completely decentralized and symmetric, and can find data using only log(N) messages, where N is the number of nodes in the system. Chord’s lookup mechanism is provably robust in the face of frequent node failures and re-joins.

Unmanaged Internet Architecture

UIA is a distributed name system and ad-hoc routing infrastructure which provides zero-configuration connectivity among users’ mobile devices without the use of centralized servers. Each user has a local namespace which is shared among all her devices and is always available on every device. Users can assign personal names to each of their devices, and can also name other users and access their friends’ namespaces. UIA devices automatically maintain connectivity with other named devices, both in ad-hoc networks and in the global Internet when available.