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

On the advice of Bill Gates (GatesNotes | 6 Books I Recommended for TED 2015), I picked up this free-to-read chapter of John Brooks's Business Adventures, titled "Xerox Xerox Xerox Xerox".

What a fantastic read.

In a story reminiscent of the dot-com boom that would come forty years later, Brooks describes the meteoric and explosive rise of xerography in the American officeplace, and the group of inventors who re-mortgaged their houses and crowded into a workshop whose roof leaked tar on hot days to create the first office copier that could print on normal, untreated paper.

Two sections stood out as particularly spectacular, though the piece is fascinating throughout. (Note that Brooks is writing in the sixties about businesses that were operating in the sixties, and that his depictions of what would today be stunning sexism and racism were entirely the norm contemporarily.)

Apart from malfunctions, the machine requires a
good deal of regular attention from its operator, who is almost invariably a woman. (The girls who operated the earliest typewriters were themselves called "typewriters," but fortunately nobody calls Xerox operators "xeroxes.") Its supply of copying paper and black electrostatic powder, called "toner," must be replenished regularly, while its most crucial part, the selenium drum, must be cleaned regularly with a special non-scratchy cotton, and waxed every so often.

I spent a couple of afternoons with one 914 [Xerox copier] and its operator, and observed what seemed to be the closest relationship between a woman and a piece of office equipment that I had ever seen. A girl who uses a typewriter or switchboard has no interest in the equipment, because it holds

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.

Peter Flom is a prolific writer on Quora, and has recently started a blog there, titled Random Thoughts. He recently made a post that I thought was great, but since I'm really not a fan of Quora as a blogging platform, I asked his permission to reprint it here for my readers.

Obviously, the beliefs expressed about what "the 25 best things ever said" consists of are Peter's, not mine, as are the messages conveyed thereby. Nevertheless, I like Peter; we seem to see eye-to-eye on a lot.

The 25 best things ever said

Not in any particular order, except the last one, which is my favorite.

25) If two men agree on everything, you may be sure that one of them is doing the thinking.
-- Lyndon Baines Johnson (1908-1973) -- I have seen this attributed to Truman, as well.

24) The legitimate powers of government extend only to such acts as are injurious to others. It does me no injury for my neighbor to say there are twenty gods or no God. It neither picks my pocket nor breaks my leg.
-- Thomas Jefferson (1743-1826) -- quoting or paraphrasing John Locke

23) I do not feel obliged to believe that the same God who has endowed us with sense, reason, and intellect has intended us to forgo their use.
-- Galileo Galilei (1564-1642)

22) To give pleasure to a single heart by a single act is better than a thousand heads bowing in prayer.
-- Mahatma Gandhi (1869-1948)

21) When I get a little money, I buy books; and if any is left, I buy food and clothes.
-- Desiderius Erasmus (1465-1536)

20) It is impossible

or, "Ted Cruz's Campaign Logo is an Upside-Down, Burning American Flag"

First, a short lesson about why you should buy www.yourname.com before announcing your presidential campaign:

The site is, apparently, registered to Ted Cruz.

Just a different Ted Cruz.

Meanwhile, on Twitter...

Ted Cruz's campaign logo looks so familiar. pic.twitter.com/XsWYau105R

— clydetheslyde (@clydetheslyde) March 23, 2015

and on Gawker...

...and the Washington Post, who "could go on all day".

I guess, if you're a serious person, you might appreciate the Christian Science Monitor's serious article asking "Isn't this a bit early to be announcing a candidacy?" -- with a resounding (and data-supported answer of "no") -- and "Hasn't there been a lot of campaign coverage already this cycle?" -- with a similarly-supported answer of "yes".

Here we go again.

Recently, Milo King, on Gains From Trade, asks: What is the economic impact of divestment? A few years ago, and seemingly unrelatedly, the HPR came to the same conclusion, namely:

Because the stock market is efficient, selling off stock for reasons unrelated to that company's profitability will cause more amoral investors to step in and kindly take your depressed-price shares, reaping the spread for themselves. No long-term depression of prices, no pain felt by Exxon et al., and now the shareholder voting those shares has worse morals than you did. Oops.

Consider, for example, the widely-acclaimed divestment from South Africa, in protest of apartheid...

Despite the prominence and publicity of the boycott and the multitude of divesting companies, the financial markets' valuations of targeted companies or even

I'm leaving on a cruise for spring break, and so will effectively be without Internet until Sunday, March 23. I don't plan to update Faults in that time, though I do hope to get some writing done and have some things to post when I get back. (This is a minor lie; I've got one more post to push out the door later today.)

But, the prospect of being a week without things to read being approximately as appealing as vacationing in the Third Circle of Hades, I'm bringing substantial reading material along. And, because I have a blog and an itch for publicy, here's my reading list (or at least, my carrying-along-like-a-comfort-blanket list):

Fiction

• A Wizard Alone, Diane Duane (Young Wizards: VI)
• A Wizard's Holiday, Diane Duane (Young Wizards: VII)
• Wizards at War, Diane Duane (Young Wizards: VIII)
• The Eternal Flame, Greg Egan (Orthoganal: II)
• The Little Prince, Antoine de Saint-Exupéry
• Snow Crash, Neil Stephenson

Poetry

• The Oldest Word for Dawn, Brad Leithauser
• destruction myth, Mathias Svalina
• Selected Poems, Dylan Thomas ed. Walford Davies

Nonfiction for Classes

• Probability and Computing, Michael Mitzenmacher and Eli Upfal
• Pattern Recognition and Machine Learning, Christopher M. Bishop

Nonfiction for Pleasure

• Six Not-So-Easy Pieces, Richard P. Feynman
• Thinking, Fast and Slow, Daniel Kahneman
• Rationality: From AI to Zombies, Eliezer Yudkowsky (pdf)

Online Material

(cached at various levels of recursion with ScrapBook for Firefox)

• Slate Star Codex (all pages and outlinks), Scott Alexander
• My Faults My Own (all pages and outlinks), Ross Rheingans-Yoo
• This also doubles as "most go-to things I'd want to read", since I've outlinked to many favorite elsewhereposts by now.
• My Faults My Own -- editor portal (all pages), Ross