Skip to content

Add missing INLIN(ABL)E in the parallel-merge code #21

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

Merged
merged 1 commit into from
Apr 2, 2025
+191 −130
Merged

Add missing INLIN(ABL)E in the parallel-merge code #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
20 changes: 11 additions & 9 deletions .github/workflows/build-test-linear.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,12 +145,14 @@ jobs:
- name: Make sure benchrunner builds and runs
run: |
cabal build benchrunner
cabal run benchrunner -- 5 Insertionsort Seq 100
cabal run benchrunner -- 5 Mergesort Seq 100
cabal run benchrunner -- 5 Mergesort Par 100 +RTS -N2
cabal run benchrunner -- 5 "VectorSort Insertionsort" Seq 100
cabal run benchrunner -- 5 "VectorSort Mergesort" Seq 100
cabal run benchrunner -- 5 "VectorSort Quicksort" Seq 100
cabal run benchrunner -- 5 "CSort Insertionsort" Seq 100
cabal run benchrunner -- 5 "CSort Mergesort" Seq 100
cabal run benchrunner -- 5 "CSort Quicksort" Seq 100
cabal run benchrunner -- 5 Insertionsort Seq 1000
cabal run benchrunner -- 5 Quicksort Seq 1000
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 "VectorSort Insertionsort" Seq 1000
cabal run benchrunner -- 5 "VectorSort Mergesort" Seq 1000
cabal run benchrunner -- 5 "VectorSort Quicksort" Seq 1000
cabal run benchrunner -- 5 "CSort Insertionsort" Seq 1000
cabal run benchrunner -- 5 "CSort Mergesort" Seq 1000
cabal run benchrunner -- 5 "CSort Quicksort" Seq 1000
3 changes: 3 additions & 0 deletions src/Array.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,7 @@ generate_loop arr idx end f =
copy2_par :: HasPrim a => Int -> Int -> Int -> Array a -. Array a -. (Array a, Array a)
copy2_par src_offset0 dst_offset0 len0 =
Unsafe.toLinear (\src0 -> Unsafe.toLinear (\dst0 -> (src0, copy_par src0 src_offset0 dst0 dst_offset0 len0)))
{-# INLINABLE copy2_par #-}

--TODO: src_offset0 and dst_offset0 are not respected.
{- @ ignore copy_par @-}
Expand All @@ -205,6 +206,7 @@ copy_par src0 src_offset0 dst0 dst_offset0 len0 = copy_par' src0 src_offset0 dst
#else
copy_par src0 src_offset0 dst0 dst_offset0 len0 = copy src0 src_offset0 dst0 dst_offset0 len0
#endif
{-# INLINABLE copy_par #-}

--TODO: src_offset0 and dst_offset0 are not respected.
{-@ ignore copy_par_m @-}
Expand All @@ -223,6 +225,7 @@ copy_par_m !src0 src_offset0 !dst0 dst_offset0 !len0 = copy_par_m' src0 src_offs
!right <- copy_par_m' src_r 0 dst_r 0 (len-half)
!left <- P.get left_f
pure $ append left right
{-# INLINABLE copy_par_m #-}

-- {-@ ignore foldl1_par @-}
-- foldl1_par :: Int -> (a -> a -> a) -> a -> Array a -> a
Expand Down
5 changes: 3 additions & 2 deletions src/Array/Mutable.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE BangPatterns #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

-- The Strict pragma is not just for performance, it's necessary for correctness.
-- Without it, this implementation contains a bug related to some thunk/effect
Expand Down Expand Up @@ -146,8 +147,8 @@ splitAt m = Unsafe.toLinear (\xs -> (slice xs 0 m, slice xs m (size xs)))
append :: Array a -. Array a -. Array a
append xs ys =
let !res = Unsafe.toLinear (\xs -> case xs of
(Array l1 _r1 !a1) -> Unsafe.toLinear (\ys -> case ys of
(Array _l2 r2 _a2) -> Array l1 r2 a1)) xs ys
(Array !l1 _r1 !a1) -> Unsafe.toLinear (\ys -> case ys of
(Array _l2 !r2 _a2) -> Array l1 r2 a1)) xs ys
in res

-- token xs == token ys
Expand Down
143 changes: 80 additions & 63 deletions src/DpsMergePar.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

module DpsMergePar where

import qualified Language.Haskell.Liquid.Bag as B
Expand Down Expand Up @@ -349,72 +351,89 @@ merge_par' :: (Show a, HasPrimOrd a, NFData a) =>
merge_par' :: (Show a, HasPrimOrd a) =>
#endif
A.Array a -. (A.Array a -. (A.Array a -. ((A.Array a, A.Array a), A.Array a)))
merge_par' !src1 !src2 !dst =
let !(Ur n3, dst') = A.size2 dst in
if n3 < goto_seqmerge
then merge' 0 0 0 src1 src2 dst'
? toProof (merge_par_func src1 src2 dst === merge_func src1 src2 dst 0 0 0)
else let !(Ur n1, src1') = A.size2 src1
!(Ur n2, src2') = A.size2 src2
in if n1 == 0
then let !(src2'1, dst'') = A.copy2_par 0 0 n2 src2' dst'
in ((src1', src2'1), dst'')
else if n2 == 0
then let !(src1'1, dst'') = A.copy2_par 0 0 n1 src1' dst'
in ((src1'1, src2'), dst'')
else let mid1 = n1 `div` 2
!(Ur pivot, src1'1) = A.get2 mid1 src1'
!(Ur mid2, src2'1) = binarySearch pivot src2' -- src2[mid2] must <= all src1[mid1+1..]
-- must >= all src1[0..mid1]
!(src1_l, src1_cr) = A.splitAt mid1 src1'1
!(src1_c, src1_r) = A.splitAt 1 src1_cr
!(src2_l, src2_r) = A.splitAt mid2 src2'1

!(dst_l, dst_cr) = A.splitAt (mid1+mid2) dst'
!(dst_c, dst_r) = A.splitAt 1 dst_cr
!dst_c' = A.setLin 0 pivot dst_c

!(((src1_l',src2_l'), dst_l'), ((src1_r',src2_r'), dst_r'))
= (merge_par' src1_l src2_l dst_l) .||. (merge_par' src1_r src2_r dst_r)
{-
(left, right) = tuple2 (merge_par' src1_l src2_l) dst_l
-- ( ( (src1_l ? lem_isSortedBtw_slice src1'1 0 mid1)
-- , (src2_l ? lem_isSortedBtw_slice src2'1 0 mid2) )
-- , dst_l )
(merge_par' src1_r src2_r) dst_r
-- ( ( (src1_r ? lem_isSortedBtw_slice src1'1 mid1 n1
-- ? lem_isSortedBtw_slice src1_cr 1 (n1-mid1))
-- , (src2_r ? lem_isSortedBtw_slice src2'1 mid2 n2) )
-- , dst_r )
-}
!src1_cr' = A.append src1_c src1_r'
!src1'3 = A.append src1_l' src1_cr'
!src2'3 = A.append src2_l' src2_r'
!dst'' = A.append dst_l' dst_c'
!dst''' = A.append dst'' dst_r'
in ((src1'3, src2'3), dst''')
merge_par' !src1 !src2 !dst = go src1 src2 dst where
{-@ go :: xs1:(Array a) -> { xs2:(Array a) | token xs1 == token xs2 }
-> { zs :(Array a) | size xs1 + size xs2 == size zs }
-> { t:_ | snd t == merge_par_func xs1 xs2 zs &&
token (fst (fst t)) == token xs1 && token (snd (fst t)) == token xs2 &&
left (fst (fst t)) == left xs1 && right (fst (fst t)) == right xs1 &&
left (snd (fst t)) == left xs2 && right (snd (fst t)) == right xs2 &&
size (snd t) == size zs && token (snd t) == token zs &&
left (snd t) == left zs && right (snd t) == right zs } / [size xs1] @-}
#ifdef MUTABLE_ARRAYS
go :: (Show a, HasPrimOrd a, NFData a) =>
#else
go :: (Show a, HasPrimOrd a) =>
#endif
A.Array a -. (A.Array a -. (A.Array a -. ((A.Array a, A.Array a), A.Array a)))
go src1 src2 dst =
let !(Ur n3, dst') = A.size2 dst in
if n3 < goto_seqmerge
then merge' 0 0 0 src1 src2 dst'
? toProof (merge_par_func src1 src2 dst === merge_func src1 src2 dst 0 0 0)
else let !(Ur n1, src1') = A.size2 src1
!(Ur n2, src2') = A.size2 src2
in if n1 == 0
then let !(src2'1, dst'') = A.copy2_par 0 0 n2 src2' dst'
in ((src1', src2'1), dst'')
else if n2 == 0
then let !(src1'1, dst'') = A.copy2_par 0 0 n1 src1' dst'
in ((src1'1, src2'), dst'')
else let mid1 = n1 `div` 2
!(Ur pivot, src1'1) = A.get2 mid1 src1'
!(Ur mid2, src2'1) = binarySearch pivot src2' -- src2[mid2] must <= all src1[mid1+1..]
-- must >= all src1[0..mid1]
!(src1_l, src1_cr) = A.splitAt mid1 src1'1
!(src1_c, src1_r) = A.splitAt 1 src1_cr
!(src2_l, src2_r) = A.splitAt mid2 src2'1

!(dst_l, dst_cr) = A.splitAt (mid1+mid2) dst'
!(dst_c, dst_r) = A.splitAt 1 dst_cr
!dst_c' = A.setLin 0 pivot dst_c

!(((src1_l',src2_l'), dst_l'), ((src1_r',src2_r'), dst_r'))
= (go src1_l src2_l dst_l) .||. (go src1_r src2_r dst_r)
{-
(left, right) = tuple2 (merge_par' src1_l src2_l) dst_l
-- ( ( (src1_l ? lem_isSortedBtw_slice src1'1 0 mid1)
-- , (src2_l ? lem_isSortedBtw_slice src2'1 0 mid2) )
-- , dst_l )
(merge_par' src1_r src2_r) dst_r
-- ( ( (src1_r ? lem_isSortedBtw_slice src1'1 mid1 n1
-- ? lem_isSortedBtw_slice src1_cr 1 (n1-mid1))
-- , (src2_r ? lem_isSortedBtw_slice src2'1 mid2 n2) )
-- , dst_r )
-}
!src1_cr' = A.append src1_c src1_r'
!src1'3 = A.append src1_l' src1_cr'
!src2'3 = A.append src2_l' src2_r'
!dst'' = A.append dst_l' dst_c'
!dst''' = A.append dst'' dst_r'
in ((src1'3, src2'3), dst''')
{-# INLINE merge_par' #-}

{-@ binarySearch :: query:_ -> ls:_
-> { tup:_ | 0 <= unur (fst tup) && unur (fst tup) <= size ls &&
snd tup == ls && (unur (fst tup), snd tup) = (binarySearch_func ls query, ls) } @-}
binarySearch :: HasPrimOrd a => a -> A.Array a -. (Ur Int, A.Array a) -- must be able to return out of bounds
binarySearch query ls = let !(Ur n, ls') = A.size2 ls
in binarySearch' query 0 n ls'

{-@ binarySearch' :: query:_ -> lo:Nat
-> { hi:Nat | lo <= hi }
-> { ls:_ | hi <= size ls }
-> { tup:_ | 0 <= unur (fst tup) && unur (fst tup) <= size ls &&
snd tup == ls &&
(unur (fst tup), snd tup) = (binarySearch_func' ls query lo hi, ls) } / [hi-lo] @-}
binarySearch' :: HasPrimOrd a => a -> Int -> Int -> A.Array a -. (Ur Int, A.Array a)
binarySearch' query lo hi ls = if lo == hi
then (Ur lo, ls)
else let mid = lo + (hi - lo) `div` 2
!(Ur midElt, ls') = A.get2 mid ls
in if query < midElt
then binarySearch' query lo mid ls'
else binarySearch' query (mid+1) hi ls'
in binarySearch' query 0 n ls' where

{-@ binarySearch' :: query:_ -> lo:Nat
-> { hi:Nat | lo <= hi }
-> { ls:_ | hi <= size ls }
-> { tup:_ | 0 <= unur (fst tup) && unur (fst tup) <= size ls &&
snd tup == ls &&
(unur (fst tup), snd tup) = (binarySearch_func' ls query lo hi, ls) } / [hi-lo] @-}
binarySearch' :: HasPrimOrd a => a -> Int -> Int -> A.Array a -. (Ur Int, A.Array a)
binarySearch' query lo hi ls = if lo == hi
then (Ur lo, ls)
else let mid = lo + (hi - lo) `div` 2
!(Ur midElt, ls') = A.get2 mid ls
in if query < midElt
then binarySearch' query lo mid ls'
else binarySearch' query (mid+1) hi ls'
{-# INLINE binarySearch #-}

{-@ merge_par :: { xs1:(Array a) | isSorted' xs1 }
-> { xs2:(Array a) | isSorted' xs2 && token xs1 == token xs2 && right xs1 == left xs2 }
Expand All @@ -426,9 +445,6 @@ binarySearch' query lo hi ls = if lo == hi
left (snd t) == left zs && right (snd t) == right zs &&
size (fst t) == size xs1 + size xs2 &&
size (snd t) == size zs } / [size xs1] @-}
{-# INLINE merge_par #-}
{-# SPECIALISE merge_par :: A.Array Float -. A.Array Float -. A.Array Float -. (A.Array Float, A.Array Float) #-}
{-# SPECIALISE merge_par :: A.Array Int -. A.Array Int -. A.Array Int -. (A.Array Int, A.Array Int) #-}
#ifdef MUTABLE_ARRAYS
merge_par :: (Show a, HasPrimOrd a, NFData a) =>
#else
Expand All @@ -441,3 +457,4 @@ merge_par !src1 !src2 !dst =
in (src', dst')
? lem_merge_par_func_sorted src1 src2 dst
? lem_merge_par_func_equiv src1 src2 dst
{-# INLINABLE merge_par #-}
62 changes: 38 additions & 24 deletions src/DpsMergeParSeqFallback.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

module DpsMergeParSeqFallback where

import qualified Language.Haskell.Liquid.Bag as B
Expand Down Expand Up @@ -247,25 +249,41 @@ merge' :: HasPrimOrd a =>
Int -> Int -> Int ->
A.Array a -. A.Array a -. A.Array a -.
((A.Array a, A.Array a), A.Array a)
merge' i1 i2 j !src1 !src2 !dst =
let !(Ur len1, src1') = A.size2 src1
!(Ur len2, src2') = A.size2 src2 in
if i1 >= len1
then
let !(src2'1, dst') = A.copy2_par i2 j (len2-i2) src2' dst in ((src1', src2'1), dst')
else if i2 >= len2
then
let !(src1'1, dst') = A.copy2_par i1 j (len1-i1) src1' dst in ((src1'1, src2'), dst')
else
let !(Ur v1, src1'1) = A.get2 i1 src1'
!(Ur v2, src2'1) = A.get2 i2 src2' in
if v1 < v2
then let dst' = A.setLin j v1 dst
!(src_tup, dst'') = merge' (i1 + 1) i2 (j + 1) src1'1 src2'1 dst' in
(src_tup, dst'')
else let dst' = A.setLin j v2 dst
!(src_tup, dst'') = merge' i1 (i2 + 1) (j + 1) src1'1 src2'1 dst' in
(src_tup, dst'')
merge' i1 i2 j !src1 !src2 !dst = go i1 i2 j src1 src2 dst where
{-@ go :: i1:Nat -> i2:Nat -> { j:Nat | i1 + i2 == j }
-> { xs1:(Array a) | i1 <= size xs1 }
-> { xs2:(Array a) | token xs1 == token xs2 && i2 <= size xs2 }
-> { zs:(Array a) | size xs1 + size xs2 == size zs && j <= size zs }
-> { t:_ | t == ((xs1, xs2), merge_func xs1 xs2 zs i1 i2 j) &&
token (fst (fst t)) == token xs1 && token (snd (fst t)) == token xs2 &&
left (fst (fst t)) == left xs1 && right (fst (fst t)) == right xs1 &&
left (snd (fst t)) == left xs2 && right (snd (fst t)) == right xs2 &&
size (snd t) == size zs && token (snd t) == token zs &&
left (snd t) == left zs && right (snd t) == right zs } / [size zs - j] @-}
go :: HasPrimOrd a =>
Int -> Int -> Int ->
A.Array a -. A.Array a -. A.Array a -.
((A.Array a, A.Array a), A.Array a)
go !i1 !i2 !j src1 src2 dst =
let !(Ur len1, !src1') = A.size2 src1
!(Ur len2, !src2') = A.size2 src2 in
if i1 >= len1
then
let !(src2'1, dst') = A.copy2_par i2 j (len2-i2) src2' dst in ((src1', src2'1), dst')
else if i2 >= len2
then
let !(src1'1, dst') = A.copy2_par i1 j (len1-i1) src1' dst in ((src1'1, src2'), dst')
else
let !(Ur v1, !src1'1) = A.get2 i1 src1'
!(Ur v2, !src2'1) = A.get2 i2 src2' in
if v1 < v2
then let !dst' = A.setLin j v1 dst
!(src_tup, dst'') = go (i1 + 1) i2 (j + 1) src1'1 src2'1 dst' in
(src_tup, dst'')
else let !dst' = A.setLin j v2 dst
!(src_tup, dst'') = go i1 (i2 + 1) (j + 1) src1'1 src2'1 dst' in
(src_tup, dst'')
{-# INLINE merge' #-}

{-@ merge :: { xs1:(Array a) | isSorted' xs1 }
-> { xs2:(Array a) | isSorted' xs2 && token xs1 == token xs2 }
Expand All @@ -278,12 +296,8 @@ merge' i1 i2 j !src1 !src2 !dst =
left (snd (fst t)) == left xs2 && right (snd (fst t)) == right xs2 &&
left (snd t) == left zs && right (snd t) == right zs &&
size (snd t) == size zs } @-}
{-# INLINE merge #-}
{-# SPECIALISE merge :: A.Array Float -. A.Array Float -. A.Array Float
-. ((A.Array Float, A.Array Float), A.Array Float) #-}
{-# SPECIALISE merge :: A.Array Int -. A.Array Int -. A.Array Int
-. ((A.Array Int, A.Array Int), A.Array Int) #-}
merge :: HasPrimOrd a => A.Array a -. A.Array a -. A.Array a -. ((A.Array a, A.Array a), A.Array a)
merge src1 src2 dst = merge' 0 0 0 src1 src2 dst -- the 0's are relative to the current
? lem_merge_func_sorted src1 src2 dst 0 0 0 -- slices, not absolute indices
? lem_merge_func_equiv src1 src2 dst 0 0 0
{-# INLINABLE merge #-}
Loading