Languages and concurrent programs

Zac Kinkaid -- U. Toronto

---

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 = 1
while(y != 0):
    y = randInt() mod x
    x = y + 2

Consider let the set of reachable states be points on the integral lattice; while we can't compute anything meaningful on all of them, we can reason about geometric supersets of them (here, the set \(y-x\leq1\))

Invariants from Constraints

Write a constraint system defined by program structure; prove by induction that the invariants continue to hold

Again, this extends badly

---

Data-flow graphs

Draw some sequential graphs side-by-side; add additional cross-thread dataflow links (aware of active synchronization). Think: When you're imposing synchronization on your programs, you're really pruning unwanted dataflow.

Multiple-threading: Need to add data-flow links within threads

---

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: rendering, javascript, parser

---

Atlantis

Taglines: security, performance, robustness

But first, some depressing things...

Browsers offer many opportunities for parallelism! ex: HTML parsing, rendering, network and disk IO. But current architectures limit concurrency, suffer from races.

But the DOM model says: JS is single-threaded, and cannot see browser locks. So: JS execution should biglock the DOM. What does happen: NOT THAT.

But in reality, there's just no concurrency re: the DOM. None. more at: Race Detection for Web Applications -- Petrov et al., PLDI '12

idiosyncratic abstraction (n.) an abstraction that is inconsistently applied throughout an application.

HTML5 screen-sharing attacks: SOP should prevent attacker.com from opening and screen-scraping bank.

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. the following case:

int before_and_after (int *the_thing, struct cv *thing_changed_cv, struct lock *thing_changed_lock) {
    lk_acquire(thing_changed_lock);
    
    int before = *the_thing;
    cv_wait(thing_changed_cv, thing_changed_lock);
    int after = *the_thing;
    
    KASSERT(before != after);
    
    lk_release(thing_changed_lock);
    return compare_things(before,after);
}

void mess_around (int *the_thing, struct cv *thing_changed_cv, struct lock *thing_changed_lock) {
    lk_acquire(thing_changed_lock);
    mutate(the_thing);
    
    cv_broadcast(thing_changed_cv, thing_changed_lock);
    
    lk_release(thing_changed_lock);
}

This code is properly synchronized (and in particular, protects the KASSERT(before != after)), assuming that your locks and CVs

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 average time)
• ...but in any case, do not starve even the long-running processes too much (exponentially is a good benchmark -- since that, analytically, places a finite cap on the total runlength of a process).

Many of the designs I've seen from the class in A2 design documents fail in at least one of these respects, so I think it may be useful to go over common design failures and good designs.

indicates a potential issue of which you should be cautious. Check that your system doesn't have this as an issue!

---

Timeslicing and Timedicing

Not every thread blocks voluntarily; after running a thread for a certain

0

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:

• Unequally Yoked | 7 Quick Takes: Costuming, Conspiracy, and Counterfeiting (Leah Libresco is a one-time atheist blogger, now a Catholic blogger, and remains a devout rationalist. Unequally Yoked's 7QT's get the credit for convincing me to to BoL's.)
• My Biased Coin | Weekend Links (November 1 Edition) (Michael Mitzenmacher is currently my professor for Complexity and Algorithms, and often has insightful things to say on the inner workings of the ivory tower, being a research professor of theoretical computer science.)
• Slate Star Codex | Links for November 2014 (Scott S. Alexander, who also writes as Yvain, writes on his own blog and on LessWrong about...well...lots of things. But I appreciate his thoughts.)

1

Vigrin Galactic's SpaceShipTwo [exploded in midair on Friday](http://www.bbc.com/news/world-us-canada-29861259), killing one of two test pilots. In [a press statement](http://www.virgingalactic.com/news/item/statement-from-virgin-galactic/), CEO George Whitesides says:

"Space is hard and today was a tough day. We are going to be supporting the investigation as we figure out what