Imports
import CLRSLean.Chapter_27.Section_27_1_Multithreading_Model
import CLRSLean.Chapter_27.Section_27_1_Multithreading_Model.S1_ComputationDAG
import CLRSLean.Chapter_27.Section_27_1_Multithreading_Model.S2_ReadyExecution
import CLRSLean.Chapter_27.Section_27_1_Multithreading_Model.S3_GreedyAccounting
import CLRSLean.Chapter_27.Section_27_1_Multithreading_Model.S4_ExecutableScheduler
import CLRSLean.Chapter_27.Section_27_1_Multithreading_Model.S5_SpawnTreeAndLoops
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.S1_CostModel
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.S2_Recurrences
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.S3_AllInputBounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Correctness
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Costs
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Costs.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Costs.ExecutionEqualities
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Costs.Monotonicity
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Costs.PowerBounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMatrix.Costs.AllInputBounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.LowerBound
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.LowerBound.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.LowerBound.Correctness
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.LowerBound.Costs
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.MergeSplit
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.PMerge
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.PMerge.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.PMerge.Correctness
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.PMerge.Correctness.Boundaries
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.PMerge.Correctness.Permutation
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.PMerge.Correctness.Main
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Correctness
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Structure
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Step
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Work
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Work.LogPotential
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Work.Bounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Span
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Span.Envelope
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Span.Bounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Span.WitnessLists
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMerge.Costs.Span.LowerBound
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Correctness
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Correctness.Spec
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Correctness.Main
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Step
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.RecurrenceLinks
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Work
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Work.Bounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Span
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Span.Bounds
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Span.WitnessInput
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Span.MapInvariance
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelMergeSort.Costs.Span.LowerBound
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelStrassen
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelStrassen.Recurrences
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelStrassen.Recurrences.Definitions
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelStrassen.Recurrences.Monotonicity
import CLRSLean.Chapter_27.Section_27_2_4_Algorithms.ParallelStrassen.Recurrences.AllInputBoundsChapter 27 - Multithreaded Algorithms
Chapter 27 opens Part VII (Parallel Algorithms) of CLRS. It develops the dynamic-multithreading model and analyzes parallel algorithms in terms of work (T₁, total operations) and span (T∞, critical-path length).
Sections
-
27.1 The basics of dynamic multithreading. The computation-DAG model has forward (topologically ordered) edges and an honestly computed longest-weighted-path span. Its ready-set semantics feeds the total executable
CLRS.Chapter27.CompDAG.greedySchedule: the final residual work is zero and its time satisfiesTₚ ≤ T₁ / p + T∞. The spawn/sync-tree model has unit spawn overhead, and the balanced parallel-loop tree has exact work/span formulas together with all-input logarithmic depth and span upper bounds. Main declarations:CLRS.Chapter27.Strand,CLRS.Chapter27.CompDAG,CLRS.Chapter27.CompDAG.work,CLRS.Chapter27.CompDAG.longestTo,CLRS.Chapter27.CompDAG.span,CLRS.Chapter27.CompDAG.span_le_work,CLRS.Chapter27.CompDAG.ready,CLRS.Chapter27.DAGScheduleStep,CLRS.Chapter27.DAGSchedule,CLRS.Chapter27.DAGSchedule.time_le_work_div_add_span,CLRS.Chapter27.CompDAG.greedySchedule,CLRS.Chapter27.CompDAG.greedySchedule_final_work_eq_zero,CLRS.Chapter27.CompDAG.greedySchedule_time_le_work_div_add_span,CLRS.Chapter27.SpawnTree,CLRS.Chapter27.SpawnTree.span_le_work,CLRS.Chapter27.parallelLoopTree,CLRS.Chapter27.parallelLoop_work,CLRS.Chapter27.parallelLoop_span,CLRS.Chapter27.parallelLoopDepth_pow,CLRS.Chapter27.parallelLoopDepth_le_log,CLRS.Chapter27.parallelLoop_span_le_log. -
27.2 Multithreaded matrix multiplication. An executable
Costedlayer attaches a pure value to exact work and span, with sequential and balanced parallel composition. P-ADD and the race-free P-MATMUL execute quadrant operations through deterministic fork/join trees;CLRS.Chapter27.pAdd_correctandCLRS.Chapter27.pMatMul_correctprove ordinary matrix addition and multiplication over any ring. Execution equalities connect their carried costs toCLRS.Chapter27.pAddWork,CLRS.Chapter27.pAddSpan,CLRS.Chapter27.pMatMulExecWork, andCLRS.Chapter27.pMatMulExecSpan. The resulting all-input bounds are Θ(n²) work / Θ(log n) span for P-ADD and Θ(n³) work / Θ(log² n) span for executable P-MATMUL. The legacyCLRS.Chapter27.pMatMulSpanrecurrence instead models a constant-time combine and therefore has Θ(log n) span; it is intentionally not the runtime of the implementation, whose sequential P-ADD combine phase yields the log-squared span. Main declarations:CLRS.Chapter27.Costed,CLRS.Chapter27.Costed.seq,CLRS.Chapter27.Costed.par,CLRS.Chapter27.Costed.par4,CLRS.Chapter27.Costed.par8,CLRS.Chapter27.pAdd,CLRS.Chapter27.pAdd_correct,CLRS.Chapter27.pMatMul,CLRS.Chapter27.pMatMul_correct,CLRS.Chapter27.pAdd_work_eq,CLRS.Chapter27.pAdd_span_eq,CLRS.Chapter27.pMatMul_work_eq,CLRS.Chapter27.pMatMul_span_eq,CLRS.Chapter27.pAddWork_allInput_bigTheta,CLRS.Chapter27.pAddSpan_allInput_bigTheta,CLRS.Chapter27.pMatMulExecWork_allInput_bigTheta,CLRS.Chapter27.pMatMulExecSpan_allInput_bigTheta,CLRS.Chapter27.pMatMulSpan_le. -
27.3 Multithreaded merge sort. The executable binary lower bound used by P-MERGE has a proved strict-left, nonstrict-right partition and logarithmic work/span. The
CLRS.Chapter27.MergeSplitandCLRS.Chapter27.pMergelayer implements the actual midpoint/binary-search P-MERGE control structure;CLRS.Chapter27.pMerge_correctproves its value is a sorted permutation of the two sorted inputs with exact output length. Its actual execution also has pointwise linear work, proved by logarithmic-potential strong induction, and pointwise quadratic-logarithmic span. A monotone three-quarter envelope proves the upper bound, while sorted interleaved even/odd power-of-two inputs provide the matching lower witness.CLRS.Chapter27.pMergeSortnow implements the full midpoint-split, parallel-recursive, P-MERGE-based sorting control structure, andCLRS.Chapter27.pMergeSort_correctproves that every result is a sorted permutation of its input with unchanged length. Exact one-step cost equations connect this execution to its recurrence: the pointwise work bounds give Θ(n log n), the universal span upper bound is cubic-logarithmic, andCLRS.Chapter27.worstMergeSortInputsupplies a matching recursive lower-witness family. Thus the executable P-MERGE-SORT cost gap is closed. The merge-based recurrences also have monotonicity, adjacent-power sandwiches, and all-input Θ theorems. Main declarations:CLRS.Chapter27.binaryLowerBound,CLRS.Chapter27.binaryLowerBound_partition,CLRS.Chapter27.binaryLowerBound_work_le_log,CLRS.Chapter27.binaryLowerBound_span_le_log,CLRS.Chapter27.MergeSplit,CLRS.Chapter27.pMerge,CLRS.Chapter27.PMergeSpec,CLRS.Chapter27.pMerge_correct,CLRS.Chapter27.pMerge_value_sorted,CLRS.Chapter27.pMerge_value_perm,CLRS.Chapter27.pMerge_value_length,CLRS.Chapter27.pMerge_childSizes_add_one,CLRS.Chapter27.pMerge_childSize_le_threeQuarters,CLRS.Chapter27.pMerge_work_step_eq,CLRS.Chapter27.pMerge_span_step_eq,CLRS.Chapter27.pMerge_work_lower,CLRS.Chapter27.pMerge_work_upper,CLRS.Chapter27.pMerge_span_upper,CLRS.Chapter27.evenKeys,CLRS.Chapter27.oddKeys,CLRS.Chapter27.pMerge_interleaved_span_lower,CLRS.Chapter27.pMergeSort,CLRS.Chapter27.PMergeSortSpec,CLRS.Chapter27.pMergeSort_correct,CLRS.Chapter27.pMergeSort_value_sorted,CLRS.Chapter27.pMergeSort_value_perm,CLRS.Chapter27.pMergeSort_value_length,CLRS.Chapter27.pMergeSort_work_step_eq,CLRS.Chapter27.pMergeSort_span_step_eq,CLRS.Chapter27.pMergeSort_work_lower,CLRS.Chapter27.pMergeSort_work_upper,CLRS.Chapter27.pMergeSort_span_upper,CLRS.Chapter27.worstMergeSortInput,CLRS.Chapter27.worstMergeSortInput_length,CLRS.Chapter27.pMergeSort_worstFamily_span_lower,CLRS.Chapter27.pMergeWork,CLRS.Chapter27.pMergeWork_pow_two,CLRS.Chapter27.pMergeWork_monotone,CLRS.Chapter27.pMergeWork_power_sandwich,CLRS.Chapter27.pMergeWork_allInput_bigTheta,CLRS.Chapter27.pMergeSpan,CLRS.Chapter27.pMergeSpan_pow_two,CLRS.Chapter27.pMergeSpan_monotone,CLRS.Chapter27.pMergeSpan_power_sandwich,CLRS.Chapter27.pMergeSpan_allInput_bigTheta,CLRS.Chapter27.pMergeSortWork,CLRS.Chapter27.pMergeSortWork_pow_two,CLRS.Chapter27.pMergeSortWork_monotone,CLRS.Chapter27.pMergeSortWork_power_sandwich,CLRS.Chapter27.pMergeSortWork_allInput_bigTheta,CLRS.Chapter27.pMergeSortSpan,CLRS.Chapter27.pMergeSortSpan_pow_two,CLRS.Chapter27.pMergeSortSpan_monotone,CLRS.Chapter27.pMergeSortSpan_power_sandwich,CLRS.Chapter27.pMergeSortSpan_allInput_bigTheta. -
Parallel Strassen compatibility extension. The historical Chapter 27 import surface retains a separate recurrence-only analysis for a parallelized Strassen variant. It is not presented as a Chapter 27 main-text section. Main declarations:
CLRS.Chapter27.strassenWork,CLRS.Chapter27.strassenWork_pow_two,CLRS.Chapter27.strassenWork_monotone,CLRS.Chapter27.strassenWork_power_sandwich,CLRS.Chapter27.strassenWork_allInput_bigTheta,CLRS.Chapter27.strassenSpan,CLRS.Chapter27.strassenSpan_pow_two,CLRS.Chapter27.strassenSpan_monotone,CLRS.Chapter27.strassenSpan_power_sandwich,CLRS.Chapter27.strassenSpan_allInput_bigTheta.
The filesystem name Section_27_2_4_Algorithms is retained solely for
import compatibility with existing clients. The represented Chapter 27 main
text ends at Section 27.3; the Strassen recurrences above are a named extension,
not a fabricated Section 27.4.
Completion boundary
The represented Chapter 27 main-text core is complete: algorithms, correctness, execution-attached work/span bounds, recurrence analyses, and the greedy-scheduler theorem are connected at their reader-facing interfaces. The retained parallel-Strassen recurrences are already isolated behind their compatibility extension and are not a Chapter 27 proof obligation. Mutable-array implementations, RAM-level operation and allocation costs, exercises, and chapter-end problems are outside this sealed pure-functional boundary.
namespace CLRSnamespace Chapter27end Chapter27end CLRS