17 posts tagged “computer science”

A Fine Rant For Colleagues To Read

Apr 28, 2009
Post a comment

The Problem With Software Transactional Memory: Your Languages Still Suck.

He's right, too. Parallelism is a bitch. Anyone who has ever had this experience...

Classic threads and locks (or threads and synchronized, for you Java programmers) lead to the worst sort of Heisenbugs. True story: I once had to trace down a race condition that, doing several thousand tests per second, only manifested itself once every four days on average. The vast majority of the time it’d work just fine- the rate of failure was small enough it had escaped testing (think about it- you’ve been running the same test, thousands of times a second, for three days, and it hasn’t failed yet- when do you declare that it looks like the test is working?), but it was common enough that it was causing our customer to lock up about once a week, so it had to get fixed. Oh, and threads and locks aren’t compositional- you can’t take two hunks of code which are individually correct, and combine them to form one large, correct, piece of code. But hey, it’s not like code reuse is that important to programmers, is it?

...doesn't need to be told how symmetric multiprocessing with traditional threads and locks is the shadow of death, the mindkiller, a road of bones down which nothing but torment and pain will you ever find.

An Abstract Machine

Mar 12, 2009
Post a comment

I seem to have one. Here's the OCaml signature. The module file is all of 250 lines at this point, but I expect to define a lot of built-in processes for the preamble. That will bloat out the module file.

type 'a t
module Op: sig
val ( >>= ): 'a t -> ('a -> 'b t) -> 'b t
end
val return: 'a -> 'a t
val eval: unit t -> unit
type n
type repeat = Once | Always
val nil: unit t
val start: unit t -> unit t
val lambda: n t
val nu: n t
val fusion: n -> repeat -> n list -> unit t -> unit t
val v_void: n
val v_true: n
val v_false: n
val if_then_else: n -> unit t -> unit t -> unit t
type dio = D_in | D_out
val def: dio list -> (n array -> unit t) -> n t
val preamble: n Name.Map.t t

Basically, the abstract machine is a monad. I'll compile programs into an abstract syntax tree, then when the tree is pruned until it conforms to all the syntax and semantics invariants, I'll visit the nodes to compose a monad value. I'll execute the program by evaluating the monad. To say that it will not be fast is an understatement of Brobdingagian proportions. It will be simulating concurrency in a single thread of control, which will seem like a wide miss of the whole point. It will, however, allow me to experiment with higher-level language syntax and semantics for a while before I hit the next wall, where I expect I will need to write a byte code interpreter in C with POSIX threads to make further progress.

Toward An Abstract Syntax

Mar 9, 2009
Post a comment

I continue to noodle around with an abstract syntax for types in my internal language. (Sigh. This is taking forever.) Here's what I'm looking at now:

τ ::= α | ν⟨σ⟩ | λ(σ)

σ ::= ∀δ,σ | ∃α,σ | τ,σ | ϵ

δ ::= α | α = τ | α > τ

Explanation. A type (τ) is either a named type variable (α), or a channel type of shape (σ) with either λ- or ν- binding. A shape (σ) is a list of universal quantifications, existential quantifications and type declarations terminated by the shape terminator code (ϵ), i.e. a channel that carries no types or values has type ϵ. The universal quantification is enriched with flexible (>) and rigid (=) constraints.

Some syntactic sugar is useful. The trailing ϵ in a shape can be elided from the bracketed expression in a λ- or ν- type expression, i.e. ν⟨α,β,ε⟩ can be written ν⟨α,β⟩. If the shape of a channel type expression has only one term before the ε, then the brackets/parentheses may be elided, i.e. λ(α,ε) can be written λα.

I'm still going back and forth with myself over where the λ's and ν's belong.

Monads In The π-Calculus

Mar 9, 2009
Post a comment

While I was in the shower this morning, it occurred to me that I should make a note for myself about how monads work in the polyadic D-fusion calculus.

The type construction is simply a channel (να) for sending a value of the underlying type.
The unit function is a channel (να λ(λ(να))) for sending a value of the underlying type and receiving a responsive channel that carries the resulting monadic value.
The binding operation is a channel (να ν(να λ(λ(νβ)))) λ(λ(νβ))) for sending two values, 1) a monadic value of type α and 2) a channel for sending a value of the underlying type α and receiving a responsive channel that carries the resulting value of monadic type β; the binding operation channel also permits receiving a responsive channel that carries the resulting value of monadic type β.

Easy as cake.

Note: the process defined according to the type above for the binding operation always starts when both inputs are available. There are two possible optimizations here: one where the process begins immediately when the value of monadic type α becomes available and one that begins immediately when the bound channel becomes available. The description of these types is left as an exercise.

Update: I made some consistency errors in the first revision of this post, so I went back and edited it to correct errors.

Curried Actions In The Polyadic π-Calculus

Feb 28, 2009
Post a comment

When you're building a concurrent functional programming language around an internal language derived from the π-calculus, it's a known strategy [c.f. Pict, by Pierce and Turner] to allow applicative expressions to be used in the place of π-names in action prefixes. These are a kind of syntactic sugar that expand to a concurrent process that produces the result of function application on an ephemerally bound name that takes the place of the expression.

