Abstract

Work-efficient parallel mergesort

Author: Sam Westrick <shwestrick@gmail.com.

Synopsis

val merge_sort_with_params [n] 't : {max_block_size: i64, max_merge_block_size: i64} -> (leq: t -> t -> bool) -> (s: [n]t) -> [n]t
val merge_sort [n] 't : (leq: t -> t -> bool) -> (s: [n]t) -> [n]t
val merge_sort_by_key [n] 't 'k : (key: t -> k) -> (leq: k -> k -> bool) -> (s: [n]t) -> [n]t
val merge_sort_with_params_by_key [n] 't 'k 't₂₄ : (params: {max_block_size: i64, max_merge_block_size: i64}) -> (key: t -> t₂₄) -> (leq: t₂₄ -> t₂₄ -> bool) -> (s: [n]t) -> [n]t

Description

↑val merge_sort_with_params [n] 't: {max_block_size: i64, max_merge_block_size: i64} -> (leq: t -> t -> bool) -> (s: [n]t) -> [n]t

Work-efficient parallel mergesort: merge_sort_with_params {max_block_size, max_merge_block_size} leq s

Any values for {max_block_size, max_merge_block_size} are acceptable, but do heavily impact performance. See merge_sort below for reasonable choices that seem to work well in practice.

↑val merge_sort [n] 't: (leq: t -> t -> bool) -> (s: [n]t) -> [n]t
↑val merge_sort_by_key [n] 't 'k: (key: t -> k) -> (leq: k -> k -> bool) -> (s: [n]t) -> [n]t
↑val merge_sort_with_params_by_key [n] 't 'k 't₂₄: (params: {max_block_size: i64, max_merge_block_size: i64}) -> (key: t -> t₂₄) -> (leq: t₂₄ -> t₂₄ -> bool) -> (s: [n]t) -> [n]t