Video 3-8: §3.6 Python's list sort & Powersort

0:00 <Untitled Chapter 1>

0:04 now I want to comment on the second method which was called Power sword I was a bit of a Daft name but it has a technical reason that I want to show you and the reason why why I'm showing you all this is that it's the new standard sorting method in Python so um a bit more tricks were needed for that so let me show you what python did before that first

0:30 Sorting in Python

0:35 so in terms of the the the names I should I should be precise and so I want to be precise python itself is a programming language and really what it is is a big document or collection of websites if you want that defines how programs in Python should look like and how how they should behave it doesn't give you a way to execute them by itself python is just the specification now there's a python Foundation that maintains this specification and develops it you know there's Python 3 now and then all these changes so the language has developed and this is what the python Foundation takes care of the second thing they do is they release a reference implementation which is a way to show the world here's the specification and here's one way to implement it and hopefully a not too crappy one because that's the implementation that most people use and this is called C python it's called C python because it's written in C it's fairly old but updated that's uh it's been around for essentially as long as python exists so if you don't do anything special python will mean c python for you even though you may not have thought about it before part of python are lists and all sorts

1:59 of other data structures and parts of lists is the sort function so you can have a list and say dot sort where you can use this sorted function uh which which produces a sorted copy of the list that's the main difference and um so these sorting algorithms are implemented in C using directly how python lists are represented I'll learn much more about this stuff than I ever wanted to know you know but uh is is quite interesting how some of the details are worked out but for those of you who just started learning python uh we don't need that yet um now so one of the core developers of of C python is Tim Peters who came up with Tim sword which was named after him without uh without necessarily his approval at the time but the name stuck so there you go um interestingly this is a custom merge sort method because the python Community really wanted a stable sort that was their spare their desire their specification when he set out to write a new sorting algorithm so uh he went he went to do this and try to design the Sorting method that really is uh is smart plus stable so he did think about the things that we discussed pick up sorted runs and all

3:28 these things but he thought about a few other things so the way that Tim sword works is a is a little different um okay since since last year uh that's the bit where now uh Power sword is used but I haven't told you what that works like what that looks like

3:50 I don't know if you have has anyone heard of Pi Pi so uh is also included there in case you care is Piper is an interesting attempt to re-implement python so it's an alternative to C python often amazingly fast because they play a lot of tricks with just in time compilation but that leads us to fights just for completeness

4:13 Timsort (original version)

4:17 so for merge sword if you think about merch sword you would expect to either see a top-down or bottom up or something like this but Tim sword is neither of the two instead it

4:31 um I think you really want a picture for that well uh it it goes through the list from left to right and instead of doing um a recursive call or something like this it keeps it keeps a manually maintained stack of runs so you guys know what a stack is here's how it's used so you find runs from the left you you scan find a new run and then you put that on the stack then there's some invariants that this stack is supposed to satisfy and if that invariant is violated you merge two adjacent elements in the stack and replace them with the result of the merge and then you keep going so it always works like finding the next run from the position where you are to the right push that on the stack and then check if some of these rules say you should merge something and you do this until you reach the end right end of the array and if there's things things left in the stack you just merge this top down uh there's there's lots of other trots of other uh low level tricks that um I'm glossing over this because they're not relevant for the the change I'm discussing with you here uh and here's the four rules uh again I

5:56 don't want to go into too much detail but they're they're quite wild uh they say some things like if the if the topmost run on the stack is larger than the Third run on the stack then you should really merge the second and third makes some sense because you don't want to merge this long one right uh

6:22 other rules are slightly less intuitive if um if the the second plus the first are bigger than the third then you want to merge the first two stuff like this okay so why and how did Tim Peters come up with this he admitted it was the first kind of set of rules that somewhat worked and that's where he stopped so these rules are surprisingly good um but there's no uh there's no real principled way behind this uh explaining why they're good not not uh that would be easy easily explainable

7:09 I want to point out a few reasons why there's going from left to right and maintaining this stack so tilting merge sort on this on its side why would you want this um well first of all it picks up existing runs but we have other means to do that uh the second thing that's that's Nifty is you detect the Run and so you have brought that data into your local cache so you touch that data and it's fresh in the cache so you want to if you have to merge this you want to do it right now instead of instead of like Peaks or you peek in the middle oh there's a run hold on let me first merge something entirely different that wastes this memory transfers so Tim's Tim's sword is is smarter on that on that front

7:59 there was also an interesting story about uh rule D wasn't in the original code and it turned out for 10 years Python and Java had a sorting method that would either suck fault or throw an array index out of Bounce exception if you called it with the right input it just never occurred in 10 years or nobody bothered to report a bug report and Rule D um stops that from happening

8:35 uh well the story is um the story is really cool so people do formal verification we discussed this very briefly and so this this is quite Advanced so some people have um have software that can take a Java program with specification in a certain language and automatically verify if the code satisfies this I told you back then it's impossible to do this automatically so they don't fully do this automatically they need a little help from the user to specify invariants but all the mechanic bits they can do for for entire Java programs and so when they were coming to a conclusion with their project they were looking for some test cases what's an algorithm or some piece of code that's not too complicated but also not trivial not boring and so they thought let's verify that Tim sword swords correctly and they tried and tried and tried and it didn't work they couldn't it was still lemas popping out proof obligations they couldn't satisfy they said oh it's all all wrong uh that tool doesn't work and then they found that actually one of the invariants that Tim Peters wrote as a comment was wrong it wasn't guaranteed by these rules if you leave out rule d and that's how people discovered so it's it's a very interesting story with this