I've been thinking lately about how currying might work in this syntax. It's doable, but I'm not sure it can be done implicitly the way OCaml and Haskell do it, i.e. where it always makes sense for the programmer to use the curried syntax over the uncurried syntax, because A) it's more flexible and B) it's faster (the uncurried form involves more boxing).

In OCaml, you can define a function like this:

let f u : int -> int -> int =

printf "u=%u\n" u;

fun v -> u + v

When you call that function with a partial application of only one argument, as in let x : int -> int = f 5 in ..., the printf function is called and the result is a function object that adds 5 to its integer argument and returns the result without printing any further output.

I'm not sure how OCaml does this, but it does.

What I want is a similar thing in the D-fusion calculus [a derivative of the π-calculus I've mentioned previously]. I think it might be doable, but I haven't figured it out yet. It seems like the arrow type operator actually needs to be a constructor in the derived syntax. The core internal syntax needs to allow for various principle channel sorts to appear in the derived syntax as expressions involving the arrow operator.

In other words, consider this derived type expression for a binary function in two polymorphic types:

∀α β. α → β → α

It can be derived from two different internal language principle type expressions that can be used equivalently in functional expressions so long as the compiler keeps track of things properly:

A :: ⟦ ∀α β. να νβ λ⟦ λα ⟧⟧

B :: ⟦ ∀α. να λ⟦ ∀β. νβ λ⟦ λα ⟧⟧⟧

The type expression in A) means send two names, one of type α and the other of type β, and receive one name of type ⟦ λα ⟧ where the response will arrive. The type expression in B) means send one name of type α and receive a name of type ⟦ ∀β. νβ λ⟦ λα ⟧⟧ where to send another name of type β and receive a name where the response will arrive. A functional definition where B and A are not equivalent processes would need to be recorded in the compiled module in pretty much the same way that OCaml does its magic.

I need to figure out how to handle that. I think, but I'm not sure, that this is what goes on inside compile interface files in OCaml. The signature says 'a b. 'a -> 'b -> 'a, but the .cmi file says the moral equivalent of "here is the address for partial applications in one variable, and here is another address for full applications in both variables."

More Math Noodling

Feb 26, 2009
Post a comment

Last night, I think I figured out some important things about the π-calculus.

p1. I believe there is a monadic D-fusion calculus in which it is possible to elaborate the canonical polyadic version described in the paper by Boreale, Buscemi and Montanari. (I don't think this is particularly surprising.)

p2. I believe I can elaborate the monadic D-fusion calculus with Milner's π-calculus. (It's possible, though it seems unlikely, that this is a novel observation. Of course, it's also possible that I'm wrong, and I don't really understand the D-fusion calculus.)

p3. I suspect— though, I can't say I'm very confident— that I will soon have a sorted derivative of the polyadic D-fusion calculus (at least, the D-fusion calculus as I understand it) in which I may be able to elaborate ML^F as described in the paper by Botlan and Rémy. [This, I believe, would be a noteworthy achievement.]

Naturally, because I am just a simple-minded code-monkey and not a real mathematician, I'm pretty much incapable of publishing results in the conventional manner with any hope of them surviving peer review. Maybe, if I get some spare time today, I'll buy a download of MathType and start trying to write up my thoughts in something approaching the conventional format for such things. What's the worst that can happen? (Answer: I'll be branded as a kook.)

Update: Ah, I see where I went wrong in p2 now. I forgot how the D-fusion calculus really is strictly more expressive than Milner's π-calculus because the scope of λ-bound variables can be weakened via the λ- OP E N rules. Okay, now I'm back on track.

I May Be On The Verge Of Inventing Something Here...

Oct 17, 2008
Post a comment

I just got through writing up my initial notes for a concurrent, real-time garbage collector for the parallel systems programming language I'm designing. (I've got a well-thumbed copy of Richard Jones's and Rafael Lins's book in front of me while I do this.) This is a short note to describe where I'm going.

My collector is a variant of the Leroy-Doligez-Gonthier collector for Caml Light, but I've got a sneaky trick up my sleeve that stems from the fact that my language is implicitly parallel. Here's the brief version of my notes...

The minor heap is reserved for immutable data, just like in LDG. I'm not sure yet whether I'll even allow mutable data in the major heap. (There's a part of me that wants to quarantine all the mutable data off in the foreign function interface, but I'm not sure I want to be that much of a jack-booted fascist yet.) The other evil thing I'm planning to do, at least for the virtual machine prototype implementation, is to use the Cheney On The M.T.A. strategy for allocating the minor heap directly on the C-language call stack.

None of that is really new.

Here's what I think might be new: a scheduling kernel in the runtime environment for the language that contains an arbiter for shifting pending work queue items from busy cores to available ones. This shifting is a special case of copying from the minor heap into the major heap. The scan can be done in parallel by one or more competing execution contexts, even while the engine for the original work queue is collecting its own minor heap. Because the C stack duals as the minor heap, this will be trivially easy to do.

