Skip to content

Commit 013ff57

Browse files
jazullojazullo
committed
Construct Cilksort with reasonable parameters
1 parent e4f6b75 commit 013ff57

File tree

3 files changed

+144
-112
lines changed

3 files changed

+144
-112
lines changed

‎lh-array-sort.cabal‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -67,13 +67,9 @@ library
6767
PiecewiseFallbackSort
6868
PiecewiseFallbackSortPar
6969

70-
-- JZ: Add Parallel Cilksort
71-
-- Current Cilksort is entirely sequential
70+
QuickSortCilk
71+
CilkSort
7272

73-
-- remove until ready:
74-
-- QuickSortNew
75-
-- the last not quite ready yet?
76-
-- CilkSort
7773
Linear.Common
7874
other-modules:
7975
Array.List

‎src/CilkSort.hs‎

Lines changed: 58 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -6,24 +6,26 @@ module CilkSort where
66
import qualified Language.Haskell.Liquid.Bag as B
77
import Language.Haskell.Liquid.ProofCombinators hiding ((?))
88
import ProofCombinators
9-
import Array
9+
import Array as A
1010
import ArrayOperations
11-
import DpsMerge
11+
import DpsMergePar
12+
import qualified DpsMergeSort4 as Seq
1213
import Properties.Equivalence
1314
import Properties.Order
14-
import Insertion
1515
import QuickSortCilk
16+
import Par
1617

18+
import Linear.Common
1719
#ifdef MUTABLE_ARRAYS
1820
import Array.Mutable as A
21+
import Control.DeepSeq ( NFData(..) )
1922
#else
2023
import Array.List as A
2124
#endif
2225

2326
#define KILO 1024
24-
#define MERGESIZE (2*KILO)
25-
#define QUICKSIZE (2*KILO)
26-
#define INSERTIONSIZE 20
27+
#define QUICKSIZE (8*KILO)
28+
#define SEQSIZE (8*KILO)
2729

