Concurrency as Basis for Scalable Parallelism

David Barbour's Concurrency as basis for Scalable Parallelism may change the way you think about programming:

It has been observed that many 'concurrent' applications fail to scale beyond a few parallel components. In many cases, some sort of data-parallelism is feasible (e.g. parmap, SIMD, GPU) and we should certainly be able to leverage those opportunities! But I'd like to address just the concurrency aspect - the coordination of diverse systems and interests - and argue that even that is a sufficient basis for scalable parallelism, assuming we leverage it properly.

The scalability of concurrency as a basis for parallelism comes in realizing that the number of relationships in a system can rise O(N^2) with the number of components. Thus, we need to embed most significant computation into the relationships, rather than the components. ...

When most computation is moved to the relationships, the resources used by a service will scale commensurately with the number of clients it directly services - and vice versa; resources used by a client will be commensurate with the number of services it directly uses.

It changed my thinking: from "ouch, this is a lot of data to process" to "wow, lots of opportunities for concurrency, and thus parallelism".

Notes on Dependent Types

Since discovering Ωmega, I've been drawn into the fantastic world of dependent typing. Dependent types allow the expression of static invariants that your program is then guaranteed to respect dynamically. This works up to computation: proofs of static invariants are programs, so arbitrary invariants may be expressed by the programmer, and verified by the type system. I repeat, arbitrary invariants. If you're not salivating yet, you might want to skip this post.

A couple of systems I've (superficially, so far) looked at are Ωmega, Epigram, Coq, and Agda.

Ωmega is closest to existing FP languages like Haskell, which makes it easier to grok than the others for newbies - it's not a full-spectrum dependent type system by design. Technically speaking, Ωmega is "faking it" by maintaining a strict phase distinction between the value and the type level (and the kind level ...). Proofs are represented as runtime instances of GADT datatypes.

GADTs, or generalized algebraic datatypes, are a more powerful (generalized) form of ordinary ADTs, such as ML's 'a list, that are used as datatypes (or "object system") in many dependently typed systems. GADTs are very closely related to generics in Java and C#; understanding generics and their proposed higher-level extensions thus provides a gentle route into dependent types.

Java and C#'s object systems already have all of the power of GADTs, only they're not as easy to use, and they are not as typesafe. What separates GADTs from ADTs can be seen in this Java code:

class A<T> {}
class B extends A<Foo> {}
B extends A with T fixed to Foo, so instances of B have type A<Foo>, by subtyping. With ordinary ADTs, B would also need to be parameterized by T - individual type constructors of an ADT, which we've expressed here as Java classes, cannot fix a type parameter to a specific type. GADT is attractive because it's a modest extension of existing ADT theory, and yet enables a wide range of data structuring styles used in fancypants typeful programming.

Epigram is programmatically aligned with Ωmega - both are passionate about the advances in programming made possible by dependent types, and vocally call programmers and researchers to join them on their quest. Epigram, in contrast to Ωmega, goes whole hog dependent typing. This includes arbitrary type-level computation, a succinct 2D-layouted syntax, and interactive support by the development environment, that goes beyond what IDEs for ordinary languages offer (and can offer).

Coq is different from Ωmega and Epigram in that it's designed as a proof assistant, and not a dependent programming language. Adam Chlipala maintains that Coq is the most useful implementation to date for expressing complex proofs, and that systems like Epigram are more useful when proofs arise very naturally from the structure of the program and/or its data. Coq programs, such as Xavier Leroy's verified C compiler, have a different flavor from ordinary and dependent functional programs. Concoqtion has an O'Caml value level, and a Coq type level.

One problem with all dependently typed systems is that you have to deal with non-terminating type-level programs somehow, otherwise your logic becomes unsound. There are different strategies: Ωmega type-level programs are written as term rewriting systems, that have to terminate; Epigram and Coq programs are written in total languages - every program terminates; in Agda, programs are interrupted when they get stuck in a loop - soundness is regained through a separate termination check (I think). In practice, nontermination doesn't seem to be a big problem.

Some of the most interesting applications of dependent types are in the area of metaprogramming by program generation: you prove interesting static properties of your program, and then spit out a program in another language that is guaranteed to obey them dynamically. Which means that you can throw away and erase a lot of stuff at compile-time, that other languages have to remember and/or check at runtime. As Epigram implementers state, they have more information available about their programs statically, than they know what to do with. Consider: in a dependent language, once a program typechecks, you may not ever need to run it!

The existing systems for doing dependent programming all seem very closely related, and "conceptual epiphanies" can be translated between them. Dependent types are an amazing area of research & development, and I urge you to join it.

