Skip to content

Cilksort spring 2025 #27

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

Cilksort spring 2025 #27

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5d28b28
Construct Cilksort with reasonable parameters and connect it to bench…
jazullo Mar 25, 2025
5899e2c
add CI calls to the newly-added Cilksort
ulysses4ever Aug 15, 2025
981e31e
typo
ulysses4ever Aug 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .github/workflows/build-test-linear.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,8 @@ jobs:
cabal run benchrunner -- 5 Mergesort Seq 1000
cabal run benchrunner -- 5 Mergesort Par 1000 +RTS -N1
cabal run benchrunner -- 5 Mergesort Par 1000 +RTS -N2
cabal run benchrunner -- 5 Cilksort Par 1000 +RTS -N1
cabal run benchrunner -- 5 Cilksort Par 1000 +RTS -N2
cabal run benchrunner -- 5 "VectorSort Insertionsort" Seq 1000
cabal run benchrunner -- 5 "VectorSort Mergesort" Seq 1000
cabal run benchrunner -- 5 "VectorSort Quicksort" Seq 1000
Expand Down
3 changes: 3 additions & 0 deletions benchrunner/Benchrunner.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ import qualified Insertion as I
import qualified QuickSort as Q
import qualified DpsMergeSort4 as DMS
import qualified DpsMergeSort4Par as DMSP
import qualified CilkSort as CSP
import qualified PiecewiseFallbackSort as PFS
import qualified PiecewiseFallbackSortPar as PFSP
import qualified Microbench as MB
Expand All @@ -41,6 +42,7 @@ getInput bench mb_size = case bench of
Insertionsort -> ArrayIn <$> randArray (Proxy :: Proxy Int64) (mb 100)
Quicksort -> ArrayIn <$> randArray (Proxy :: Proxy Int64) (mb 1000000)
Mergesort -> ArrayIn <$> randArray (Proxy :: Proxy Int64) (mb 8000000)
Cilksort -> ArrayIn <$> randArray (Proxy :: Proxy Int64) (mb 8000000)
Optsort -> ArrayIn <$> randArray (Proxy :: Proxy Int64) (mb 8000000)
_ -> error "getInput: Unexpected Input!"
where
Expand Down Expand Up @@ -103,6 +105,7 @@ sortFn bench parorseq = case (bench,parorseq) of
(Mergesort, Par) -> DMSP.msort
(Optsort, Seq) -> PFS.pfsort
(Optsort, Par) -> PFSP.pfsort
(Cilksort, Par) -> CSP.cilkSort
oth -> error $ "sortFn: unknown configuration: " ++ show oth

vectorSortFn :: SortAlgo -> ParOrSeq -> VecSort
Expand Down
1 change: 1 addition & 0 deletions benchrunner/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ data SortAlgo
= Insertionsort
| Mergesort
| Quicksort
| Cilksort
| Optsort -- piecewise fallback
deriving (Eq, Show, Read)

Expand Down
8 changes: 2 additions & 6 deletions lh-array-sort.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,13 +67,9 @@ library
PiecewiseFallbackSort
PiecewiseFallbackSortPar

-- JZ: Add Parallel Cilksort
-- Current Cilksort is entirely sequential
QuickSortCilk
CilkSort

-- remove until ready:
-- QuickSortNew
-- the last not quite ready yet?
-- CilkSort
Linear.Common
other-modules:
Array.List
Expand Down
95 changes: 58 additions & 37 deletions src/CilkSort.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,24 +6,26 @@ module CilkSort where
import qualified Language.Haskell.Liquid.Bag as B
import Language.Haskell.Liquid.ProofCombinators hiding ((?))
import ProofCombinators
import Array
import Array as A
import ArrayOperations
import DpsMerge
import DpsMergePar
import qualified DpsMergeSort4 as Seq
import Properties.Equivalence
import Properties.Order
import Insertion
import QuickSortCilk
import Par

import Linear.Common
#ifdef MUTABLE_ARRAYS
import Array.Mutable as A
import Control.DeepSeq ( NFData(..) )
#else
import Array.List as A
#endif

#define KILO 1024
#define MERGESIZE (2*KILO)
#define QUICKSIZE (2*KILO)
#define INSERTIONSIZE 20
#define QUICKSIZE (8*KILO)
#define SEQSIZE (8*KILO)