2830
-- DPS mergesort -- unfold twice, merge twice
2931
{-@ cilkSortInplace :: xs:Array a
@@ -35,51 +37,70 @@ import Array.List as A
3537
left zs == left xs && right zs == right xs &&
3638
left ts == left ys && right ts == right ys }>
3739
/ [A.size xs] @-}
38-
cilkSortInplace :: (Show a, Ord a) => A.Array a -> A.Array a -> (A.Array a, A.Array a)
40+
#ifdef MUTABLE_ARRAYS
41+
cilkSortInplace :: (Show a, HasPrimOrd a, NFData a) =>
42+
#else
43+
cilkSortInplace :: (Show a, HasPrimOrd a) =>
44+
#endif
45+
A.Array a -. A.Array a -. (A.Array a, A.Array a)
3946
cilkSortInplace src tmp =
40-
let (len, src') = A.size2 src in
41-
if len <= QUICKSIZE
42-
then let src'' = quickSort src'
43-
in (src'', tmp)
47+
let !(Ur len, src') = A.size2 src in
48+
if len <= SEQSIZE
49+
then
50+
if len <= QUICKSIZE
51+
then let src'' = quickSort src'
52+
in (src'', tmp)
53+
else Seq.msortInplace src' tmp
4454
else
45-
let (srcA, srcB) = splitMid src'
46-
(tmpA, tmpB) = splitMid tmp
47-
(src1, src2) = splitMid srcA
48-
(src3, src4) = splitMid srcB
49-
(tmp1, tmp2) = splitMid tmpA
50-
(tmp3, tmp4) = splitMid tmpB
51-
(src1', tmp1') = cilkSortInplace src1 tmp1
52-
(src2', tmp2') = cilkSortInplace src2 tmp2
53-
(src3', tmp3') = cilkSortInplace src3 tmp3
54-
(src4', tmp4') = cilkSortInplace src4 tmp4
55+
let !(srcA, srcB) = splitMid src'
56+
!(tmpA, tmpB) = splitMid tmp
57+
!(src1, src2) = splitMid srcA
58+
!(src3, src4) = splitMid srcB
59+
!(tmp1, tmp2) = splitMid tmpA
60+
!(tmp3, tmp4) = splitMid tmpB
61+
!(((src1', tmp1'), (src2', tmp2')), ((src3', tmp3'), (src4', tmp4')))
62+
= (.||||.) (cilkSortInplace src1 tmp1) (cilkSortInplace src2 tmp2)
63+
(cilkSortInplace src3 tmp3) (cilkSortInplace src4 tmp4)
5564
tmpA' = A.append tmp1' tmp2'
5665
tmpB' = A.append tmp3' tmp4'
57-
(srcA'', tmpA'') = merge src1' src2' tmpA'
58-
(srcB'', tmpB'') = merge src3' src4' tmpB'
66+
!((srcA'', tmpA''), (srcB'', tmpB''))
67+
= merge_par src1' src2' tmpA' .||. merge_par src3' src4' tmpB'
68+
-- = tuple2 (merge_par src1' src2') tmpA' (merge_par src3' src4') tmpB'
5969
src'' = A.append srcA'' srcB''
60-
(tmp''', src''') = merge tmpA'' tmpB'' src''
61-
in (src''', tmp''') ? lem_toBag_splitMid src
70+
!(tmp''', src''') = merge_par tmpA'' tmpB'' src''
71+
in (src''', tmp''') ? lem_toBag_splitMid src
6272
? lem_toBag_splitMid tmp
6373
? lem_toBag_splitMid srcA
6474
? lem_toBag_splitMid srcB
6575
? lem_toBag_splitMid tmpA
6676
? lem_toBag_splitMid tmpB
6777

68-
{-@ cilkSort' :: { xs:(Array a) | A.size xs > 0 && left xs == 0 && right xs == size xs }
69-
-> { y:a | y == A.get xs 0 }
70-
-> { zs:(Array a) | toBag xs == toBag zs && isSorted' zs &&
71-
A.size xs == A.size zs && token xs == token zs } @-}
72-
cilkSort' :: (Show a, Ord a) => A.Array a -> a -> A.Array a
73-
cilkSort' src anyVal =
74-
let (len, src') = A.size2 src
75-
(src'', _tmp) = cilkSortInplace src' (A.make len anyVal) in
76-
_tmp `seq` src''
78+
{-@ cilkSort' :: y:a
79+
-> { xs:(Array a) | A.size xs > 0 && left xs == 0 && right xs == size xs && y == A.get xs 0 }
80+
-> { zs:(Array a) | toBag xs == toBag zs && isSorted' zs &&
81+
A.size xs == A.size zs && token xs == token zs } @-}
82+
#ifdef MUTABLE_ARRAYS
83+
cilkSort' :: (Show a, HasPrimOrd a, NFData a) =>
84+
#else
85+
cilkSort' :: (Show a, HasPrimOrd a) =>
86+
#endif
87+
a -> A.Array a -. A.Array a
88+
cilkSort' anyVal src =
89+
let !(Ur len, src') = A.size2 src
90+
!src'' = A.allocScratch len anyVal cilkSortInplace src' in
91+
src''
7792

93+
-- finally, the top-level merge sort function
7894
{-@ cilkSort :: { xs:(A.Array a) | left xs == 0 && right xs == size xs }
7995
-> { ys:_ | toBag xs == toBag ys && isSorted' ys &&
8096
A.size xs == A.size ys && token xs == token ys } @-}
81-
cilkSort :: (Show a, Ord a) => A.Array a -> A.Array a
97+
#ifdef MUTABLE_ARRAYS
98+
cilkSort :: (Show a, HasPrimOrd a, NFData a) =>
99+
#else
100+
cilkSort :: (Show a, HasPrimOrd a) =>
101+
#endif
102+
A.Array a -. A.Array a
82103
cilkSort src =
83-
let (len, src') = A.size2 src in
104+
let !(Ur len, src') = A.size2 src in
84105
if len == 0 then src'
85-
else let (x0, src'') = A.get2 src' 0 in cilkSort' src'' x0
106+
else let !(Ur x0, src'') = A.get2 0 src' in cilkSort' x0 src''

‎src/QuickSortCilk.hs‎

Lines changed: 84 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ import Properties.RangeProperties
2020

2121
import Insertion
2222

23+
import Linear.Common
2324
#ifdef MUTABLE_ARRAYS
2425
import qualified Unsafe.Linear as Unsafe
2526
import Array.Mutable as A
@@ -41,27 +42,33 @@ import qualified Array as A
4142
{-@ quickSort :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
4243
toBag xs == toBag ys } @-}
4344
-- quickSort :: (Ord a, Show a) => Array a -> Array a
44-
quickSort :: (HasPrimOrd a, Show a) => Array a -> Array a
45+
quickSort :: (HasPrimOrd a, Show a) => Array a -. Array a
4546
quickSort xs =
46-
let (n, xs1) = A.size2 xs in
47+
let (Ur n, xs1) = A.size2 xs in
4748
if n == 0 then xs1
48-
else let (hd, xs2) = A.get2 xs1 0
49-
{-@ promise :: { tmp:(Array a) | size tmp == n }
50-
-> { out:(Ur (Array a)) | size (unur out) == n &&
51-
toSlice (unur out) 0 n == toSlice xs2 0 n} @-}
52-
promise tmp = Ur (A.copy xs2 0 tmp 0 n)
53-
? lem_copy_equal_slice xs2 0 tmp 0 n
54-
{- @ cpy :: { ys:(Array a) | size ys == n && toSlice ys 0 n == toSlice xs2 0 n } @-}
55-
Ur cpy = A.alloc n hd (Unsafe.toLinear promise)
56-
in quickSortBtw (cpy ? lem_equal_slice_bag xs2 cpy 0 n) 0 n
49+
else let (Ur hd, xs2) = A.get2 0 xs1
50+
tmp = makeArray n hd in
51+
A.copy2 0 0 n xs2 tmp ? lem_copy_equal_slice xs2 0 tmp 0 n & \(xs2', cpy0) ->
52+
(A.free(xs2'), cpy0) & \((), cpy) ->
53+
quickSortBtw 0 n (cpy ? lem_equal_slice_bag xs2 cpy 0 n)
54+
{-# INLINABLE quickSort #-}
55+
56+
{-@ quickSort' :: xs:(Array a) -> { ys:(Array a) | isSorted' ys && A.size xs == A.size ys &&
57+
toBag xs == toBag ys } @-}
58+
quickSort' :: (HasPrimOrd a, Show a) => Array a -. Array a
59+
quickSort' xs =
60+
let (Ur n, xs1) = A.size2 xs in
61+
if n == 0 then xs1
62+
else quickSortBtw 0 n xs1
63+
{-# INLINABLE quickSort' #-}
5764

5865
{-@ quickSortBtw :: xs:(Array a) -> { i:Int | 0 <= i } -> { j:Int | i <= j && j <= A.size xs }
5966
-> { ys:(Array a) | isSortedBtw ys i j && A.size xs == A.size ys &&
6067
toSlice xs 0 i == toSlice ys 0 i &&
6168
toSlice xs j (A.size xs) == toSlice ys j (A.size xs) &&
6269
toBagBtw xs i j == toBagBtw ys i j } / [j - i] @-}
63-
quickSortBtw :: HasPrimOrd a => Array a -> Int -> Int -> Array a
64-
quickSortBtw xs i j =
70+
quickSortBtw :: HasPrimOrd a => Int -> Int -> (Array a -. Array a)
71+
quickSortBtw i j xs =
6572
if j - i < 2 then xs else
6673
if j - i <= INSERTIONSIZE
6774
then let (xs_l, xs_cr) = A.splitAt i xs
@@ -101,9 +108,9 @@ quickSortBtw xs i j =
101108
? lem_toSlice_slice xs i (A.size xs) (j-i) (A.size xs - i)
102109
=== toSlice xs j (A.size xs)
103110
)
104-
else let (xs', i_piv) = shuffleBtw xs i j -- isPartitionedBtw xs' i i_piv j
105-
xs'' = quickSortBtw xs' i i_piv
106-
xs''' = quickSortBtw xs'' (i_piv + 1) j
111+
else let (xs', Ur i_piv) = shuffleBtw i j xs
112+
xs'' = quickSortBtw i i_piv xs'
113+
xs''' = quickSortBtw (i_piv + 1) j xs''
107114
? lem_qs_pres_partition_left xs' xs'' i i_piv j
108115
in xs''' ? lem_sorted_partitions xs''' i i_piv (j
109116
? lem_equal_slice_sorted xs'' xs''' 0 i i_piv (i_piv+1)
@@ -116,66 +123,74 @@ quickSortBtw xs i j =
116123
? lem_equal_slice_bag xs'' xs''' i (i_piv+1)
117124
? lem_toBagBtw_compose xs' xs'' i i_piv j
118125
? lem_toBagBtw_compose xs'' xs''' i (i_piv+1) j
126+
{-# INLINE quickSortBtw #-}
119127

120-
{-@ shuffleBtw :: xs:(Array a) -> { i:Int | 0 <= i } -> { j:Int | i + 1 < j && j <= A.size xs }
121-
-> (Array a, Int)<{\ys ip -> isPartitionedBtw ys i ip j &&
128+
{-@ shuffleBtw :: { i:Int | 0 <= i } -> j:Int -> { xs:(Array a) | i + 1 < j && j <= A.size xs }
129+
-> (Array a, Ur Int)<{\ys ip -> isPartitionedBtw ys i (unur ip) j &&
122130
toSlice xs 0 i == toSlice ys 0 i &&
123131
toSlice xs j (A.size xs) == toSlice ys j (A.size xs) &&
124132
toBagBtw xs i j == toBagBtw ys i j &&
125-
i <= ip && ip < j && A.size ys == A.size xs }> @-}
126-
shuffleBtw :: HasPrimOrd a => Array a -> Int -> Int -> (Array a, Int)
127-
shuffleBtw xs i j =
133+
i <= unur ip && unur ip < j && A.size ys == A.size xs }> @-}
134+
135+
shuffleBtw :: forall a. HasPrimOrd a => Int -> Int -> (Array a -. (Array a, Ur Int))
136+
shuffleBtw i j xs = xs & A.get2 (j-1) {- fix (j-1)^th element as the pivot -} & \(Ur piv, xs1) ->
128137
let
129-
(piv, xs1) = A.get2 xs (j-1) -- fix xs[j-1] as the pivot
130-
{-@ goShuffle :: { zs:(Array a) | get zs (j-1) == piv && A.size zs == A.size xs &&
131-
toBagBtw zs i j == toBagBtw xs i j &&
132-
toSlice xs 0 i == toSlice zs 0 i &&
133-
toSlice xs j (A.size zs) == toSlice zs j (A.size zs)}
134-
-> { jl:Int | i <= jl && rangeUpperBound zs i jl piv }
135-
-> { jr:Int | jl <= jr+1 && jr < j-1 && rangeLowerBound zs (jr+1) (j-1) piv }
136-
-> (Array a, Int)<{\ws ip -> rangeUpperBound ws i ip piv &&
137-
rangeLowerBound ws ip (j-1) piv &&
138-
A.size ws == A.size zs &&
139-
get ws (j-1) == get zs (j-1) &&
140-
toBagBtw zs i j == toBagBtw ws i j &&
141-
toBagBtw xs i j == toBagBtw ws i j &&
142-
toSlice zs 0 i == toSlice ws 0 i &&
143-
toSlice zs j (A.size zs) == toSlice ws j (A.size zs) &&
144-
i <= ip && ip < j }> / [jr - jl + 1] @-}
145-
-- at return, all of ws[i:ip] <= ws[j-1] and all of ws[ip:j-1] > ws[j-1].
146-
goShuffle zs jl jr = -- BOTH bounds inclusive here
147-
if jl > jr
148-
then (zs, jl)
149-
else let (vl, zs') = A.get2 zs jl in
150-
if vl <= piv
151-
then goShuffle zs' (jl+1 ? lem_rangeProperty_build_right zs (belowPivot (get zs (j-1)))
152-
i (jl ? toProof (belowPivot (get zs (j-1)) (get zs jl))))
153-
jr
154-
else let (vr, zs'') = A.get2 zs' jr in
155-
if vr > piv
156-
then goShuffle zs'' jl (jr-1)
157-
else let zs''' = swap zs'' jl jr
158-
? lem_range_outside_swap zs i jl jr (j-1) piv
159-
? lma_swap zs jl jr
160-
? lma_swap_eql zs jl jr (j-1)
161-
? lem_bagBtw_swap zs i jl jr j
162-
? lem_toSlice_swap zs i jl jr j
163-
in goShuffle zs''' jl (jr-1)
138+
{-@ goShuffle ::
139+
{ jl:Int | i <= jl }
140+
-> { jr:Int | jl <= jr+1 }
141+
-> { zs:(Array a) | get zs (j-1) == piv && A.size zs == A.size xs &&
142+
toBagBtw zs i j == toBagBtw xs i j &&
143+
toSlice xs 0 i == toSlice zs 0 i &&
144+
toSlice xs j (A.size zs) == toSlice zs j (A.size zs)
164145

165-
(xs', ip) = goShuffle xs1 i (j-2) -- BOTH bounds inclusive
166-
{- @ xs'' :: { vs:(Array a) | isPartitionedBtw vs i ip j &&
167-
toSlice xs' 0 i == toSlice vs 0 i &&
168-
toSlice xs' j (A.size xs') == toSlice vs j (A.size xs') &&
169-
A.size xs' == A.size vs &&
170-
toBagBtw xs i j == toBagBtw vs i j } @-}
171-
xs'' = if ip < j-1
172-
then swap2 xs' ip (j-1) ? lma_swap xs' ip (j-1)
173-
? lem_bagBtw_swap xs' i ip (j-1) j
174-
? lem_range_inside_swap xs' ip (j-1)
175-
? lem_range_outside_swap xs' i ip (j-1) j (get xs' (j-1))
176-
? lem_toSlice_swap xs' i ip (j-1) j
146+
&& rangeUpperBound zs i jl piv
147+
&& jr < j-1 && rangeLowerBound zs (jr+1) (j-1) piv }
148+
-> (Array a, Ur Int)<{\ws ip -> rangeUpperBound ws i (unur ip) piv &&
149+
rangeLowerBound ws (unur ip) (j-1) piv &&
150+
A.size ws == A.size zs &&
151+
get ws (j-1) == get zs (j-1) &&
152+
toBagBtw zs i j == toBagBtw ws i j &&
153+
toBagBtw xs i j == toBagBtw ws i j &&
154+
toSlice zs 0 i == toSlice ws 0 i &&
155+
toSlice zs j (A.size zs) == toSlice ws j (A.size zs) &&
156+
i <= unur ip && unur ip < j }> / [jr - jl + 1] @-}
157+
-- at return, all of ws[i:ip] <= ws[j-1] and all of ws[ip:j-1] > ws[j-1].
158+
goShuffle :: HasPrimOrd a => Int -> Int -> (Array a -. (Array a, Ur Int))
159+
goShuffle jl jr zs = -- BOTH bounds inclusive here
160+
if jl > jr
161+
then (zs, Ur jl)
162+
else A.get2 jl zs & \(Ur vl, zs') ->
163+
if vl <= piv
164+
then goShuffle (jl+1 ? lem_rangeProperty_build_right zs (belowPivot (get zs (j-1)))
165+
i (jl ? toProof (belowPivot (get zs (j-1)) (get zs jl))))
166+
jr zs'
167+
else A.get2 jr zs' & \(Ur vr, zs'') ->
168+
if vr > piv
169+
then goShuffle jl (jr-1) zs''
170+
else let zs''' = swap2 jl jr zs''
171+
? lem_range_outside_swap zs i jl jr (j-1) piv
172+
? lma_swap zs jl jr
173+
? lma_swap_eql zs jl jr (j-1)
174+
? lem_bagBtw_swap zs i jl jr j
175+
? lem_toSlice_swap zs i jl jr j
176+
in goShuffle jl (jr-1) zs''' in
177+
178+
goShuffle i (j-2) xs1 & \(xs', Ur ip) -> -- BOTH bounds inclusive
179+
let
180+
{- @ xs'' :: { vs:(Array a) | isPartitionedBtw vs i ip j &&
181+
toSlice xs' 0 i == toSlice vs 0 i &&
182+
toSlice xs' j (A.size xs') == toSlice vs j (A.size xs') &&
183+
A.size xs' == A.size vs &&
184+
toBagBtw xs i j == toBagBtw vs i j } @-}
185+
xs'' = if ip < j-1
186+
then swap2 ip (j-1) xs' ? lma_swap xs' ip (j-1)
187+
? lem_bagBtw_swap xs' i ip (j-1) j
188+
? lem_range_inside_swap xs' ip (j-1)
189+
? lem_range_outside_swap xs' i ip (j-1) j (get xs' (j-1))
190+
? lem_toSlice_swap xs' i ip (j-1) j
177191
else xs'
178-
in (xs'', ip)
192+
in (xs'', Ur ip)
193+
{-# INLINE shuffleBtw #-}
179194
-- where
180195

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

0 commit comments

Comments
 (0)