9:53 Twist of formal verification being really useful yeah it's another Twist of the story that for 10 years nobody ever noticed so it's a really special you need a very specific sequence of run lengths for this problem to occur and the Crash come came from the fact that the stack was using a fixed size array stack because these are fast if you know the upper Bound for the stack height you can do it but the computation of the stack height was wrong if rule D wasn't there so that's how it all fell apart that's fixed by now um but still running a bit out of time so let's try to speed this up a little bit uh here's a specific input that two researchers found I don't know how they discovered this weird pattern so this is it's two one one three red is is all runs half length one two or three and if you execute Tim sword with all these four rules and all of that it spits out that kind of merge tree which is uh I mean it's really hard to work out manually you want to do this with a computer program now if you look at this closely You observe there's a few merges which are appear really really stupid

10:31 Timsort bad case

11:13 there's uh and this repeats uh indefinitely if you make the input bigger you time and again have a merge that has one long run and adds a single more element to make it in the slightly make it to a slightly bigger run and that can't really be good because you're wasting all these merge costs to just get one bigger this and uh if if you uh look at this from from further away the runs are almost the same length so doing just your standard bottom-up merch sword would probably do better uh it's too bad I didn't put the bar for bottom up well Tim sword for this small input is at 371 the lower bound is this age is thin as 16 and Peak sword would get it with 321 so um if you make the input bigger the overhead grows to uh Factor 1.5

12:16 and I think the real problem is just these rules are so complicated no one fully has a good intuition and so yeah weird things just happen in some you needed someone to find these

12:31 um luckily there's a better way so the solution and what what power sword then does is do something like this peak sort but in the way that's in a way that's compatible with Tim stores idea of going left to right and keep things on a stack which is a bit of a problem because we you can't use recursion Peak sword used recursion to find the middle now what's the middle if you're if you're starting left to right you don't want to jump into the middle you want to keep going left to right without seeing the future and it's a little surprising that this is possible but uh again there's there's old works on on binary search trees that that guided this search um and it turns out the the following Works um I'll just run through this at a little a little quicker and leave you to Marvel at why it works um

13:31 there's a magic function here that I'll explain the next slide that takes two runs and computes a power this is just some number the algorithm then works as follows it similar to Tim sword left to right it scans runs when it finds some it puts them on a stack and there will be some invariant what happens to the stack and you keep going now the invariance receiving the code says if you if you look down from top of the stack downwards then the power should only decrease so at this point this is violated 2 is smaller than three so that's a violation so we should merge those two so we do that and um that means that gives us a first bit of our tree at the end uh once you've done that so here now the invariant is satisfied because it's just a single element on the stack so you can move on put the next thing on top now same problem right one is smaller than two so we have to merge what's on the stack that gives us the next next bit and then it's satisfied because it's a single element we keep moving now we find a power of two so that can go on top without violation another Power this time is four so it

14:55 can go on top and then we reach the the end of the array and at that point similar to Tim sword um you just merge down take the topmost two until the stack is just a single element so we merge those two then those two and finally this uh the entire run okay

15:19 if you compare this that's the same input I showed you Peak sword on before and there's a slight difference on how it works but um from uh from zooming out a little it works almost the same as Peak sort it does a very similar way of merging up things um using these magic powers so you probably want to know where these numbers came from and okay bam I know that slide is a bit full so here's code to compute these blue numbers and it's just doing some some arithmetic with the indices of of the Run boundaries a slightly more intuitive way to look at it is there is a recursive procedure behind it which is very similar to peaksort but instead of in Peak sword when you split here you would now have the recursive call on this side in Peak sword you would say let's find the middle of this part and then you detect this run and find the closest boundary and Power sword you don't do that but instead you keep cutting the original length in half so here you take the one quarter Mark of the original array that works almost the same as for Peak sword but the trick is now we don't need the history of the recursion because the

15:45 Powersort-Computing powers

16:46 quarter Mark of the entire array is at the same spot no matter where the first cut was so that's that's intuitively the change and well there's there's a power computation that's why it's called Power

17:07 foreign there's another more graphical way to show what the powers do uh I'm not sure how helpful this is without more explanation you have two runs you can connect the two midpoints that gives you the blue intervals and then you find what's the the largest pole of these blue poles that uh lies in the inside this interval and the poles are the one half mark gets a height of one the quarter marks get Heights of two the next uh cut things in half get higher free and so on uh

17:47 Powersort - Discussion

17:49 good I don't think I have time to explain more so let me just briefly say the good things again it keeps everything like Tim sword so people like that because you can keep all the good things that work there uh we have a similar proof of merge cost as for Peak sword it's actually the same same outcome and the other bit that may not be obvious from the code I've shown you but it's it's really really fast to compute these Powers it's actually very cheap with playing playing word Ram tricks and so you have very little overhead to find this good merge order but you can prove that is essentially a best possible way