Skip to content

Draft: Parallel Simplifier

Matthew Pickering requested to merge wip/par-simpl into master

There are a few parts to this patch.

  1. Main parallelism implementation is fairly standard, see simplTopBinds. The binds are sorted in topological order and then split into groups of size k, each group is simplified together and spawned into a new thread. Once a group is finished the results are placed into an MVar, each group combines together the results of previous groups in order to construct an up-to-date environment to simplify the bindings in. Creating groups of a big-enough size was one of the key points in getting the implementation to work, if the group size is too small you waste a lot of time unioning together floats and in-scope sets.
  2. InScopeSet definition tracks the "age" of variables so that when we union InScopeSets together we can choose the updated variables rather than out-of-date variables. This is achieved by using a VarEnv (Var, Int) rather than a VarSet.
  3. When simplifying things in parallel the InScopeSet doesn't account for bindings in other branches, so when you float out local things and come up with a new unique you can get clashes. Therefore after simplifying things in parallel we need to rewrite the floats so that the names no longer clash with each other. The difficulty here is that then you have to fully apply this substitution to the whole simplified term, including inside stable unfoldings. The substitution functions currently don't traverse into stable unfoldings.
Edited by Matthew Pickering

Merge request reports