dagit.o

Fun, but pointless, code metrics

2010-08-29T15:40:00.000-07:00

I'm not really sure what motivated this, but I just used cloc to count the lines of code in both the darcs source and the git source. Here are the numbers. The git source tree:

1951 text files.
    1836 unique files.                                          
     848 files ignored.

http://cloc.sourceforge.net v 1.51  T=15.0 s (72.3 files/s, 20377.3 lines/s)
--------------------------------------------------------------------------------
Language                      files          blank        comment           code
--------------------------------------------------------------------------------
C                               267          15517          13469         100133
Bourne Shell                    589          15127           5508          84826
Perl                             40           3798           3441          23825
Tcl/Tk                           39           1453            375           9762
C/C++ Header                     99           1977           3557           8301
make                             12            413            434           2673
Bourne Again Shell                1            144            110           2165
Lisp                              2            231            170           1779
Python                           13            465            442           1384
ASP.Net                           8            141              0            931
m4                                2             87             21            858
CSS                               2            154             24            710
Javascript                        2            113            319            477
Assembly                          1             26            100             98
XSLT                              7             15             29             77
DOS Batch                         1              0              0              1
--------------------------------------------------------------------------------
SUM:                           1085          39661          27999         238000
--------------------------------------------------------------------------------

The darcs source tree:

561 text files.
     549 unique files.                                          
      57 files ignored.

http://cloc.sourceforge.net v 1.51  T=189.0 s (2.7 files/s, 298.0 lines/s)
--------------------------------------------------------------------------------
Language                      files          blank        comment           code
--------------------------------------------------------------------------------
Haskell                         169           4361           7374          27760
Bourne Shell                    300           2071           2869           8333
C                                 7            325            153           1494
HTML                              5             41              4            316
C/C++ Header                     12             92             83            308
Bourne Again Shell                3             51             95            180
Perl                              2             43             36            130
CSS                               1             21              3             79
make                              1             12              6             53
Lisp                              1              5              6             23
--------------------------------------------------------------------------------
SUM:                            501           7022          10629          38676
--------------------------------------------------------------------------------

Take those categories with a grain of salt. For example, the darcs source does not have any lisp files. It is interesting that git has 200k more lines than darcs. I'm not sure what that says. C is far more verbose than Haskell? Although, that's not really fair because they also have an order of magnitude more shell code. If you're just comparing C to Haskell it's a factor of about 4.

Delimited Continuations and version control: an update

2010-06-10T13:44:00.000-07:00

Last time I presented the idea that version control and delimited continuations are related. I left off with a question how how to make Darcs fit this model. I think I understand now what I was missing.

I forgot to think about Darcs operations in terms of the intermediate operations that get performed. In Darcs, everything is based on commuting patches, even merging. Therefore, to see how Darcs fits into this model it's important to think about commuting patches in terms of delimited continuations.

Specifically, I now believe that commuting two patches introduces marks that can be shifted to later.

I have several ideas for the next steps of this. One is to start modeling toy versions of svn and darcs in Haskell via delimited continuations. After that, I would like to figure out the correspondence between the delimited continuations that I've identified and their data structure reification as zippers. I hope to have more about that later.

Judging by a paper written by Oleg, there should be a natural way to convert the delimited continuation representation into a zipper. Investigating this model might shed light on the Darcs patch model, or even lead to a more concise formalism.

Delimited Continuations and Version Control

2010-06-06T02:30:00.000-07:00

Delimited continuations give us a way to create markers that we can jump back to. We can construct the future of the computation, work with the computation so far, or abort the current continuation and go down a new path (create a new future).

These primitives have a natural correspondence with version control systems that snapshot the world like
SVN. Focusing on SVN for a moment:

The current continuation is the transformation of repository state that you're working on. It's the diff you're creating.
For commits, each revision created by commit is a marker, so we model this with reset.
Checking out an older revision, or reverting changes, corresponds to a shift. We discard the current continuation and move back to a marker created by a specific reset.
Updating consists of having the client copy learn the current state of the continuation on the server and applying it to the local copy.
Starting a branch corresponds to a reset.
Merging two branches is a bit trickier I suspect. I haven't worked out all the details sufficiently to convince myself I have it right, but here is how I think this case works. The merge first shifts to each of the markers and then combines those two continuations into one future. The part that seems weird to me about this, is that I haven't really seen examples of delimited continuations were the continuation of two different markers (prompts) were combined.

