<?xml version='1.0' encoding='UTF-8'?><?xml-stylesheet href="http://www.blogger.com/styles/atom.css" type="text/css"?><feed xmlns='http://www.w3.org/2005/Atom' xmlns:openSearch='http://a9.com/-/spec/opensearchrss/1.0/' xmlns:georss='http://www.georss.org/georss' xmlns:gd='http://schemas.google.com/g/2005' xmlns:thr='http://purl.org/syndication/thread/1.0'><id>tag:blogger.com,1999:blog-8573067371275934806</id><updated>2011-11-23T15:29:33.712-05:00</updated><category term='fs'/><category term='linux'/><category term='acl2'/><category term='gsoc'/><category term='irritation'/><category term='error message of doom'/><category term='zfs'/><category term='web'/><category term='os'/><category term='icfp'/><category term='ffmpeg'/><category term='disk'/><category term='allocation'/><category term='multimedia'/><category term='proof'/><category term='meta'/><category term='get off my lawn'/><category term='great apes'/><category term='ui'/><category term='stack'/><category term='icfp2007'/><category term='soekris'/><category term='coq'/><category term='algol'/><category term='value restriction'/><category term='tips'/><category term='ppc'/><category term='spam'/><category term='human input devices'/><category term='sun'/><category term='realworld'/><category term='ocaml'/><category term='popularity'/><category term='performance'/><category term='integers'/><category term='netbsd'/><category term='insn'/><category term='naming'/><category term='runtimes'/><category term='compiler'/><category term='hardware'/><title type='text'>rlwinm</title><subtitle type='html'>Jed's Serious Technical Blog</subtitle><link rel='http://schemas.google.com/g/2005#feed' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/posts/default'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default?max-results=100'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/'/><link rel='hub' href='http://pubsubhubbub.appspot.com/'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><generator version='7.00' uri='http://www.blogger.com'>Blogger</generator><openSearch:totalResults>26</openSearch:totalResults><openSearch:startIndex>1</openSearch:startIndex><openSearch:itemsPerPage>100</openSearch:itemsPerPage><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-4364501528770053401</id><published>2009-09-04T02:38:00.003-04:00</published><updated>2009-09-04T03:03:26.111-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='soekris'/><category scheme='http://www.blogger.com/atom/ns#' term='hardware'/><title type='text'>Soekris net4526 JP3 (GPIO) pinout</title><content type='html'>This thing gets indexed by Google, so I'll post this here for the next person who wonders.  (I've also updated &lt;a href="http://acelere.net/twiki/bin/view/Soekris/PinoutSummaryNet4526"&gt;some random wiki page&lt;/a&gt; I wound when googling, and should probably mail the soekris-tech list while I'm at it, but probably won't do that tonight.)&lt;br /&gt;&lt;br /&gt;Anyway.  &lt;a href="http://www.soekris.com/net4526.htm"&gt;The Soekris net4526&lt;/a&gt; single-board computer has on it an 8-bin header connector labelled JP3, which is known to carry five &lt;a href="http://en.wikipedia.org/wiki/GPIO"&gt;GPIO&lt;/a&gt; lines.  However, Soekris Engineering hasn't released a manual for the net4526, only for the related net4501, and the only related traffic I found on their mailing list was someone who had figured out some of the pins and was asking for help with the others.  (Which is odd, because I thought I'd seen a complete pinout posted there at one point.)&lt;br /&gt;&lt;br /&gt;So, since I have a project that might need this feature, I went in and tested myself, and (arranged like they are here, with the JP3 label upright):&lt;br /&gt;&lt;br /&gt;&lt;tt&gt;1: +3.3V     2: +5V&lt;br /&gt;3: GPIO 7    4: GPIO 8&lt;br /&gt;5: GPIO 11   6: GPIO 21&lt;br /&gt;7: GPIO 22   8: GND&lt;/tt&gt;&lt;br /&gt;&lt;br /&gt;I saw some talk about GPIO numbers in octal or something, so I will add: those are in decimal and zero-indexed, as accepted and reported by NetBSD's &lt;tt&gt;gpioctl(8)&lt;/tt&gt; command.  ALso, I have independently confirmed those of the pin assignments noted in &lt;a href="http://lists.soekris.com/pipermail/soekris-tech/2004-October/007030.html"&gt;the mailing list message I mentioned.&lt;/a&gt;&lt;br /&gt;&lt;br /&gt;Know further that the pins' input mode has an internal pullup.&lt;br /&gt;&lt;br /&gt;The connector I ginned up for the header is also… &lt;i&gt;interesting&lt;/i&gt;, and may deserve a post of its own.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-4364501528770053401?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/4364501528770053401/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=4364501528770053401' title='1 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/4364501528770053401'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/4364501528770053401'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2009/09/soekris-net4526-jp3-gpio-pinout.html' title='Soekris net4526 JP3 (GPIO) pinout'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-6904692106584173891</id><published>2009-07-14T00:52:00.006-04:00</published><updated>2009-07-14T02:43:41.581-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='gsoc'/><title type='text'>The truth is also a three-edged sword.</title><content type='html'>But these are a different three from the canonical ones for understanding.  Of course I'm talking about the RAIDframe stuff, because that's all I seem to get around to posting here.  Anyway, there's what we believed at boot, what we know now, and what we want to be believed on the next boot.  For the code I've written, they're fields of the same struct.  For the existing &lt;tt&gt;raid(4)&lt;/tt&gt; code, the information can be a bit more… &lt;i&gt;scattered&lt;/i&gt;.  (Making things slightly more fun: all the metadata for a RAID set is replicated on each component, so there's the question of what to do if there are non-fatal differences.)  My SoC mentor has noted that things could use some reorganizing there, and part of me would like that too, but a much larger part of me says It's Working Code, Leave It Alone.&lt;br /&gt;&lt;br /&gt;This notion applies to fault-tolerant persistent data systems in general, really; there, as with RAIDframe, the first item is relevant only until some kind of roll-forward is done to clean up after a failure.  In RAIDframe's case, this is &lt;tt&gt;raidctl -P&lt;/tt&gt;, and it's a little more prominent because it runs in parallel with, to borrow a term, the mutator; contrast with &lt;tt&gt;wapbl(4)&lt;/tt&gt;'s roll-forward, which is done automatically on mount, appears to be quite quick, and I assume blocks use of the filesystem until it's done.&lt;br /&gt;&lt;br /&gt;(In the other half of my life I'm looking at the literature on persistence, and it's almost odd how these two things are converging here.)&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-6904692106584173891?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/6904692106584173891/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=6904692106584173891' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6904692106584173891'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6904692106584173891'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2009/07/truth-is-three-edged-sword.html' title='The truth is also a three-edged sword.'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-8080103062061457650</id><published>2009-06-12T01:14:00.002-04:00</published><updated>2009-06-12T01:28:46.905-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='gsoc'/><title type='text'>It Is Written</title><content type='html'>What I'll call a first draft of the RAIDframe parity map stuff is written, and compiles and links, and if run will actually do something.  That something will, in practice, probably involve bugs.&lt;br /&gt;&lt;br /&gt;Now to get my &lt;a href="http://en.wikipedia.org/wiki/QEMU"&gt;QEMU&lt;/a&gt; setup into something more resembling a useful state, because the time I spend on that will almost certainly be paid back by not waiting for my test box to reboot, and I've been meaning to deal with that anyway.  Once this gets to the point of serious benchmarking I'll need to use actual hardware for the most part, of course.&lt;br /&gt;&lt;br /&gt;The RAIDframe codebase, incidentally, is… not unelaborate.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-8080103062061457650?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/8080103062061457650/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=8080103062061457650' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8080103062061457650'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8080103062061457650'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2009/06/it-is-written.html' title='It Is Written'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-8527789621657007432</id><published>2009-06-11T02:15:00.005-04:00</published><updated>2009-06-11T03:00:21.207-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='gsoc'/><title type='text'>The RAID Project: Things Not To Do</title><content type='html'>&lt;ol&gt;&lt;li&gt;Let writes to the RAID hit the disk before the corresponding parity map bit is set on disk.&lt;/li&gt;&lt;br /&gt;&lt;li&gt;Let writes to the RAID hit the disk after the corresponding parity map bit is cleared on disk.  (That is, updates which just mark regions clean again still need a barrier.)&lt;/li&gt;&lt;br /&gt;&lt;li&gt;Have one write see that its region needs to be marked unclean, then do that, and then before that actually gets committed to the disk another write to the same region sees that it's allegedly already marked and just does the write, which happens to hit the disk before the parity map update and then the power goes out at that exact moment.&lt;br /&gt;&lt;br /&gt;This may not even be possible — I think I'll only ever be starting writes from one particular thread, given the RAIDframe architecture, though I'm not sure of that yet — and even if it is it sounds stunningly unlikely.  Which is to say that if I get this wrong I may never find out; so don't do that.&lt;br /&gt;&lt;br /&gt;Point also being that it's important to keep invariants in mind when dealing with shared-state concurrency, including those invariants that involve the state of secondary storage and the potential behavior of loosely specified hardware as well as the program's data structures proper.&lt;br /&gt;&lt;/li&gt;&lt;/ol&gt;&lt;br /&gt;Completely unrelatedly, I've just learned that the posting interface here rejects ill-formed HTML.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-8527789621657007432?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/8527789621657007432/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=8527789621657007432' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8527789621657007432'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8527789621657007432'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2009/06/raid-project-things-not-to-do.html' title='The RAID Project: Things Not To Do'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-1913399484905763291</id><published>2009-06-01T17:15:00.003-04:00</published><updated>2009-06-01T18:29:18.030-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='gsoc'/><title type='text'>Parity</title><content type='html'>I didn't go into too much detail about my Google Summer of Code project last time.  It is: improving RAIDframe parity handling.  And now I'm going to be excessively verbose about it.&lt;br /&gt;&lt;br /&gt;Specifically: the thing about RAID levels that provide redundancy (i.e., not &lt;a href="http://en.wikipedia.org/wiki/RAID_0"&gt;RAID 0&lt;/a&gt;) is that there's some kind of invariant over what's on the disk: both halves of a mirror are the same, or each parity block is the &lt;a href="http://en.wikipedia.org/wiki/Exclusive_or"&gt;XOR&lt;/a&gt; of its corresponding data blocks, &amp;amp;c.  And the thing about software RAID is that, if the power goes out (or the system crashes) while you're in the middle of writing stuff to each of the disks, some of those writes might happen while others don't.  Then, when the lights come back on, the invariant may no longer hold for any stripe that was being written.&lt;br /&gt;&lt;br /&gt;This is of particular concern for RAID 5, because if the parity is still wrong when (not if) a disk fails and one of the data blocks needs to be reconstructed by XORing the parity with the remaining data, you will get complete garbage instead of the data you lost.  This is bad.&lt;br /&gt;&lt;br /&gt;One solution, and the one currently used in NetBSD, is to set a flag on each disk making up the RAID when it's configured, and clear it when it's unconfigured.  If that flag is already set when the set is brought up, then there might have been an unclean shutdown requiring the parity to be recomputed.&lt;br /&gt;&lt;br /&gt;That is, requiring the entire array to be read from beginning to end.  Which, as magnetic disk drives pack more and more tracks onto their platters, inevitably takes longer and longer.  As it is, each unclean shutdown requires many hours of parity rewriting, during which the disk I/O load interferes with whatever the system's actual job is.  This is also kind of bad.&lt;br /&gt;&lt;br /&gt;It is said that the Solaris Volume Manager (which I briefly administered an instance of, but didn't have to care how it worked in this much detail) divides the RAID into some number of regions and records for each one whether its parity might be out of sync.  This seems like a simple enough idea.&lt;br /&gt;&lt;br /&gt;Except it's kind of not.  Ideally, you'd like as many of these regions to be marked clean as possible, to cut down on the parity rewriting time.  On the other hand, because you'll have to do disk seeks (and probably disk cache flushes, too, and hope the firmware isn't too broken) to set or clear a region's dirty bit, and it's absolutely essential that that bit-setting hit the disk before any writes to the region are done, you also want to hold off on marking clean those regions that you think might be getting written to sometime soon.&lt;br /&gt;&lt;br /&gt;So, if you're getting truly random I/O, then you're kind of stuck.  But, if what's on top of the RAID is some halfway reasonable filesystem that's been painstakingly designed to exhibit reasonable locality of reference, then recent write activity should (at the region level) be a decent predictor of the future.  I hope.&lt;br /&gt;&lt;br /&gt;And then there's the part of the project where I get all this integrated into the kernel, which is beyond the scope of this post.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-1913399484905763291?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/1913399484905763291/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=1913399484905763291' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/1913399484905763291'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/1913399484905763291'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2009/06/parity.html' title='Parity'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-6650851723396215615</id><published>2009-05-21T21:54:00.003-04:00</published><updated>2009-05-21T22:12:15.434-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='gsoc'/><category scheme='http://www.blogger.com/atom/ns#' term='netbsd'/><category scheme='http://www.blogger.com/atom/ns#' term='meta'/><title type='text'>The blog is alive!</title><content type='html'>This summer, I'm participating in &lt;a href="http://code.google.com/soc/"&gt;Google's Summer of Code&lt;/a&gt;, attached to &lt;a href="http://www.NetBSD.org/"&gt;the NetBSD project&lt;/a&gt; and working on fixing certain misfeatures of the software &lt;a href="http://en.wikipedia.org/wiki/RAID"&gt;RAID&lt;/a&gt; driver — more details on which later.&lt;br /&gt;&lt;br /&gt;Various other SoCers have declared their intention of keeping a weblog on their work; and, since I'm not entirely unfamiliar with the concept, I thought I might do that as well.  And this blog, being created for me to do Serious Technical Blogging (and then left to gather dust when I stopped being bothered with writing for it), and hosted by Google no less, seems like the best place.&lt;br /&gt;&lt;br /&gt;Well.  I briefly considered “blogging” by hand-writing an RSS file and giving out that URL — why, some web browsers even format RSS nicely when you browse to it — but then came to my senses.  I also considered making a separate blog (as BlogSpot has a nice interface/ontology for that), but didn't really see the point.  And, hey, tags; they're what Web 2.0 is all about, except when it's not, or something.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-6650851723396215615?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/6650851723396215615/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=6650851723396215615' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6650851723396215615'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6650851723396215615'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2009/05/blog-is-alive.html' title='The blog is alive!'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-6979273253128561738</id><published>2008-06-19T14:18:00.004-04:00</published><updated>2008-06-19T14:34:37.111-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='ui'/><category scheme='http://www.blogger.com/atom/ns#' term='web'/><title type='text'>Vocabulary Time!</title><content type='html'>&lt;b&gt;ajax&lt;/b&gt;, &lt;i&gt;v.t.&lt;/i&gt;: Of a dynamic website, to cause a user to take an unintended action (esp. one difficult or impossible to undo) because the interface rearranged itself (e.g., by removing an item from a list) in delayed response to an earlier action, concurrently with the user's attempting to activate an interface element.  Often used passively, as e.g. &lt;cite&gt;I just got ajaxed!&lt;/cite&gt;&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-6979273253128561738?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/6979273253128561738/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=6979273253128561738' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6979273253128561738'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6979273253128561738'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/06/vocabulary-time.html' title='Vocabulary Time!'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-1110383221091541029</id><published>2008-06-04T01:02:00.005-04:00</published><updated>2008-06-04T01:14:38.781-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='runtimes'/><category scheme='http://www.blogger.com/atom/ns#' term='popularity'/><category scheme='http://www.blogger.com/atom/ns#' term='allocation'/><title type='text'>Before It Was Popular?</title><content type='html'>I remember when I heard about &lt;a href="http://diehard-software.org/"&gt;DieHard&lt;/a&gt;, the probabilistic memory-safety contrivance, at a talk at &lt;a href="http://www.nepls.org/"&gt;NEPLS&lt;/a&gt;; that was &lt;a href="http://www.nepls.org/Events/16/"&gt;in 2005&lt;/a&gt;, so their PLDI paper wouldn't have existed yet.&lt;br /&gt;&lt;br /&gt;And then today I &lt;a href="http://www.hackaday.com/2008/06/03/using-multiple-browsers-for-security/"&gt;see them get name-checked on hack-a-day&lt;/a&gt; — perhaps because they've taken to promoting it as a way to increase the security of the popular web browser Firefox.&lt;br /&gt;&lt;br /&gt;Go figure.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-1110383221091541029?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/1110383221091541029/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=1110383221091541029' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/1110383221091541029'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/1110383221091541029'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/06/before-it-was-popular.html' title='Before It Was Popular?'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-2451147093320056640</id><published>2008-04-21T13:17:00.001-04:00</published><updated>2008-04-21T13:59:22.640-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='human input devices'/><title type='text'>Damn you, Microsoft!</title><content type='html'>Many people have reason to curse Microsoft, of course, but this is a bit different.&lt;br /&gt;&lt;br /&gt;Microsoft's greatest and perhaps only contribution to humanity, the &lt;a href="http://www.microsoft.com/products/info/product.aspx?view=22&amp;type=ovr&amp;pcid=a9fdd4c0-41da-4045-9d6f-f087c17ffd30"&gt;Trackball Explorer&lt;/a&gt;, seems to have become a collector's item (with second-hand prices to match!) while I wasn't looking.&lt;br /&gt;&lt;br /&gt;Mine is still working (for now), but I'd wanted to have one at home and one at school (read “in the office”), like I did at my last job, which is where I became acquainted with this device, and now that can't happen.&lt;br /&gt;&lt;br /&gt;If only I'd known or even suspected back in 2005 or so; I would have picked up a few more.&lt;br /&gt;&lt;br /&gt;But perhaps it's only appropriate, given that my extinct trackball is paired with an IBM Model M keyboard which marked its 21st birthday last Thursday.  (It was not celebrated, as I'd misremembered the date.  Oops.)  This means it can legally drink alcoholic beverages now.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-2451147093320056640?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/2451147093320056640/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=2451147093320056640' title='1 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/2451147093320056640'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/2451147093320056640'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/04/damn-you-microsoft.html' title='Damn you, Microsoft!'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-3885346748247634359</id><published>2008-04-10T18:13:00.000-04:00</published><updated>2008-04-10T19:23:06.319-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='coq'/><category scheme='http://www.blogger.com/atom/ns#' term='integers'/><title type='text'>Negativity</title><content type='html'>On Tuesday, I stayed home sick with a cold-and/or-flu (thus missing a class &lt;a href="http://www.ccs.neu.edu/home/shivers/"&gt;that might&lt;/a&gt; have held some information I hadn't yet gotten from the original paper); but &lt;a href="http://scalzi.com/whatever/?p=603"&gt;people on the Internet were arguing about religion&lt;/a&gt;.  As they often do.  And, as they often do, someone said “it’s true technically you can’t prove a negative”.&lt;br /&gt;&lt;br /&gt;This is, of course, false.  Negatives can be proven, even without &lt;a href="http://en.wikipedia.org/wiki/Law_of_excluded_middle"&gt;the law of the excluded middle&lt;/a&gt;, and even without your logic having a primitive concept of “not”.  In, say, the Calculus of Inductive Constructions, “not P” is “P &amp;rarr; False”, where “False” is an inductive predicate with no constructors, so you get your &lt;i&gt;ex falso quodlibet&lt;/i&gt; just from case analysis, and it's all terribly pretty.&lt;br /&gt;&lt;br /&gt;Anyway.  Negatives.  Even without this newfangled lambda-cube stuff, you can prove that the square root of 2 is irrational, which is to say that there &lt;b&gt;do not exist&lt;/b&gt; integers &lt;i&gt;p&lt;/i&gt; and &lt;i&gt;q&lt;/i&gt;, where &lt;i&gt;q ≠ 0&lt;/i&gt;, such that &lt;i&gt;p&lt;sup&gt;2&lt;/sup&gt; = 2 q&lt;sup&gt;2&lt;/sup&gt;&lt;/i&gt;.  This was first done around 500 BC, and the person responsible was drowned.  Modern Internet religion arguments are, thankfully(?), much tamer.&lt;br /&gt;&lt;br /&gt;So, last year, when I was first learning about &lt;a href="http://coq.inria.fr/"&gt;the Coq proof assistant&lt;/a&gt;, I used it to obtain &lt;a href="http://www.xlerb.net/misc/sqrt2.v"&gt;a machine-checkable proof of just that negative&lt;/a&gt;.  Knowledgeable readers will notice that I independently reinvented part of the &lt;tt&gt;NArith&lt;/tt&gt; library there, because I didn't know about the original.&lt;br /&gt;&lt;br /&gt;Thus, what better to do on such a Tuesday, while feverish and generally out of it, but fiddle with an esoteric logic?  Which is why I now have &lt;a href="http://www.xlerb.net/misc/sqrt2x.v"&gt;a much shorter proof&lt;/a&gt;, though I didn't bother mapping it back to the Peano numbers like I did with the other one.&lt;br /&gt;&lt;br /&gt;The next obvious thing is, of course, to prove irrational the square roots of other numbers than 2.  Or all of them!  Or at least all the primes, because it's only in prime bases that the count of trailing zeroes (&lt;tt&gt;ctz&lt;/tt&gt; ≈ &lt;tt&gt;bsf&lt;/tt&gt;) interacts with multiplication in the way needed.  (Hints: 2*5=10, 9*9=81.)  And that I eventually gave up on.&lt;br /&gt;&lt;br /&gt;But, first, I defined subtraction using specification types: given natural numbers &lt;i&gt;a&lt;/i&gt; and &lt;i&gt;b&lt;/i&gt;, return either &lt;i&gt;c&lt;/i&gt; and a proof that &lt;i&gt;a = b + c&lt;/i&gt;, or a proof that &lt;i&gt;a &amp;lt; b&lt;/i&gt;.  And then division: given &lt;i&gt;n&lt;/i&gt; and &lt;i&gt;d&lt;/i&gt; and a proof of &lt;i&gt;d &amp;gt; 0&lt;/i&gt;, return either &lt;i&gt;q&lt;/i&gt; and a proof that &lt;i&gt;n = d * q&lt;/i&gt;, or a proof that no such &lt;i&gt;q&lt;/i&gt; exists.&lt;br /&gt;&lt;br /&gt;That last one sounds trivial, but of course it isn't; there's no excluded middle, but, perhaps more to the point, the proof of that “it is or it isn't” can be converted into an actual, runnable, proven-correct OCaml program which does the division.  Not that that's very practically useful — it works on Peano numbers and does repeated subtraction (which in turn is repeated decrement).&lt;br /&gt;&lt;br /&gt;But it does mark the first time I've successfully used Coq's support for strong induction.  Twice, for the division and then for the count-trailing-zeroes, which... or, maybe instead of trying to gloss it into English, I'll just post the original type:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;Definition ctz_spec : forall n b, 1 &amp;lt; b -&amp;gt; { e |&lt;br /&gt;&amp;nbsp;&amp;nbsp;(exists2 m, 0 &amp;lt; m &amp;amp; n = expt b e * m) &amp;amp;&lt;br /&gt;&amp;nbsp;&amp;nbsp;(forall e' m, e &amp;lt; e' -&amp;gt; 0 &amp;lt; m -&amp;gt; n &amp;lt;&amp;gt; expt b e' * m) } + { n = 0 }.&lt;/code&gt;&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-3885346748247634359?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/3885346748247634359/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=3885346748247634359' title='1 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/3885346748247634359'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/3885346748247634359'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/04/negativity.html' title='Negativity'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-965324765937443889</id><published>2008-04-10T17:40:00.001-04:00</published><updated>2008-04-10T19:47:56.263-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='spam'/><category scheme='http://www.blogger.com/atom/ns#' term='irritation'/><title type='text'>The Spammers Have Won</title><content type='html'>My last post here warned, in a cryptic and laconic way, of the dangers of trusting automated processes over human judgment — to wit, it was a Google search for the result of people doing a search-and-replace on the font name “Arial” to replace it with the font name “Verdana”, but also altering content as well as markup, and partial words as well as whole.  Thus, “adversarial” &amp;rarr; “adversverdana”.  Cute, huh?  (No, I don't go trolling for that kind of thing.  I was reading one of the documents so afflicted.)&lt;br /&gt;&lt;br /&gt;Apparently, between that and the way that I'll leave this thing unattended for months while meaning to post stuff but not actually doing that thing (in part because, well, originally I'd been hoping to write actual halfway-decent posts here, not twitters-out-of-place like that), I've been declared a possible spam blog and must now transcribe letters from an image to prove my humanity in order to make or edit posts.&lt;br /&gt;&lt;br /&gt;Really?  In my last job, I got paged in the middle of the night, on weekends, on weekends in the middle of the night, and even on vacation &lt;b&gt;HOW&lt;/b&gt; many times, because some mail system had fallen over with its legs in the air from too much spam?  And I spent &lt;b&gt;HOW&lt;/b&gt; much time delicately tuning Postfix's rate-limiting, because there just wasn't enough hardware for the spam, but I didn't want to delay actual people's LKML subscriptions or whatever as collateral damage?  To get this.&lt;br /&gt;&lt;br /&gt;So, on the one hand, I can understand where the Google Overlords are coming from, but on the other hand, I'm kind of insulted.  And I usually don't take computers' opinions of me all that personally.&lt;br /&gt;&lt;br /&gt;&lt;br /&gt;Meanwhile, I note that, mysterious spam flag or no, infrequently updated or no, this blog still comes up in the first page of a Google search for... my name.  Which, as it's shared by someone famous enough to have his own Wikipedia page, is not a completely vacuous achievement.  Or something.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-965324765937443889?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/965324765937443889/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=965324765937443889' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/965324765937443889'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/965324765937443889'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/04/spammers-have-won.html' title='The Spammers Have Won'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-1679158671103964243</id><published>2008-04-01T14:32:00.005-04:00</published><updated>2008-04-01T14:39:08.896-04:00</updated><title type='text'>Word Of The Day</title><content type='html'>“&lt;a href="http://www.google.com/search?q=adversverdana"&gt;adversverdana&lt;/a&gt;”&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-1679158671103964243?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/1679158671103964243/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=1679158671103964243' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/1679158671103964243'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/1679158671103964243'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/04/word-of-day.html' title='Word Of The Day'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-8762617445203584305</id><published>2008-02-28T14:44:00.005-05:00</published><updated>2008-04-10T17:39:58.379-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='ocaml'/><category scheme='http://www.blogger.com/atom/ns#' term='value restriction'/><category scheme='http://www.blogger.com/atom/ns#' term='error message of doom'/><title type='text'>Fun with the Value Restriction</title><content type='html'>This is not a valid OCaml program:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;type 'a endo = Endo of int * ('a -&amp;gt; 'a)&lt;br /&gt;let poly = Endo ((succ 23),(fun x -&amp;gt; x))&lt;br /&gt;type thing = { u : unit }&lt;br /&gt;let mono = Endo (0,(fun { u = u } -&amp;gt; { u = u }))&lt;br /&gt;let _ = [mono;poly]&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;The typechecker rejects it, with this error message:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;File "vrmh.ml", line 5, characters 14-18:&lt;br /&gt;This expression has type 'a endo but is here used with type thing endo&lt;br /&gt;The type constructor thing would escape its scope&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;Removing the last line makes it typecheck.  As does exchanging the second and third lines, thusly:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;type 'a endo = Endo of int * ('a -&amp;gt; 'a)&lt;br /&gt;type thing = { u : unit }&lt;br /&gt;let poly = Endo ((succ 23),(fun x -&amp;gt; x))&lt;br /&gt;let mono = Endo (0,(fun { u = u } -&amp;gt; { u = u }))&lt;br /&gt;let _ = [mono;poly]&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;Yes.  Notice the mysterious action-at-a-distance.  Notice also how the type inferred for &lt;tt&gt;poly&lt;/tt&gt; (see &lt;tt&gt;ocamlc -i&lt;/tt&gt;) is not polymorphic at all, but rather &lt;tt&gt;thing endo&lt;/tt&gt;, the same as &lt;tt&gt;mono&lt;/tt&gt;.  Notice further that it would not be possible to define it with an explicit ascription of that type before the definition (i.e., outside the scope) of &lt;tt&gt;thing&lt;/tt&gt; itself.  Apparently this is bad.&lt;br /&gt;&lt;br /&gt;And then there's the reason why the type of &lt;tt&gt;poly&lt;/tt&gt; didn't have its type variable generalized, thus leaving it with the type &lt;tt&gt;'_a endo&lt;/tt&gt; and subject to unification with the type of &lt;tt&gt;mono&lt;/tt&gt;.  This is, of course, the value restriction of ML fame, which I will not explain here; but it's a little more confusing (read: I spent far too much time trying to come up with the mostly minimal test case seen here) (so, yes, this actually is something I ran into in a halfway-real program) in OCaml, where it's been relaxed in certain ways.  But not others.  For example, this:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;type 'a endo = Endo of int * ('a -&amp;gt; 'a)&lt;br /&gt;let poly = Endo (24,(fun x -&amp;gt; x))&lt;br /&gt;type thing = { u : unit }&lt;br /&gt;let mono = Endo (0,(fun { u = u } -&amp;gt; { u = u }))&lt;br /&gt;let _ = [mono;poly]&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;Is fine.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-8762617445203584305?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/8762617445203584305/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=8762617445203584305' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8762617445203584305'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8762617445203584305'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/02/value-restrict-me-harder.html' title='Fun with the Value Restriction'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-8528407927770655656</id><published>2008-01-27T00:38:00.000-05:00</published><updated>2008-01-27T02:34:38.137-05:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='os'/><category scheme='http://www.blogger.com/atom/ns#' term='great apes'/><title type='text'>Wheels Within Wheels</title><content type='html'>Exhibit A: &lt;em&gt;Hashed and Hierarchical Timing Wheels: Efficient Data Structures for Implementing a Timer Facility&lt;/em&gt;, by George Varghese and Tony Lauck, &lt;a href="http://portal.acm.org/citation.cfm?id=37504"&gt;originally in SOSP '87&lt;/a&gt; and &lt;a href="http://citeseer.ist.psu.edu/144652.html"&gt;later reappeared in 1996&lt;/a&gt; when network protocol research had caught up to it.&lt;br /&gt;&lt;br /&gt;Exhibit B: &lt;a href="http://en.wikipedia.org/wiki/Getting_Things_Done#Tickler_file"&gt;An implementation of hierarchical timing wheels for the fleshy-ape platform, due to David Allen&lt;/a&gt; (2002).&lt;br /&gt;&lt;br /&gt;&lt;br /&gt;&lt;small&gt;(I haven't actually read &lt;em&gt;Getting Things Done&lt;/em&gt;, but I have friends who swear by it, some of whom talk to me about it, to which I tend to wind up responding with “oh, that's just locality of reference” or similar.)&lt;/small&gt;&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-8528407927770655656?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/8528407927770655656/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=8528407927770655656' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8528407927770655656'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8528407927770655656'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2008/01/wheels-within-wheels.html' title='Wheels Within Wheels'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-8961031703091973642</id><published>2007-12-31T03:18:00.000-05:00</published><updated>2007-12-31T03:27:02.876-05:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='netbsd'/><title type='text'>Burning Questions Answered</title><content type='html'>1. &lt;a href="http://netbsd.gw.com/cgi-bin/man-cgi?kvm_dump_wrtheader+3"&gt;The &lt;tt&gt;kcore_hdr_t&lt;/tt&gt; is written by &lt;tt&gt;savecore&lt;/tt&gt; using &lt;tt&gt;libkvm&lt;/tt&gt;&lt;/a&gt;.&lt;br /&gt;&lt;br /&gt;2. &lt;a href="http://www.google.com/search?q=%22the+german+owns+the+zebra%22"&gt;The German owns the zebra&lt;/a&gt;.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-8961031703091973642?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/8961031703091973642/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=8961031703091973642' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8961031703091973642'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8961031703091973642'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/12/burning-questions-answered.html' title='Burning Questions Answered'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-985582073327808535</id><published>2007-12-30T23:59:00.000-05:00</published><updated>2007-12-31T00:12:53.256-05:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='naming'/><category scheme='http://www.blogger.com/atom/ns#' term='get off my lawn'/><title type='text'>On the importance of punctuation</title><content type='html'>Just now I was reading a slashdot article where a bunch of people where whining about some links or other being to some site called “myminicity”.  Several mentions of that name later, it finally dawned on me that it was not, in fact, a compound of the usual English state-of-being suffix &lt;i&gt;-ity&lt;/i&gt; and some hypothetical trendy nonsense word(s) I hadn't heard of yet (cf. “meme”); but, rather, was to be read as the words “my mini city”.&lt;br /&gt;&lt;br /&gt;(I still don't know what the thing actually is, because I don't care.)&lt;br /&gt;&lt;br /&gt;If only people had decided to use hyphens when gluing words together for domain names, then I wouldn't have to occasionally waste valuable seconds wondering WTF some string of half-pronounceable letters is supposed to be.  (They also wouldn't run the risk of an unfortunate &lt;a href="http://itre.cis.upenn.edu/~myl/languagelog/archives/003388.html"&gt;powergenitalia incident&lt;/a&gt;, but how often does that happen?)  Ah well.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-985582073327808535?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/985582073327808535/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=985582073327808535' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/985582073327808535'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/985582073327808535'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/12/on-importance-of-punctuation.html' title='On the importance of punctuation'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-7685824949480979677</id><published>2007-12-27T22:15:00.000-05:00</published><updated>2007-12-27T23:39:51.174-05:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='multimedia'/><category scheme='http://www.blogger.com/atom/ns#' term='ffmpeg'/><category scheme='http://www.blogger.com/atom/ns#' term='tips'/><title type='text'>The Sound of Silence</title><content type='html'>Let's say you have a video file of some sort with no audio stream, and a device that plays video files but can't handle ones with no audio.  And you want to use the command-line tool &lt;tt&gt;ffmpeg&lt;/tt&gt;, because you already have a script set up to use it to do whatever transcoding, but for the slight problem of sound.&lt;br /&gt;&lt;br /&gt;Maybe you don't, but I did.  Know that &lt;tt&gt;ffmpeg&lt;/tt&gt; can take multiple input and/or output files and shuffle them around, in addition to decoding/encoding them.  Know also that &lt;tt&gt;ffmpeg&lt;/tt&gt; is documented in a manner both voluminous and not terribly approachable.&lt;br /&gt;&lt;br /&gt;The &lt;b&gt;wrong&lt;/b&gt; thing to do is to try to figure out how to extract the length of the video track and generate that many audio samples of silence.  But, if one hasn't noticed the right part of the man page, this may be what one tries to do.  (I did.)&lt;br /&gt;&lt;br /&gt;The right thing to do is to use the &lt;tt&gt;-shortest&lt;/tt&gt; flag, which directs &lt;tt&gt;ffmpeg&lt;/tt&gt; to stop whenever &lt;em&gt;any&lt;/em&gt; input stream reaches its end, rather than when &lt;em&gt;all&lt;/em&gt; inputs are done.  Some of you may be (but probably none of you are) thinking of various versions of the Scheme procedure &lt;tt&gt;map&lt;/tt&gt; and their behavior on lists of unequal and/or infinite length, recently a point of contention in the discussion leading up to &lt;acronym title="the Revised^6 Report on [the Algorithmic Language] Scheme"&gt;R6RS&lt;/acronym&gt;.  And what is Unix if not a platform for stream processing?  (Don't answer that.)&lt;br /&gt;&lt;br /&gt;Thus: &lt;tt&gt;-f s8 -i /dev/zero -shortest&lt;/tt&gt;, placed either before or after the regular input file, depending on whether input that does have audio should be silenced or not, respectively.&lt;br /&gt;&lt;br /&gt;It's a not entirely inelegant solution to a mildly ridiculous problem.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-7685824949480979677?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/7685824949480979677/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=7685824949480979677' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/7685824949480979677'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/7685824949480979677'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/12/sound-of-silence.html' title='The Sound of Silence'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-5667368293984327671</id><published>2007-11-13T12:16:00.000-05:00</published><updated>2007-11-13T12:38:34.112-05:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='proof'/><category scheme='http://www.blogger.com/atom/ns#' term='coq'/><category scheme='http://www.blogger.com/atom/ns#' term='acl2'/><title type='text'>Quod Erat Covered-In-Bees</title><content type='html'>Trying to prove something in &lt;a href="http://coq.inria.fr/"&gt;Coq&lt;/a&gt; is like operating a large, fly-by-wire bulldozer.  On the one hand, you have to figure out what to shove where, or how to program the machine to do the shoving for you.  On the other hand, you can use your superior human pattern-recognition skills to avoid driving into obstacles, and if you do get stuck, you have at least some chance of figuring out how to extricate yourself.&lt;br /&gt;&lt;br /&gt;Trying to prove something in &lt;a href="http://www.cs.utexas.edu/users/moore/acl2/"&gt;ACL2&lt;/a&gt; is like imperiously proclaiming, “Robot servants, hear my command!” and then they run out into the junkyard picking up stuff and moving it around.  And if you're lucky, and the task you've given them simple enough, they get the job done for you while you sit back on a lounge chair sipping a strawberry daiquiri.  But if that's not the case, they run around doing exactly the wrong thing, until either they explode messily of their own accord or you call in an airstrike.  And then you get to examine the flaming wreckage to figure out what went wrong, and what helpful hints you might be able to offer the robots next time.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-5667368293984327671?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/5667368293984327671/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=5667368293984327671' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/5667368293984327671'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/5667368293984327671'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/11/quod-erat-covered-in-bees.html' title='Quod Erat Covered-In-Bees'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-2209438055942140318</id><published>2007-11-09T11:13:00.000-05:00</published><updated>2007-11-09T11:30:04.901-05:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='algol'/><category scheme='http://www.blogger.com/atom/ns#' term='compiler'/><category scheme='http://www.blogger.com/atom/ns#' term='stack'/><title type='text'>This Morning's Compiler Meditation:</title><content type='html'>translating &lt;a href="http://en.wikipedia.org/wiki/Man_or_boy_test"&gt;Knuth's “man or boy” test&lt;/a&gt; from ALGOL 60 into C, by reifying the activations as &lt;tt&gt;struct&lt;/tt&gt;s and closure-converting the call-by-name thunks.  &lt;a href="http://www.xlerb.net/misc/mob.c"&gt;Like this&lt;/a&gt;.&lt;br /&gt;&lt;br /&gt;I considered trying to run it by hand instead, but that would certainly take a lot of paper, and also as Knuth himself apparently failed in that task, I thought perhaps not.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-2209438055942140318?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/2209438055942140318/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=2209438055942140318' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/2209438055942140318'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/2209438055942140318'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/11/this-mornings-compiler-meditation.html' title='This Morning&apos;s Compiler Meditation:'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-4903274466345327039</id><published>2007-10-29T19:48:00.000-04:00</published><updated>2007-10-29T20:24:16.258-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='performance'/><category scheme='http://www.blogger.com/atom/ns#' term='realworld'/><category scheme='http://www.blogger.com/atom/ns#' term='disk'/><category scheme='http://www.blogger.com/atom/ns#' term='sun'/><category scheme='http://www.blogger.com/atom/ns#' term='zfs'/><category scheme='http://www.blogger.com/atom/ns#' term='fs'/><title type='text'>My Parity Iz Pastede On Yay</title><content type='html'>Sun's ZFS, to hear some people tell it, is the last filesystem anyone will ever need.  It slices, it dices, and so on.  Why, its magical powers are so great, &lt;a href="http://blogs.sun.com/bonwick/entry/raid_z"&gt;it can give you all the advantages RAID-5 (or -6) without any of the historical drawbacks!&lt;/a&gt;&lt;br /&gt;&lt;br /&gt;&lt;a href="http://blogs.sun.com/roch/entry/when_to_and_not_to"&gt;Except that it doesn't.&lt;/a&gt;  Give you all of the benefits of RAID-[56], that is.  In order for RAID-Z to do its thing, each filesystem block has to be divided into stripes independently.  Which is great if you're dealing with a large file divided into 128kB blocks.  And not so great if you're dealing with a single 5kB file that's been scattered across 10 data disks, one sector to each.  Now you have to do I/O operations on all 10 disks to read the file back (and 12 to write it in the first place, assuming the use of double-parity &lt;tt&gt;raidz2&lt;/tt&gt;), whereas with a conventional RAID with a more reasonable stripe size, it would take only one.&lt;br /&gt;&lt;br /&gt;And that's the tradeoff.  It might not sound like much, but it's a really big deal if you're trying to store mail in the Maildir format (one file per message!), or any other workload with a lot of small files and random access.  System administrators dealing with such things may take to talking about “spindles” as an attribute of a disk array, as metonymy for the rate at which it can handle random I/Os.  As in, the mail fileserver has been slow lately; looks like it needs more spindles.  So you add disks to it, even though you have plenty of space free.  Because it's all about how fast you can move the physical heads around.&lt;br /&gt;&lt;br /&gt;In this light, what RAID-Z does is takes all of your disks and turns them into one spindle.  Burning half the blocks to do mirroring instead doesn't sound so bad now, does it?&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-4903274466345327039?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/4903274466345327039/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=4903274466345327039' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/4903274466345327039'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/4903274466345327039'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/my-parity-iz-pastede-on-yay.html' title='My Parity Iz Pastede On Yay'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-5341907314951079348</id><published>2007-10-28T13:13:00.000-04:00</published><updated>2007-10-28T13:34:48.155-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='linux'/><category scheme='http://www.blogger.com/atom/ns#' term='fs'/><title type='text'>Thank you, SGI.</title><content type='html'>Not only can &lt;a href="http://oss.sgi.com/projects/xfs/"&gt;XFS&lt;/a&gt; be resized &lt;abbr title="i.e., while the filesystem is mounted"&gt;online&lt;/abbr&gt;, but that works just as well on the root filesystem.&lt;br /&gt;&lt;br /&gt;Well, after I symlinked &lt;tt&gt;/dev/root&lt;/tt&gt; to the correct device, because Linux still uses the ridiculous archaic SunOS-ism of having &lt;tt&gt;mount&lt;/tt&gt; and &lt;tt&gt;unmount&lt;/tt&gt; and &lt;tt&gt;df&lt;/tt&gt; update and consult the regular file &lt;tt&gt;/etc/mtab&lt;/tt&gt; instead of just asking the kernel, like any sane system would do.&lt;br /&gt;&lt;br /&gt;And thus the kernel's filesystem table (readable at &lt;tt&gt;/proc/mounts&lt;/tt&gt;, in the same format as &lt;tt&gt;mtab&lt;/tt&gt;, even) winds up with a bunch of useless junk in it, which probably wouldn't be put up with if people actually had to look at it all the time.&lt;br /&gt;&lt;br /&gt;Anyway.  Being able to &lt;tt&gt;xfs_growfs&lt;/tt&gt; the root filesystem and have it (mostly) just work is a refreshing change from certain other filesystem features; e.g., on Solaris 9, UFS snapshots' being forbidden for the filesystems holding &lt;tt&gt;/&lt;/tt&gt; and &lt;tt&gt;/var&lt;/tt&gt;, because it's necessary to briefly disable writing, and I guess that might deadlock or something.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-5341907314951079348?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/5341907314951079348/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=5341907314951079348' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/5341907314951079348'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/5341907314951079348'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/thank-you-sgi.html' title='Thank you, SGI.'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-827905547020733993</id><published>2007-10-12T16:15:00.000-04:00</published><updated>2007-10-12T16:48:35.549-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='ocaml'/><title type='text'>Fun with Polymorphic Variants</title><content type='html'>ML variants.  Wonderful stuff:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# type color = Red | Yellow | Green | Cyan | Blue | Magenta | Other of int * int * int;;&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;OCaml has &lt;a href="http://caml.inria.fr/pub/docs/manual-ocaml/manual006.html#htoc41"&gt;polymorphic variants&lt;/a&gt;, where you don't need to bother with declaring types like that:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# `Foobar;;&lt;br /&gt;- : [&amp;gt; `Foobar ] = `Foobar&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;It's almost like it's dynamically typed, except it can't go wrong.  Of course, when you do go to define types, you have to deal with the type variables hidden in abbreviations like the above, but that's not the point.  Nor is this unfortunate limitation of the type sytem:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# function `Foo i -&amp;gt; `Foo (string_of_int i) | x -&amp;gt; &lt;u&gt;x&lt;/u&gt;;;&lt;br /&gt;This expression has type [&amp;gt; `Foo of int ] but is here used with type&lt;br /&gt;&amp;nbsp;&amp;nbsp;[&amp;gt; `Foo of string ]&lt;br /&gt;Types for tag `Foo are incompatible&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;No, this post is actually about representations.  Since OCaml is statically typed to the point of having no runtime type information, it can represent a variant case with no data using the same bits it would use for an &lt;code&gt;int&lt;/code&gt;.  And it does this thing &amp;mdash; meaning that &lt;code&gt;0&lt;/code&gt;, &lt;code&gt;false&lt;/code&gt;, the empty list and so on are all equal; but, unlike in Lisp, there's no way to know that without breaking the type system, as the comparison operators work only on two things of like type.&lt;br /&gt;&lt;br /&gt;So, break the type system; you could use &lt;code&gt;Obj.repr&lt;/code&gt; and &lt;code&gt;Obj.is_int&lt;/code&gt; to verify what I just said, or:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# external unsafe_to_int : 'a -&amp;gt; int = "%identity";;&lt;br /&gt;external unsafe_to_int : 'a -&amp;gt; int = "%identity"&lt;br /&gt;# List.map unsafe_to_int [Red;Yellow;Green;Cyan;Blue;Magenta];;&lt;br /&gt;- : int list = [0; 1; 2; 3; 4; 5]&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;Well, what about polymorphic variants?  You can use different, non-disjoint sets of tags in different places, and it somehow has to work.  This is somehow:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# unsafe_to_int `Foobar;;&lt;br /&gt;- : int = 807339693&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;Gee.  I wonder how it does that...&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# unsafe_to_int `A;;&lt;br /&gt;- : int = 65&lt;br /&gt;# unsafe_to_int `B;;&lt;br /&gt;- : int = 66&lt;br /&gt;# unsafe_to_int `AA;;&lt;br /&gt;- : int = 14560&lt;br /&gt;# unsafe_to_int `AB;;&lt;br /&gt;- : int = 14561&lt;br /&gt;# unsafe_to_int `BA;;&lt;br /&gt;- : int = 14783&lt;/code&gt;&lt;br /&gt;&lt;br /&gt;Oh look.  It's a simple polynomial hash function.  At this point, your first thought should be approximately this:&lt;br /&gt;&lt;br /&gt;&lt;code&gt;# `Uctakw == `Uctakw;;&lt;br /&gt;- : bool = true&lt;br /&gt;# `Uctakw == `Foobar;;&lt;br /&gt;- : bool = false&lt;br /&gt;# `Uctakw == &lt;u&gt;`Saazaa&lt;/u&gt;;;&lt;br /&gt;Variant tags `Uctakw and `Saazaa have same hash value. Change one of them.&lt;/code&gt;&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-827905547020733993?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/827905547020733993/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=827905547020733993' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/827905547020733993'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/827905547020733993'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/fun-with-polymorphic-variants.html' title='Fun with Polymorphic Variants'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-8821977481530711295</id><published>2007-10-09T14:44:00.000-04:00</published><updated>2007-10-10T14:34:48.574-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='icfp2007'/><category scheme='http://www.blogger.com/atom/ns#' term='icfp'/><title type='text'>How did this happen?</title><content type='html'>&lt;img src="http://www.celestial-dire-badger.com/icfp/2007/sun.png" align="right" alt="[*]"&gt;Concerning &lt;a href="http://rlwinm.blogspot.com/2007/10/proximate-cause.html"&gt;this matter&lt;/a&gt;, the organizers definitely intended that people have to reverse-engineer the alien genome and solve their little puzzles; earlier I'd wondered if they'd deliberately designed the problem to make the image-processing approach feasible, but this appears not to have been the case.&lt;br /&gt;&lt;br /&gt;Now, that kind of strategy had certainly occurred to them, and indeed they deliberately did not outright forbid it, but they did seek to make it highly challenging at best.  And they tested all this on two separate batches of undergrad guinea pigs.&lt;br /&gt;&lt;br /&gt;Clearly, then, my relative success is a sign that something went horribly wrong.&lt;br /&gt;&lt;br /&gt;My theory: the organizers were thinking of the DNA as just a platform on which to build some kind of sequential random-access machine, on which conventional algorithms could then be run; and the RNA as a mostly opaque means to an end.  (In fact, now that &lt;a href="http://www.cs.uu.nl/research/techreps/UU-CS-2007-029.html"&gt;the official report has been released&lt;/a&gt;, evidence of this worldview can be seen.)&lt;br /&gt;&lt;br /&gt;&lt;br /&gt;But in fact the RNA is all but opaque: where the DNA can use all manner of obfuscation and even outright encryption to hide its secrets, the RNA has no control flow, and is limited in what it can do with the graphics context.&lt;br /&gt;&lt;br /&gt;Then, the genome's output RNA almost &lt;i&gt;invites&lt;/i&gt; editing &amp;mdash; pretty much everything in the image, including the &amp;ldquo;anticompressant&amp;rdquo; moir&amp;eacute; pattern applied at the very end, is drawn in its own canvas and composed down, recursively where appropriate.  Deleting or extracting items is thus relatively easy; and there's no need to guess at what each piece does, because it's immediately visible.  (Okay, maybe not the anticompressant so much, but once you know it's there....)&lt;br /&gt;&lt;br /&gt;&lt;br /&gt;As for the DNA, certainly it would be difficult indeed to outdo the organizers at creating an operating system and libraries for such a strange substrate in the time provided, let alone port a useful image decompressor to it, and then you're still stuck with an image that's 240kB in PNG.  So went the organizers' reasoning, anyway.  Thus, surely teams would abandon such foolish ideas for the simpler alternative of dealing with the existing genome, puzzles and encryption and damaged bits and all.  Right?&lt;br /&gt;&lt;br /&gt;But what if I don't want general computation?  Let's say I want a very specific computation: Given a dictionary (list of words) and a list of numeric indices into the dictionary, return the concatenation of the corresponding words.  The DNA machine can execute this operation directly: just put the dictionary words into the data section, capture them with sub-patterned skips, and encode the list of indices as a template.  Or, in other words: copy and paste.&lt;br /&gt;&lt;br /&gt;And that is data compression.  Mostly because it can be iterated; I've &lt;a href="http://www.celestial-dire-badger.com/icfp/2007/760.dna"&gt;prepared a DNA sequence that may be instructive&lt;/a&gt;.  Obviously not every piece of DNA will be &lt;i&gt;quite&lt;/i&gt; that repetitive, but it can get pretty good results, especially for something so simplistic &amp;mdash; 90:1 for my winning prefix &amp;mdash; and I didn't have to do anything remotely like building an entire computational world to get there.&lt;br /&gt;&lt;br /&gt;Once practical inexpensive compression becomes available, the picture changes a bit (so to speak).  No longer does it matter that the RNA commands are so long &amp;mdash; a deliberate countermeasure to image reconstruction &amp;mdash; nor that lengthy runs of &lt;tt&gt;IIIPIIIIIP&lt;/tt&gt; are needed to move the point around, and similarly for color.  Nor even is subtlety in the use of flood-fill and such to keep the RNA size down necessarily still a win; it may even be a net loss compared to, say, just drawing lots of identical 3x3 boxes.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-8821977481530711295?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/8821977481530711295/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=8821977481530711295' title='1 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8821977481530711295'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/8821977481530711295'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/how-did-this-happen.html' title='How did this happen?'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-162218276516744672</id><published>2007-10-08T12:22:00.000-04:00</published><updated>2007-10-09T17:26:45.304-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='icfp2007'/><category scheme='http://www.blogger.com/atom/ns#' term='icfp'/><title type='text'>The Proximate Cause</title><content type='html'>&lt;img align="right" src="http://www.celestial-dire-badger.com/icfp/2007/mu.png" alt="(mu)"&gt;There is, of course, a specific event that got me to actually create this thing.  That would be ICFP'07, or rather the 2007 &lt;acronym title="Association for Computing Machinery"&gt;ACM&lt;/acronym&gt; &lt;acronym title="Special Interest Group on Programming LANguages"&gt;SIGPLAN&lt;/acronym&gt; &lt;a href="http://www.icfpconference.org/"&gt;International Conference on Functional Programming&lt;/a&gt;.  It was last week.  And, every year since 1998, there's been a &lt;a href="http://www.icfpcontest.org/"&gt;programming competition associate with it&lt;/a&gt; held back in July or so, with winners announced (and the contest organizers' experience reported on) at the conference.&lt;br /&gt;&lt;br /&gt;I attended the conference, as I (as team Celestial Dire Badger) had won the Judges' Prize (for an uncommonly “creative” solution) in the contest, and — as even I didn't discover until last Tuesday when the announcements were made — also placed third out of, oh, 357 teams.  As a team of one person, while for example the #1 team had four and the #2 twelve.&lt;br /&gt;&lt;br /&gt;So, I don't know, maybe I'm famous now or something?  I mean, I was declared to be an “extremely cool hacker” to the applause of a few hundred members of the functional programming community, which I guess isn't quite the same as being entirely unknown.  Or at least someone might be wanting to read what I have to say about that thing.  And besides, &lt;a href="http://marco-za.blogspot.com/search/label/icfp"&gt;everyone else is doing it&lt;/a&gt;.&lt;br /&gt;&lt;br /&gt;In that case: I already have &lt;a href="http://www.celestial-dire-badger.com/icfp/2007/report.html"&gt;a chronological writeup of the contest weekend itself&lt;/a&gt;, but I have a bit more perspective now that I know more about the making of the contest... but more on that later.&lt;br /&gt;&lt;br /&gt;&lt;br /&gt;Useful background for random people wandering in: if &lt;a href="http://www.icfpcontest.org"&gt;the contest website&lt;/a&gt; &lt;!--FIXME: that link will go to the wrong place next year--&gt; doesn't have enough info lying around, then the beginning of &lt;a href="http://www.icfpcontest.org/Endo.pdf"&gt;the problem statement&lt;/a&gt; (PDF) should be helpful in determining what on earth I'm talking about.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-162218276516744672?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/162218276516744672/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=162218276516744672' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/162218276516744672'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/162218276516744672'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/proximate-cause.html' title='The Proximate Cause'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-6715403038409614304</id><published>2007-10-07T00:15:00.001-04:00</published><updated>2007-10-07T00:48:19.634-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='ppc'/><category scheme='http://www.blogger.com/atom/ns#' term='insn'/><category scheme='http://www.blogger.com/atom/ns#' term='meta'/><title type='text'>What's in a name?</title><content type='html'>Because somebody's going to wonder: &lt;tt&gt;rlwinm&lt;/tt&gt; is a &lt;a href="http://en.wikipedia.org/wiki/PowerPC"&gt;PowerPC&lt;/a&gt; machine instruction, the mnemonic standing for “Rotate Left Word Immediate then aNd with Mask”.&lt;br /&gt;&lt;br /&gt;The mask in question isn't fully general, of course — this is RISC, so it wouldn't fit — but it can be any contiguous non-empty range of 1 bits, which can wrap around the beginning/end of the word, or not.  Thus, things like left and right (logical) shifts, clearing the low or high N bits, and extracting a bitfield from a word are all just special cases of &lt;tt&gt;rlwinm&lt;/tt&gt;.&lt;br /&gt;&lt;br /&gt;In other words, it's a fairly elegant generalization of a bunch of related operations which are often considered as separate, and some of which usually require multiple instructions.&lt;br /&gt;&lt;br /&gt;(It's also not a terribly common username, and perhaps more importantly it's six characters long.)&lt;br /&gt;&lt;br /&gt;Ironically, I haven't really done any assembly or machine-language stuff on PowerPC, whereas I have on x86.&lt;br /&gt;&lt;br /&gt;I might eventually decide in something different for the Blog Title, but the domain name will definitely stay.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-6715403038409614304?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/6715403038409614304/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=6715403038409614304' title='1 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6715403038409614304'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/6715403038409614304'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/whats-in-name.html' title='What&apos;s in a name?'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8573067371275934806.post-4875077610977305531</id><published>2007-10-06T23:40:00.000-04:00</published><updated>2007-10-06T23:58:31.238-04:00</updated><category scheme='http://www.blogger.com/atom/ns#' term='meta'/><title type='text'>Hello, World!</title><content type='html'>So I've finally gotten around to setting up a Serious Technical Blog, like I've been meaning to do for a while now.&lt;br /&gt;&lt;br /&gt;(I do have another weblog-like object, but that's more of a personal thing, for people I know to keep track of my life and so on, and other arbitrary acts of self-indulgence, and much of it would probably bore other people at best.  Notice how I'm not linking to it here.)&lt;br /&gt;&lt;br /&gt;Basically, I felt like a place for just the computery stuff, formatted for more public consumption, might be a good thing to have.  This, hopefully, will be that.&lt;div class="blogger-post-footer"&gt;&lt;img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/8573067371275934806-4875077610977305531?l=rlwinm.blogspot.com' alt='' /&gt;&lt;/div&gt;</content><link rel='replies' type='application/atom+xml' href='http://rlwinm.blogspot.com/feeds/4875077610977305531/comments/default' title='Post Comments'/><link rel='replies' type='text/html' href='http://www.blogger.com/comment.g?blogID=8573067371275934806&amp;postID=4875077610977305531' title='0 Comments'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/4875077610977305531'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8573067371275934806/posts/default/4875077610977305531'/><link rel='alternate' type='text/html' href='http://rlwinm.blogspot.com/2007/10/hello-world.html' title='Hello, World!'/><author><name>Jed Davis</name><uri>http://www.blogger.com/profile/11228234046083389226</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='24' height='32' src='http://3.bp.blogspot.com/_ezER6xcSGk8/ShYFZ8Ub3mI/AAAAAAAAAAM/7Lpww4EGE9Q/S220/fm216.jpeg'/></author><thr:total>0</thr:total></entry></feed>
