Parallel typesig analysis

7 files changed, 538 insertions, 96 deletions

diff --git a/lib/dialyzer/src/Makefile b/lib/dialyzer/src/Makefile
index 04f3b844c4..2f1eaf5754 100644
--- a/lib/dialyzer/src/Makefile
+++ b/lib/dialyzer/src/Makefile
@@ -64,6 +64,8 @@ MODULES =  \
 	dialyzer_races \
 	dialyzer_succ_typings \
 	dialyzer_typesig \
+	dialyzer_typesig_coordinator \
+	dialyzer_typesig_worker \
 	dialyzer_utils
 
 HRL_FILES= dialyzer.hrl dialyzer_gui_wx.hrl
diff --git a/lib/dialyzer/src/dialyzer.hrl b/lib/dialyzer/src/dialyzer.hrl
index 5e089d1773..44b1ebeabd 100644
--- a/lib/dialyzer/src/dialyzer.hrl
+++ b/lib/dialyzer/src/dialyzer.hrl
@@ -110,6 +110,7 @@
 -type label()	      :: non_neg_integer().
 -type rep_mode()      :: 'quiet' | 'normal' | 'verbose'.
 -type start_from()    :: 'byte_code' | 'src_code'.
+-type mfa_or_funlbl() :: label() | mfa().
 
 %%--------------------------------------------------------------------
 %% Record declarations used by various files