My only worry is about how badly I will blow up the cache with all the calls to OSAtomicTestAndSet I'll be making. (No, I don't give a rat's ass about any platforms other than Mac OS X right now. Thanks for asking.) Hey, it's just a prototype though— the whole point is to figure out where the performance bottlenecks are located, then lean into them hard with the power tools. This will be fun.

Once Again, The Americans Blow It...

Oct 9, 2008
1 comment

I should have known the Eurozone would have done what I've been trying to do.

Update: I've now read the paper, and I was struck by how many things I had been failing to achieve that the authors of this paper also think are unachievable with a proof assistant. They selected a labeled transition system instead of a theory of structural congruence. At the end of section four, they explain why structural congruence is so painful (but cut and paste doesn't work, and I'm too sick with a ear/throat infection right now to transcribe all the math symbols by hand). Suffice to say, my understanding of why it doesn't work came at the expense of a lot of headache. I reproduced exactly those results with Twelf.

I also don't feel too bad about not succeeding. The problem is apparently not one for beginners. Consider the paragraph introducing section 4:

This is one of the most important sections of the present paper. In it we report a very substantial case-study of formal verification development in Coq, namely the theory of the π-calculus developed in [Milner92, section 2]. This enterprise is significant from various viewpoints. To our knowledge, it is one of the largest case-studies involving co-inductive types. But furthermore, it is perhaps the first serious attempt of using higher order syntax á la Church in metatheoretical studies outside type theory.

Okay, I don't feel too bad. I knew there were issue revolving around co-induction and higher-order syntax. I didn't know I was treading into a part of the mathematical landscape that has not been explored very deeply.

Okay, That Was A Bad Idea...

Oct 8, 2008
Post a comment

I'm think I'm through fighting with Twelf. It's theorem prover is almost useless. The whole reason I taught myself how to use the thing was the hope of not have to write the goddamn theorems myself. However. Even if it can't find a proof of a theorem, it would still be nice to have more feedback than a pegged CPU meter and a hung console, which when you interrupt it, it says: %% ABORTED %%.

I wonder if MetaPRL is what I should be using.

Why My Head Still Hurts

Sep 29, 2008
2 comments

I'm still climbing the Twelf learning curve.

Learned in painful ways the difference between the %total and %terminates assertions, and now I know when to use one and not the other. Basically, %terminates is for hypothetical judgments, and %total is for meta-theorems. I don't know how I didn't get this before, but I now understand that you use %terminates when you need to prove that the acceptable inputs produce the required outputs, and that you use %total when you need to prove that all the possible inputs produce the required outputs.

So, that's all good. I've been struggling to figure out how to prove sort-preservation in the sorted polyadic π-calculus, and that isn't working. I keep going back to the monadic version and painting myself into a corner. I suspect some of the informative text in Chapter 9 of Milner's book warns against trying to do the thing I've been failing to do. I should have listened. It's never a good idea to second-guess Robin Milner. (And, I haven't even been meaning to... it's just that I keep analyzing my failures and finding out that Milner told me fifteen years ago not to do it that way.)

Anyway, as if that wasn't enough to make my head collapse from the strain, I've now discovered the D-Fusion Calculus— a variant of the polyadic π-calculus with two binding operators instead of one and a symmetry between input and output. Just when I thought I had all the weird math in Milner's book figured out, I've got yet another collection of evil Eurozone hippies hammering on my tender lobes. I am fcking doomed.

Gina is struggling her way through the undergraduate physics for earth sciences majors, and she says it's kicking her ass. I tutored physics and calculus a lot when I was in college (it was my work-study program), so I have some idea how badly she's getting pasted by it. She's working hard, but things are coming together slowly for her. I have seen people work a lot harder for worse results, but they usually fail out. She might scrape out a passing grade, but she needs encouragement that she really can do the math. She can. I've seen her do it. But she makes mistakes and gets frustrated too easily. I can almost see the wheels in her brain start grinding when she loses the plot in a homework problem: it's not just that she can't see how to do the problem; it's that she's convincing herself that she's not smart enough to see it. That's her biggest challenge, I think. I'm afraid she might drop out before she hits her stride. She's working hard, and she's learning it. She's never going to be a quantum physicist, but she can probably pass the physics class for earth sciences majors if she just keeps up her current level of effort through to the end of the semester.

She has her first big mid-term quiz today. I hope she manages to scrape out a passing grade. If she fails it, I'm going to have a lot harder time encouraging her to stick with it. I don't think the Wilbur Robinson "Keep Moving Forward" pep-talk of the century is going to work very well.

Anyway, I say all this because I'm pretty sure I know exactly how Gina feels right now. All this programming language theory I've been learning lately is scary complicated, and I'm pretty sure if I was learning it in a classroom setting, I'd fail out pretty hard. I often wonder if the reason it seems to come so slowly to me is that I'm just not smart enough to learn it sufficiently well that I can trust my intuitions with it. You can't really call yourself a scientist until you can get new results added to the literature. I'm a long way off from that: I can barely read the literature, much less have any hope of writing a paper that would be readable.

So my head hurts. A lot.