diff --git a/README.md b/README.md index bc80cd8..3efe52a 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ A Causal-Consistent Reversible Debugger for Erlang. -[![Erlang](https://img.shields.io/badge/Erlang%2FOTP-23.0-blue?logo=erlang)](https://www.erlang.org/) +[![Erlang](https://img.shields.io/badge/Erlang%2FOTP-25.0-blue?logo=erlang)](https://www.erlang.org/) [![GitHub Actions](https://img.shields.io/github/workflow/status/mistupv/cauder/Test?label=test&logo=github)](https://github.com/mistupv/cauder/actions/workflows/erlang.yml) [![License](https://img.shields.io/github/license/mistupv/cauder?label=License&logo=data:image/svg+xml;base64,PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz48IURPQ1RZUEUgc3ZnIFBVQkxJQyAiLS8vVzNDLy9EVEQgU1ZHIDEuMS8vRU4iICJodHRwOi8vd3d3LnczLm9yZy9HcmFwaGljcy9TVkcvMS4xL0RURC9zdmcxMS5kdGQiPjxzdmcgeG1sbnM9Imh0dHA6Ly93d3cudzMub3JnLzIwMDAvc3ZnIiB4bWxuczp4bGluaz0iaHR0cDovL3d3dy53My5vcmcvMTk5OS94bGluayIgdmVyc2lvbj0iMS4xIiB3aWR0aD0iMjQiIGhlaWdodD0iMjQiIHZpZXdCb3g9IjAgMCAyNCAyNCI+PHBhdGggZmlsbD0iI0Y1RjVGNSIgZD0iTTEyLDNDMTAuNzMsMyA5LjYsMy44IDkuMTgsNUgzVjdINC45NUwyLDE0QzEuNTMsMTYgMywxNyA1LjUsMTdDOCwxNyA5LjU2LDE2IDksMTRMNi4wNSw3SDkuMTdDOS41LDcuODUgMTAuMTUsOC41IDExLDguODNWMjBIMlYyMkgyMlYyMEgxM1Y4LjgyQzEzLjg1LDguNSAxNC41LDcuODUgMTQuODIsN0gxNy45NUwxNSwxNEMxNC41MywxNiAxNiwxNyAxOC41LDE3QzIxLDE3IDIyLjU2LDE2IDIyLDE0TDE5LjA1LDdIMjFWNUgxNC44M0MxNC40LDMuOCAxMy4yNywzIDEyLDNNMTIsNUExLDEgMCAwLDEgMTMsNkExLDEgMCAwLDEgMTIsN0ExLDEgMCAwLDEgMTEsNkExLDEgMCAwLDEgMTIsNU01LjUsMTAuMjVMNywxNEg0TDUuNSwxMC4yNU0xOC41LDEwLjI1TDIwLDE0SDE3TDE4LjUsMTAuMjVaIiAvPjwvc3ZnPg==)](https://github.com/mistupv/cauder/blob/dev/LICENSE) diff --git a/case-studies/math_server/info.txt b/case-studies/math_server/info.txt new file mode 100644 index 0000000..dfb59a4 --- /dev/null +++ b/case-studies/math_server/info.txt @@ -0,0 +1,5 @@ +Example described in the chapter on debugging in the final book of +COST Action 1405, which is to appear. +A copy of the chapter is available in this directory. + + diff --git a/case-studies/math_server/math_server.erl b/case-studies/math_server/math_server.erl new file mode 100644 index 0000000..8fa9304 --- /dev/null +++ b/case-studies/math_server/math_server.erl @@ -0,0 +1,59 @@ +-module(math_server). +-export([main/1, server/0, logger/2, square/0, log/0, adder/0, sendRequest/1]). +%[{square, 10}, {adder, 20}, {log, 100}, {adder, 30}, {adder, 100}] +%casestudy:main([{square, 10}, {adder, 20}, {log, 100}, {adder, 30}, {adder, 100}]). +%casestudy:sendRequest([{square, 10}, {adder, 20}, {log, 100}, {adder, 30}, {adder, 100}]). + + +main(A)-> + register(server,spawn(?MODULE, server,[])), + register(log,spawn(?MODULE, logger,[0,[]])), + sendRequest(A). + +server() -> + receive + {logged,{Res,Time}} -> + io:format("LOGGED ~p TIME:~p\n", [Res,Time]); + {reply, Res} -> + io:format("RESULT:~p\n", [Res]), + log ! Res; + {Atom, Val} -> + io:format("SEND REQUEST:~p\n", [{Atom, Val}]), + case whereis(Atom) of + undefined -> + register(Atom,spawn(?MODULE, Atom,[])), + Atom ! Val; + _ -> + Atom ! Val + end + end, + server(). + +logger(N,L)-> + receive + Val -> + server ! {logged,{Val, N}}, logger(N+1,L++[Val]) + end. + +square() -> + receive + N -> + server ! {reply,{square,N*N}}, square() + end. + +log() -> + receive + N -> + server ! {reply,{log,math:log10(N)}}, log() + end. + +adder() -> adder(0). +adder(N)-> + receive + Val -> + server ! {reply,{adder,Val + N}}, adder(Val + N) + end. + +sendRequest([]) -> ok; +sendRequest([El | T]) -> + server ! El, sendRequest(T). diff --git a/elvis.config b/elvis.config index a8ec861..c07cf70 100644 --- a/elvis.config +++ b/elvis.config @@ -11,7 +11,7 @@ {elvis_style, nesting_level, #{level => 5}}, % TODO Enable and fix warnings {elvis_style, dont_repeat_yourself, disable}, - {elvis_style, max_module_length}, + {elvis_style, max_module_length, disable}, % TODO Use logging module {elvis_style, no_debug_call, disable}, {elvis_style, no_common_caveats_call}, diff --git a/examples/math_server.erl b/examples/math_server.erl new file mode 100644 index 0000000..774e63a --- /dev/null +++ b/examples/math_server.erl @@ -0,0 +1,59 @@ +-module(math_server). +-export([main/1, server/0, logger/2, square/0, log/0, adder/0, sendRequest/1]). +%[{square, 10}, {adder, 20}, {log, 100}, {adder, 30}, {adder, 100}] +%casestudy:main([{square, 10}, {adder, 20}, {log, 100}, {adder, 30}, {adder, 100}]). +%casestudy:sendRequest([{square, 10}, {adder, 20}, {log, 100}, {adder, 30}, {adder, 100}]). + + +main(A)-> + register(server,spawn(?MODULE, server,[])), + register(log,spawn(?MODULE, logger,[0,[]])), + sendRequest(A). + +server() -> + receive + {logged,{Res,Time}} -> + io:format("LOGGED ~p TIME:~p\n", [Res,Time]); + {reply, Res} -> + io:format("RESULT:~p\n", [Res]), + log ! Res; + {Atom, Val} -> + io:format("SEND REQUEST:~p\n", [{Atom, Val}]), + case whereis(Atom) of + undefined -> + register(Atom,spawn(?MODULE, Atom,[])), + Atom ! Val; + _ -> + Atom ! Val + end + end, + server(). + +logger(N,L)-> + receive + Val -> + server ! {logged,{Val, N}}, logger(N+1,L++[Val]) + end. + +square() -> + receive + N -> + server ! {reply,{square,N*N}}, square() + end. + +log() -> + receive + N -> + server ! {reply,{log,math:log10(N)}}, log() + end. + +adder() -> adder(0). +adder(N)-> + receive + Val -> + server ! {reply,{addder,Val + N}}, adder(Val + N) + end. + +sendRequest([]) -> ok; +sendRequest([El | T]) -> + server ! El, sendRequest(T). diff --git a/include/cauder_eval.hrl b/include/cauder_eval.hrl index 30d807c..78e90aa 100644 --- a/include/cauder_eval.hrl +++ b/include/cauder_eval.hrl @@ -14,7 +14,7 @@ -record(label_start, { var :: cauder_syntax:af_variable(), - name :: atom(), + name :: atom() | list(), host :: 'undefined' | atom() }). @@ -33,7 +33,7 @@ }). -record(label_send, { - dst :: cauder_process:id(), + dst :: cauder_process:id() | atom(), val :: term() }). @@ -42,6 +42,26 @@ clauses :: cauder_syntax:af_clause_seq() }). +-record(label_registered, { + var :: cauder_syntax:af_variable() +}). + +-record(label_whereis, { + var :: cauder_syntax:af_variable(), + atom :: atom() +}). + +-record(label_register, { + var :: cauder_syntax:af_variable(), + atom :: atom(), + pid :: cauder_process:id() +}). + +-record(label_unregister, { + var :: cauder_syntax:af_variable(), + atom :: atom() +}). + -record(result, { env :: cauder_bindings:bindings(), expr :: [cauder_syntax:abstract_expr()], diff --git a/include/cauder_history.hrl b/include/cauder_history.hrl index c8d3a95..7db5c61 100644 --- a/include/cauder_history.hrl +++ b/include/cauder_history.hrl @@ -36,8 +36,8 @@ expr :: [cauder_syntax:abstract_expr()], stack :: cauder_stack:stack(), node :: node(), - pid :: cauder_process:id() - %success :: boolean() % TODO + pid :: cauder_process:id(), + success :: boolean() }). -record(hist_send, { @@ -54,3 +54,56 @@ msg :: cauder_message:message(), q_pos :: pos_integer() }). + +-record(hist_regS, { + env :: cauder_bindings:bindings(), + expr :: [cauder_syntax:abstract_expr()], + stack :: cauder_stack:stack(), + mapEl :: cauder_map:map_element(), + node :: node() +}). + +-record(hist_del, { + env :: cauder_bindings:bindings(), + expr :: [cauder_syntax:abstract_expr()], + stack :: cauder_stack:stack(), + mapEl :: cauder_map:map_element(), + map :: [cauder_map:map_element()], + node :: node() +}). + +-record(hist_readS, { + env :: cauder_bindings:bindings(), + expr :: [cauder_syntax:abstract_expr()], + stack :: cauder_stack:stack(), + atom :: atom(), + pid :: cauder_process:id(), + mapEl :: [cauder_map:map_element()], + node :: node() +}). + +-record(hist_readF, { + env :: cauder_bindings:bindings(), + expr :: [cauder_syntax:abstract_expr()], + stack :: cauder_stack:stack(), + atom :: atom() | cauder_process:id(), + mapGhost :: [cauder_map:map_element()], + node :: node() +}). + +-record(hist_sendA, { + env :: cauder_bindings:bindings(), + expr :: [cauder_syntax:abstract_expr()], + stack :: cauder_stack:stack(), + msg :: cauder_message:message(), + mapEl :: cauder_map:map_element(), + node :: node() +}). + +-record(hist_registered, { + env :: cauder_bindings:bindings(), + expr :: [cauder_syntax:abstract_expr()], + stack :: cauder_stack:stack(), + map :: [cauder_map:map_element()], + node :: node() +}). diff --git a/include/cauder_log.hrl b/include/cauder_log.hrl index 81c7ea2..f1ef553 100644 --- a/include/cauder_log.hrl +++ b/include/cauder_log.hrl @@ -20,3 +20,28 @@ -record(log_receive, { uid :: cauder_message:uid() }). + +-record(log_del, { + key :: cauder_map:key(), + atom :: atom(), + pid :: cauder_process:id(), + map :: [cauder_map:map_element()] +}). + +-record(log_reg, { + key :: cauder_map:key(), + atom :: atom(), + pid :: cauder_process:id(), + map :: [cauder_map:map_element()] +}). + +-record(log_sendA, { + uid :: cauder_message:uid(), + el :: cauder_map:map_element() +}). + +-record(log_read, { + atom :: atom(), + pid :: cauder_process:id() | undefined, + map :: [cauder_map:map_element()] +}). diff --git a/include/cauder_process.hrl b/include/cauder_process.hrl index 960df85..a971544 100644 --- a/include/cauder_process.hrl +++ b/include/cauder_process.hrl @@ -5,7 +5,8 @@ env = cauder_bindings:new() :: cauder_bindings:bindings(), expr :: [cauder_syntax:abstract_expr()], stack = cauder_stack:new() :: cauder_stack:stack(), - hist = cauder_history:new() :: cauder_history:history() + hist = cauder_history:new() :: cauder_history:history(), + is_alive = true :: boolean() }). -define(SCHEDULER_RoundRobin, round_robin). diff --git a/include/cauder_semantics.hrl b/include/cauder_semantics.hrl index e1e18e5..af7f76e 100644 --- a/include/cauder_semantics.hrl +++ b/include/cauder_semantics.hrl @@ -9,3 +9,6 @@ -define(RULE_START, 'start'). -define(RULE_SEND, 'send'). -define(RULE_RECEIVE, 'receive'). +-define(RULE_READ, 'read'). +-define(RULE_REG, 'register'). +-define(RULE_DEL, 'del'). diff --git a/include/cauder_system.hrl b/include/cauder_system.hrl index 7fe34eb..6de2407 100644 --- a/include/cauder_system.hrl +++ b/include/cauder_system.hrl @@ -2,6 +2,7 @@ mail = cauder_mailbox:new() :: cauder_mailbox:mailbox(), pool :: cauder_pool:pool(), nodes = [] :: [node()], + maps = [] :: [{cauder_map:map_node()}], log = cauder_log:new() :: cauder_log:log(), trace = cauder_trace:new() :: cauder_trace:trace(), % TODO Remove? diff --git a/include/cauder_trace.hrl b/include/cauder_trace.hrl index ca7b4b0..e64a593 100644 --- a/include/cauder_trace.hrl +++ b/include/cauder_trace.hrl @@ -25,3 +25,28 @@ -record(trace_receive, { uid :: cauder_message:uid() }). + +-record(trace_del, { + key :: cauder_map:key(), + atom :: atom(), + pid :: cauder_process:id(), + map :: [cauder_map:map_element()] +}). + +-record(trace_reg, { + key :: cauder_map:key(), + atom :: atom(), + pid :: cauder_process:id(), + map :: [cauder_map:map_element()] +}). + +-record(trace_sendA, { + uid :: cauder_message:uid(), + el :: cauder_map:map_element() +}). + +-record(trace_read, { + atom :: atom(), + pid :: cauder_process:id() | undefined, + map :: [cauder_map:map_element()] +}). diff --git a/src/cauder.erl b/src/cauder.erl index eb31296..51f1533 100644 --- a/src/cauder.erl +++ b/src/cauder.erl @@ -28,6 +28,8 @@ replay_spawn/1, replay_send/1, replay_receive/1, + replay_register/1, + replay_delete/1, replay_full_log/0 ]). % Rollback actions @@ -36,8 +38,11 @@ rollback_start/1, rollback_spawn/1, rollback_send/1, + %rollback_senda/1, rollback_receive/1, - rollback_variable/1 + rollback_variable/1, + rollback_reg/1, + rollback_del/1 ]). -export([resume/1, cancel/0]). -export([get_entry_points/1, get_system/0, get_path/0]). @@ -366,6 +371,40 @@ replay_send(Uid) -> gen_server:call(?SERVER, {user, {replay_send, Uid}}). replay_receive(Uid) -> gen_server:call(?SERVER, {user, {replay_receive, Uid}}). +%%------------------------------------------------------------------------------ +%% @doc Replays the reception of the message with the given uid. +%% +%% This is an asynchronous action: if the server accepts the task then the tuple +%% `{ok, CurrentSystem}' is returned, where `CurrentSystem' is the current +%% system prior to executing this action, otherwise the atom `busy' is returned, +%% to indicate that the server is currently executing a different task. +%% +%% @see task_replay_register/2 + +-spec replay_register(El) -> Reply when + El :: cauder_map:map_element(), + Reply :: {ok, CurrentSystem} | busy, + CurrentSystem :: cauder_system:system(). + +replay_register({A,B,C}) -> gen_server:call(?SERVER, {user, {replay_register, {A,B,C,top}}}). + +%%------------------------------------------------------------------------------ +%% @doc Replays the reception of the message with the given uid. +%% +%% This is an asynchronous action: if the server accepts the task then the tuple +%% `{ok, CurrentSystem}' is returned, where `CurrentSystem' is the current +%% system prior to executing this action, otherwise the atom `busy' is returned, +%% to indicate that the server is currently executing a different task. +%% +%% @see task_replay_delete/2 + +-spec replay_delete(El) -> Reply when + El :: cauder_map:map_element(), + Reply :: {ok, CurrentSystem} | busy, + CurrentSystem :: cauder_system:system(). + +replay_delete({A,B,C}) -> gen_server:call(?SERVER, {user, {replay_delete, {A,B,C,bot}}}). + %%------------------------------------------------------------------------------ %% @doc Replays the full log. %% @@ -453,6 +492,23 @@ rollback_spawn(Pid) -> gen_server:call(?SERVER, {user, {rollback_spawn, Pid}}). rollback_send(Uid) -> gen_server:call(?SERVER, {user, {rollback_send, Uid}}). +%%------------------------------------------------------------------------------ +%% @doc Rolls back the sending of the message with the given uid. +%% +%% This is an asynchronous action: if the server accepts the task then the tuple +%% `{ok, CurrentSystem}' is returned, where `CurrentSystem' is the current +%% system prior to executing this action, otherwise the atom `busy' is returned, +%% to indicate that the server is currently executing a different task. +%% +%% @see task_rollback_senda/2 + +%-spec rollback_senda(Uid) -> Reply when +% Uid :: cauder_message:uid(), +% Reply :: {ok, CurrentSystem} | busy, +% CurrentSystem :: cauder_system:system(). + +%rollback_senda(Uid) -> gen_server:call(?SERVER, {user, {rollback_senda, Uid}}). + %%------------------------------------------------------------------------------ %% @doc Rolls back the reception of the message with the given uid. %% @@ -470,6 +526,40 @@ rollback_send(Uid) -> gen_server:call(?SERVER, {user, {rollback_send, Uid}}). rollback_receive(Uid) -> gen_server:call(?SERVER, {user, {rollback_receive, Uid}}). +%%------------------------------------------------------------------------------ +%% @doc Rolls back +%% +%% This is an asynchronous action: if the server accepts the task then the tuple +%% `{ok, CurrentSystem}' is returned, where `CurrentSystem' is the current +%% system prior to executing this action, otherwise the atom `busy' is returned, +%% to indicate that the server is currently executing a different task. +%% +%% @see task_rollback_reg/2 + +-spec rollback_reg(El) -> Reply when + El :: cauder_map:map_element(), + Reply :: {ok, CurrentSystem} | busy, + CurrentSystem :: cauder_system:system(). + +rollback_reg(El) -> gen_server:call(?SERVER, {user, {rollback_reg, El}}). + +%%------------------------------------------------------------------------------ +%% @doc Rolls back +%% +%% This is an asynchronous action: if the server accepts the task then the tuple +%% `{ok, CurrentSystem}' is returned, where `CurrentSystem' is the current +%% system prior to executing this action, otherwise the atom `busy' is returned, +%% to indicate that the server is currently executing a different task. +%% +%% @see task_rollback_del/2 + +-spec rollback_del(El) -> Reply when + El :: cauder_map:map_element(), + Reply :: {ok, CurrentSystem} | busy, + CurrentSystem :: cauder_system:system(). + +rollback_del(El) -> gen_server:call(?SERVER, {user, {rollback_del, El}}). + %%------------------------------------------------------------------------------ %% @doc Rolls back the binding of the variable with the given name. %% @@ -626,6 +716,7 @@ handle_call({user, stop}, {FromPid, _}, #state{system = System, task = Task} = S ets:delete(?APP_DB, last_pid), ets:delete(?APP_DB, last_uid), ets:delete(?APP_DB, last_var), + ets:delete(?APP_DB, last_key), % TODO Add dialog when UI receives this message [Sub ! {dbg, stop} || Sub <- State#state.subs, Sub =/= FromPid], {reply, {ok, System}, State#state{system = undefined, task = undefined}}; @@ -670,12 +761,17 @@ handle_call({user, {Task, Args}}, _From, #state{system = System} = State) -> replay_spawn -> fun task_replay_spawn/2; replay_send -> fun task_replay_send/2; replay_receive -> fun task_replay_receive/2; + replay_register -> fun task_replay_register/2; + replay_delete -> fun task_replay_delete/2; replay_full_log -> fun task_replay_full_log/2; rollback_steps -> fun task_rollback_steps/2; rollback_start -> fun task_rollback_start/2; rollback_spawn -> fun task_rollback_spawn/2; rollback_send -> fun task_rollback_send/2; + rollback_senda -> fun task_rollback_senda/2; rollback_receive -> fun task_rollback_receive/2; + rollback_reg -> fun task_rollback_reg/2; + rollback_del -> fun task_rollback_del/2; rollback_variable -> fun task_rollback_variable/2 end, Pid = run_task(Fun, Args, System), @@ -956,6 +1052,40 @@ task_replay_receive(Uid, Sys0) -> {success, Uid, Time, Sys1}. +-spec task_replay_register(El, System) -> task_result(El) when + El :: cauder_map:map_element(), + System :: cauder_system:system(). + +task_replay_register(El, Sys0) -> + {Time, Sys1} = + timer:tc( + fun() -> + case cauder_replay:can_replay_register(El, Sys0) of + false -> error(no_replay); + true -> cauder_replay:replay_register(El, Sys0) + end + end + ), + + {success, El, Time, Sys1}. + +-spec task_replay_delete(El, System) -> task_result(El) when + El :: cauder_map:map_element(), + System :: cauder_system:system(). + +task_replay_delete(El, Sys0) -> + {Time, Sys1} = + timer:tc( + fun() -> + case cauder_replay:can_replay_delete(El, Sys0) of + false -> error(no_replay); + true -> cauder_replay:replay_delete(El, Sys0) + end + end + ), + + {success, El, Time, Sys1}. + -spec task_replay_full_log([], System) -> task_result() when System :: cauder_system:system(). @@ -1020,8 +1150,30 @@ task_rollback_send(Uid, Sys0) -> timer:tc( fun() -> case cauder_rollback:can_rollback_send(Uid, Sys0) of + false -> + case cauder_rollback:can_rollback_senda(Uid, Sys0) of + false -> error(no_rollback); + true -> cauder_rollback:rollback_senda(Uid, Sys0) + end; + true -> + cauder_rollback:rollback_send(Uid, Sys0) + end + end + ), + + {success, Uid, Time, Sys1}. + +-spec task_rollback_senda(Uid, System) -> task_result(Uid) when + Uid :: cauder_message:uid(), + System :: cauder_system:system(). + +task_rollback_senda(Uid, Sys0) -> + {Time, Sys1} = + timer:tc( + fun() -> + case cauder_rollback:can_rollback_senda(Uid, Sys0) of false -> error(no_rollback); - true -> cauder_rollback:rollback_send(Uid, Sys0) + true -> cauder_rollback:rollback_senda(Uid, Sys0) end end ), @@ -1045,6 +1197,40 @@ task_rollback_receive(Uid, Sys0) -> {success, Uid, Time, Sys1}. +-spec task_rollback_reg(El, System) -> task_result(El) when + El :: cauder_map:map_element(), + System :: cauder_system:system(). + +task_rollback_reg(El, Sys0) -> + {Time, Sys1} = + timer:tc( + fun() -> + case cauder_rollback:can_rollback_reg(El, Sys0) of + false -> error(no_rollback); + true -> cauder_rollback:rollback_reg(El, Sys0) + end + end + ), + + {success, El, Time, Sys1}. + +-spec task_rollback_del(El, System) -> task_result(El) when + El :: cauder_map:map_element(), + System :: cauder_system:system(). + +task_rollback_del(El, Sys0) -> + {Time, Sys1} = + timer:tc( + fun() -> + case cauder_rollback:can_rollback_del(El, Sys0) of + false -> error(no_rollback); + true -> cauder_rollback:rollback_del(El, Sys0) + end + end + ), + + {success, El, Time, Sys1}. + -spec task_rollback_variable(Name, System) -> task_result(Name) when Name :: atom(), System :: cauder_system:system(). diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 620882e..bc7a6e6 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -22,7 +22,11 @@ | label_spawn_fun() | label_spawn_mfa() | label_send() - | label_receive(). + | label_receive() + | label_registered() + | label_whereis() + | label_register() + | label_unregister(). -type label_tau() :: #label_tau{}. -type label_self() :: #label_self{}. @@ -33,6 +37,10 @@ -type label_spawn_mfa() :: #label_spawn_mfa{}. -type label_send() :: #label_send{}. -type label_receive() :: #label_receive{}. +-type label_registered() :: #label_registered{}. +-type label_whereis() :: #label_whereis{}. +-type label_register() :: #label_register{}. +-type label_unregister() :: #label_unregister{}. %%%============================================================================= %%% API @@ -237,6 +245,42 @@ expr(Bs, {nodes, Line}, Stk) -> Var = cauder_utils:temp_variable(Line), Label = #label_nodes{var = Var}, #result{env = Bs, expr = [Var], stack = Stk, label = Label}; +expr(Bs, {registered, Line}, Stk) -> + Var = cauder_utils:temp_variable(Line), + Label = #label_registered{var = Var}, + #result{env = Bs, expr = [Var], stack = Stk, label = Label}; +expr(Bs, E = {whereis, Line, Atom}, Stk) -> + case is_reducible(Atom, Bs) of + true -> + eval_and_update({Bs, Atom, Stk}, {3, E}); + false -> + Var = cauder_utils:temp_variable(Line), + Label = #label_whereis{var = Var, atom = concrete(Atom)}, + #result{env = Bs, expr = [Var], stack = Stk, label = Label} + end; +expr(Bs, E = {register, Line, Atom, Pid}, Stk) -> + case is_reducible(Atom, Bs) of + true -> + eval_and_update({Bs, Atom, Stk}, {3, E}); + false -> + case is_reducible(Pid, Bs) of + true -> + eval_and_update({Bs, Pid, Stk}, {4, E}); + false -> + Var = cauder_utils:temp_variable(Line), + Label = #label_register{var = Var, atom = concrete(Atom), pid = concrete(Pid)}, + #result{env = Bs, expr = [Var], stack = Stk, label = Label} + end + end; +expr(Bs, E = {unregister, Line, Atom}, Stk) -> + case is_reducible(Atom, Bs) of + true -> + eval_and_update({Bs, Atom, Stk}, {3, E}); + false -> + Var = cauder_utils:temp_variable(Line), + Label = #label_unregister{var = Var, atom = concrete(Atom)}, + #result{env = Bs, expr = [Var], stack = Stk, label = Label} + end; expr(Bs, E = {spawn, Line, Fun}, Stk) -> case is_reducible(Fun, Bs) of true -> diff --git a/src/cauder_history.erl b/src/cauder_history.erl index 493cb81..46f7eb8 100644 --- a/src/cauder_history.erl +++ b/src/cauder_history.erl @@ -15,7 +15,13 @@ has_failed_start/2, has_spawn/2, has_send/2, - has_receive/2 + has_receive/2, + has_read_map/2, + has_fail_read_map/2, + has_registered/2, + has_reg/2, + has_del/2, + has_senda/2 ]). -export([ group_actions/1, @@ -36,7 +42,13 @@ | entry_start() | entry_spawn() | entry_send() - | entry_receive(). + | entry_receive() + | entry_readS() + | entry_readF() + | entry_registered() + | entry_regS() + | entry_del() + | entry_sendA(). -type entry_tau() :: #hist_tau{}. -type entry_self() :: #hist_self{}. @@ -46,6 +58,12 @@ -type entry_spawn() :: #hist_spawn{}. -type entry_send() :: #hist_send{}. -type entry_receive() :: #hist_receive{}. +-type entry_readS() :: #hist_readS{}. +-type entry_readF() :: #hist_readF{}. +-type entry_registered() :: #hist_registered{}. +-type entry_regS() :: #hist_regS{}. +-type entry_del() :: #hist_del{}. +-type entry_sendA() :: #hist_sendA{}. %%%============================================================================= %%% API @@ -133,6 +151,14 @@ has_send(_, []) -> false; has_send(Uid, [#hist_send{msg = #message{uid = Uid}} | _]) -> true; has_send(Uid, [_ | H]) -> has_send(Uid, H). +-spec has_senda(Uid, History) -> boolean() when + Uid :: cauder_message:uid(), + History :: cauder_history:history(). + +has_senda(_, []) -> false; +has_senda(Uid, [#hist_sendA{msg = #message{uid = Uid}} | _]) -> true; +has_senda(Uid, [_ | H]) -> has_senda(Uid, H). + -spec has_receive(Uid, History) -> boolean() when Uid :: cauder_message:uid(), History :: cauder_history:history(). @@ -141,6 +167,88 @@ has_receive(_, []) -> false; has_receive(Uid, [#hist_receive{msg = #message{uid = Uid}} | _]) -> true; has_receive(Uid, [_ | H]) -> has_receive(Uid, H). +-spec has_reg(El, History) -> boolean() when + El :: cauder_map:map_element(), + History :: cauder_history:history(). + +has_reg(_, []) -> false; +has_reg(El, [#hist_regS{mapEl = El} | _]) -> true; +has_reg(El, [_ | H]) -> has_reg(El, H). + +-spec has_del(El, History) -> boolean() when + El :: cauder_map:map_element(), + History :: cauder_history:history(). + +has_del(_, []) -> false; +has_del(El, [#hist_del{mapEl = El} | _]) -> true; +has_del(El, [_ | H]) -> has_del(El, H). + +%%------------------------------------------------------------------------------ +%% @doc Checks whether the given history contains a read of `element' by checking +%% the history items 'read1', 'registered' or 'sendS' + +-spec has_read_map(History, El) -> boolean() when + History :: cauder_history:history(), + El :: cauder_map:map_element(). + +has_read_map([], _) -> + false; +has_read_map([#hist_readS{mapEl = SubMap} | H], El) -> + case cauder_map:is_in_map(SubMap, El) of + true -> true; + false -> has_read_map(H, El) + end; +has_read_map([#hist_sendA{mapEl = SubMap} | H], El) -> + case cauder_map:is_in_map([SubMap], El) of + true -> true; + false -> has_read_map(H, El) + end; +has_read_map([#hist_registered{map = SubMap} | H], El) -> + case cauder_map:is_in_map(SubMap, El) of + true -> true; + false -> has_read_map(H, El) + end; +has_read_map([_ | H], El) -> + has_read_map(H, El). + +%%------------------------------------------------------------------------------ +%% @doc Checks whether the given history contains a fail read of `element' by checking +%% the history item 'readF' + +-spec has_fail_read_map(History, El) -> boolean() when + History :: cauder_history:history(), + El :: cauder_map:map_element(). + +has_fail_read_map([], _) -> + false; +has_fail_read_map([#hist_readF{mapGhost = SubMap} | H], El) -> + case cauder_map:is_in_map(SubMap, El) of + true -> true; + false -> has_fail_read_map(H, El) + end; +has_fail_read_map([#hist_registered{map = SubMap} | H], El) -> + case cauder_map:is_in_map(SubMap, El) of + true -> true; + false -> has_fail_read_map(H, El) + end; +has_fail_read_map([_ | H], El) -> + has_fail_read_map(H, El). + +%%------------------------------------------------------------------------------ +%% @doc Checks whether the given history contains a read of `element' by checking +%% the history items 'registered' + +-spec has_registered(History, Map) -> boolean() when + History :: cauder_history:history(), + Map :: [cauder_map:map_element()]. + +has_registered([], _) -> + false; +has_registered([#hist_registered{map = Map} | _], Map) -> + true; +has_registered([_ | H], Map) -> + has_registered(H, Map). + %%%============================================================================= -spec group_actions(History) -> Map when @@ -149,7 +257,10 @@ has_receive(Uid, [_ | H]) -> has_receive(Uid, H). 'send' := ordsets:ordset(cauder_message:uid()), 'receive' := ordsets:ordset(cauder_message:uid()), 'spawn' := ordsets:ordset(cauder_process:id()), - 'start' := ordsets:ordset(node()) + 'start' := ordsets:ordset(node()), + 'register' := ordsets:ordset(cauder_map:map_element()), + 'sendA' := ordsets:ordset(cauder_message:uid()), + 'del' := ordsets:ordset([{cauder_map:map_element(), [cauder_map:map_element()]}]) }. group_actions(History) -> @@ -157,6 +268,8 @@ group_actions(History) -> fun (#hist_send{msg = #message{uid = Uid}}, Map) -> maps:update_with('send', fun(Uids) -> ordsets:add_element(Uid, Uids) end, Map); + (#hist_sendA{msg = #message{uid = Uid}}, Map) -> + maps:update_with('send', fun(Uids) -> ordsets:add_element(Uid, Uids) end, Map); (#hist_receive{msg = #message{uid = Uid}}, Map) -> maps:update_with('receive', fun(Uids) -> ordsets:add_element(Uid, Uids) end, Map); % TODO CHeck success @@ -164,6 +277,12 @@ group_actions(History) -> maps:update_with('spawn', fun(Pids) -> ordsets:add_element(Pid, Pids) end, Map); (#hist_start{node = Node, success = 'true'}, Map) -> maps:update_with('start', fun(Nodes) -> ordsets:add_element(Node, Nodes) end, Map); + %(#hist_sendA{mapEl = El, msg = #message{uid = Uid}}, Map) -> + % maps:update_with('sendA', fun(Uids) -> ordsets:add_element({El, Uid}, Uids) end, Map); + (#hist_regS{mapEl = RegEl}, Map) -> + maps:update_with('register', fun(El) -> ordsets:add_element(RegEl, El) end, Map); + (#hist_del{mapEl = DelEl}, Map) -> + maps:update_with('del', fun(El) -> ordsets:add_element(DelEl, El) end, Map); (_, Map1) -> Map1 end, @@ -171,7 +290,10 @@ group_actions(History) -> 'send' => ordsets:new(), 'receive' => ordsets:new(), 'spawn' => ordsets:new(), - 'start' => ordsets:new() + 'start' => ordsets:new(), + 'register' => ordsets:new(), + 'sendA' => ordsets:new(), + 'del' => ordsets:new() }, History ). @@ -185,6 +307,12 @@ is_concurrent(#hist_self{}) -> false; is_concurrent(#hist_node{}) -> false; is_concurrent(#hist_nodes{}) -> true; is_concurrent(#hist_start{}) -> true; +is_concurrent(#hist_readS{}) -> true; +is_concurrent(#hist_readF{}) -> true; +is_concurrent(#hist_registered{}) -> true; +is_concurrent(#hist_regS{}) -> true; +is_concurrent(#hist_del{}) -> true; +is_concurrent(#hist_sendA{}) -> true; is_concurrent(#hist_spawn{}) -> true; is_concurrent(#hist_send{}) -> true; is_concurrent(#hist_receive{}) -> true. diff --git a/src/cauder_log.erl b/src/cauder_log.erl index 82937b5..4f8b732 100644 --- a/src/cauder_log.erl +++ b/src/cauder_log.erl @@ -10,6 +10,9 @@ pop_spawn/2, pop_send/2, pop_receive/2, + pop_reg/2, + pop_del/2, + pop_read/2, push/3, is_element/2, is_empty/1, @@ -25,7 +28,12 @@ %has_start/3, has_spawn/3, has_send/3, - has_receive/3 + has_receive/3, + has_register/3, + has_delete/3, + has_registered/3, + has_fail_read/4, + has_success_read/3 ]). -export([ find_nodes/2, @@ -34,7 +42,12 @@ find_spawn_action/2, find_failed_spawns/2, find_send/2, - find_receive/2 + find_receive/2, + find_register/2, + find_delete/2, + find_registered/2, + find_fail_read/3, + find_success_read/2 ]). -include("cauder_log.hrl"). @@ -47,13 +60,19 @@ | action_send() | action_receive() | action_nodes() - | action_start(). + | action_start() + | action_reg() + | action_del() + | action_read(). -type action_spawn() :: #log_spawn{}. --type action_send() :: #log_send{}. +-type action_send() :: #log_send{} | #log_sendA{}. -type action_receive() :: #log_receive{}. -type action_nodes() :: #log_nodes{}. -type action_start() :: #log_start{}. +-type action_reg() :: #log_reg{}. +-type action_del() :: #log_del{}. +-type action_read() :: #log_read{}. %%%============================================================================= %%% API @@ -110,6 +129,8 @@ pop_send(Pid, Log) -> case maps:find(Pid, Log) of {ok, [#log_send{} = Action | Actions]} -> {Action, update_or_remove(Pid, Actions, Log)}; + {ok, [#log_sendA{} = Action | Actions]} -> + {Action, update_or_remove(Pid, Actions, Log)}; _ -> error end. @@ -156,6 +177,48 @@ pop_start(Pid, Log) -> error end. +-spec pop_reg(Pid, Log) -> {Action, NewLog} | error when + Pid :: cauder_process:id(), + Log :: cauder_log:log(), + Action :: cauder_log:action_reg(), + NewLog :: cauder_log:log(). + +pop_reg(Pid, Log) -> + case maps:find(Pid, Log) of + {ok, [#log_reg{} = Action | Actions]} -> + {Action, update_or_remove(Pid, Actions, Log)}; + _ -> + error + end. + +-spec pop_del(Pid, Log) -> {Action, NewLog} | error when + Pid :: cauder_process:id(), + Log :: cauder_log:log(), + Action :: cauder_log:action_del(), + NewLog :: cauder_log:log(). + +pop_del(Pid, Log) -> + case maps:find(Pid, Log) of + {ok, [#log_del{} = Action | Actions]} -> + {Action, update_or_remove(Pid, Actions, Log)}; + _ -> + error + end. + +-spec pop_read(Pid, Log) -> {Action, NewLog} | error when + Pid :: cauder_process:id(), + Log :: cauder_log:log(), + Action :: cauder_log:action_read(), + NewLog :: cauder_log:log(). + +pop_read(Pid, Log) -> + case maps:find(Pid, Log) of + {ok, [#log_read{} = Action | Actions]} -> + {Action, update_or_remove(Pid, Actions, Log)}; + _ -> + error + end. + -spec push(Pid, Action, Log) -> NewLog when Pid :: cauder_process:id(), Action :: cauder_log:action(), @@ -211,7 +274,9 @@ rdep(Pid, Log) -> remove_dependents_spawn(Pid, Log). 'send' := ordsets:ordset(cauder_message:uid()), 'receive' := ordsets:ordset(cauder_message:uid()), 'spawn' := ordsets:ordset(cauder_process:id()), - 'start' := ordsets:ordset(node()) + 'start' := ordsets:ordset(node()), + 'register' := ordsets:ordset(cauder_map:map_element()), + 'delete' := ordsets:ordset(cauder_map:map_element()) }. group_actions(Log) -> @@ -221,12 +286,18 @@ group_actions(Log) -> fun (#log_send{uid = Uid}, Map1) -> maps:update_with('send', fun(Uids) -> ordsets:add_element(Uid, Uids) end, Map1); + (#log_sendA{uid = Uid}, Map1) -> + maps:update_with('send', fun(Uids) -> ordsets:add_element(Uid, Uids) end, Map1); (#log_receive{uid = Uid}, Map1) -> maps:update_with('receive', fun(Uids) -> ordsets:add_element(Uid, Uids) end, Map1); (#log_spawn{pid = Pid, success = 'true'}, Map1) -> maps:update_with('spawn', fun(Pids) -> ordsets:add_element(Pid, Pids) end, Map1); (#log_start{node = Node, success = 'true'}, Map1) -> maps:update_with('start', fun(Nodes) -> ordsets:add_element(Node, Nodes) end, Map1); + (#log_reg{key = K, atom = A, pid = P}, Map1) -> + maps:update_with('register', fun(Els) -> ordsets:add_element({A, P, K, top}, Els) end, Map1); + (#log_del{key = K, atom = A, pid = P}, Map1) -> + maps:update_with('delete', fun(Els) -> ordsets:add_element({A, P, K, bot}, Els) end, Map1); (_, Map1) -> Map1 end, @@ -238,7 +309,9 @@ group_actions(Log) -> 'send' => ordsets:new(), 'receive' => ordsets:new(), 'spawn' => ordsets:new(), - 'start' => ordsets:new() + 'start' => ordsets:new(), + 'register' => ordsets:new(), + 'delete' => ordsets:new() }, Log ). @@ -270,6 +343,7 @@ has_send(Pid, Uid, Log) -> lists:any( fun (#log_send{uid = Uid1}) -> Uid1 =:= Uid; + (#log_sendA{uid = Uid1}) -> Uid1 =:= Uid; (_) -> false end, maps:get(Pid, Log) @@ -290,6 +364,84 @@ has_receive(Pid, Uid, Log) -> maps:get(Pid, Log) ). +-spec has_register(Pid, El, Log) -> boolean() when + Pid :: cauder_process:id(), + El :: cauder_map:map_element(), + Log :: cauder_log:log(). + +has_register(Pid, _, Log) when not is_map_key(Pid, Log) -> false; +has_register(Pid, {_, _, Key, _}, Log) -> + lists:any( + fun + (#log_reg{key = Key1}) -> Key1 =:= Key; + (_) -> false + end, + maps:get(Pid, Log) + ). + +-spec has_delete(Pid, El, Log) -> boolean() when + Pid :: cauder_process:id(), + El :: cauder_map:map_element(), + Log :: cauder_log:log(). + +has_delete(Pid, _, Log) when not is_map_key(Pid, Log) -> false; +has_delete(Pid, {_, _, Key, _}, Log) -> + lists:any( + fun + (#log_del{key = Key1}) -> Key1 =:= Key; + (_) -> false + end, + maps:get(Pid, Log) + ). + +-spec has_registered(Pid, Map, Log) -> boolean() when + Pid :: cauder_process:id(), + Map :: [cauder_map:map_element()], + Log :: cauder_log:log(). + +has_registered(Pid, _, Log) when not is_map_key(Pid, Log) -> false; +has_registered(Pid, Map, Log) -> + lists:any( + fun + (#log_read{atom = undefined, pid = undefined, map = LogMap}) -> + ((LogMap -- Map == []) and (Map -- LogMap == [])); + (_) -> + 'false' + end, + maps:get(Pid, Log) + ). + +-spec has_fail_read(Pid, Map, El, Log) -> boolean() when + Pid :: cauder_process:id(), + Map :: [cauder_map:map_element()], + El :: cauder_map:map_element(), + Log :: cauder_log:log(). + +has_fail_read(Pid, _, _, Log) when not is_map_key(Pid, Log) -> false; +has_fail_read(Pid, Map, {A1, P1, _, _}, Log) -> + lists:any( + fun + (#log_read{atom = A, pid = P, map = LogMap}) -> (((A =:= A1) or (P =:= P1)) and (LogMap -- Map == [])); + (_) -> false + end, + maps:get(Pid, Log) + ). + +-spec has_success_read(Pid, El, Log) -> boolean() when + Pid :: cauder_process:id(), + El :: cauder_map:map_element(), + Log :: cauder_log:log(). + +has_success_read(Pid, _, Log) when not is_map_key(Pid, Log) -> false; +has_success_read(Pid, El, Log) -> + lists:any( + fun + (#log_read{map = Map}) -> cauder_map:is_in_map(Map, El); + (_) -> false + end, + maps:get(Pid, Log) + ). + %%%============================================================================= %%------------------------------------------------------------------------------ @@ -306,7 +458,7 @@ find_nodes(Node, Log) -> fun(_Pid, Actions) -> lists:any( fun - (#log_nodes{nodes = Nodes}) -> lists:member(Node, Nodes); + (#log_nodes{nodes = Nodes}) -> not lists:member(Node, Nodes); (_) -> 'false' end, Actions @@ -418,6 +570,7 @@ find_send(Uid, Log) -> find_pid( fun (#log_send{uid = Uid1}) -> Uid =:= Uid1; + (#log_sendA{uid = Uid1}) -> Uid =:= Uid1; (_) -> 'false' end, Log @@ -441,6 +594,92 @@ find_receive(Uid, Log) -> Log ). +%%------------------------------------------------------------------------------ +%% @doc Checks the log of each process, until it finds the process that delete +%% the message with the given `Uid'. + +-spec find_delete(El, Log) -> {ok, Pid} | error when + El :: cauder_map:map_element(), + Log :: cauder_log:log(), + Pid :: cauder_process:id(). + +find_delete({_, _, Key, _}, Log) -> + find_pid( + fun + (#log_del{key = Key1}) -> Key =:= Key1; + (_) -> 'false' + end, + Log + ). + +%%------------------------------------------------------------------------------ +%% @doc Checks the log of each process, until it finds the process that registered +%% the message with the given `Uid'. + +-spec find_register(El, Log) -> {ok, Pid} | error when + El :: cauder_map:map_element(), + Log :: cauder_log:log(), + Pid :: cauder_process:id(). + +find_register({_, _, Key, _}, Log) -> + find_pid( + fun + (#log_reg{key = Key1}) -> Key =:= Key1; + (_) -> 'false' + end, + Log + ). + +%%------------------------------------------------------------------------------ +%% @doc Checks the log of each process, until it finds the process that registered +%% the message with the given `Uid'. + +-spec find_registered(Map, Log) -> {ok, Pid} | error when + Map :: [cauder_map:map_element()], + Log :: cauder_log:log(), + Pid :: cauder_process:id(). + +find_registered(Map, Log) -> + find_pid( + fun + (#log_read{atom = undefined, pid = undefined, map = LogMap}) -> + ((LogMap -- Map == []) and (Map -- LogMap == [])); + (_) -> + 'false' + end, + Log + ). + +-spec find_fail_read(El, Map, Log) -> {ok, Pid} | error when + El :: cauder_map:map_element(), + Map :: [cauder_map:map_element()], + Log :: cauder_log:log(), + Pid :: cauder_process:id(). + +find_fail_read({A1, P1, _, _}, Map, Log) -> + find_pid( + fun + (#log_read{atom = A, pid = P, map = LogMap}) -> (((A =:= A1) or (P =:= P1)) and (LogMap -- Map == [])); + (_) -> 'false' + end, + Log + ). + +-spec find_success_read(El, Log) -> {ok, Pid} | error when + El :: cauder_map:map_element(), + Log :: cauder_log:log(), + Pid :: cauder_process:id(). + +find_success_read(El, Log) -> + find_pid( + fun + (#log_read{map = Map}) -> cauder_map:is_in_map(Map, El); + (#log_sendA{el = El1}) -> El1 == El; + (_) -> 'false' + end, + Log + ). + %%%============================================================================= %%% Internal functions %%%============================================================================= @@ -518,6 +757,7 @@ remove_dependents_receive(Uid, Log) -> remove_dependents(#log_spawn{pid = Pid}, Log) -> remove_dependents_spawn(Pid, Log); remove_dependents(#log_send{uid = Uid}, Log) -> remove_dependents_receive(Uid, Log); +remove_dependents(#log_sendA{uid = Uid}, Log) -> remove_dependents_receive(Uid, Log); remove_dependents(_, Log) -> Log. %%%============================================================================= diff --git a/src/cauder_map.erl b/src/cauder_map.erl new file mode 100644 index 0000000..9b2cf94 --- /dev/null +++ b/src/cauder_map.erl @@ -0,0 +1,132 @@ +-module(cauder_map). + +%% API +-export([new_key/0]). + +-export([ + get_map/2, + is_in_map/2, + in_map/2, + not_in_map/2, + find_pid/2, + find_atom/2, + find_el/2, + get_atoms_list/2, + get_ghost_list/3 +]). + +-include("cauder.hrl"). +-include("cauder_process.hrl"). + +-export_type([key/0, map_node/0]). + +-opaque key() :: pos_integer(). +-type alive() :: top | bot. +-type map_element() :: {atom(), cauder_process:id(), cauder_map:key(), cauder_map:alive()}. +-type map_node() :: {[map_element()], node()}. + +%%%============================================================================= +%%% API +%%%============================================================================= + +%%------------------------------------------------------------------------------ +%% @doc Returns a new UID. + +-spec new_key() -> Key when + Key :: cauder_map:key(). + +new_key() -> + ets:update_counter(?APP_DB, last_key, 1, {last_key, -1}). + +%%------------------------------------------------------------------------------ +%% @doc Return the Map connected with the node Nid + +-spec get_map(Maps, Node) -> Map when + Maps :: [{cauder_map:map_node()}], + Node :: node(), + Map :: [cauder_map:map_element()]. + +get_map([], _) -> []; +get_map([{Map, Nid} | _], Nid) -> Map; +get_map([_ | Maps], Nid) -> get_map(Maps, Nid). + +-spec is_in_map(Map, El) -> boolean() when + Map :: [cauder_map:map_element()], + El :: cauder_map:map_element(). + +is_in_map([], _) -> false; +is_in_map([El | _], El) -> true; +is_in_map([_ | M], El) -> is_in_map(M, El). + +-spec in_map(Map, El) -> boolean() when + Map :: [cauder_map:map_element()], + El :: [cauder_map:map_element()]. + +in_map(_, []) -> + true; +in_map(M, [El]) -> + is_in_map(M, El); +in_map(M, [El | T]) -> + case is_in_map(M, El) of + true -> in_map(M, T); + false -> false + end. + +-spec not_in_map(Map, El) -> true | false when + Map :: [cauder_map:map_element()], + El :: atom() | cauder_process:id(). + +not_in_map([], _) -> true; +not_in_map([{Atom, _, _, top} | _], Atom) -> false; +not_in_map([{_, Pid, _, top} | _], Pid) -> false; +not_in_map([{_, _, _, _} | M], El) -> not_in_map(M, El). + +-spec find_pid(Atom, Map) -> {Pid, Key} | undefined when + Atom :: atom(), + Map :: [cauder_map:map_element()], + Pid :: cauder_process:id(), + Key :: cauder_map:key(). + +find_pid(_, []) -> undefined; +find_pid(Atom, [{Atom, Pid, K, top} | _]) -> {Pid, K}; +find_pid(Atom, [{_, _, _, _} | Map]) -> find_pid(Atom, Map). + +-spec find_atom(Pid, Map) -> {Atom, Key} | undefined when + Pid :: cauder_process:id(), + Map :: [cauder_map:map_element()], + Atom :: atom(), + Key :: cauder_map:key(). + +find_atom(_, []) -> undefined; +find_atom(Pid, [{Atom, Pid, K, top} | _]) -> {Atom, K}; +find_atom(Pid, [{_, _, _, _} | Map]) -> find_atom(Pid, Map). + +-spec get_atoms_list(Map, ListAtoms) -> Atoms when + Map :: [cauder_map:map_element()], + ListAtoms :: [atom()], + Atoms :: [atom()]. + +get_atoms_list([], R) -> R; +get_atoms_list([{Atom, _, _, top} | T], R) -> get_atoms_list(T, [Atom | R]); +get_atoms_list([{_, _, _, _} | T], R) -> get_atoms_list(T, R). + +-spec get_ghost_list(El, Map, ListGhost) -> Ghosts when + El :: atom() | cauder_process:id(), + Map :: [cauder_map:map_element()], + ListGhost :: [cauder_map:map_element()], + Ghosts :: [cauder_map:map_element()]. + +get_ghost_list(_, [], LG) -> LG; +get_ghost_list(Atom, [{Atom, Pid, K, bot} | Map], LG) -> get_ghost_list(Atom, Map, [{Atom, Pid, K, bot} | LG]); +get_ghost_list(Pid, [{Atom, Pid, K, bot} | Map], LG) -> get_ghost_list(Pid, Map, [{Atom, Pid, K, bot} | LG]); +get_ghost_list(El, [{_, _, _, _} | Map], LG) -> get_ghost_list(El, Map, LG). + +-spec find_el(El, Map) -> Tuple | undefined when + El :: atom() | cauder_process:id(), + Map :: [cauder_map:map_element()], + Tuple :: cauder_map:map_element(). + +find_el(_, []) -> undefined; +find_el(El, [{El, Pid, K, top} | _]) -> {El, Pid, K, top}; +find_el(El, [{Atom, El, K, top} | _]) -> {Atom, El, K, top}; +find_el(El, [{_, _, _, _} | Map]) -> find_atom(El, Map). diff --git a/src/cauder_pool.erl b/src/cauder_pool.erl index 3049e70..7f6698d 100644 --- a/src/cauder_pool.erl +++ b/src/cauder_pool.erl @@ -22,7 +22,13 @@ find_history_spawn/2, find_history_send/2, find_history_receive/2, - find_variable/2 + find_variable/2, + find_read_map/3, + find_failed_read_map/3, + find_registered/3, + find_history_reg/2, + find_history_del/2, + find_history_senda/2 ]). -include("cauder_process.hrl"). @@ -227,6 +233,23 @@ find_history_send(Uid, Pool) -> %% @doc Checks the history of each process, until it finds the process that %% sent the message with the given `Uid'. +-spec find_history_senda(Uid, Pool) -> {ok, Process} | error when + Uid :: cauder_message:uid(), + Pool :: cauder_pool:pool(), + Process :: cauder_process:process(). + +find_history_senda(Uid, Pool) -> + value_to_ok( + lists:search( + fun(P) -> cauder_history:has_senda(Uid, P#process.hist) end, + maps:values(Pool) + ) + ). + +%%------------------------------------------------------------------------------ +%% @doc Checks the history of each process, until it finds the process that +%% sent the message with the given `Uid'. + -spec find_history_receive(Uid, Pool) -> {ok, Process} | error when Uid :: cauder_message:uid(), Pool :: cauder_pool:pool(), @@ -240,6 +263,40 @@ find_history_receive(Uid, Pool) -> ) ). +%%------------------------------------------------------------------------------ +%% @doc Checks the history of each process, until it finds the process that +%% . + +-spec find_history_reg(El, Pool) -> {ok, Process} | error when + El :: cauder_map:map_element(), + Pool :: cauder_pool:pool(), + Process :: cauder_process:process(). + +find_history_reg(El, Pool) -> + value_to_ok( + lists:search( + fun(P) -> cauder_history:has_reg(El, P#process.hist) end, + maps:values(Pool) + ) + ). + +%%------------------------------------------------------------------------------ +%% @doc Checks the history of each process, until it finds the process that +%% . + +-spec find_history_del(El, Pool) -> {ok, Process} | error when + El :: cauder_map:map_element(), + Pool :: cauder_pool:pool(), + Process :: cauder_process:process(). + +find_history_del(El, Pool) -> + value_to_ok( + lists:search( + fun(P) -> cauder_history:has_del(El, P#process.hist) end, + maps:values(Pool) + ) + ). + %%------------------------------------------------------------------------------ %% @doc Searches for the process that defined the variable with the given name, %% by looking at its history. @@ -257,6 +314,72 @@ find_variable(Name, Pool) -> ) ). +%%------------------------------------------------------------------------------ +%% @doc Searches for process(es) that have performed a read operation on map + +-spec find_read_map(Pool, Node, El) -> {ok, Process} | error when + Pool :: cauder_pool:pool(), + Node :: node(), + El :: cauder_map:map_element(), + Process :: cauder_process:process(). + +find_read_map(Pool, Node, El) -> + value_to_ok( + lists:search( + fun(#process{node = ProcNode, hist = H}) -> + case ProcNode =:= Node of + true -> cauder_history:has_read_map(H, El); + false -> error + end + end, + maps:values(Pool) + ) + ). + +%%------------------------------------------------------------------------------ +%% @doc Searches for process(es) that have performed a fail read operation on map + +-spec find_failed_read_map(Pool, Node, El) -> {ok, Process} | error when + Pool :: cauder_pool:pool(), + Node :: node(), + El :: cauder_map:map_element(), + Process :: cauder_process:process(). + +find_failed_read_map(Pool, Node, El) -> + value_to_ok( + lists:search( + fun(#process{node = ProcNode, hist = H}) -> + case ProcNode =:= Node of + true -> cauder_history:has_fail_read_map(H, El); + false -> error + end + end, + maps:values(Pool) + ) + ). + +%%------------------------------------------------------------------------------ +%% @doc Searches for process(es) that have performed a read operation on map + +-spec find_registered(Pool, Node, Map) -> {ok, Process} | error when + Pool :: cauder_pool:pool(), + Node :: node(), + Map :: [cauder_map:map_element()], + Process :: cauder_process:process(). + +find_registered(Pool, Node, Map) -> + value_to_ok( + lists:search( + fun(#process{node = ProcNode, hist = H}) -> + case ProcNode =:= Node of + true -> cauder_history:has_registered(H, Map); + false -> error + end + end, + maps:values(Pool) + ) + ). + %%%============================================================================= %%% Internal functions %%%============================================================================= diff --git a/src/cauder_pp.erl b/src/cauder_pp.erl index c996a0a..0c8fce4 100644 --- a/src/cauder_pp.erl +++ b/src/cauder_pp.erl @@ -46,7 +46,15 @@ log_action(#log_spawn{node = Node, pid = Pid, success = 'false'}) -> log_action(#log_send{uid = Uid}) -> "send(" ++ blue(to_string(Uid)) ++ ")"; log_action(#log_receive{uid = Uid}) -> - "receive(" ++ blue(to_string(Uid)) ++ ")". + "receive(" ++ blue(to_string(Uid)) ++ ")"; +log_action(#log_reg{key = K}) -> + "register {" ++ blue(to_string(K)) ++ "}"; +log_action(#log_del{key = K}) -> + "delete {" ++ blue(to_string(K)) ++ "}"; +log_action(#log_read{}) -> + "read"; +log_action(#log_sendA{uid = Uid, el = {A, _, _, _}}) -> + "send(" ++ blue(to_string(Uid)) ++ ") with atom " ++ blue(to_string(A)). %%%============================================================================= @@ -73,6 +81,18 @@ history_entry(#hist_tau{}) -> "local"; history_entry(#hist_self{}) -> "self"; +history_entry(#hist_registered{}) -> + "registered"; +history_entry(#hist_readS{mapEl = Map}) -> + "read of " ++ to_string(Map); +history_entry(#hist_readF{atom = Atom}) -> + "try to read " ++ to_string(Atom); +history_entry(#hist_regS{mapEl = {A, P, K, _}}) -> + "register {" ++ to_string(A) ++ ", " ++ to_string(P) ++ ", " ++ to_string(K) ++ "}"; +history_entry(#hist_del{mapEl = El}) -> + "delete " ++ to_string(El); +history_entry(#hist_sendA{mapEl = {A, _, _, _}, msg = #message{uid = Uid, val = Val}}) -> + "send with atom " ++ to_string(A) ++ " (" ++ to_string(Val) ++ "," ++ blue(to_string(Uid)) ++ ")"; history_entry(#hist_nodes{nodes = Nodes}) -> "nodes(" ++ pp_nodes(Nodes) ++ ")"; history_entry(#hist_start{node = Node, success = true}) -> diff --git a/src/cauder_replay.erl b/src/cauder_replay.erl index 68c07c7..577bed9 100644 --- a/src/cauder_replay.erl +++ b/src/cauder_replay.erl @@ -10,19 +10,24 @@ can_replay_start/2, can_replay_spawn/2, can_replay_send/2, - can_replay_receive/2 + can_replay_receive/2, + can_replay_register/2, + can_replay_delete/2 ]). -export([ replay_step/2, replay_start/2, replay_spawn/2, replay_send/2, - replay_receive/2 + replay_receive/2, + replay_register/2, + replay_delete/2 ]). -include("cauder_system.hrl"). -include("cauder_message.hrl"). -include("cauder_log.hrl"). +-include("cauder_process.hrl"). %%%============================================================================= %%% API @@ -85,6 +90,28 @@ can_replay_send(Uid, #system{log = Log}) -> can_replay_receive(Uid, #system{log = Log}) -> cauder_log:find_receive(Uid, Log) =/= error. +%%------------------------------------------------------------------------------ +%% @doc Checks whether the of the message with the given uid can be +%% replayed in the given system, or not. + +-spec can_replay_delete(El, System) -> boolean() when + El :: cauder_map:map_element(), + System :: cauder_system:system(). + +can_replay_delete(El, #system{log = Log}) -> + cauder_log:find_delete(El, Log) =/= error. + +%%------------------------------------------------------------------------------ +%% @doc Checks whether the of the message with the given uid can be +%% replayed in the given system, or not. + +-spec can_replay_register(El, System) -> boolean() when + El :: cauder_map:map_element(), + System :: cauder_system:system(). + +can_replay_register(El, #system{log = Log}) -> + cauder_log:find_register(El, Log) =/= error. + %%%============================================================================= %%------------------------------------------------------------------------------ @@ -105,12 +132,21 @@ replay_step(Pid, #system{log = Log} = Sys) -> case cauder_log:peek(Pid, Log) of {value, #log_send{uid = Uid}} -> replay_send(Uid, Sys); + {value, #log_sendA{el = El, uid = Uid}} -> + replay_reg_del((cauder_pool:get(Pid, Sys#system.pool))#process.node, [El], Sys), + replay_send(Uid, Sys); {value, #log_receive{uid = Uid}} -> replay_receive(Uid, Sys); {value, #log_start{node = Node, success = 'true'}} -> replay_start(Node, Sys); {value, #log_spawn{pid = ChildPid, success = 'true'}} -> - replay_spawn(ChildPid, Sys) + replay_spawn(ChildPid, Sys); + {value, #log_reg{atom = A, pid = P, key = Key, map = LogMap}} -> + replay_register({A, P, Key, top}, LogMap, Sys); + {value, #log_del{atom = A, pid = P, key = Key, map = LogMap}} -> + replay_delete({A, P, Key, bot}, LogMap, Sys); + {value, #log_read{map = LogMap}} -> + replay_read(Pid, (cauder_pool:get(Pid, Sys#system.pool))#process.node, LogMap, Sys) end end. @@ -203,6 +239,36 @@ replay_receive(Uid, #system{log = Log} = Sys) -> error -> Sys end. +%%------------------------------------------------------------------------------ +%% @doc Replays the reception of the message with the given uid, in the given +%% system. + +-spec replay_register(El, System) -> NewSystem when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_register(El, #system{log = Log} = Sys) -> + case cauder_log:find_register(El, Log) of + {ok, Pid} -> replay_until_register(Pid, Sys, El); + error -> Sys + end. + +%%------------------------------------------------------------------------------ +%% @doc Replays the reception of the message with the given uid, in the given +%% system. + +-spec replay_delete(El, System) -> NewSystem when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_delete(El, #system{log = Log} = Sys) -> + case cauder_log:find_delete(El, Log) of + {ok, Pid} -> replay_until_delete(Pid, Sys, El); + error -> Sys + end. + %%%============================================================================= %%% Internal functions %%%============================================================================= @@ -311,3 +377,269 @@ replay_until_receive1(Pid, Sys0, Uid) -> true -> replay_until_receive1(Pid, Sys1, Uid); false -> Sys1 end. + +-spec replay_until_register(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_register(Pid, Sys0, El) -> + #system{log = Log} = Sys1 = replay_spawn(Pid, Sys0), + case cauder_log:has_register(Pid, El, Log) of + true -> replay_until_register1(Pid, Sys1, El); + false -> Sys0 + end. + +-spec replay_until_register1(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_register1(Pid, Sys0, El) -> + #system{log = Log} = Sys1 = replay_step(Pid, Sys0), + case cauder_log:has_register(Pid, El, Log) of + true -> replay_until_register1(Pid, Sys1, El); + false -> Sys1 + end. + +-spec replay_register(El, LogMap, System) -> NewSystem when + El :: cauder_map:map_element(), + LogMap :: [cauder_map:map_element()], + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_register(El, LogMap, #system{log = Log} = Sys) -> + case cauder_log:find_register(El, Log) of + {ok, Pid} -> replay_until_register(Pid, LogMap, Sys, El); + error -> Sys + end. + +-spec replay_until_register(Pid, LogMap, System, El) -> NewSystem when + Pid :: cauder_process:id(), + LogMap :: [cauder_map:map_element()], + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_register(Pid, LogMap, Sys0, El) -> + Proc = cauder_pool:get(Pid, Sys0#system.pool), + SystemMap = cauder_map:get_map(Sys0#system.maps, Proc#process.node), + Sys1 = replay_registereds(SystemMap, Sys0), + Sys2 = replay_fail_reads(El, LogMap, Sys1), + Sys3 = replay_spawn(Pid, Sys2), + Proc = cauder_pool:get(Pid, Sys3#system.pool), + #system{log = Log2} = Sys4 = replay_reg_del(Proc#process.node, LogMap, Sys3), + case cauder_log:has_register(Pid, El, Log2) of + true -> replay_until_register1(Pid, Sys4, El); + false -> Sys4 + end. + +-spec replay_fail_reads(El, Map, System) -> NewSystem when + El :: cauder_map:map_element(), + Map :: [cauder_map:map_element()], + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_fail_reads(El, LogMap, #system{log = Log} = Sys0) -> + %io:format("\nreplay_fail_reads\n", []), + case cauder_log:find_fail_read(El, LogMap, Log) of + {ok, Pid} -> + Sys1 = replay_until_fail_read(Pid, Sys0, LogMap, El), + replay_fail_reads(El, LogMap, Sys1); + error -> + Sys0 + end. + +-spec replay_until_fail_read(Pid, System, Map, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + Map :: [cauder_map:map_element()], + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_fail_read(Pid, Sys0, Map, El) -> + %io:format("\nreplay_until_fail_read\n", []), + case cauder_log:has_fail_read(Pid, Map, El, Sys0#system.log) of + true -> + Sys1 = replay_step(Pid, Sys0), + replay_until_fail_read(Pid, Sys1, Map, El); + false -> + Sys0 + end. + +-spec replay_registereds(Map, System) -> NewSystem when + Map :: [cauder_map:map_element()], + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_registereds(Map, #system{log = Log} = Sys0) -> + %io:format("\nreplay_registereds\n", []), + case cauder_log:find_registered(Map, Log) of + {ok, Pid} -> + Sys1 = replay_until_registered(Pid, Sys0, Map), + Proc = cauder_pool:get(Pid, Sys1#system.pool), + SystemMap = cauder_map:get_map(Sys1#system.maps, Proc#process.node), + replay_registereds(SystemMap, Sys1); + error -> + Sys0 + end. + +-spec replay_until_registered(Pid, System, Map) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + Map :: [cauder_map:map_element()], + NewSystem :: cauder_system:system(). + +replay_until_registered(Pid, Sys0, Map) -> + %io:format("\nreplay_until_registered~p\n", [Sys0#system.log]), + + case cauder_log:has_registered(Pid, Map, Sys0#system.log) of + true -> + Sys1 = replay_step(Pid, Sys0), + Proc = cauder_pool:get(Pid, Sys1#system.pool), + SystemMap = cauder_map:get_map(Sys1#system.maps, Proc#process.node), + replay_until_registered(Pid, Sys1, SystemMap); + false -> + Sys0 + end. + +-spec replay_until_delete(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_delete(Pid, Sys0, El) -> + #system{log = Log} = Sys1 = replay_spawn(Pid, Sys0), + case cauder_log:has_delete(Pid, El, Log) of + true -> replay_until_delete1(Pid, Sys1, El); + false -> Sys0 + end. + +-spec replay_until_delete1(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_delete1(Pid, Sys0, El) -> + #system{log = Log} = Sys1 = replay_step(Pid, Sys0), + case cauder_log:has_delete(Pid, El, Log) of + true -> replay_until_delete1(Pid, Sys1, El); + false -> Sys1 + end. + +-spec replay_delete(El, LogMap, System) -> NewSystem when + El :: cauder_map:map_element(), + LogMap :: [cauder_map:map_element()], + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_delete(Key, LogMap, #system{log = Log} = Sys) -> + case cauder_log:find_delete(Key, Log) of + {ok, Pid} -> replay_until_delete(Pid, LogMap, Sys, Key); + error -> Sys + end. + +-spec replay_until_delete(Pid, LogMap, System, El) -> NewSystem when + Pid :: cauder_process:id(), + LogMap :: [cauder_map:map_element()], + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_delete(Pid, LogMap, Sys0, El) -> + Proc = cauder_pool:get(Pid, Sys0#system.pool), + SystemMap = cauder_map:get_map(Sys0#system.maps, Proc#process.node), + Sys1 = replay_registereds(SystemMap, Sys0), + Sys2 = replay_fail_reads(El, LogMap, Sys1), + Sys3 = replay_register(El, Sys2), + + Sys4 = replay_success_reads(El, Sys3), + + Sys5 = replay_spawn(Pid, Sys4), + Proc = cauder_pool:get(Pid, Sys5#system.pool), + #system{log = Log2} = Sys6 = replay_reg_del(Proc#process.node, LogMap, Sys5), + + case cauder_log:has_delete(Pid, El, Log2) of + true -> replay_until_delete1(Pid, Sys6, El); + false -> Sys6 + end. + +-spec replay_success_reads(El, System) -> NewSystem when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_success_reads({A, P, K, _}, #system{log = Log} = Sys0) -> + %io:format("\nreplay_success_reads\n", []), + case cauder_log:find_success_read({A, P, K, top}, Log) of + {ok, Pid} -> + Sys1 = replay_until_success_read(Pid, Sys0, {A, P, K, top}), + replay_success_reads({A, P, K, top}, Sys1); + error -> + Sys0 + end. + +-spec replay_until_success_read(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +replay_until_success_read(Pid, Sys0, El) -> + %io:format("\nreplay_until_success_read\n", []), + case cauder_log:has_success_read(Pid, El, Sys0#system.log) of + true -> + Sys1 = replay_step(Pid, Sys0), + replay_until_success_read(Pid, Sys1, El); + false -> + Sys0 + end. + +-spec replay_read(Pid, Node, LogMap, System) -> NewSystem when + Pid :: cauder_process:id(), + Node :: node(), + LogMap :: [cauder_map:map_element()], + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_read(Pid, Node, LogMap, Sys0) -> + Sys1 = replay_reg_del(Node, LogMap, Sys0), + replay_step(Pid, Sys1). + +% -spec replay_SendA(Pid, Node, LogMap, System) -> NewSystem when +% Pid :: cauder_process:id(), +% Node :: node(), +% LogMap :: [cauder_map:map_element()], +% System :: cauder_system:system(), +% NewSystem :: cauder_system:system(). + +% replay_SendA(Pid, Node, LogMap, Sys0) -> +% replay_reg_del(Node, LogMap, Sys0). + +-spec replay_reg_del(Node, LogMap, System) -> NewSystem when + Node :: node(), + LogMap :: [cauder_map:map_element()], + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +replay_reg_del(Node, LogMap, OldSystem) -> + SystemMap = cauder_map:get_map(OldSystem#system.maps, Node), + %io:format("\nLOGMAP ~p\n", [LogMap]), + %io:format("\nSystemMap ~p\n", [SystemMap]), + case LogMap -- SystemMap of + [{_, _, K, top} = El | _] -> + %io:format("\nREG ~p\n", [K]), + NewSystem = replay_register(El, OldSystem), + replay_reg_del(Node, LogMap, NewSystem); + [{_, _, K, bot} = El | _] -> + %io:format("\nDEL ~p\n", [K]), + NewSystem = replay_delete(El, OldSystem), + replay_reg_del(Node, LogMap, NewSystem); + [] -> + %io:format("I am Here", []), + OldSystem + end. diff --git a/src/cauder_rollback.erl b/src/cauder_rollback.erl index 7b1fee4..9152a66 100644 --- a/src/cauder_rollback.erl +++ b/src/cauder_rollback.erl @@ -10,16 +10,22 @@ can_rollback_start/2, can_rollback_spawn/2, can_rollback_send/2, + can_rollback_senda/2, can_rollback_receive/2, - can_rollback_variable/2 + can_rollback_variable/2, + can_rollback_reg/2, + can_rollback_del/2 ]). -export([ rollback_step/2, rollback_start/2, rollback_spawn/2, rollback_send/2, + rollback_senda/2, rollback_receive/2, - rollback_variable/2 + rollback_variable/2, + rollback_reg/2, + rollback_del/2 ]). -include("cauder_system.hrl"). @@ -92,6 +98,21 @@ can_rollback_send(Uid, #system{pool = Pool}) -> error -> false end. +%%------------------------------------------------------------------------------ +%% @doc Checks whether the sending of the message with the given uid can be +%% rolled back in the given system, or not. + +-spec can_rollback_senda(Uid, System) -> CanRollback when + Uid :: cauder_message:uid(), + System :: cauder_system:system(), + CanRollback :: boolean(). + +can_rollback_senda(Uid, #system{pool = Pool}) -> + case cauder_pool:find_history_senda(Uid, Pool) of + {ok, _} -> true; + error -> false + end. + %%------------------------------------------------------------------------------ %% @doc Checks whether the reception of the message with the given uid can be %% rolled back in the given system, or not. @@ -107,6 +128,36 @@ can_rollback_receive(Uid, #system{pool = Pool}) -> error -> false end. +%%------------------------------------------------------------------------------ +%% @doc Checks whether can be +%% rolled back in the given system, or not. + +-spec can_rollback_reg(El, System) -> CanRollback when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + CanRollback :: boolean(). + +can_rollback_reg(El, #system{pool = Pool}) -> + case cauder_pool:find_history_reg(El, Pool) of + {ok, _} -> true; + error -> false + end. + +%%------------------------------------------------------------------------------ +%% @doc Checks whether can be +%% rolled back in the given system, or not. + +-spec can_rollback_del(El, System) -> CanRollback when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + CanRollback :: boolean(). + +can_rollback_del(El, #system{pool = Pool}) -> + case cauder_pool:find_history_del(El, Pool) of + {ok, _} -> true; + error -> false + end. + %%------------------------------------------------------------------------------ %% @doc Checks whether the binding of the variable with the given name can be %% rolled back in the given system, or not. @@ -149,6 +200,24 @@ rollback_step(Pid, #system{pool = Pool, nodes = SysNodes, roll = RollLog} = Sys0 {value, #hist_send{msg = #message{uid = Uid, dst = Dst} = Msg}} -> Sys = Sys0#system{roll = RollLog ++ cauder_utils:gen_log_send(Pid, Msg)}, rollback_send(Pid, Sys, Dst, Uid); + {value, #hist_sendA{node = Node, mapEl = El, msg = #message{uid = Uid, dst = Dst}}} -> + Sys = Sys0#system{}, + rollback_senda(Pid, Sys, Dst, Uid, El, Node); + {value, #hist_regS{mapEl = El, node = Node}} -> + Sys = Sys0#system{}, + rollback_reg(Pid, Sys, El, Node); + {value, #hist_del{mapEl = El, map = Map, node = Node}} -> + Sys = Sys0#system{}, + rollback_del(Pid, Sys, El, Map, Node); + {value, #hist_registered{map = Map, node = Node}} -> + Sys = Sys0#system{}, + rollback_registered(Pid, Sys, Map, Node); + {value, #hist_readF{atom = El, mapGhost = MapGhost, node = Node}} -> + Sys = Sys0#system{}, + rollback_read_f(Pid, Sys, El, MapGhost, Node); + {value, #hist_readS{mapEl = El, node = Node}} -> + Sys = Sys0#system{}, + rollback_read_s(Pid, Sys, El, Node); {value, _} -> cauder_semantics_backwards:step(Pid, Sys0) end. @@ -192,6 +261,19 @@ rollback_send(Uid, #system{pool = Pool} = Sys) -> {ok, #process{pid = SenderPid}} = cauder_pool:find_history_send(Uid, Pool), rollback_until_send(SenderPid, Sys#system{roll = []}, Uid). +%%------------------------------------------------------------------------------ +%% @doc Rolls back the sending of the message with the given uid, in the given +%% system. + +-spec rollback_senda(Uid, System) -> NewSystem when + Uid :: cauder_message:uid(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rollback_senda(Uid, #system{pool = Pool} = Sys) -> + {ok, #process{pid = SenderPid}} = cauder_pool:find_history_senda(Uid, Pool), + rollback_until_senda(SenderPid, Sys#system{roll = []}, Uid). + %%------------------------------------------------------------------------------ %% @doc Rolls back the reception of the message with the given uid, in the given %% system. @@ -205,6 +287,32 @@ rollback_receive(Uid, #system{pool = Pool} = Sys) -> {ok, #process{pid = ReceiverPid}} = cauder_pool:find_history_receive(Uid, Pool), rollback_until_receive(ReceiverPid, Sys#system{roll = []}, Uid). +%%------------------------------------------------------------------------------ +%% @doc Rolls back , in the given +%% system. + +-spec rollback_reg(El, System) -> NewSystem when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rollback_reg(El, #system{pool = Pool} = Sys) -> + {ok, #process{pid = Pid}} = cauder_pool:find_history_reg(El, Pool), + rollback_until_reg(Pid, Sys#system{roll = []}, El). + +%%------------------------------------------------------------------------------ +%% @doc Rolls back , in the given +%% system. + +-spec rollback_del(El, System) -> NewSystem when + El :: cauder_map:map_element(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rollback_del(El, #system{pool = Pool} = Sys) -> + {ok, #process{pid = Pid}} = cauder_pool:find_history_del(El, Pool), + rollback_until_del(Pid, Sys#system{roll = []}, El). + %%------------------------------------------------------------------------------ %% @doc Rolls back the binding of the variable with the given name, in the given %% system. @@ -284,6 +392,206 @@ rollback_send(Pid, Sys0, DestPid, Uid) -> rollback_send(Pid, Sys1, DestPid, Uid) end. +-spec rollback_senda(Pid, System, DestPid, Uid, El, Node) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + DestPid :: cauder_process:id(), + Uid :: cauder_message:uid(), + El :: cauder_map:map_element(), + Node :: node(), + NewSystem :: cauder_system:system(). + +rollback_senda(Pid, Sys0, DestPid, Uid, El, Node) -> + Opts = cauder_semantics_backwards:options(Sys0), + case maps:find(Pid, Opts) of + {ok, ?RULE_SEND} -> + cauder_semantics_backwards:step(Pid, Sys0); + error -> + Map = cauder_map:get_map(Sys0#system.maps, Node), + case cauder_map:is_in_map(Map, El) of + true -> + Sys1 = rollback_step(DestPid, Sys0), + rollback_senda(Pid, Sys1, DestPid, Uid, El, Node); + false -> + {ok, #process{pid = DelPid}} = cauder_pool:find_history_del(El, Sys0#system.pool), + Sys1 = rollback_step(DelPid, Sys0), + rollback_senda(Pid, Sys1, DestPid, Uid, El, Node) + end + end. + +-spec rollback_reg(Pid, System, El, Node) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + Node :: node(), + NewSystem :: cauder_system:system(). + +rollback_reg(Pid, Sys0, El, Node) -> + Opts = cauder_semantics_backwards:options(Sys0), + case maps:find(Pid, Opts) of + {ok, ?RULE_REG} -> + cauder_semantics_backwards:step(Pid, Sys0); + error -> + Map = cauder_map:get_map(Sys0#system.maps, Node), + PidUndo = + case cauder_map:is_in_map(Map, El) of + true -> + {ok, #process{pid = ReadPid}} = cauder_pool:find_read_map(Sys0#system.pool, Node, El), + ReadPid; + false -> + {ok, #process{pid = DelPid}} = cauder_pool:find_history_del(El, Sys0#system.pool), + DelPid + end, + Sys1 = rollback_step(PidUndo, Sys0), + rollback_reg(Pid, Sys1, El, Node) + end. + +-spec rollback_del(Pid, System, El, MapG, Node) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + MapG :: [cauder_map:map_element()], + Node :: node(), + NewSystem :: cauder_system:system(). + +rollback_del(Pid, Sys0, El = {A, P, K, _}, MapG, Node) -> + Opts = cauder_semantics_backwards:options(Sys0), + case maps:find(Pid, Opts) of + {ok, ?RULE_DEL} -> + cauder_semantics_backwards:step(Pid, Sys0); + error -> + case cauder_pool:find_failed_read_map(Sys0#system.pool, Node, {A, P, K, bot}) of + {ok, #process{pid = PidUndo}} -> + Sys1 = rollback_step(PidUndo, Sys0), + rollback_del(Pid, Sys1, El, MapG, Node); + error -> + Map = cauder_map:get_map(Sys0#system.maps, Node), + LG = cauder_map:get_ghost_list(A, Map, []) ++ cauder_map:get_ghost_list(P, Map, []), + case LG -- MapG of + [{Atom1, Pid1, K1, bot} | _] -> + {ok, #process{pid = PidUndo}} = cauder_pool:find_history_del( + {Atom1, Pid1, K1, top}, Sys0#system.pool + ), + Sys1 = rollback_step(PidUndo, Sys0), + rollback_del(Pid, Sys1, El, MapG, Node); + [] -> + case cauder_map:find_atom(P, Map) of + {Atom, Key} -> + {ok, #process{pid = PidUndo}} = cauder_pool:find_history_reg( + {Atom, P, Key, top}, Sys0#system.pool + ), + Sys1 = rollback_step(PidUndo, Sys0), + rollback_del(Pid, Sys1, El, MapG, Node); + undefined -> + {PidReg, Key} = cauder_map:find_pid(A, Map), + {ok, #process{pid = PidUndo}} = cauder_pool:find_history_reg( + {A, PidReg, Key, top}, Sys0#system.pool + ), + Sys1 = rollback_step(PidUndo, Sys0), + rollback_del(Pid, Sys1, El, MapG, Node) + end + end + end + end. + +-spec rollback_read_s(Pid, System, El, Node) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: [cauder_map:map_element()], + Node :: node(), + NewSystem :: cauder_system:system(). + +rollback_read_s(Pid, Sys0, El, Node) -> + Opts = cauder_semantics_backwards:options(Sys0), + case maps:find(Pid, Opts) of + {ok, ?RULE_READ} -> + cauder_semantics_backwards:step(Pid, Sys0); + error -> + SystemMap = cauder_map:get_map(Sys0#system.maps, Node), + PidUndo = + case El of + [{A, P, K, _}] -> + {ok, #process{pid = PidEl}} = cauder_pool:find_history_del({A, P, K, top}, Sys0#system.pool), + PidEl; + [{A1, P1, K1, _} | [{A2, P2, K2, _}]] -> + case cauder_map:is_in_map(SystemMap, {A1, P1, K1, top}) of + true -> + {ok, #process{pid = PidEl1}} = cauder_pool:find_history_del( + {A2, P2, K2, top}, Sys0#system.pool + ), + PidEl1; + false -> + {ok, #process{pid = PidEl2}} = cauder_pool:find_history_del( + {A1, P1, K1, top}, Sys0#system.pool + ), + PidEl2 + end + end, + Sys1 = rollback_step(PidUndo, Sys0), + rollback_read_s(Pid, Sys1, El, Node) + end. + +-spec rollback_read_f(Pid, System, El, MapGhost, Node) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: atom() | cauder_process:id(), + MapGhost :: [cauder_map:map_element()], + Node :: node(), + NewSystem :: cauder_system:system(). + +rollback_read_f(Pid, Sys0, El, MapGhost, Node) -> + Opts = cauder_semantics_backwards:options(Sys0), + case maps:find(Pid, Opts) of + {ok, ?RULE_READ} -> + cauder_semantics_backwards:step(Pid, Sys0); + error -> + Map = cauder_map:get_map(Sys0#system.maps, Node), + SystemGhost = cauder_map:get_ghost_list(El, Map, []), + PidUndo = + case SystemGhost -- MapGhost of + [] -> + Tuple = cauder_map:find_el(El, Map), + {ok, #process{pid = PidU}} = cauder_pool:find_history_reg(Tuple, Sys0#system.pool), + PidU; + [{A, P, K, _} | _] -> + {ok, #process{pid = DelPid}} = cauder_pool:find_history_del({A, P, K, top}, Sys0#system.pool), + DelPid + end, + Sys1 = rollback_step(PidUndo, Sys0), + rollback_read_f(Pid, Sys1, El, MapGhost, Node) + end. + +-spec rollback_registered(Pid, System, Map, Node) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + Map :: [cauder_map:map_element()], + Node :: node(), + NewSystem :: cauder_system:system(). + +rollback_registered(Pid, Sys0, Map, Node) -> + Opts = cauder_semantics_backwards:options(Sys0), + case maps:find(Pid, Opts) of + {ok, ?RULE_READ} -> + cauder_semantics_backwards:step(Pid, Sys0); + error -> + SystemMap = cauder_map:get_map(Sys0#system.maps, Node), + PidUndo = + case SystemMap -- Map of + [{Atom1, Pid1, K1, top} | _] -> + {ok, #process{pid = ReadPid}} = cauder_pool:find_history_reg( + {Atom1, Pid1, K1, top}, Sys0#system.pool + ), + ReadPid; + [{Atom1, Pid1, K1, bot} | _] -> + {ok, #process{pid = DelPid}} = cauder_pool:find_history_del( + {Atom1, Pid1, K1, top}, Sys0#system.pool + ), + DelPid + end, + Sys1 = rollback_step(PidUndo, Sys0), + rollback_registered(Pid, Sys1, Map, Node) + end. + %%%============================================================================= -spec rollback_until_start(Pid, System, Node) -> NewSystem when @@ -348,6 +656,22 @@ rollback_until_send(Pid, #system{pool = Pool} = Sys0, Uid) -> rollback_until_send(Pid, Sys1, Uid) end. +-spec rollback_until_senda(Pid, System, Uid) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + Uid :: cauder_message:uid(), + NewSystem :: cauder_system:system(). + +rollback_until_senda(Pid, #system{pool = Pool} = Sys0, Uid) -> + #process{hist = Hist} = cauder_pool:get(Pid, Pool), + case cauder_history:peek(Hist) of + {value, #hist_sendA{msg = #message{uid = Uid}}} -> + rollback_step(Pid, Sys0); + {value, _} -> + Sys1 = rollback_step(Pid, Sys0), + rollback_until_senda(Pid, Sys1, Uid) + end. + -spec rollback_until_receive(Pid, System, Uid) -> NewSystem when Pid :: cauder_process:id(), System :: cauder_system:system(), @@ -376,10 +700,44 @@ rollback_after_receive(Pid, Sys0, Uid) -> case cauder_history:peek(Hist) of {value, #hist_send{msg = #message{uid = Uid}}} -> rollback_after_receive(Pid, Sys1, Uid); + {value, #hist_sendA{msg = #message{uid = Uid}}} -> + rollback_after_receive(Pid, Sys1, Uid); {value, _} -> Sys1 end. +-spec rollback_until_reg(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +rollback_until_reg(Pid, #system{pool = Pool} = Sys0, El) -> + #process{hist = Hist} = cauder_pool:get(Pid, Pool), + case cauder_history:peek(Hist) of + {value, #hist_regS{mapEl = El}} -> + rollback_step(Pid, Sys0); + {value, _} -> + Sys1 = rollback_step(Pid, Sys0), + rollback_until_reg(Pid, Sys1, El) + end. + +-spec rollback_until_del(Pid, System, El) -> NewSystem when + Pid :: cauder_process:id(), + System :: cauder_system:system(), + El :: cauder_map:map_element(), + NewSystem :: cauder_system:system(). + +rollback_until_del(Pid, #system{pool = Pool} = Sys0, El) -> + #process{hist = Hist} = cauder_pool:get(Pid, Pool), + case cauder_history:peek(Hist) of + {value, #hist_del{mapEl = El}} -> + rollback_step(Pid, Sys0); + {value, _} -> + Sys1 = rollback_step(Pid, Sys0), + rollback_until_del(Pid, Sys1, El) + end. + -spec rollback_until_variable(Pid, System, Name) -> NewSystem when Pid :: cauder_process:id(), System :: cauder_system:system(), diff --git a/src/cauder_semantics.erl b/src/cauder_semantics.erl index ebf10ae..0c58548 100644 --- a/src/cauder_semantics.erl +++ b/src/cauder_semantics.erl @@ -21,4 +21,7 @@ | ?RULE_START | ?RULE_SPAWN | ?RULE_SEND - | ?RULE_RECEIVE. + | ?RULE_RECEIVE + | ?RULE_READ + | ?RULE_REG + | ?RULE_DEL. diff --git a/src/cauder_semantics_backwards.erl b/src/cauder_semantics_backwards.erl index 5c6c75a..5e375c8 100644 --- a/src/cauder_semantics_backwards.erl +++ b/src/cauder_semantics_backwards.erl @@ -48,6 +48,18 @@ step(Pid, #system{pool = Pool} = Sys0) -> rule_node(Pid, Entry, Sys); #hist_nodes{} -> rule_nodes(Pid, Entry, Sys); + #hist_registered{} -> + rule_registered(Pid, Entry, Sys); + #hist_readS{} -> + rule_read_s(Pid, Entry, Sys); + #hist_readF{} -> + rule_read_f(Pid, Entry, Sys); + #hist_regS{} -> + rule_reg_s(Pid, Entry, Sys); + #hist_del{} -> + rule_del(Pid, Entry, Sys); + #hist_sendA{} -> + rule_send_a(Pid, Entry, Sys); #hist_start{} -> rule_start(Pid, Entry, Sys); #hist_spawn{} -> @@ -111,6 +123,74 @@ rule_self(Pid, #hist_self{env = Bs, expr = Es, stack = Stk}, Sys) -> rule_node(Pid, #hist_node{env = Bs, expr = Es, stack = Stk}, Sys) -> rule_simple(Pid, {Bs, Es, Stk}, Sys). +-spec rule_registered(Pid, Entry, System) -> NewSystem when + Pid :: cauder_process:id(), + Entry :: cauder_history:entry_registered(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_registered(Pid, #hist_registered{map = MapRd} = Entry, #system{pool = Pool} = Sys) -> + P0 = cauder_pool:get(Pid, Pool), + P1 = P0#process{ + env = Entry#hist_registered.env, + expr = Entry#hist_registered.expr, + stack = Entry#hist_registered.stack + }, + LogAction = #log_read{ + map = MapRd + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = cauder_log:push(Pid, LogAction, Sys#system.log) + }. + +-spec rule_read_s(Pid, Entry, System) -> NewSystem when + Pid :: cauder_process:id(), + Entry :: cauder_history:entry_readS(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_read_s(Pid, #hist_readS{atom = A, pid = P, mapEl = MapRd} = Entry, #system{pool = Pool} = Sys) -> + P0 = cauder_pool:get(Pid, Pool), + P1 = P0#process{ + env = Entry#hist_readS.env, + expr = Entry#hist_readS.expr, + stack = Entry#hist_readS.stack + }, + LogAction = #log_read{ + atom = A, + pid = P, + map = MapRd + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = cauder_log:push(Pid, LogAction, Sys#system.log) + }. + +-spec rule_read_f(Pid, Entry, System) -> NewSystem when + Pid :: cauder_process:id(), + Entry :: cauder_history:entry_readF(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_read_f(Pid, #hist_readF{atom = AP, mapGhost = MapRd} = Entry, #system{pool = Pool} = Sys) -> + P0 = cauder_pool:get(Pid, Pool), + P1 = P0#process{ + env = Entry#hist_readF.env, + expr = Entry#hist_readF.expr, + stack = Entry#hist_readF.stack, + is_alive = true + }, + LogAction = #log_read{ + atom = AP, + pid = AP, + map = MapRd + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = cauder_log:push(Pid, LogAction, Sys#system.log) + }. + -spec rule_simple(Pid, {Bs, Es, Stk}, System) -> NewSystem when Pid :: cauder_process:id(), Bs :: cauder_bindings:bindings(), @@ -188,9 +268,14 @@ rule_start( node = Node, success = Success }, + Nodes = + case Success of + true -> lists:delete(Node, Sys#system.nodes); + false -> Sys#system.nodes + end, Sys#system{ pool = cauder_pool:update(P, Pool), - nodes = lists:delete(Node, Sys#system.nodes), + nodes = Nodes, log = cauder_log:push(Pid, LogAction, Sys#system.log), trace = cauder_trace:pop(Pid, TraceAction, Sys#system.trace) }. @@ -289,6 +374,101 @@ rule_receive( trace = cauder_trace:pop(Pid, TraceAction, Sys#system.trace) }. +-spec rule_del(Pid, Entry, System) -> NewSystem when + Pid :: cauder_process:id(), + Entry :: cauder_history:entry_del(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_del( + Pid, + #hist_del{mapEl = El = {A, P, K, top}} = Entry, + #system{pool = Pool} = Sys +) -> + P0 = cauder_pool:get(Pid, Pool), + P1 = P0#process{ + env = Entry#hist_del.env, + expr = Entry#hist_del.expr, + stack = Entry#hist_del.stack, + is_alive = true + }, + SystemMap = cauder_map:get_map(Sys#system.maps, P0#process.node), + NewMaps = lists:delete({SystemMap, P1#process.node}, Sys#system.maps), + NewMap = lists:delete({A, P, K, bot}, lists:append(SystemMap, [El])), + LogAction = #log_del{ + key = K, + atom = A, + pid = P, + map = sets:to_list( + sets:from_list(cauder_map:get_ghost_list(A, NewMap, []) ++ cauder_map:get_ghost_list(P, NewMap, [])) + ) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + maps = lists:append(NewMaps, [{NewMap, P1#process.node}]), + log = cauder_log:push(Pid, LogAction, Sys#system.log) + }. + +-spec rule_reg_s(Pid, Entry, System) -> NewSystem when + Pid :: cauder_process:id(), + Entry :: cauder_history:entry_regS(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_reg_s( + Pid, + #hist_regS{mapEl = El = {A, P, K, _}} = Entry, + #system{pool = Pool} = Sys +) -> + P0 = cauder_pool:get(Pid, Pool), + P1 = P0#process{ + env = Entry#hist_regS.env, + expr = Entry#hist_regS.expr, + stack = Entry#hist_regS.stack + }, + SystemMap = cauder_map:get_map(Sys#system.maps, P1#process.node), + NewMaps = lists:delete({SystemMap, P1#process.node}, Sys#system.maps), + NewMap = lists:delete(El, SystemMap), + LogAction = #log_reg{ + key = K, + atom = A, + pid = P, + map = cauder_map:get_ghost_list(A, SystemMap, []) ++ cauder_map:get_ghost_list(P, SystemMap, []) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + maps = lists:append(NewMaps, [{NewMap, P1#process.node}]), + log = cauder_log:push(Pid, LogAction, Sys#system.log) + }. + +-spec rule_send_a(Pid, Entry, System) -> NewSystem when + Pid :: cauder_process:id(), + Entry :: cauder_history:entry_sendA(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_send_a( + Pid, + #hist_sendA{msg = Msg, mapEl = MapRd} = Entry, + #system{mail = Mail, pool = Pool} = Sys +) -> + {_, OldMail} = cauder_mailbox:remove(Msg, Mail), + P0 = cauder_pool:get(Pid, Pool), + P = P0#process{ + env = Entry#hist_sendA.env, + expr = Entry#hist_sendA.expr, + stack = Entry#hist_sendA.stack + }, + LogAction = #log_sendA{ + uid = Msg#message.uid, + el = MapRd + }, + Sys#system{ + mail = OldMail, + pool = cauder_pool:update(P, Pool), + log = cauder_log:push(Pid, LogAction, Sys#system.log) + }. + %%%============================================================================= %%------------------------------------------------------------------------------ @@ -318,6 +498,57 @@ process_option(Pid, Sys) -> _ -> false end; + {value, #hist_registered{map = Map, node = Node}} -> + M = cauder_map:get_map(Sys#system.maps, Node), + case Map =:= M of + true -> {ok, ?RULE_READ}; + false -> false + end; + {value, #hist_readS{mapEl = El, node = Node}} -> + M = cauder_map:get_map(Sys#system.maps, Node), + case cauder_map:in_map(M, El) of + true -> {ok, ?RULE_READ}; + false -> false + end; + {value, #hist_readF{atom = A, mapGhost = MG, node = Node}} -> + M = cauder_map:get_map(Sys#system.maps, Node), + Ghost = cauder_map:get_ghost_list(A, M, []), + case {Ghost =:= MG, cauder_map:not_in_map(M, A)} of + {true, true} -> {ok, ?RULE_READ}; + _ -> false + end; + {value, #hist_regS{mapEl = El, node = Node}} -> + M = cauder_map:get_map(Sys#system.maps, Node), + PairsInMap = cauder_map:is_in_map(M, El), + ProcWithRead = cauder_pool:find_read_map(Pool1, Node, El), + case {PairsInMap, ProcWithRead} of + {true, error} -> {ok, ?RULE_REG}; + _ -> false + end; + {value, #hist_del{map = MapG, mapEl = {A, P, K, _}, node = Node}} -> + SystemMap = cauder_map:get_map(Sys#system.maps, Node), + AtomInMap = cauder_map:not_in_map(SystemMap, A), + PidInMap = cauder_map:not_in_map(SystemMap, P), + LG = cauder_map:get_ghost_list(A, SystemMap, []) ++ cauder_map:get_ghost_list(P, SystemMap, []), + ProcWithRegistered = cauder_pool:find_registered(Pool1, Node, SystemMap), + ProcWithFailRead = cauder_pool:find_failed_read_map(Pool1, Node, {A, P, K, bot}), + case {AtomInMap, PidInMap, LG =:= MapG, ProcWithRegistered, ProcWithFailRead} of + {true, true, true, error, error} -> {ok, ?RULE_DEL}; + _ -> false + end; + {value, #hist_sendA{mapEl = El, node = Node, msg = #message{uid = Uid}}} -> + M = cauder_map:get_map(Sys#system.maps, Node), + case cauder_map:in_map(M, [El]) of + true -> + case cauder_mailbox:is_element(Uid, Sys#system.mail) of + true -> + {ok, ?RULE_SEND}; + false -> + false + end; + false -> + false + end; {value, #hist_spawn{pid = SpawnPid}} -> case cauder_pool:find(SpawnPid, Pool1) of error -> diff --git a/src/cauder_semantics_forwards.erl b/src/cauder_semantics_forwards.erl index 5aaad74..ca477bf 100644 --- a/src/cauder_semantics_forwards.erl +++ b/src/cauder_semantics_forwards.erl @@ -41,6 +41,7 @@ step(Pid, Sys, Sched, Mode) -> #process{stack = Stk0, env = Bs0, expr = Es0} = cauder_pool:get(Pid, Sys#system.pool), Result = cauder_eval:seq(Bs0, Es0, Stk0), case Result#result.label of + % consider the map contains ghost #label_tau{} -> rule_local(Pid, Result, Sys); #label_self{} -> @@ -49,12 +50,25 @@ step(Pid, Sys, Sched, Mode) -> rule_node(Pid, Result, Sys); #label_nodes{} -> rule_nodes(Pid, Result, Sys); + % consider the map contains ghost + #label_registered{} -> + rule_registered(Pid, Result, Sys); + % consider the map contains ghost + #label_whereis{} -> + rule_whereis(Pid, Result, Sys); + % consider the map contains ghost + #label_register{} -> + rule_register(Pid, Result, Sys); + % consider the map contains ghost + #label_unregister{} -> + rule_unregister(Pid, Result, Sys); #label_start{} -> rule_start(Pid, Result, Sys); #label_spawn_fun{} -> rule_spawn(Pid, Result, Sys); #label_spawn_mfa{} -> rule_spawn(Pid, Result, Sys); + % consider the map contains ghost #label_send{} -> rule_send(Pid, Result, Sys); #label_receive{var = Var} when Result#result.expr == [Var] -> @@ -94,6 +108,92 @@ options(#system{pool = Pool} = Sys, Mode) -> System :: cauder_system:system(), NewSystem :: cauder_system:system(). +rule_local( + Pid, + #result{expr = [{'value', _, _}], stack = Stk, label = #label_tau{}} = Result, + #system{pool = Pool, maps = Maps, log = Log0} = Sys +) -> + case cauder_stack:is_empty(Stk) of + true -> + P0 = cauder_pool:get(Pid, Pool), + M = cauder_map:get_map(Maps, P0#process.node), + case cauder_map:find_atom(Pid, M) of + {A, K} -> + Log1 = + case cauder_log:pop_del(Pid, Log0) of + {#log_del{} = _, Log} -> + Log; + error -> + Log0 + end, + NewMaps = Maps -- [{M, P0#process.node}], + NewMap = (M -- [{A, Pid, K, top}]) ++ [{A, Pid, K, bot}], + HistEntry = #hist_del{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + mapEl = {A, Pid, K, top}, + map = cauder_map:get_ghost_list(A, NewMap, []) ++ cauder_map:get_ghost_list(Pid, NewMap, []) + }, + P1 = P0#process{ + env = Result#result.env, + expr = Result#result.expr, + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist), + is_alive = false + }, + Sys#system{ + maps = NewMaps ++ [{NewMap, P0#process.node}], + pool = cauder_pool:update(P1, Pool), + log = Log1 + }; + undefined -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + Ghost = cauder_map:get_ghost_list(Pid, M, []), + HistEntry = #hist_readF{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Pid, + mapGhost = Ghost + }, + P1 = P0#process{ + env = Result#result.env, + expr = Result#result.expr, + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist), + is_alive = false + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + } + end; + false -> + P0 = cauder_pool:get(Pid, Pool), + HistEntry = #hist_tau{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack + }, + P1 = P0#process{ + env = Result#result.env, + expr = Result#result.expr, + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool) + } + end; rule_local( Pid, #result{label = #label_tau{}} = Result, @@ -181,15 +281,14 @@ rule_nodes( #system{pool = Pool, log = Log0} = Sys ) -> P0 = cauder_pool:get(Pid, Pool), - - {LogEntry, Log1} = + {Nodes, Log1} = case cauder_log:pop_nodes(Pid, Log0) of - {#log_nodes{} = Entry, Log} -> - {Entry, Log}; + {#log_nodes{nodes = Nodes1}, Log} -> + {Nodes1, Log}; error -> {Sys#system.nodes, Log0} end, - OtherNodes = lists:delete(P0#process.node, LogEntry#log_nodes.nodes), + OtherNodes = lists:delete(P0#process.node, Nodes), HistEntry = #hist_nodes{ env = P0#process.env, @@ -238,14 +337,25 @@ rule_start( Host0 end end, - - Node = list_to_atom(atom_to_list(Name) ++ "@" ++ atom_to_list(Host)), + %io:format("\n Host ~p \n", [Host]), + %io:format("\n Name ~p \n", [Name]), + AtomName = + case is_atom(Name) of + true -> + %io:format("\n I am Here TRUE ~p \n", [Name]), + Name; + _ -> + %io:format("\n I am Here False~p \n", [Name]), + list_to_atom(Name) + end, + Node = list_to_atom(atom_to_list(AtomName) ++ "@" ++ atom_to_list(Host)), + %io:format("\n Node ~p \n", [Node]), {LogEntry, Log1} = case cauder_log:pop_start(Pid, Log0) of {#log_start{node = Node} = Entry, Log} -> % Assert node is not started - false = lists:member(Node, Nodes0), + %false = lists:member(Node, Nodes0), {Entry, Log}; error -> Entry = #log_start{ @@ -330,8 +440,8 @@ rule_spawn( expr = P0#process.expr, stack = P0#process.stack, node = LogEntry#log_spawn.node, - pid = LogEntry#log_spawn.pid - %success = LogEntry#log_spawn.success + pid = LogEntry#log_spawn.pid, + success = LogEntry#log_spawn.success }, P1 = P0#process{ @@ -386,43 +496,114 @@ rule_send( #result{label = #label_send{dst = Dst, val = Val}} = Result, #system{pool = Pool, log = Log0} = Sys ) -> - {Uid, Log1} = - case cauder_log:pop_send(Pid, Log0) of - {#log_send{} = Entry, Log} -> - {Entry#log_send.uid, Log}; - error -> - {cauder_message:new_uid(), Log0} - end, + case erlang:is_atom(Dst) of + true -> + P0 = cauder_pool:get(Pid, Pool), + Map = cauder_map:get_map(Sys#system.maps, P0#process.node), + case cauder_map:find_pid(Dst, Map) of + undefined -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + [{send_op, Line, _, _}, _] = P0#process.expr, + Ghost = cauder_map:get_ghost_list(Dst, Map, []), + HistEntry = #hist_readF{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Dst, + mapGhost = Ghost + }, + P1 = P0#process{ + env = Result#result.env, + expr = [{value, Line, error}], + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + }; + {PidDst, Key} -> + {Uid, Log1} = + case cauder_log:pop_send(Pid, Log0) of + {#log_sendA{} = Entry, Log} -> + {Entry#log_sendA.uid, Log}; + error -> + {cauder_message:new_uid(), Log0} + end, - M = #message{ - uid = Uid, - src = Pid, - dst = Dst, - val = Val - }, + M = #message{ + uid = Uid, + src = Pid, + dst = PidDst, + val = Val + }, - P0 = cauder_pool:get(Pid, Pool), - HistEntry = #hist_send{ - env = P0#process.env, - expr = P0#process.expr, - stack = P0#process.stack, - msg = M - }, - P1 = P0#process{ - env = Result#result.env, - expr = Result#result.expr, - stack = Result#result.stack, - hist = cauder_history:push(HistEntry, P0#process.hist) - }, - TraceAction = #trace_send{ - uid = Uid - }, - Sys#system{ - mail = cauder_mailbox:add(M, Sys#system.mail), - pool = cauder_pool:update(P1, Pool), - log = Log1, - trace = cauder_trace:push(Pid, TraceAction, Sys#system.trace) - }. + HistEntry = #hist_sendA{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + msg = M, + mapEl = {Dst, PidDst, Key, top} + }, + P1 = P0#process{ + env = Result#result.env, + expr = Result#result.expr, + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + mail = cauder_mailbox:add(M, Sys#system.mail), + pool = cauder_pool:update(P1, Pool), + log = Log1 + } + end; + false -> + {Uid, Log1} = + case cauder_log:pop_send(Pid, Log0) of + {#log_send{} = Entry, Log} -> + {Entry#log_send.uid, Log}; + error -> + {cauder_message:new_uid(), Log0} + end, + + M = #message{ + uid = Uid, + src = Pid, + dst = Dst, + val = Val + }, + + P0 = cauder_pool:get(Pid, Pool), + HistEntry = #hist_send{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + msg = M + }, + P1 = P0#process{ + env = Result#result.env, + expr = Result#result.expr, + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + TraceAction = #trace_send{ + uid = Uid + }, + Sys#system{ + mail = cauder_mailbox:add(M, Sys#system.mail), + pool = cauder_pool:update(P1, Pool), + log = Log1, + trace = cauder_trace:push(Pid, TraceAction, Sys#system.trace) + } + end. -spec rule_receive(Pid, Result, Mode, Scheduler, System) -> NewSystem when Pid :: cauder_process:id(), @@ -481,6 +662,343 @@ rule_receive( trace = cauder_trace:push(Pid, TraceAction, Sys#system.trace) }. +-spec rule_registered(Pid, Result, System) -> NewSystem when + Pid :: cauder_process:id(), + Result :: cauder_eval:result(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_registered( + Pid, + #result{label = #label_registered{var = VarMap}} = Result, + #system{pool = Pool, maps = Maps, log = Log0} = Sys +) -> + P0 = cauder_pool:get(Pid, Pool), + M = cauder_map:get_map(Maps, P0#process.node), + L = cauder_map:get_atoms_list(M, []), + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + HistEntry = #hist_registered{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + map = M + }, + P1 = P0#process{ + env = Result#result.env, + expr = cauder_syntax:replace_variable(Result#result.expr, VarMap, L), + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + }. + +-spec rule_whereis(Pid, Result, System) -> NewSystem when + Pid :: cauder_process:id(), + Result :: cauder_eval:result(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_whereis( + Pid, + #result{label = #label_whereis{var = VarPid, atom = Atom}} = Result, + #system{pool = Pool, maps = Maps, log = Log0} = Sys +) -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + P0 = cauder_pool:get(Pid, Pool), + M = cauder_map:get_map(Maps, P0#process.node), + P1 = + case cauder_map:find_pid(Atom, M) of + undefined -> + Ghost = cauder_map:get_ghost_list(Atom, M, []), + HistEntry = #hist_readF{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + mapGhost = Ghost + }, + P0#process{ + env = Result#result.env, + expr = cauder_syntax:replace_variable(Result#result.expr, VarPid, undefined), + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }; + {MyPid, K} -> + HistEntry = #hist_readS{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + pid = MyPid, + mapEl = [{Atom, MyPid, K, top}] + }, + P0#process{ + env = Result#result.env, + expr = cauder_syntax:replace_variable(Result#result.expr, VarPid, MyPid), + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + } + end, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + }. + +-spec rule_register(Pid, Result, System) -> NewSystem when + Pid :: cauder_process:id(), + Result :: cauder_eval:result(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_register( + Pid, + #result{label = #label_register{var = VarResult, atom = Atom, pid = MyPid}} = Result, + #system{pool = Pool, maps = Maps, log = Log0} = Sys +) -> + P0 = cauder_pool:get(Pid, Pool), + M = cauder_map:get_map(Maps, P0#process.node), + case cauder_map:find_pid(Atom, M) of + undefined -> + case cauder_map:find_atom(MyPid, M) of + undefined -> + {Key, Log1} = + case cauder_log:pop_reg(Pid, Log0) of + {#log_reg{} = Entry, Log} -> + {Entry#log_reg.key, Log}; + error -> + {cauder_map:new_key(), Log0} + end, + HistEntry = #hist_regS{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + mapEl = {Atom, MyPid, Key, top} + }, + P1 = P0#process{ + env = Result#result.env, + expr = cauder_syntax:replace_variable(Result#result.expr, VarResult, true), + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + NewMaps = Maps -- [{M, P0#process.node}], + NewMap = M ++ [{Atom, MyPid, Key, top}], + Sys#system{ + maps = NewMaps ++ [{NewMap, P0#process.node}], + pool = cauder_pool:update(P1, Pool), + log = Log1 + }; + {MapAtom, K} -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + {var, Line, _} = VarResult, + HistEntry = #hist_readS{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + pid = MyPid, + mapEl = [{MapAtom, MyPid, K, top}] + }, + P1 = P0#process{ + env = Result#result.env, + expr = [{value, Line, error}], + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + } + end; + {MapPid, K1} -> + case cauder_map:find_atom(MyPid, M) of + undefined -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + {var, Line, _} = VarResult, + HistEntry = #hist_readS{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + pid = MyPid, + mapEl = [{Atom, MapPid, K1, top}] + }, + P1 = P0#process{ + env = Result#result.env, + expr = [{value, Line, error}], + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + }; + {MapAtom, K2} -> + case {MapAtom, MyPid} =:= {Atom, MapPid} of + true -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + {var, Line, _} = VarResult, + HistEntry = #hist_readS{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + pid = MyPid, + mapEl = [{MapAtom, MyPid, K1, top}] + }, + P1 = P0#process{ + env = Result#result.env, + expr = [{value, Line, error}], + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + }; + false -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + {var, Line, _} = VarResult, + HistEntry = #hist_readS{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + pid = MyPid, + mapEl = [{MapAtom, MyPid, K2, top}, {Atom, MapPid, K1, top}] + }, + P1 = P0#process{ + env = Result#result.env, + expr = [{value, Line, error}], + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + } + end + end + end. + +-spec rule_unregister(Pid, Result, System) -> NewSystem when + Pid :: cauder_process:id(), + Result :: cauder_eval:result(), + System :: cauder_system:system(), + NewSystem :: cauder_system:system(). + +rule_unregister( + Pid, + #result{label = #label_unregister{var = VarResult, atom = Atom}} = Result, + #system{pool = Pool, maps = Maps, log = Log0} = Sys +) -> + P0 = cauder_pool:get(Pid, Pool), + M = cauder_map:get_map(Maps, P0#process.node), + case cauder_map:find_pid(Atom, M) of + undefined -> + Log1 = + case cauder_log:pop_read(Pid, Log0) of + {#log_read{} = _, Log} -> + Log; + error -> + Log0 + end, + {var, Line, _} = VarResult, + Ghost = cauder_map:get_ghost_list(Atom, M, []), + HistEntry = #hist_readF{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + atom = Atom, + mapGhost = Ghost + }, + P1 = P0#process{ + env = Result#result.env, + expr = [{value, Line, error}], + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + pool = cauder_pool:update(P1, Pool), + log = Log1 + }; + {MapPid, K} -> + {Key, Log1} = + case cauder_log:pop_del(Pid, Log0) of + {#log_del{} = Entry, Log} -> + {Entry#log_del.key, Log}; + error -> + {K, Log0} + end, + NewMaps = Maps -- [{M, P0#process.node}], + NewMap = (M -- [{Atom, MapPid, K, top}]) ++ [{Atom, MapPid, K, bot}], + HistEntry = #hist_del{ + env = P0#process.env, + expr = P0#process.expr, + stack = P0#process.stack, + node = P0#process.node, + mapEl = {Atom, MapPid, Key, top}, + map = cauder_map:get_ghost_list(Atom, NewMap, []) ++ cauder_map:get_ghost_list(MapPid, NewMap, []) + }, + P1 = P0#process{ + env = Result#result.env, + expr = cauder_syntax:replace_variable(Result#result.expr, VarResult, true), + stack = Result#result.stack, + hist = cauder_history:push(HistEntry, P0#process.hist) + }, + Sys#system{ + maps = NewMaps ++ [{NewMap, P0#process.node}], + pool = cauder_pool:update(P1, Pool), + log = Log1 + } + end. + %%%============================================================================= %%------------------------------------------------------------------------------ @@ -496,6 +1014,7 @@ rule_receive( expression_option([E0 | Es0], Pid, Sys, Mode) -> Proc = cauder_pool:get(Pid, Sys#system.pool), + %TODO is alive false check for del or read otherwhise normal check case is_reducible(E0, Proc#process.env) of false -> case {Es0, cauder_stack:is_empty(Proc#process.stack)} of @@ -516,6 +1035,14 @@ expression_option([E0 | Es0], Pid, Sys, Mode) -> {ok, ?RULE_SELF}; {node, _} -> {ok, ?RULE_NODE}; + {registered, _} -> + check_reducibility([], Pid, Sys, Mode, registered); + {whereis, _, A} -> + check_reducibility([A], Pid, Sys, Mode, whereis); + {register, _, A, P} -> + check_reducibility([A, P], Pid, Sys, Mode, register); + {unregister, _, A} -> + check_reducibility([A], Pid, Sys, Mode, unregister); {tuple, _, Es} -> expression_option(Es, Pid, Sys, Mode); {nodes, _} -> @@ -563,10 +1090,34 @@ expression_option([E0 | Es0], Pid, Sys, Mode) -> end end. -check_reducibility([], _, _, _, send) -> - {ok, ?RULE_SEND}; -check_reducibility([], _, _, _, send_op) -> - {ok, ?RULE_SEND}; +check_reducibility([], Pid, #system{maps = Maps, log = Log} = Sys, _, send) -> + Proc = cauder_pool:get(Pid, Sys#system.pool), + SystemMap = cauder_map:get_map(Maps, Proc#process.node), + case cauder_log:peek(Pid, Log) of + {value, #log_sendA{el = El}} -> + case cauder_map:is_in_map(SystemMap, El) of + true -> + {ok, ?RULE_SEND}; + _ -> + false + end; + _ -> + {ok, ?RULE_SEND} + end; +check_reducibility([], Pid, #system{maps = Maps, log = Log} = Sys, _, send_op) -> + Proc = cauder_pool:get(Pid, Sys#system.pool), + SystemMap = cauder_map:get_map(Maps, Proc#process.node), + case cauder_log:peek(Pid, Log) of + {value, #log_sendA{el = El}} -> + case cauder_map:is_in_map(SystemMap, El) of + true -> + {ok, ?RULE_SEND}; + _ -> + false + end; + _ -> + {ok, ?RULE_SEND} + end; check_reducibility([], _, _, _, local_call) -> {ok, ?RULE_LOCAL}; check_reducibility([], _, _, _, remote_call) -> @@ -630,15 +1181,17 @@ check_reducibility([], Pid, #system{log = Log, nodes = Nodes}, _, start) -> case cauder_log:find_failed_spawns(Node, Log) of [_ | _] when Success -> false; - [] -> + _ -> case cauder_log:find_nodes(Node, Log) of [_ | _] when Success -> false; - [] -> + _ -> case lists:member(Node, Nodes) of false when not Success -> false; - true -> + true when Success -> + false; + _ -> {ok, ?RULE_START} end end @@ -646,6 +1199,95 @@ check_reducibility([], Pid, #system{log = Log, nodes = Nodes}, _, start) -> _ -> {ok, ?RULE_START} end; +check_reducibility([], Pid, #system{maps = Maps, log = Log} = Sys, _, whereis) -> + Proc = cauder_pool:get(Pid, Sys#system.pool), + SystemMap = cauder_map:get_map(Maps, Proc#process.node), + case cauder_log:peek(Pid, Log) of + {value, #log_read{map = M}} -> + case cauder_map:in_map(SystemMap, M) of + true -> + {ok, ?RULE_READ}; + _ -> + false + end; + _ -> + {ok, ?RULE_READ} + end; +check_reducibility([], Pid, #system{maps = Maps, log = Log} = Sys, _, registered) -> + Proc = cauder_pool:get(Pid, Sys#system.pool), + SystemMap = cauder_map:get_map(Maps, Proc#process.node), + case cauder_log:peek(Pid, Log) of + {value, #log_read{map = M}} -> + case {SystemMap -- M, M -- SystemMap} of + {[], []} -> + {ok, ?RULE_READ}; + _ -> + false + end; + _ -> + {ok, ?RULE_READ} + end; +check_reducibility([], Pid, #system{maps = Maps, log = Log} = Sys, _, register) -> + Proc = cauder_pool:get(Pid, Sys#system.pool), + SystemMap = cauder_map:get_map(Maps, Proc#process.node), + case cauder_log:peek(Pid, Log) of + {value, #log_reg{key = K, atom = A, pid = P, map = M}} -> + case + { + cauder_map:in_map(SystemMap, M), + cauder_map:find_pid(A, SystemMap) =:= cauder_map:find_atom(P, SystemMap), + cauder_log:find_fail_read({A, P, K, bot}, M, Log) =:= error, + cauder_log:find_registered(M, Log) =:= error + } + of + {true, true, true, true} -> + {ok, ?RULE_REG}; + _ -> + false + end; + {value, #log_read{atom = A, pid = P, map = M}} -> + case + { + cauder_map:in_map(SystemMap, M), + cauder_map:find_pid(A, SystemMap) =/= cauder_map:find_atom(P, SystemMap) + } + of + {true, true} -> + {ok, ?RULE_REG}; + _ -> + false + end; + _ -> + {ok, ?RULE_REG} + end; +check_reducibility([], Pid, #system{maps = Maps, log = Log} = Sys, _, unregister) -> + Proc = cauder_pool:get(Pid, Sys#system.pool), + SystemMap = cauder_map:get_map(Maps, Proc#process.node), + case cauder_log:peek(Pid, Log) of + {value, #log_del{atom = A, pid = P, key = K, map = M}} -> + case + { + cauder_map:in_map(SystemMap, M), + cauder_map:find_pid(A, SystemMap), + cauder_log:find_success_read({A, P, K, top}, Log) =:= error, + cauder_log:find_registered(M, Log) =:= error + } + of + {true, S, true, true} when S =/= undefined -> + {ok, ?RULE_DEL}; + _ -> + false + end; + {value, #log_read{atom = A, map = M}} -> + case {cauder_map:in_map(SystemMap, M), cauder_map:find_pid(A, SystemMap)} of + {true, undefined} -> + {ok, ?RULE_DEL}; + _ -> + false + end; + _ -> + {ok, ?RULE_DEL} + end; check_reducibility([H | T], Pid, Sys, Mode, ExprType) -> #process{env = Bs} = cauder_pool:get(Pid, Sys#system.pool), case is_reducible(H, Bs) of diff --git a/src/cauder_syntax.erl b/src/cauder_syntax.erl index b2f8c21..f15bb91 100644 --- a/src/cauder_syntax.erl +++ b/src/cauder_syntax.erl @@ -54,6 +54,10 @@ | af_self_call() | af_node_call() | af_nodes_call() + | af_registered_call() + | af_whereis_call() + | af_register_call() + | af_unregister_call() | af_start_1_call() | af_start_2_call() | af_spawn_1_call() @@ -98,6 +102,14 @@ -type af_nodes_call() :: {nodes, line()}. +-type af_registered_call() :: {registered, line()}. + +-type af_whereis_call() :: {whereis, line(), abstract_expr()}. + +-type af_register_call() :: {register, line(), abstract_expr(), abstract_expr()}. + +-type af_unregister_call() :: {unregister, line(), abstract_expr()}. + -type af_start_1_call() :: {start, line(), abstract_expr()}. -type af_start_2_call() :: {start, line(), abstract_expr(), abstract_expr()}. @@ -158,7 +170,11 @@ | af_guard_call() | af_self_call() | af_node_call() - | af_nodes_call(). + | af_nodes_call() + | af_registered_call() + | af_whereis_call() + | af_register_call() + | af_unregister_call(). -type af_guard_call() :: {'bif', line(), erlang, atom(), [af_guard_test()]}. @@ -295,6 +311,14 @@ guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, node}}, []}) -> {node, ln(Anno)}; guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, nodes}}, []}) -> {nodes, ln(Anno)}; +guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, registered}}, []}) -> + {registered, ln(Anno)}; +guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, whereis}}, [Atom]}) -> + {whereis, ln(Anno), expr(Atom)}; +guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, register}}, [Atom, Pid]}) -> + {register, ln(Anno), expr(Atom), expr(Pid)}; +guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, unregister}}, [Atom]}) -> + {unregister, ln(Anno), expr(Atom)}; guard_test({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, F}}, As0}) -> check_guard_bif(F, length(As0)), As = gexpr_list(As0), @@ -373,6 +397,14 @@ gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, node}}, []}) -> {node, ln(Anno)}; gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, nodes}}, []}) -> {nodes, ln(Anno)}; +gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, registered}}, []}) -> + {registered, ln(Anno)}; +gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, whereis}}, [Atom]}) -> + {whereis, ln(Anno), expr(Atom)}; +gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, register}}, [Atom, Pid]}) -> + {register, ln(Anno), expr(Atom), expr(Pid)}; +gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, unregister}}, [Atom]}) -> + {unregister, ln(Anno), expr(Atom)}; gexpr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, F}}, As0}) -> check_guard_bif(F, length(As0)), As = gexpr_list(As0), @@ -449,6 +481,14 @@ expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, node}}, []}) -> {node, ln(Anno)}; expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, nodes}}, []}) -> {nodes, ln(Anno)}; +expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, registered}}, []}) -> + {registered, ln(Anno)}; +expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, whereis}}, [Atom]}) -> + {whereis, ln(Anno), expr(Atom)}; +expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, register}}, [Atom, Pid]}) -> + {register, ln(Anno), expr(Atom), expr(Pid)}; +expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, unregister}}, [Atom]}) -> + {unregister, ln(Anno), expr(Atom)}; expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, spawn}}, [Fun]}) -> {spawn, ln(Anno), expr(Fun)}; expr({call, Anno, {remote, _, {atom, _, erlang}, {atom, _, spawn}}, [Node, Fun]}) -> @@ -635,6 +675,18 @@ replace_variable(E = {node, _}, _, _) -> E; replace_variable(E = {nodes, _}, _, _) -> E; +replace_variable(E = {registered, _}, _, _) -> + E; +replace_variable({whereis, Line, Atom}, Var, Val) -> + A = replace_variable(Atom, Var, Val), + {whereis, Line, A}; +replace_variable({register, Line, Atom, Pid}, Var, Val) -> + A = replace_variable(Atom, Var, Val), + P = replace_variable(Pid, Var, Val), + {register, Line, A, P}; +replace_variable({unregister, Line, Atom}, Var, Val) -> + A = replace_variable(Atom, Var, Val), + {unregister, Line, A}; replace_variable({spawn, Line, Fun0}, Var, Val) -> Fun = replace_variable(Fun0, Var, Val), {spawn, Line, Fun}; @@ -757,6 +809,30 @@ to_abstract_expr({node, Line}) -> to_abstract_expr({nodes, Line}) -> Node = erl_syntax:application(erl_syntax:atom(erlang), erl_syntax:atom(nodes), []), set_line(Node, Line); +to_abstract_expr({registered, Line}) -> + Node = erl_syntax:application(erl_syntax:atom(erlang), erl_syntax:atom(registered), []), + set_line(Node, Line); +to_abstract_expr({whereis, Line, Atom}) -> + Node = erl_syntax:application( + erl_syntax:atom(erlang), + erl_syntax:atom(whereis), + [to_abstract_expr(Atom)] + ), + set_line(Node, Line); +to_abstract_expr({register, Line, Atom, Pid}) -> + Node = erl_syntax:application( + erl_syntax:atom(erlang), + erl_syntax:atom(register), + [to_abstract_expr(Atom), to_abstract_expr(Pid)] + ), + set_line(Node, Line); +to_abstract_expr({unregister, Line, Atom}) -> + Node = erl_syntax:application( + erl_syntax:atom(erlang), + erl_syntax:atom(unregister), + [to_abstract_expr(Atom)] + ), + set_line(Node, Line); to_abstract_expr({spawn, Line, Fun}) -> Node = erl_syntax:application(erl_syntax:atom(erlang), erl_syntax:atom(spawn), [to_abstract_expr(Fun)]), set_line(Node, Line); diff --git a/src/cauder_wx.erl b/src/cauder_wx.erl index b30415d..8a9025c 100644 --- a/src/cauder_wx.erl +++ b/src/cauder_wx.erl @@ -383,7 +383,6 @@ handle_event(?BUTTON_EVENT(?ACTION_Replay_Spawn_Button), State) -> cauder_wx_statusbar:replay_spawn_start(Pid), {noreply, refresh(State, State#wx_state{system = System, task = replay_spawn})}; handle_event(?BUTTON_EVENT(?ACTION_Replay_Start_Button), State) -> - io:format("Ciao~n"), Choice = cauder_wx:find(?ACTION_Replay_Start, wxChoice), Idx = wxChoice:getSelection(Choice), Node = wxChoice:getClientData(Choice, Idx), @@ -404,6 +403,22 @@ handle_event(?BUTTON_EVENT(?ACTION_Replay_Receive_Button), State) -> {ok, System} = cauder:replay_receive(Uid), cauder_wx_statusbar:replay_receive_start(Uid), {noreply, refresh(State, State#wx_state{system = System, task = replay_receive})}; +handle_event(?BUTTON_EVENT(?ACTION_Replay_Register_Button), State) -> + Choice = cauder_wx:find(?ACTION_Replay_Register, wxChoice), + Idx = wxChoice:getSelection(Choice), + {_, _, Key} = wxChoice:getClientData(Choice, Idx), + %io:format("\nChoice~p\nIdx=~p\nKey~p\n", [Choice,Idx, Key]), + {ok, System} = cauder:replay_register(wxChoice:getClientData(Choice, Idx)), + cauder_wx_statusbar:replay_register_start(Key), + {noreply, refresh(State, State#wx_state{system = System, task = replay_register})}; +handle_event(?BUTTON_EVENT(?ACTION_Replay_Delete_Button), State) -> + Choice = cauder_wx:find(?ACTION_Replay_Delete, wxChoice), + Idx = wxChoice:getSelection(Choice), + {_, _, Key} = wxChoice:getClientData(Choice, Idx), + %io:format("\nChoice~p\nIdx=~p\nKey~p\n", [Choice,Idx, Key]), + {ok, System} = cauder:replay_delete(wxChoice:getClientData(Choice, Idx)), + cauder_wx_statusbar:replay_delete_start(Key), + {noreply, refresh(State, State#wx_state{system = System, task = replay_delete})}; handle_event(?BUTTON_EVENT(?ACTION_Replay_FullLog_Button), State) -> {ok, System} = cauder:replay_full_log(), cauder_wx_statusbar:replay_full_log_start(), @@ -430,6 +445,29 @@ handle_event(?BUTTON_EVENT(?ACTION_Rollback_Start_Button), State) -> {ok, System} = cauder:rollback_start(Node), cauder_wx_statusbar:rollback_start_begin(Node), {noreply, refresh(State, State#wx_state{system = System, task = rollback_start})}; +handle_event(?BUTTON_EVENT(?ACTION_Rollback_Register_Button), State) -> + Choice = cauder_wx:find(?ACTION_Rollback_Register, wxChoice), + Idx = wxChoice:getSelection(Choice), + {A,B,C} = wxChoice:getClientData(Choice, Idx), + Couple = {A,B,C,top}, + {ok, System} = cauder:rollback_reg(Couple), + cauder_wx_statusbar:rollback_reg_start(Couple), + {noreply, refresh(State, State#wx_state{system = System, task = rollback_reg})}; +handle_event(?BUTTON_EVENT(?ACTION_Rollback_Delete_Button), State) -> + Choice = cauder_wx:find(?ACTION_Rollback_Delete, wxChoice), + Idx = wxChoice:getSelection(Choice), + Couple1 = {A,B,C} = wxChoice:getClientData(Choice, Idx), + Couple = {A,B,C,top}, + {ok, System} = cauder:rollback_del(Couple), + cauder_wx_statusbar:rollback_del_start(Couple), + {noreply, refresh(State, State#wx_state{system = System, task = rollback_del})}; +%handle_event(?BUTTON_EVENT(?ACTION_Rollback_Senda_Button), State) -> +% Choice = cauder_wx:find(?ACTION_Rollback_Senda, wxChoice), +% Idx = wxChoice:getSelection(Choice), +% {_, Uid} = wxChoice:getClientData(Choice, Idx), +% {ok, System} = cauder:rollback_senda(Uid), +% cauder_wx_statusbar:rollback_senda_start(Uid), +% {noreply, refresh(State, State#wx_state{system = System, task = rollback_senda})}; handle_event(?BUTTON_EVENT(?ACTION_Rollback_Send_Button), State) -> Choice = cauder_wx:find(?ACTION_Rollback_Send, wxChoice), Idx = wxChoice:getSelection(Choice), @@ -615,6 +653,18 @@ handle_info(?DBG_SUCCESS(replay_receive, Uid, Time, System), #wx_state{task = re handle_info(?DBG_FAILURE(replay_receive, no_replay, _Stacktrace), #wx_state{task = replay_receive} = State) -> cauder_wx_statusbar:replay_receive_fail(), {noreply, refresh(State, State#wx_state{task = undefined})}; +handle_info(?DBG_SUCCESS(replay_register, Key, Time, System), #wx_state{task = replay_register} = State) -> + cauder_wx_statusbar:replay_register_finish(Key, Time), + {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; +handle_info(?DBG_FAILURE(replay_register, no_replay, _Stacktrace), #wx_state{task = replay_register} = State) -> + cauder_wx_statusbar:replay_register_fail(), + {noreply, refresh(State, State#wx_state{task = undefined})}; +handle_info(?DBG_SUCCESS(replay_delete, Key, Time, System), #wx_state{task = replay_delete} = State) -> + cauder_wx_statusbar:replay_delete_finish(Key, Time), + {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; +handle_info(?DBG_FAILURE(replay_delete, no_replay, _Stacktrace), #wx_state{task = replay_delete} = State) -> + cauder_wx_statusbar:replay_delete_fail(), + {noreply, refresh(State, State#wx_state{task = undefined})}; handle_info(?DBG_SUCCESS(replay_full_log, Time, System), #wx_state{task = replay_full_log} = State) -> cauder_wx_statusbar:replay_full_log_finish(Time), {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; @@ -641,6 +691,24 @@ handle_info(?DBG_SUCCESS(rollback_send, Uid, Time, System), #wx_state{task = rol handle_info(?DBG_FAILURE(rollback_send, no_rollback, _Stacktrace), #wx_state{task = rollback_send} = State) -> cauder_wx_statusbar:rollback_send_fail(), {noreply, refresh(State, State#wx_state{task = undefined})}; +%handle_info(?DBG_SUCCESS(rollback_senda, Uid, Time, System), #wx_state{task = rollback_senda} = State) -> +% cauder_wx_statusbar:rollback_senda_finish(Uid, Time), +% {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; +%handle_info(?DBG_FAILURE(rollback_senda, no_rollback, _Stacktrace), #wx_state{task = rollback_senda} = State) -> +% cauder_wx_statusbar:rollback_senda_fail(), +% {noreply, refresh(State, State#wx_state{task = undefined})}; +handle_info(?DBG_SUCCESS(rollback_reg, El, Time, System), #wx_state{task = rollback_reg} = State) -> + cauder_wx_statusbar:rollback_reg_finish(El, Time), + {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; +handle_info(?DBG_FAILURE(rollback_reg, no_rollback, _Stacktrace), #wx_state{task = rollback_reg} = State) -> + cauder_wx_statusbar:rollback_reg_fail(), + {noreply, refresh(State, State#wx_state{task = undefined})}; +handle_info(?DBG_SUCCESS(rollback_del, El, Time, System), #wx_state{task = rollback_del} = State) -> + cauder_wx_statusbar:rollback_del_finish(El, Time), + {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; +handle_info(?DBG_FAILURE(rollback_del, no_rollback, _Stacktrace), #wx_state{task = rollback_del} = State) -> + cauder_wx_statusbar:rollback_del_fail(), + {noreply, refresh(State, State#wx_state{task = undefined})}; handle_info(?DBG_SUCCESS(rollback_receive, Uid, Time, System), #wx_state{task = rollback_receive} = State) -> cauder_wx_statusbar:rollback_receive_finish(Uid, Time), {noreply, refresh(State, State#wx_state{system = System, task = undefined})}; @@ -767,6 +835,7 @@ refresh(OldState, NewState) -> cauder_wx_actions:update(OldState, State), cauder_wx_process:update(OldState, State), cauder_wx_system:update(OldState, State), + cauder_wx_map:update(OldState, State), State. diff --git a/src/cauder_wx.hrl b/src/cauder_wx.hrl index 7d6c449..ebe52be 100644 --- a/src/cauder_wx.hrl +++ b/src/cauder_wx.hrl @@ -164,6 +164,8 @@ -define(ACTION_Replay_Receive, 2313). -define(ACTION_Replay_Start, 2314). -define(ACTION_Replay_Spawn, 2315). +-define(ACTION_Replay_Register, 2316). +-define(ACTION_Replay_Delete, 2317). -define(ACTION_Replay_Steps_Button, 2320). -define(ACTION_Replay_Send_Button, 2321). @@ -171,6 +173,8 @@ -define(ACTION_Replay_Receive_Button, 2323). -define(ACTION_Replay_Start_Button, 2324). -define(ACTION_Replay_Spawn_Button, 2325). +-define(ACTION_Replay_Register_Button, 2327). +-define(ACTION_Replay_Delete_Button, 2328). -define(ACTION_Replay_FullLog_Button, 2326). %% ----- @@ -185,6 +189,10 @@ -define(ACTION_Rollback_Spawn, 2415). -define(ACTION_Rollback_Variable, 2416). +-define(ACTION_Rollback_Register, 2417). +-define(ACTION_Rollback_Delete, 2418). +-define(ACTION_Rollback_Senda, 2419). + -define(ACTION_Rollback_Steps_Button, 2420). -define(ACTION_Rollback_Send_Button, 2421). %-define(ACTION_Rollback_Deliver_Button, 2422). @@ -193,6 +201,10 @@ -define(ACTION_Rollback_Spawn_Button, 2425). -define(ACTION_Rollback_Variable_Button, 2426). +-define(ACTION_Rollback_Register_Button, 2427). +-define(ACTION_Rollback_Delete_Button, 2428). +-define(ACTION_Rollback_Senda_Button, 2429). + %% ----- System Info Panel ----- %% -define(SYSTEM_Panel, 2500). @@ -214,6 +226,9 @@ -define(SYSTEM_Trace, 2532). -define(SYSTEM_RollLog, 2533). +-define(SYSTEM_Map, 2534). +-define(PROCESS_Map, 2535). + %% ----- Process Info Panel ----- %% -define(PROCESS_Panel, 2600). diff --git a/src/cauder_wx_actions.erl b/src/cauder_wx_actions.erl index 90cf067..3cae06c 100644 --- a/src/cauder_wx_actions.erl +++ b/src/cauder_wx_actions.erl @@ -389,6 +389,13 @@ create_replay(Parent) -> create_choice(Win, Content, "Pid:", ?ACTION_Replay_Spawn, {"Replay spawn", ?ACTION_Replay_Spawn_Button}), wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), + create_choice( + Win, Content, "Map Element:", ?ACTION_Replay_Register, {"Replay register", ?ACTION_Replay_Register_Button} + ), + wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), + create_choice(Win, Content, "Map Element:", ?ACTION_Replay_Delete, {"Replay delete", ?ACTION_Replay_Delete_Button}), + wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), + % Replay Full Log FullLog = wxBoxSizer:new(?wxHORIZONTAL), @@ -427,7 +434,9 @@ update_replay(_, #wx_state{system = #system{log = Log}, pid = Pid}) -> 'send' := SendUids, 'receive' := ReceiveUids, 'start' := StartNodes, - 'spawn' := SpawnPids + 'spawn' := SpawnPids, + 'register' := RegEls, + 'delete' := DelEls } = cauder_log:group_actions(Log), update_choice(?ACTION_Replay_Send, ?ACTION_Replay_Send_Button, SendUids), @@ -435,6 +444,10 @@ update_replay(_, #wx_state{system = #system{log = Log}, pid = Pid}) -> update_choice(?ACTION_Replay_Receive, ?ACTION_Replay_Receive_Button, ReceiveUids), update_choice(?ACTION_Replay_Start, ?ACTION_Replay_Start_Button, StartNodes), update_choice(?ACTION_Replay_Spawn, ?ACTION_Replay_Spawn_Button, SpawnPids), + ElsReg = updates(RegEls), + ElsDel = updates(DelEls), + update_choice(?ACTION_Replay_Register, ?ACTION_Replay_Register_Button, ElsReg), + update_choice(?ACTION_Replay_Delete, ?ACTION_Replay_Delete_Button, ElsDel), ok end. @@ -448,6 +461,9 @@ disable_replay() -> update_choice(?ACTION_Replay_Receive, ?ACTION_Replay_Receive_Button, []), update_choice(?ACTION_Replay_Start, ?ACTION_Replay_Start_Button, []), update_choice(?ACTION_Replay_Spawn, ?ACTION_Replay_Spawn_Button, []), + update_choice(?ACTION_Replay_Register, ?ACTION_Replay_Register_Button, []), + update_choice(?ACTION_Replay_Delete, ?ACTION_Replay_Delete_Button, []), + ok. %%%============================================================================= @@ -474,6 +490,10 @@ create_rollback(Parent) -> wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), create_choice(Win, Content, "Uid:", ?ACTION_Rollback_Send, {"Roll send", ?ACTION_Rollback_Send_Button}), wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), + %create_choice( + % Win, Content, "Atom-Uid:", ?ACTION_Rollback_Senda, {"Roll send with atom", ?ACTION_Rollback_Senda_Button} + %), + %wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), %create_choice(Win, Content, "Uid:", ?ACTION_Rollback_Deliver, {"Roll deliver", ?ACTION_Rollback_Deliver_Button}), %wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), create_choice(Win, Content, "Uid:", ?ACTION_Rollback_Receive, {"Roll receive", ?ACTION_Rollback_Receive_Button}), @@ -484,6 +504,15 @@ create_rollback(Parent) -> wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), create_text(Win, Content, "Name:", ?ACTION_Rollback_Variable, {"Roll variable", ?ACTION_Rollback_Variable_Button}), + wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), + create_choice( + Win, Content, "Map Element:", ?ACTION_Rollback_Register, {"Roll register", ?ACTION_Rollback_Register_Button} + ), + wxBoxSizer:addSpacer(Content, ?SPACER_LARGE), + create_choice( + Win, Content, "Map Element:", ?ACTION_Rollback_Delete, {"Roll delete", ?ACTION_Rollback_Delete_Button} + ), + Win. -spec update_rollback(OldState, NewState) -> ok when @@ -521,7 +550,10 @@ update_rollback(_, #wx_state{system = #system{pool = Pool}, pid = Pid}) -> 'send' := SendUids, 'receive' := ReceiveUids, 'start' := StartNodes, - 'spawn' := SpawnPids + 'spawn' := SpawnPids, + 'register' := RegEls, + %'sendA' := AtomsUids, + 'del' := DelEls } = lists:foldl( fun(P, Map0) -> maps:fold( @@ -547,6 +579,12 @@ update_rollback(_, #wx_state{system = #system{pool = Pool}, pid = Pid}) -> update_choice(?ACTION_Rollback_Start, ?ACTION_Rollback_Start_Button, StartNodes), update_choice(?ACTION_Rollback_Spawn, ?ACTION_Rollback_Spawn_Button, SpawnPids), + %update_choice(?ACTION_Rollback_Senda, ?ACTION_Rollback_Senda_Button, AtomsUids), + ElsReg = updates(RegEls), + ElsDel = updates(DelEls), + update_choice(?ACTION_Rollback_Register, ?ACTION_Rollback_Receive_Button, ElsReg), + update_choice(?ACTION_Rollback_Delete, ?ACTION_Rollback_Delete_Button, ElsDel), + ok end. @@ -559,6 +597,11 @@ disable_rollback() -> update_choice(?ACTION_Rollback_Receive, ?ACTION_Rollback_Receive_Button, []), update_choice(?ACTION_Rollback_Start, ?ACTION_Rollback_Start_Button, []), update_choice(?ACTION_Rollback_Spawn, ?ACTION_Rollback_Spawn_Button, []), + + %update_choice(?ACTION_Rollback_Senda, ?ACTION_Rollback_Senda_Button, []), + update_choice(?ACTION_Rollback_Register, ?ACTION_Rollback_Register_Button, []), + update_choice(?ACTION_Rollback_Delete, ?ACTION_Rollback_Delete_Button, []), + ok. %%%============================================================================= @@ -677,9 +720,14 @@ populate_choice(Choice, Items) -> wxChoice:clear(Choice), lists:foreach( fun + %ONLY FOR SEND WITH ATOM + ({{A, _, _}, Item}) -> wxChoice:append(Choice, io_lib:format("~p", [{A, Item}]), {A, Item}); ({Item, ClientData}) -> wxChoice:append(Choice, Item, ClientData); (Item) -> wxChoice:append(Choice, io_lib:format("~p", [Item]), Item) end, Items ), wxChoice:thaw(Choice). + +updates([])->[]; +updates([{A,B,C,_} | L]) -> [{A,B,C} | updates(L)]. diff --git a/src/cauder_wx_areas.erl b/src/cauder_wx_areas.erl index f7cd183..c2f1acf 100644 --- a/src/cauder_wx_areas.erl +++ b/src/cauder_wx_areas.erl @@ -30,6 +30,7 @@ create(Frame) -> ActionsPanel = cauder_wx_actions:create(Win), ProcessPanel = cauder_wx_process:create(Win), SystemPanel = cauder_wx_system:create(Win), + MapPanel = cauder_wx_map:create(Win), % ----- Left ----- % @@ -40,6 +41,9 @@ create(Frame) -> wxSizer:addSpacer(Left, ?SPACER_MEDIUM), wxSizer:add(Left, ProcessPanel, [{proportion, 1}, {flag, ?wxEXPAND}]), + wxSizer:addSpacer(Left, ?SPACER_MEDIUM), + wxSizer:add(Left, MapPanel, [{proportion, 1}, {flag, ?wxEXPAND}]), + % ----- wxSizer:addSpacer(Content, ?SPACER_MEDIUM), diff --git a/src/cauder_wx_map.erl b/src/cauder_wx_map.erl new file mode 100644 index 0000000..4ccb6c1 --- /dev/null +++ b/src/cauder_wx_map.erl @@ -0,0 +1,131 @@ +-module(cauder_wx_map). + +%% API +-export([create/1, update/2]). + +-include("cauder_system.hrl"). +-include("cauder_process.hrl"). +-include("cauder.hrl"). +-include("cauder_wx.hrl"). +-include_lib("wx/include/wx.hrl"). + +%%%============================================================================= +%%% API +%%%============================================================================= + +%%------------------------------------------------------------------------------ +%% @doc Creates the map info panel and populates it. + +-spec create(Parent) -> Window when + Parent :: wxWindow:wxWindow(), + Window :: wxWindow:wxWindow(). + +create(Parent) -> + Win = wxPanel:new(Parent, [{winid, ?SYSTEM_Map}]), + + Sizer = wxStaticBoxSizer:new(?wxHORIZONTAL, Win, [{label, "Map Info"}]), + wxWindow:setSizer(Win, Sizer), + + Expand = [{proportion, 1}, {flag, ?wxEXPAND}], + + LeftPanel = wxPanel:new(Win), + wxBoxSizer:add(Sizer, LeftPanel, Expand), + + LeftSizer = wxBoxSizer:new(?wxHORIZONTAL), + wxPanel:setSizer(LeftPanel, LeftSizer), + + wxBoxSizer:add(LeftSizer, create_map(LeftPanel), Expand), + + Win. + +%%------------------------------------------------------------------------------ +%% @doc Updates the map info panel according to the given new state, +%% by comparing it with the given old state. + +-spec update(OldState, NewState) -> ok when + OldState :: cauder_wx:state(), + NewState :: cauder_wx:state(). + +update(OldState, NewState) -> + update_map(OldState, NewState). + +%%%============================================================================= +%%% Internal functions +%%%============================================================================= + +-spec create_map(Parent) -> Window when + Parent :: wxWindow:wxWindow(), + Window :: wxWindow:wxWindow(). + +create_map(Parent) -> + Win = wxPanel:new(Parent), + + Sizer = wxStaticBoxSizer:new(?wxHORIZONTAL, Win, [{label, "Node Map"}]), + wxPanel:setSizer(Win, Sizer), + + BindingsControl = wxListCtrl:new(Win, [ + {winid, ?PROCESS_Map}, + {style, ?wxLC_REPORT bor ?wxLC_SINGLE_SEL} + ]), + wxBoxSizer:add(Sizer, BindingsControl, [{proportion, 1}, {flag, ?wxEXPAND}]), + + Item = wxListItem:new(), + + wxListItem:setText(Item, "Atom"), + wxListItem:setAlign(Item, ?wxLIST_FORMAT_LEFT), + wxListCtrl:insertColumn(BindingsControl, 0, Item), + + wxListItem:setText(Item, "PID"), + wxListCtrl:insertColumn(BindingsControl, 1, Item), + + wxListItem:setText(Item, "Tuple ID"), + wxListCtrl:insertColumn(BindingsControl, 2, Item), + + wxListItem:destroy(Item), + + wxListCtrl:setColumnWidth(BindingsControl, 0, 100), + wxListCtrl:setColumnWidth(BindingsControl, 1, 150), + wxListCtrl:setColumnWidth(BindingsControl, 2, 150), + + wxListCtrl:connect(BindingsControl, command_list_item_activated), + + Win. + +% consider the map contains ghost + +-spec update_map(OldState, NewState) -> ok when + OldState :: cauder_wx:state(), + NewState :: cauder_wx:state(). + +update_map(_, #wx_state{system = undefined}) -> + wxListCtrl:deleteAllItems(cauder_wx:find(?PROCESS_Map, wxListCtrl)), + ok; +update_map(_, #wx_state{system = #system{maps = []}}) -> + wxListCtrl:deleteAllItems(cauder_wx:find(?PROCESS_Map, wxListCtrl)), + ok; +update_map(_, #wx_state{system = #system{pool = Pool, maps = Maps}, pid = Pid}) -> + Font = wxFont:new(9, ?wxTELETYPE, ?wxNORMAL, ?wxNORMAL), + MapArea = cauder_wx:find(?PROCESS_Map, wxListCtrl), + wxListCtrl:freeze(MapArea), + wxListCtrl:deleteAllItems(MapArea), + #process{node = Node} = cauder_pool:get(Pid, Pool), + Map = cauder_map:get_map(Maps, Node), + lists:foldl( + fun(Entry, Row) -> + {A, P, K, Life} = Entry, + case Life =:= top of + true -> + wxListCtrl:insertItem(MapArea, Row, ""), + wxListCtrl:setItemFont(MapArea, Row, Font), + wxListCtrl:setItem(MapArea, Row, 0, cauder_pp:to_string(A)), + wxListCtrl:setItem(MapArea, Row, 1, cauder_pp:to_string(P)), + wxListCtrl:setItem(MapArea, Row, 2, cauder_pp:to_string(K)), + Row + 1; + false -> + Row + end + end, + 0, + Map + ), + wxListCtrl:thaw(MapArea). diff --git a/src/cauder_wx_statusbar.erl b/src/cauder_wx_statusbar.erl index e5a11be..5f3b660 100644 --- a/src/cauder_wx_statusbar.erl +++ b/src/cauder_wx_statusbar.erl @@ -15,6 +15,8 @@ -export([replay_spawn_start/1, replay_spawn_finish/2, replay_spawn_fail/0]). -export([replay_send_start/1, replay_send_finish/2, replay_send_fail/0]). -export([replay_receive_start/1, replay_receive_finish/2, replay_receive_fail/0]). +-export([replay_register_start/1, replay_register_finish/2, replay_register_fail/0]). +-export([replay_delete_start/1, replay_delete_finish/2, replay_delete_fail/0]). -export([replay_full_log_start/0, replay_full_log_finish/1]). % Rollback -export([rollback_steps_start/0, rollback_steps_finish/2]). @@ -23,6 +25,9 @@ -export([rollback_send_start/1, rollback_send_finish/2, rollback_send_fail/0]). -export([rollback_receive_start/1, rollback_receive_finish/2, rollback_receive_fail/0]). -export([rollback_variable_start/1, rollback_variable_finish/2, rollback_variable_fail/0]). +-export([rollback_reg_start/1, rollback_reg_finish/2, rollback_reg_fail/0]). +-export([rollback_del_start/1, rollback_del_finish/2, rollback_del_fail/0]). +%-export([rollback_senda_start/1, rollback_senda_finish/2, rollback_senda_fail/0]). -elvis([{elvis_style, god_modules, disable}]). @@ -304,6 +309,46 @@ replay_receive_fail() -> set_text(?REPLAY_RECEIVE_FAIL). %%%============================================================================= +-spec replay_register_start(Key) -> ok when + Key :: cauder_map:key(). + +replay_register_start(Key) -> set_text(io_lib:format(?REPLAY_REGISTER_START, [Key])). + +-spec replay_register_finish(Key, Time) -> ok when + Key :: cauder_map:key(), + Time :: non_neg_integer(). + +replay_register_finish(Key, Time) -> + TimeStr = time_to_string(Time), + Status = io_lib:format(?REPLAY_REGISTER_FINISH, [Key, TimeStr]), + set_text(Status). + +-spec replay_register_fail() -> ok. + +replay_register_fail() -> set_text(?REPLAY_REGISTER_FAIL). + +%%%============================================================================= + +-spec replay_delete_start(Key) -> ok when + Key :: cauder_map:key(). + +replay_delete_start(Key) -> set_text(io_lib:format(?REPLAY_DELETE_START, [Key])). + +-spec replay_delete_finish(Key, Time) -> ok when + Key :: cauder_map:key(), + Time :: non_neg_integer(). + +replay_delete_finish(Key, Time) -> + TimeStr = time_to_string(Time), + Status = io_lib:format(?REPLAY_DELETE_FINISH, [Key, TimeStr]), + set_text(Status). + +-spec replay_delete_fail() -> ok. + +replay_delete_fail() -> set_text(?REPLAY_DELETE_FAIL). + +%%%============================================================================= + -spec replay_full_log_start() -> ok. replay_full_log_start() -> set_text(?REPLAY_FULL_LOG_START). @@ -394,6 +439,65 @@ rollback_send_fail() -> set_text(?ROLLBACK_SEND_FAIL). %%%============================================================================= +%-spec rollback_senda_start(Uid) -> ok when +% Uid :: cauder_message:uid(). + +%rollback_senda_start(Uid) -> set_text(io_lib:format(?ROLLBACK_SENDA_START, [Uid])). + +%-spec rollback_senda_finish(Uid, Time) -> ok when +% Uid :: cauder_message:uid(), +% Time :: non_neg_integer(). + +%rollback_senda_finish(Uid, Time) -> +% TimeStr = time_to_string(Time), +% Status = io_lib:format(?ROLLBACK_SENDA_FINISH, [Uid, TimeStr]), +% set_text(Status). + +%-spec rollback_senda_fail() -> ok. + +%rollback_senda_fail() -> set_text(?ROLLBACK_SENDA_FAIL). + +%%%============================================================================= + +-spec rollback_reg_start(El) -> ok when + El :: cauder_map:map_element(). + +rollback_reg_start(El) -> set_text(io_lib:format(?ROLLBACK_REG_START, [El])). + +-spec rollback_reg_finish(El, Time) -> ok when + El :: cauder_map:map_element(), + Time :: non_neg_integer(). + +rollback_reg_finish(El, Time) -> + TimeStr = time_to_string(Time), + Status = io_lib:format(?ROLLBACK_REG_FINISH, [El, TimeStr]), + set_text(Status). + +-spec rollback_reg_fail() -> ok. + +rollback_reg_fail() -> set_text(?ROLLBACK_REG_FAIL). + +%%%============================================================================= + +-spec rollback_del_start(El) -> ok when + El :: cauder_map:map_element(). + +rollback_del_start(El) -> set_text(io_lib:format(?ROLLBACK_DEL_START, [El])). + +-spec rollback_del_finish(El, Time) -> ok when + El :: cauder_map:map_element(), + Time :: non_neg_integer(). + +rollback_del_finish(El, Time) -> + TimeStr = time_to_string(Time), + Status = io_lib:format(?ROLLBACK_DEL_FINISH, [El, TimeStr]), + set_text(Status). + +-spec rollback_del_fail() -> ok. + +rollback_del_fail() -> set_text(?ROLLBACK_DEL_FAIL). + +%%%============================================================================= -spec rollback_receive_start(Uid) -> ok when Uid :: cauder_message:uid(). diff --git a/src/cauder_wx_statusbar.hrl b/src/cauder_wx_statusbar.hrl index 7de5181..0e11d50 100644 --- a/src/cauder_wx_statusbar.hrl +++ b/src/cauder_wx_statusbar.hrl @@ -36,6 +36,14 @@ -define(REPLAY_RECEIVE_FINISH, "Replayed the reception of the message with UID ~p in ~s"). -define(REPLAY_RECEIVE_FAIL, "Could not replay the reception of that message"). +-define(REPLAY_REGISTER_START, "Replaying the register of the tuple with KEY ~p..."). +-define(REPLAY_REGISTER_FINISH, "Replayed the register of the tuple with KEY ~p in ~s"). +-define(REPLAY_REGISTER_FAIL, "Could not replay the register"). + +-define(REPLAY_DELETE_START, "Replaying the delete of the tuple with KEY ~p..."). +-define(REPLAY_DELETE_FINISH, "Replayed the delete of the tuple with KEY ~p in ~s"). +-define(REPLAY_DELETE_FAIL, "Could not replay the delete"). + -define(REPLAY_FULL_LOG_START, "Replaying the full log..."). -define(REPLAY_FULL_LOG_FINISH, "Replayed the full log in ~s"). @@ -54,10 +62,22 @@ -define(ROLLBACK_SEND_FINISH, "Rolled back the sending of the message with UID ~p in ~s"). -define(ROLLBACK_SEND_FAIL, "Could not rollback the sending of that message"). +%-define(ROLLBACK_SENDA_START, "Rolling back the sending of the message with UID ~p..."). +%-define(ROLLBACK_SENDA_FINISH, "Rolled back the sending of the message with UID ~p in ~s"). +%-define(ROLLBACK_SENDA_FAIL, "Could not rollback the sending of that message"). + -define(ROLLBACK_RECEIVE_START, "Rolling back the reception of the message with UID ~p..."). -define(ROLLBACK_RECEIVE_FINISH, "Rolled back the reception of the message with UID ~p in ~s"). -define(ROLLBACK_RECEIVE_FAIL, "Could not rollback the reception of that message"). +-define(ROLLBACK_REG_START, "Rolling back the register of the element ~p..."). +-define(ROLLBACK_REG_FINISH, "Rolled back the register of the element ~p in ~s"). +-define(ROLLBACK_REG_FAIL, "Could not rollback the register"). + +-define(ROLLBACK_DEL_START, "Rolling back the delete of the element ~p..."). +-define(ROLLBACK_DEL_FINISH, "Rolled back the delete of the element ~p in ~s"). +-define(ROLLBACK_DEL_FAIL, "Could not rollback the delete"). + -define(ROLLBACK_VARIABLE_START, "Rolling back the binding of the variable with name ~p..."). -define(ROLLBACK_VARIABLE_FINISH, "Rolled back the binding of the variable with name ~p in ~s"). -define(ROLLBACK_VARIABLE_FAIL, "Could not rollback the binding of that variable").