diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 4f1cff598..36ff74d15 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -2,7 +2,10 @@ -We track notes for updates to smt/parallel.cpp and possibly solver/parallel\_tactic.cpp +We track notes for updates to +[smt/parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/smt/smt_parallel.cpp) +and possibly +[https://github.com/Z3Prover/z3/blob/master/src/solver/parallel_tactic.cpp](solver/parallel_tactic.cpp). @@ -116,4 +119,4 @@ Threads can work on more than one cube in a batch. ### Synchronization * The first thread to time out or finish could kill other threads instead of joining on all threads to finish. -* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in sat/sat_parallel.cpp. +* Instead of synchronization barriers have threads continue concurrently without terminating. They synchronize on signals and new units. This is trickier to implement, but in some guises accomplished in [sat/sat_parallel.cpp](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_parallel.cpp)