Update:

Stephanie Weirich maintains that dependent types not only aid verification, but they also increase expressiveness of a language, and that generic programming is a killer-app for dependently-typed languages.

Also: what are dependent types actually good for? I think a good example is found in Why Dependent Types Matter: it shows how to write a list-sorting function, whose type proves that the output lists are always correctly sorted. I think a lot of software will be written this way in the near future.

Keeping up with the GNUses

Just wanted to mention that for keeping up with GNU/Linux progress, the following two sources are very good:

• Michael Kerrisk's Linux man-pages
• Nick Clifton's GNU Toolchain Updates

Split stacks!

This could be big - in the October 2010 GNU Toolchain Update (subscribe!), Nick Clifton reports that split stacks have been added to GCC. With split stacks, thread stacks can grow (and shrink (?)) automatically.

al-Khwārizmī

I think that's a great statue showing the act of algorithm design.

Program Your Size

When programming, I often find myself striving for minimalism. Trying to make the program as succinct as possible, sweating over details like how to arrange the sections in a file, or the number of files to create.

But minimalism in programming may cause programs to appear cramped, may persuade you to choose forms of expression that are unneededly terse, and may also lead to programs that are hard to refactor or extend.

Point is, when you start programming, you don't know how big the program's gonna be, so starting with minimalism may be a bad choice. When looking at the sources of some huge programs, I found that some of them have found very relaxed ways to deal with their sprawling size. Gnus for example comprises dozens of large source files, containing hundreds or thousands of operational definitions, and yet remains very readable.

I don't want to get into the details of architecting large programs - I'd rather like to focus on a way to write programs, from the start, so that the source then has a "density" that's adequate to its size. Gnus for example is meandering, and that's perfectly adequate - Gnus being a mail reader for the most customizable OS in existence. That's a job that's never done, so the source should reflect that - you can't write a cute blog post about a program like Gnus, there's no single overarching, minimalist design principle.

Maybe, as Perlis said, every program needs to be written at least twice. After the first run, we know the approximate size of the program, and can then find a code density/terseness that's adequate to that size.

I find minimalism in source code is often limiting. In my next program, I'll write it from the start as if it were really huge.

Linus on transactional memory

I want transactional memory like the next guy, but comments like this one by Linus indicate that we still have a long way to go:

So that's what it boils down to: transactions are "free" and a wonderful way to elide those horrible expensive locks.

But only if you never make a mistake.

