Dr. TLA+ Series – Byzantine Paxos
In this lecture we will discuss how to tolerate Byzantine faults in achieving consensus. We illustrate through refining Paxos step by step. This should be most fun to those who have become familiar with Paxos-based…
CCI (Common Compiler Infrastructure)
CCI provides a rich infrastructure for working with .NET Assemblies: generating them from source, or rewriting them.
Monadic Second-Order Logic on Finite Sequences
Dijkstra monads for free
44th ACM SIGPLAN Symposium on Principles of Programming Languages
The 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on…
Reducing Faulty Executions of Distributed Systems, MSR Redmond Job Talk
When a bug is found in a long-running distributed system, developers typically start by identifying (i) which events in the execution caused their system to arrive at the unsafe state, and (ii) which events are…
PerfOrator
This project is focused on optimizing the resource usage of bigData jobs. Standard database query optimization focuses on finding the best query execution plan, given fixed hardware resources. In BigData settings, both pay-as-you-go clouds and on-prem shared clusters,…