test/machi_file_proxy_eqc.erl

@@ -62,49 +62,88 @@ csum(Type, Binary) ->
         _ -> machi_util:checksum_chunk(Binary)
     end.
 
+position(P) ->
+    ?LET(O, offset(), P + O).
+
 offset() ->
-%    ?SUCHTHAT(X, oneof([largeint(), int()]), X >= 0).
     ?SUCHTHAT(X, int(), X >= 0).
 
+offset_base() ->
+    elements([4096, 6144, 7168, 8192, 20480, 100000, 1000000]).
+
+big_offset() ->
+    ?LET(P, int(), ?LET(X, offset_base(), P+X)).
+
 len() ->
-%    ?SUCHTHAT(X, oneof([largeint(), int()]), X >= 1).
     ?SUCHTHAT(X, int(), X >= 1).
 
 data_with_csum() ->
     ?LET({B,T},{eqc_gen:largebinary(), csum_type()}, {B,T, csum(T, B)}).
+    %?LET({B,T},{eqc_gen:binary(), csum_type()}, {B,T, csum(T, B)}).
+
+data_with_csum(Limit) ->
+    ?LET({B,T},{?LET(S, Limit, eqc_gen:largebinary(S)), csum_type()}, {B,T, csum(T, B)}).
+    %?LET({B,T},{?LET(S, Limit, eqc_gen:binary(S)), csum_type()}, {B,T, csum(T, B)}).
+
+maybe_gen_valid_write([{Off, L}]) ->
+    {default(Off+L, offset()), len()};
+maybe_gen_valid_write([{O1, L1}, {O2, L2}]) ->
+    Pos = O1 + L1, % end of previous write
+    case Pos == O2 of
+        true ->
+            %% The previous write ended where next write begins, so
+            %% we'll pick the end of the next write and a random length
+            {O2 + L2, len()};
+        false ->
+            {position(O2-Pos), len()}
+    end;
+maybe_gen_valid_write(_) ->
+    {big_offset(), len()}.
+    
     
-small_data() ->
-    ?LET(D, ?SUCHTHAT(S, int(), S >= 1 andalso S < 500), binary(D)).
 
 %% INITIALIZATION
 
 -record(state, {pid, file = 0, written=[]}).
 
-initial_state() -> #state{written=[{0,1023}]}.
+initial_state() -> #state{written=[{0,1024}]}.
 
 %% HELPERS
 
 %% check if an operation is permitted based on whether a write has
 %% occurred
-check_writes([], _Off, _L) ->
+check_writes(_Op, [], _Off, _L) ->
     false;
-check_writes([{Pos, Sz}|_T], Off, L) when Off >= Pos
-                                           andalso Off < (Pos + Sz)
-                                           andalso L < ( Sz - ( Off - Pos ) )->
+check_writes(_Op, [{Pos, Sz}|_T], Off, L) when Pos == Off 
+                                          andalso Sz == L ->
+    mostly_true;
+check_writes(read, [{Pos, Sz}|_T], Off, L) when Off >= Pos 
+                                          andalso Off < (Pos + Sz) 
+                                          andalso Sz >= ( L - ( Off - Pos ) ) ->
     true;
-check_writes([{Pos, Sz}|_T], Off, _L) when Off > ( Pos + Sz ) ->
-    false;
-check_writes([_H|T], Off, L) ->
-    check_writes(T, Off, L).
+check_writes(write, [{Pos, Sz}|_T], Off, L) when ( Off + L ) > Pos 
+                                                 andalso Off < (Pos + Sz) ->
+    true;
+check_writes(Op, [_H|T], Off, L) ->
+    check_writes(Op, T, Off, L).
 
 is_error({error, _}) -> true;
 is_error({error, _, _}) -> true;
 is_error(Other) -> {expected_ERROR, Other}.
 
+probably_error(ok) -> true;
+probably_error(V) -> is_error(V).
+
 is_ok({ok, _, _}) -> true;
 is_ok(ok) -> true;
 is_ok(Other) -> {expected_OK, Other}.
 
+get_offset({ok, _Filename, Offset}) -> Offset;
+get_offset(_) -> error(badarg).
+
+offset_valid(Offset, L) ->
+    {Pos, Sz} = lists:last(L),
+    Offset == Pos + Sz.
 
 -define(TESTDIR, "./eqc").
 
@@ -144,14 +183,14 @@ read_args(S) ->
 
 read_ok(S, Off, L) ->
     case S#state.written of
-        [] -> false;
-        [{0, 1023}] -> false;
-        W -> check_writes(W, Off, L)
+        [{0, 1024}] -> false;
+        W -> check_writes(read, W, Off, L)
     end.
 
 read_post(S, [_Pid, Off, L], Res) ->
     case read_ok(S, Off, L) of
         true -> is_ok(Res);
+        mostly_true -> is_ok(Res);
         false -> is_error(Res)
     end.
 
@@ -165,8 +204,15 @@ read(Pid, Offset, Length) ->
 write_pre(S) ->
     S#state.pid /= undefined.
 
+%% do not allow writes with empty data
+write_pre(_S, [_Pid, _Extra, {<<>>, _Tag, _Csum}]) ->
+    false;
+write_pre(_S, _Args) ->
+    true.
+
 write_args(S) ->
-    [S#state.pid, offset(), data_with_csum()].
+    %{Offset, Length} = maybe_gen_valid_write(S#state.written),
+    [S#state.pid, big_offset(), data_with_csum()].
 
 write_ok(_S, [_Pid, Off, _Data]) when Off < 1024 -> false;
 write_ok(S, [_Pid, Off, {Bin, _Tag, _Csum}]) ->
@@ -174,17 +220,31 @@ write_ok(S, [_Pid, Off, {Bin, _Tag, _Csum}]) ->
     %% Check writes checks if a byte range is *written*
     %% So writes are ok IFF they are NOT written, so
     %% we want not check_writes/3 to be true.
-    not check_writes(S#state.written, Off, Size).
+    check_writes(write, S#state.written, Off, Size).
 
 write_post(S, Args, Res) ->
     case write_ok(S, Args) of
-        true -> eq(Res, ok);
-        false -> is_error(Res)
+        %% false means this range has NOT been written before, so
+        %% it should succeed
+        false -> eq(Res, ok);
+        %% mostly true means we've written this range before BUT
+        %% as a special case if we get a call to write the EXACT
+        %% same data that's already on the disk, we return "ok"
+        %% instead of {error, written}.
+        mostly_true -> probably_error(Res); 
+        %% If we get true, then we've already written this section 
+        %% or a portion of this range to disk and should return an 
+        %% error.
+        true -> is_error(Res)
     end.
 
-write_next(S, ok, [_Pid, Offset, {Bin, _Tag, _Csum}]) ->
-    S#state{written = lists:sort(S#state.written ++ [{Offset, iolist_size(Bin)}])};
-write_next(S, _Res, _Args) -> S.
+write_next(S, Res, [_Pid, Offset, {Bin, _Tag, _Csum}]) ->
+    case is_ok(Res) of
+        true -> 
+            S#state{written = lists:sort(S#state.written ++ [{Offset, iolist_size(Bin)}])};
+        _ -> 
+            S
+    end.
 
 write(Pid, Offset, {Bin, Tag, Csum}) ->
     Meta = [{client_csum_tag, Tag},
@@ -192,11 +252,16 @@ write(Pid, Offset, {Bin, Tag, Csum}) ->
     machi_file_proxy:write(Pid, Offset, Meta, Bin).
 
 %% append
-%% TODO - ensure offset is expected offset
 
 append_pre(S) ->
     S#state.pid /= undefined.
 
+%% do not allow appends with empty binary data
+append_pre(_S, [_Pid, _Extra, {<<>>, _Tag, _Csum}]) ->
+    false;
+append_pre(_S, _Args) ->
+    true.
+
 append_args(S) ->
     [S#state.pid, default(0, len()), data_with_csum()].
 
@@ -205,22 +270,27 @@ append(Pid, Extra, {Bin, Tag, Csum}) ->
             {client_csum, Csum}],
     machi_file_proxy:append(Pid, Meta, Extra, Bin).
 
-append_next(S, {ok, _File, Offset}, [_Pid, _Extra, {Bin, _Tag, _Csum}]) ->
-    S#state{written = lists:sort(S#state.written ++ [{Offset, iolist_size(Bin)}])};
-append_next(S, _Res, _Args) -> S.
+append_next(S, Res, [_Pid, _Extra, {Bin, _Tag, _Csum}]) ->
+    case is_ok(Res) of
+        true -> 
+            Offset = get_offset(Res),
+            true == offset_valid(Offset, S#state.written),
+            S#state{written = lists:sort(S#state.written ++ [{Offset, iolist_size(Bin)}])};
+        _ ->
+            S
+    end.
 
 %% appends should always succeed unless the disk is full 
 %% or there's a hardware failure.
 append_post(_S, _Args, Res) ->
-    is_ok(Res).
+    true == is_ok(Res).
 
 %% Property
 
 prop_ok() ->
+  cleanup(),
   ?FORALL(Cmds, commands(?MODULE),
   begin
-    cleanup(),
-    %io:format(user, "Commands: ~p~n", [Cmds]),
     {H, S, Res} = run_commands(?MODULE, Cmds),
     pretty_commands(?MODULE, Cmds, {H, S, Res},
       aggregate(command_names(Cmds), Res == ok))