Now, if you accept the above it gives us some intuition to build on. Although my correspondence is terribly informal at the moment, if we took some time to make it formal by working out enough details to model it in, say, Haskell, then we'd have a nice formal backing for how SVN works. I think the above model applies equally well to git, but I'm not confident with git's model.

One insight the above gives, is that the way merging works is not described by the continuations in general. It's up to the exact combining function to determine the merge. We know that an automatic merge can fail in practice due to things like conflicts between the changes in the branches. So, in the SVN implementation considerable work has gone into implementing logic for creating the proper continuation.

Now, in general when a merge, or update, is performed human intervention may be required. This typically happens when the changes are in conflict. What this means for our model is that in general the creation of the continuation requires knowledge outside of our model. What does that correspond to? Well, it's essentially saying that calculating the correct continuation to resolve the merge is non-deterministic!

In other words, this continuation view of version control gives us a rigorous way to talk about our intuition. Of course we can easily tell that merging is going to require human intervention without needing to study delimited continuations, but this framework of reasoning now gives us a more mathematical way to say it.

The next question is: How does the delimited continuation model of vcs apply to Darcs?

So far I'm not sure. I suspect, without working through the details, that in Darcs, every time you record a patch multiple resets happen, instead of just one. The model really breaks down for Darcs because you can seemingly visit points in "history" that did not exist when the patches were created, but they are valid repository states.

For example, imagine a repository that only exists locally. You create a sequence of patches. Now, take a patch in the middle that can be commuted to the end of the patch sequence. Doing so has not created a new repository state; so far this is fine with the above model as no new markers need to be created. Suppose we remove the patch from the end of the patch sequence. This is exactly how darcs unpull works. The funny thing is, we've now created a state that never existed previously. So in the delimited continuation model, what marker did we just shift to?

I don't know the answer yet, but I think it's an interesting question. I suspect there are multiple "correct" answers, but that only some answers will yield elegant and robust models here.

Type-Correct Changes — A Safe Approach to Version Control Implementation

2009-03-25T01:12:00.000-07:00

On March 20th, 2009, I successfully defended my Master’s thesis in Computer Science.

Abstract:
Ensuring correctness of real-world software applications is a challenging task. Testing can be used to find many bugs, but is typically not sufficient for proving correctness or even eliminating entire classes of bugs. However, formal proof and verification techniques tend to be very heavy weight and are simply not available for day to day use in many common programming environments.

We demonstrate a form of light-weight proof assistant by using the type checking features of the programming language Haskell with existing extensions. We apply this work to the Open Source version control system Darcs. The properties checked by our approach are derived directly from the data model used by Darcs. This allows us to eliminate entire classes of bugs at compile time. We also examine how these techniques improve the quality of the Darcs codebase and the challenges that arise when applying these techniques in practice.

You can read the full thesis here. The slides from my presentation are located here.

The bottom line is that we used Generalized Algebraic Data Types (GADTs) to enforce proper patch manipulations. In the Darcs implementation, patches are stored in sequences and rearranging those sequences can only be done is very specific ways. Our use of GADTs allowed us to express those constraints using existentially quantified types, phantom types, and witness types. If you’ve ever wondered how to use GADTs in real-world software, this serves as a very illustrative example.

Darcs Hacking Sprint — Summary from Portland Team

2008-10-28T01:09:00.000-07:00

The weekend of 24-25 October 2008 was an International darcs hacking sprint! The sprint was a lot of fun and we’ll be having more. The sprint provides a very productive atmosphere for hacking.

We had a team in Brighton with posts from Day 1 and Day 2. We also had team in Paris but I don’t have a link for them.

Here are just some of the highlights from the Portland Team:

Adding language pragmas in all files:
- makes the code cleaner when it’s time to drop ghc6.6 support
- all required language extensions are now known
- makes it easier to check for Haskell’ compatibility
Removed OldFastPackedStrings
Replaced FastPackedStrings api in favor of Data.ByteString api
- lots of small optimizations, less pack/unpack, more standard
  ByteString code
- removed a fair bit of C code, new code compiles to same or
  faster assembly (Don checked)
cabalization:
- no autoconf or make needed
- cabal install tested and working on linux / osx, windows testing
  soon to follow
