diff --git a/prototype/poc-machi/.gitignore b/prototype/poc-machi/.gitignore index 91f0c9c..8b6cb48 100644 --- a/prototype/poc-machi/.gitignore +++ b/prototype/poc-machi/.gitignore @@ -1,5 +1,6 @@ .eunit .eqc-info +concuerror_report.txt current_counterexample.eqc deps ebin/*.beam diff --git a/prototype/poc-machi/Makefile b/prototype/poc-machi/Makefile index c3bdbe5..2a86235 100644 --- a/prototype/poc-machi/Makefile +++ b/prototype/poc-machi/Makefile @@ -24,3 +24,12 @@ eunit: pulse: compile env USE_PULSE=1 $(REBAR_BIN) skip_deps=true clean compile env USE_PULSE=1 $(REBAR_BIN) skip_deps=true -D PULSE eunit + +CONC_ARGS = --pz ./.eunit --treat_as_normal shutdown --after_timeout 1000 + +concuerror: deps compile + $(REBAR_BIN) -v skip_deps=true eunit suites=do_not_exist + concuerror -m machi_flu0_test -t concuerror1_test $(CONC_ARGS) && \ + concuerror -m machi_flu0_test -t concuerror2_test $(CONC_ARGS) && \ + concuerror -m machi_flu0_test -t concuerror3_test $(CONC_ARGS) && \ + concuerror -m machi_flu0_test -t concuerror4_test $(CONC_ARGS) diff --git a/prototype/poc-machi/src/machi_flu0.erl b/prototype/poc-machi/src/machi_flu0.erl new file mode 100644 index 0000000..4e0ccc4 --- /dev/null +++ b/prototype/poc-machi/src/machi_flu0.erl @@ -0,0 +1,86 @@ +-module(machi_flu0). + +-behaviour(gen_server). + +-export([start_link/0, stop/1, + write/2, get/1, trim/1]). +-ifdef(TEST). +-compile(export_all). +-endif. + +-export([init/1, handle_call/3, handle_cast/2, handle_info/2, + terminate/2, code_change/3]). + +-ifdef(TEST). +-include_lib("eunit/include/eunit.hrl"). +-compile(export_all). +-ifdef(PULSE). +-compile({parse_transform, pulse_instrument}). +-endif. +-endif. + +-define(SERVER, ?MODULE). +-define(LONG_TIME, infinity). +%% -define(LONG_TIME, 30*1000). +%% -define(LONG_TIME, 5*1000). + +-type register() :: 'unwritten' | binary() | 'trimmed'. + +-record(state, { + register = 'unwritten' :: register() + }). + +start_link() -> + gen_server:start_link(?MODULE, [], []). + +stop(Pid) -> + gen_server:call(Pid, stop, infinity). + +get(Pid) -> + gen_server:call(Pid, {get}, ?LONG_TIME). + +write(Pid, Bin) when is_binary(Bin) -> + gen_server:call(Pid, {write, Bin}, ?LONG_TIME). + +trim(Pid) -> + gen_server:call(Pid, {trim}, ?LONG_TIME). + +%%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% + +init([]) -> + {ok, #state{}}. + +handle_call({write, Bin}, _From, #state{register=unwritten} = S) -> + {reply, ok, S#state{register=Bin}}; +handle_call({write, _Bin}, _From, #state{register=B} = S) when is_binary(B) -> + {reply, error_written, S}; +handle_call({write, _Bin}, _From, #state{register=trimmed} = S) -> + {reply, error_trimmed, S}; +handle_call({get}, _From, #state{register=Reg} = S) -> + {reply, {ok, Reg}, S}; +handle_call({trim}, _From, #state{register=unwritten} = S) -> + {reply, ok, S#state{register=trimmed}}; +handle_call({trim}, _From, #state{register=B} = S) when is_binary(B) -> + {reply, ok, S#state{register=trimmed}}; +handle_call({trim}, _From, #state{register=trimmed} = S) -> + {reply, error_trimmed, S}; +handle_call(stop, _From, MLP) -> + {stop, normal, ok, MLP}; +handle_call(_Request, _From, MLP) -> + Reply = whaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa, + {reply, Reply, MLP}. + +handle_cast(_Msg, MLP) -> + {noreply, MLP}. + +handle_info(_Info, MLP) -> + {noreply, MLP}. + +terminate(_Reason, _MLP) -> + ok. + +code_change(_OldVsn, MLP, _Extra) -> + {ok, MLP}. + +%%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% + diff --git a/prototype/poc-machi/test/machi_flu0_test.erl b/prototype/poc-machi/test/machi_flu0_test.erl new file mode 100644 index 0000000..ec5bc8b --- /dev/null +++ b/prototype/poc-machi/test/machi_flu0_test.erl @@ -0,0 +1,66 @@ + +-module(machi_flu0_test). + +-ifdef(TEST). +-include_lib("eunit/include/eunit.hrl"). +-compile(export_all). +-endif. + +-ifdef(TEST). +-ifndef(PULSE). + +concuerror1_test() -> + ok. + +concuerror2_test() -> + {ok, F} = machi_flu0:start_link(), + ok = machi_flu0:stop(F), + ok. + +concuerror3_test() -> + Me = self(), + Fun = fun() -> {ok, F1} = machi_flu0:start_link(), + ok = machi_flu0:stop(F1), + Me ! done + end, + P1 = spawn(Fun), + P2 = spawn(Fun), + [receive done -> ok end || _ <- [P1, P2]], + + ok. + +concuerror4_test() -> + {ok, F1} = machi_flu0:start_link(), + Val = <<"val!">>, + ok = machi_flu0:write(F1, Val), + Me = self(), + TrimFun = fun() -> Res = machi_flu0:trim(F1), + Me ! {self(), Res} + end, + TrimPids = [spawn(TrimFun), spawn(TrimFun),spawn(TrimFun)], + TrimExpected = [error_trimmed,error_trimmed,ok], + + GetFun = fun() -> Res = machi_flu0:get(F1), + Me ! {self(), Res} + end, + GetPids = [spawn(GetFun)], + GetExpected = fun(Results) -> + [] = [X || X <- Results, X == unwritten], + ok + end, + + TrimResults = lists:sort([receive + {TrimPid, Res} -> Res + end || TrimPid <- TrimPids]), + TrimExpected = TrimResults, + GetResults = lists:sort([receive + {GetPid, Res} -> Res + end || GetPid <- GetPids]), + ok = GetExpected(GetResults), + + ok = machi_flu0:stop(F1), + ok. + + +-endif. +-endif.