BT

IronFleet: A Methodology for Proving Distributed Systems

| by Abel Avram Follow 9 Followers on Dec 29, 2015. Estimated reading time: 1 minute |

A group of researchers from Microsoft has published the paper “IronFleet: Proving Practical Distributed Systems Correct” (PDF) and made available the accompanying source code demonstrating the use of the methodology in machine proving the correctness of a non-trivial distributed system from a safety and liveliness point of view.

Given the difficulty of building correct distributed systems due to the possibility of bugs generated by the parallel execution of code on multiple machines, a Microsoft research team has developed IronFleet, a methodology for automatically verifying such systems. Going beyond specifying and verifying distributed protocols, IronFleet “guarantees” that the implementation of a distributed system satisfies the demands of a centralized specification, ruling out “race conditions, violations of global invariants, integer overflow, disagreements between packet encoding and decoding, and bugs in rarely exercised code paths such as failure recovery.” The aim is to determine if a distributed system is “correct” and it will behave properly at all times.

IronFleet proves both the safety - the correctness of actions performed - and liveliness – the usefulness of the actions - properties of a distributed system. According to the paper, IronFleet does that by the

comprehensive verification of complex distributed systems via a methodology for structuring and writing proofs about them, as well as a collection of generic verified libraries useful for implementing such systems. Structurally, IronFleet’s methodology uses a concurrency containment strategy that blends two distinct verification styles within the same automated theorem-proving framework, preventing any semantic gaps between them. We use TLA-style state-machine refinement [TLA - Temporal Logic of Actions] to reason about protocol-level concurrency, ignoring implementation complexities, then use Floyd-Hoare-style imperative verification to reason about those complexities while ignoring concurrency. To simplify reasoning about concurrency, we impose a machine checked reduction-enabling obligation on the implementation. Finally, we structure our protocols using always-enabled actions to greatly simplify liveliness proofs.

Such systems are written in Dafny, a language and program verification tool used to determine the functional correctness of a program. After verification, the code can be compiled to C# or assembly code to remove any dependence on .NET or Windows. Dafny could be enhanced to compile the code to other languages such as C++.

IronFleet has been used to demonstrate the correctness of IronRSL – a distributed Paxos state machine – and IronKV – a sharded key-value store-. The source code of IronFleet and of the verified systems is available on GitHub.

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT