Lecture: Distributed Systems: IronFleet - Part 2

Date: 4/12/17

Reading

• Required reading: IronFleet: Proving Practical Distributed Systems Correct, Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Michael Lowell Roberts, Srinath Setty, Brian Zill, SOSP, 2015.
• Optional reading: The Saddest Moment, James Mickens, USENIX ;login, 2013.

Preparation

• Clone a copy of the IronFleet code base: git clone git@github.com:Microsoft/Ironclad.git.

• Make sure you can invoke Dafny, e.g., using the following command line from the ironfleet directory:

./tools/Dafny/Dafny.exe /noNLarith /allowGlobals /z3opt:nlsat.randomize=false /compile:0 /timeLimit:30 /noCheating:1 /autoTriggers:1 /ironDafny src/Dafny/Distributed/Protocol/Lock/RefinementProof/RefinementProof.i.dfy

Exercise

Apply the following changes to the Lock system. All file paths are relative to ironfleet/src/Dafny/Distributed/.

• In Services/Lock/AbstractService.s.dfy, extend the existential inside Service_Next to say that the new lock holder is in fact a new holder; i.e., add:

        && |s.history| > 0
        && new_lock_holder != s.history[|s.history|-1]   

so the complete definition is now:

predicate Service_Next(s:ServiceState, s':ServiceState)
{
       s'.hosts == s.hosts
    && (exists new_lock_holder :: 
            new_lock_holder in s.hosts
         && |s.history| > 0
         && new_lock_holder != s.history[|s.history|-1]   
         && s'.history == s.history + [new_lock_holder])
}

Update the refinement proof to prove that the protocol meets the new specification.

Hints

• The definition of the protocol (in Protocol/Node.i.dfy) will need a small fix.
• DistributedSystem.i.dfy will need a one-line fix
• You may want to make use of and to strengthen the MakeHistory lemma in Protocol/Lock/RefinementProof/RefinementProof.i.dfy.
• You may want a handy property about mod. To get it, modify Protocol/Lock/RefinementProof/RefinementProof.i.dfy. At the top, add include "../../../../Libraries/Math/div.i.dfy". Inside the module declaration, add import opened Math__div_i. Finally, add the following lemma that will likely come in handy:

    lemma mod_identity(x:int, m:int)
        requires m > 1;
        ensures  x % m != (x+1) % m;
    {
        if x % m == (x+1) % m {
            lemma_mod_equivalence(x+1,x, m);
            lemma_mod_is_mod_recursive(1, m);
            assert false;
        }
    }