- builds out of the box w/ 6.8 and 6.10
- configure is much faster
module graph (depends on cabalization)
Duncan improved zlib
- soon to be available on hackage
- allows us to replace our own implementation of zlib bindings
  with the main stream one
- will make building on windows easier
- can use lazy bytestrings

Here are some random pictures from the Portland Sprint.
Packages we should consider:

The TODO list we made on the first day:

Checking on Team Brighton:

Duncan and Jason looking at the projector:

Ah, beautiful Portland in fall:

Understanding Darcs Commute

2008-10-24T00:52:00.000-07:00

People often want to understand how commute on patches works. Usually we start by saying:

Given two patches, A and B, if A and B commute then: AB <--> B’ A’, for some B’ and A’.

Naturally people ask, “But what is the relationship between A and A’ or B and B’?” This is a very important question and I’ll provide you with some insight.

Suppose we have a repository with 2 files, a and b. We could then make the following operations:

mv b c
mv a b
mv c a

You can think of each operation as a transformation on the ’state’ of your repository.
Suppose also, that we make an edit to a, and an edit to b.

Let’s name the above, using T for transformation:

T_bc = mv b c
T_ab = mv a b
T_ca = mv c a
T_a = edit a
T_b = edit b

You can imagine that if I gave the diff for T_a and the diff for T_b that you could apply those diffs in either order to your repository and get the same final ’state’. Meaning, a and b are the same whether you update a first or b first.

But, suppose instead that I performed T_bc, T_ab, and then T_ca. This has the effect of swapping a and b by name. Now suppose you applied the diffs T_a and T_b. What would you want the outcome to be?
It turns out, that it matters which operations were created first. If you created the diffs T_a and T_b *before* you did the operations of the swap, then you should expect that after the swap the diff for T_a actually modifies b, whereas T_b should modify a. On the other hand, if you created the diffs T_a and T_b *after* the swap, then you expect T_a to modify a and T_b to modify b.

We have an intuitive idea of ‘context’ now. As in, what is the context that T_a and T_b were created in? Knowing this will tell us how they transform the repository state.

Intuitively, it seems as though we need to remember the ‘context’ in which T_a and T_b were created. So let’s say that the operations performed up to the point where T_a is created is the context of T_a. In other words, the context for T_a is sequence of transformations that existed when T_a was created. Similarly, since T_a is a transformation, creating it results in a new context, which is the old context plus T_a. We could say that T_b has this context. Going a bit further, it seems like we should talk about how T_a has a pre-context and it also has a post-context.

For example, if we created T_a before doing the swap, then the pre-context might include two transformations, one that creates a and another one that creates b. The post-context would then include those two transformations and T_a itself. If we created T_a after doing the swap, the pre-context and post-contexts of T_a would include T_bc, T_ab and T_ca also.

Now a side note about commutative functions. Consider the function created by composing T_a and T_b, let’s write T_a . T_b. Recall, that with function composition parameters start on the right and pass through the sequence to the left. As discussed in the intro, T_a . T_b is equal to T_b . T_a. This is because T_a and T_b are independent of each other. Thus, we would say that the functions T_a and T_b are commutative functions. This means, that changing their order of application does not change the result.

We are saying that:

T_a . T_b = T_b . T_a

Because T_a and T_b are commutative it doesn’t matter which order we compose them. If we restrict our view to just the repository above with only the files a, b and no c, then on this restricted set of repository state how do these two compare?

T_b . T_a
T_a . T_b . (T_ca . T_ab . T_bc)

In plain English, the first one edits a and then b, the second one swaps a and b, edits b and finally edits a.
As far as the mathematics of it is concerned, the first one will edit a and b, while the second one will have T_a editing a different a than the first one and T_b editing a different b than the second one.
Going a bit further, let’s say that T_a and T_b were created without any of T_bc, T_ab or T_ca in their context. So we could have two scenarios.

We could, for example, start with T_b and T_a, swap their order and then do the swap of a and b afterwards. That would give us:

T_b . T_a

and

(T_ca . T_ab . T_bc) . T_a . T_b

Intuitively, it seems like T_a and T_bc are commutative functions, eg., T_bc . T_a = T_a . T_bc. So we could rewrite the second one as this:

T_ca . T_ab . T_a . T_bc . T_b

Now, suppose when we commute the function T_a with T_ab, that we replace T_a with T_a’. T_a’ is like T_a except that T_a’ makes the edits of T_a to b instead of a. After all, this results in T_a’ editing the correct file after the rename. Similarly, when we commute T_b with T_bc, T_b is replaced with T_b’ that edits c instead of b. When we commute T_b’ with T_ca we replace T_b’ with T_b” that edits a instead of c.

