\documentclass[online,helvetica]{chaksem} % 15 slides \usepackage[]{graphicx} \usepackage{haskell} \usepackage{amsmath} \usepackage{url} \usepackage{amsfonts,amssymb} \newcommand{\spair}{\mathrel{{:}{*}{:}}} \newcommand{\typeind}[1]{\langle#1\rangle} \newcommand{\scheme}[3]{% \forall{}~#1~.\\~~{#2}~\mapsto\\~~~~{#3}} % how to preserve space? \newcommand{\RULE}[4]{\begin{haskell}\typeind{#1}~\scheme{#2}{#3}{#4}\end{haskell}} \begin{document} \begin{slide} \begin{center} \vspace*{-.9\bigskipamount} \vspace*{\fill} \Large{\dblue Rewriting Haskell Strings}\\ \par\vfill \begin{figure}[htbp] \begin{center} \includegraphics[scale=0.51]{images/bytestring.eps} \end{center} \end{figure} \vspace*{1\bigskipamount} \footnotesize \begin{center} \begin{tabular}{cc} Don Stewart & Duncan Coutts \\ \texttt{dons@cse.unsw.edu.au} & \texttt{duncan.coutts@comlab.ox.ac.uk} \\ \includegraphics[scale=0.3]{images/pls-icon.ps} {\dblue Programming Languages and Systems} & {\dblue Programming Tools Group}\\ {\dblue University of New South Wales} & {\dblue Oxford University}\\ \end{tabular} \\ \end{center} \end{center} \par\vfill \end{slide} % Part 1. % % Motivation: slow strings % Solution: arrays % % Problem: no lazy operation, no infinite data structures % Solution: lazy lists of arrays % % Improving performance: deforestation via rewriting % Further improvements: % - down loops % - maps and folds % % Results % - speed up % - allocations % % ------------------------------------------ % % Part 2. % % Maintaining it all: QuickCheck % % Overview of QuickCheck % % Checking rewrite rules % % QuickCheck as a model checker % - list versus bytestring versus lazy bytestring % % ------------------------------------------ % % Motivation: \begin{slide} \heading{IO in Haskell} \subheading{Lazy Haskell IO can be beautiful} {\small \begin{verbatim} main = print . sum . map read . lines =<< getContents \end{verbatim} } \begin{second} \subheading{But naive code can be slow} {\small \begin{verbatim} $ time ./string < in 1280000 ./string < in 44.32s user 96% cpu 46.045 total \end{verbatim} } \end{second} \end{slide} \begin{slide} \heading{And entirely unlike C} {\footnotesize \begin{verbatim} #include #include #define MAXLINELEN 128 int main() { int sum = 0; char line[MAXLINELEN]; while (fgets(line, MAXLINELEN, stdin)) { sum += atoi(line); } printf("%d\n", sum); return(0); } \end{verbatim} } The C entry for the 'sum' benchmark in the Great Language Shootout. \end{slide} \begin{slide} \heading{And entirely unlike C} {\small \begin{verbatim} $ time ./c < in 1280000 ./c < in 0.68s user 98% cpu 0.700 total \end{verbatim} } \dgreen{What can we do to improve the situation?} \end{slide} \begin{slide} \heading{Strings in Haskell} \subheading{The problem is the String type} {\small \begin{verbatim} data [] a = [] | a : [a] type String = [Char] \end{verbatim} } A lovely recursive type, defining a recursive structure. Excellent for inductive definitions: {\small \begin{verbatim} f [] = 0 f (_:xs) = 1 + f xs \end{verbatim} } \end{slide} \begin{slide} \heading{Strings in Haskell} However, this means strings are represented as linked lists of pointers to chars. \begin{center} \begin{figure}[htbp] \includegraphics[scale=0.7]{images/list.eps} \end{figure} \end{center} So every node requires an indirection, and another to retrieve character. Bad for the cache, bad for gcc, bad for performance. Usually the compiler can recover some performance, using strictness analysis, or lazyness. \end{slide} \begin{slide} \heading{The solution: packed strings} Our hardware is tuned to handling flat, packed byte arrays. So we take the hint: {\small \begin{verbatim} data ByteString = PS (ForeignPtr Word8) Int Int \end{verbatim} } Represent a string as a single pointer to a flat byte array, caching the length and an offset. \begin{center} \begin{figure}[htbp] \includegraphics[scale=0.7]{images/packed.eps} \end{figure} \end{center} \end{slide} \begin{slide} \heading{Performance} {\footnotesize \begin{verbatim} main = print . sum . map readInt . lines =<< getContents \end{verbatim} } \begin{second} \subheading{Within 10\% of C, with the same `naive' code} {\footnotesize \begin{verbatim} $ time ./packed < in 1280000 ./packed < in 0.66s user 98% cpu 0.773 total \end{verbatim} } \end{second} \end{slide} \begin{slide} \heading{Performance continued.} In fact, by further tuning the 'read' function, we can get as low as: {\small \begin{verbatim} $ time ./tuned < in 1280000 ./tuned < in 0.17s user 0.06s system 91% cpu 0.256 total \end{verbatim} } {\dgreen 3 times faster than the C entry, with gcc -O2} \end{slide} \begin{slide} \heading{Lists versus packed string performance} \begin{center} \begin{figure}[htbp] \includegraphics[angle=-90,scale=0.3]{images/list_v_bytestring.eps} \end{figure} \end{center} Our implementation of packed strings (red) is faster across the entire list api (each tic on the x axis is a function). \end{slide} % ------------------------------------------------------- \begin{slide} \heading{Writing packed string functions} \end{slide} \begin{slide} \heading{List functions are easy} \subheading{Writing packed string functions is a bit more work} {\small \begin{verbatim} head :: ByteString -> Word8 head (PS x s l) | l <= 0 = errorEmptyList "head" | otherwise = inlinePerformIO $ withForeignPtr x $ \p -> peekByteOff p s \end{verbatim} } Pointers have to be dereferenced, and `peeked'. Arrays have to be manually copied. A lot more work for the library author. \end{slide} \begin{slide} \heading{User's view of the library} However, users see just a drop-in replacement for the list interface: {\footnotesize \begin{verbatim} ByteString, -- abstract, Eq, Ord, Show, Read, Typeable, Monoid empty, -- :: ByteString singleton, -- :: Char -> ByteString cons, -- :: Char -> ByteString -> ByteString head, -- :: ByteString -> Char tail, -- :: ByteString -> ByteString length, -- :: ByteString -> Int map, -- :: (Char -> Char) -> ByteString -> ByteString foldl, -- :: (a -> Char -> a) -> a -> ByteString -> a filter, -- :: (Char -> Bool) -> ByteString -> ByteString ... \end{verbatim} } \end{slide} % ------------------------------------------------------- % % lazy packed strings % \begin{slide} \heading{We should all be lazier} \end{slide} \begin{slide} \heading{Infinite strings} The new `packed' string type is great for many cases. However, programs that manipulate large or infinite streams, or use lazily evaluated strings, have trouble: {\footnotesize \begin{verbatim} main = getContents >>= putStr . filter (/= 'e') \end{verbatim} } {\footnotesize \begin{verbatim} $ ./strictio < 256M > /dev/null strictio: realloc: resource exhausted (out of memory) \end{verbatim} } A lazy, $[Char]$ program might have been able to handle this. \end{slide} \begin{slide} \heading{Lazy, packed strings} \subheading{The solution: lazy lists of packed strings} {\small \begin{verbatim} newtype LazyByteString = LPS [ByteString] \end{verbatim} } So have a lazy list spine, whose elements are strict chunks. \begin{slitemize} \item The processor should be able to load each chunk into the cache, and apply fast packed string operations \item And we can still lazily expand the list \end{slitemize} \begin{second} \begin{center} \begin{figure}[htbp] \includegraphics[scale=0.7]{images/lazy.eps} \end{figure} \end{center} \end{second} \end{slide} \begin{slide} \heading{Lazy filters} {\footnotesize \begin{verbatim} main = getContents >>= putStr . filter (/= 'e') \end{verbatim} } {\footnotesize \begin{verbatim} $ time ./lazyio < 256M > /dev/null ./lazyio < 256M > /dev/null 2.30s user 20% cpu 12.449 total \end{verbatim} } Lazy IO wins. This program uses a constant heap size of around: {\footnotesize \begin{verbatim} 14433 dons 32 0 4036K 2528K run - 0:00 2.00% lazyio \end{verbatim} } So no realloc problems. \end{slide} \begin{slide} \heading{Lazy packed string functions} Lazy bytestring functions use list functions over the spine of the structure, and packed functions over each chunk: {\small \begin{verbatim} map :: (Word8 -> Word8) -> ByteString -> ByteString map f (LPS xs) = LPS (L.map (P.map f) xs) append :: ByteString -> ByteString -> ByteString append (LPS xs) (LPS ys) = LPS (xs ++ ys) \end{verbatim} } So we reuse the already optimised list functions -- less work. Lazy bytestrings often have better complexity that their strict siblings (as `cons' is an O(1) operation). \end{slide} \begin{slide} \heading{Comparing strict and lazy packed strings} \begin{center} \begin{figure}[htbp] \includegraphics[angle=-90,scale=0.3]{images/strictlazy.eps} \end{figure} \end{center} {\small Performance of strict strings (red) versus lazy strings, across their shared api. The better complexity of many lazy string functions is apparent (often having $O(1)$ complexity over $O(n)$ for flat, strict strings). } \end{slide} \begin{slide} \heading{Tuning the chunk size} \begin{center} \begin{figure}[htbp] \includegraphics[angle=-90,scale=0.3]{images/chunk_v_cache.eps} \end{figure} \end{center} {\small Running time versus lazy string chunk size (in bytes). Note the speed improvement when the chunk is around the L1 and L2 cache sizes. } \end{slide} % ------------------------------------------------------- % Fusion \begin{slide} \heading{Rewrite rules for optimised strings} \end{slide} \begin{slide} \heading{Function composition} \subheading{Function composition is common in packed string code} {\footnotesize \begin{verbatim} print . minimum . filter (`isPrefixOf` x) . map toUpper \end{verbatim} } \begin{second} \subheading{And this is compiled to} {\footnotesize \begin{verbatim} case map toUpper s of s' -> case filter (`isPrefixOf` x) s' of s'' -> case minimum s'' of s''' -> print s''' \end{verbatim} } {\dgreen Lots of temporary arrays are being allocated and discarded!} \end{second} \end{slide} \begin{slide} \heading{Functional array fusion} \subheading*{Ideally, we'd like to make just one pass over the input data} We'd write: {\footnotesize \begin{verbatim} map f . map g \end{verbatim} } \begin{second} and the compiler would emit: {\footnotesize \begin{verbatim} map (f.g) \end{verbatim} } This is know as loop (or array) fusion. Unfortunately, such properties are too high-level to be found by the compiler. \end{second} \end{slide} \begin{slide} \heading{Rewrite rules} GHC allows us to specify equational transformations \RULE{map/map~fusion} {f~g~arr} {map~f~(map~g~arr)} {map~(f~.~g)~arr} \begin{second} \begin{slitemize} \item Whenever the left side is spotted, GHC will replace that code with the right hand side. \item We can tell the compiler about important equivalences in our program, that it cannot find on its own. \end{slitemize} \end{second} \end{slide} \begin{slide} \heading{What about other functions?} \subheading*{Works nicely for map. What about filters, folds} One option would be to add a new rule for each new function \begin{slitemize} \item But this leads to $O(n^2)$ rules \item E.g. \end{slitemize} {\footnotesize \RULE{map/map~fusion} {f~g~arr} {map~f~(map~g~arr)} {map~(f~.~g)~arr} \RULE{filter/filter~fusion} {f~g~arr} {filter~f~(filter~g~arr)} {filter~(\lambda{}e~\rightarrow~f~e~\&\&~g~e)~arr} \RULE{filter/map~fusion} {f~g~arr} {filter~f~(map~g~arr)} {filter~(\lambda{}e~\rightarrow~case~f~e~of~e'~\rightarrow{}if~g~e'~then~Just~e'~else~Nothing)~arr} and more... } \end{slide} \begin{slide} \heading{Rewriting as a practical optimisation} By specifying functions in terms of a single loop combinator, we would be able to fuse all sorts of functions, without an explosion of rules. \begin{second} \subheading*{$loopU$} \begin{slitemize} \item loopU is a generic map, filter and fold function \item Described in Chakravarty and Keller, 2001. \end{slitemize} \subheading{So rewrite map and filter in terms of loopU} {\footnotesize \begin{verbatim} map f = snd . loopU (mapFn f) NoAcc mapFn f = \_ e -> (NoAcc, (Just (f e))) filter p = snd . loopU (filterFn p) NoAcc filterFn p = \_ e -> if p e then (NoAcc, Just e) else (NoAcc, Nothing) \end{verbatim} } \end{second} \end{slide} \begin{slide} \heading{loopU fusion} \subheading{And then we need a single fusion rule only} \RULE{loopU/loopU~fusion} {f~g~a~b~arr} {loopU~g~b~(snd~(loopU~f~a~arr))} {loopU~(f~`fused`~g)~(a,b)~arr} \begin{second} \subheading{And a generic fusion body} {\footnotesize \begin{verbatim} fused f g (a,b) arr = case f a arr of (a', Nothing -> ((a', b), Nothing) (a', Just arr' -> case g b arr' of (b', res) -> ((a', b'), res) \end{verbatim} } \end{second} \end{slide} \begin{slide} \heading{Results} \begin{center} \begin{figure}[htbp] \includegraphics[angle=-90,scale=0.3]{images/fusion.eps} \end{figure} \end{center} {\small Works very well. All left-to-right loops (map, foldl, filter) can be fused into a single pass. The running time of fused pipelines (green) is always better. } \end{slide} \begin{slide} \heading{Improving fusion} \begin{slitemize} \item Using loopU, only `left-to-right' loops can be fused (foldl, scanl) \item Reverse loops, those starting at the end of the array, can't fuse (foldr, scanr) \item And the common operations -- map, filter -- carry an unused accumulator \end{slitemize} \begin{second} We've developed an improved fusion scheme using 4 combinators to fuse up, down, and unidirectional loops. \begin{slitemize} \item map, and filter can fuse with any direction \item and up and down loops fuse, improving cache behaviour \item requires 24 rewrite rules \end{slitemize} \end{second} \end{slide} \begin{slide} \heading{More results : speed} \begin{center} \begin{figure}[htbp] \includegraphics[angle=-90,scale=0.3]{images/fusion2.eps} \end{figure} \end{center} {\small Same graph as before, but with reverse loops (such as foldr). These were not fuseable under the old scheme (red) } \end{slide} \begin{slide} \heading{More results : memory} \begin{center} \begin{figure}[htbp] \includegraphics[angle=-90,scale=0.3]{images/allocs.eps} \end{figure} \end{center} Across all fuseable 2-element pipelines, memory use on average is roughly halved. \end{slide} % ------------------------------------------------------- \begin{slide} \heading{Testing with QuickCheck} \end{slide} \begin{slide} \heading{Keeping things together} Data.ByteString is a large library, that needs to be a functionally-equivalent replacement for Data.List. \begin{slitemize} \item Rewrite rules need to be correct \item All functions should produce the same result as their List siblings. \item All lazy functions need to be equivalent to the strict ones \item The results before and after rewriting need to be equivalent List versions \end{slitemize} \subheading*{A lot of testing..} \end{slide} \begin{slide} \heading{Automate!} \subheading*{QuickCheck is a type-based Haskell testing framework} First define a generator for your type: {\footnotesize \begin{verbatim} instance Arbitrary Char where arbitrary = choose ('a', 'z') \end{verbatim} } And then specify properties that should hold on functions over your type: {\footnotesize \begin{haskell} prop\_sort1 xs = (not (null xs)) \Longrightarrow (head . sort) xs \equiv minimum xs \\ prop\_sort2 xs = (not (null xs)) \Longrightarrow (last . sort) xs \equiv maximum xs \\ prop\_sort3 xs ys = \\ ~~~~~(not (null xs)) \Longrightarrow \\ ~~~~~(not (null ys)) \Longrightarrow \\ ~~~~~(head . sort) (append xs ys) \equiv min (minimum xs) (minimum ys) \\ \end{haskell} } \end{slide} \begin{slide} \heading{Running QuickCheck} {\small \begin{verbatim} *Main> main invariant : OK, 100 tests. all : OK, 100 tests. any : OK, 100 tests. append : OK, 100 tests. compare : OK, 100 tests. concat : OK, 100 tests. cons : OK, 100 tests. eq : OK, 100 tests. filter : OK, 100 tests. find : OK, 100 tests. ... \end{verbatim} } \end{slide} \begin{slide} \heading{Failing tests} Failing tests show the failing data. In this case, the $all$ function failed when given an empty string (and a random function!) {\small \begin{verbatim} *Main> main invariant : OK, 100 tests. all : Falsifiable after 0 tests: LPS [] \end{verbatim} } Generating random functions is useful for testing higher-order code. \end{slide} \begin{slide} \heading{Testing rewrite rules} \subheading{The first thing we want checked are the rewrite rules} \begin{slitemize} \item These are compiler optimisations \item So both sides of a rewrite rule need to be equivalent \item Or user's code will be mangled! \end{slitemize} Short of an actual proof of equivalence, we need to at least test that for all input data, both sides of the rewrite rule return the same result. \end{slide} \begin{slide} \heading{Encoding rewrite rules} The map/map rule: {\footnotesize \RULE{map/map~fusion} {f~g~arr} {map~f~(map~g~arr)} {map~(f~.~g)~arr} }% Can be directly coded as a QuickCheck property: {\footnotesize \begin{haskell} prop\_map\_map\_fusion f g arr = \\ ~~~~map f (map g arr) \equiv \\ ~~~~~~~~map (f~.~g) arr \end{haskell} }% When executed, QuickCheck generates $n$ random functions and random arrays, checking the left and right sides are always equivalent. \end{slide} \begin{slide} \heading{More examples} Another rewrite rule requires a particular function, $sequenceLoops$, to be associative. Coded up in QuickCheck: Can be directly coded as a QuickCheck property: {\footnotesize \begin{haskell} prop\_sequenceloops\_assoc n m o x y z a1 a2 a3 xs = \\ ~~~~~~~~k ((f * g) * h) \equiv k (f * (g * h)) ~\\ ~~~~where \\ ~~~~~~~(*) = sequenceLoops \\ ~~~~~~~f = (sel n) x a1 \\ ~~~~~~~g = (sel m) y a2 \\ ~~~~~~~h = (sel o) z a3 \\ ~~~~~~~k g = loopArr (loopWrapper g xs) \\ \end{haskell} } \end{slide} \begin{slide} \heading{More testing} In fact, the QuickCheck rewrite properties are tested automatically when every patch is comitted. {\small \begin{verbatim} loop/loop wrapper elim : OK, 100 tests. sequence association : OK, 100 tests. up/up loop fusion: OK, 100 tests. down/down loop fusion: OK, 100 tests. noAcc/noAcc loop fusion: OK, 100 tests. noAcc/up loop fusion: OK, 100 tests. up/noAcc loop fusion: OK, 100 tests. map/map loop fusion: OK, 100 tests. filter/filter loop fusion: OK, 100 tests. map/filter loop fusion: OK, 100 tests. filter/map loop fusion: OK, 100 tests. map/noAcc loop fusion: OK, 100 tests. ... \end{verbatim} } \end{slide} % ---------------------------------------------------------------- \begin{slide} \heading{Model Checking with QuickCheck} \end{slide} \begin{slide} \heading{Checking against a model api} $ByteString$ functions should be equivalent to the same functions in the $[Char]$ and $Lazy.ByteString$ types. \subheading{Types and their models} \begin{center} \begin{figure}[htbp] \includegraphics[scale=0.7]{images/model.eps} \end{figure} \end{center} We've written the beginnings a model checking domain specific language on top of QuickCheck, to simplify property specification. \end{slide} \begin{slide} \heading{Example} \subheading{Two functions on different types can be stated to be equivalent} {\small \begin{haskell*} prop\_concat & = & L.concat & \equiv & P.concat \\ prop\_null & = & L.null & \equiv & P.null \\ prop\_reverse & = & L.reverse & \equiv & P.reverse \\ prop\_transpose & = & L.transpose & \equiv & P.transpose \\ \end{haskell*} }% QuickCheck will then generate all the required arguments, and test the results. Greatly simplifies property specification. \end{slide} \begin{slide} \heading{Under the hood} The model language uses one type to model another \begin{slitemize} \item This fact is encoded using type classes \item For each pair of types, a natural transformation function is defined \end{slitemize} {\small \begin{haskell*} class Model a b where \\ ~~~~model :: a \rightarrow b \\ ~\\ instance Model P [Char] & ~where model = & C.unpack \\ instance Model B [Char] & ~where model = & L.unpack . checkInvariant \\ instance Model B P & ~where model = & abstr . checkInvariant \\ ~\\ instance Model Bool Bool & ~where model = id \\ instance Model Int Int & ~where model = id \\ \end{haskell*} } Types are trivially modelled by themselves \end{slide} \begin{slide} \heading{Further under the hood} Non-simple types are modeled recursively: {\small \begin{haskell*} class (Functor f, Functor g) \Rightarrow NatTrans f g where \\ ~~~~eta :: f a \rightarrow g a \\ instance Model f g \Rightarrow NatTrans ((,) f) ((,) g) where \\ ~~~~eta (f,a) = (model f, a) \\ instance (NatTrans m n, Model a b) \Rightarrow Model (m a) (n b) where \\ ~~~~model x = fmap model (eta x)\\ \end{haskell*} } For pairs, model the first element, then recurse and model the second element. Similar for function types. \end{slide} \begin{slide} \heading{Connecting two types} Using $model$ two transform one type to another, we're able to specify a class of $\equiv$ functions. {\small \begin{haskell*} f \equiv g = \lambda{}a & \rightarrow & ~ \\ ~~~~model (f a) & == & g (model a) \\ f \equiv g = \lambda{}a b &\rightarrow & ~ \\ ~~~~model (f a b) & == & g (model a) (model b) \\ f \equiv g = \lambda{}a b c & \rightarrow & ~ \\ ~~~~model (f a b c) & == & g (model a) (model b) (model c) \\ f \equiv g = \lambda{}a b c d & \rightarrow & ~ \\ ~~~~model (f a b c d) & == & g (model a) (model b) (model c) (model d) \\ f \equiv g = \lambda{}a b c d e & \rightarrow & ~ \\ ~~~~model (f a b c d e) & == & g (model a) (model b) (model c) (model d) (model e) \\ \end{haskell*} } \end{slide} \begin{slide} \heading{Finally} And finally, QuickCheck is able to generate the random arguments, perform the necessary transformations on types, for us to simply state: {\small \begin{haskell*} prop\_concat & = & L.concat & \equiv & P.concat \\ prop\_null & = & L.null & \equiv & P.null \\ prop\_reverse & = & L.reverse & \equiv & P.reverse \\ prop\_transpose & = & L.transpose & \equiv & P.transpose \\ \end{haskell*} }% \end{slide} \begin{slide} \heading{Future} \begin{slitemize} \item Write a paper on this stuff \item \emph{Prove} rewrite rules are safe (Gerwin.. ?) \item Google's funding a Summer of Code project to add unicode support \end{slitemize} Already used in \begin{slitemize} \item Lindows/Linspire system tools \item Pugs, world's only perl6 compiler \item Lots of other cool Haskell projects \end{slitemize} \end{slide} % THE END \begin{slide} \heading {Data.ByteString} \begin{figure}[htbp] \begin{center} \includegraphics[scale=0.51]{images/bytestring.eps} \end{center} \end{figure} \begin{slitemize} \item Home page : \url{http://www.cse.unsw.edu.au/~dons/fps.html} \item Available with the current version of Hugs \item Available with the next version of GHC \end{slitemize} \vspace*{1\bigskipamount} \begin{figure}[htbp] \flushleft \includegraphics[scale=0.3]{images/phd.ps} \end{figure} \end{slide} % ------------------------------------------------------- \end{document}