✨ Bootstrap faults

[joaomlneto]

Discussion card on Trello

---

Requesting comments on how to implement the faults. This is a synopsis of what I want to implement.

1. Fault representation OK?
2. When/how to inject faults OK?

---

A Fault is a <Trigger, Behavior> tuple. A Trigger checks whether a given behavior is to be applied. A behavior is something happening outside of the specification of the application.

Some examples of triggers:

• Sender and Recipient are not on same partition
• Sender is node 0
• Message has Round = N
• Destination is one of nodes {0, 2, 4}
• Composition: a combination of triggers via conjunctions/disjunctions/negations.

Some examples of behaviors:

• Drop message
• Kill/Restart node
• Increment round field in message

This should place little to no limits on expressivity and allows for reusability via composition.

---

When to inject faults, the option that makes most sense to me is the following:

Apply faults when a message is queued (captured by the Interceptor and passed through the Translator).

So, after the translator does its thing, we’d pass the message through the faults. Something like this

tm := r.MessageTranslator.Translate(message)
for _, fault := range faults {
  fault.ApplyIfTriggered(message)
}

Since we’re likely to have a small number of faults, the O(N) should be negligible.

[joaomlneto]

Slight but meaningful changes from the above definition.

• A Precondition is a function: state → boolean, free of side-effects.
• A Behavior is a function: state → void, where the faults are injected as side-effects (e.g. invoking processManager.crashNode(0)).

Before Faults were being applied automatically. Now, they are either enabled or disabled. The Scheduler can then decide to schedule these instead of messages: Whenever we invoke Scheduler.Next(actions) from the scheduler, we now also pass the set of enabled faults (the faults that have a true precondition): Scheduler.Next(actions, faults).

The set of faults are configured in the config.yml file. See example.

TODO

• Faults are not being appended to the trace: need to figure out serialization/deserialization. Note to self: piggyback from instantiating faults from the config.
• Their actual behavior has not yet been properly tested; but the logic is mostly all there.
• Not strictly required, but the user should be able to specify fault generators in the config similar to Jepsen, rather than individual faults. For example, currently we have to specify one fault for each node to crash.