
ALT A comic riffing on the one by @jrecursive at http://howfuckedismydatabase.com/nosql/fault-tolerance.png. Title: "Dataflow processing" Panel 1: "So, how do I read the memory?" "It's not memory, it's an independent component that will eventually return with the associated cache line!" Panel 2: "Ok, it's not memory. How do I read it?" "You introduce a read request into the memory controller!" Panel 3: "Did you just tell me to go fuck myself?" "I believe I did, Bob."

ALT Under the covers, your computer (the one on which you are reading this text) is a dataflow processor. When your computer reads memory it doesn't actually wander off to find the memory, it introduces a read request into your memory controller, an independent component that will eventually return with the associated cache line. Your computer then gets back to work on whatever it was doing, hoping the responses from the controller return in a timely fashion. Academically, I treat "my computer can do this, but timely dataflow cannot" as a bug. There are degrees, of course, and timely dataflow isn't on par with the processor's custom hardware designed to handle low level requests efficiently, but algorithmically, the goal is that anything you can do efficiently with a computer you should be able to express in timely dataflow.

ALT Photo of radio/player console. It’s a beautiful piece of polished hardwood furniture the size of a dresser, suitable for a living room or dining room. The two doors in the top half are for the radio (left) and record player (right). The bottom half has a fabric-covered screen where the speakers are.

ALT Zulip poll: "What do you want to focus on in our winter 290 course?" with six choices: - Concurrent and distributed program logics (separation logic, Views, Iris, etc.) - Distributed systems verification (IronFleet, Verdi, Aneris, etc.) - "Actually deployable verified software" (seL4, CompCert, VST, etc.) - Local-first software (CRDTs, DHTs, peer-to-peer systems, etc.) - Monotonic systems (CRDTs, LVars, Datalog, etc.) - Choreographic and multitier programming (Pirouette, Links, etc.)" The choices have 3, 1, 3, 3, 2, and 3 votes respectively.

ALT A diagram of the key pieces of a proof that executions of a causal broadcast protocol ensure causal message delivery. The key idea is that, to get from reasoning about individual processes to reasoning about entire executions, we leverage the correspondence between vector clocks and happens-before: we move from global to local, take a local step, then move back from local to global. At the bottom is a specification of an execution that observes causal delivery, expressed as a refinement type in Liquid Haskell.



