-- DPS mergesort -- unfold twice, merge twice
{-@ cilkSortInplace :: xs:Array a
Expand All @@ -35,51 +37,70 @@ import Array.List as A
left zs == left xs && right zs == right xs &&
left ts == left ys && right ts == right ys }>
/ [A.size xs] @-}
cilkSortInplace :: (Show a, Ord a) => A.Array a -> A.Array a -> (A.Array a, A.Array a)
#ifdef MUTABLE_ARRAYS
cilkSortInplace :: (Show a, HasPrimOrd a, NFData a) =>
#else
cilkSortInplace :: (Show a, HasPrimOrd a) =>
#endif
A.Array a -. A.Array a -. (A.Array a, A.Array a)
cilkSortInplace src tmp =
let (len, src') = A.size2 src in
if len <= QUICKSIZE
then let src'' = quickSort src'
in (src'', tmp)
let !(Ur len, src') = A.size2 src in
if len <= SEQSIZE
then
if len <= QUICKSIZE
then let src'' = quickSort src'
in (src'', tmp)
else Seq.msortInplace src' tmp
else
let (srcA, srcB) = splitMid src'
(tmpA, tmpB) = splitMid tmp
(src1, src2) = splitMid srcA
(src3, src4) = splitMid srcB
(tmp1, tmp2) = splitMid tmpA
(tmp3, tmp4) = splitMid tmpB
(src1', tmp1') = cilkSortInplace src1 tmp1
(src2', tmp2') = cilkSortInplace src2 tmp2
(src3', tmp3') = cilkSortInplace src3 tmp3
(src4', tmp4') = cilkSortInplace src4 tmp4
let !(srcA, srcB) = splitMid src'
!(tmpA, tmpB) = splitMid tmp
!(src1, src2) = splitMid srcA
!(src3, src4) = splitMid srcB
!(tmp1, tmp2) = splitMid tmpA
!(tmp3, tmp4) = splitMid tmpB
!(((src1', tmp1'), (src2', tmp2')), ((src3', tmp3'), (src4', tmp4')))
= (.||||.) (cilkSortInplace src1 tmp1) (cilkSortInplace src2 tmp2)
(cilkSortInplace src3 tmp3) (cilkSortInplace src4 tmp4)
tmpA' = A.append tmp1' tmp2'
tmpB' = A.append tmp3' tmp4'
(srcA'', tmpA'') = merge src1' src2' tmpA'
(srcB'', tmpB'') = merge src3' src4' tmpB'
!((srcA'', tmpA''), (srcB'', tmpB''))
= merge_par src1' src2' tmpA' .||. merge_par src3' src4' tmpB'
-- = tuple2 (merge_par src1' src2') tmpA' (merge_par src3' src4') tmpB'
src'' = A.append srcA'' srcB''
(tmp''', src''') = merge tmpA'' tmpB'' src''
in (src''', tmp''') ? lem_toBag_splitMid src
!(tmp''', src''') = merge_par tmpA'' tmpB'' src''
in (src''', tmp''') ? lem_toBag_splitMid src
? lem_toBag_splitMid tmp
? lem_toBag_splitMid srcA
? lem_toBag_splitMid srcB
? lem_toBag_splitMid tmpA
? lem_toBag_splitMid tmpB

{-@ cilkSort' :: { xs:(Array a) | A.size xs > 0 && left xs == 0 && right xs == size xs }
-> { y:a | y == A.get xs 0 }
-> { zs:(Array a) | toBag xs == toBag zs && isSorted' zs &&
A.size xs == A.size zs && token xs == token zs } @-}
cilkSort' :: (Show a, Ord a) => A.Array a -> a -> A.Array a
cilkSort' src anyVal =
let (len, src') = A.size2 src
(src'', _tmp) = cilkSortInplace src' (A.make len anyVal) in
_tmp `seq` src''
{-@ cilkSort' :: y:a
-> { xs:(Array a) | A.size xs > 0 && left xs == 0 && right xs == size xs && y == A.get xs 0 }
-> { zs:(Array a) | toBag xs == toBag zs && isSorted' zs &&
A.size xs == A.size zs && token xs == token zs } @-}
#ifdef MUTABLE_ARRAYS
cilkSort' :: (Show a, HasPrimOrd a, NFData a) =>
#else
cilkSort' :: (Show a, HasPrimOrd a) =>
#endif
a -> A.Array a -. A.Array a
cilkSort' anyVal src =
let !(Ur len, src') = A.size2 src
!src'' = A.allocScratch len anyVal cilkSortInplace src' in
src''

-- finally, the top-level cilksort function
{-@ cilkSort :: { xs:(A.Array a) | left xs == 0 && right xs == size xs }
-> { ys:_ | toBag xs == toBag ys && isSorted' ys &&
A.size xs == A.size ys && token xs == token ys } @-}
cilkSort :: (Show a, Ord a) => A.Array a -> A.Array a
#ifdef MUTABLE_ARRAYS
cilkSort :: (Show a, HasPrimOrd a, NFData a) =>
#else
cilkSort :: (Show a, HasPrimOrd a) =>
#endif
A.Array a -. A.Array a
cilkSort src =
let (len, src') = A.size2 src in
let !(Ur len, src') = A.size2 src in
if len == 0 then src'
else let (x0, src'') = A.get2 src' 0 in cilkSort' src'' x0
else let !(Ur x0, src'') = A.get2 0 src' in cilkSort' x0 src''
153 changes: 84 additions & 69 deletions src/QuickSortCilk.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import Properties.RangeProperties

import Insertion

import Linear.Common
#ifdef MUTABLE_ARRAYS
import qualified Unsafe.Linear as Unsafe
import Array.Mutable as A
Expand All @@ -41,27 +42,33 @@ import qualified Array as A
{-@ quickSort :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
toBag xs == toBag ys } @-}
-- quickSort :: (Ord a, Show a) => Array a -> Array a
quickSort :: (HasPrimOrd a, Show a) => Array a -> Array a
quickSort :: (HasPrimOrd a, Show a) => Array a -. Array a
quickSort xs =
let (n, xs1) = A.size2 xs in
let (Ur n, xs1) = A.size2 xs in
if n == 0 then xs1
else let (hd, xs2) = A.get2 xs1 0
{-@ promise :: { tmp:(Array a) | size tmp == n }
-> { out:(Ur (Array a)) | size (unur out) == n &&
toSlice (unur out) 0 n == toSlice xs2 0 n} @-}
promise tmp = Ur (A.copy xs2 0 tmp 0 n)
? lem_copy_equal_slice xs2 0 tmp 0 n
{- @ cpy :: { ys:(Array a) | size ys == n && toSlice ys 0 n == toSlice xs2 0 n } @-}
Ur cpy = A.alloc n hd (Unsafe.toLinear promise)
in quickSortBtw (cpy ? lem_equal_slice_bag xs2 cpy 0 n) 0 n
else let (Ur hd, xs2) = A.get2 0 xs1
tmp = makeArray n hd in
A.copy2 0 0 n xs2 tmp ? lem_copy_equal_slice xs2 0 tmp 0 n & \(xs2', cpy0) ->
(A.free(xs2'), cpy0) & \((), cpy) ->
quickSortBtw 0 n (cpy ? lem_equal_slice_bag xs2 cpy 0 n)
{-# INLINABLE quickSort #-}

{-@ quickSort' :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
toBag xs == toBag ys } @-}
quickSort' :: (HasPrimOrd a, Show a) => Array a -. Array a
quickSort' xs =
let (Ur n, xs1) = A.size2 xs in
if n == 0 then xs1
else quickSortBtw 0 n xs1
{-# INLINABLE quickSort' #-}

{-@ quickSortBtw :: xs:(Array a) -> { i:Int | 0 <= i } -> { j:Int | i <= j && j <= A.size xs }
-> { ys:(Array a) | isSortedBtw ys i j && A.size xs == A.size ys &&
toSlice xs 0 i == toSlice ys 0 i &&
toSlice xs j (A.size xs) == toSlice ys j (A.size xs) &&
toBagBtw xs i j == toBagBtw ys i j } / [j - i] @-}
quickSortBtw :: HasPrimOrd a => Array a -> Int -> Int -> Array a
quickSortBtw xs i j =
quickSortBtw :: HasPrimOrd a => Int -> Int -> (Array a -. Array a)
quickSortBtw i j xs =
if j - i < 2 then xs else
if j - i <= INSERTIONSIZE
then let (xs_l, xs_cr) = A.splitAt i xs
Expand Down Expand Up @@ -101,9 +108,9 @@ quickSortBtw xs i j =
? lem_toSlice_slice xs i (A.size xs) (j-i) (A.size xs - i)
=== toSlice xs j (A.size xs)
)
else let (xs', i_piv) = shuffleBtw xs i j -- isPartitionedBtw xs' i i_piv j
xs'' = quickSortBtw xs' i i_piv
xs''' = quickSortBtw xs'' (i_piv + 1) j
else let (xs', Ur i_piv) = shuffleBtw i j xs
xs'' = quickSortBtw i i_piv xs'
xs''' = quickSortBtw (i_piv + 1) j xs''
? lem_qs_pres_partition_left xs' xs'' i i_piv j
in xs''' ? lem_sorted_partitions xs''' i i_piv (j
? lem_equal_slice_sorted xs'' xs''' 0 i i_piv (i_piv+1)
Expand All @@ -116,66 +123,74 @@ quickSortBtw xs i j =
? lem_equal_slice_bag xs'' xs''' i (i_piv+1)
? lem_toBagBtw_compose xs' xs'' i i_piv j
? lem_toBagBtw_compose xs'' xs''' i (i_piv+1) j
{-# INLINE quickSortBtw #-}

{-@ shuffleBtw :: xs:(Array a) -> { i:Int | 0 <= i } -> { j:Int | i + 1 < j && j <= A.size xs }
-> (Array a, Int)<{\ys ip -> isPartitionedBtw ys i ip j &&
{-@ shuffleBtw :: { i:Int | 0 <= i } -> j:Int -> { xs:(Array a) | i + 1 < j && j <= A.size xs }
-> (Array a, Ur Int)<{\ys ip -> isPartitionedBtw ys i (unur ip) j &&
toSlice xs 0 i == toSlice ys 0 i &&
toSlice xs j (A.size xs) == toSlice ys j (A.size xs) &&
toBagBtw xs i j == toBagBtw ys i j &&
i <= ip && ip < j && A.size ys == A.size xs }> @-}
shuffleBtw :: HasPrimOrd a => Array a -> Int -> Int -> (Array a, Int)
shuffleBtw xs i j =
i <= unur ip && unur ip < j && A.size ys == A.size xs }> @-}

shuffleBtw :: forall a. HasPrimOrd a => Int -> Int -> (Array a -. (Array a, Ur Int))
shuffleBtw i j xs = xs & A.get2 (j-1) {- fix (j-1)^th element as the pivot -} & \(Ur piv, xs1) ->
let
(piv, xs1) = A.get2 xs (j-1) -- fix xs[j-1] as the pivot
{-@ goShuffle :: { zs:(Array a) | get zs (j-1) == piv && A.size zs == A.size xs &&
toBagBtw zs i j == toBagBtw xs i j &&
toSlice xs 0 i == toSlice zs 0 i &&
toSlice xs j (A.size zs) == toSlice zs j (A.size zs)}
-> { jl:Int | i <= jl && rangeUpperBound zs i jl piv }
-> { jr:Int | jl <= jr+1 && jr < j-1 && rangeLowerBound zs (jr+1) (j-1) piv }
-> (Array a, Int)<{\ws ip -> rangeUpperBound ws i ip piv &&
rangeLowerBound ws ip (j-1) piv &&
A.size ws == A.size zs &&
get ws (j-1) == get zs (j-1) &&
toBagBtw zs i j == toBagBtw ws i j &&
toBagBtw xs i j == toBagBtw ws i j &&
toSlice zs 0 i == toSlice ws 0 i &&
toSlice zs j (A.size zs) == toSlice ws j (A.size zs) &&
i <= ip && ip < j }> / [jr - jl + 1] @-}
-- at return, all of ws[i:ip] <= ws[j-1] and all of ws[ip:j-1] > ws[j-1].
goShuffle zs jl jr = -- BOTH bounds inclusive here
if jl > jr
then (zs, jl)
else let (vl, zs') = A.get2 zs jl in
if vl <= piv
then goShuffle zs' (jl+1 ? lem_rangeProperty_build_right zs (belowPivot (get zs (j-1)))
i (jl ? toProof (belowPivot (get zs (j-1)) (get zs jl))))
jr
else let (vr, zs'') = A.get2 zs' jr in
if vr > piv
then goShuffle zs'' jl (jr-1)
else let zs''' = swap zs'' jl jr
? lem_range_outside_swap zs i jl jr (j-1) piv
? lma_swap zs jl jr
? lma_swap_eql zs jl jr (j-1)
? lem_bagBtw_swap zs i jl jr j
? lem_toSlice_swap zs i jl jr j
in goShuffle zs''' jl (jr-1)
{-@ goShuffle ::
{ jl:Int | i <= jl }
-> { jr:Int | jl <= jr+1 }
-> { zs:(Array a) | get zs (j-1) == piv && A.size zs == A.size xs &&
toBagBtw zs i j == toBagBtw xs i j &&
toSlice xs 0 i == toSlice zs 0 i &&
toSlice xs j (A.size zs) == toSlice zs j (A.size zs)

(xs', ip) = goShuffle xs1 i (j-2) -- BOTH bounds inclusive
{- @ xs'' :: { vs:(Array a) | isPartitionedBtw vs i ip j &&
toSlice xs' 0 i == toSlice vs 0 i &&
toSlice xs' j (A.size xs') == toSlice vs j (A.size xs') &&
A.size xs' == A.size vs &&
toBagBtw xs i j == toBagBtw vs i j } @-}
xs'' = if ip < j-1
then swap2 xs' ip (j-1) ? lma_swap xs' ip (j-1)
? lem_bagBtw_swap xs' i ip (j-1) j
? lem_range_inside_swap xs' ip (j-1)
? lem_range_outside_swap xs' i ip (j-1) j (get xs' (j-1))
? lem_toSlice_swap xs' i ip (j-1) j
&& rangeUpperBound zs i jl piv
&& jr < j-1 && rangeLowerBound zs (jr+1) (j-1) piv }
-> (Array a, Ur Int)<{\ws ip -> rangeUpperBound ws i (unur ip) piv &&
rangeLowerBound ws (unur ip) (j-1) piv &&
A.size ws == A.size zs &&
get ws (j-1) == get zs (j-1) &&
toBagBtw zs i j == toBagBtw ws i j &&
toBagBtw xs i j == toBagBtw ws i j &&
toSlice zs 0 i == toSlice ws 0 i &&
toSlice zs j (A.size zs) == toSlice ws j (A.size zs) &&
i <= unur ip && unur ip < j }> / [jr - jl + 1] @-}
-- at return, all of ws[i:ip] <= ws[j-1] and all of ws[ip:j-1] > ws[j-1].
goShuffle :: HasPrimOrd a => Int -> Int -> (Array a -. (Array a, Ur Int))
goShuffle jl jr zs = -- BOTH bounds inclusive here
if jl > jr
then (zs, Ur jl)
else A.get2 jl zs & \(Ur vl, zs') ->
if vl <= piv
then goShuffle (jl+1 ? lem_rangeProperty_build_right zs (belowPivot (get zs (j-1)))
i (jl ? toProof (belowPivot (get zs (j-1)) (get zs jl))))
jr zs'
else A.get2 jr zs' & \(Ur vr, zs'') ->
if vr > piv
then goShuffle jl (jr-1) zs''
else let zs''' = swap2 jl jr zs''
? lem_range_outside_swap zs i jl jr (j-1) piv
? lma_swap zs jl jr
? lma_swap_eql zs jl jr (j-1)
? lem_bagBtw_swap zs i jl jr j
? lem_toSlice_swap zs i jl jr j
in goShuffle jl (jr-1) zs''' in

goShuffle i (j-2) xs1 & \(xs', Ur ip) -> -- BOTH bounds inclusive
let
{- @ xs'' :: { vs:(Array a) | isPartitionedBtw vs i ip j &&
toSlice xs' 0 i == toSlice vs 0 i &&
toSlice xs' j (A.size xs') == toSlice vs j (A.size xs') &&
A.size xs' == A.size vs &&
toBagBtw xs i j == toBagBtw vs i j } @-}
xs'' = if ip < j-1
then swap2 ip (j-1) xs' ? lma_swap xs' ip (j-1)
? lem_bagBtw_swap xs' i ip (j-1) j
? lem_range_inside_swap xs' ip (j-1)
? lem_range_outside_swap xs' i ip (j-1) j (get xs' (j-1))
? lem_toSlice_swap xs' i ip (j-1) j
else xs'
in (xs'', ip)
in (xs'', Ur ip)
{-# INLINE shuffleBtw #-}
-- where

-- | This belongs in Equivalence.hs but causes a Fixpoint panic if it's there
Expand Down
Loading