[Script Info]
Title: 
[Events]
Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
Dialogue: 0,0:00:09.52,0:00:14.48,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:00:14.48,0:00:16.93,Default,,0000,0000,0000,,Peter Sewell: Thank you for that\Nintroduction and to the organisers for
Dialogue: 0,0:00:16.93,0:00:23.46,Default,,0000,0000,0000,,this opportunity to speak to you guys. So\Nmy name is Peter Sewell. I'm an academic
Dialogue: 0,0:00:23.46,0:00:30.61,Default,,0000,0000,0000,,computer scientist and as such, I bear a\Nheavy burden of guilt for what we have to
Dialogue: 0,0:00:30.61,0:00:38.04,Default,,0000,0000,0000,,work with. Shared guilt, to be fair, but\Nguilt all the same. In many, many years of
Dialogue: 0,0:00:38.04,0:00:44.67,Default,,0000,0000,0000,,higher education, I know two things about\Ncomputers. Maybe you've figured them out
Dialogue: 0,0:00:44.67,0:00:55.00,Default,,0000,0000,0000,,slightly faster. The first thing, there's\Nan awful lot of them about. Shocking. And
Dialogue: 0,0:00:55.00,0:01:03.30,Default,,0000,0000,0000,,the second is that they go wrong. They go\Nwrong a lot. Really a lot. A lot. A lot!
Dialogue: 0,0:01:03.30,0:01:09.01,Default,,0000,0000,0000,,And they go wrong in many interestingly\Ndifferent ways. So sometimes they go wrong
Dialogue: 0,0:01:09.01,0:01:17.85,Default,,0000,0000,0000,,in spectacular ways, right? With\Nfireworks. And here, we see...
Dialogue: 0,0:01:17.85,0:01:24.03,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:01:24.03,0:01:31.26,Default,,0000,0000,0000,,Here we see half a billion dollars worth\Nof sparkle. You don't get that every day.
Dialogue: 0,0:01:31.26,0:01:34.97,Default,,0000,0000,0000,,And so what was going on? So as I\Nunderstand it, what was going on was that
Dialogue: 0,0:01:34.97,0:01:40.60,Default,,0000,0000,0000,,the - this was the first flight of the\NAriane 5 launcher and it reused some of
Dialogue: 0,0:01:40.60,0:01:45.85,Default,,0000,0000,0000,,the guidance software from Ariane 4.\NThat's fine. Good, tested code. Should
Dialogue: 0,0:01:45.85,0:01:53.03,Default,,0000,0000,0000,,reuse it. But the launch profile for\NAriane 5 went sideways a bit more - on
Dialogue: 0,0:01:53.03,0:01:58.83,Default,,0000,0000,0000,,purpose - than the Ariane 5 launch. And as\Na result, one of the sideways values in
Dialogue: 0,0:01:58.83,0:02:04.74,Default,,0000,0000,0000,,the guidance control software overflowed.\NBad. And hence, the guidance software
Dialogue: 0,0:02:04.74,0:02:08.45,Default,,0000,0000,0000,,decided that something bad was going wrong\Nand in order to not land rockets on
Dialogue: 0,0:02:08.45,0:02:15.84,Default,,0000,0000,0000,,people's heads, it kindly blew itself up.\NOkay. So that's a spectacular. Sometimes
Dialogue: 0,0:02:15.84,0:02:21.20,Default,,0000,0000,0000,,they go wrong in insidious ways. And you\Npeople probably know much more about that
Dialogue: 0,0:02:21.20,0:02:29.37,Default,,0000,0000,0000,,than me. Very insidious ways. Exploited by\Nbad people to our detriment. And they go
Dialogue: 0,0:02:29.37,0:02:36.99,Default,,0000,0000,0000,,wrong in insidious ways, exploited by our\Nkindly governments for our protection.
Dialogue: 0,0:02:36.99,0:02:44.96,Default,,0000,0000,0000,,Right? And these - there are many, many,\Nmany different causes of these things but
Dialogue: 0,0:02:44.96,0:02:49.42,Default,,0000,0000,0000,,many of these causes are completely\Ntrivial. You know, you have one line of
Dialogue: 0,0:02:49.42,0:02:56.15,Default,,0000,0000,0000,,code in the wrong place - something like\Nthat, right? So that's very, very bad and
Dialogue: 0,0:02:56.15,0:03:01.04,Default,,0000,0000,0000,,you're all conscious of how bad that is.\NBut from my point of view, this is as
Dialogue: 0,0:03:01.04,0:03:06.96,Default,,0000,0000,0000,,nothing with the real disaster that we\Nhave been facing and continue to face.
Dialogue: 0,0:03:06.96,0:03:14.95,Default,,0000,0000,0000,,Right? The real disaster is the enormous\Nwaste of human life and energy and effort
Dialogue: 0,0:03:14.95,0:03:21.36,Default,,0000,0000,0000,,and emotion dealing with these crap\Nmachines that we've built. Right? And it's
Dialogue: 0,0:03:21.36,0:03:25.49,Default,,0000,0000,0000,,hard to quantify that. I did a little\Nexperiment a couple of months ago. I
Dialogue: 0,0:03:25.49,0:03:34.03,Default,,0000,0000,0000,,Googled up "Android problem" and "Windows\Nproblem" and got about 300 million hits
Dialogue: 0,0:03:34.03,0:03:43.84,Default,,0000,0000,0000,,for each, right? Somehow indicative of the\Namount of wrongness. So this should you
Dialogue: 0,0:03:43.84,0:03:49.79,Default,,0000,0000,0000,,seem kind of familiar to you. If you think\Nback - think back to when you were young.
Dialogue: 0,0:03:49.79,0:03:55.70,Default,,0000,0000,0000,,Maybe back in the 19th century when you\Nwere young, and what were you doing then
Dialogue: 0,0:03:55.70,0:04:00.94,Default,,0000,0000,0000,,as a community of hackers and makers and\Nbuilders? Well, this was the full-on
Dialogue: 0,0:04:00.94,0:04:07.13,Default,,0000,0000,0000,,industrial revolution. You were building\Nstuff. You were building beautiful bridges
Dialogue: 0,0:04:07.13,0:04:14.74,Default,,0000,0000,0000,,of cast-iron and stone with numerous\Narches and pillars. And every so often
Dialogue: 0,0:04:14.74,0:04:22.30,Default,,0000,0000,0000,,they would fall down. I believe someone\Nmiscalculated the wind loading. And we
Dialogue: 0,0:04:22.30,0:04:30.63,Default,,0000,0000,0000,,would build magical steam engines to whisk\Nus away. And every so often, they would
Dialogue: 0,0:04:30.63,0:04:35.77,Default,,0000,0000,0000,,blow up. And that kind of thing, as you\Nmay have noticed in the last hundred years
Dialogue: 0,0:04:35.77,0:04:41.81,Default,,0000,0000,0000,,- sorry - that kind of thing doesn't\Nhappen very often any more, right? We have
Dialogue: 0,0:04:41.81,0:04:46.99,Default,,0000,0000,0000,,pretty good civil and mechanical\Nengineering. And what does it mean to have
Dialogue: 0,0:04:46.99,0:04:52.62,Default,,0000,0000,0000,,good civil and mechanical engineering? It\Nmeans that we know enough thermodynamics
Dialogue: 0,0:04:52.62,0:04:56.75,Default,,0000,0000,0000,,and materials science and quality control\Nmanagement and all that kind of thing to
Dialogue: 0,0:04:56.75,0:05:01.83,Default,,0000,0000,0000,,model our designs before we build them and\Npredict how they're going to behave pretty
Dialogue: 0,0:05:01.83,0:05:10.75,Default,,0000,0000,0000,,well and with pretty high confidence,\Nright? I see an optimisation in this talk.
Dialogue: 0,0:05:10.75,0:05:15.34,Default,,0000,0000,0000,,For computer science, for computing\Nsystems we can predict with 100 per cent
Dialogue: 0,0:05:15.34,0:05:20.45,Default,,0000,0000,0000,,certainty that they will not work.\NAh, time for lunch!
Dialogue: 0,0:05:20.45,0:05:26.51,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:05:26.51,0:05:33.33,Default,,0000,0000,0000,,But it's not a very satisfying answer,\Nreally. So why is it so hard? Let me
Dialogue: 0,0:05:33.33,0:05:38.50,Default,,0000,0000,0000,,discuss a couple of the reasons why\Ncomputing is tricky. In some sense,
Dialogue: 0,0:05:38.50,0:05:45.43,Default,,0000,0000,0000,,trickier than steam engines. The first\Nreason is that there is just too much
Dialogue: 0,0:05:45.43,0:05:50.36,Default,,0000,0000,0000,,code. Right? So this is one of the more\Nscary graphs I've found on the internet
Dialogue: 0,0:05:50.36,0:05:55.47,Default,,0000,0000,0000,,recently. This is a measure of code in\Nhundreds of millions of lines. Each of
Dialogue: 0,0:05:55.47,0:06:00.25,Default,,0000,0000,0000,,these blocks I think is 10 million lines\Nof code. And in the little letters - you
Dialogue: 0,0:06:00.25,0:06:04.86,Default,,0000,0000,0000,,might not be able to see we have Android\Nand the Large Hadron Collider and Windows
Dialogue: 0,0:06:04.86,0:06:12.82,Default,,0000,0000,0000,,Vista and Facebook, US Army Future Combat\NSystem, Mac OS and software in a high-end
Dialogue: 0,0:06:12.82,0:06:15.01,Default,,0000,0000,0000,,car. Right?
Dialogue: 0,0:06:15.01,0:06:23.23,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:06:23.23,0:06:25.32,Default,,0000,0000,0000,,I'm flying home.
Dialogue: 0,0:06:25.32,0:06:27.81,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:06:27.81,0:06:33.52,Default,,0000,0000,0000,,So we that's a bit of a problem, really.\NWe're never going to get that right. Then
Dialogue: 0,0:06:33.52,0:06:37.41,Default,,0000,0000,0000,,there's too much legacy complexity there,\Nright? Really too much. So as
Dialogue: 0,0:06:37.41,0:06:41.84,Default,,0000,0000,0000,,right-minded, pure-minded people you might\Nthink that software and hardware should be
Dialogue: 0,0:06:41.84,0:06:46.49,Default,,0000,0000,0000,,architected beautifully with regular\Nstructure a bit like a Mies van der Rohe
Dialogue: 0,0:06:46.49,0:06:53.66,Default,,0000,0000,0000,,skyscraper or something. Clean. Okay. You\Nknow that's not realistic, right? You
Dialogue: 0,0:06:53.66,0:06:59.47,Default,,0000,0000,0000,,might expect a bit of baroqueness. You\Nmight expect maybe something more like
Dialogue: 0,0:06:59.47,0:07:02.68,Default,,0000,0000,0000,,this. You know, it's a bit twiddly but it\Nstill hangs together. It's still got
Dialogue: 0,0:07:02.68,0:07:08.16,Default,,0000,0000,0000,,structure. It still works. But then you\Nstop and you think and you realise that
Dialogue: 0,0:07:08.16,0:07:15.77,Default,,0000,0000,0000,,software and hardware is built by very\Nsmart people and usually in big groups and
Dialogue: 0,0:07:15.77,0:07:20.30,Default,,0000,0000,0000,,subject to a whole assortment of rather\Nintense commercial pressure and related
Dialogue: 0,0:07:20.30,0:07:25.21,Default,,0000,0000,0000,,open-source pressure and using the best\Ncomponents and tools that they know and
Dialogue: 0,0:07:25.21,0:07:27.17,Default,,0000,0000,0000,,they like.
Dialogue: 0,0:07:27.17,0:07:34.52,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:07:34.52,0:07:38.99,Default,,0000,0000,0000,,Someone from the room: (Indistinct)\NYou forgot management!
Dialogue: 0,0:07:38.99,0:07:42.48,Default,,0000,0000,0000,,And the best management that\Nhuman beings can arrange.
Dialogue: 0,0:07:42.48,0:07:49.68,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:07:49.68,0:07:54.91,Default,,0000,0000,0000,,So we end up with something\Nspectacularly ingenious.
Dialogue: 0,0:07:54.91,0:08:05.49,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:08:05.49,0:08:09.73,Default,,0000,0000,0000,,You can see here, if you look\Nclosely, you can see all the parts.
Dialogue: 0,0:08:09.73,0:08:11.00,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:08:11.00,0:08:15.77,Default,,0000,0000,0000,,This was just a found picture from the\Ninternet. But you can see there's a bunch
Dialogue: 0,0:08:15.77,0:08:19.06,Default,,0000,0000,0000,,of, you know, transparent sort of\Nsilicon-like stuff down here. Let's say
Dialogue: 0,0:08:19.06,0:08:25.08,Default,,0000,0000,0000,,that's our hardware. And over here, I see\Na C compiler with all of its phases.
Dialogue: 0,0:08:25.08,0:08:28.60,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:08:28.60,0:08:36.93,Default,,0000,0000,0000,,And these bottles, that's the file system,\NI reckon. And there's a TCP stack in here
Dialogue: 0,0:08:36.93,0:08:43.69,Default,,0000,0000,0000,,somewhere. And there's a piece that\Nbelongs to the NSA, obviously. And up
Dialogue: 0,0:08:43.69,0:08:50.26,Default,,0000,0000,0000,,here, I think up here - yeah, there's a\NJavaScript engine and a TLS stack and a
Dialogue: 0,0:08:50.26,0:08:56.05,Default,,0000,0000,0000,,web browser. And then perched at the top\Nis the software that most people use to
Dialogue: 0,0:08:56.05,0:08:57.91,Default,,0000,0000,0000,,talk to their banks.
Dialogue: 0,0:08:57.91,0:09:01.49,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:09:01.49,0:09:09.49,Default,,0000,0000,0000,,It's just - it's just insane, right? And\Nthen we have to look at how we build these
Dialogue: 0,0:09:09.49,0:09:14.09,Default,,0000,0000,0000,,pieces, right? So we build them\Nfundamentally by a process of trial and
Dialogue: 0,0:09:14.09,0:09:20.65,Default,,0000,0000,0000,,error, right? Just occasionally we write\Nsome specifications in text. And then we
Dialogue: 0,0:09:20.65,0:09:26.03,Default,,0000,0000,0000,,write some code and maybe we write a few\Nad hoc texts and then we test and fix
Dialogue: 0,0:09:26.03,0:09:30.61,Default,,0000,0000,0000,,until the thing is marketable and then we\Ntest and fix and extend until the thing is
Dialogue: 0,0:09:30.61,0:09:36.07,Default,,0000,0000,0000,,no longer marketable and then we keep on\Nusing it until we can't anymore. Right? So
Dialogue: 0,0:09:36.07,0:09:40.26,Default,,0000,0000,0000,,the fundamental process that we're using\Nto develop these systems is trial and
Dialogue: 0,0:09:40.26,0:09:47.93,Default,,0000,0000,0000,,error by exploring particular execution\Npaths of the code on particular inputs.
Dialogue: 0,0:09:47.93,0:09:54.46,Default,,0000,0000,0000,,But - you know this, but I want to\Nhighlight - there are too many. The number
Dialogue: 0,0:09:54.46,0:09:59.65,Default,,0000,0000,0000,,of execution paths scales typically at\Nleast exponentially with the size of the
Dialogue: 0,0:09:59.65,0:10:04.49,Default,,0000,0000,0000,,code and the number of states scales\Nexponentially with the size of the data
Dialogue: 0,0:10:04.49,0:10:08.79,Default,,0000,0000,0000,,that you're dealing with and the number of\Npossible inputs is also shockingly large.
Dialogue: 0,0:10:08.79,0:10:14.92,Default,,0000,0000,0000,,There is no way that we can do this and we\Nshould perhaps stop deluding ourselves
Dialogue: 0,0:10:14.92,0:10:21.13,Default,,0000,0000,0000,,that there is. And then the most\Nfundamental reason that computers are hard
Dialogue: 0,0:10:21.13,0:10:27.90,Default,,0000,0000,0000,,is that they are too discrete, right? If\Nyou take a bridge or, I don't know, a
Dialogue: 0,0:10:27.90,0:10:36.52,Default,,0000,0000,0000,,chair or something - where's something\Nslightly bendable? You take a chair and
Dialogue: 0,0:10:36.52,0:10:44.20,Default,,0000,0000,0000,,you exert a bit more force on it than it's\Nused to - I'm not very strong - and it
Dialogue: 0,0:10:44.20,0:10:51.30,Default,,0000,0000,0000,,bends a bit. It deforms continuously. If\Nyou take a bridge and you tighten up one
Dialogue: 0,0:10:51.30,0:10:55.24,Default,,0000,0000,0000,,of the bolts a bit too much or you\Nunderspecify one of the girders by 10 per
Dialogue: 0,0:10:55.24,0:11:01.02,Default,,0000,0000,0000,,cent, occasionally you'll reach a point of\Ncatastrophic failure but usually it will
Dialogue: 0,0:11:01.02,0:11:04.09,Default,,0000,0000,0000,,just be a little bit weaker or a little\Nbit stronger or a little bit wibbly.
Dialogue: 0,0:11:04.09,0:11:08.96,Default,,0000,0000,0000,,Right? But computer systems, you change a\Nbit - sometimes it doesn't make a
Dialogue: 0,0:11:08.96,0:11:13.18,Default,,0000,0000,0000,,difference but disturbingly often you\Nchange a line of code - as in system of
Dialogue: 0,0:11:13.18,0:11:19.60,Default,,0000,0000,0000,,those bugs that we were talking about -\Nthe whole thing becomes broken, right? So
Dialogue: 0,0:11:19.60,0:11:26.93,Default,,0000,0000,0000,,it's quite different from that traditional\Nengineering. It's really different. Okay.
Dialogue: 0,0:11:26.93,0:11:34.85,Default,,0000,0000,0000,,So, "A New Dawn", this thing is titled.\NWhat can we do? What might we do? So I'm
Dialogue: 0,0:11:34.85,0:11:40.88,Default,,0000,0000,0000,,going to talk about several different\Npossibilities, all right? One thing, we
Dialogue: 0,0:11:40.88,0:11:46.49,Default,,0000,0000,0000,,can do more of the stuff which is\Ntraditionally called software engineering.
Dialogue: 0,0:11:46.49,0:11:50.91,Default,,0000,0000,0000,,It's not really engineering in my book,\Nbut some of it's good. I mean, it's
Dialogue: 0,0:11:50.91,0:11:55.12,Default,,0000,0000,0000,,useful, you know? We can do more testing\Nand have more assertions in our code and
Dialogue: 0,0:11:55.12,0:11:58.92,Default,,0000,0000,0000,,better management maybe and all that kind\Nof stuff. We can do all that - we should
Dialogue: 0,0:11:58.92,0:12:04.34,Default,,0000,0000,0000,,do all that, but it's not going to make a\Nvery big change, all right? It's not
Dialogue: 0,0:12:04.34,0:12:13.99,Default,,0000,0000,0000,,addressing any of those root causes of the\Nproblem. What else could we do? So as an
Dialogue: 0,0:12:13.99,0:12:18.57,Default,,0000,0000,0000,,academic computer scientist, I've devoted\Nseveral years of my life to working in the
Dialogue: 0,0:12:18.57,0:12:24.51,Default,,0000,0000,0000,,area of programming languages and I look\Nat the programming languages used out
Dialogue: 0,0:12:24.51,0:12:36.92,Default,,0000,0000,0000,,there in the world today. Oh, it's just\Ndisgusting! It's shocking.
Dialogue: 0,0:12:36.92,0:12:43.40,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:12:43.40,0:12:50.42,Default,,0000,0000,0000,,The reasons that languages become popular\Nand built into our shared infrastructure,
Dialogue: 0,0:12:50.42,0:12:54.79,Default,,0000,0000,0000,,the reasons for that have almost nothing\Nto do with how well those languages are
Dialogue: 0,0:12:54.79,0:13:00.60,Default,,0000,0000,0000,,designed and in fact whether\Nthey are designed at all, right?
Dialogue: 0,0:13:00.60,0:13:04.11,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:13:04.11,0:13:09.04,Default,,0000,0000,0000,,So I didn't really want to get too much\Nhate mail after this talk so I'm going to
Dialogue: 0,0:13:09.04,0:13:13.100,Default,,0000,0000,0000,,try and avoid naming particular languages\Nas much as I can, but I encourage you to
Dialogue: 0,0:13:13.100,0:13:20.28,Default,,0000,0000,0000,,think away as I speak and imagine the\Nexamples. No, that was - I didn't want to
Dialogue: 0,0:13:20.28,0:13:23.73,Default,,0000,0000,0000,,get much hate mail. Sorry.
Dialogue: 0,0:13:23.73,0:13:25.16,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:13:25.16,0:13:26.58,Default,,0000,0000,0000,,So...
Dialogue: 0,0:13:26.58,0:13:32.07,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:13:32.07,0:13:36.54,Default,,0000,0000,0000,,So at the very least, we could use\Nprogramming languages based on ideas from
Dialogue: 0,0:13:36.54,0:13:47.39,Default,,0000,0000,0000,,the 1970s instead of the 1960s. I mean,\Nreally, come on. Right? You know, back in
Dialogue: 0,0:13:47.39,0:13:54.12,Default,,0000,0000,0000,,'67 or '69 or whatever we had ECPL and C\Nand only a couple of years later we had
Dialogue: 0,0:13:54.12,0:14:00.07,Default,,0000,0000,0000,,languages that guaranteed type and memory\Nsafety and enforcement of abstraction
Dialogue: 0,0:14:00.07,0:14:05.09,Default,,0000,0000,0000,,boundaries and gave us rich mechanisms for\Nprogramming so we could say what we mean
Dialogue: 0,0:14:05.09,0:14:11.35,Default,,0000,0000,0000,,and not futz about with 23 million\Npointers, about 1 per cent of which were
Dialogue: 0,0:14:11.35,0:14:16.63,Default,,0000,0000,0000,,completely wrong, right? So for any\Nparticular - in the context of any
Dialogue: 0,0:14:16.63,0:14:20.46,Default,,0000,0000,0000,,particular project or any particular\Nexisting legacy infrastructure there may
Dialogue: 0,0:14:20.46,0:14:25.79,Default,,0000,0000,0000,,be very good reasons why one just can't\Nmake a switch. Right? But for us
Dialogue: 0,0:14:25.79,0:14:31.86,Default,,0000,0000,0000,,collectively, there is no excuse. It's\Njust wretched, right?
Dialogue: 0,0:14:31.86,0:14:37.04,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:14:37.04,0:14:40.97,Default,,0000,0000,0000,,It's completely bonkers. And then the\Nother thing that you see as a programming
Dialogue: 0,0:14:40.97,0:14:49.24,Default,,0000,0000,0000,,language researcher is that - er, well, to\Nmake another analogy, it looks as if
Dialogue: 0,0:14:49.24,0:14:55.53,Default,,0000,0000,0000,,anyone who was capable of driving a car\Nconsidered themselves an expert on car
Dialogue: 0,0:14:55.53,0:15:03.56,Default,,0000,0000,0000,,design, right? There is in fact a rather\Nwell-established subject of, you know,
Dialogue: 0,0:15:03.56,0:15:08.24,Default,,0000,0000,0000,,programming language design and we know\Nhow to specify completely precisely,
Dialogue: 0,0:15:08.24,0:15:13.02,Default,,0000,0000,0000,,mathematically precisely not just the\Nsyntax like we had in these BNF grammars
Dialogue: 0,0:15:13.02,0:15:18.16,Default,,0000,0000,0000,,from the 1960s and still have, but also\Nthe behaviour of these things. We know how
Dialogue: 0,0:15:18.16,0:15:22.70,Default,,0000,0000,0000,,to specify a few operational semantics and\Nthe type systems. And we know how to do
Dialogue: 0,0:15:22.70,0:15:27.36,Default,,0000,0000,0000,,mathematical proofs that our language\Ndesigns are self-consistent, that they do
Dialogue: 0,0:15:27.36,0:15:35.06,Default,,0000,0000,0000,,guarantee good properties of arbitrary\Nwell-typed programs that you write, right?
Dialogue: 0,0:15:35.06,0:15:38.76,Default,,0000,0000,0000,,We can do this now. We can do this, if we\Nhave to, post hoc. And people are doing
Dialogue: 0,0:15:38.76,0:15:45.67,Default,,0000,0000,0000,,this for JavaScript and C and god help\Nthem, PHP and other such languages. But
Dialogue: 0,0:15:45.67,0:15:50.83,Default,,0000,0000,0000,,even better, we can do it at design time.\NAnd if you do this at design time, you see
Dialogue: 0,0:15:50.83,0:15:55.51,Default,,0000,0000,0000,,the structure. You have to - the act of\Nwriting that specification forces you to
Dialogue: 0,0:15:55.51,0:15:59.94,Default,,0000,0000,0000,,consider all the cases and all the\Ninteractions between features. You can
Dialogue: 0,0:15:59.94,0:16:07.86,Default,,0000,0000,0000,,still get it wrong, but you get it wrong\Nin more interesting ways. Right? So people
Dialogue: 0,0:16:07.86,0:16:12.12,Default,,0000,0000,0000,,are starting to do this now. So I think\Nthere was a talk on the first day of this
Dialogue: 0,0:16:12.12,0:16:17.43,Default,,0000,0000,0000,,by Hannes and David who are building\Nsystem software in maybe not the best sys
Dialogue: 0,0:16:17.43,0:16:21.80,Default,,0000,0000,0000,,language you could possibly imagine, but\Nsomething which compared with C is as
Dialogue: 0,0:16:21.80,0:16:27.76,Default,,0000,0000,0000,,manna from heaven. Anil Madhavapeddy and\Nhis colleagues in Cambridge have been
Dialogue: 0,0:16:27.76,0:16:32.76,Default,,0000,0000,0000,,working hard to build system software in\Nat least moderately modern languages. And
Dialogue: 0,0:16:32.76,0:16:40.78,Default,,0000,0000,0000,,it works. Sometimes you have to use C but\Nsurprisingly often you really don't. Yeah,
Dialogue: 0,0:16:40.78,0:16:47.05,Default,,0000,0000,0000,,so I teach, as my introducer said, in the\NUniversity of Cambridge. And I teach
Dialogue: 0,0:16:47.05,0:16:51.27,Default,,0000,0000,0000,,semantics. And one of my fears is that I\Nwill accidentally let someone out in the
Dialogue: 0,0:16:51.27,0:16:54.97,Default,,0000,0000,0000,,world who will accidentally find\Nthemselves over a weekend inventing a
Dialogue: 0,0:16:54.97,0:16:58.15,Default,,0000,0000,0000,,little scripting language which will\Naccidentally take over the world and
Dialogue: 0,0:16:58.15,0:17:05.36,Default,,0000,0000,0000,,become popular and I won't have explained\Nto them what they have to do or even that
Dialogue: 0,0:17:05.36,0:17:08.19,Default,,0000,0000,0000,,there is a subject they have to\Nunderstand. And if you want to understand
Dialogue: 0,0:17:08.19,0:17:18.74,Default,,0000,0000,0000,,it, there's lots of stuff you can look at.\NOkay. Let's go to the uppermost extreme.
Dialogue: 0,0:17:18.74,0:17:23.83,Default,,0000,0000,0000,,If we want software and hardware that\Nactually works, we should prove it
Dialogue: 0,0:17:23.83,0:17:30.70,Default,,0000,0000,0000,,correct. Right? So this is something which\Nacademics, especially in the domain of
Dialogue: 0,0:17:30.70,0:17:36.83,Default,,0000,0000,0000,,labelled "formal methods" in the '70s and\N'80s, they've been pushing this, promoting
Dialogue: 0,0:17:36.83,0:17:44.79,Default,,0000,0000,0000,,this as an idea and a promise and an\Nexhortation for decades, right? Why don't
Dialogue: 0,0:17:44.79,0:17:50.17,Default,,0000,0000,0000,,we just prove our programs correct? And\Nfor some of those decades it wasn't really
Dialogue: 0,0:17:50.17,0:17:54.57,Default,,0000,0000,0000,,plausible. I remember back when I was\Nconsiderably younger, it was a big thing
Dialogue: 0,0:17:54.57,0:17:59.54,Default,,0000,0000,0000,,to proof that if you took a linked list\Nand reversed it twice, you got back the
Dialogue: 0,0:17:59.54,0:18:08.06,Default,,0000,0000,0000,,same thing. Right? That was hard, then.\NBut now, well, we can't do this for the
Dialogue: 0,0:18:08.06,0:18:14.42,Default,,0000,0000,0000,,Linux kernel, let's say, but we can\Nsurprising often do this. And I just give
Dialogue: 0,0:18:14.42,0:18:19.59,Default,,0000,0000,0000,,you a couple of the examples of modern\Nday, state-of-the-art academic
Dialogue: 0,0:18:19.59,0:18:25.72,Default,,0000,0000,0000,,verification projects. People have\Nverified compilers all the way from C-like
Dialogue: 0,0:18:25.72,0:18:31.77,Default,,0000,0000,0000,,languages down to assembly or from ML-like\Nlanguages. You know, higher-order
Dialogue: 0,0:18:31.77,0:18:36.96,Default,,0000,0000,0000,,functional imperative languages all the\Nway down to binary models of how x86
Dialogue: 0,0:18:36.96,0:18:44.47,Default,,0000,0000,0000,,behaves. And people have verified LLVM\Noptimisation paths. There's verified
Dialogue: 0,0:18:44.47,0:18:49.88,Default,,0000,0000,0000,,software fault isolation which I believe\Ngoes faster than the original non-verified
Dialogue: 0,0:18:49.88,0:18:56.13,Default,,0000,0000,0000,,form. Win for them. There's a verified\Nhypervisor from Nectar group in Australia.
Dialogue: 0,0:18:56.13,0:19:00.57,Default,,0000,0000,0000,,Right? Verified secure hypervisor with\Nproofs of security properties. There's any
Dialogue: 0,0:19:00.57,0:19:06.69,Default,,0000,0000,0000,,amount of work verifying crypto protocols,\Nsometimes with respect to assumptions - I
Dialogue: 0,0:19:06.69,0:19:12.51,Default,,0000,0000,0000,,think reasonable assumption on what the\Nunderlying mathematics is giving you. So
Dialogue: 0,0:19:12.51,0:19:22.92,Default,,0000,0000,0000,,we can do this. I maybe have to explain a\Nbit what I mean by "prove". To some
Dialogue: 0,0:19:22.92,0:19:30.99,Default,,0000,0000,0000,,computery people, "I proved it works"\Nmeans "I tested it a little bit".
Dialogue: 0,0:19:30.99,0:19:32.51,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:19:32.51,0:19:34.96,Default,,0000,0000,0000,,In extremis, "it compiled".
Dialogue: 0,0:19:34.96,0:19:44.12,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:19:44.12,0:19:50.77,Default,,0000,0000,0000,,To a program analysis person, you might\Nrun some sophisticated tool but written in
Dialogue: 0,0:19:50.77,0:19:54.65,Default,,0000,0000,0000,,untrusted code and possibly doing an\Napproximate and maybe unsound analysis and
Dialogue: 0,0:19:54.65,0:19:59.72,Default,,0000,0000,0000,,you might find an absence of certain kinds\Nof bugs. That's tremendously useful; it's
Dialogue: 0,0:19:59.72,0:20:04.64,Default,,0000,0000,0000,,not what we would really call "proved".\NI mean, nor would they, to be fair.
Dialogue: 0,0:20:04.64,0:20:08.97,Default,,0000,0000,0000,,Scientists generally don't use the word\Nbecause they know they're not doing it,
Dialogue: 0,0:20:08.97,0:20:13.56,Default,,0000,0000,0000,,right? They're doing controlled\Nexperiments, which gives them, you know,
Dialogue: 0,0:20:13.56,0:20:20.07,Default,,0000,0000,0000,,information for or against some\Nhypothesis. Mathematician write proofs.
Dialogue: 0,0:20:20.07,0:20:25.14,Default,,0000,0000,0000,,You probably did that when you were young.\NAnd those proofs are careful mathematical
Dialogue: 0,0:20:25.14,0:20:30.14,Default,,0000,0000,0000,,arguments usually written on paper with\Npencils and their aim is to convince a
Dialogue: 0,0:20:30.14,0:20:33.39,Default,,0000,0000,0000,,human being that if that mathematician was\Nreally nailed up against the wall and
Dialogue: 0,0:20:33.39,0:20:38.98,Default,,0000,0000,0000,,pushed, they could expand that into a\Ncompletely detailed proof. But what we
Dialogue: 0,0:20:38.98,0:20:47.75,Default,,0000,0000,0000,,have in computing, we don't have the rich\Nmathematical structure that these people
Dialogue: 0,0:20:47.75,0:20:51.95,Default,,0000,0000,0000,,are working with, we have a tremendous\Namount of ad hoc and stupid detail mixed
Dialogue: 0,0:20:51.95,0:20:57.77,Default,,0000,0000,0000,,in which a smidgin of rich mathematical\Nstructure. So - and we have hundreds of
Dialogue: 0,0:20:57.77,0:21:03.40,Default,,0000,0000,0000,,millions of lines of code. So this is just\Nnot going to cut it. And if we want say
Dialogue: 0,0:21:03.40,0:21:08.44,Default,,0000,0000,0000,,the word "prove" ever, then the only thing\Nwhich is legitimate is to do honest
Dialogue: 0,0:21:08.44,0:21:13.23,Default,,0000,0000,0000,,program proof and that means you have to\Nhave some system that machine-checks that
Dialogue: 0,0:21:13.23,0:21:17.54,Default,,0000,0000,0000,,your proof is actually a proof. And\Nsometime we'll also have machines that
Dialogue: 0,0:21:17.54,0:21:22.25,Default,,0000,0000,0000,,will sort of help and sort of hinder that\Nprocess, right? And there's a variety of
Dialogue: 0,0:21:22.25,0:21:27.34,Default,,0000,0000,0000,,these systems. Coq and HOL4 and Isabelle4\N- Isabelle/HOL and what have you that we
Dialogue: 0,0:21:27.34,0:21:36.80,Default,,0000,0000,0000,,can look up. So using these systems we can\Nprove nontrivial facts about these. Not
Dialogue: 0,0:21:36.80,0:21:41.53,Default,,0000,0000,0000,,necessarily that they do what you want\Nthem to do, but that they meet the precise
Dialogue: 0,0:21:41.53,0:21:48.52,Default,,0000,0000,0000,,specification that we've written down. We\Ncan do that. But it's tricky, right? So
Dialogue: 0,0:21:48.52,0:21:52.93,Default,,0000,0000,0000,,these projects, these are by academic\Nstandards all quite big, you know? This is
Dialogue: 0,0:21:52.93,0:21:58.01,Default,,0000,0000,0000,,something like, I don't know, 10 people\Nfor a few years or something. By industry
Dialogue: 0,0:21:58.01,0:22:03.40,Default,,0000,0000,0000,,scale, maybe not that big. By your scale,\Nmaybe not that big. But still a lot of
Dialogue: 0,0:22:03.40,0:22:08.15,Default,,0000,0000,0000,,work for a research group to do. And quite\Nhigh-end work. It can take, you know,
Dialogue: 0,0:22:08.15,0:22:13.73,Default,,0000,0000,0000,,literally a few years to become really\Nfluent in using these tools, right? And
Dialogue: 0,0:22:13.73,0:22:20.14,Default,,0000,0000,0000,,there isn't as yet sort of an open-source,\Ncollaborative movement doing this kind of
Dialogue: 0,0:22:20.14,0:22:26.71,Default,,0000,0000,0000,,stuff. Maybe it's the time to start. Maybe\Nin five years, ten years. I don't know. If
Dialogue: 0,0:22:26.71,0:22:35.68,Default,,0000,0000,0000,,you want a challenge, there's a challenge.\NBut it's really quite hard, right? It's
Dialogue: 0,0:22:35.68,0:22:40.83,Default,,0000,0000,0000,,not something that one can quite put\Nforward credibly as a solution for all
Dialogue: 0,0:22:40.83,0:22:46.53,Default,,0000,0000,0000,,software and hardware development, right?\NSo that leads me to, like an intermediate
Dialogue: 0,0:22:46.53,0:22:53.40,Default,,0000,0000,0000,,point. That should have been a four there.\NWhat can we do which improves the quality
Dialogue: 0,0:22:53.40,0:22:58.34,Default,,0000,0000,0000,,of our system, which injects some\Nmathematical rigour but which involves
Dialogue: 0,0:22:58.34,0:23:06.37,Default,,0000,0000,0000,,less work and is kind of easy? And what we\Ncan do is take some of these interfaces
Dialogue: 0,0:23:06.37,0:23:11.68,Default,,0000,0000,0000,,and be precise about what they are. And\Ninitially, we have to do that after the
Dialogue: 0,0:23:11.68,0:23:16.94,Default,,0000,0000,0000,,fact. We have to reverse-engineer good\Nspecs of existing stuff. But then we can
Dialogue: 0,0:23:16.94,0:23:23.47,Default,,0000,0000,0000,,use the same techniques to make much\Ncleaner and better-tested and things which
Dialogue: 0,0:23:23.47,0:23:30.67,Default,,0000,0000,0000,,are easier to test in the future. That's\Nthe idea. So my colleagues and I have been
Dialogue: 0,0:23:30.67,0:23:35.36,Default,,0000,0000,0000,,doing this kind of stuff for the last\Nquite a few years and I just want to give
Dialogue: 0,0:23:35.36,0:23:41.57,Default,,0000,0000,0000,,you just a - two little vignettes just to\Nsort of show you how it goes. So I can't
Dialogue: 0,0:23:41.57,0:23:46.76,Default,,0000,0000,0000,,give you much detail. And this is,\Nobviously, joint work with a whole bunch
Dialogue: 0,0:23:46.76,0:23:55.40,Default,,0000,0000,0000,,of very smart and good people, some of\Nwhich I name here. So this is not me, this
Dialogue: 0,0:23:55.40,0:24:00.84,Default,,0000,0000,0000,,is a whole community effort. So I'm going\Nto talk for a little bit about the
Dialogue: 0,0:24:00.84,0:24:05.80,Default,,0000,0000,0000,,behaviour of multiprocessors, so at that\Nhardware interface. And I'm going to talk
Dialogue: 0,0:24:05.80,0:24:11.09,Default,,0000,0000,0000,,a tiny little bit about the behaviour of\Nthe TCP and socket API, right? Network
Dialogue: 0,0:24:11.09,0:24:17.17,Default,,0000,0000,0000,,protocols. So - and there'll be some\Nsimilarities and some differences between
Dialogue: 0,0:24:17.17,0:24:24.99,Default,,0000,0000,0000,,these two things. So multiprocessors. You\Nprobably want your computers to go fast.
Dialogue: 0,0:24:24.99,0:24:31.09,Default,,0000,0000,0000,,Most people do. And it's an obvious idea\Nto glom together, because processors don't
Dialogue: 0,0:24:31.09,0:24:35.53,Default,,0000,0000,0000,,go that fast, let's glom together a whole\Nbunch of processors and make them all talk
Dialogue: 0,0:24:35.53,0:24:46.15,Default,,0000,0000,0000,,to the same memory. This is not a new\Nidea. It goes back at least to 1962 when
Dialogue: 0,0:24:46.15,0:24:51.38,Default,,0000,0000,0000,,the Burroughs D825 had, I think, two\Nprocessors talking to a single shared
Dialogue: 0,0:24:51.38,0:24:55.85,Default,,0000,0000,0000,,memory. It had outstanding features\Nincluding truly modular hardware with
Dialogue: 0,0:24:55.85,0:25:02.65,Default,,0000,0000,0000,,parallel processing throughout, and - some\Nthings do not change very much - the
Dialogue: 0,0:25:02.65,0:25:11.64,Default,,0000,0000,0000,,complement of compiling languages was to\Nbe expanded, right? 1962, so that'll be 52
Dialogue: 0,0:25:11.64,0:25:18.82,Default,,0000,0000,0000,,years ago. Deary me. Okay. Now, how do\Nthese things behave? So let me show you
Dialogue: 0,0:25:18.82,0:25:22.90,Default,,0000,0000,0000,,some code, right? It's a hacker\Nconference. There should be code. Let me
Dialogue: 0,0:25:22.90,0:25:29.03,Default,,0000,0000,0000,,show you two example programs and these\Nwill both be programs with two threads and
Dialogue: 0,0:25:29.03,0:25:34.57,Default,,0000,0000,0000,,they will both be acting on two shared\Nvariables, X and Y. And in the initial
Dialogue: 0,0:25:34.57,0:25:42.90,Default,,0000,0000,0000,,state, X and Y are both zero. So, the\Nfirst program. On this thread we write X
Dialogue: 0,0:25:42.90,0:25:48.97,Default,,0000,0000,0000,,and then we read Y, and over here we write\NY and then we read X, right? Now, these
Dialogue: 0,0:25:48.97,0:25:53.63,Default,,0000,0000,0000,,are operating, you know, in an\Ninterleaving concurrency, you might think,
Dialogue: 0,0:25:53.63,0:25:58.03,Default,,0000,0000,0000,,so there's no synchronisation between\Nthose two threads so we might interleave
Dialogue: 0,0:25:58.03,0:26:03.27,Default,,0000,0000,0000,,them. We might run all of thread 0 before\Nall of thread 1 or all of thread 1 before
Dialogue: 0,0:26:03.27,0:26:10.34,Default,,0000,0000,0000,,all of thread 0 or they might be mixed in\Nlike that or like that or like that or
Dialogue: 0,0:26:10.34,0:26:16.94,Default,,0000,0000,0000,,like that. There's six possible ways of\Ninterleaving two lists of two things. And
Dialogue: 0,0:26:16.94,0:26:22.98,Default,,0000,0000,0000,,in all of those ways you never see in the\Nsame execution that this reads from the
Dialogue: 0,0:26:22.98,0:26:30.17,Default,,0000,0000,0000,,initial state AND this reads from the\Ninitial state. You never see that. So you
Dialogue: 0,0:26:30.17,0:26:35.48,Default,,0000,0000,0000,,might expect and you might assume in your\Ncode that these are the possible outcomes.
Dialogue: 0,0:26:35.48,0:26:40.49,Default,,0000,0000,0000,,So what happens if you were to actually\Nrun that code on my laptop in a particular
Dialogue: 0,0:26:40.49,0:26:46.97,Default,,0000,0000,0000,,test harness? Well, okay, you see\Noccasionally they're quite well
Dialogue: 0,0:26:46.97,0:26:52.50,Default,,0000,0000,0000,,synchronised and they both read the other\Nguy's right. Sorry, big call. They both
Dialogue: 0,0:26:52.50,0:26:57.51,Default,,0000,0000,0000,,read the other guy's right. And quite\Noften one thread comes completely before
Dialogue: 0,0:26:57.51,0:27:09.77,Default,,0000,0000,0000,,the other. But sometimes, sometimes they\Nboth see 0. Huh. Rats. Well, that's
Dialogue: 0,0:27:09.77,0:27:18.84,Default,,0000,0000,0000,,interesting. Let me show you another\Nprogram. So now, thread 0 writes some
Dialogue: 0,0:27:18.84,0:27:23.44,Default,,0000,0000,0000,,stuff. Maybe it writes a big bunch of\Ndata, maybe multi-word data. And then it
Dialogue: 0,0:27:23.44,0:27:28.25,Default,,0000,0000,0000,,writes, let's say that's a flag announcing\Nto some another thread that that data is
Dialogue: 0,0:27:28.25,0:27:33.25,Default,,0000,0000,0000,,ready to go now. And the other thread\Nbusy-waits reading that value until it
Dialogue: 0,0:27:33.25,0:27:38.71,Default,,0000,0000,0000,,gets 1, until it sees the flag. And then\Nit reads the data. So you might want, as a
Dialogue: 0,0:27:38.71,0:27:43.61,Default,,0000,0000,0000,,programmer, you might want a guarantee\Nthat this read will always see the data
Dialogue: 0,0:27:43.61,0:27:48.76,Default,,0000,0000,0000,,that you have initialised. Hey? That would\Nbe like a message-passing kind of an
Dialogue: 0,0:27:48.76,0:27:56.23,Default,,0000,0000,0000,,idiom. So what happens if you run that?\NWell, on the x86 processors that we've
Dialogue: 0,0:27:56.23,0:28:03.93,Default,,0000,0000,0000,,tested, you always see that value. Good.\NThis is a descent coding idiom on x86. All
Dialogue: 0,0:28:03.93,0:28:12.23,Default,,0000,0000,0000,,right. On Arma IBM Power processors,\Nhowever, you see sometimes you just ignore
Dialogue: 0,0:28:12.23,0:28:16.85,Default,,0000,0000,0000,,the value written and you see the initial\Nstate. So this is not a good
Dialogue: 0,0:28:16.85,0:28:25.54,Default,,0000,0000,0000,,message-passing idiom, right? So what's\Ngoing on? Well, these behaviours, it might
Dialogue: 0,0:28:25.54,0:28:31.26,Default,,0000,0000,0000,,be surprising, eh? And when you see\Nsurprising behaviour in hardware, you have
Dialogue: 0,0:28:31.26,0:28:36.10,Default,,0000,0000,0000,,two choices. Either it's a bug in the\Nhardware, and we have found a number of
Dialogue: 0,0:28:36.10,0:28:45.26,Default,,0000,0000,0000,,bugs in hardware. It's always - it's very\Nrewarding. Or it's a bug in your
Dialogue: 0,0:28:45.26,0:28:51.35,Default,,0000,0000,0000,,expectation. Or it's a bug in your test\Nharness. Right? So what you do is you walk
Dialogue: 0,0:28:51.35,0:28:58.05,Default,,0000,0000,0000,,along and you walk up to your friendly\Nprocessor architect in IBM or ARM or x86
Dialogue: 0,0:28:58.05,0:29:04.77,Default,,0000,0000,0000,,land, and we have worked with all of these\Npeople. And you ask them, "Is this a bug?"
Dialogue: 0,0:29:04.77,0:29:12.36,Default,,0000,0000,0000,,And a processor architect is a person who\Nis - has the authority to decide whether
Dialogue: 0,0:29:12.36,0:29:16.24,Default,,0000,0000,0000,,some behaviour is intended or is a bug.
Dialogue: 0,0:29:16.24,0:29:17.75,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:29:17.75,0:29:24.67,Default,,0000,0000,0000,,That's what they do, essentially. And for\Nthese, they say, "Oh, we meant it to be
Dialogue: 0,0:29:24.67,0:29:29.24,Default,,0000,0000,0000,,like that". Right? No question. "We meant\Nit to be like that. That's perfectly
Dialogue: 0,0:29:29.24,0:29:36.56,Default,,0000,0000,0000,,proper. We have, because you and everybody\Nelse wanted their computers to go fast, we
Dialogue: 0,0:29:36.56,0:29:41.69,Default,,0000,0000,0000,,as processor designers have introduced all\Nmanner of sophisticated optimizations,
Dialogue: 0,0:29:41.69,0:29:45.20,Default,,0000,0000,0000,,which if you were running sequential code,\Nyou would never notice, but if you start
Dialogue: 0,0:29:45.20,0:29:49.29,Default,,0000,0000,0000,,running fancy concurrent code like this,\Nfancy concurrent code that isn't just
Dialogue: 0,0:29:49.29,0:29:56.05,Default,,0000,0000,0000,,trivially locked, you can notice", so this\Nis intentional behaviour. And if you want
Dialogue: 0,0:29:56.05,0:30:00.13,Default,,0000,0000,0000,,to write that code, like a mutual\Nexclusion algorithm or a message-passing
Dialogue: 0,0:30:00.13,0:30:06.46,Default,,0000,0000,0000,,algorithm or something, then you need to\Ninsert special instructions, memory
Dialogue: 0,0:30:06.46,0:30:11.18,Default,,0000,0000,0000,,barrier instructions. And so you go away\Nand you say, "What do they do?" And you
Dialogue: 0,0:30:11.18,0:30:18.95,Default,,0000,0000,0000,,look up in the vendor documentation. And\Nyou get stuff like this. I'll read it out:
Dialogue: 0,0:30:18.95,0:30:22.19,Default,,0000,0000,0000,,(Reads quickly) "For any applicable pair\NAB, the memory barrier ensures that a will
Dialogue: 0,0:30:22.19,0:30:24.74,Default,,0000,0000,0000,,be performed with respect to any processor\Nor mechanism, to the extent required by
Dialogue: 0,0:30:24.74,0:30:27.59,Default,,0000,0000,0000,,the associated memory coherence required\Nat beauties, before b is performed with
Dialogue: 0,0:30:27.59,0:30:30.36,Default,,0000,0000,0000,,respect to that prior or mechanism. A\Nincludes all applicable storage accesses
Dialogue: 0,0:30:30.36,0:30:33.09,Default,,0000,0000,0000,,by any such processor or mechanism that\Nhave been performed with respect to P1
Dialogue: 0,0:30:33.09,0:30:36.21,Default,,0000,0000,0000,,before the memory barrier is created. B\Nincludes all applicable storage accesses
Dialogue: 0,0:30:36.21,0:30:38.67,Default,,0000,0000,0000,,by any such processor or mechanism that\Nare performed after a Load instruction
Dialogue: 0,0:30:38.67,0:30:41.29,Default,,0000,0000,0000,,executed by that processor or mechanism\Nhas returned the value stored by a store
Dialogue: 0,0:30:41.29,0:30:42.70,Default,,0000,0000,0000,,that is in B."
Dialogue: 0,0:30:42.70,0:30:49.85,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:30:49.85,0:30:58.63,Default,,0000,0000,0000,,Hands up if you understand what that\Nmeans? Hands up if you think that if you
Dialogue: 0,0:30:58.63,0:31:02.14,Default,,0000,0000,0000,,thought about it and read the rest of the\Nbook, you would understand or you could
Dialogue: 0,0:31:02.14,0:31:09.73,Default,,0000,0000,0000,,understand what that means? Hands up the\Npeople who think that we're doomed forever?
Dialogue: 0,0:31:09.73,0:31:12.92,Default,,0000,0000,0000,,{\i1}laughter{\i0}
Dialogue: 0,0:31:12.92,0:31:16.98,Default,,0000,0000,0000,,So I'm sorry to the first few groups,\Nbut the last ones are right.
Dialogue: 0,0:31:16.98,0:31:22.30,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:31:22.30,0:31:28.85,Default,,0000,0000,0000,,This looks like it's really intricate and\Nreally carefully thought out stuff. And we
Dialogue: 0,0:31:28.85,0:31:32.22,Default,,0000,0000,0000,,thought that for a while and we spent\Nliterally years trying to make precise
Dialogue: 0,0:31:32.22,0:31:37.16,Default,,0000,0000,0000,,mathematical models that give precise\Nmeaning to these words, but actually it
Dialogue: 0,0:31:37.16,0:31:45.46,Default,,0000,0000,0000,,can't be done. So what do you have to do\Nin that circumstance? You have to go away
Dialogue: 0,0:31:45.46,0:31:52.12,Default,,0000,0000,0000,,and you have to invent some kind of a\Nmodel. And there's a - this is a really
Dialogue: 0,0:31:52.12,0:31:56.19,Default,,0000,0000,0000,,fundamental problem, that we - on the one\Nhand, we develop our software by this
Dialogue: 0,0:31:56.19,0:32:01.96,Default,,0000,0000,0000,,trial and error process, but on the other\Nhand are points like this. We have these
Dialogue: 0,0:32:01.96,0:32:06.47,Default,,0000,0000,0000,,loose specifications, supposedly, that\Nhave to cover all manner of behaviour of
Dialogue: 0,0:32:06.47,0:32:10.73,Default,,0000,0000,0000,,many generations of processors that might\Nall behave the same way, written just in
Dialogue: 0,0:32:10.73,0:32:16.77,Default,,0000,0000,0000,,text. And we tell people they should write\N"to the spec", but the only way they have
Dialogue: 0,0:32:16.77,0:32:22.45,Default,,0000,0000,0000,,of developing their code is to run it and\Nrun particular executions on the
Dialogue: 0,0:32:22.45,0:32:26.96,Default,,0000,0000,0000,,particular hardware implementations that\Nthey have, whose relationship to the spec
Dialogue: 0,0:32:26.96,0:32:34.74,Default,,0000,0000,0000,,is very elusive. We can't use those thick\Nbooks that you get or those quite weighty
Dialogue: 0,0:32:34.74,0:32:39.26,Default,,0000,0000,0000,,PDFs that you get these days from the\Nprocessor vendors to test programs. You
Dialogue: 0,0:32:39.26,0:32:43.97,Default,,0000,0000,0000,,can't feed a program into that thick book\Nand get output out. And you can't test
Dialogue: 0,0:32:43.97,0:32:47.43,Default,,0000,0000,0000,,processor implementations and you can't\Nprove anything and you can't even
Dialogue: 0,0:32:47.43,0:32:53.43,Default,,0000,0000,0000,,communicate between human beings, right?\NSo these things, really, they don't exist.
Dialogue: 0,0:32:53.43,0:32:58.50,Default,,0000,0000,0000,,So what can we do? Well, the best we can\Ndo at this point in time is a bit of
Dialogue: 0,0:32:58.50,0:33:04.95,Default,,0000,0000,0000,,empirical science, right? So we can invent\Nsome model off the top of our heads,
Dialogue: 0,0:33:04.95,0:33:09.65,Default,,0000,0000,0000,,trying to describe just the\Nprogrammer-visible behaviour, not the
Dialogue: 0,0:33:09.65,0:33:15.53,Default,,0000,0000,0000,,internal structure. And we can make a\Ntool. Because that's not prose now. Now we
Dialogue: 0,0:33:15.53,0:33:18.95,Default,,0000,0000,0000,,can - now it's stuff. It's real\Nmathematics and we can turn that into code
Dialogue: 0,0:33:18.95,0:33:23.20,Default,,0000,0000,0000,,and execute it. We can make tools that\Ntake programs and execute it and - small
Dialogue: 0,0:33:23.20,0:33:28.28,Default,,0000,0000,0000,,programs - tell us the set of all\Nbehaviours allowed by that model. And then
Dialogue: 0,0:33:28.28,0:33:33.76,Default,,0000,0000,0000,,we can compare those sets of behaviours\Nagainst the experimental observations. And
Dialogue: 0,0:33:33.76,0:33:38.36,Default,,0000,0000,0000,,you might have to fix the model and you\Nmight find hard bugs. And then the model
Dialogue: 0,0:33:38.36,0:33:42.87,Default,,0000,0000,0000,,also has to make sense to the architect so\Nyou can discuss with the architects what
Dialogue: 0,0:33:42.87,0:33:47.10,Default,,0000,0000,0000,,they intend and what their institution is,\Nand then you can also prove some other
Dialogue: 0,0:33:47.10,0:33:50.98,Default,,0000,0000,0000,,facts about it to give a bit more\Nassurance and then because you probably
Dialogue: 0,0:33:50.98,0:33:57.25,Default,,0000,0000,0000,,got this wrong the first couple of times,\Nyou can go back. And this results or has
Dialogue: 0,0:33:57.25,0:34:04.51,Default,,0000,0000,0000,,resulted in models which are not\Nguaranteed to be correct, but they are
Dialogue: 0,0:34:04.51,0:34:08.64,Default,,0000,0000,0000,,effectively the de facto standard for\Nunderstanding the concurrency behaviour of
Dialogue: 0,0:34:08.64,0:34:14.30,Default,,0000,0000,0000,,these things, you know? And various people\Nuse them. And just to give you a tiny
Dialogue: 0,0:34:14.30,0:34:18.57,Default,,0000,0000,0000,,snippet - I'll have to speed up a bit - a\Ntiny snippet of what the model looks like,
Dialogue: 0,0:34:18.57,0:34:22.97,Default,,0000,0000,0000,,it's basically just an abstract machine.\NIt's got some stuff for the threads that
Dialogue: 0,0:34:22.97,0:34:26.95,Default,,0000,0000,0000,,handles the programmer-visible speculative\Nexecution, and some stuff for a storage
Dialogue: 0,0:34:26.95,0:34:32.74,Default,,0000,0000,0000,,subsystem that handles the fact that in\Nthese architectures, memory rights can be
Dialogue: 0,0:34:32.74,0:34:38.27,Default,,0000,0000,0000,,propagated to different threads at\Ndifferent times, right? And there's a -
Dialogue: 0,0:34:38.27,0:34:42.54,Default,,0000,0000,0000,,that model has a state which is just a\Ncollection of some sets and lists and
Dialogue: 0,0:34:42.54,0:34:47.23,Default,,0000,0000,0000,,partial orders and a few other things\Nwhich I won't talk about. And it has some
Dialogue: 0,0:34:47.23,0:34:51.03,Default,,0000,0000,0000,,transitions, right? In any state, there\Nmight be several possible transitions.
Dialogue: 0,0:34:51.03,0:34:54.70,Default,,0000,0000,0000,,This is just a sample. I'm not going to\Nexplain all of this. But when you want to
Dialogue: 0,0:34:54.70,0:34:58.57,Default,,0000,0000,0000,,propagate a write to another thread, there\Nhave to be some preconditions that you have to
Dialogue: 0,0:34:58.57,0:35:07.14,Default,,0000,0000,0000,,satisfy. And than there is an action. It's not\Namazingly complicated, really. So this is text,
Dialogue: 0,0:35:07.14,0:35:13.32,Default,,0000,0000,0000,,but it's very precisely written text and it has\Nthe great advantage that you can go through
Dialogue: 0,0:35:13.32,0:35:16.57,Default,,0000,0000,0000,,these bullet points with your friendly\Narchitect and say, "Is this what you
Dialogue: 0,0:35:16.57,0:35:22.44,Default,,0000,0000,0000,,mean?" And they can think about it and say\Nyes or no. But for the actual definition,
Dialogue: 0,0:35:22.44,0:35:27.31,Default,,0000,0000,0000,,that's in mathematics but it's mathematics\Nthat's quite close to code. I mean, it's
Dialogue: 0,0:35:27.31,0:35:32.38,Default,,0000,0000,0000,,terribly close to pure, functional code\Nwith outside effects. And just to give you
Dialogue: 0,0:35:32.38,0:35:37.23,Default,,0000,0000,0000,,an idea, this is some of it and those are\Nthree of those conditions in the real,
Dialogue: 0,0:35:37.23,0:35:42.66,Default,,0000,0000,0000,,honest, true version. Then we can take\Nthis mathematics and because it's in a
Dialogue: 0,0:35:42.66,0:35:49.27,Default,,0000,0000,0000,,particular style, we can compile this into\Nactually OCaml and then OCaml byte code
Dialogue: 0,0:35:49.27,0:35:55.77,Default,,0000,0000,0000,,and then we can run it for batch jobs. But\Nthen you can compile that OCaml byte code
Dialogue: 0,0:35:55.77,0:36:02.58,Default,,0000,0000,0000,,to JavaScript and glue on an user interface\Nand stick it into a web browser and then you
Dialogue: 0,0:36:02.58,0:36:07.76,Default,,0000,0000,0000,,have a web interface that lets people\Nexplore this model. And that's also a
Dialogue: 0,0:36:07.76,0:36:16.19,Default,,0000,0000,0000,,necessary part of validating that it makes\Nsense. Okay. This is not rocket science.
Dialogue: 0,0:36:16.19,0:36:21.71,Default,,0000,0000,0000,,You've missed the talk for rocket science,\NI'm sorry. All we're doing here is
Dialogue: 0,0:36:21.71,0:36:28.63,Default,,0000,0000,0000,,specifying the intended behaviour of a\Nsystem. Okay? That's - it's not very
Dialogue: 0,0:36:28.63,0:36:32.49,Default,,0000,0000,0000,,technical but it's unusual. And we happen\Nto be doing it in this mathematical
Dialogue: 0,0:36:32.49,0:36:37.05,Default,,0000,0000,0000,,language, but you could use in fact almost\Nany language so long as you understand
Dialogue: 0,0:36:37.05,0:36:40.17,Default,,0000,0000,0000,,what you're doing. What you have to\Nunderstand is that you're writing
Dialogue: 0,0:36:40.17,0:36:45.23,Default,,0000,0000,0000,,something which is not an implementation.\NIt is something which, given some observed
Dialogue: 0,0:36:45.23,0:36:49.81,Default,,0000,0000,0000,,behaviour, some arbitrary observed\Nbehaviour, will be able to decide if it's
Dialogue: 0,0:36:49.81,0:36:54.58,Default,,0000,0000,0000,,allowed, if you want it to be allowed or\Nnot, right? It has to be executed as a
Dialogue: 0,0:36:54.58,0:37:02.06,Default,,0000,0000,0000,,test oracle. The key question for getting\Nthis to work is to understand how much
Dialogue: 0,0:37:02.06,0:37:05.73,Default,,0000,0000,0000,,non-determinism or loose specification\Nthere is in the system that you're working
Dialogue: 0,0:37:05.73,0:37:08.89,Default,,0000,0000,0000,,with, right? So if everything is\Ncompletely deterministic, you can write a
Dialogue: 0,0:37:08.89,0:37:13.84,Default,,0000,0000,0000,,reference implementation in the cleanest\Nlanguage of your choice and just compare
Dialogue: 0,0:37:13.84,0:37:19.27,Default,,0000,0000,0000,,the output of that and the output of the\Nreal thing, right? But if there's more
Dialogue: 0,0:37:19.27,0:37:24.00,Default,,0000,0000,0000,,non-determinism, then you can't do that.\NI'm going to have to abbreviate this a
Dialogue: 0,0:37:24.00,0:37:31.37,Default,,0000,0000,0000,,little tiny bit. So for the TCP network\Nprotocols, there is more non-determinism.
Dialogue: 0,0:37:31.37,0:37:35.22,Default,,0000,0000,0000,,You know what the TCP is, yes? A protocol\Nthat gives you sort of reliable
Dialogue: 0,0:37:35.22,0:37:41.72,Default,,0000,0000,0000,,connections, assuming that the world is\Nmade of good people, right? You look at
Dialogue: 0,0:37:41.72,0:37:47.64,Default,,0000,0000,0000,,the standards for TCP, and they're the\Nsame kind of wibbly text from the 1980s
Dialogue: 0,0:37:47.64,0:37:52.40,Default,,0000,0000,0000,,and you look at the implementations and\Nthey are a ghastly mess. And you try and
Dialogue: 0,0:37:52.40,0:37:55.69,Default,,0000,0000,0000,,understand the relationship between the\Ntwo of them and you can't because the
Dialogue: 0,0:37:55.69,0:38:01.74,Default,,0000,0000,0000,,standard, again, is not the definition. It\Ndoesn't define in all circumstances what
Dialogue: 0,0:38:01.74,0:38:07.01,Default,,0000,0000,0000,,behaviour is allowed and what isn't. So\Nagain, we had to make up a specification
Dialogue: 0,0:38:07.01,0:38:14.31,Default,,0000,0000,0000,,in the first instance just of this host, a\Nsingle endpoint, and observing its
Dialogue: 0,0:38:14.31,0:38:18.51,Default,,0000,0000,0000,,sockets, API, calls and returns and its\Nbehaviour on the wire, right? And when
Dialogue: 0,0:38:18.51,0:38:21.97,Default,,0000,0000,0000,,you've decided - and a few internal debug\Nevents. And when you've decided what to
Dialogue: 0,0:38:21.97,0:38:26.62,Default,,0000,0000,0000,,observe, then observation is just a trace,\Nit's just a list of those events. And you
Dialogue: 0,0:38:26.62,0:38:34.75,Default,,0000,0000,0000,,have to be able to ask your spec "Is that\Nlist admissible or not"? But there's a lot
Dialogue: 0,0:38:34.75,0:38:38.82,Default,,0000,0000,0000,,of non-determinism. Variation between the\Nimplementations, variations within the
Dialogue: 0,0:38:38.82,0:38:45.65,Default,,0000,0000,0000,,implementations. And that's internal. It's\Nnot announced in the API or on the wire
Dialogue: 0,0:38:45.65,0:38:50.98,Default,,0000,0000,0000,,maybe until much later when the\Nimplementation picks a new window size or
Dialogue: 0,0:38:50.98,0:38:56.89,Default,,0000,0000,0000,,something. You can't tell until quite a\Nlot later in the trace what it's picked.
Dialogue: 0,0:38:56.89,0:39:02.74,Default,,0000,0000,0000,,And that makes the job of checking whether\Na trace is admissible by the spec much
Dialogue: 0,0:39:02.74,0:39:08.56,Default,,0000,0000,0000,,harder than it has to be. Right? And if\Nyou had designed the TCP protocol and
Dialogue: 0,0:39:08.56,0:39:14.47,Default,,0000,0000,0000,,those implementations for to be testable\Nin this very discriminating way, back in
Dialogue: 0,0:39:14.47,0:39:20.47,Default,,0000,0000,0000,,the 1980s when you were designing TCP\Nprotocol, it would be much easier. And for
Dialogue: 0,0:39:20.47,0:39:25.65,Default,,0000,0000,0000,,new protocols, one should make sure that\Nyou're doing this in this particular way.
Dialogue: 0,0:39:25.65,0:39:30.93,Default,,0000,0000,0000,,I don't think I want to talk about that\Nslide. That's just one of the rules of
Dialogue: 0,0:39:30.93,0:39:35.48,Default,,0000,0000,0000,,that specification. But the key fact about\Nthat spec is the - well, we handled the
Dialogue: 0,0:39:35.48,0:39:40.21,Default,,0000,0000,0000,,real protocols for arbitrary inputs. But\Nit's structured not just for this
Dialogue: 0,0:39:40.21,0:39:46.24,Default,,0000,0000,0000,,executability as a test oracle, but it's\Nstructured for clarity, not performance,
Dialogue: 0,0:39:46.24,0:39:49.75,Default,,0000,0000,0000,,which is scarcely ever what anyone ever\Ndoes, right? So it's a whole new kind of
Dialogue: 0,0:39:49.75,0:39:54.48,Default,,0000,0000,0000,,thing. And the testing is very\Ndiscriminating. So we found all manner of
Dialogue: 0,0:39:54.48,0:40:03.84,Default,,0000,0000,0000,,amusing and bizarre bugs which I think I\Ndon't have time to talk about. Okay. So
Dialogue: 0,0:40:03.84,0:40:12.61,Default,,0000,0000,0000,,I've described three kinds of things that\Nwe might do. The first thing - for
Dialogue: 0,0:40:12.61,0:40:18.80,Default,,0000,0000,0000,,goodness sake - I mean, it's just a\Nno-brainer. Just do it already. Everybody.
Dialogue: 0,0:40:18.80,0:40:29.67,Default,,0000,0000,0000,,All of you. All of you. Right? This middle\Nzone is a very interesting zone as far as
Dialogue: 0,0:40:29.67,0:40:33.92,Default,,0000,0000,0000,,I'm concerned, right? It's - out of what -\Na place where we could get a very good
Dialogue: 0,0:40:33.92,0:40:39.22,Default,,0000,0000,0000,,benefit for not that much effort, right?\NWe can do it, if necessary, post hoc. We
Dialogue: 0,0:40:39.22,0:40:44.49,Default,,0000,0000,0000,,can also do it and even better, at design\Ntime. We have to do this in a way that
Dialogue: 0,0:40:44.49,0:40:48.24,Default,,0000,0000,0000,,makes our executions testable as test\Noracles, and another thing that that
Dialogue: 0,0:40:48.24,0:40:52.12,Default,,0000,0000,0000,,enables is completely random testing. When\Nyou've got a test oracle, you can just
Dialogue: 0,0:40:52.12,0:40:58.21,Default,,0000,0000,0000,,feed in random goop. This is fuzzing, but\Nbetter fuzzing - feed in random goop and
Dialogue: 0,0:40:58.21,0:41:02.86,Default,,0000,0000,0000,,check at every point whether what the\Nbehaviour that you're getting is allowable
Dialogue: 0,0:41:02.86,0:41:09.27,Default,,0000,0000,0000,,or not. And then they're written for\Nclarity, not for performance, and that
Dialogue: 0,0:41:09.27,0:41:13.62,Default,,0000,0000,0000,,means you can see what you're doing,\Nright? You can see the complexity. If you
Dialogue: 0,0:41:13.62,0:41:17.14,Default,,0000,0000,0000,,go ahead and you add some feature to your\Nprotocol or your programming language or
Dialogue: 0,0:41:17.14,0:41:22.42,Default,,0000,0000,0000,,whatever and you're working just with text\Nspecifications, then you can't see the
Dialogue: 0,0:41:22.42,0:41:24.76,Default,,0000,0000,0000,,interactions. You just chuck in a couple\Nof paragraphs and you think for a few
Dialogue: 0,0:41:24.76,0:41:30.21,Default,,0000,0000,0000,,minutes, right? And if you're lucky, you\Nmake an implementation. But if you're
Dialogue: 0,0:41:30.21,0:41:35.31,Default,,0000,0000,0000,,writing a spec that has to cover all the\Ncases like this, the act of doing that
Dialogue: 0,0:41:35.31,0:41:41.15,Default,,0000,0000,0000,,encourages you to think or helps you think\Nabout the excess complexity. And you might
Dialogue: 0,0:41:41.15,0:41:46.69,Default,,0000,0000,0000,,think that's too complex, I'm being silly,\NI'll make it simpler. And it has to be
Dialogue: 0,0:41:46.69,0:41:51.63,Default,,0000,0000,0000,,usable for proof. So this, I think also is\Npretty much a no-brainer. And it doesn't
Dialogue: 0,0:41:51.63,0:41:56.65,Default,,0000,0000,0000,,require great technical, you know,\Nmathematical skill either, right? Lots of
Dialogue: 0,0:41:56.65,0:42:01.76,Default,,0000,0000,0000,,people can do this. And then there's\Noption 3, best option, full-on formal
Dialogue: 0,0:42:01.76,0:42:07.93,Default,,0000,0000,0000,,verification of the key components. And\Nthat is now also in reach. You can imagine
Dialogue: 0,0:42:07.93,0:42:16.31,Default,,0000,0000,0000,,secure systems made using actual verified\Ncompilers and verified hypervisors with
Dialogue: 0,0:42:16.31,0:42:22.54,Default,,0000,0000,0000,,verified TLS stacks and you can imagine\Nmaking things out of those or making those
Dialogue: 0,0:42:22.54,0:42:27.87,Default,,0000,0000,0000,,and then making things out of those. And\Nmaybe one should be thinking about that.
Dialogue: 0,0:42:27.87,0:42:34.07,Default,,0000,0000,0000,,So, maybe not appropriate for everything.\NIf you were writing Word, you would not
Dialogue: 0,0:42:34.07,0:42:38.60,Default,,0000,0000,0000,,wish to do these things. Probably, you're\Nnot. But for this key infrastructure that
Dialogue: 0,0:42:38.60,0:42:46.42,Default,,0000,0000,0000,,we really depend on, we trust even though\Nit's not trustworthy, we have to do this.
Dialogue: 0,0:42:46.42,0:42:52.45,Default,,0000,0000,0000,,Is this a new dawn? I wonder if there's\Nanyone standing next to a light switch
Dialogue: 0,0:42:52.45,0:42:58.92,Default,,0000,0000,0000,,that can dim them for me. I didn't ask\Nthem beforehand, so... If you think back
Dialogue: 0,0:42:58.92,0:43:05.54,Default,,0000,0000,0000,,the last 70-odd years, we started building\Ncomputers in around 1940. It's been pretty
Dialogue: 0,0:43:05.54,0:43:12.76,Default,,0000,0000,0000,,dark from the point of view of rigorous,\Nsolid, reliable engineering, stuff that is
Dialogue: 0,0:43:12.76,0:43:21.76,Default,,0000,0000,0000,,actually trustworthy. Pretty dark, I would\Nsay. Maybe, just maybe there's a tiny
Dialogue: 0,0:43:21.76,0:43:26.34,Default,,0000,0000,0000,,smidgen of light coming through the doors.\NAnd we start to have a little bit of a
Dialogue: 0,0:43:26.34,0:43:31.11,Default,,0000,0000,0000,,clue and we start to get reusable models\Nof processor architectures and programming
Dialogue: 0,0:43:31.11,0:43:35.54,Default,,0000,0000,0000,,languages and network protocols and what\Nhave you. It's just the beginnings of the
Dialogue: 0,0:43:35.54,0:43:39.79,Default,,0000,0000,0000,,analogue of that thermodynamics and\Nmaterials science and quality control
Dialogue: 0,0:43:39.79,0:43:47.82,Default,,0000,0000,0000,,management and what have you that we have\Nfrom mechanical engineering. And we've got
Dialogue: 0,0:43:47.82,0:43:57.20,Default,,0000,0000,0000,,no choice. If we don't, the next 75 years\Nis going to be a lot worse. You can just
Dialogue: 0,0:43:57.20,0:44:02.40,Default,,0000,0000,0000,,imagine, right? So I went to this - as I'm\Nsure many of you do - this great talk on
Dialogue: 0,0:44:02.40,0:44:08.37,Default,,0000,0000,0000,,some Apple boot loader exploit yesterday\Nwhich was relying on some feature that had
Dialogue: 0,0:44:08.37,0:44:14.90,Default,,0000,0000,0000,,been introduced in the early '80s and was\Nstill present. And you can imagine in 100
Dialogue: 0,0:44:14.90,0:44:22.80,Default,,0000,0000,0000,,years from now, you can imagine as long as\Nhuman civilisation endures, the x86
Dialogue: 0,0:44:22.80,0:44:28.87,Default,,0000,0000,0000,,architecture and the socket API and all of\Nthis stuff, it will be embedded in some
Dialogue: 0,0:44:28.87,0:44:34.10,Default,,0000,0000,0000,,monumental ghastly stack of\Nvirtualisation layers forever.
Dialogue: 0,0:44:34.10,0:44:45.76,Default,,0000,0000,0000,,{\i1}laughter{\i0}{\i1}applause{\i0}
Dialogue: 0,0:44:45.76,0:44:50.72,Default,,0000,0000,0000,,So I'd like to thank especially all of my\Ncolleagues that have been working with me
Dialogue: 0,0:44:50.72,0:44:56.55,Default,,0000,0000,0000,,or not with me in these directions. I'd\Nlike to thank our generous funders who
Dialogue: 0,0:44:56.55,0:45:01.39,Default,,0000,0000,0000,,support this stuff. I'd like to thank you\Nfor your attention and I exhort you,
Dialogue: 0,0:45:01.39,0:45:04.85,Default,,0000,0000,0000,,sort it out.
Dialogue: 0,0:45:04.85,0:45:20.80,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:45:20.80,0:45:25.30,Default,,0000,0000,0000,,Herald: Thank you very much, Peter, for\Nthose interesting insights to our
Dialogue: 0,0:45:25.30,0:45:31.27,Default,,0000,0000,0000,,programming. We have now time for a Q & A,\Nso those people who have to leave the
Dialogue: 0,0:45:31.27,0:45:39.97,Default,,0000,0000,0000,,room, please do so quietly and as fast as\Npossible, so we can go on and hear what
Dialogue: 0,0:45:39.97,0:45:51.27,Default,,0000,0000,0000,,the questions are. So we\Nstart with microphone 4, please.
Dialogue: 0,0:45:51.27,0:45:58.79,Default,,0000,0000,0000,,Mic 4: Hello. Thanks for the talk and my\Nquestion is if you got an oracle of the
Dialogue: 0,0:45:58.79,0:46:04.27,Default,,0000,0000,0000,,software behaviour which can translate\Nevery possible input to a correct output,
Dialogue: 0,0:46:04.27,0:46:08.41,Default,,0000,0000,0000,,how can this be less complex and\Nerror-prone than the reference
Dialogue: 0,0:46:08.41,0:46:10.51,Default,,0000,0000,0000,,implementation?
Dialogue: 0,0:46:10.51,0:46:15.62,Default,,0000,0000,0000,,Peter: Good question. So the first point\Nis that this oracle doesn't have to
Dialogue: 0,0:46:15.62,0:46:22.01,Default,,0000,0000,0000,,produce the outputs. It only has to check\Nthat the inputs and the outputs match up.
Dialogue: 0,0:46:22.01,0:46:26.56,Default,,0000,0000,0000,,And then the second point is that in\Ngeneral it might have to have much of the
Dialogue: 0,0:46:26.56,0:46:33.22,Default,,0000,0000,0000,,same complexity, but by writing it to be\Nclear as opposed to to be fast, you may
Dialogue: 0,0:46:33.22,0:46:37.73,Default,,0000,0000,0000,,adopt a completely different structure,\Nright? So the structure of our TCP spec is
Dialogue: 0,0:46:37.73,0:46:43.54,Default,,0000,0000,0000,,organised by the behaviour that you see\Nfor particular transitions. The structure
Dialogue: 0,0:46:43.54,0:46:49.16,Default,,0000,0000,0000,,of a real implementation has fast-path\Ncode and lots of complicated intertwined
Dialogue: 0,0:46:49.16,0:46:55.31,Default,,0000,0000,0000,,branching and all manner of excess\Ncomplexity, of implementation complexity,
Dialogue: 0,0:46:55.31,0:46:56.88,Default,,0000,0000,0000,,if you will.
Dialogue: 0,0:46:56.88,0:47:01.45,Default,,0000,0000,0000,,Mic 4: Thanks.\NHerald: So microphone 3, please?
Dialogue: 0,0:47:01.45,0:47:06.71,Default,,0000,0000,0000,,Mic 3: I wanted to ask you what you\Nthought about programming by manipulating
Dialogue: 0,0:47:06.71,0:47:13.86,Default,,0000,0000,0000,,the abstract syntax tree directly so as to\Nnot allow incompilable programs because of
Dialogue: 0,0:47:13.86,0:47:18.41,Default,,0000,0000,0000,,some, like, you're missing a semicolon or\Nsomething like that. What's your thoughts
Dialogue: 0,0:47:18.41,0:47:20.22,Default,,0000,0000,0000,,on that?
Dialogue: 0,0:47:20.22,0:47:23.70,Default,,0000,0000,0000,,Peter: So that's - in the grand scheme of\Nthings, I think that's not a very big
Dialogue: 0,0:47:23.70,0:47:28.89,Default,,0000,0000,0000,,deal, right? So there's - people have\Nworked on structured editors for lordy
Dialogue: 0,0:47:28.89,0:47:33.31,Default,,0000,0000,0000,,knows how many years. It's not a big deal\Nbecause it's very easy for a compiler to
Dialogue: 0,0:47:33.31,0:47:38.57,Default,,0000,0000,0000,,detect that kind of thing. And even more,\Nit's very easy for a compiler of a
Dialogue: 0,0:47:38.57,0:47:43.14,Default,,0000,0000,0000,,sensibly designed language to detect type\Nerrors, even for a very sophisticated type
Dialogue: 0,0:47:43.14,0:47:49.59,Default,,0000,0000,0000,,system. So I don't think that - that's not\N- I mean, some people might find it
Dialogue: 0,0:47:49.59,0:47:52.93,Default,,0000,0000,0000,,helpful, but I don't think it's getting to\Nthe heart of the matter.
Dialogue: 0,0:47:52.93,0:47:54.25,Default,,0000,0000,0000,,Mic 3: Thanks.
Dialogue: 0,0:47:54.25,0:47:59.85,Default,,0000,0000,0000,,Herald: So we've got some questions\Nfrom our signal angels from the IRC.
Dialogue: 0,0:47:59.85,0:48:06.15,Default,,0000,0000,0000,,Signal angel: Yes. There's one question.\NIt's about the repository for Isabelle and
Dialogue: 0,0:48:06.15,0:48:11.30,Default,,0000,0000,0000,,HOL proofs. It should be on source forge,\Nand you said there are no open source
Dialogue: 0,0:48:11.30,0:48:15.48,Default,,0000,0000,0000,,repositories. What about them?
Dialogue: 0,0:48:15.48,0:48:20.59,Default,,0000,0000,0000,,Peter: I'm not quite sure what the\Nquestion is, really. So there's a
Dialogue: 0,0:48:20.59,0:48:28.23,Default,,0000,0000,0000,,repository of Isabelle formal proofs which\Nis the archival form of proofs, it's
Dialogue: 0,0:48:28.23,0:48:34.79,Default,,0000,0000,0000,,called. I didn't really mean to say there\Nare no open source repositories and in
Dialogue: 0,0:48:34.79,0:48:38.50,Default,,0000,0000,0000,,fact I don't know under what conditions\Nmost of those proofs are licensed. They
Dialogue: 0,0:48:38.50,0:48:43.21,Default,,0000,0000,0000,,probably are open. But there isn't an open\Nsource community building these things,
Dialogue: 0,0:48:43.21,0:48:47.71,Default,,0000,0000,0000,,right? It's still pretty\Nmuch an academic pursuit.
Dialogue: 0,0:48:47.71,0:48:50.33,Default,,0000,0000,0000,,Herald: Microphone 2, please.
Dialogue: 0,0:48:50.33,0:48:55.53,Default,,0000,0000,0000,,Mic 2: Hello. Thanks again for your talk.\NI just want to add something that you
Dialogue: 0,0:48:55.53,0:49:01.97,Default,,0000,0000,0000,,didn't address, and that's that we\Nactually need more good studies in
Dialogue: 0,0:49:01.97,0:49:07.97,Default,,0000,0000,0000,,software engineering. We often hear a lot\Nof experts and also very well-known
Dialogue: 0,0:49:07.97,0:49:11.74,Default,,0000,0000,0000,,computer scientists say things like,\N"Well, we just need to do functional
Dialogue: 0,0:49:11.74,0:49:17.84,Default,,0000,0000,0000,,programming and OOP is bad and stuff like\Nthat", which I think there's a lot of
Dialogue: 0,0:49:17.84,0:49:24.11,Default,,0000,0000,0000,,truth to it, but we actually need studies\Nwhere we test these kinds of claims that
Dialogue: 0,0:49:24.11,0:49:29.53,Default,,0000,0000,0000,,we make, because when you look at other\Nfields which it also did compare to, like,
Dialogue: 0,0:49:29.53,0:49:34.25,Default,,0000,0000,0000,,medicine, if somebody comes around and\Nis well-known and says things like,
Dialogue: 0,0:49:34.25,0:49:42.23,Default,,0000,0000,0000,,"homeopathy works", we don't believe them.\NWe do trials, we do good trials. And
Dialogue: 0,0:49:42.23,0:49:50.43,Default,,0000,0000,0000,,there's a lot of myths out there, like, or\Nnot well tested things, like "hire the
Dialogue: 0,0:49:50.43,0:49:54.74,Default,,0000,0000,0000,,best programmers, they are 100 times\Nmore productive", "do steady type
Dialogue: 0,0:49:54.74,0:50:00.43,Default,,0000,0000,0000,,systems", and stuff like that. And we need\Nto verify that this is true, that this
Dialogue: 0,0:50:00.43,0:50:02.21,Default,,0000,0000,0000,,helps. And it's...
Dialogue: 0,0:50:02.21,0:50:07.49,Default,,0000,0000,0000,,Peter: Okay. So in the grand scheme of\Nthings, arguably you're right. In the
Dialogue: 0,0:50:07.49,0:50:12.74,Default,,0000,0000,0000,,grandest scheme of things, computer\Nscience is actually a branch of psychology
Dialogue: 0,0:50:12.74,0:50:18.61,Default,,0000,0000,0000,,or really sociology. We are trying to\Nunderstand how large groups of people can
Dialogue: 0,0:50:18.61,0:50:25.84,Default,,0000,0000,0000,,combine to make things which are insanely\Ncomplicated. Now, for - would it be good
Dialogue: 0,0:50:25.84,0:50:31.33,Default,,0000,0000,0000,,if we had, you know, solid evidence that\Nprogramming in this language was better
Dialogue: 0,0:50:31.33,0:50:38.45,Default,,0000,0000,0000,,than programming in that language? Well,\Nyes, but it's staggeringly difficult and
Dialogue: 0,0:50:38.45,0:50:45.08,Default,,0000,0000,0000,,expensive to do honest experiments of that\Nnature and they're scarcely ever done,
Dialogue: 0,0:50:45.08,0:50:49.04,Default,,0000,0000,0000,,right? You might do little experiments on\Nlittle groups of students but it's really
Dialogue: 0,0:50:49.04,0:50:55.93,Default,,0000,0000,0000,,difficult. And then some of these things\Nwhich I'm saying, when one is familiar
Dialogue: 0,0:50:55.93,0:51:01.74,Default,,0000,0000,0000,,with the different possible options, are\Njust blindingly obvious. I mean, there are
Dialogue: 0,0:51:01.74,0:51:09.16,Default,,0000,0000,0000,,reasons why these people are using OCaml\Nfor their system programming, right? It's
Dialogue: 0,0:51:09.16,0:51:16.61,Default,,0000,0000,0000,,not - you know, it's not - "Homeopathy is\Nright", but "Homeopathy is wrong" which is
Dialogue: 0,0:51:16.61,0:51:21.23,Default,,0000,0000,0000,,the kind of argument being put forward.
Dialogue: 0,0:51:21.23,0:51:24.26,Default,,0000,0000,0000,,Herald: Question from\Nmicrophone 5, please.
Dialogue: 0,0:51:24.26,0:51:29.61,Default,,0000,0000,0000,,Mic 5: So where are you using ECC\Nmemory for your testing - up here.
Dialogue: 0,0:51:29.61,0:51:33.51,Default,,0000,0000,0000,,Peter: When you say up here,\Nthere's a bit of ambiguity.
Dialogue: 0,0:51:33.51,0:51:34.82,Default,,0000,0000,0000,,Mic 5: Here.
Dialogue: 0,0:51:34.82,0:51:37.86,Default,,0000,0000,0000,,Peter: Thank you. Say again?
Dialogue: 0,0:51:37.86,0:51:43.12,Default,,0000,0000,0000,,Mic 5: So where are you using ECC memory\Nfor the testing you showed about the
Dialogue: 0,0:51:43.12,0:51:51.07,Default,,0000,0000,0000,,results of the multithreaded results due\Nto memory barriers and memory reorderings?
Dialogue: 0,0:51:51.07,0:51:55.45,Default,,0000,0000,0000,,Peter: Well...
Dialogue: 0,0:51:55.45,0:52:00.13,Default,,0000,0000,0000,,Mic 5: Okay, but even if you were or you\Nwere not, the point I want to make is that
Dialogue: 0,0:52:00.13,0:52:05.95,Default,,0000,0000,0000,,you can expect about 1 bit flip each\Nminute in a modern computer system that
Dialogue: 0,0:52:05.95,0:52:13.67,Default,,0000,0000,0000,,may completely change what your software\Nis doing, so perhaps we also have to look
Dialogue: 0,0:52:13.67,0:52:19.18,Default,,0000,0000,0000,,in ways how we can work if something goes\Nwrong at the very low level so that we
Dialogue: 0,0:52:19.18,0:52:25.01,Default,,0000,0000,0000,,kind of have a check against our\Nspecification on a more higher level of
Dialogue: 0,0:52:25.01,0:52:31.94,Default,,0000,0000,0000,,our software. So it is valuable to do good\Nengineering on the low levels, but still I
Dialogue: 0,0:52:31.94,0:52:37.67,Default,,0000,0000,0000,,think we will not solve the problems of\Ncomputation and computer engineering just
Dialogue: 0,0:52:37.67,0:52:42.52,Default,,0000,0000,0000,,by proving things in the mathematical\Ndomain because computers are physical
Dialogue: 0,0:52:42.52,0:52:47.74,Default,,0000,0000,0000,,entities. They have errors and so on and\Nwe really have to deal with them as well.
Dialogue: 0,0:52:47.74,0:52:54.34,Default,,0000,0000,0000,,Peter: So it's certainly true that there\Nare such random errors. In fact, I would
Dialogue: 0,0:52:54.34,0:52:59.48,Default,,0000,0000,0000,,put the point that I would argue that you\Nhave to be able to model the physics well
Dialogue: 0,0:52:59.48,0:53:03.68,Default,,0000,0000,0000,,enough and you have to be able to model\Nthe statistics of those errors well
Dialogue: 0,0:53:03.68,0:53:07.75,Default,,0000,0000,0000,,enough, so that's a different kind of\Nmathematics. And it's certainly valuable
Dialogue: 0,0:53:07.75,0:53:13.29,Default,,0000,0000,0000,,and necessary. But if you look at the\Nstatistic you just quoted, is that the
Dialogue: 0,0:53:13.29,0:53:22.11,Default,,0000,0000,0000,,main cause of why systems go wrong? Except\Npossibly for space hardware, no. So
Dialogue: 0,0:53:22.11,0:53:26.50,Default,,0000,0000,0000,,important, yes. The most important thing\Nthat we should be paying attention to? I
Dialogue: 0,0:53:26.50,0:53:29.94,Default,,0000,0000,0000,,don't really think so.
Dialogue: 0,0:53:29.94,0:53:32.98,Default,,0000,0000,0000,,Herald: Microphone 6, please?
Dialogue: 0,0:53:32.98,0:53:41.20,Default,,0000,0000,0000,,Mic 6: Hi. I really think that what you're\Nproposing to specify and verify more key
Dialogue: 0,0:53:41.20,0:53:47.16,Default,,0000,0000,0000,,components is - would be a valuable\Naddition, but how do you make sure that
Dialogue: 0,0:53:47.16,0:53:51.88,Default,,0000,0000,0000,,your specification actually matches the\Nbehaviour that you want to do or to have?
Dialogue: 0,0:53:51.88,0:53:58.30,Default,,0000,0000,0000,,Peter: So as I described, we do as partial\Nvalidation of those specifications, we do
Dialogue: 0,0:53:58.30,0:54:03.05,Default,,0000,0000,0000,,a lot of testing against the\Nimplementations, against a range of
Dialogue: 0,0:54:03.05,0:54:07.06,Default,,0000,0000,0000,,existing implementations. That's one\Nsource of validation. Another source of
Dialogue: 0,0:54:07.06,0:54:11.52,Default,,0000,0000,0000,,validation is that you talk to the\Narchitects and the designers. You want the
Dialogue: 0,0:54:11.52,0:54:16.93,Default,,0000,0000,0000,,internal structure to match their intent.\NYou want it to be comprehensible to them.
Dialogue: 0,0:54:16.93,0:54:21.51,Default,,0000,0000,0000,,Another kind of validation that we do is\Nprove properties about them. So we proved
Dialogue: 0,0:54:21.51,0:54:28.75,Default,,0000,0000,0000,,that you can correctly compile from a C11\Nconcurrency, a mathematical model of that,
Dialogue: 0,0:54:28.75,0:54:35.43,Default,,0000,0000,0000,,to a IBM Power concurrency. And that kind\Nof proof gives you a bit more level of
Dialogue: 0,0:54:35.43,0:54:39.45,Default,,0000,0000,0000,,assurance in both. So none of this is\Ngiving you a total guarantee. You
Dialogue: 0,0:54:39.45,0:54:43.98,Default,,0000,0000,0000,,certainly don't claim a total guarantee.\NBut it gives you pretty good levels of
Dialogue: 0,0:54:43.98,0:54:47.88,Default,,0000,0000,0000,,assurance by normal standards.
Dialogue: 0,0:54:47.88,0:54:49.58,Default,,0000,0000,0000,,Herald: Mic 4?
Dialogue: 0,0:54:49.58,0:54:56.31,Default,,0000,0000,0000,,Mic 4: Yes. Thanks again. You proposed\Nrandom tests, and with my expertise, it's
Dialogue: 0,0:54:56.31,0:55:02.86,Default,,0000,0000,0000,,very annoying if you have tests where the\Noutcome is sometimes a failure and you
Dialogue: 0,0:55:02.86,0:55:10.50,Default,,0000,0000,0000,,want to have reproducible tests to fix a\Nbug. So how do we bring this aspects to
Dialogue: 0,0:55:10.50,0:55:17.85,Default,,0000,0000,0000,,test more variety in data and to have it\Nreproducible together?
Dialogue: 0,0:55:17.85,0:55:24.80,Default,,0000,0000,0000,,Peter: Well, if - as I was mentioning, for\Nthe TCP thing, one of the - so the problem
Dialogue: 0,0:55:24.80,0:55:29.15,Default,,0000,0000,0000,,is reproducibility is exactly this\Ninternal non-determinism, right? The
Dialogue: 0,0:55:29.15,0:55:33.39,Default,,0000,0000,0000,,system makes this scheduling choice or\Nwhat have you and you can't see what it
Dialogue: 0,0:55:33.39,0:55:39.60,Default,,0000,0000,0000,,is, or the checker can't see what it is.\NSo one way to do that is to really design
Dialogue: 0,0:55:39.60,0:55:45.37,Default,,0000,0000,0000,,the protocols in a different way to expose\Nthat non-determinism. The other fact about
Dialogue: 0,0:55:45.37,0:55:53.42,Default,,0000,0000,0000,,this kind of general purpose specification\Nas test oracle idea is that in some sense,
Dialogue: 0,0:55:53.42,0:55:59.24,Default,,0000,0000,0000,,it doesn't have to be reproducible. Right?\NThe specification is giving a yes-no
Dialogue: 0,0:55:59.24,0:56:05.51,Default,,0000,0000,0000,,answer for an arbitrary test. And that\Nmeans that you can use arbitrary tests.
Dialogue: 0,0:56:05.51,0:56:09.73,Default,,0000,0000,0000,,Figuring out the root causes of the\Ndifferences afterwards may be tricky, but
Dialogue: 0,0:56:09.73,0:56:13.20,Default,,0000,0000,0000,,you can use them for assurance.
Dialogue: 0,0:56:13.20,0:56:18.49,Default,,0000,0000,0000,,Herald: So we now got time for two\Nmore questions. Microphone 1, please?
Dialogue: 0,0:56:18.49,0:56:23.07,Default,,0000,0000,0000,,Mic 1: Hiya. Thanks for a great talk. So\Nwhat you've described seems to be a middle
Dialogue: 0,0:56:23.07,0:56:28.26,Default,,0000,0000,0000,,ground between a full-on, formal\Nverification and more practical testing,
Dialogue: 0,0:56:28.26,0:56:34.31,Default,,0000,0000,0000,,like, in between. So where do you see in\Nthe future where formal verifications will
Dialogue: 0,0:56:34.31,0:56:39.83,Default,,0000,0000,0000,,go? Will they converge to the middle or\Nwhether it will still be there just to
Dialogue: 0,0:56:39.83,0:56:44.30,Default,,0000,0000,0000,,verify something that's more\Nwell-specified?
Dialogue: 0,0:56:44.30,0:56:49.94,Default,,0000,0000,0000,,Peter: So the progress of sort of the\Nwhole subject of formal verification in
Dialogue: 0,0:56:49.94,0:56:56.93,Default,,0000,0000,0000,,general, if you look at that over the last\N10 years or so, it's been very - it's been
Dialogue: 0,0:56:56.93,0:57:01.35,Default,,0000,0000,0000,,really amazing compared with what we could\Ndo in the 80s and 90s and early 2000s,
Dialogue: 0,0:57:01.35,0:57:06.48,Default,,0000,0000,0000,,right? So the scope of things, the scale\Nof things which are - for which it is
Dialogue: 0,0:57:06.48,0:57:11.18,Default,,0000,0000,0000,,becoming feasible to do verification is\Ngetting bigger. And I think that will
Dialogue: 0,0:57:11.18,0:57:16.34,Default,,0000,0000,0000,,continue. You know, I don't know when you\Nmight see a completely verified TOR
Dialogue: 0,0:57:16.34,0:57:23.98,Default,,0000,0000,0000,,client, let's say, but that's not\Ninconceivable now. And 20 years ago, that
Dialogue: 0,0:57:23.98,0:57:29.47,Default,,0000,0000,0000,,would have been completely inconceivable.\NSo that is expanding and at the same time,
Dialogue: 0,0:57:29.47,0:57:36.83,Default,,0000,0000,0000,,I hope we see more of this interface, text\Nbased oracle specification - and these -
Dialogue: 0,0:57:36.83,0:57:41.00,Default,,0000,0000,0000,,when you're doing formal verification of a\Npiece of the system, you have to have
Dialogue: 0,0:57:41.00,0:57:47.81,Default,,0000,0000,0000,,these indicators already defined, all\Nright? So these two fit very well together.
Dialogue: 0,0:57:47.81,0:57:51.49,Default,,0000,0000,0000,,Herald: So the last question\Nfrom microphone 2, please.
Dialogue: 0,0:57:51.49,0:57:56.04,Default,,0000,0000,0000,,Mic 2: Hi. You mentioned that you often\Nfind bugs in hardware. Is there any effort
Dialogue: 0,0:57:56.04,0:58:00.31,Default,,0000,0000,0000,,to verify the transistors on chips\Nthemselves as well?
Dialogue: 0,0:58:00.31,0:58:03.44,Default,,0000,0000,0000,,Peter: So there's a whole world of\Nhardware verification. That wasn't my
Dialogue: 0,0:58:03.44,0:58:10.64,Default,,0000,0000,0000,,topic today. And most of the big processor\Nvendors have teams working on this.
Dialogue: 0,0:58:10.64,0:58:14.44,Default,,0000,0000,0000,,Unsurprisingly, if you remember your\Nhistory, many of them have teams focusing
Dialogue: 0,0:58:14.44,0:58:21.06,Default,,0000,0000,0000,,on the floating-point behaviour of their\Nprocessors. And they're doing - they're
Dialogue: 0,0:58:21.06,0:58:26.98,Default,,0000,0000,0000,,also doing by the standards of ten years\Nago, pretty spectacularly well. So there
Dialogue: 0,0:58:26.98,0:58:33.18,Default,,0000,0000,0000,,are companies that have the whole of some\Nexecution unit formally verified. There's
Dialogue: 0,0:58:33.18,0:58:36.98,Default,,0000,0000,0000,,been a lot of work over the years on\Nverification of cache protocols and such
Dialogue: 0,0:58:36.98,0:58:43.10,Default,,0000,0000,0000,,like. Right? There's a lot of work on not\Nverifying the hardware as a whole, but
Dialogue: 0,0:58:43.10,0:58:47.52,Default,,0000,0000,0000,,verifying that, you know, the RTL-level\Ndescription of the hardware matches some
Dialogue: 0,0:58:47.52,0:58:54.06,Default,,0000,0000,0000,,lower level description. So\Nthere is a lot of that going on.
Dialogue: 0,0:58:54.06,0:58:57.62,Default,,0000,0000,0000,,Herald: Thank you very much\Nagain for this great talk.
Dialogue: 0,0:58:57.62,0:59:00.48,Default,,0000,0000,0000,,Give him another applause.\NThank you, Peter.
Dialogue: 0,0:59:00.48,0:59:01.79,Default,,0000,0000,0000,,Peter: Thank you.
Dialogue: 0,0:59:01.79,0:59:04.22,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:59:04.22,0:59:15.00,Default,,0000,0000,0000,,subtitles created by c3subtitles.de\NJoin, and help us!