Jason Hickey

DISTRIBUTED PROVING WITH ENSEMBLE AND NURPL

Ensemble provides a toolkit for building distributed, fault-tolerant applications that can take advantage of features like parallel computation, distributed resource management, and process migration. Furthermore, the applications can be made robust in the present of process and network failures.

In this seminar, I'll present my experience using Ensemble to distribute the Nurpl-Light logical framework. The system spreads proof computation over multiple processes, which can fail or join a computation at any time without affecting the proof result. The principles used form a failry general model of distributed functional programming, and the model is transparent to the programmer--we use the coding techniques developed over the past decade without change. Current measurements show nearly linear speedup on large problems.

I'll also talk about the security model: this form of distributed computation breaks the abstraction barriers we commonly use to ensure correctness, so we use a model akin to "proof-carrying code." This model has the advtange of providing safety even in the presence of Byzantine behavior.

Site Contents