My Faults My Own

…willing to sacrifice something we don't have

for something we won't have, so somebody will someday.

IN WHICH Ross Rheingans-Yoo, a sometimes-poet and erstwhile student of Computer Science and Math, oc­cas­ion­al­ly writes on things of int­erest.

Reading Feed (last update: July 28)

A collection of things that I was happy I read. Views expressed by linked authors are chosen because I think they're interesting, not because I think they're correct, unless indicated otherwise.


(5)

Blog: Marginal Revolution | How well is Germany dealing with the migration crisis? — "Whatever respite Germany may have gained this week is offset, and then some, by the arrival of a new and frightening political dynamic. Mr. Seehofer succeeded by going nuclear; chances are, he won’t be the last. The politics of fear and menace may be here to stay, undermining the foundations of democracy. In sound democracies, policies are the results of compromise between parties representing a majority of the voters. Through the politics of artificial crisis, minorities take the system hostage. They create policies redeeming fictional problems for fictional

READ MORE

Notes: Parallel Proofs for Parallel Programs

Languages and concurrent programs

Zac Kinkaid -- U. Toronto

Notes legibility estimate: LOW


Automatic analysis of algorithms

We'd like to know things like "What numeric types are used here? Are these array accesses in-bounds?"

Today: Proving the absence of faults in multi-threaded programs.
Multi-threaded programs are a great target for automated analysis, since they're so notoriously difficult for humans to reason about.

History:

  • Floyd -- program invariants
  • Ashcroft, Manna -- extended Floyd to multithreaded programs by treating a multiprogram as a nondeterministic single-threaded program -- difficulty: doesn't scale in #threads
  • ??, Reese -- (for data-independent threads) Prove each thread correct individually; then check that the reasoning doesn't interfere across threads -- difficulty extending to data-dependent threads, which requires some cleverness, which is difficult to automate

in common: attempts to reason about multi-threaded code using (extensions of) sequential reasoning


The big problem

Given (program, property), does property(program) hold?

Problem!

Turing: Halting indeterminacy
Rice's Theorem: Every nontrivial property is undecideable

Solution

Allow either one-sided error or indeterminacy/divergence


Example

x = 2; y
READ MORE

Notes: Building a Better Web Browser

These are my cursory notes from a talk given by James Mickens of Microsoft Research, in March 2015, titled "Building a Better Web Browser".

Notes legibility estimate: MEDIUM


The State of Progress

Chrome, Opera isolate the renderer in separate processes -- this allows tabs to crash on their own. ...but the issue is that the browswer is still a monolithic kernel.

Servo -- extra threading! ...but still monolithic.

The problem: Browser developers take the monolithic design as a given, and tinker around the edges.

The Problem

What is a browser trying to do? Provide services for origins -- render, computation, i/o + messaging

  • It provides origin = <protocol, host, port>

Render: HTML CSS MathML Aria WebGL video canvas images

IO: XHR DOM IndexedDB Cookies FileReader BrowserCache AppCache

Currently: providing services for origins, but they're high-level and complex. You wouldn't ask your operating system to implement Emacs in the kernel. ...well, you might. That was a test; I've already called the police on you.

Kernel: network, UI, storage (concurrency)

Usercode:

READ MORE

[CS161] The Classic CV Error

This is a very technical post, largely for the benefit of the students of CS161: Operating Systems, for which I am a Teaching Fellow this semester. It may be useful to you if you're interested in operating systems for some reason, but if you're not in a CS mood today, maybe just move along.

From what I've seen as a TF for this course, it is very, very normal to write condition-variables code that looks like this:
struct cv {  
    struct semaphore *sem;
    volatile int waiters;
}

void cv_wait(struct cv *cv, struct lock *lock) {  
    KASSERT(lk_do_i_hold(lock));

    cv->waiters++;
    lk_release(lock);
    P(cv->sem);
    lk_acquire(lock);
}

void cv_broadcast(struct cv *cy struct lock *lock) {  
    KASSERT(lk_do_i_hold(lock));

    for (; cv->waiters > 0; cv->waiters--)
        V(cv->sem);
}
This code is wrong (or, more specifically, badly synchronized). And it is such a common error that I'm choosing to dub it The Classic CV Error. It's subject to a race condition in e.g.
READ MORE

[CS161] On Scheduling

This is a very technical post, largely for the benefit of the students of CS161: Operating Systems, for which I am a Teaching Fellow this semester. It may be useful to you if you're interested in operating systems for some reason, but if you're not in a CS mood today, maybe just move along.

Why Do We Schedule, Master Bruce?

A scheduler, as you know, is responsible for determining which threads run, for how long, and in what order. As much as possible, it should give the shared illusion that each process is running constantly to completion, using the entire processor. To this end, there are three major desiderata:

  • That interactive threads (in particular, user-interactive threads) are responsive.
  • That no process starves.
  • That the system, on average, runs quickly.

These high-level desiderata factor into the low-level conditions that:

  • Threads which block expecting a response are rescheduled promptly after waking.
  • Time is allocated more-or-less fairly, subject to:
  • Processes closer to completion are prioritized (recall that shortest-time-to-completion-first is provably optimal in total
READ MORE

October 31 Bucket o' Links: "Links, Explosions, and People Talking" Edition

Welp, Friday post goes out on Sunday NO shut up it's still saturday is that how this daylight savings thing works HRMPH. (It's not.)

Anyway, I'm in the middle of writing some stuff about a topic that's almost certainly going to end up being controversial, and I've decided to publish some of it, and I'll get around to doing the part where I actually say things later. Anyway, that's a work in progress; here's a finished linkwrap!

First, meta of metas, if you like my takes on (some subset of) the week, maybe also check out other people's linkwraps that have come out in the last day or so:

READ MORE
1 / 1