They are expensive as hell even for very low rates of transaction failures. And you really cannot know statically (even if you don't end up reaching some transaction limit, you may easily end up just having heavy contention on the data structures in question).

So I claim that anybody who does transactional memory without having a very good dynamic fallback is basically totally incompetent. And so far I haven't seen anything that convinces me that competence even exists in this area.

The ghosts of blog posts past

Ah, blogging. On the one hand there's value to reading someone's opinion unfiltered and raw. On the other hand it creates a lot of friction, and pisses people off.

This is a blog. It is a special medium. I'm not writing articles, which I expect to stand the test of time. I don't let my friends preview the posts I write, and point out their problems. Because I think there's a difference between writing articles (as, say, Paul Graham does) and blogging. And both have merits. This is a blog.

It presents my opinions and mood at a specific point in time. If you don't like it, argue with me, but don't take it too seriously. Take my posts like snarky or humorous remarks over a beer. That's how I write them. Because that's what I think is one of the things blogs are good for, and that's how I'm running this particular blog.

-- Manuel

The far side of the lambda cube

Of course, once you investigate higher-order types, you begin to think about unifying the type and term levels.

Reading a bit about this I found some interesting links:

Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic. A recent paper I found via Ahmed, Findler, Siek, and Wadler's new Blame for All. I find the use of a counter-example database in a compiler a bit frightening, though.

Henk: A Typed Intermediate Language, from 1997, by SPJ and Erik Meijer:

There is growing interest in the use of richly-typed intermediate languages in sophisticated compilers for higher-order, typed source languages. These intermediate languages are typically stratified, involving terms, types, and kinds. As the sophistication of the type system increases, these three levels begin to look more and more similar, so an attractive approach is to use a single syntax, and a single data type in the compiler, to represent all three.

The theory of so-called pure type systems makes precisely such an identification. This paper describes Henk, a new typed intermediate language based closely on a particular pure type system, the lambda cube. On the way we give a tutorial introduction to the lambda cube.

Languages of the Future, by Tim Sheard on Omega, on which I'll post something soon.

And, Your lambda-cube is puny.

A moment of respectful silence, please.

Higher kinds are sexier

In the process of formalizing generics for my Lisp, I'm also studying FGJ_ω again, the extension of Featherweight Generic Java with higher kinds. Instead of just parameterizing types with first-order types, such as T, you can parameterize types with type-level "functions", such as F<T>. One example of such a function is the type List<T> - you give it a T, and it "returns" the concrete type of lists containing that type.

And it turns out, the theory behind that looks simpler, and thus sexier:

(types)             T ::= (K K*)
(type constructors) K ::= X | C | (P* => T)
(type param defs)   P ::= (X P*) | (<: (X P*) (C K*))
(class defs)        D ::= DEFCLASS (C P*) ((C K*)*)
(method defs)       M ::= DEFMETHOD (m P*) ((param T)* -> T)

I like the definition of types: a type's the application of a constructor to zero or more other constructors. Constructors may be variables (X), classes (C), or functions taking zero or more parameters and returning a type. (So you basically have a lambda calculus at the type-level.) A type parameter is a variable constructor with zero or more parameters, optionally bounded to a class type with zero or more type arguments. Class definitions are parameterized over zero or more type parameters, and extend zero or more existing classes. (I'm taking some liberties with adding multiple inheritance, hoping it doesn't mess up the theory. :P) Method definitions are, as usual, parameterized on the type- and term-level and have a result type.

It's kinda embarrassing to post this stuff here, since I'm so bad at type theory, but I think I can make it work. One insight giving me this faith is that none of this stuff survives till runtime: at runtime, only concrete instantiations, such as List<String> remain. Or so I hope.

Formalizing generics

In the previous post, Minimal generics for an untyped language, I've discussed some basic requirements for the implementation of parametric polymorphism in the Lisp I'm working on.

I've now made some progress in formalizing this, based on Featherweight Generic Java. Here's a basic overview of the type system in the FGJ style:

(types)       T ::= C | X | Top
(classes)     C ::= (klass T*)
(class defs)  D ::= DEFCLASS (klass (<: X C)*) (C*) ((slot T)*)
(method defs) M ::= DEFMETHOD (method (<: X C)*) ((param T)* -> T)

Types are either class types (C), type parameters (X), or Top. Class types have a name (klass) and zero or more types as parameters. A class definition introduces a named class, parameterized over zero or more type parameters that have class types as bounds, zero or more superclass types, and zero or more named and typed slots. A method definition introduces a named method, parameterized over zero or more type parameters that have class types as bounds, with zero or more named and typed parameters and a result type.

Type parameters in a class definition or method definition (X) are scoped over the entire definition, including the bounds (in the style of F-bounded polymorphism).

All of this is pretty much equivalent to FGJ. The only difference is that classes do not contain methods.

[Updates: I've added type parameterization to method definitions. Added Top. Added some parentheses to make the syntax unambiguous.]

Minimal generics for an untyped language

So, I'm developing a Lisp, which means I have to support untyped, dynamically type-checked code in any case. But I still like typeful programming.

Generics, or parametric polymorphism, are jolly useful, even on a totally limited scale: all I want from the first round of this endeavor is to support something like the following:

(defclass (list T))
(defmethod add ((list (list T)) (element T))
...)

Here, I define the class (list T) - a list parameterized over the type of its elements, T. That's the same as Java's List<T>. The method ADD takes such a list and an element, and adds it to the list.

To create an instance of a parameterized class, you have to pass a concrete type argument to use for the element type, as in:

(defvar *my-list* (make (list string)))

This creates a list that accepts strings (and instances of subclasses of string) as elements.

The instance has to remember that it's a list of strings for type safety. When ADD is called on a list, the runtime needs to check that the element type matches:

(add *my-list* "foo") ;; OK
(add *my-list* 12) ;; runtime error

One more thing I'd also like is the following;

(defclass (foo (<: X bar)))

That's a class foo that has one parameter, that must be a subtype of bar, analogous to Java's Foo<X extends Bar>. Being able to give such a bound to a type parameter seems quite essential.

Furthermore, it has to be possible to pass on type parameters to superclasses, as in:

(defclass (super-1 T))
(defclass (super-2 T))
(defclass (klass X Y) ((super-1 X) (super-2 Y)))

(klass X Y) is parameterized over two types, X and Y, and passes them on to its two superclasses, each of which is parameterized over one type.

Of course, it also has to be possible to remove parameterization, as in:

(defclass string-list ((list string)))

This defines an unparameterized class string-list, which is a subclass of (list string).

Another requirement is that it has to be possible to create instances of type arguments, as in:

(defclass (klass T))
(defmethod make-a-new-t ((k (klass T)))
(make T))

That's just cute, and may have some applications to dependency injection.

I'd also like to be able to write polymorphic functions:

(defun identity ((a T) -> T) a)

The arrow indicates the result type of the function. In this case it takes an instance of any type and returns it.

It should also be possible to give slots (member variables) of classes the types of type parameters:

(defclass (klass X Y) ()
((slot-1 X)
(slot-2 Y)))

This defines a class with two type parameters X and Y, (no superclasses,) and two slots slot-1 and slot-2 with the types X and Y, respectively.

These are the basic requirements. Now I need a plan! ;)

Fast dynamic casting

Fast dynamic casting, a cute paper by Michael Gibbs and Bjarne Stroustrup:

We have demonstrated that it is possible for a linker to generate integer type IDs for classes such that it may be verified by a simple integer modulo computation that one class derives from another in an object-oriented language. When combined with a suitable way of adjusting offsets, this method provides for a fast, constant-time dynamic casting algorithm. A 64-bit type ID is capable of representing quite large class hierarchies containing thousands of classes and at least nine levels deep.

I knew that prime numbers could be used for this somehow, but these guys have already worked it out.

Relatedly, I've also been thinking about using perfect hashing to implement multiple dispatch. It should work just fine, and actually reduce the number of type tests, compared to single dispatch. Unforch, I'm still in the make-it-work phase, which is followed by the make-it-correct phase. Only then does the glorious make-it-fast phase start.

Programmer feel-good quote

From a bit to a few hundred megabytes, from a microsecond to a half an hour of computing confronts us with completely baffling ratio of 10⁹! The programmer is in the unique position that his is the only discipline and profession in which such a gigantic ratio, which totally baffles our imagination, has to be bridged by a single technology. He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. — E.W. Dijkstra

The three great virtues of programming language designers

Diligence, Patience, Humility.

The many forms of polymorphism

It's important to realize that different kinds of polymorphism in type systems can be quite orthogonal.

Here are some forms of polymorphism, from Types and Polymorphism in Persistent Programming Systems by R.C.H. Connor:

ad hoc: An operation is defined over a number of different types, and its semantics may depend upon the type of its operands. An example is the operator "+", which may be defined over integers and reals, and has a different interpretation for each type.

parametric: Instances of the same type within a type description may be abstracted over by an implicit or explicit type parameter. An example is an identity function, where although the parameter and result may be of any type, they are statically known to be the same type.

inclusion: The type of a value may be partially abstracted over, so that unnecessary type information need not be stated. An example is a function which is defined over any record value which has an age field of type integer.

He further writes:

All of these language concepts have evolved independently from each other. Languages such as early assemblers contained no polymorphism whatsoever. Ad hoc polymorphism was the first to appear, in languages such as Fortran, which defined overloaded operators, such as "+", along with the ability to coerce values from integer to real according to the use of such operators. Parametric polymorphism appeared in ML, and inclusion polymorphism in Simula. Existentially quantified types as described by Mitchell and Plotkin is a model of abstract data types which introduces abstraction over a type description, and such types are included in the definition of parametric polymorphism given above.

The motivation for all of these diverse language models is the same: the need to abstract over type. As type systems include more static constraints, then flexibility is lost as well as safety gained. Some of this flexibility, however, may be regained without the loss of safety by the introduction of type abstraction. Polymorphism is viewed here not as some theoretical attribute of type systems but as a solution to a class of practical problems which require type abstraction.

I, for one, welcome our new, optically-interconnected blade overlords

The IBM hub module brings 48 10Gbit/s optical links to a Power7 board.

From Choosing VMs to Feng Shui for HCI

There's a nice discussion going on in the LtU thread Choosing a VM for a concurrent language. Some quotes, out of context:

Sean McDirmid:

I'm sick and tired of PL papers that present a novel language idea and then justify it with...a formal model...huh? This is a logical fallacy of the shaggy dog variety.

David Barbour:

developing a new language is also nigh completely pointless unless there is something useful and interesting you can say about it. ...

Usage doesn't justify a design. Valid technical design seems to be a relatively minor factor in market success. ...

most attempts to achieve 'ease-of-use' and 'ergonomics' involve guidance by reasoned principles... a sort of Feng Shui for HCI (which holistically includes PL).

Matt Hellige:

Programming languages are tools that require significant investment of time to learn to use well. To a large degree, their value is measured in terms of how valuable they are to the people who know them best.

No more "minimal early Lisps", pulleezz

If there's one thing that irritates me about the pg-led Lisp renaissance it's the fascination with the Ur-Lisp. Rewriting that Ur-Lisp has become a pastime. Here are just some of the reasons I think that's dumb:

Lisp is a bad model if you want some kind of axioms of computing

We already have the lambda calculus for that, and you can build a real language with that (see Haskell). If you want to write some minimal thingy in C, consider writing a Haskell, not a Lisp.

That you can write a Lisp evaluator in Lisp was interesting in 1959 (and maybe 1960), and let's face it, that Ur-Lisp was one broken language.

Car, cdr, wtf?

Contents of the address part of register, contents of the decrement part of register, what the fuck? What are they doing in a language, even a toy, written in 2010? Please use data structures.

Where are the closures?

If you're looking for a challenge, as opposed to redoing something that's been done ad meam nauseam for half a century fachrissakes, try to find a minimal and explainable way to do closures. Bonus points for efficient flat environments. Languages without closures are so 1959.

Where are the macros?

A Lisp without macros is meaningless.

Where's the control flow?

A Lisp without some kind of continuations and condition system is useless.

Where are the semantics?

If you read the RnRS attentively, you'll see that Lisp has evolved a deep and subtle set of semantic concepts, none of which feature in the Ur-Lisp.

What's the purpose?

Surely you're not learning much by repeating JMC's flawed Ur-Lisp from 1959. If you want to learn something, implement a language with closures and macros. If you want to learn more, make it a compiler. If you want to blow your head, implement hygienic macros or a higher-order module system or a static type checker. That's today's standard.

Look, Lisp is such a great language, but if anything we have to push it harder, not continuously go back to 1959.

Update: More fully-featured, modern Lisps, pulleezz

Dalvik DEX

Good binary formats rock. Reading the ELF spec was quite eye-opening for me.

Dalvik's DEX format is another nice one.

Interestingly, Dalvik is the brainchild of Dan Bornstein, who was at Kaleida Labs (RIP), where he worked on ScriptX, one of the many avant-garde codes that fell victim to the WWW-induced ice age of GUI innovation.

The 2010 Linux Storage and Filesystem Summit

As usual, Jonathan Corbet does an admirable job of informing us on happenings in kernel land in his summaries of The 2010 Linux Storage and Filesystem Summit, day 1 and day 2.

On testing:

It was suggested that the real test should be "put the new code on the Google cluster and see if the Internet breaks."

On Google:

There are two fundamental types of workload at Google. "Shared" workloads work like classic mainframe batch jobs, contending for resources while the system tries to isolate them from each other. "Dedicated workloads" are the ones which actually make money for Google - indexing, searching, and such - and are very sensitive to performance degradation. ...

The workloads exhibit a lot of big, sequential writes and smaller, random reads. Disk I/O latencies matter a lot for dedicated workloads; 15ms latencies can cause phone calls to the development group.

Meta: Blogging is difficult

The Axis of Eval is my second blog, after the venerable plans within plans within plans. (Yeah, there were others.)

Both of these blogs have gone through the same stages:

1. A few days of writing in solitude with a couple of friends.
2. Chris Neukirchen mentions the blog on Anarchaia or Trivium.
3. Al3x twitters about it.
4. Attack of the unwashed HN masses (just kidding).

It's hard to go from 1 to N. The rush of thousands of readers is great, but it's confusing (being able to write to thousands of peers in real-time isn't really accounted for by our DNA and social structure). For me, it's kinda hard to write when I know that a post I write will show up in the inboxes of many people most of which I don't know.

I'd like to keep a certain entertaining and informative niveau, and in the best case, I'd also like to improve it. In the early days, aggressive diss-posts and funny flames flow freely, because the audience is small and trusted. And those posts are entertaining. But in a more public setting, I have a bit of a bad feeling writing them, because I feel they may harm people I write about, when all I'm intending is to vent about some ideas I think are bad or ridiculous, or would like to tell a stupid joke.

So, what I want to say is that there are some difficulties to blogging that are seldom written about, and I'm still trying to figure out the boundaries of this strange new thingy, and where to draw the line between fact and fiction in blogging.

--Manuel

No Paranoia Rule

Good rules are few and far between in the programming scene.

The first time I heard of what I now call the No Paranoia Rule was in the following comment by Luke Gorrie on LtU:

"Oh my, what if Luke installed an exception handler that ROT13 encoded every string on the heap, then how would Jane debug her programs?"

I hear that early on, people opposed subroutines for similar reasons. And of course, macros are frequently criticised for their potential of wreaking havoc.

But that's where the No Paranoia Rule comes into play. Stop being paranoid, and don't discount language features for their potentially devastating effect.

As Luke further states,

This [being paranoid] is not the way to illumination.

(Clemens A. Szyperski coined the term No Paranoia Rule.)