Changes

Summary

1. merged;
2. more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
3. more synchronized Execution.snapshot;
4. tuned spelling;
5. tuned;
6. tuned;