Now, I’m wondering how property testing can be used for distributed/consensus algorithms, e.g. something like basic paxos? I wrote a small paxos library and was wondering what property testing here would look like. Here’s my test file so far…
Consensus can be defined as all nodes reaching the same state given a variety of (generated) inputs { in this paxos context, it would probably be time / proposal id and proposal val). I’m guessing that if more sophistication was required you could use PropCheck’s state machine properties to ensure all nodes (acceptors) are in the same state beyond what I currently have.
You could probably generate symbolic calls as the aforementioned book talks about in Chapter 4: Custom Generators e.g. a sequence of function calls that are generated with different proposal ids and values…
(From the book) ===> Testing prop_generators:prop_dict_symb() ..............! Failed: After 15 test(s). {call,dict,store,[-6,8, {call,dict,store,[46,-13, {call,dict,store,[2,-2, {call,dict,store,[22,-2, {call,dict,store,[-12,-2, {call,dict,new,[]}]}]}]}]}]}
Here’s some more on consensus in a popular context these days Consensus
You would possibly have a chance of modelling things like consensus with property-based testing by using stateful generators, which are covered later in the book. I know Chris Meiklejohn has had some success doing fault injection with fancier annotated models, though he eventually reoriented his stuff towards other forms of analysis.
While you can find errors and get more confident that specific execution paths are rather safe, a property test is not exhaustive and never represents an actual proof. Generally for protocols people will prefer to rely on formal specifications (like TLA+) at a higher level.
# Here’s a simple TLA+ specification, representing people trading unique items. Can you find the bug?
People == {"alice", "bob"}
Items == {"ore", "sheep", "brick"}
(* --algorithm trade
variable owner_of \in [Items -> People]
process giveitem \in 1..3 \* up to three possible trades made
variables item \in Items,
owner = owner_of[item],
to \in People,
origin_of_trade \in People
begin Give:
if origin_of_trade = owner then
owner_of[item] := to;
end if;
end process;
end algorithm; *)