How to go about property testing a consensus protocol using PropCheck

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

Super smart people? @adkron @ferd

Just curious..

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.

Much appreciated Fred – quite intriguing!

TLA+ (pronounced as tee ell a plus , /ˈtiː ɛl eɪ plʌs/) is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode,[4] and its use likened to drawing blueprints for software systems;[5] TLA is an acronym for Temporal Logic of Actions.

TLA+ 1
TLA+ 2

# 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; *)

Leslie Lamport strikes again it would seem