Erlang processes are trivially linearizible

ex.erl

-module(ex).

-compile(export_all).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").

%% reg_ is a register process maintaining a single register
reg_proc() ->
    case whereis(reg) of
        Pid when is_pid(Pid) ->
          reg_reset();
        undefined ->
          S = self(),
          spawn(fun() -> reg_init(S) end),
          receive
            ok -> ok
          end
    end.
    
reg_init(Initiator) ->
    register(reg, self()),
    Initiator ! ok,
    reg_loop(0).
    
reg_loop(Value) ->
    receive
        {reset, From} ->
        	From ! ok,
        	reg_loop(0);
        {get, From} ->
        	From ! Value,
        	reg_loop(Value);
        {put, From, NewVal} ->
        	From ! ok,
        	reg_loop(NewVal)
    end.
    
reg_reset() ->
	reg ! {reset, self()},
	receive
	  ok -> ok
	end.
	
reg_get() ->
	reg ! {get, self()},
	receive
	  V -> V
	end.
	
reg_put(Val) ->
	reg ! {put, self(), Val},
	receive
	   ok -> ok
	end.

%% Quickcheck model
-record(state, { value = 0 }).

initial_state() ->
	#state{}.
	
get() ->
	reg_get().
	
get_args(_S) -> [].

get_post(#state { value = V }, _, R) ->
	eq(R, V).
	
put(V) ->
	reg_put(V).
	
put_args(_S) ->
	[int()].

put_next(#state{} = S, _V, [Value]) ->
	S#state { value = Value }.
	
put_post(_S, _, R) ->
	eq(R, ok).

prop_model_seq() ->
	?FORALL(Cmds, commands(?MODULE),
	  begin
	    reg_proc(),
	    {H, S, R} = run_commands(?MODULE, Cmds),
	    aggregate(command_names(Cmds),
	      pretty_commands(?MODULE, cmds, {H, S, R}, R == ok))
	  end).

prop_model_par() ->
	?LET(Shrinking, parameter(shrinking, false),
	  ?FORALL(Cmds, parallel_commands(?MODULE),
	    ?ALWAYS(if not Shrinking -> 1; Shrinking -> 20 end,
	      begin
	        reg_proc(),
	        {H, S, R} = run_parallel_commands(?MODULE, Cmds),
	        aggregate(command_names(Cmds),
	          pretty_commands(?MODULE, Cmds, {H, S, R}, R == ok))
	      end))).