Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
105 lines (99 sloc) 4.39 KB
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.
% cd /path/to/top/of/msgdropsim
% make
% erl -pz ./ebin
(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)
%% Server s1 starts with counter = 2.
%% Server s2 starts with counter = 0.
%% Schedule isn't crazy
%% 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}},
F1 = {1,2,1}
F2 = {[{c1,{counter_op,[s1,s2]}},{c1,{counter_op,[s1,s2]}}],
End2 = {sched,15,6,
%% Here's the system trace, in reverse order. Here's the timeout...
%%% ... and here's the dropped message that creates the timeout @ sim time = 14
%% Here's the user trace, in reverse order.
Runnable = [], Receivable = []
Emitted counters = [2.21,1.2]
per_client_not_retro: failed
Jump to Line
Something went wrong with that request. Please try again.