diff --git a/lib/dialyzer/src/dialyzer_analysis_callgraph.erl b/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
index 7221d81a72..7060028d17 100644
--- a/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
+++ b/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
@@ -179,22 +179,21 @@ analyze_callgraph(Callgraph, State) ->
   Parent = State#analysis_state.parent,
   DocPlt = State#analysis_state.doc_plt,
   Plt = dialyzer_plt:insert_callbacks(State#analysis_state.plt, Codeserver),
-  Callgraph1 = dialyzer_callgraph:finalize(Callgraph),
   {NewPlt, NewDocPlt} =
     case State#analysis_state.analysis_type of
       plt_build ->
-	{dialyzer_succ_typings:analyze_callgraph(Callgraph1, Plt,
+	{dialyzer_succ_typings:analyze_callgraph(Callgraph, Plt,
 						 Codeserver, Parent),
 	 DocPlt};
       succ_typings ->
 	NoWarn = State#analysis_state.no_warn_unused,
 	{Warnings, NewPlt0, NewDocPlt0} =
-	  dialyzer_succ_typings:get_warnings(Callgraph1, Plt, DocPlt,
+	  dialyzer_succ_typings:get_warnings(Callgraph, Plt, DocPlt,
 					     Codeserver, NoWarn, Parent),
 	send_warnings(State#analysis_state.parent, Warnings),
 	{NewPlt0, NewDocPlt0}
     end,
-  dialyzer_callgraph:delete(Callgraph1),
+  dialyzer_callgraph:delete(Callgraph),
   State#analysis_state{plt = NewPlt, doc_plt = NewDocPlt}.
 
 %%--------------------------------------------------------------------
diff --git a/lib/dialyzer/src/dialyzer_callgraph.erl b/lib/dialyzer/src/dialyzer_callgraph.erl
index 2a01b0f753..1cbb83a44a 100644
--- a/lib/dialyzer/src/dialyzer_callgraph.erl
+++ b/lib/dialyzer/src/dialyzer_callgraph.erl
@@ -43,12 +43,14 @@
 	 %% module_postorder/1,
 	 module_postorder_from_funs/2,
 	 new/0,
+	 mini_callgraph/1,
+	 get_depends_on/2,
+	 get_required_by/2,
 	 in_neighbours/2,
 	 renew_race_info/4,
 	 reset_from_funs/2,
 	 scan_core_tree/2,
 	 strip_module_deps/2,
-	 take_scc/1,
 	 remove_external/1,
 	 to_dot/2,
 	 to_ps/3]).
@@ -65,7 +67,6 @@
 
 %%----------------------------------------------------------------------
 
--type mfa_or_funlbl() :: label() | mfa().
 -type scc()	      :: [mfa_or_funlbl()].
 -type mfa_calls()     :: [{mfa_or_funlbl(), mfa_or_funlbl()}].
 
@@ -78,9 +79,6 @@
 %% digraph	-  A digraph representing the callgraph. 
 %%		   Nodes are represented as MFAs or labels.
 %% esc		-  A set of all escaping functions as reported by dialyzer_dep.
-%% postorder	-  A list of strongly connected components of the callgraph
-%%		   sorted in a topological bottom-up order.
-%%		   This is produced by calling finalize/1.
 %% name_map	-  A mapping from label to MFA.
 %% rev_name_map	-  A reverse mapping of the name_map.
 %% rec_var_map	-  A dict mapping from letrec bound labels to function names.
@@ -91,13 +89,13 @@
 %%-----------------------------------------------------------------------------
 
 -record(callgraph, {digraph        = digraph:new() :: digraph(),
-                    esc	           = sets:new()    :: set(),
-                    name_map	   = dict:new()    :: dict(),
-                    rev_name_map   = dict:new()    :: dict(),
-                    postorder      = []	           :: [scc()],
-                    rec_var_map    = dict:new()    :: dict(),
-                    self_rec	   = sets:new()    :: set(),
-                    calls          = dict:new()    :: dict(),
+		    active_digraph                 :: digraph(),
+                    esc	           = sets:new()    :: set()  | ets:tid(),
+                    name_map	   = dict:new()    :: dict() | ets:tid(),
+                    rev_name_map   = dict:new()    :: dict() | ets:tid(),
+                    rec_var_map    = dict:new()    :: dict() | ets:tid(),
+                    self_rec	   = sets:new()    :: set()  | ets:tid(),
+                    calls          = dict:new()    :: dict() | ets:tid(),
                     race_code      = dict:new()    :: dict(),
                     public_tables  = []            :: [label()],
                     named_tables   = []            :: [string()],
@@ -115,6 +113,25 @@
 new() ->
   #callgraph{}.
 
+-spec mini_callgraph(callgraph()) -> callgraph().
+
+mini_callgraph(#callgraph{digraph        = Digraph,
+			  active_digraph = ActiveDigraph,
+			  esc	         = Esc,
+			  name_map       = NameMap,
+			  rev_name_map   = RevNameMap,
+			  rec_var_map    = RecVarMap,
+			  self_rec       = SelfRecs,
+			  calls          = Calls}) ->
+  #callgraph{digraph        = Digraph,
+	     active_digraph = ActiveDigraph,
+	     esc	         = Esc,
+	     name_map       = NameMap,
+	     rev_name_map   = RevNameMap,
+	     rec_var_map    = RecVarMap,
+	     self_rec       = SelfRecs,
+	     calls          = Calls}.
+
 -spec delete(callgraph()) -> 'true'.
 
 delete(#callgraph{digraph = Digraph}) ->
@@ -129,32 +146,32 @@ all_nodes(#callgraph{digraph = DG}) ->
 
 lookup_rec_var(Label, #callgraph{rec_var_map = RecVarMap}) 
   when is_integer(Label) ->
-  dict:find(Label, RecVarMap).
+  ets_lookup_dict(Label, RecVarMap).
 
 -spec lookup_call_site(label(), callgraph()) -> 'error' | {'ok', [_]}. % XXX: refine
 
 lookup_call_site(Label, #callgraph{calls = Calls})
   when is_integer(Label) ->
-  dict:find(Label, Calls).
+  ets_lookup_dict(Label, Calls).
 
 -spec lookup_name(label(), callgraph()) -> 'error' | {'ok', mfa()}.
 
 lookup_name(Label, #callgraph{name_map = NameMap})
   when is_integer(Label) ->
-  dict:find(Label, NameMap).
+  ets_lookup_dict(Label, NameMap).
 
 -spec lookup_label(mfa_or_funlbl(), callgraph()) -> 'error' | {'ok', integer()}.
 
 lookup_label({_,_,_} = MFA, #callgraph{rev_name_map = RevNameMap}) ->
-  dict:find(MFA, RevNameMap);
+  ets_lookup_dict(MFA, RevNameMap);
 lookup_label(Label, #callgraph{}) when is_integer(Label) ->
   {ok, Label}.
 
 -spec in_neighbours(mfa_or_funlbl(), callgraph()) -> 'none' | [mfa_or_funlbl(),...].
 
-in_neighbours(Label, #callgraph{digraph = Digraph, name_map = NameMap})
+in_neighbours(Label, #callgraph{digraph = Digraph} = CG)
   when is_integer(Label) ->
-  Name = case dict:find(Label, NameMap) of
+  Name = case lookup_name(Label, CG) of
 	   {ok, Val} -> Val;
 	   error -> Label
 	 end,
@@ -165,12 +182,12 @@ in_neighbours({_, _, _} = MFA, #callgraph{digraph = Digraph}) ->
 -spec is_self_rec(mfa_or_funlbl(), callgraph()) -> boolean().
 
 is_self_rec(MfaOrLabel, #callgraph{self_rec = SelfRecs}) ->
-  sets:is_element(MfaOrLabel, SelfRecs).
+  ets_lookup_set(MfaOrLabel, SelfRecs).
 
 -spec is_escaping(label(), callgraph()) -> boolean().
 
 is_escaping(Label, #callgraph{esc = Esc}) when is_integer(Label) ->
-  sets:is_element(Label, Esc).  
+  ets_lookup_set(Label, Esc).
 
 -type callgraph_edge() :: {mfa_or_funlbl(),mfa_or_funlbl()}.
 -spec add_edges([callgraph_edge()], callgraph()) -> callgraph().
@@ -186,13 +203,6 @@ add_edges(Edges, MFAs, #callgraph{digraph = DG} = CG) ->
   DG = digraph_confirm_vertices(MFAs, DG),
   add_edges(Edges, CG).
 
--spec take_scc(callgraph()) -> 'none' | {'ok', scc(), callgraph()}.
-
-take_scc(#callgraph{postorder = [SCC|SCCs]} = CG) ->
-  {ok, SCC, CG#callgraph{postorder = SCCs}};
-take_scc(#callgraph{postorder = []}) ->
-  none.
-
 -spec remove_external(callgraph()) -> {callgraph(), [tuple()]}.
 
 remove_external(#callgraph{digraph = DG} = CG) ->
@@ -229,6 +239,16 @@ renew_race_info(CG, RaceCode, PublicTables, NamedTables) ->
                public_tables = PublicTables,
                named_tables = NamedTables}.
 
+-spec get_depends_on(scc(), callgraph()) -> [scc()].
+
+get_depends_on(SCC, #callgraph{active_digraph = DG}) ->
+  digraph:out_neighbours(DG, SCC).
+
+-spec get_required_by(scc(), callgraph()) -> [scc()].
+
+get_required_by(SCC, #callgraph{active_digraph = DG}) ->
+  digraph:in_neighbours(DG, SCC).
+
 %%----------------------------------------------------------------------
 %% Handling of modules & SCCs
 %%----------------------------------------------------------------------
@@ -282,18 +302,44 @@ create_module_digraph([{_, _}|Left], MDG) ->
 create_module_digraph([], MDG) ->
   MDG.
 
--spec finalize(callgraph()) -> callgraph().
-
-finalize(#callgraph{digraph = DG} = CG) ->
-  CG#callgraph{postorder = digraph_finalize(DG)}.
-
--spec reset_from_funs([mfa_or_funlbl()], callgraph()) -> callgraph().
-
-reset_from_funs(Funs, #callgraph{digraph = DG} = CG) ->
+-spec finalize(callgraph()) -> {[scc()], callgraph()}.
+
+finalize(#callgraph{digraph      = DG,
+		    esc          = Esc,
+		    name_map     = NameMap,
+		    rev_name_map = RevNameMap,
+		    rec_var_map  = RecVarMap,
+		    self_rec     = SelfRec,
+		    calls        = Calls
+		   } = CG) ->
+  [ETSEsc, ETSNameMap, ETSRevNameMap, ETSRecVarMap, ETSSelfRec, ETSCalls] =
+    [ets:new(N,[public]) ||
+      N <- [callgraph_esc, callgraph_name_map, callgraph_rev_name_map,
+	    callgraph_rec_var_map, callgraph_self_rec, callgraph_calls]],
+  [true,true] = [ets:insert(ETS, [{E} || E <- sets:to_list(Data)]) ||
+		  {ETS, Data} <- [{ETSEsc, Esc}, {ETSSelfRec, SelfRec}]],
+  [true, true, true, true] =
+    [ets:insert(ETS, dict:to_list(Data)) ||
+      {ETS, Data} <- [{ETSNameMap, NameMap}, {ETSRevNameMap, RevNameMap},
+		      {ETSRecVarMap, RecVarMap}, {ETSCalls, Calls}]],
+  {ActiveDG, Postorder} = digraph_finalize(DG),
+  {Postorder, CG#callgraph{active_digraph = ActiveDG,
+			   esc            = ETSEsc,
+			   name_map       = ETSNameMap,
+			   rev_name_map   = ETSRevNameMap,
+			   rec_var_map    = ETSRecVarMap,
+			   self_rec       = ETSSelfRec,
+			   calls          = ETSCalls}}.
+
+-spec reset_from_funs([mfa_or_funlbl()], callgraph()) -> {[scc()], callgraph()}.
+
+reset_from_funs(Funs, #callgraph{digraph = DG,
+				 active_digraph = OldActiveDG} = CG) ->
+  digraph_delete(OldActiveDG),
   SubGraph = digraph_reaching_subgraph(Funs, DG),
-  Postorder = digraph_finalize(SubGraph),
+  {NewActiveDG, Postorder} = digraph_finalize(SubGraph),
   digraph_delete(SubGraph),
-  CG#callgraph{postorder = Postorder}.
+  {Postorder, CG#callgraph{active_digraph = NewActiveDG}}.
 
 -spec module_postorder_from_funs([mfa_or_funlbl()], callgraph()) -> [module()].
 
@@ -302,7 +348,20 @@ module_postorder_from_funs(Funs, #callgraph{digraph = DG} = CG) ->
   PO = module_postorder(CG#callgraph{digraph = SubGraph}),
   digraph_delete(SubGraph),
   PO.
-  
+
+ets_lookup_dict(Key, Table) ->
+  try ets:lookup_element(Table, Key, 2) of
+      Val -> {ok, Val}
+  catch
+    _:_ -> error
+  end.
+
+ets_lookup_set(Key, Table) ->
+  case ets:lookup(Table, Key) of
+      [] -> false;
+      _ -> true
+  end.
+
 %%----------------------------------------------------------------------
 %% Core code
 %%----------------------------------------------------------------------
@@ -516,13 +575,12 @@ digraph_in_neighbours(V, DG) ->
   end.
 
 digraph_postorder(Digraph) ->
-  digraph_utils:postorder(Digraph).
+  digraph_utils:topsort(Digraph).
 
 digraph_finalize(DG) ->
   DG1 = digraph_utils:condensation(DG),
   Postorder = digraph_postorder(DG1),
-  digraph:delete(DG1),
-  Postorder.
+  {DG1, Postorder}.
 
 digraph_reaching_subgraph(Funs, DG) ->  
   Vertices = digraph_utils:reaching(Funs, DG),
diff --git a/lib/dialyzer/src/dialyzer_succ_typings.erl b/lib/dialyzer/src/dialyzer_succ_typings.erl
index 9e6702b484..af935f54f7 100644
--- a/lib/dialyzer/src/dialyzer_succ_typings.erl
+++ b/lib/dialyzer/src/dialyzer_succ_typings.erl
@@ -29,7 +29,12 @@
 
 -export([analyze_callgraph/3, 
 	 analyze_callgraph/4,
-	 get_warnings/6]).
+	 get_warnings/6,
+	 find_succ_types_for_scc/1,
+	 collect_scc_data/2,
+	 find_required_by/2,
+	 find_depends_on/2
+	]).
 
 %% These are only intended as debug functions.
 -export([doit/1,
@@ -75,15 +80,20 @@ analyze_callgraph(Callgraph, Plt, Codeserver) ->
          dialyzer_plt:plt().
 
 analyze_callgraph(Callgraph, Plt, Codeserver, Parent) ->
-  State = #st{callgraph = Callgraph, plt = dialyzer_plt:get_mini_plt(Plt),
-	      codeserver = Codeserver, parent = Parent},
-  NewState = get_refined_success_typings(State),
+  NewState =
+    init_state_and_get_success_typings(Callgraph, Plt, Codeserver, Parent),
   dialyzer_plt:restore_full_plt(NewState#st.plt, Plt).
 
 %%--------------------------------------------------------------------
 
-get_refined_success_typings(State) ->
-  case find_succ_typings(State) of
+init_state_and_get_success_typings(Callgraph, Plt, Codeserver, Parent) ->
+  {SCCs, Callgraph1} = dialyzer_callgraph:finalize(Callgraph),
+  State = #st{callgraph = Callgraph1, plt = dialyzer_plt:get_mini_plt(Plt),
+	      codeserver = Codeserver, parent = Parent},
+  get_refined_success_typings(SCCs, State).
+
+get_refined_success_typings(SCCs, State) ->
+  case find_succ_typings(SCCs, State) of
     {fixpoint, State1} -> State1;
     {not_fixpoint, NotFixpoint1, State1} ->
       Callgraph = State1#st.callgraph,
@@ -97,9 +107,10 @@ get_refined_success_typings(State) ->
 	  Callgraph1 = State2#st.callgraph,
 	  %% Need to reset the callgraph.
 	  NotFixpoint4 = [lookup_name(F, Callgraph1) || F <- NotFixpoint3],
-	  Callgraph2 = dialyzer_callgraph:reset_from_funs(NotFixpoint4, 
-							  Callgraph1),
-	  get_refined_success_typings(State2#st{callgraph = Callgraph2})
+	  {NewSCCs, Callgraph2} =
+	    dialyzer_callgraph:reset_from_funs(NotFixpoint4, Callgraph1),
+	  NewState = State2#st{callgraph = Callgraph2},
+	  get_refined_success_typings(NewSCCs, NewState)
       end
   end.
 
@@ -110,9 +121,11 @@ get_refined_success_typings(State) ->
 	 {[dial_warning()], dialyzer_plt:plt(), doc_plt()}.
 
 get_warnings(Callgraph, Plt, DocPlt, Codeserver, NoWarnUnused, Parent) ->
-  InitState = #st{callgraph = Callgraph, codeserver = Codeserver,
-		  no_warn_unused = NoWarnUnused, parent = Parent, plt = Plt},
-  NewState = get_refined_success_typings(InitState),
+  InitState =
+    init_state_and_get_success_typings(Callgraph, Plt, Codeserver, Parent),
+  NewState =
+    InitState#st{no_warn_unused = NoWarnUnused,
+		 plt = dialyzer_plt:restore_full_plt(InitState#st.plt, Plt)},
   Mods = dialyzer_callgraph:modules(NewState#st.callgraph),
   CWarns = dialyzer_contracts:get_invalid_contract_warnings(Mods, Codeserver,
 							    NewState#st.plt),
@@ -213,8 +226,8 @@ refine_one_module(M, State) ->
       {State1, ordsets:new()};
     {false, NotFixpoint} ->
       ?debug("Not fixpoint\n", []),
-      NewState = insert_into_plt(dict:from_list(NotFixpoint), State),
-      NewState1 = st__renew_state_calls(NewCallgraph, NewState),
+      NewPlt = insert_into_plt(dict:from_list(NotFixpoint), Callgraph, PLT),
+      NewState1 = st__renew_state_calls(NewCallgraph, State#st{plt = NewPlt}),
       {NewState1, ordsets:from_list([FunLbl || {FunLbl,_Type} <- NotFixpoint])}
   end.
 
@@ -276,31 +289,44 @@ compare_types_1([], [], _Strict, NotFixpoint) ->
     false -> {false, NotFixpoint}
   end.
 
-find_succ_typings(State) ->
-  find_succ_typings(State, []).
-
-find_succ_typings(#st{callgraph = Callgraph, parent = Parent} = State,
-		  NotFixpoint) ->
-  case dialyzer_callgraph:take_scc(Callgraph) of
-    {ok, SCC, NewCallgraph} ->
-      Msg = io_lib:format("Typesig analysis for SCC: ~w\n", [format_scc(SCC)]),
-      ?debug("~s", [Msg]),
-      send_log(Parent, Msg),
-      {NewState, NewNotFixpoint1} =
-	analyze_scc(SCC, State#st{callgraph = NewCallgraph}),
-      NewNotFixpoint2 = ordsets:union(NewNotFixpoint1, NotFixpoint),
-      find_succ_typings(NewState, NewNotFixpoint2);
-    none ->
-      ?debug("==================== Typesig done ====================\n\n", []),
-      case NotFixpoint =:= [] of
-	true -> {fixpoint, State};
-	false -> {not_fixpoint, NotFixpoint, State}
-      end
+find_succ_typings(SCCs, #st{codeserver = Codeserver, callgraph = Callgraph,
+			    plt = Plt} = State) ->
+  Servers = {Codeserver, dialyzer_callgraph:mini_callgraph(Callgraph), Plt},
+  Coordinator = dialyzer_typesig_coordinator:start(Servers),
+  find_succ_typings(SCCs, State, Coordinator).
+
+find_succ_typings([SCC|Rest], #st{parent = Parent} = State, Coordinator) ->
+  Msg = io_lib:format("Typesig analysis for SCC: ~w\n", [format_scc(SCC)]),
+  ?debug("~s", [Msg]),
+  send_log(Parent, Msg),
+  dialyzer_typesig_coordinator:scc_spawn(SCC, Coordinator),
+  find_succ_typings(Rest, State, Coordinator);
+find_succ_typings([], State, Coordinator) ->
+  dialyzer_typesig_coordinator:all_spawned(Coordinator),
+  NotFixpoint = dialyzer_typesig_coordinator:receive_not_fixpoint(),
+  ?debug("==================== Typesig done ====================\n\n", []),
+  case NotFixpoint =:= [] of
+    true -> {fixpoint, State};
+    false -> {not_fixpoint, NotFixpoint, State}
   end.
 
-analyze_scc(SCC, #st{codeserver = Codeserver,
-		     callgraph = Callgraph,
-		     plt = Plt} = State) ->
+-type servers()  :: term().
+-type scc_data() :: term().
+-type scc()      :: [mfa_or_funlbl()].
+
+-spec find_depends_on(scc(), servers()) -> [scc()].
+
+find_depends_on(SCC, {_Codeserver, Callgraph, _Plt}) ->
+  dialyzer_callgraph:get_depends_on(SCC, Callgraph).
+
+-spec find_required_by(scc(), servers()) -> [scc()].
+
+find_required_by(SCC, {_Codeserver, Callgraph, _Plt}) ->
+  dialyzer_callgraph:get_required_by(SCC, Callgraph).
+
+-spec collect_scc_data(scc(), servers()) -> scc_data().
+
+collect_scc_data(SCC, {Codeserver, Callgraph, Plt}) ->
   SCC_Info = [{MFA, 
 	       dialyzer_codeserver:lookup_mfa_code(MFA, Codeserver),
 	       dialyzer_codeserver:lookup_mod_records(M, Codeserver)}
@@ -310,16 +336,15 @@ analyze_scc(SCC, #st{codeserver = Codeserver,
   Contracts2 = [{MFA, Contract} || {MFA, {ok, Contract}} <- Contracts1],
   Contracts3 = orddict:from_list(Contracts2),
   NextLabel = dialyzer_codeserver:get_next_core_label(Codeserver),
-  {SuccTypes, PltContracts, NotFixpoint} = 
-    find_succ_types_for_scc(SCC_Info, Contracts3, NextLabel, Callgraph, Plt),
-  State1 = insert_into_plt(SuccTypes, State),
-  ContrPlt = dialyzer_plt:insert_contract_list(State1#st.plt, PltContracts),
-  {State1#st{plt = ContrPlt}, NotFixpoint}.
-
-find_succ_types_for_scc(SCC_Info, Contracts, NextLabel, Callgraph, Plt) ->
-  %% Assume that the PLT contains the current propagated types
   AllFuns = collect_fun_info([Fun || {_MFA, {_Var, Fun}, _Rec} <- SCC_Info]),
   PropTypes = get_fun_types_from_plt(AllFuns, Callgraph, Plt),
+  {SCC_Info, Contracts3, NextLabel, AllFuns, PropTypes, Callgraph, Plt}.
+
+-spec find_succ_types_for_scc(scc_data()) -> [mfa_or_funlbl()].
+
+find_succ_types_for_scc({SCC_Info, Contracts, NextLabel, AllFuns,
+			 PropTypes, Callgraph, Plt}) ->
+  %% Assume that the PLT contains the current propagated types
   FunTypes = dialyzer_typesig:analyze_scc(SCC_Info, NextLabel, 
 					  Callgraph, Plt, PropTypes),
   AllFunSet = sets:from_list([X || {X, _} <- AllFuns]),
@@ -337,14 +362,14 @@ find_succ_types_for_scc(SCC_Info, Contracts, NextLabel, Callgraph, Plt) ->
 		    {value, _} -> true
 		  end
 	      end, PltContracts),
+  insert_into_plt(FilteredFunTypes, Callgraph, Plt),
+  dialyzer_plt:insert_contract_list(Plt, PltContracts),
   case (ContractFixpoint andalso 
 	reached_fixpoint_strict(PropTypes, FilteredFunTypes)) of
-    true ->
-      {FilteredFunTypes, PltContracts, []};
+    true -> [];
     false ->
       ?debug("Not fixpoint for: ~w\n", [AllFuns]),
-      {FilteredFunTypes, PltContracts,
-       ordsets:from_list([Fun || {Fun, _Arity} <- AllFuns])}
+      ordsets:from_list([Fun || {Fun, _Arity} <- AllFuns])
   end.
 
 get_fun_types_from_plt(FunList, Callgraph, Plt) ->
@@ -384,10 +409,10 @@ insert_into_doc_plt(FunTypes, Callgraph, DocPlt) ->
   SuccTypes = format_succ_types(FunTypes, Callgraph),
   dialyzer_plt:insert_list(DocPlt, SuccTypes).
 
-insert_into_plt(SuccTypes0, #st{callgraph = Callgraph, plt = Plt} = State) ->
+insert_into_plt(SuccTypes0, Callgraph, Plt) ->
   SuccTypes = format_succ_types(SuccTypes0, Callgraph),
   debug_pp_succ_typings(SuccTypes),
-  State#st{plt = dialyzer_plt:insert_list(Plt, SuccTypes)}.
+  dialyzer_plt:insert_list(Plt, SuccTypes).
 
 format_succ_types(SuccTypes, Callgraph) ->
   format_succ_types(dict:to_list(SuccTypes), Callgraph, []).
diff --git a/lib/dialyzer/src/dialyzer_typesig_coordinator.erl b/lib/dialyzer/src/dialyzer_typesig_coordinator.erl
new file mode 100644
index 0000000000..9475bc6895
--- /dev/null
+++ b/lib/dialyzer/src/dialyzer_typesig_coordinator.erl
@@ -0,0 +1,215 @@
+%% -*- erlang-indent-level: 2 -*-
+%%-----------------------------------------------------------------------
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2006-2011. All Rights Reserved.
+%%
+%% The contents of this file are subject to the Erlang Public License,
+%% Version 1.1, (the "License"); you may not use this file except in
+%% compliance with the License. You should have received a copy of the
+%% Erlang Public License along with this software. If not, it can be
+%% retrieved online at http://www.erlang.org/.
+%%
+%% Software distributed under the License is distributed on an "AS IS"
+%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
+%% the License for the specific language governing rights and limitations
+%% under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+%%%-------------------------------------------------------------------
+%%% File        : dialyzer_typesig_coordinator.erl
+%%% Authors     : Stavros Aronis <[email protected]>
+%%%
+%%% Description:
+%%%
+%%% The parallel version of Dialyzer's typesig analysis is spread over 4 modules
+%%% with the intention to both minimize the changes on the original code and use
+%%% a separate module for every kind of Erlang process that will be running.
+%%%
+%%% There are therefore 3 kinds of processes:
+%%%
+%%% - The original Dialyzer backend (in succ_typings module)
+%%% - The worker process for the typesig analysis (in typesig and
+%%%   typesig_worker)
+%%% - A coordinator of the worker processes (in typesig_coordinator)
+%%%
+%%% Operation guidelines:
+%%%
+%%% - The backend requests from the coordinator to spawn a worker for each SCC
+%%% - The backend notifies the coordinator when all SCC have been spawned and
+%%%   waits for the server to report that the PLT has been updated
+%%% - Each worker is responsible to notify all those who wait for it.
+%%%
+%%%-------------------------------------------------------------------
+
+-module(dialyzer_typesig_coordinator).
+
+-export([
+	 all_spawned/1,
+	 scc_done/3,
+	 scc_spawn/2,
+	 sccs_to_pids_reply/0,
+	 sccs_to_pids_request/2,
+	 start/1,
+	 receive_not_fixpoint/0
+	]).
+
+-behaviour(gen_server).
+
+-export([init/1, handle_call/3, handle_cast/2, handle_info/2, terminate/2,
+	 code_change/3]).
+
+-type coordinator() :: pid().
+-type map() :: dict().
+-type scc() :: [mfa_or_funlbl()].
+
+-record(state, {parent                   :: pid(),
+		spawn_count  = 0         :: integer(),
+		all_spawned  = false     :: boolean(),
+		scc_to_pid   = new_map() :: map(),
+		not_fixpoint = []        :: [mfa_or_funlbl()],
+		servers                  :: dialyzer_typesig:servers()
+	       }).
+
+-include("dialyzer.hrl").
+
+%%--------------------------------------------------------------------
+
+-spec start(dialyzer_typesig:servers()) -> pid().
+
+start(Servers) ->
+    {ok, Pid} = gen_server:start(?MODULE, {self(), Servers}, []),
+    Pid.
+
+-spec scc_spawn(scc(), coordinator()) -> ok.
+
+scc_spawn(SCC, Coordinator) ->
+    cast({scc_spawn, SCC}, Coordinator).
+
+-spec sccs_to_pids_request([scc()], coordinator()) -> ok.
+
+sccs_to_pids_request(SCCs, Coordinator) ->
+    cast({sccs_to_pids, SCCs, self()}, Coordinator).
+
+scc_to_pids_request_handle(Worker, SCCs, SCCtoPID) ->
+    Pids = [fetch_map(SCC, SCCtoPID) || SCC <- SCCs],
+    Worker ! {sccs_to_pids, Pids},
+    ok.
+
+-spec sccs_to_pids_reply() -> [dialyzer_typesig_worker:worker()].
+
+sccs_to_pids_reply() ->
+    receive {sccs_to_pids, Pids} -> Pids end.
+
+-spec scc_done(scc(), scc(), coordinator()) -> ok.
+
+scc_done(SCC, NotFixpoint, Coordinator) ->
+    cast({scc_done, SCC, NotFixpoint}, Coordinator).
+
+-spec all_spawned(coordinator()) -> ok.
+
+all_spawned(Coordinator) ->
+    cast(all_spawned, Coordinator).
+
+send_done_to_parent(#state{parent = Parent, not_fixpoint = NotFixpoint}) ->
+    Parent ! {not_fixpoint, NotFixpoint}.
+
+-spec receive_not_fixpoint() -> dialyzer_plt:plt().
+
+receive_not_fixpoint() ->
+    receive {not_fixpoint, NotFixpoint} -> NotFixpoint end.
+
+%%--------------------------------------------------------------------
+
+-spec init([]) -> {ok, #state{}}.
+
+init({Parent, Servers}) ->
+    {ok, #state{parent = Parent, servers = Servers}}.
+
+-spec handle_call(Query::term(), From::term(), #state{}) ->
+        {reply, Reply::term(), #state{}}.
+
+handle_call(_Request, _From, State) ->
+    {reply, ok, State}.
+
+-spec handle_cast(Msg::term(), #state{}) ->
+        {noreply, #state{}} | {stop, normal, #state{}}.
+
+handle_cast({scc_done, _SCC, NotFixpoint},
+	    #state{spawn_count = SpawnCount,
+		   all_spawned = AllSpawned,
+		   not_fixpoint = OldNotFixpoint
+		  } = State) ->
+    NewNotFixpoint = ordsets:union(OldNotFixpoint, NotFixpoint),
+    UpdatedState = State#state{not_fixpoint = NewNotFixpoint},
+    Action =
+	case AllSpawned of
+	    false -> reduce;
+	    true ->
+		case SpawnCount of
+		    1 -> finish;
+		    _ -> reduce
+		end
+	end,
+    case Action of
+	reduce ->
+	    NewState = UpdatedState#state{spawn_count = SpawnCount - 1},
+	    {noreply, NewState};
+	finish ->
+	    send_done_to_parent(UpdatedState),
+	    {stop, normal, State}
+    end;
+handle_cast(all_spawned, #state{spawn_count = SpawnCount} = State) ->
+    case SpawnCount of
+	0 ->
+	    send_done_to_parent(State),
+	    {stop, normal, State};
+	_ ->
+	    NewState = State#state{all_spawned = true},
+	    {noreply, NewState}
+    end;
+handle_cast({sccs_to_pids, SCCs, Worker},
+	    #state{scc_to_pid = SCCtoPID} = State) ->
+    scc_to_pids_request_handle(Worker, SCCs, SCCtoPID),
+    {noreply, State};
+handle_cast({scc_spawn, SCC},
+	    #state{servers = Servers,
+		   spawn_count = SpawnCount,
+		   scc_to_pid = SCCtoPID
+		  } = State) ->
+    Pid = dialyzer_typesig_worker:launch(SCC, Servers),
+    {noreply,
+     State#state{spawn_count = SpawnCount + 1,
+		 scc_to_pid = store_map(SCC, Pid, SCCtoPID)}
+    }.
+
+-spec handle_info(term(), #state{}) -> {noreply, #state{}}.
+
+handle_info(_Info, State) ->
+  {noreply, State}.
+
+-spec terminate(term(), #state{}) -> ok.
+
+terminate(_Reason, _State) ->
+  ok.
+
+-spec code_change(term(), #state{}, term()) -> {ok, #state{}}.
+
+code_change(_OldVsn, State, _Extra) ->
+  {ok, State}.
+
+%%--------------------------------------------------------------------
+
+cast(Message, Coordinator) ->
+    gen_server:cast(Coordinator, Message).
+
+new_map() ->
+    dict:new().
+
+store_map(Key, Value, Map) ->
+    dict:store(Key, Value, Map).
+
+fetch_map(Key, Map) ->
+    dict:fetch(Key, Map).
diff --git a/lib/dialyzer/src/dialyzer_typesig_worker.erl b/lib/dialyzer/src/dialyzer_typesig_worker.erl
new file mode 100644
index 0000000000..3a7cd22eed
--- /dev/null
+++ b/lib/dialyzer/src/dialyzer_typesig_worker.erl
@@ -0,0 +1,142 @@
+%% -*- erlang-indent-level: 2 -*-
+%%-----------------------------------------------------------------------
+%% %CopyrightBegin%
+%%
+%% Copyright Ericsson AB 2006-2010. All Rights Reserved.
+%%
+%% The contents of this file are subject to the Erlang Public License,
+%% Version 1.1, (the "License"); you may not use this file except in
+%% compliance with the License. You should have received a copy of the
+%% Erlang Public License along with this software. If not, it can be
+%% retrieved online at http://www.erlang.org/.
+%%
+%% Software distributed under the License is distributed on an "AS IS"
+%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
+%% the License for the specific language governing rights and limitations
+%% under the License.
+%%
+%% %CopyrightEnd%
+%%
+
+-module(dialyzer_typesig_worker).
+
+-export([launch/2]).
+
+-type worker() :: pid().
+
+-record(state, {
+	  scc         = [] :: mfa_or_funlbl(),
+	  depends_on  = [] :: list(),
+	  coordinator      :: dialyzer_coordinator:coordinator(),
+	  servers          :: dialyzer_typesig:servers(),
+	  scc_data         :: dialyzer_typesig:scc_data()
+	 }).
+
+-include("dialyzer.hrl").
+
+%% -define(DEBUG, true).
+
+-ifdef(DEBUG).
+-define(debug(X__, Y__), io:format(X__, Y__)).
+-else.
+-define(debug(X__, Y__), ok).
+-endif.
+
+%%--------------------------------------------------------------------
+
+-spec launch([mfa_or_funlbl()], dialyzer_typesig:servers()) -> worker().
+
+launch(SCC, Servers) ->
+  State = #state{scc         = SCC,
+		 servers     = Servers,
+		 coordinator = self()},
+  spawn(fun() -> loop(initializing, State) end).
+
+%%--------------------------------------------------------------------
+
+loop(updating, State) ->
+  ?debug("Update: ~p\n",[State#state.scc]),
+  NextStatus =
+    case waits_more_success_typings(State) of
+      true -> waiting;
+      Other ->
+	case has_data(State) of
+	  false -> getting_data;
+	  true ->
+	    case Other of
+	      imminent -> waiting;
+	      false -> running
+	    end
+	end
+    end,
+  loop(NextStatus, State);
+loop(initializing, #state{scc = SCC, servers = Servers} = State) ->
+  DependsOn = dialyzer_succ_typings:find_depends_on(SCC, Servers),
+  WithoutSelf = DependsOn -- [SCC],
+  ?debug("Deps ~p: ~p\n",[State#state.scc, WithoutSelf]),
+  loop(updating, State#state{depends_on = WithoutSelf});
+loop(waiting, State) ->
+  ?debug("Wait: ~p\n",[State#state.scc]),
+  NewState = wait_for_success_typings(State),
+  loop(updating, NewState);
+loop(getting_data, State) ->
+  ?debug("Data: ~p\n",[State#state.scc]),
+  loop(updating, get_typesig_data(State));
+loop(running, State) ->
+  ?debug("Run: ~p\n",[State#state.scc]),
+  ok = ask_coordinator_for_callers(State),
+  NotFixpoint = find_succ_typings(State),
+  Callers = get_callers_reply_from_coordinator(),
+  ok = broadcast_own_succ_typings(State, Callers),
+  report_to_coordinator(NotFixpoint, State).
+
+waits_more_success_typings(#state{depends_on = Depends}) ->
+  case Depends of
+    [] -> false;
+    [_] -> imminent;
+    _ -> true
+  end.
+
+has_data(#state{scc_data = Data}) ->
+  case Data of
+    undefined -> false;
+    _ -> true
+  end.
+
+get_typesig_data(#state{scc = SCC, servers = Servers} = State) ->
+  State#state{scc_data = dialyzer_succ_typings:collect_scc_data(SCC, Servers)}.
+
+ask_coordinator_for_callers(#state{scc = SCC,
+				   servers = Servers,
+				   coordinator = Coordinator}) ->
+  RequiredBy = dialyzer_succ_typings:find_required_by(SCC, Servers),
+  WithoutSelf = RequiredBy -- [SCC],
+  ?debug("Waiting for me~p: ~p\n",[SCC, WithoutSelf]),
+  dialyzer_typesig_coordinator:sccs_to_pids_request(WithoutSelf, Coordinator).
+
+get_callers_reply_from_coordinator() ->
+  dialyzer_typesig_coordinator:sccs_to_pids_reply().
+
+broadcast_own_succ_typings(#state{scc = SCC}, Callers) ->
+  ?debug("Sending ~p: ~p\n",[SCC, Callers]),
+  SendSTFun = fun(PID) -> PID ! {done, SCC} end,
+  lists:foreach(SendSTFun, Callers).
+
+wait_for_success_typings(#state{depends_on = DependsOn} = State) ->
+  receive
+    {done, SCC} ->
+      ?debug("GOT ~p: ~p\n",[State#state.scc, SCC]),
+      State#state{depends_on = DependsOn -- [SCC]}
+  after
+    5000 ->
+      ?debug("Still Waiting ~p: ~p\n",[State#state.scc, DependsOn]),
+      State
+  end.
+
+find_succ_typings(#state{scc_data = SCCData}) ->
+  dialyzer_succ_typings:find_succ_types_for_scc(SCCData).
+
+report_to_coordinator(NotFixpoint,
+		      #state{scc = SCC, coordinator = Coordinator}) ->
+  ?debug("Done: ~p\n",[SCC]),
+  dialyzer_typesig_coordinator:scc_done(SCC, NotFixpoint, Coordinator).