search

ongardie / raft.tla

TLA+ specification for the Raft consensus algorithm
458 stars 74 forks source link

Add check to AppendEntries #3

Open dricketts opened 8 years ago

dricketts commented 8 years ago

I don't think there's a correctness issue with AppendEntries, but I think there's a simple way to make verification (by proof) easier. In particular, it would be useful to add a check to this line to test if prevLogIndex <= Len(log[i]). I believe that this check is unnecessary, but verifying this adds substantial complexity to the type invariant for the system. Is there any downside to adding the check?

ongardie commented 8 years ago

I suspect this isn't the only change you'll want to make verification easier. Want to just accumulate them locally or in a fork for now?

As to this particular change, I'd expect to see the invariant 1 <= nextIndex[i][*] <= Len(log[i]) + 1 somewhere. I don't think you'll be able to avoid that, right? Perhaps other parts of the spec don't do enough to enforce that (the spec might well be buggy).