So, the above goes through these steps:

T_ca . T_a’ . T_ab . T_bc . T_b (commute T_a to the left)
T_a’ . T_ca . T_ab . T_bc . T_b (commute T_a’ to the left)
T_a’ . T_ca . T_ab . T_b’ . T_bc (commute T_b to the left)
T_a’ . T_ca . T_b’ . T_ab . T_bc (commute T_b’ to the left)
T_a’ . T_b” . T_ca . T_ab . T_bc

The last one will then have T_a’ and T_b” making edits the same file contents as T_a and T_b respectively, even though the names of the files were changed by the swap.

So, if you’ve followed me to this point, then you now have the intuition for what we mean when two patches A and B, commute to B’ and A’, as AB <--> B’ A’. You can think of a patch as being one of the above transformations along with the context of the transformation. You might also notice that commute of patches must be doing something to the context of the patches.

Patch commute has the potential to update the context and transformation the patches it swaps OR it could update the context and leave the state transformations equal to what they were in the input. Patch commute can also fail, but we’re ignoring that case for the moment.

Thinking back to how we arrived at the need for context, you might notice that for each context, that is each sequence of operations, we get one unique repository state. This is a very important property of context. Without it, context wouldn’t really be useful. Also, notice that the opposite is not true, repository state does not determine the context. Which makes sense, because there are lots of operations you can do that get the repository to a particular state, so given a state how do you know what was done?

The next important property we want for commuting patches is that once two patches have been commuted, you can commute them again to undo the commutation. In fact, it turns out the examples above are saying we want contexts to determine the same state if you commute the patches inside the context (again, context is a sequence of patches!).

For R to be an equivalence relation, we need three things:

x R x, is true for all x
if x R y then y R x
if x R y and y R z then x R z

Here, we replace x R y with “the sequencing, or order, of x can be obtained by commuting adjacent elements of y”. Roughly how to prove each:

either claim that 0 commutes satisfies definition of R or check that commute is self-inverting
relies on self-inverting nature, I think
messier but should still be provable

I’m pretty sure both (2) and (3) could be done with a brute force proof that considered all the pairings of patch types in their general cases. Start with all sequences of length 2, then 3 and I think at that point you could make an inductive argument to hit sequences of length n. This would be a lot of work, and I’m not convinced it could be fully automated.

Why would we want to show the above? Showing that R is a relation would tell us that sequences of patches are equivalent under commute. Now, combine this with the idea that context determines the state uniquely and now we know sets of patches uniquely determine your repository.

Darcs 2 Real-World Push Performance Evaluation

2008-08-21T00:49:00.000-07:00

Thanks to Eric Kow, Duncan Coutts and Ian Lynagh we have some great timing data for using darcs2 and darcs1 to push patches over ssh.

Eric wrote a script to test three different scenarios of using darcs to push patches:

Scenario l1r1:
Scenario l1r2:
Scenario l2r2:

Next, Duncan and Ian provided us with access to 131 real-world repositories hosted at http://code.haskell.org. We ran the script to push patches to each repository, this gave us a ton of times. Then in Excel we crunched these numbers to see that not only is scenario l2r2 no worse than the other two, it’s actually faster on the time consuming cases!

The one caveat we found is that the minimum start-up time for the first two scenarios is 1 second and in the last scenario it’s 2 seconds. I’m confident we can shave off this 1 second difference in the future.

This is a histogram that shows you how the push times distribute, click on it for a large image. Along the bottom we have how many seconds the push took, and along the vertical axis we have the number of data points in that range. At a glance you can see that most repositories take just a few seconds to push. We can also see that darcs2 is slower on small pushes by about one second. Darcs2 in this chart corresponds to l2r2 and darcs1 corresponds to l1r1.

On a side note, we also tested converting all the repositories to darcs2 repository format and that worked great as well. Converting all the repositories at once takes less than 20 minutes on my laptop without a single error. There were a few warnings, but that’s to be expected as potentially exponential merges are fixed in the new darcs2 format, but darcs emits a warning when fixing them.

For anyone that wants to see the raw numbers click here. The link does work, but not all web browsers are showing the numbers. Opera and FF3 work on some platforms and not others.