From 964363504ceca953c5d0aad72f657491707c80c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Jul 2025 20:13:06 -0700 Subject: [PATCH] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 5964037a7..4f1cff598 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -2,7 +2,7 @@ -We track notes for updates to smt\_parallel.cpp and possibly solver/parallel\_tactic.cpp +We track notes for updates to smt/parallel.cpp and possibly solver/parallel\_tactic.cpp @@ -112,3 +112,8 @@ We can represent a list of cubes by using intervals and only represent start and #### Batching 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.