Author: yodaiken

  • what do we got to verify in an os?

    From comments below. Just one more comment: I think we should make a distinction between a tool that can verify threaded code and a tool that can verify the code that implements threading. The latter is what you are looking for here and it is much more difficult. Furthermore it is arguably unnecessary — a…

  • blog administration

    Nonessential update: if you are getting a feed, you can update the path /w/feed/ or /w/rss can have the “w/” drop since this is now the main page.

  • Update to blog

    We start the new year with a brand new design and link structure. If you have any trouble with access to pages or with RSS feeds, please drop me a line or leave a comment. thanks The Mngmt.

  • Happy new year and validation

    Updated below! Years ago I proposed the following code snippet as a minimal standard for a useful verification method. Still not quite there. /* you are not expected to understand this */ if(save()){ load_memory_management(); /* map in new current */ return; }else { current = new; resume(); panic(“RESUME RETURNED! KERNEL BROKENn”); } Not so complicated,…

  • imitation hemingway winner repost

    I found this on Larry McVoy’s site, and repost it every now and then because it is so good. But I’d like to read a Cormac McCarthy version too.

  • Cell phone handsets and linux and software value

    Update at the end. Two FSMLabs alumni are leading the charge for Linux handsets in two different companies. Jason Whitmire is now GM of cell phones for Wind River. Jason’s blog is here and a Linuxdevices article discusses his first post which concerns the, well, machinations of Google and the two big cell-phone consortia Limo…

  • formal methods considered harmful and more on soft real-time

    [fixed a couple of typos, Dec. 20 2007] John Regehr writes: On the other hand, there is plenty of useful work to be done on supporting time sensitive applications (I’ll just avoid saying “soft real-time”) even when no guarantees are made. Let’s take the example of an OS that disables interrupts when any process is…

  • Are programmers smarter than Hollywood writers after all?

    Don Marti in comments below notes Reruns of “I Love Lucy”  and “Knight Rider” don’t stop working when the studio fails to bring in writers to maintain them. Maybe the programmers are smarter after all.  

  • Soft real-time and QOS (revised)

    [ revised version of an older post] “Soft real-time” is a perfect example of the “soft design” noted in an earlier post. There are perfectly good ways of characterizing quality of service (QOS) assurances precisely. Doug Jenson proposes one possible definition: The general case of a deadline (which is a soft deadline) has utility measured…

  • Free digital content and the daily show

    Video about “free digital content”. [youtube http://www.youtube.com/watch?v=PzRHlpEmr0w&rel=0&color1=0xd6d6d6&color2=0xf0f0f0&border=1]