Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Initial transplantation/checkin of message passing & dropping simulator.

  • Loading branch information...
commit 16a0f67dab1dba9cc040ef9f5207e97c082aa86e 0 parents
@slfritchie authored
BIN  rebar
Binary file not shown
4 rebar.config
@@ -0,0 +1,4 @@
+%% -*- mode: erlang;erlang-indent-level: 4;indent-tabs-mode: nil -*-
+%% ex: ts=4 sw=4 ft=erlang et
+
+{cover_enabled, true}.
123 src/distrib_counter_bad1_sim.erl
@@ -0,0 +1,123 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(distrib_counter_bad1_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_counter_op(NumClients, NumServers)).
+
+gen_counter_op(NumClients, NumServers) ->
+ ?LET(ClientI, choose(1, NumClients),
+ {lists:nth(ClientI, all_clients()),
+ {counter_op, lists:sublist(all_servers(), NumServers)}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun counter_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, gen_nat_nat2(5, 1), fun counter_server1/2} || Server <- Servers].
+
+gen_nat_nat2(A, B) ->
+ %% Use nat() A/(A+B) of the time, nat()*nat() B/(A+B) of the time
+ slf_msgsim_qc:gen_nat_nat2(A, B).
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, UTrc) ->
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ NumCrashes = length([x || {process_crash,_,_,_,_,_} <- Trc]),
+ Emitted = [Count || {_Clnt,_Step,{counter,Count}} <- UTrc,
+ Count /= timeout],
+ Steps = slf_msgsim:get_step(Sched1),
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd2 = ~P\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Emitted counters = ~w\n",
+ [F1, F2, Sched1, 250,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Emitted]),
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("sched steps ", Steps,
+ measure("crashes ", NumCrashes,
+ measure("# ops ", length(Ops),
+ measure("# emitted ", length(Emitted),
+ measure("msgs sent ", NumMsgs,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {ops_finish, length(Ops) == length(UTrc)},
+ {emits_unique, length(Emitted) ==
+ length(lists:usort(Emitted))},
+ {not_retro, Emitted == lists:sort(Emitted)}])
+ end))))))))))).
+
+%%% Protocol implementation
+
+%% Known to be flawed: ask each server for its counter, then
+%% choose the max of all responses. The servers are naive
+%% and are not keeping per-key counters but rather a single
+%% counter for the entire server.
+
+counter_client1({counter_op, Servers}, _St) ->
+ [slf_msgsim:bang(Server, {incr_counter, slf_msgsim:self()}) ||
+ Server <- Servers],
+ {recv_timeout, fun counter_client1_reply/2, {Servers, []}}.
+
+counter_client1_reply({incr_counter_reply, Server, Count},
+ {Waiting, Replies})->
+ Replies2 = [{Server, Count}|Replies],
+ case Waiting -- [Server] of
+ [] ->
+ Val = make_val(Replies2),
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused};
+ Waiting2 ->
+ {recv_timeout, same, {Waiting2, Replies2}}
+ end;
+counter_client1_reply(timeout, {Waiting, Replies}) ->
+ Val = if length(Waiting) > length(Replies) ->
+ timeout;
+ true ->
+ make_val(Replies)
+ end,
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused}.
+
+counter_server1({incr_counter, From}, Count) ->
+ slf_msgsim:bang(From, {incr_counter_reply, slf_msgsim:self(), Count}),
+ {recv_general, same, Count + 1}.
+
+make_val(Replies) ->
+ lists:max([Counter || {_Server, Counter} <- Replies]).
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
150 src/distrib_counter_bad1_sim.txt
@@ -0,0 +1,150 @@
+NOTE: Search for %% for hints on what to look for when something goes wrong.
+
+Summary: Found an error: duplicate counters seen by the same client.
+
+(rk@sbb)75> eqc:quickcheck(eqc:numtests(100,slf_msgsim_qc:prop_simulate(distrib_counter_bad1_sim, []))).
+.......................Failed! After 24 tests.
+%% 1 client, 2 servers, 1 key (ignored)
+{1,2,1}
+%% 2 counter ops, both by same client
+{[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad1_sim.5.52918649>}],
+ [{s1,6,#Fun<distrib_counter_bad1_sim.4.5305677>},
+ {s2,5,#Fun<distrib_counter_bad1_sim.4.5305677>}],
+%% Schedule isn't weird
+ [c1,s2,c1,s1],
+%% A single partition between c1 -> s1
+ [{partition,[c1,c1,c1],[s1,s1,s1],4,12}]}
+Failed:
+F1 = {1,2,1}
+F2 = {[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad1_sim.5.52918649>}],
+ [{s1,6,#Fun<distrib_counter_bad1_sim.4.5305677>},
+ {s2,5,#Fun<distrib_counter_bad1_sim.4.5305677>}],
+ [c1,s2,c1,s1],
+ [{partition,[c1,c1,c1],[s1,s1,s1],4,12}]}
+End2 = {sched,15,6,
+ [c1,s2,c1,s1],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad1_sim.5.52918649>,
+ undefined}},
+ {s1,{proc,s1,7,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad1_sim.4.5305677>,
+ undefined}},
+ {s2,{proc,s2,7,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad1_sim.4.5305677>,
+ undefined}}],
+ [{recv,14,scheduler,c1,timeout},
+ {recv,13,s2,c1,{incr_counter_reply,s2,6}},
+ {deliver,12,s2,c1,{incr_counter_reply,s2,6}},
+ {bang,11,s2,c1,{incr_counter_reply,s2,6}},
+ {recv,11,c1,s2,{incr_counter,c1}},
+ {deliver,10,c1,s2,{incr_counter,c1}},
+ {bang,9,c1,s2,{incr_counter,c1}},
+ {drop,9,c1,s1,{incr_counter,c1}},
+ {recv,9,scheduler,c1,{counter_op,[s1,s2]}},
+ {recv,8,s2,c1,{incr_counter_reply,s2,5}},
+ {deliver,7,s2,c1,{incr_counter_reply,s2,5}},
+ {recv,6,s1,c1,{incr_counter_reply,s1,6}},
+ {deliver,5,s1,c1,{incr_counter_reply,s1,6}},
+ {bang,4,s2,c1,{incr_counter_reply,s2,5}},
+ {recv,4,c1,s2,{incr_counter,c1}},
+ {deliver,3,c1,s2,{incr_counter,c1}},
+ {bang,2,s1,c1,{incr_counter_reply,s1,6}},
+ {recv,2,c1,s1,{incr_counter,c1}},
+ {deliver,1,c1,s1,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2]}}],
+ [{c1,14,{counter,6}},{c1,8,{counter,6}}],
+ [{{c1,s1},[4,5,6,7,8,9,10,11,12]}]}
+Runnable = [], Receivable = []
+%% Duplicate counters are bad
+Emitted counters = [6,6]
+runnable: passed
+ops_finish: passed
+%% ... and the emits_unique property caught the duplicates
+emits_unique: failed
+not_retro: passed
+Shrinking.........(9 times)
+{1,2,1}
+%% Same ops with same actors
+{[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad1_sim.5.52918649>}],
+ [{s1,1,#Fun<distrib_counter_bad1_sim.4.5305677>},
+ {s2,0,#Fun<distrib_counter_bad1_sim.4.5305677>}],
+%% Scheduler simplified slightly
+ [s1,c1,s2],
+%% The length of the c1 -> s1 partition shortened slightly.
+ [{partition,[c1],[s1],1,9}]}
+Failed:
+F1 = {1,2,1}
+F2 = {[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad1_sim.5.52918649>}],
+%% Server s1 starts with counter = 1
+%% Server s2 starts with counter = 0
+ [{s1,1,#Fun<distrib_counter_bad1_sim.4.5305677>},
+ {s2,0,#Fun<distrib_counter_bad1_sim.4.5305677>}],
+ [s1,c1,s2],
+%% The network partition will interfere with c1's second request, look
+%% for the timeout that it receives at the end of the trace.
+ [{partition,[c1],[s1],1,9}]}
+End2 = {sched,15,6,
+ [s1,c1,s2],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad1_sim.5.52918649>,
+ undefined}},
+ {s1,{proc,s1,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad1_sim.4.5305677>,
+ undefined}},
+ {s2,{proc,s2,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad1_sim.4.5305677>,
+ undefined}}],
+%% This is the scheduler trace, in reverse order. Note that the
+%% partition has caused a timeout at simulated time = 14.
+ [{recv,14,scheduler,c1,timeout},
+ {recv,13,s2,c1,{incr_counter_reply,s2,1}},
+ {deliver,12,s2,c1,{incr_counter_reply,s2,1}},
+ {bang,11,s2,c1,{incr_counter_reply,s2,1}},
+ {recv,11,c1,s2,{incr_counter,c1}},
+ {deliver,10,c1,s2,{incr_counter,c1}},
+ {bang,9,c1,s2,{incr_counter,c1}},
+ {drop,9,c1,s1,{incr_counter,c1}},
+ {recv,9,scheduler,c1,{counter_op,[s1,s2]}},
+ {recv,8,s2,c1,{incr_counter_reply,s2,0}},
+ {deliver,7,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,6,s1,c1,{incr_counter_reply,s1,1}},
+ {deliver,5,s1,c1,{incr_counter_reply,s1,1}},
+ {bang,4,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,4,c1,s2,{incr_counter,c1}},
+ {deliver,3,c1,s2,{incr_counter,c1}},
+ {bang,2,s1,c1,{incr_counter_reply,s1,1}},
+ {recv,2,c1,s1,{incr_counter,c1}},
+ {deliver,1,c1,s1,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2]}}],
+%% This is the user trace, in reverse order. After the timeout,
+%% client c1 uses the single reply that it received (at time = 12)
+%% and emits a duplicate counter.
+ [{c1,14,{counter,1}},{c1,8,{counter,1}}],
+ [{{c1,s1},[1,2,3,4,5,6,7,8,9]}]}
+Runnable = [], Receivable = []
+%% Bummer, non-unique counters
+Emitted counters = [1,1]
+emits_unique: failed
+false
135 src/distrib_counter_bad2_sim.erl
@@ -0,0 +1,135 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(distrib_counter_bad2_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_counter_op(NumClients, NumServers)).
+
+gen_counter_op(NumClients, NumServers) ->
+ ?LET(ClientI, choose(1, NumClients),
+ {lists:nth(ClientI, all_clients()),
+ {counter_op, lists:sublist(all_servers(), NumServers)}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun counter_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, gen_nat_nat2(5, 1), fun counter_server1/2} || Server <- Servers].
+
+gen_nat_nat2(A, B) ->
+ %% Use nat() A/(A+B) of the time, nat()*nat() B/(A+B) of the time
+ slf_msgsim_qc:gen_nat_nat2(A, B).
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, UTrc) ->
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ NumCrashes = length([x || {process_crash,_,_,_,_,_} <- Trc]),
+ Emitted = [Count || {_Clnt,_Step,{counter,Count}} <- UTrc,
+ Count /= timeout],
+ Steps = slf_msgsim:get_step(Sched1),
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd2 = ~P\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Emitted counters = ~p\n",
+ [F1, F2, Sched1, 250,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Emitted]),
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("sched steps ", Steps,
+ measure("crashes ", NumCrashes,
+ measure("# ops ", length(Ops),
+ measure("# emitted ", length(Emitted),
+ measure("msgs sent ", NumMsgs,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {ops_finish, length(Ops) == length(UTrc)},
+ {emits_unique, length(Emitted) ==
+ length(lists:usort(Emitted))},
+ {not_retro, Emitted == lists:sort(Emitted)}])
+ end))))))))))).
+
+%%% Protocol implementation
+
+%% Known to be flawed: ask each server for its counter, then
+%% choose the max of all responses. The servers are naive
+%% and are not keeping per-key counters but rather a single
+%% counter for the entire server.
+
+counter_client1({counter_op, Servers}, _St) ->
+ [slf_msgsim:bang(Server, {incr_counter, slf_msgsim:self()}) ||
+ Server <- Servers],
+ {recv_timeout, fun counter_client1_reply/2, {Servers, []}}.
+
+counter_client1_reply({incr_counter_reply, Server, Count},
+ {Waiting, Replies})->
+ Replies2 = [{Server, Count}|Replies],
+ case Waiting -- [Server] of
+ [] ->
+ Val = make_val(Replies2),
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused};
+ Waiting2 ->
+ {recv_timeout, same, {Waiting2, Replies2}}
+ end;
+counter_client1_reply(timeout, {Waiting, Replies}) ->
+ Val = if length(Waiting) > length(Replies) ->
+ timeout;
+ true ->
+ make_val(Replies)
+ end,
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused}.
+
+counter_server1({incr_counter, From}, Count) ->
+ slf_msgsim:bang(From, {incr_counter_reply, slf_msgsim:self(), Count}),
+ {recv_general, same, Count + 1}.
+
+make_val(Replies) ->
+ Ns = [N || {_Server, N} <- Replies],
+ ByN = lists:sort([{N, Server} || {Server, N} <- Replies]),
+ SvrOrder = [Server || {_N, Server} <- ByN],
+ LHS_int = lists:max(Ns),
+ Left = integer_to_list(LHS_int),
+ Right = make_suffix(SvrOrder),
+ Left ++ "." ++ Right.
+
+make_suffix(ReplyServers) ->
+ lists:append(make_suffix2(ReplyServers)).
+
+make_suffix2(ReplyServers) ->
+ [atom_to_list(Svr) || Svr <- ReplyServers].
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
274 src/distrib_counter_bad2_sim.txt
@@ -0,0 +1,274 @@
+NOTE: Search for %% for hints on what to look for when something goes wrong.
+
+Difference with distrib_counter_bad1_sim.erl:
+
+This time we try to convert the counter that the client emits as a
+fake floating point number, then calculate the two sides of the
+decimal point differently:
+
+ lefthand side: Use the maximum of all server responses
+ righthand side: Use the order in which the server responses return
+ to use to create a fraction-like thing that we
+ append to the righthand side of the decimal. This
+ suffix attempts to give a global ordering in cases
+ when clients emit what would otherwise be the same
+ counter.
+
+This scheme could be used to create an string that could be converted
+to a real floating point number, but we are lazy and do not perform
+that extra step.
+
+Summary: Unfortunately, it doesn't work. This time we found a
+ counterexample where the lefthand side of the fake floating
+ point number goes backward.
+
+(rk@sbb)100> eqc:quickcheck(slf_msgsim_qc:prop_simulate(distrib_counter_bad2_sim, [])).
+...................Failed! After 20 tests.
+%% 5 clients, 3 servers, 1 key (ignored)
+{5,3,1}
+%% 2 ops by two different clients
+{[{c2,{counter_op,[s1,s2,s3]}},{c4,{counter_op,[s1,s2,s3]}}],
+ [{c1,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c2,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c3,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c4,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c5,[],#Fun<distrib_counter_bad2_sim.5.52918649>}],
+%% Server s1 starts with counter = 4
+%% Server s2 starts with counter = 3
+%% Server s3 starts with counter = 6
+ [{s1,4,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s2,3,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s3,6,#Fun<distrib_counter_bad2_sim.4.5305677>}],
+%% Scheduler isn't crazy
+ [c1,c3,c4,c2,c5,s1,s2,s3],
+%% No effective partitions because source or dest sets is empty
+ [{partition,[],[s1,s3],0,3},
+ {partition,[s1,s3],[],0,3},
+ {partition,[],[s2],4,4},
+ {partition,[s2],[],4,4}]}
+Failed:
+F1 = {5,3,1}
+F2 = {[{c2,{counter_op,[s1,s2,s3]}},{c4,{counter_op,[s1,s2,s3]}}],
+ [{c1,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c2,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c3,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c4,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c5,[],#Fun<distrib_counter_bad2_sim.5.52918649>}],
+ [{s1,4,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s2,3,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s3,6,#Fun<distrib_counter_bad2_sim.4.5305677>}],
+ [c1,c3,c4,c2,c5,s1,s2,s3],
+ [{partition,[],[s1,s3],0,3},
+ {partition,[s1,s3],[],0,3},
+ {partition,[],[s2],4,4},
+ {partition,[s2],[],4,4}]}
+End2 = {sched,26,12,
+ [c1,c3,c4,c2,c5,s1,s2,s3],
+ [],
+%% End states for each process, not exciting
+ [{c1,{proc,c1,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c2,{proc,c2,unused,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c3,{proc,c3,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c4,{proc,c4,unused,[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c5,{proc,c5,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {s1,{proc,s1,6,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.4.5305677>,
+ undefined}},
+ {s2,{proc,s2,5,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.4.5305677>,
+ undefined}},
+ {s3,{proc,s3,8,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.4.5305677>,
+ undefined}}],
+%% System trace, in reverse order
+ [{recv,25,s2,c2,{incr_counter_reply,s2,4}},
+ {recv,24,s3,c4,{incr_counter_reply,s3,7}},
+ {deliver,23,s3,c4,{incr_counter_reply,s3,7}},
+ {recv,22,s3,c2,{incr_counter_reply,s3,6}},
+ {bang,21,s3,c4,{incr_counter_reply,s3,7}},
+ {recv,21,c4,s3,{incr_counter,c4}},
+ {deliver,20,s2,c2,{incr_counter_reply,s2,4}},
+ {recv,19,s1,c2,{incr_counter_reply,s1,5}},
+ {deliver,18,c4,s3,{incr_counter,c4}},
+ {deliver,17,s3,c2,{incr_counter_reply,s3,6}},
+ {bang,16,s2,c2,{incr_counter_reply,s2,4}},
+ {recv,16,c2,s2,{incr_counter,c2}},
+ {deliver,15,s1,c2,{incr_counter_reply,s1,5}},
+ {recv,14,s2,c4,{incr_counter_reply,s2,3}},
+ {bang,13,s3,c2,{incr_counter_reply,s3,6}},
+ {recv,13,c2,s3,{incr_counter,c2}},
+ {deliver,12,s2,c4,{incr_counter_reply,s2,3}},
+ {bang,11,s1,c2,{incr_counter_reply,s1,5}},
+ {recv,11,c2,s1,{incr_counter,c2}},
+ {deliver,10,c2,s3,{incr_counter,c2}},
+ {recv,9,s1,c4,{incr_counter_reply,s1,4}},
+ {bang,8,s2,c4,{incr_counter_reply,s2,3}},
+ {recv,8,c4,s2,{incr_counter,c4}},
+ {deliver,7,s1,c4,{incr_counter_reply,s1,4}},
+ {deliver,6,c2,s2,{incr_counter,c2}},
+ {deliver,5,c4,s2,{incr_counter,c4}},
+ {bang,4,s1,c4,{incr_counter_reply,s1,4}},
+ {recv,4,c4,s1,{incr_counter,c4}},
+ {deliver,3,c2,s1,{incr_counter,c2}},
+ {deliver,2,c4,s1,{incr_counter,c4}},
+ {bang,1,c2,s3,{incr_counter,c2}},
+ {bang,1,c2,s2,{incr_counter,c2}},
+ {bang,1,c2,s1,{incr_counter,c2}},
+ {recv,1,scheduler,c2,{counter_op,[s1,s2,s3]}},
+ {bang,0,c4,s3,{incr_counter,c4}},
+ {bang,0,c4,s2,{incr_counter,c4}},
+ {bang,0,c4,s1,{incr_counter,c4}},
+ {recv,0,scheduler,c4,{counter_op,[s1,s2,s3]}}],
+%% User trace, in reverse order
+ [{c2,25,{counter,"6.s2s1s3"}},{c4,24,{counter,"7.s2s1s3"}}],
+ []}
+Runnable = [], Receivable = []
+Emitted counters = ["7.s2s1s3","6.s2s1s3"]
+runnable: passed
+ops_finish: passed
+emits_unique: passed
+%% Yup, our pseudo-floating point counters go backward
+not_retro: failed
+%% Hooray, I *love* shrinking
+Shrinking..........(10 times)
+%% Number of clients & servers & keys is the same, due to shrinking limitations
+{4,3,1}
+%% Still 2 ops, one by two different clients, though their client
+%% names have been shrunk.
+{[{c1,{counter_op,[s1,s2,s3]}},{c2,{counter_op,[s1,s2,s3]}}],
+ [{c1,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c2,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c3,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c4,[],#Fun<distrib_counter_bad2_sim.5.52918649>}],
+%% Different initial counters for the servers
+%% Server s1 starts with counter = 0
+%% Server s2 starts with counter = 0
+%% Server s3 starts with counter = 1
+ [{s1,0,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s2,0,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s3,1,#Fun<distrib_counter_bad2_sim.4.5305677>}],
+%% Same scheduler, except with client c5 removed (but c5 also does nothing)
+ [c1,c3,c4,c2,s1,s2,s3],
+%% No network partitions
+ [{partition,[],[],0,0},{partition,[],[],0,0}]}
+Failed:
+F1 = {4,3,1}
+F2 = {[{c1,{counter_op,[s1,s2,s3]}},{c2,{counter_op,[s1,s2,s3]}}],
+ [{c1,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c2,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c3,[],#Fun<distrib_counter_bad2_sim.5.52918649>},
+ {c4,[],#Fun<distrib_counter_bad2_sim.5.52918649>}],
+ [{s1,0,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s2,0,#Fun<distrib_counter_bad2_sim.4.5305677>},
+ {s3,1,#Fun<distrib_counter_bad2_sim.4.5305677>}],
+ [c1,c3,c4,c2,s1,s2,s3],
+ [{partition,[],[],0,0},{partition,[],[],0,0}]}
+End2 = {sched,26,12,
+ [c1,c3,c4,c2,s1,s2,s3],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c2,{proc,c2,unused,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c3,{proc,c3,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {c4,{proc,c4,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad2_sim.5.52918649>,
+ undefined}},
+ {s1,{proc,s1,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.4.5305677>,
+ undefined}},
+ {s2,{proc,s2,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.4.5305677>,
+ undefined}},
+ {s3,{proc,s3,3,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad2_sim.4.5305677>,
+ undefined}}],
+ [{recv,25,s2,c2,{incr_counter_reply,s2,1}},
+ {recv,24,s3,c1,{incr_counter_reply,s3,2}},
+ {deliver,23,s3,c1,{incr_counter_reply,s3,2}},
+ {recv,22,s3,c2,{incr_counter_reply,s3,1}},
+ {bang,21,s3,c1,{incr_counter_reply,s3,2}},
+ {recv,21,c1,s3,{incr_counter,c1}},
+ {deliver,20,s2,c2,{incr_counter_reply,s2,1}},
+ {recv,19,s1,c2,{incr_counter_reply,s1,1}},
+ {deliver,18,c1,s3,{incr_counter,c1}},
+ {deliver,17,s3,c2,{incr_counter_reply,s3,1}},
+ {bang,16,s2,c2,{incr_counter_reply,s2,1}},
+ {recv,16,c2,s2,{incr_counter,c2}},
+ {deliver,15,s1,c2,{incr_counter_reply,s1,1}},
+ {recv,14,s2,c1,{incr_counter_reply,s2,0}},
+ {bang,13,s3,c2,{incr_counter_reply,s3,1}},
+ {recv,13,c2,s3,{incr_counter,c2}},
+ {deliver,12,s2,c1,{incr_counter_reply,s2,0}},
+ {bang,11,s1,c2,{incr_counter_reply,s1,1}},
+ {recv,11,c2,s1,{incr_counter,c2}},
+ {deliver,10,c2,s3,{incr_counter,c2}},
+ {recv,9,s1,c1,{incr_counter_reply,s1,0}},
+ {bang,8,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,8,c1,s2,{incr_counter,c1}},
+ {deliver,7,s1,c1,{incr_counter_reply,s1,0}},
+ {deliver,6,c2,s2,{incr_counter,c2}},
+ {deliver,5,c1,s2,{incr_counter,c1}},
+ {bang,4,s1,c1,{incr_counter_reply,s1,0}},
+ {recv,4,c1,s1,{incr_counter,c1}},
+ {deliver,3,c2,s1,{incr_counter,c2}},
+ {deliver,2,c1,s1,{incr_counter,c1}},
+ {bang,1,c2,s3,{incr_counter,c2}},
+ {bang,1,c2,s2,{incr_counter,c2}},
+ {bang,1,c2,s1,{incr_counter,c2}},
+ {recv,1,scheduler,c2,{counter_op,[s1,s2,s3]}},
+ {bang,0,c1,s3,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2,s3]}}],
+ [{c2,25,{counter,"1.s1s2s3"}},{c1,24,{counter,"2.s1s2s3"}}],
+ []}
+Runnable = [], Receivable = []
+%% Yup, still retrograde counters.
+Emitted counters = ["2.s1s2s3","1.s1s2s3"]
+not_retro: failed
+false
143 src/distrib_counter_bad3_sim.erl
@@ -0,0 +1,143 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(distrib_counter_bad3_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_counter_op(NumClients, NumServers)).
+
+gen_counter_op(NumClients, NumServers) ->
+ ?LET(ClientI, choose(1, NumClients),
+ {lists:nth(ClientI, all_clients()),
+ {counter_op, lists:sublist(all_servers(), NumServers)}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun counter_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, gen_nat_nat2(5, 1), fun counter_server1/2} || Server <- Servers].
+
+gen_nat_nat2(A, B) ->
+ %% Use nat() A/(A+B) of the time, nat()*nat() B/(A+B) of the time
+ slf_msgsim_qc:gen_nat_nat2(A, B).
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, UTrc) ->
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ NumCrashes = length([x || {process_crash,_,_,_,_,_} <- Trc]),
+ Emitted = [Count || {_Clnt,_Step,{counter,Count}} <- UTrc,
+ Count /= timeout],
+ Steps = slf_msgsim:get_step(Sched1),
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ F_retro = fun(Clnt) ->
+ L = [Count || {Cl,_Step,{counter, Count}} <- UTrc,
+ Count /= timeout, Cl == Clnt],
+ %% Retrograde counter?
+ L /= lists:usort(L)
+ end,
+ ClientRetroP = lists:any(F_retro, Clients),
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd2 = ~P\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Emitted counters = ~p\n",
+ [F1, F2, Sched1, 250,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Emitted]),
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("sched steps ", Steps,
+ measure("crashes ", NumCrashes,
+ measure("# ops ", length(Ops),
+ measure("# emitted ", length(Emitted),
+ measure("msgs sent ", NumMsgs,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {ops_finish, length(Ops) == length(UTrc)},
+ {emits_unique, length(Emitted) ==
+ length(lists:usort(Emitted))},
+ {per_client_not_retro, not ClientRetroP}])
+ end))))))))))).
+
+%%% Protocol implementation
+
+%% Known to be flawed: ask each server for its counter, then
+%% choose the max of all responses. The servers are naive
+%% and are not keeping per-key counters but rather a single
+%% counter for the entire server.
+
+counter_client1({counter_op, Servers}, _St) ->
+ [slf_msgsim:bang(Server, {incr_counter, slf_msgsim:self()}) ||
+ Server <- Servers],
+ {recv_timeout, fun counter_client1_reply/2, {Servers, []}}.
+
+counter_client1_reply({incr_counter_reply, Server, Count},
+ {Waiting, Replies})->
+ Replies2 = [{Server, Count}|Replies],
+ case Waiting -- [Server] of
+ [] ->
+ Val = make_val(Replies2),
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused};
+ Waiting2 ->
+ {recv_timeout, same, {Waiting2, Replies2}}
+ end;
+counter_client1_reply(timeout, {Waiting, Replies}) ->
+ Val = if length(Waiting) > length(Replies) ->
+ timeout;
+ true ->
+ make_val(Replies)
+ end,
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused}.
+
+counter_server1({incr_counter, From}, Count) ->
+ slf_msgsim:bang(From, {incr_counter_reply, slf_msgsim:self(), Count}),
+ {recv_general, same, Count + 1}.
+
+make_val(Replies) ->
+ Ns = [N || {_Server, N} <- Replies],
+ ByN = lists:sort([{N, Server} || {Server, N} <- Replies]),
+ SvrOrder = [Server || {_N, Server} <- ByN],
+ LHS_int = lists:max(Ns),
+ Left = integer_to_list(LHS_int),
+ Right = make_suffix(SvrOrder),
+ Left ++ "." ++ Right.
+
+make_suffix(ReplyServers) ->
+ lists:append(make_suffix2(ReplyServers)).
+
+make_suffix2(ReplyServers) ->
+ [atom_to_list(Svr) || Svr <- ReplyServers].
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
263 src/distrib_counter_bad3_sim.txt
@@ -0,0 +1,263 @@
+NOTE: Search for %% for hints on what to look for when something goes wrong.
+
+Difference with distrib_counter_bad2_sim.erl:
+
+The previous flawed protocol, #2, showed that the current protocol
+can't keep clients that act at roughly the same time from emitting
+counters that do not go backward when interpreted by *wall clock*
+time.
+
+So, we change the nature of the verification: we check to make certain
+that each client never sees its own counters go backward.
+
+This change of model means that we now acknowledge that the actual
+client<->server protocol cannot provide strictly increasing counters
+across multiple clients as seen/interpreted by wall clock time.
+
+Let us now see if the protocol is sufficient to provide strictly
+increasing counters to individual clients.
+
+Summary: Unfortunately, there's another problem: our fake floating
+ point numbers do not collate as we expect. "9.anything" will
+ always be larger than "10.anything". A single client gets
+ counters in order of "9.something" and "10.something", which
+ violates our strictly increasing property.
+
+(rk@sbb)114> eqc:quickcheck(slf_msgsim_qc:prop_simulate(distrib_counter_bad3_sim, [])).
+...................................Failed! After 36 tests.
+%% 1 client, 4 servers, 1 key (ignored)
+{1,4,1}
+%% 2 ops by one client
+{[{c1,{counter_op,[s1,s2,s3,s4]}},{c1,{counter_op,[s1,s2,s3,s4]}}],
+ [{c1,[],#Fun<distrib_counter_bad3_sim.6.52918649>}],
+%% Server s1 starts with counter = 3
+%% Server s2 starts with counter = 6
+%% Server s3 starts with counter = 7
+%% Server s4 starts with counter = 9
+ [{s1,3,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s2,6,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s3,7,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s4,9,#Fun<distrib_counter_bad3_sim.5.5305677>}],
+%% Scheduler isn't crazy
+ [c1,s1,s2,s3,s4],
+%% One effective network partition (both source & dest sets are non-empty)
+ [{partition,[],[],10,15},
+ {partition,[c1,c1,c1,c1],[s1],1,1},
+ {partition,[s4,s4,s2,s3],[],9,19},
+ {partition,[],[s3],3,10},
+ {partition,[s3],[],3,10}]}
+Failed:
+F1 = {1,4,1}
+F2 = {[{c1,{counter_op,[s1,s2,s3,s4]}},{c1,{counter_op,[s1,s2,s3,s4]}}],
+ [{c1,[],#Fun<distrib_counter_bad3_sim.6.52918649>}],
+ [{s1,3,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s2,6,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s3,7,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s4,9,#Fun<distrib_counter_bad3_sim.5.5305677>}],
+ [c1,s1,s2,s3,s4],
+ [{partition,[],[],10,15},
+ {partition,[c1,c1,c1,c1],[s1],1,1},
+ {partition,[s4,s4,s2,s3],[],9,19},
+ {partition,[],[s3],3,10},
+ {partition,[s3],[],3,10}]}
+End2 = {sched,34,16,
+ [c1,s1,s2,s3,s4],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad3_sim.6.52918649>,
+ undefined}},
+ {s1,{proc,s1,5,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}},
+ {s2,{proc,s2,8,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}},
+ {s3,{proc,s3,9,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}},
+ {s4,{proc,s4,11,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}}],
+ [{recv,33,s4,c1,{incr_counter_reply,s4,10}},
+ {deliver,32,s4,c1,{incr_counter_reply,s4,10}},
+ {recv,31,s3,c1,{incr_counter_reply,s3,8}},
+ {bang,30,s4,c1,{incr_counter_reply,s4,10}},
+ {recv,30,c1,s4,{incr_counter,c1}},
+ {deliver,29,s3,c1,{incr_counter_reply,s3,8}},
+ {deliver,28,c1,s4,{incr_counter,c1}},
+ {bang,27,s3,c1,{incr_counter_reply,s3,8}},
+ {recv,27,c1,s3,{incr_counter,c1}},
+ {deliver,26,c1,s3,{incr_counter,c1}},
+ {recv,25,s2,c1,{incr_counter_reply,s2,7}},
+ {deliver,24,s2,c1,{incr_counter_reply,s2,7}},
+ {recv,23,s1,c1,{incr_counter_reply,s1,4}},
+ {bang,22,s2,c1,{incr_counter_reply,s2,7}},
+ {recv,22,c1,s2,{incr_counter,c1}},
+ {deliver,21,s1,c1,{incr_counter_reply,s1,4}},
+ {deliver,20,c1,s2,{incr_counter,c1}},
+ {bang,19,s1,c1,{incr_counter_reply,s1,4}},
+ {recv,19,c1,s1,{incr_counter,c1}},
+ {deliver,18,c1,s1,{incr_counter,c1}},
+ {bang,17,c1,s4,{incr_counter,c1}},
+ {bang,17,c1,s3,{incr_counter,c1}},
+ {bang,17,c1,s2,{incr_counter,c1}},
+ {bang,17,c1,s1,{incr_counter,c1}},
+ {recv,17,scheduler,c1,{counter_op,[s1,s2,s3,s4]}},
+ {recv,16,s4,c1,{incr_counter_reply,s4,9}},
+ {deliver,15,s4,c1,{incr_counter_reply,s4,9}},
+ {recv,14,s3,c1,{incr_counter_reply,s3,7}},
+ {bang,13,s4,c1,{incr_counter_reply,s4,9}},
+ {recv,13,c1,s4,{incr_counter,c1}},
+ {deliver,12,s3,c1,{incr_counter_reply,s3,7}},
+ {deliver,11,c1,s4,{incr_counter,c1}},
+ {bang,10,s3,c1,{incr_counter_reply,s3,7}},
+ {recv,10,c1,s3,{incr_counter,c1}},
+ {deliver,9,c1,s3,{incr_counter,c1}},
+ {recv,8,s2,c1,{incr_counter_reply,s2,6}},
+ {deliver,7,s2,c1,{incr_counter_reply,s2,6}},
+ {recv,6,s1,c1,{incr_counter_reply,s1,3}},
+ {bang,5,s2,c1,{incr_counter_reply,s2,6}},
+ {recv,5,c1,s2,{incr_counter,c1}},
+ {deliver,4,s1,c1,{incr_counter_reply,s1,3}},
+ {deliver,3,c1,s2,{incr_counter,c1}},
+ {bang,2,s1,c1,{incr_counter_reply,s1,3}},
+ {recv,2,c1,s1,{incr_counter,c1}},
+ {deliver,1,c1,s1,{incr_counter,c1}},
+ {bang,0,c1,s4,{incr_counter,c1}},
+ {bang,0,c1,s3,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2,s3,s4]}}],
+ [{c1,33,{counter,"10.s1s2s3s4"}},{c1,16,{counter,"9.s1s2s3s4"}}],
+ [{{c1,s1},[1]}]}
+Runnable = [], Receivable = []
+Emitted counters = ["9.s1s2s3s4","10.s1s2s3s4"]
+runnable: passed
+ops_finish: passed
+emits_unique: passed
+%% Bummer
+per_client_not_retro: failed
+%% I just love shrinking....
+Shrinking.......(7 times)
+%% Number of clients & servers & keys is the same, due to shrinking limitations
+{1,4,1}
+%% Same ops
+{[{c1,{counter_op,[s1,s2,s3,s4]}},{c1,{counter_op,[s1,s2,s3,s4]}}],
+ [{c1,[],#Fun<distrib_counter_bad3_sim.6.52918649>}],
+%% Server s1 starts with counter = 0
+%% Server s2 starts with counter = 0
+%% Server s3 starts with counter = 0
+%% Server s4 starts with counter = 9
+ [{s1,0,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s2,0,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s3,0,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s4,9,#Fun<distrib_counter_bad3_sim.5.5305677>}],
+%% Same scheduler
+ [c1,s1,s2,s3,s4],
+%% No partitions
+ [{partition,[],[],0,0}]}
+Failed:
+F1 = {1,4,1}
+F2 = {[{c1,{counter_op,[s1,s2,s3,s4]}},{c1,{counter_op,[s1,s2,s3,s4]}}],
+ [{c1,[],#Fun<distrib_counter_bad3_sim.6.52918649>}],
+ [{s1,0,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s2,0,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s3,0,#Fun<distrib_counter_bad3_sim.5.5305677>},
+ {s4,9,#Fun<distrib_counter_bad3_sim.5.5305677>}],
+ [c1,s1,s2,s3,s4],
+ [{partition,[],[],0,0}]}
+End2 = {sched,34,16,
+ [c1,s1,s2,s3,s4],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad3_sim.6.52918649>,
+ undefined}},
+ {s1,{proc,s1,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}},
+ {s2,{proc,s2,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}},
+ {s3,{proc,s3,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}},
+ {s4,{proc,s4,11,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad3_sim.5.5305677>,
+ undefined}}],
+ [{recv,33,s4,c1,{incr_counter_reply,s4,10}},
+ {deliver,32,s4,c1,{incr_counter_reply,s4,10}},
+ {recv,31,s3,c1,{incr_counter_reply,s3,1}},
+ {bang,30,s4,c1,{incr_counter_reply,s4,10}},
+ {recv,30,c1,s4,{incr_counter,c1}},
+ {deliver,29,s3,c1,{incr_counter_reply,s3,1}},
+ {deliver,28,c1,s4,{incr_counter,c1}},
+ {bang,27,s3,c1,{incr_counter_reply,s3,1}},
+ {recv,27,c1,s3,{incr_counter,c1}},
+ {deliver,26,c1,s3,{incr_counter,c1}},
+ {recv,25,s2,c1,{incr_counter_reply,s2,1}},
+ {deliver,24,s2,c1,{incr_counter_reply,s2,1}},
+ {recv,23,s1,c1,{incr_counter_reply,s1,1}},
+ {bang,22,s2,c1,{incr_counter_reply,s2,1}},
+ {recv,22,c1,s2,{incr_counter,c1}},
+ {deliver,21,s1,c1,{incr_counter_reply,s1,1}},
+ {deliver,20,c1,s2,{incr_counter,c1}},
+ {bang,19,s1,c1,{incr_counter_reply,s1,1}},
+ {recv,19,c1,s1,{incr_counter,c1}},
+ {deliver,18,c1,s1,{incr_counter,c1}},
+ {bang,17,c1,s4,{incr_counter,c1}},
+ {bang,17,c1,s3,{incr_counter,c1}},
+ {bang,17,c1,s2,{incr_counter,c1}},
+ {bang,17,c1,s1,{incr_counter,c1}},
+ {recv,17,scheduler,c1,{counter_op,[s1,s2,s3,s4]}},
+ {recv,16,s4,c1,{incr_counter_reply,s4,9}},
+ {deliver,15,s4,c1,{incr_counter_reply,s4,9}},
+ {recv,14,s3,c1,{incr_counter_reply,s3,0}},
+ {bang,13,s4,c1,{incr_counter_reply,s4,9}},
+ {recv,13,c1,s4,{incr_counter,c1}},
+ {deliver,12,s3,c1,{incr_counter_reply,s3,0}},
+ {deliver,11,c1,s4,{incr_counter,c1}},
+ {bang,10,s3,c1,{incr_counter_reply,s3,0}},
+ {recv,10,c1,s3,{incr_counter,c1}},
+ {deliver,9,c1,s3,{incr_counter,c1}},
+ {recv,8,s2,c1,{incr_counter_reply,s2,0}},
+ {deliver,7,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,6,s1,c1,{incr_counter_reply,s1,0}},
+ {bang,5,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,5,c1,s2,{incr_counter,c1}},
+ {deliver,4,s1,c1,{incr_counter_reply,s1,0}},
+ {deliver,3,c1,s2,{incr_counter,c1}},
+ {bang,2,s1,c1,{incr_counter_reply,s1,0}},
+ {recv,2,c1,s1,{incr_counter,c1}},
+ {deliver,1,c1,s1,{incr_counter,c1}},
+ {bang,0,c1,s4,{incr_counter,c1}},
+ {bang,0,c1,s3,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2,s3,s4]}}],
+ [{c1,33,{counter,"10.s1s2s3s4"}},{c1,16,{counter,"9.s1s2s3s4"}}],
+ []}
+Runnable = [], Receivable = []
+%% Bummer again
+Emitted counters = ["9.s1s2s3s4","10.s1s2s3s4"]
+per_client_not_retro: failed
+false
153 src/distrib_counter_bad4_sim.erl
@@ -0,0 +1,153 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(distrib_counter_bad4_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_counter_op(NumClients, NumServers)).
+
+gen_counter_op(NumClients, NumServers) ->
+ ?LET(ClientI, choose(1, NumClients),
+ {lists:nth(ClientI, all_clients()),
+ {counter_op, lists:sublist(all_servers(), NumServers)}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun counter_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, gen_nat_nat2(5, 1), fun counter_server1/2} || Server <- Servers].
+
+gen_nat_nat2(A, B) ->
+ %% Use nat() A/(A+B) of the time, nat()*nat() B/(A+B) of the time
+ slf_msgsim_qc:gen_nat_nat2(A, B).
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, UTrc) ->
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ NumCrashes = length([x || {process_crash,_,_,_,_,_} <- Trc]),
+ Emitted = [Count || {_Clnt,_Step,{counter,Count}} <- UTrc,
+ Count /= timeout],
+ Steps = slf_msgsim:get_step(Sched1),
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ F_retro = fun(Clnt) ->
+ L = [Count || {Cl,_Step,{counter, Count}} <- UTrc,
+ Count /= timeout, Cl == Clnt],
+ %% Retrograde counter if we truncate the floats?
+ Lt = [trunc(Count) || Count <- L],
+ decreasing_p(Lt)
+ end,
+ ClientRetroP = lists:any(F_retro, Clients),
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd2 = ~P\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Emitted counters = ~p\n",
+ [F1, F2, Sched1, 250,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Emitted]),
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("sched steps ", Steps,
+ measure("crashes ", NumCrashes,
+ measure("# ops ", length(Ops),
+ measure("# emitted ", length(Emitted),
+ measure("msgs sent ", NumMsgs,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {ops_finish, length(Ops) == length(UTrc)},
+ {emits_unique, length(Emitted) ==
+ length(lists:usort(Emitted))},
+ {per_client_not_retro, not ClientRetroP}])
+ end))))))))))).
+
+%%% Protocol implementation
+
+%% Known to be flawed: ask each server for its counter, then
+%% choose the max of all responses. The servers are naive
+%% and are not keeping per-key counters but rather a single
+%% counter for the entire server.
+
+counter_client1({counter_op, Servers}, _St) ->
+ [slf_msgsim:bang(Server, {incr_counter, slf_msgsim:self()}) ||
+ Server <- Servers],
+ {recv_timeout, fun counter_client1_reply/2, {Servers, []}}.
+
+counter_client1_reply({incr_counter_reply, Server, Count},
+ {Waiting, Replies})->
+ Replies2 = [{Server, Count}|Replies],
+ case Waiting -- [Server] of
+ [] ->
+ Val = make_val(Replies2),
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused};
+ Waiting2 ->
+ {recv_timeout, same, {Waiting2, Replies2}}
+ end;
+counter_client1_reply(timeout, {Waiting, Replies}) ->
+ Val = if length(Waiting) > length(Replies) ->
+ timeout;
+ true ->
+ make_val(Replies)
+ end,
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused}.
+
+counter_server1({incr_counter, From}, Count) ->
+ slf_msgsim:bang(From, {incr_counter_reply, slf_msgsim:self(), Count}),
+ {recv_general, same, Count + 1}.
+
+make_val(Replies) ->
+ Ns = [N || {_Server, N} <- Replies],
+ ByN = lists:sort([{N, Server} || {Server, N} <- Replies]),
+ SvrOrder = [Server || {_N, Server} <- ByN],
+ LHS_int = lists:max(Ns),
+ Left = integer_to_list(LHS_int),
+ Right = make_suffix(SvrOrder),
+ list_to_float(Left ++ "." ++ Right).
+
+make_suffix(ReplyServers) ->
+ lists:flatten(make_suffix2(ReplyServers)).
+
+make_suffix2(ReplyServers) ->
+ [lists:nth(2, atom_to_list(Svr)) || Svr <- ReplyServers].
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
+
+decreasing_p([A, B|Rest]) when A =< B ->
+ decreasing_p([B|Rest]);
+decreasing_p([_]) ->
+ false;
+decreasing_p([]) ->
+ false;
+decreasing_p(_) ->
+ true.
100 src/distrib_counter_bad4_sim.txt
@@ -0,0 +1,100 @@
+NOTE: Search for %% for hints on what to look for when something goes wrong.
+
+Difference with distrib_counter_bad3_sim.erl:
+
+The previous flawed protocol, #3, showed that converting to actual
+floating point numbers is sufficient for correctly ordering the output
+for cases like "9.something" -> "10.something".
+
+Summary: Protocol #4 does not prevent counters going backward, even
+ when we consider only the lefthand side of a floating point
+ number. We change the verification of the model to truncate
+ each float and check for retrograde results seen by each
+ client. Counterexample = Emitted counters = [2.21,1.2]
+
+So, the whole notion of having a client emit a floating point number
+to handle a "tie" really doesn't work.
+
+(rk@sbb)174> eqc:quickcheck(slf_msgsim_qc:prop_simulate(distrib_counter_bad4_sim, [])).
+%% I'm going to show only the shrunken case from now on....
+[...]
+Runnable = [], Receivable = []
+Emitted counters = [42.21,6.2]
+runnable: passed
+ops_finish: passed
+emits_unique: passed
+%% Here's the problem
+per_client_not_retro: failed
+%% Hooray, I love shrinking...
+Shrinking............(12 times)
+%% 1 client, 2 servers, 1 key (ignored)
+{1,2,1}
+{[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad4_sim.6.52918649>}],
+%% Server s1 starts with counter = 2.
+%% Server s2 starts with counter = 0.
+ [{s1,2,#Fun<distrib_counter_bad4_sim.5.5305677>},
+ {s2,0,#Fun<distrib_counter_bad4_sim.5.5305677>}],
+%% Schedule isn't crazy
+ [s2,s1,c1],
+%% One bi-directional partition c1<->s1 between simulated time 3-9.
+%% The net effect is that a message is dropped at sim time = 9 from c1 -> s1.
+%% {drop,9,c1,s1,{incr_counter,c1}},
+ [{partition,[c1],[s1],3,9},{partition,[s1],[c1],3,9}]}
+Failed:
+F1 = {1,2,1}
+F2 = {[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad4_sim.6.52918649>}],
+ [{s1,2,#Fun<distrib_counter_bad4_sim.5.5305677>},
+ {s2,0,#Fun<distrib_counter_bad4_sim.5.5305677>}],
+ [s2,s1,c1],
+ [{partition,[c1],[s1],3,9},{partition,[s1],[c1],3,9}]}
+End2 = {sched,15,6,
+ [s2,s1,c1],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad4_sim.6.52918649>,
+ undefined}},
+ {s1,{proc,s1,3,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad4_sim.5.5305677>,
+ undefined}},
+ {s2,{proc,s2,2,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad4_sim.5.5305677>,
+ undefined}}],
+%% Here's the system trace, in reverse order. Here's the timeout...
+ [{recv,14,scheduler,c1,timeout},
+ {recv,13,s2,c1,{incr_counter_reply,s2,1}},
+ {deliver,12,s2,c1,{incr_counter_reply,s2,1}},
+ {bang,11,s2,c1,{incr_counter_reply,s2,1}},
+ {recv,11,c1,s2,{incr_counter,c1}},
+ {deliver,10,c1,s2,{incr_counter,c1}},
+ {bang,9,c1,s2,{incr_counter,c1}},
+%%% ... and here's the dropped message that creates the timeout @ sim time = 14
+ {drop,9,c1,s1,{incr_counter,c1}},
+ {recv,9,scheduler,c1,{counter_op,[s1,s2]}},
+ {recv,8,s2,c1,{incr_counter_reply,s2,0}},
+ {deliver,7,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,6,s1,c1,{incr_counter_reply,s1,2}},
+ {deliver,5,s1,c1,{incr_counter_reply,s1,2}},
+ {bang,4,s2,c1,{incr_counter_reply,s2,0}},
+ {recv,4,c1,s2,{incr_counter,c1}},
+ {deliver,3,c1,s2,{incr_counter,c1}},
+ {bang,2,s1,c1,{incr_counter_reply,s1,2}},
+ {recv,2,c1,s1,{incr_counter,c1}},
+ {deliver,1,c1,s1,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2]}}],
+%% Here's the user trace, in reverse order.
+ [{c1,14,{counter,1.2}},{c1,8,{counter,2.21}}],
+ [{{c1,s1},[3,4,5,6,7,8,9]},{{s1,c1},[3,4,5,6,7,8,9]}]}
+Runnable = [], Receivable = []
+Emitted counters = [2.21,1.2]
+per_client_not_retro: failed
+false
148 src/distrib_counter_bad5_sim.erl
@@ -0,0 +1,148 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(distrib_counter_bad5_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_counter_op(NumClients, NumServers)).
+
+gen_counter_op(NumClients, NumServers) ->
+ ?LET(ClientI, choose(1, NumClients),
+ {lists:nth(ClientI, all_clients()),
+ {counter_op, lists:sublist(all_servers(), NumServers)}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun counter_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, gen_nat_nat2(5, 1), fun counter_server1/2} || Server <- Servers].
+
+gen_nat_nat2(A, B) ->
+ %% Use nat() A/(A+B) of the time, nat()*nat() B/(A+B) of the time
+ slf_msgsim_qc:gen_nat_nat2(A, B).
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, UTrc) ->
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ NumCrashes = length([x || {process_crash,_,_,_,_,_} <- Trc]),
+ Emitted = [Count || {_Clnt,_Step,{counter,Count}} <- UTrc,
+ Count /= timeout],
+ Steps = slf_msgsim:get_step(Sched1),
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ F_retro = fun(Clnt) ->
+ L = [Count || {Cl,_Step,{counter, Count}} <- UTrc,
+ Count /= timeout, Cl == Clnt],
+ %% Retrograde counter?
+ L /= lists:usort(L)
+ end,
+ ClientRetroP = lists:any(F_retro, Clients),
+ Ph1Drops = [Msg || Msg = {drop,_,_,_,T} <- Trc,
+ element(1, T) == incr_counter orelse
+ element(1, T) == incr_counter_reply],
+ Ph2Drops = [Msg || Msg = {drop,_,_,_,T} <- Trc,
+ element(1, T) == maybe_set_counter],
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd2 = ~P\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Emitted counters = ~w\n"
+ "1st phase msg drops = ~p\n"
+ "2nd phase msg drops = ~p\n",
+ [F1, F2, Sched1, 250,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Emitted,
+ Ph1Drops,
+ Ph2Drops
+ ]),
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("sched steps ", Steps,
+ measure("crashes ", NumCrashes,
+ measure("# ops ", length(Ops),
+ measure("# emitted ", length(Emitted),
+ measure("msgs sent ", NumMsgs,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {ops_finish, length(Ops) == length(UTrc)},
+ {emits_unique, length(Emitted) ==
+ length(lists:usort(Emitted))},
+ {per_client_not_retro, not ClientRetroP}])
+ %% {not_retro, Emitted == lists:sort(Emitted)}])
+ end))))))))))).
+
+%%% Protocol implementation
+
+%% Known to be flawed: ask each server for its counter, then
+%% choose the max of all responses. The servers are naive
+%% and are not keeping per-key counters but rather a single
+%% counter for the entire server.
+
+counter_client1({counter_op, Servers}, _St) ->
+ [slf_msgsim:bang(Server, {incr_counter, slf_msgsim:self()}) ||
+ Server <- Servers],
+ {recv_timeout, fun counter_client1_reply/2, {Servers, Servers, []}}.
+
+counter_client1_reply({incr_counter_reply, Server, Count},
+ {AllServers, Waiting, Replies})->
+ Replies2 = [{Server, Count}|Replies],
+ case Waiting -- [Server] of
+ [] ->
+ Val = make_val(Replies2),
+ [slf_msgsim:bang(Svr, {maybe_set_counter, Val}) || Svr <- AllServers],
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused};
+ Waiting2 ->
+ {recv_timeout, same, {AllServers, Waiting2, Replies2}}
+ end;
+counter_client1_reply(timeout, {AllServers, Waiting, Replies}) ->
+ Val = if length(Waiting) > length(Replies) ->
+ timeout;
+ true ->
+ make_val(Replies)
+ end,
+ [slf_msgsim:bang(Svr, {maybe_set_counter, Val}) || Svr <- AllServers],
+ slf_msgsim:add_utrace({counter, Val}),
+ {recv_general, same, unused}.
+
+counter_server1({incr_counter, From}, Count) ->
+ slf_msgsim:bang(From, {incr_counter_reply, slf_msgsim:self(), Count}),
+ {recv_general, same, Count + 1};
+counter_server1({maybe_set_counter, MaybeCount}, OldCount) ->
+ Count = lists:max([MaybeCount, OldCount]),
+ {recv_general, same, Count}.
+
+make_val(Replies) ->
+ lists:max([Counter || {_Server, Counter} <- Replies]).
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
+
242 src/distrib_counter_bad5_sim.txt
@@ -0,0 +1,242 @@
+NOTE: Search for %% for hints on what to look for when something goes wrong.
+
+Difference with distrib_counter_bad4_sim.erl:
+
+Protocol #4 was also quite easily broken, so this protocol, #5, tries
+a different approach.
+
+The #5 client uses a 2-phase approach. Phase 1 is the same as
+protocol #4, and the client uses protocol #1's integer method for
+calculating its value V.
+
+In phase 2, the client tells each server that it had calculated V with
+a {maybe_set_counter, V} message. When the server receives a
+{maybe_set_counter message,...}, it will update its counter to be the
+maximum of V and the server's current counter value.
+
+Summary: This protocol is also broken, though sometimes it can pass
+ 100 test cases without failing. All it takes is a single
+ partition that causes two dropped messages.
+
+ Naively adding a 2nd phase to a protocol to fix a 1st phase
+ does not guarantee success.
+
+ In later exploration with this same protocol #5, I see that
+ it's indeed possible for the protocol to fail even when only
+ a single message is dropped ... and that message is a *1st
+ phase* message, e.g. {incr_counter_reply,s2,2} ... so the 2nd
+ phase doesn't actually help at all!)
+
+ Actually, it's also possible for the protocol to fail the
+ emits_unique property without any dropped messages at all!
+ I'll include that counterexample after the first one.
+
+Shrinking............(12 times)
+%% 1 client, 2 servers, 1 key (ignored)
+{1,2,1}
+%% Two ops by the same client
+{[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad5_sim.6.52918649>}],
+%% Server s1 starts with counter = 0
+%% Server s2 starts with counter = 1
+ [{s1,0,#Fun<distrib_counter_bad5_sim.5.5305677>},
+ {s2,1,#Fun<distrib_counter_bad5_sim.5.5305677>}],
+ [s2,s1,c1],
+%% There is a unidirectional partition c1 -> s2 from sim time 1-11.
+%% This causes two dropped messages:
+%% {drop,8,c1,s2,{maybe_set_counter,1}}, ... at sim time = 8
+%% {drop,11,c1,s2,{incr_counter,c1}}, ... at sim time = 11
+ [{partition,[c1],[s2],1,11}]}
+Failed:
+F1 = {1,2,1}
+F2 = {[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
+ [{c1,[],#Fun<distrib_counter_bad5_sim.6.52918649>}],
+ [{s1,0,#Fun<distrib_counter_bad5_sim.5.5305677>},
+ {s2,1,#Fun<distrib_counter_bad5_sim.5.5305677>}],
+ [s2,s1,c1],
+ [{partition,[c1],[s2],1,11}]}
+End2 = {sched,21,9,
+ [s2,s1,c1],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad5_sim.6.52918649>,
+ undefined}},
+ {s1,{proc,s1,2,[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad5_sim.5.5305677>,
+ undefined}},
+ {s2,{proc,s2,2,[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<distrib_counter_bad5_sim.5.5305677>,
+ undefined}}],
+%% Here's the system trace, in reverse order.
+ [{recv,20,c1,s2,{maybe_set_counter,1}},
+ {deliver,19,c1,s2,{maybe_set_counter,1}},
+ {recv,18,c1,s1,{maybe_set_counter,1}},
+ {deliver,17,c1,s1,{maybe_set_counter,1}},
+ {bang,16,c1,s2,{maybe_set_counter,1}},
+ {bang,16,c1,s1,{maybe_set_counter,1}},
+%% Here's a timeout
+ {recv,16,scheduler,c1,timeout},
+ {recv,15,s1,c1,{incr_counter_reply,s1,1}},
+ {deliver,14,s1,c1,{incr_counter_reply,s1,1}},
+ {bang,13,s1,c1,{incr_counter_reply,s1,1}},
+ {recv,13,c1,s1,{incr_counter,c1}},
+ {deliver,12,c1,s1,{incr_counter,c1}},
+%% Here's dropped message #2
+ {drop,11,c1,s2,{incr_counter,c1}},
+ {bang,11,c1,s1,{incr_counter,c1}},
+ {recv,11,scheduler,c1,{counter_op,[s1,s2]}},
+ {recv,10,c1,s1,{maybe_set_counter,1}},
+ {deliver,9,c1,s1,{maybe_set_counter,1}},
+%% Here's dropped message #1
+ {drop,8,c1,s2,{maybe_set_counter,1}},
+ {bang,8,c1,s1,{maybe_set_counter,1}},
+ {recv,8,s2,c1,{incr_counter_reply,s2,1}},
+ {deliver,7,s2,c1,{incr_counter_reply,s2,1}},
+ {recv,6,s1,c1,{incr_counter_reply,s1,0}},
+ {deliver,5,s1,c1,{incr_counter_reply,s1,0}},
+ {bang,4,s2,c1,{incr_counter_reply,s2,1}},
+ {recv,4,c1,s2,{incr_counter,c1}},
+ {deliver,3,c1,s2,{incr_counter,c1}},
+ {bang,2,s1,c1,{incr_counter_reply,s1,0}},
+ {recv,2,c1,s1,{incr_counter,c1}},
+ {deliver,1,c1,s1,{incr_counter,c1}},
+ {bang,0,c1,s2,{incr_counter,c1}},
+ {bang,0,c1,s1,{incr_counter,c1}},
+ {recv,0,scheduler,c1,{counter_op,[s1,s2]}}],
+ [{c1,16,{counter,1}},{c1,8,{counter,1}}],
+ [{{c1,s2},[1,2,3,4,5,6,7,8,9,10,11]}]}
+Runnable = [], Receivable = []
+%% Bummer.
+Emitted counters = [1,1]
+emits_unique: failed
+per_client_not_retro: failed
+false
+
+--------------------------------------------------------
+
+Shrinking.......(7 times)
+%% 2 clients, 3 servers, 1 key (ignored)
+{2,3,1}
+%% 2 ops, executed by 2 different clients
+{[{c2,{counter_op,[s1,s2,s3]}},{c1,{counter_op,[s1,s2,s3]}}],
+ [{c1,[],#Fun<distrib_counter_bad5_sim.6.52918649>},
+ {c2,[],#Fun<distrib_counter_bad5_sim.6.52918649>}],
+ [{s1,0,#Fun<distrib_counter_bad5_sim.5.5305677>},
+ {s2,1,#Fun<distrib_counter_bad5_sim.5.5305677>},
+ {s3,1,#Fun<distrib_counter_bad5_sim.5.5305677>}],
+%% Scheduler isn't crazy
+ [s2,s3,s1,c2,c1],
+%% No effective partitions
+ [{partition,[],[],0,0}]}
+Failed:
+F1 = {2,3,1}
+F2 = {[{c2,{counter_op,[s1,s2,s3]}},{c1,{counter_op,[s1,s2,s3]}}],
+ [{c1,[],#Fun<distrib_counter_bad5_sim.6.52918649>},
+ {c2,[],#Fun<distrib_counter_bad5_sim.6.52918649>}],
+ [{s1,0,#Fun<distrib_counter_bad5_sim.5.5305677>},
+ {s2,1,#Fun<distrib_counter_bad5_sim.5.5305677>},
+ {s3,1,#Fun<distrib_counter_bad5_sim.5.5305677>}],
+ [s2,s3,s1,c2,c1],
+ [{partition,[],[],0,0}]}
+End2 = {sched,38,18,
+ [s2,s3,s1,c2,c1],
+ [],
+ [{c1,{proc,c1,unused,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad5_sim.6.52918649>,
+ undefined}},
+ {c2,{proc,c2,unused,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<distrib_counter_bad5_sim.6.52918649>,
+ undefined}},
+ {s1,{proc,s1,2,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad5_sim.5.5305677>,
+ undefined}},
+ {s2,{proc,s2,3,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad5_sim.5.5305677>,
+ undefined}},
+ {s3,{proc,s3,3,[],
+ {[],[]},
+ {[],[]},
+ outbox,#Fun<distrib_counter_bad5_sim.5.5305677>,
+ undefined}}],
+ [{recv,37,c1,s3,{maybe_set_counter,2}},
+ {recv,36,c2,s3,{maybe_set_counter,2}},
+ {recv,35,c1,s2,{maybe_set_counter,2}},
+ {deliver,34,c1,s3,{maybe_set_counter,2}},
+ {deliver,33,c2,s3,{maybe_set_counter,2}},
+ {recv,32,c1,s1,{maybe_set_counter,2}},
+ {recv,31,c2,s2,{maybe_set_counter,2}},
+ {deliver,30,c1,s2,{maybe_set_counter,2}},
+ {deliver,29,c2,s2,{maybe_set_counter,2}},
+ {recv,28,c2,s1,{maybe_set_counter,2}},
+ {deliver,27,c1,s1,{maybe_set_counter,2}},
+ {deliver,26,c2,s1,{maybe_set_counter,2}},
+ {bang,25,c1,s3,{maybe_set_counter,2}},
+ {bang,25,c1,s2,{maybe_set_counter,2}},
+ {bang,25,c1,s1,{maybe_set_counter,2}},
+ {recv,25,s2,c1,{incr_counter_reply,s2,2}},
+ {bang,24,c2,s3,{maybe_set_counter,2}},
+ {bang,24,c2,s2,{maybe_set_counter,2}},
+ {bang,24,c2,s1,{maybe_set_counter,2}},
+ {recv,24,s3,c2,{incr_counter_reply,s3,2}},
+ {deliver,23,s3,c2,{incr_counter_reply,s3,2}},
+ {recv,22,s1,c1,{incr_counter_reply,s1,1}},
+ {bang,21,s3,c2,{incr_counter_reply,s3,2}},
+ {recv,21,c2,s3,{incr_counter,c2}},
+ {deliver,20,s2,c1,{incr_counter_reply,s2,2}},
+ {recv,19,s3,c1,{incr_counter_reply,s3,1}},
+ {deliver,18,c2,s3,{incr_counter,c2}},
+ {deliver,17,s1,c1,{incr_counter_reply,s1,1}},
+ {deliver,16,s3,c1,{incr_counter_reply,s3,1}},
+ {bang,15,s2,c1,{incr_counter_reply,s2,2}},
+ {recv,15,c1,s2,{incr_counter,c1}},
+ {recv,14,s2,c2,{incr_counter_reply,s2,1}},
+ {bang,13,s1,c1,{incr_counter_reply,s1,1}},
+ {recv,13,c1,s1,{incr_counter,c1}},
+ {bang,12,s3,c1,{incr_counter_reply,s3,1}},
+ {recv,12,c1,s3,{incr_counter,c1}},
+ {deliver,11,s2,c2,{incr_counter_reply,s2,1}},
+ {deliver,10,c1,s3,{incr_counter,c1}},
+ {recv,9,s1,c2,{incr_counter_reply,s1,0}},
+ {deliver,8,s1,c2,{incr_counter_reply,s1,0}},
+ {bang,7,s2,c2,{incr_counter_reply,s2,1}},
+ {recv,7,c2,s2,{incr_counter,c2}},
+ {deliver,6,c1,s2,{incr_counter,c1}},
+ {deliver,5,c2,s2,{incr_counter,c2}},
+ {bang,4,s1,c2,{incr_counter_reply,s1,0}},
+ {recv,4,c2,s1,{incr_counter,c2}},
+ {deliver,3,c1,s1,{incr_counter,c1}},
+ {deliver,2,c2,s1,{incr_counter,c2}},
+ {bang,1,c1,s3,{incr_counter,c1}},
+ {bang,1,c1,s2,{incr_counter,c1}},
+ {bang,1,c1,s1,{incr_counter,c1}},
+ {recv,1,scheduler,c1,{counter_op,[s1,s2,s3]}},
+ {bang,0,c2,s3,{incr_counter,c2}},
+ {bang,0,c2,s2,{incr_counter,c2}},
+ {bang,0,c2,s1,{incr_counter,c2}},
+ {recv,0,scheduler,c2,{counter_op,[s1,s2,s3]}}],
+%% Here are the duplicate counters. They're emitted at nearly the
+%% same "wall clock" time. But it's just a matter of scheduler
+%% interleaving that causes the duplicate counters.
+ [{c1,25,{counter,2}},{c2,24,{counter,2}}],
+ []}
+Runnable = [], Receivable = []
+%% Bummer: dupes without any dropped messages.
+Emitted counters = [2,2]
+1st phase msg drops = []
+2nd phase msg drops = []
+emits_unique: failed
+false
116 src/echo_bad1_sim.erl
@@ -0,0 +1,116 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(echo_bad1_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+-define(MAGIC_NUMBER, 13).
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_echo_op(NumClients, NumServers)).
+
+gen_echo_op(NumClients, NumServers) ->
+ ?LET({ClientI, ServerI},
+ {choose(1, NumClients), choose(1, NumServers)},
+ {lists:nth(ClientI, all_clients()),
+ {echo_op, lists:nth(ServerI, all_servers()), int()}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun echo_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, {unused, Server}, fun echo_server1/2} || Server <- Servers].
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, _UTrc) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ Predicted = predict_echos(Clients, Ops),
+ Actual = actual_echos(Clients, Sched1),
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd = ~p\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Predicted ~w\nActual ~w\n",
+ [F1, F2, Sched1,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Predicted, Actual]),
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("echoes ", length(Ops),
+ measure("msgs sent ", NumMsgs,
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {all_ok, slf_msgsim_qc:check_exact_msg_or_timeout(
+ Clients, Predicted, Actual)}])
+ end)))))))).
+
+predict_echos(Clients, Ops) ->
+ [{Client, begin
+ ClientOps = [Op || {Cl, Op} <- Ops, Cl == Client],
+ [Msg || {echo_op, _Server, Msg} <- ClientOps]
+ end} || Client <- Clients].
+
+actual_echos(Clients, Sched) ->
+ [{Client, lists:reverse(slf_msgsim:get_proc_state(Client, Sched))} ||
+ Client <- Clients].
+
+%%% Protocol implementation
+
+%% proto bad 1: An echo server. Compared to the good echo_sim.erl,
+%% this server starts acting badly after it has received
+%% a magic number.
+
+echo_client1({echo_op, Server, Key}, ReplyList) ->
+ slf_msgsim:bang(Server, {echo, slf_msgsim:self(), Key}),
+ {recv_timeout, fun echo_client1_echoreply/2, ReplyList}.
+
+echo_client1_echoreply(timeout, ReplyList) ->
+ {recv_general, same, [server_timeout|ReplyList]};
+echo_client1_echoreply({echo_reply, Msg}, ReplyList) ->
+ {recv_general, same, [Msg|ReplyList]}.
+
+echo_server1({echo, Client, _Msg}, ?MAGIC_NUMBER = St) ->
+ slf_msgsim:bang(Client, {echo_reply, St}),
+ {recv_general, same, St};
+echo_server1({echo, Client, ?MAGIC_NUMBER = Msg}, _St) ->
+ slf_msgsim:bang(Client, {echo_reply, Msg}),
+ {recv_general, same, Msg};
+echo_server1({echo, Client, Msg}, St) ->
+ slf_msgsim:bang(Client, {echo_reply, Msg}),
+ {recv_general, same, St}.
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
+
+all_keys() ->
+ [k1, k2, k3, k4, k5, k6, k7, k8, k9].
+
151 src/echo_bad1_sim.txt
@@ -0,0 +1,151 @@
+33> eqc:quickcheck(slf_msgsim_qc:prop_simulate(echo_bad1_sim, [])).
+..................................................Failed! After 51 tests.
+{5,1,1} %% 5 Clients, 1 server, 1 key
+{[{c3,{echo_op,s1,13}}, %% 4 echo ops executed by 2 different clients
+ {c3,{echo_op,s1,-14}},
+ {c1,{echo_op,s1,15}},
+ {c3,{echo_op,s1,8}}],
+ [{c1,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c2,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c3,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c4,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c5,[],#Fun<echo_bad1_sim.5.45368517>}],
+ [{s1,{unused,s1},#Fun<echo_bad1_sim.4.12451426>}],
+ %% Scheduler isn't unfair: all procs listed once
+ [c2,c4,c4,c5,c1,s1,c3],
+ %% There's a bidirectional partition between simulator steps 14 and 27.
+ %% Though not known at test case generation time, this simulation will
+ %% require 16 steps and therefore dropped messages are possible.
+ %% In fact, a message is indeed dropped at the very tail end of the test,
+ %% which in turn triggers a timeout.
+ [{partition,[c5,c5,c2,c3],[s1,s1,s1,s1],14,27},
+ {partition,[s1,s1,s1,s1],[c5,c5,c2,c3],14,27}]}
+Failed:
+F1 = {5,1,1}
+F2 = {[{c3,{echo_op,s1,13}},
+ {c3,{echo_op,s1,-14}},
+ {c1,{echo_op,s1,15}},
+ {c3,{echo_op,s1,8}}],
+ [{c1,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c2,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c3,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c4,[],#Fun<echo_bad1_sim.5.45368517>},
+ {c5,[],#Fun<echo_bad1_sim.5.45368517>}],
+ [{s1,{unused,s1},#Fun<echo_bad1_sim.4.12451426>}],
+ [c2,c4,c4,c5,c1,s1,c3],
+ [{partition,[c5,c5,c2,c3],[s1,s1,s1,s1],14,27},
+ {partition,[s1,s1,s1,s1],[c5,c5,c2,c3],14,27}]}
+End = {sched,17,6,
+ [c2,c4,c4,c5,c1,s1,c3],
+ [],
+ [{c1,{proc,c1,
+ [15],
+ [],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<echo_bad1_sim.5.45368517>,undefined}},
+ {c2,{proc,c2,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<echo_bad1_sim.5.45368517>,undefined}},
+ {c3,{proc,c3,
+ [server_timeout,13,13],
+ [],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<echo_bad1_sim.5.45368517>,undefined}},
+ {c4,{proc,c4,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<echo_bad1_sim.5.45368517>,undefined}},
+ {c5,{proc,c5,[],[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<echo_bad1_sim.5.45368517>,undefined}},
+ {s1,{proc,s1,13,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<echo_bad1_sim.4.12451426>,undefined}}],
+ [{recv,16,scheduler,c3,timeout},
+ {drop,15,c3,s1,{echo,c3,8}},
+ {recv,15,scheduler,c3,{echo_op,s1,8}},
+ {recv,14,s1,c3,{echo_reply,13}},
+ {deliver,13,s1,c3,{echo_reply,13}},
+ {bang,12,s1,c3,{echo_reply,13}},
+ {recv,12,c3,s1,{echo,c3,-14}},
+ {deliver,11,c3,s1,{echo,c3,-14}},
+ {bang,10,c3,s1,{echo,c3,-14}},
+ {recv,10,scheduler,c3,{echo_op,s1,-14}},
+ {recv,9,s1,c3,{echo_reply,13}},
+ {deliver,8,s1,c3,{echo_reply,13}},
+ {bang,7,s1,c3,{echo_reply,13}},
+ {recv,7,c3,s1,{echo,c3,13}},
+ {recv,6,s1,c1,{echo_reply,15}},
+ {deliver,5,s1,c1,{echo_reply,15}},
+ {deliver,4,c3,s1,{echo,c3,13}},
+ {bang,3,s1,c1,{echo_reply,15}},
+ {recv,3,c1,s1,{echo,c1,15}},
+ {deliver,2,c1,s1,{echo,c1,15}},
+ {bang,1,c3,s1,{echo,c3,13}},
+ {recv,1,scheduler,c3,{echo_op,s1,13}},
+ {bang,0,c1,s1,{echo,c1,15}},
+ {recv,0,scheduler,c1,{echo_op,s1,15}}],
+ [],
+ [{{c2,s1},[14,15,16,17,18,19,20,21,22,23,24,25,26,27]},
+ {{c3,s1},[14,15,16,17,18,19,20,21,22,23,24,25,26,27]},
+ {{c5,s1},[14,15,16,17,18,19,20,21,22,23,24,25,26,27]},
+ {{s1,c2},[14,15,16,17,18,19,20,21,22,23,24,25,26,27]},
+ {{s1,c3},[14,15,16,17,18,19,20,21,22,23,24,25,26,27]},
+ {{s1,c5},[14,15,16,17,18,19,20,21,22,23,24,25,26,27]}]}
+Runnable = [], Receivable = []
+Predicted [{c1,[15]},{c2,[]},{c3,[13,-14,8]},{c4,[]},{c5,[]}]
+Actual [{c1,[15]},{c2,[]},{c3,[13,13,server_timeout]},{c4,[]},{c5,[]}]
+runnable: passed
+all_ok: failed
+Shrinking.........(9 times)
+{1,1,1} %% One server, one client, one key
+{[{c1,{echo_op,s1,13}},{c1,{echo_op,s1,0}}],
+ [{c1,[],#Fun<echo_bad1_sim.5.45368517>}],
+ [{s1,{unused,s1},#Fun<echo_bad1_sim.4.12451426>}],
+ %% Simplest possible secheduler
+ [c1,s1],
+ %% No partitions (effectively)
+ [{partition,[],[],0,0},{partition,[],[],0,0}]}
+Failed:
+F1 = {1,1,1}
+F2 = {[{c1,{echo_op,s1,13}},{c1,{echo_op,s1,0}}],
+ [{c1,[],#Fun<echo_bad1_sim.5.45368517>}],
+ [{s1,{unused,s1},#Fun<echo_bad1_sim.4.12451426>}],
+ [c1,s1],
+ [{partition,[],[],0,0},{partition,[],[],0,0}]}
+End = {sched,10,4,
+ [c1,s1],
+ [],
+ [{c1,{proc,c1,"\r\r",[],
+ {[],[]},
+ {[],[]},
+ mbox,#Fun<echo_bad1_sim.5.45368517>,undefined}},
+ {s1,{proc,s1,13,[],
+ {[],[]},
+ {[],[]},
+ delayed,#Fun<echo_bad1_sim.4.12451426>,undefined}}],
+ [{recv,9,s1,c1,{echo_reply,13}},
+ {deliver,8,s1,c1,{echo_reply,13}},
+ {bang,7,s1,c1,{echo_reply,13}},
+ {recv,7,c1,s1,{echo,c1,0}},
+ {deliver,6,c1,s1,{echo,c1,0}},
+ {bang,5,c1,s1,{echo,c1,0}},
+ {recv,5,scheduler,c1,{echo_op,s1,0}},
+ {recv,4,s1,c1,{echo_reply,13}},
+ {deliver,3,s1,c1,{echo_reply,13}},
+ {bang,2,s1,c1,{echo_reply,13}},
+ {recv,2,c1,s1,{echo,c1,13}},
+ {deliver,1,c1,s1,{echo,c1,13}},
+ {bang,0,c1,s1,{echo,c1,13}},
+ {recv,0,scheduler,c1,{echo_op,s1,13}}],
+ [],[]}
+Runnable = [], Receivable = []
+Predicted [{c1,[13,0]}]
+Actual [{c1,[13,13]}]
+all_ok: failed
+false
108 src/echo_sim.erl
@@ -0,0 +1,108 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc
+%%%
+%%% @end
+%%% Created : 26 Mar 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+-module(echo_sim).
+
+-compile(export_all).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%%% Generators
+
+%% required
+gen_initial_ops(NumClients, NumServers, _NumKeys, _Props) ->
+ list(gen_echo_op(NumClients, NumServers)).
+
+gen_echo_op(NumClients, NumServers) ->
+ ?LET({ClientI, ServerI},
+ {choose(1, NumClients), choose(1, NumServers)},
+ {lists:nth(ClientI, all_clients()),
+ {echo_op, lists:nth(ServerI, all_servers()), make_ref()}}).
+
+%% required
+gen_client_initial_states(NumClients, _Props) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ [{Clnt, [], fun echo_client1/2} || Clnt <- Clients].
+
+%% required
+gen_server_initial_states(NumServers, _Props) ->
+ Servers = lists:sublist(all_servers(), 1, NumServers),
+ [{Server, {unused, Server}, fun echo_server1/2} || Server <- Servers].
+
+%%% Verify our properties
+
+%% required
+verify_property(NumClients, NumServers, _Props, F1, F2, Ops,
+ _Sched0, Runnable, Sched1, Trc, _UTrc) ->
+ Clients = lists:sublist(all_clients(), 1, NumClients),
+ Predicted = predict_echos(Clients, Ops),
+ Actual = actual_echos(Clients, Sched1),
+ NumMsgs = length([x || {bang,_,_,_,_} <- Trc]),
+ NumDrops = length([x || {drop,_,_,_,_} <- Trc]),
+ NumTimeouts = length([x || {recv,_,scheduler,_,timeout} <- Trc]),
+ ?WHENFAIL(
+ io:format("Failed:\nF1 = ~p\nF2 = ~p\nEnd = ~p\n"
+ "Runnable = ~p, Receivable = ~p\n"
+ "Predicted ~p\nActual ~p\n",
+ [F1, F2, Sched1,
+ slf_msgsim:runnable_procs(Sched1),
+ slf_msgsim:receivable_procs(Sched1),
+ Predicted, Actual]),
+ measure("clients ", NumClients,
+ measure("servers ", NumServers,
+ measure("echoes ", length(Ops),
+ measure("msgs sent ", NumMsgs,
+ classify(NumDrops /= 0, at_least_1_msg_dropped,
+ measure("msgs dropped", NumDrops,
+ measure("timeouts ", NumTimeouts,
+ begin
+ conjunction([{runnable, Runnable == false},
+ {all_ok, slf_msgsim_qc:check_exact_msg_or_timeout(
+ Clients, Predicted, Actual)}])
+ end)))))))).
+
+predict_echos(Clients, Ops) ->
+ [{Client, begin
+ ClientOps = [Op || {Cl, Op} <- Ops, Cl == Client],
+ [Msg || {echo_op, _Server, Msg} <- ClientOps]
+ end} || Client <- Clients].
+
+actual_echos(Clients, Sched) ->
+ [{Client, lists:reverse(slf_msgsim:get_proc_state(Client, Sched))} ||
+ Client <- Clients].
+
+%%% Protocol implementation
+
+%% proto 1: An echo server. Not interesting by itself, but hopefully
+%% useful in figuring out how best to handle dropped packets
+%% and timeouts.
+
+echo_client1({echo_op, Server, Key}, ReplyList) ->
+ slf_msgsim:bang(Server, {echo, slf_msgsim:self(), Key}),
+ {recv_timeout, fun echo_client1_echoreply/2, ReplyList}.
+
+echo_client1_echoreply(timeout, ReplyList) ->
+ {recv_general, same, [server_timeout|ReplyList]};
+echo_client1_echoreply({echo_reply, Msg}, ReplyList) ->
+ {recv_general, same, [Msg|ReplyList]}.
+
+echo_server1({echo, Client, Msg}, St) ->
+ slf_msgsim:bang(Client, {echo_reply, Msg}),
+ {recv_general, same, St}.
+
+%%% Misc....
+
+all_clients() ->
+ [c1, c2, c3, c4, c5, c6, c7, c8, c9].
+
+all_servers() ->
+ [s1, s2, s3, s4, s5, s6, s7, s8, s9].
+
+all_keys() ->
+ [k1, k2, k3, k4, k5, k6, k7, k8, k9].
+
13 src/msgdropsim.app.src
@@ -0,0 +1,13 @@
+{application, msgdropsim,
+ [
+ {description, "Message dropping simulator"},
+ {vsn, "0.1.0"},
+ {registered, []},
+ {applications, [
+ kernel,
+ stdlib,
+ sasl
+ ]},
+ %% {mod, { msgdropsim_app, []}},
+ {env, []}
+ ]}.
466 src/slf_msgsim.erl
@@ -0,0 +1,466 @@
+%%%-------------------------------------------------------------------
+%%% @author Scott Lystig Fritchie <fritchie@snookles.com>
+%%% @copyright (C) 2011, Scott Lystig Fritchie
+%%% @doc A message passing simulator, with delayed/lost messages and
+%%% network partitions.
+%%%
+%%% @end
+%%% Created : 21 Feb 2011 by Scott Lystig Fritchie <fritchie@snookles.com>
+%%%-------------------------------------------------------------------
+
+-module(slf_msgsim).
+-compile(export_all).
+
+-include_lib("eunit/include/eunit.hrl").
+
+-type orddict() :: orddict:orddict().
+-type partition() :: {partition, [proc()], [proc()], integer(), integer()}.
+-type proc() :: atom().
+
+-record(proc, {
+ name :: proc(), % All procs have a name
+ state :: term(), % proc private state
+ mbox :: list(), % incoming mailbox
+ outbox :: queue(), % outgoing msgs waiting send sched'ing
+ delayed :: queue(), % {Delay::integer(), Rcpt::atom(), Msg}
+ next :: mbox | outbox | delayed, % next execution type
+ recv_gen :: fun(), % Fun for generic receive without timeout
+ recv_w_timeout :: fun() % Fun for receive with timeout
+ }).
+
+-record(sched, {
+ step = 0 :: integer(), % Scheduling step #
+ numsent = 0 :: integer(), % Number of messages sent
+ tokens :: list(atom()),% Process scheduler tokens
+ crashed = [] :: list(atom()),% Processes that have crashed
+ procs :: orddict(), % key=proc name, val=#proc{}
+ trace = [] :: list(), % trace events
+ utrace = [] :: list(), % user trace events
+ %% Partition dictionary: key = {From::atom(), To::atom()}
+ %% value = list of steps to drop packets
+ partitions :: orddict()
+ }).
+
+-spec new_sim([{proc(), term(), fun()}], [{proc(), term(), fun()}],
+ [term()], [proc()], [partition()]) -> #sched{}.
+new_sim(Clients, Servers, InitialMsgs, SchedOrder, Partitions) ->
+ AllCSs = Clients ++ Servers,
+ AllNames = lists:usort([Name || {Name, _St, _Recv} <- AllCSs]),
+ MissingPs = AllNames -- lists:usort(SchedOrder),% Add missing procs to toks
+ S = #sched{tokens = SchedOrder ++ MissingPs,
+ procs = orddict:from_list([{Name, init_proc(ProcSpec)} ||
+ {Name,_,_} = ProcSpec <- AllCSs]),
+ partitions = make_partition_dict(Partitions)
+ },
+ send_initial_msgs_to_procs(InitialMsgs, S).
+
+-spec init_proc({proc(), term(), function()}) ->
+ #proc{}.
+init_proc({Name, State, RecvFun}) ->
+ init_proc(Name, State, RecvFun).
+
+-spec init_proc(proc(), term(), function()) ->
+ #proc{}.
+init_proc(Name, State, RecvFun) ->
+ #proc{name = Name,
+ state = State,
+ mbox = [],
+ outbox = queue:new(),
+ delayed = queue:new(),
+ next = mbox,
+ recv_gen = RecvFun,
+ recv_w_timeout = undefined}.
+
+-spec make_partition_dict([partition()]) -> orddict().
+
+make_partition_dict(Ps) ->
+ Raw = [{{From, To}, N} ||
+ {partition, Froms, Tos, Start, End} <- Ps,
+ From <- lists:usort(Froms), To <- lists:usort(Tos),
+ N <- lists:seq(Start, End)],
+ lists:foldl(fun({Key, V}, D) -> orddict:append(Key, V, D) end,
+ orddict:new(), Raw).
+
+-spec send_initial_msgs_to_procs([term()], #sched{}) ->
+ #sched{}.
+send_initial_msgs_to_procs(Ops, S0) ->
+ lists:foldl(fun({Proc, Msg}, S) ->
+ bang(scheduler, Proc, Msg, false, S)
+ end, S0, Ops).
+
+%% NOTE: bang/2, for use by simulation functions, is defined in the
+%% impure section.
+
+bang(Sender, Rcpt, Msg, S) ->
+ bang(Sender, Rcpt, Msg, true, S).
+
+bang(scheduler, Rcpt, Msg, false, S) ->
+ P = fetch_proc(Rcpt, S),
+ store_proc(P#proc{mbox = P#proc.mbox ++ [{imsg, scheduler, Rcpt, Msg}]}, S);
+bang(Sender, Rcpt, Msg, IncrSentP,
+ #sched{numsent = NumSent0, partitions = PartD, step = Step} = S) ->
+ DropP = case orddict:find({Sender, Rcpt}, PartD) of
+ {ok, PartSteps} -> lists:member(Step, PartSteps);
+ error -> false
+ end,
+ if DropP ->
+ Trc = {drop, S#sched.step, Sender, Rcpt, Msg},
+ add_trace(Trc, S);
+ true ->
+ P = fetch_proc(Sender, S),
+ NumSent = if IncrSentP -> NumSent0 + 1;
+ true -> NumSent0
+ end,
+ Trc = {bang, S#sched.step, Sender, Rcpt, Msg},
+ store_proc(add_outgoing_msg(Sender, Rcpt, Msg, P),
+ add_trace(Trc, S#sched{numsent = NumSent}))
+ end.
+
+fetch_proc(Name, S) ->
+ orddict:fetch(Name, S#sched.procs).
+
+%% NOTE: For export to outside world/external API
+
+get_proc_state(Name, S) ->
+ (fetch_proc(Name, S))#proc.state.
+
+store_proc(P, S) ->
+ S#sched{procs = orddict:store(P#proc.name, P, S#sched.procs)}.
+
+runnable_proc_p(#proc{mbox = Mbox, outbox = Outbox, delayed = Delayed}) ->
+ Mbox /= [] orelse (not queue:is_empty(Outbox))
+ orelse (not queue:is_empty(Delayed)).
+
+runnable_any_proc_p(S) ->
+ lists:any(fun({_Name, P}) -> runnable_proc_p(P) end, S#sched.procs).
+
+runnable_procs(S) ->
+ [Name || {Name, P} <- S#sched.procs, runnable_proc_p(P)].
+
+receivable_proc_p(#proc{recv_w_timeout = undefined}) ->
+ false;
+receivable_proc_p(_) ->
+ true.
+
+receivable_any_proc_p(S) ->
+ lists:any(fun({_Name, P}) -> receivable_proc_p(P) end, S#sched.procs).
+
+receivable_procs(S) ->
+ [Name || {Name, P} <- S#sched.procs, receivable_proc_p(P)].
+
+run_scheduler(S) ->
+ run_scheduler(S, 5000).
+
+run_scheduler(S0, 0) ->
+ %% Run one more time: if the processes are stupid enough to
+ %% consume timeout messages without doing The Right Thing, then S1
+ %% should have the last timeout message consumed so that all procs
+ %% in S1 is neither runnable nor receivable.
+ S1 = run_scheduler_with_tokens(S0#sched.tokens, S0),
+ {runnable_any_proc_p(S1) orelse receivable_any_proc_p(S1), S1};
+run_scheduler(S0, MaxIters) ->
+ S1 = run_scheduler_with_tokens(S0#sched.tokens, S0),
+ if S0#sched.step == S1#sched.step ->
+ %% No work was done on that iteration, need to send 'timeout'?
+ case receivable_any_proc_p(S1) of
+ false ->
+ {false, S1};
+ true ->
+ %% There's at least 1 proc waiting for a timeout message.
+ %% Bummer. Find it/them and get moving again.
+ Waiters = receivable_procs(S1),
+ S2 = lists:foldl(
+ fun(Proc, S) ->
+ bang(scheduler, Proc, timeout, false, S)
+ end, S1, Waiters),
+ run_scheduler(S2, MaxIters - 1)
+ end;
+ true ->
+ run_scheduler(S1, MaxIters - 1)
+ end.
+
+run_scheduler_with_tokens(Tokens, Schedule) ->
+ try
+ lists:foldl(fun(Name, S) ->
+ consume_scheduler_token(Name, S)
+ end, Schedule, Tokens)
+ catch throw:{receive_crash, NewS} ->
+ NewS
+ end.
+
+%% consume_scheduler_token(check_runnable, S) when is_atom(ProcName) ->
+%% {false, S};
+consume_scheduler_token(ProcName, S) when is_atom(ProcName) ->
+ P = fetch_proc(ProcName, S),
+ consume_scheduler_token(P, S, 0).
+
+consume_scheduler_token(_P, S, 3) ->
+ S;
+consume_scheduler_token(P = #proc{mbox = Mbox, outbox = Outbox,
+ delayed = Delayed}, S, IterNum) ->
+ OutNotEmpty = not queue:is_empty(Outbox), % very cheap
+ DelayedNotEmpty = not queue:is_empty(Delayed), % very cheap
+ case P#proc.next of
+ mbox when Mbox /= [] ->
+ NewS = run_proc_receive(P, S),
+ try
+ P1 = fetch_proc(P#proc.name, NewS),
+ if NewS#sched.step /= S#sched.step ->
+ store_proc(rotate_next_type(P1), NewS);
+ true ->
+ consume_scheduler_token(rotate_next_type(P), S, IterNum + 1)
+ end
+ catch
+ error:function_clause ->
+ %% Almost certain cause: the proc's receive pattern failed
+ Name = P#proc.name,
+ NewToks = [T || T <- NewS#sched.tokens, T /= Name],
+ NewS2 = NewS#sched{tokens = NewToks,
+ crashed = [Name|NewS#sched.crashed]},
+ throw({receive_crash, NewS2})
+ end;
+ outbox when OutNotEmpty ->
+ {{value, IMsg}, Q2} = queue:out(P#proc.outbox),
+ NewS = deliver_msg(IMsg, S),
+ store_proc(rotate_next_type(P#proc{outbox = Q2}), incr_step(NewS));
+ delayed when DelayedNotEmpty ->
+ %% TODO: Implement message delays. N.B. message ordering
+ %% between pairs of recipients should be respected
+ %% in order to be properly Erlang'ish.
+ exit(delayed_not_supported);
+ _ ->
+ consume_scheduler_token(rotate_next_type(P), S, IterNum + 1)
+ end.
+
+add_trace(Msg, S) ->
+ S#sched{trace = [Msg|S#sched.trace]}.
+
+%% NOTE: For export to outside world/external API
+
+get_trace(S) ->
+ lists:reverse(S#sched.trace).
+
+get_utrace(S) ->
+ lists:reverse(S#sched.utrace).
+
+get_step(S) ->
+ S#sched.step.
+
+incr_numsent(#sched{numsent = NumSent} = S) ->