PLSE Seminar Series: Derek Dreyer, “RustBelt”

folks, so welcome to the first PLSE colloquium
talk for the 2018-2019 school year. Today I am super,
super, super excited that we have Derek Dreyer here. For those of you who are new
Derek’s work, Derek’s done a– sort of had this pattern
of discovering modularity where it looked really hard to
extract throughout his career. And this was represented
in early papers, like “F-ing Modules”– he’s
also good a paper titles– and really fancy program
logics, like Iris, which we’ve been
looking at as part of the diesel work
for inspiration. But today we’re going to
hear more about RustBelt, which is a project to– research about this
new program that’s named Rust, which many of
you have seen for doing type-safe systems programming. Along the way, Derek’s
collected a lot of awards, including the Milner
Award in 2017. And he also has a killer
whiskey collection. So plenty to ask him
about during one-on-ones. Please, take it away. DEREK DREYER:
[CHUCKLES] Thanks, Zach. So thanks for inviting me. So I’m excited to tell
you about RustBelt. So this is a project
that we’ve been doing now for a couple of years. It started about 2
and 1/2 years ago. And I’m particularly
excited about it because I’ve spent a
long time, you know, doing research on programming
language theory where we build a lot of these pipe systems,
and logics, and semantic models, and all this sort
of mumbo jumbo. And you wonder if
it has anything to do with a real
programming language. And so I’m happy to say it
does, and that actually I’ll– there’s some work that’s come
out of the programming language and verification community
over the past 20 years that has a direct relevance
to both understanding and evolving a major new
actively developed programming language called Rust. So how many of you
have heard of rust? Yeah, OK, I figured. [LAUGHTER] You know, for
different audiences, you get different results. But I figured, OK,
that one was easy. And how many of you have
actually programmed in Rust? Well, those are pretty good. How many of you have proven
that Rust is a safe (LAUGHING) language? [LAUGHTER] All right. Usually one of those
questions there’s like two people who raise
their hand for a second. I have to adapt the talk
for different audiences. OK, so indeed, RustBelt is
all about the Rust programming language. So let me just– I know many of you
know a bit about it, but I’m just going to
go quickly through some of these backgrounds slides. So first of all, the
basic idea of Rust is that it’s trying to
address a longstanding problem in the design of
programming languages, namely how do you balance
safety and control? Right, so on the one hand,
you have high-level languages, like Java and C Sharp,
and Haskell, and Go. These are sort of–
they’re develop– they’re intended for building
high-level safe applications. They have nice high-level
abstractions, automatic memory management, things like this. But they don’t let you write– they don’t give you sort
of low-level control over resource management
and data layout and memory. And for those kind of language–
for those kind of tasks, you are forced to work at a
much lower level of programming in low-level, unsafe systems
programming languages, like C or C++. And those give
you much more fine grain control over resource
management and performance, but at the expense of losing
these nice high-level safe abstractions. So the question has
always been, can you somehow get the
best of both worlds and get a safe systems
programming language? So this is the sort of niche
that Rust is trying to fill. And so a few things about Rust. So basically it’s been developed
at Mozilla since around 2010. And it’s– Mozilla is still
the biggest user of Rust. They’ve been using
it to build Servo, which is this next-generation
browser engine that has, you know, geared for better
parallel performance, pieces of which have been
already integrated into Firefox since last year. And I think the reason
that a lot of people are excited about Rust is
that it’s the only systems programming language so far
to provide three things. One is low-level control
over resource management in the style of modern C++. The second is strong
safety guarantees, things like type safety
and memory safety, but also
data-race-freedom, which is not something
you typically get in other safe
high-level languages. And third, and
definitely not least, it has industrial
development and backing, which is essential for the
language to be adopted. So those three things
alone, I think, sort of make it a very
interesting object for study. And there has been very
little study of Rust so far. Another thing is, so there
are– although Mozilla is still the prime user of Rust, there
are many other companies that have small teams or
groups within them that are using Rust in production code. One of the examples
of this is Dropbox, which we wrote a core component
of its block storage engine from Go into Rust in order
to get better control over its memory
footprint while still maintaining safety guarantees. But there’s many other
companies using it. When I first gave this
talk two years ago, the number was like– the number
I was given by people at Rust was over 15 companies. So this number has
gone [AUDIO OUT].. So you know, at a
high-level, the point here is I think Rust
has the potential to become a sort of next big
thing in systems programming. All right, so enough
sort of marketing stuff. So like now let’s get to the–
let’s get to the details. What’s actually
interesting about Rust? So basically the idea
of Rust, the core idea, which you would hear
about also if you’ve heard talks about
Rust before, is that the sort of root of all
evil in systems programming is the unrestricted combination
of mutation and aliasing. So, in particular, if you
have like multiple aliases or references to some
object in memory, and one of those references
is used to access it and maybe mutate it or de-allocate
it, reallocate it, this can result in things
like dangling pointers, use-after-free errors, data
erases, iterator invalidation– we’ll see an example
of that in a second. And these are all sort
of common anomaly– very, very common anomalies
in C++ programming. And so the idea
in Rust is that it wants to try to prevent all
these kind of errors using what’s often called an
ownership type system, in the academic world more often
a substructural type system. And the basic idea of that
type system is the following. So the basic idea is that
what Rust tries to do is it tries to enforce a
certain principle, which is that an object can either be
mutable or it can be aliased. And it can go back and
forth between both, between being mutable
and being aliased, but it can’t be both
at the same time. And the way that
this is enforced is through this, as I said,
this idea of ownership. So the idea is that,
in a standard language, you know, most other languages,
if you have a value of type T, let’s say value x of
type T in your scope that you can refer to, well,
you can refer to as many times as you want, and
that’s perfectly fine. In Rust, if you have a value
of type T in your scope, it means you know
something additional about it, which is that
you own that object, meaning there can’t be other
pieces of the program that have access to that object
at the same time, OK? There can’t be other parts
to have aliases into it or anything like that. So this means, once you have– that means you can
mutate it as much as you want without fear
of invalidating any other references
into the object. Now, of course, you do want to
be able to create references to an object. So that’s supported through
something called “borrowing.” You can borrow a value
of a certain type that creates references that can
either be shared or mutable. And, basically,
the difference is that when you create
something by– when you create a reference
that’s mutable, it’s the unique reference. That’s the only reference
that can be used to access it. And, correspondingly,
you are allowed to mutate through
that reference. You have, in other words,
mutation but no aliasing. The other one is shared. So you can make a
shared reference by– as the name suggests,
you can make arbitrarily many copies of that
reference, share them with different
threads, for example. But they cannot be used to
directly mutate the object. So there you have
aliasing but no mutation. So this is the basic
idea of a language. And to sort of make this
a little more concrete I’m going to go to a demo, which
is not a very exciting demo, but I feel it’s a little more– yeah, OK, good. Right. There. OK, so here’s– this is
like sort of Rust 101. So this is just a
little program that creates a vector, v, containing
three elements, 1, 2, 3. It pushes an element onto
the end of the vector, 42, and then it just iterates
over the vector and prints out the elements, OK? It’s nothing very fancy. So, you know, just
to show you what happens if I run this
in Rust, and– can you see that in the back? That’s OK?– it prints 1,
2, 3, 42 as you’d expect. OK, so now let’s
see what happens if I move this push onto the
vector inside the for-loop, OK? So now what do you think
will happen or should happen when I try to compile this? AUDIENCE: It should be– DEREK DREYER: Say again? AUDIENCE: Like, you
have the ampersand so we should commute this? DEREK DREYER: I have
the ampersand, yes. So, OK, so that’s a sort
of– that’s correct. That’s going to be a– that’s
a fairly technical explanation. So is like– what would go–
let me put it a different way. What would go wrong if, indeed– so you’re right that Rust
is going to reject this. What would go wrong if
Rust were to accept this? [INTERPOSING VOICES] DEREK DREYER: Say again? AUDIENCE: It should
be infinitely, right? Because every time you’re trying
to iterate over something, you’re also adding something– DEREK DREYER: There’s
a more– that could be, but there’s a more
basic problem. AUDIENCE: Well, eventually,
the buffer you– for sticking your vector
in is gonna be too small. And so you’re
probably going to have to go accompany the entire
vector somewhere else. And that for-loop is going
to have a point or two, who the hell knows what! DEREK DREYER: Exactly, right. So that’s the– there’s a
safety violation here, right? And the safety
violation is that– and I didn’t tell you exactly
how the push operation works. But the way that the
push on the vector works is that, when you
push onto the vector, it tries to add it
within the space that it’s already allocated. If it runs out of space
that’s been allocated, then it has to reallocate the
whole vector, copy it over, and then this for-loop
will be operating on a dangling pointer, OK? So this is a common phenomenon
known as iterator invalidation. And in a language like C++,
you would not get any static– I mean, that happens
all the time. So let’s see what happens
when you actually do this. All right, so we see that– oh, it’s off the end there. Right, so you see it says,
“cannot borrow ‘v’ as mutable” here, mutable
borrow occurs here– “cannot borrow a ‘v’ as mutable
because it is also borrowed as immutable,” OK? So this is getting back
to what you were saying. So at this point, when
we created the iterator, we actually– and you
were– you had to write this as an ampersand v in the code– you actually created a shared
or immutable borrow of v to pass it to the iterator, OK? And that means that, while
the iterator is active, there can’t be any other– you can’t do any mutable
operations on the vector, right? And in particular here, what
you may wonder why it says “mutable borrow occurs here.” Well, implicitly, when you
call the push function, it takes as an argument
a mutable reference to the vector. So this is– there’s
some syntactic sugar here that’s actually creating a
mutable reference in order to pass the push function. So it’s saying, well,
you can’t possibly create a mutable borrow here
because there’s currently a shared borrow in scope. Now, of course, you may
wonder, like how does it know that the shared
borrow is in scope? Or what is the scope
during which the shared borrow is active? That’s handled through something
called lifetimes, which I’m not going to get into in this talk. But, basically, the lifetimes
are sort of inferred scopes during which a reference
is allowed to be used. And so, in particular,
you would hope that, if I move this operation
outside of the loop, right– so if I move it after
the loop, that this would be allowed because
now the iterator is over. And so I should get back
control of the vector, and I should be
able to mutate it. And, indeed, it is. OK, and that’s fine. And so there’s
something– the point– is the point of this
example is just to show Rust is doing
something useful. It’s preventing
iterator invalidation. And it’s quite
subtle because it has to figure out what is exactly
the scope during which that reference that was
passed to the iterator is allowed to be used. And not make it–
you know, it doesn’t want to make it the
rest of the program. It wants to make it
as small as possible. So Rust is doing quite a
lot of useful stuff here. So that was– that’s my demo. OK, so the story
I’ve told you so far, this idea that Rust is
preventing the combination of mutation and aliasing, is– at a high-level, this
makes a lot of sense. This is the story you’ll hear
if you hear talk about Rust. Unfortunately, it’s
actually false. And the reason is sometimes
you need the combination of mutation and aliasing, OK? So, in particular, if
you’re implementing a variety of different kinds
of libraries, so for example, pointer-based data
structures, so it’s actually doubly-linked
lists, fundamentally rely on the combination
of mutation and aliasing. Synchronization mechanisms,
like locks, channels, and semaphores, to implement
that, you need to implement communication between threads. And you need to– to implement
that, you basically– you fundamentally need
shared mutable state. Memory management libraries,
like the reference counting libraries in Rust,
again, fundamentally rely on shared mutable
state because you have multiple
aliases to an object, and they all need to be able
to modify the reference count that’s stored in the object. So these things cannot be
implemented in the safe fragment of Rust. And so, what do you do? Well, here’s what– so
here’s what actually happens. Oh, sorry, before I do that– I forgot. I’m going to show you an example
of some of these libraries and how you can use them to do– to have shared mutable
state but in a safe way. So here I’m going to show you
how you can take an object, x of type T, and you can share it
between multiple threads that can all mutate the object, but
only in a synchronized way, OK? And this is using two
libraries, Arc and Mutex. And I chose these– I chose these libraries– I chose this example
and these libraries specifically because I’m going
to return to Arc and Mutex later in the talk and talk
about sort of why this is– why these libraries are reasonable. Mutex, what is it doing? It’s providing
synchronized access to x. So that means that
the only way you’re going to be able to access
the underlying object and get mutable access
to it is by calling the lock method on the Mutex. Arc is then allowing dynamic
sharing of this Mutex. So you can make arbitrarily
many copies of that Mutex and spread them to
different threads without explicitly tracking the
lifetime of those references. OK, so this is just
a little example to show you how you could– what you can do with
these libraries. Now that we’ve wrapped
it in an Arc and a Mutex, you can spawn a
bunch of threads. Each one is gonna own
its own clone of the Arc. So you first clone the Arc. You then spawn a thread,
and you move the ownership of that clone of the Arc into
the ownership of that thread. And then you can have– and then, each
thread, when it wants to access the
underlying object, it calls the lock
method on the arc. Implicitly, here there’s
a dereference of the Arc that happens. And then that calls
the lock method. There’s some error handling. And now you basically get,
in the scope of the thread, mutable access to the underlying
object through this handle y. And the whole point is, this is
something you cannot implement without using these libraries
because clearly you’re getting shared mutable state, right? And that’s something
that’s disallowed by Fiat by the type system. But it is allowed here because
these libraries sort of give you a safely controlled
use of shared mutable state. Yeah? AUDIENCE: Sorry, can you
just say that bit about move louder and more slowly? DEREK DREYER: Yeah,
I’m not– that’s not so important for this talk. But basically, what’s
happened– the move is just– this is syntax
for saying, move– the thing– it’s basically
moving the ownership of my data implicitly, because that’s a
free variable of the closure, into the scope of the– AUDIENCE: So– I see. So it captures whatever– [INTERPOSING VOICES] DEREK DREYER: It’s saying
that the free variables here have to be moved into the
ownership of this closure. Yeah. Yeah? AUDIENCE: What is the type of y? DEREK DREYER: Yeah, I don’t
want to get into that. [LAUGHTER] You may wonder why I
didn’t write the type of y. I’m fudging some details. I mean, this is
correct code, but– well, OK. Mindful of the fact that
there’s no code here. But, OK, whatever. [LAUGHTER] But, yeah, it gets a little– you get into like
Mutex guards and stuff like this, which I didn’t
want to show, all right? So, yeah. Morally, you can
think of it as you have like ampersand mute of
T. That’s not quite right. It’s more complicated than that. AUDIENCE: So the lock gets
released automatically? DEREK DREYER: Yes. This is what’s called in the
C++ world the RAII style, right? So you basically–
you acquired a lock, and then implicitly
when y– when this handle goes out of scope,
then it gets unlocked, yeah. OK? OK. So this is just– so this is
a positive example of what you can do with these libraries. But, of course, as
I said, this means you’re going– somehow we’re
going outside the safe fragment language. So what’s going on? Well, what’s going on is these
libraries fundamentally extend the expressive power of Rust. And they do that
using unsafe code. So the idea is that
most of the code in Rust is written in– in sort
of the Rust ecosystem is written in the safe
fragment of the language. But then there are
these libraries, like Arc and Mutex
and many others, that provide so-called safe
AP Is that are internally implemented with unsafe code. So meaning that inside their
implementations, at some point, you’ll see these unsafe blocks
where additional operations are permitted that do things like
raw pointer manipulations that are not sanctioned
by the core type system. And so the claim that the
library developers will often want to make about these APIs
is that, if you write your code using the same fragment extended
with calls to these APIs, you will never observe any
undefined behavior, OK? So as long as you don’t use
unsafe features yourself, except the ones that appear
inside these safe APIs, you’re OK. And, you know, as a
verification person, I get very excited when
I hear claims like that. That’s very– [LAUGHTER] –that sounds like a
fertile– fertile ground for, you know, for research
and bug finding. So to give you an example
of the kind of problems that have arisen, and
that continue to arise, so there was a blog post–
a very nice blog post that Arron Turon,
who’s currently the manager of the Rust
project, wrote a couple of years ago right before the 1.0
release of the launch. And this was– basically,
he was showing– he was actually touting the
benefits of this whole approach that I’ve talked about
so far, this sort of safe core, extended with– where its expressive
powers extended through these libraries. And it built up a bunch
of interesting concurrent libraries from simple ones
to more complicated ones. And the sort of piece de
résistance of the whole blog post was this library for
scoped threads, which were– basically, it was
the– it allowed you to spawn threads that had
access to the parent thread stack frame. And this is something that’s
not typically available in safe programming languages. So that was like the– you know, that was– that was
the very exciting conclusion of the post. Unfortunately, so the
fearless concurrence here was a little too fearless. Because on basically the same– I think was the same day that
he actually posted this– someone found a bug in
the scoped threads, API. And this led to a lot of– some embarrassment for
the Rust community. And it was– it was like,
you know, especially coming a few weeks
before the 1.0 release. So if you want– I’m not going to tell you
a detail about the bug. It’s actually very interesting. But basically the
point was, you could combine this API with another
API that was very common, the reference counting API. And you could– and
by the combination of those two things, you could
get used after free errors. And this came to be
known as leak apocalypse. And, you know, this is– it’s kind the thing
you don’t want to happen– you don’t
want to have happen right before the 1.0
released the language. But also, I mean, this is not
like a one-time problem, right? This is the kind of
thing that will continue to keep happening because people
are always developing new APIs. They’re– in fact, one of the
benefits I would say of Rust is that people keep building– they keep finding new safely
controlled ways of manipulating shared mutable state. This is like a very
common pattern in how people develop Rust code. And they put these
things out as safe APIs. And so, you want to
have a way of saying, like, you know, how do I
know that this is actually safe to do? So how can we ensure
formally that bugs like this don’t occur? So this is the basic goal
of the RustBelt project. We’re trying to develop the
first logical foundations for Rust. We want to use these
foundations to verify the safety of both the
core Rust type system and standard libraries
and future libraries that people will develop. And, in particular, we want
to give Rust developers the tools they
would need in order to safely evolve the
language and have confidence that the libraries they’re
building are safe to use. And so I’m going to talk– yeah, so that’s the
goal of the project. So in the rest of the
talk, so first of all, I want to go into a little
more detail about what I mean by “safety.” So, and by the way, if there’s
any questions, feel free to– OK, good. So what do I mean by “safety?” So first of all, the standard
approach programming language safety that people have taken
in the programming language community for a long time
is this so-called syntactic approach, that I’m sure many– I’m sure all of you are familiar
with, due to writing flaws in this progress and
preservation approach. And the problem is that the
syntactic safety approach fundamentally assumes
there’s no unsafe code. It assumes that your
entire language is safe. And so basically this
doesn’t work for Rust, OK? Yeah? AUDIENCE: Can you
just unpack that? I mean– DEREK DREYER: Yeah, sure. So the idea of
syntactic safety, right, as you say here’s– you
know, I take the notion of well-typedness on programs,
I lift just the machine states, and then I prove this progress
and preservation theory. AUDIENCE: INAUDIBLE DEREK DREYER: What? AUDIENCE: Yeah,
no, I said, amen. Right? DEREK DREYER: Yeah. [LAUGHTER] But this assumes that your
notion of well-typedness covers the whole program, right? So though– I mean, the
problem is with unsafe blocks. Basically, you have pieces of
a program that are just not syntactically well typed. AUDIENCE: I see,
but you could always invent more breadcrumbs and
more syntax to box them, state their assumptions,
you know, basically reflect the assumptions of the
API, like in the syntax, right? Now, I don’t want to
disjoint you at all. I was just– DEREK DREYER: So
I– yeah, so I don’t know how to do that for
a language like Rust. AUDIENCE: OK, fine. And fair enough. I don’t want to derail– [INTERPOSING VOICES] DEREK DREYER: I mean,
just the general, right– AUDIENCE: I’m trying
to approach on what’s the technical point here. And– DEREK DREYER: Sure. AUDIENCE: –you’re technical
point is just, hey, I clearly need to reflect
back into my syntax everything about the
machine state that’s relevant to safety. How do I do that for what’s
essentially a foreign function thing? DEREK DREYER: Yes. AUDIENCE: And you and I could
discuss over a beer sometime like how one might
do that or might not, but it’s certainly not– [INTERPOSING VOICES] AUDIENCE: –it’s certainly
not a plain old boilerplate– DEREK DREYER: No. AUDIENCE: –do it. DEREK DREYER: Yeah. AUDIENCE: Yeah. DEREK DREYER: And so,
basically, I mean, you need to have
a way of saying– so, I mean, currently
what happens is, right, if people
give an API in Rust, they have some idea in
mind of what property the implementation is
supposed to satisfy in order to be considered safe, but
it’s not a syntactic property. And it may depend on arbitrarily
complicated invariance about why that code is– about the data structure
that code is maintaining. And so that’s not something–
those kinds of invariants are typically not the kind
of thing you see in a– expressed in typing rules. Let’s put it that way. But I– so I can’t say
it’s impossible to come up with typing rules. But the point would
be, even if you could, it wouldn’t explain– you’re right, ultimately,
the language is extensible. People keep coming
up with new APIs that are not valid for
the same reason that other APIs are valid. And so if you want to
explain why– you know, sort of have one
unifying framework to explain why all those
things would be valid, you need some other
more semantic approach, and that’s the approach
that we’ve taken. [CELL PHONE RINGING] Yeah. [CHUCKLES] And so basically the idea
is we want to generalize to a notion of semantic safety. So very, very roughly,
the idea is a library is semantically safe
if there’s no way that any application
that is constructed from a bunch of
these semantically safe libraries and
syntactically safe code can get it to induce
undefined behavior. Let’s get into a little
more detail about that. So, first of all, the idea
is you take, basically, what we do is we define
a semantic model. This is a mapping from
interf– from types, the types of the language. All right, so you
give me an interface of a library, which is
just basically a type. You translate that
into a safety contract, which is a– essentially
a verification condition that the implementation
of library has to satisfy in order to
be deemed semantically safe. And then I prove two
things about this. I first of all prove that if the
library is implemented entirely in the safe fragment,
in other words the syntactically safe
subset of the language, then it satisfies its safety
contract by construction, OK? Second, I prove– second– right. For the libraries that do
make use of unsafe code, I have a manual
verification burden, OK? I have to show that they
satisfy their safety contract. But at least I have a safety
contract against which to verify them, OK? And then when you put these
together, this is what you get. So basically, remember this
picture, most of the code is written in the safe
fragment of language. That code is safe
by construction. All you have to do to improve
the safety of your program is to manually
verify the libraries that you use that make
use of unsafe code, and prove that they semantically
inhabit their APIs– they satisfy the verification
condition corresponding to their APIs. And then, you know, those can
be used in any safe program. OK? Yeah? AUDIENCE: So your
framework for thinking about this kind of automates
a little link there? Like, the– DEREK DREYER: You know, the
link is automated, yes, yes. As long as the– right, as
long as the types match up, syntactic– yeah, as long
as the composed things, according to the typing
rules of language, which– yeah, then, exactly. OK? So this is basically what
we’ve been doing in RustBelt. So we have our
initial paper on this was in POPL this
year where we showed how to do this for
a representative but somewhat simplified
version of Rust, which made various
simplifying assumptions, which I’ll get to
some of those later. But, yeah. So, basically, we
took this approach and we showed how we
could do this for Rust. And what I want to do
in– and, oh, sorry. Before I get to that,
the first thing to say is, this is not a new idea. So this is– this
idea has been around for a long time, this basic
idea of semantic safety. However, most– almost–
basically all the prior work has done this much, much,
more toy languages, all right? So very simple– much more
simple lambda calculi, nothing with a type system
as sophisticated as Rust’s and nothing with,
you know, libraries that are doing as sofi– as
complicated low-level things as Rust libraries are doing. So basically what I want to talk
about in the rest of the talk is the key challenge– instead of going into a
lot of details about rust that will be sort of
somewhat impenetrable, I’m going to go
and try to explain what is the key challenge that
we faced in doing something like RustBelt. And
that is figuring out what is the right logic in which
to express these verification conditions, OK? Because, you know, if
you try to express– so if you take the approach
that a lot of previous work has done on semantic safety,
you may have seen things like step-indexed models, step
index logics relations models. If you haven’t seen
them to worry about it. But if you have, they’re quite
complicated and low-level and difficult to reason about. And so what you really want is
a logic that is higher-level and matches better
than the concepts of– the intuitive concepts
of the rust language. So it provides a
higher-level framework in which to carry these
proofs out in an easier way. And I don’t know if
anyone has any guesses as to the sort of general
framework I’m going to suggest? AUDIENCE: How about Iris? DEREK DREYER: You know too much. [LAUGHTER] Even simpler than that. AUDIENCE: Separation logic? DEREK DREYER: Yes. [LAUGHTER] AUDIENCE: All right. DEREK DREYER: So
separation logic. So how many of you have
heard of separation logic? How many of you have ever
used separation logic? OK, good. Good, because I’m going to talk
a lot about separation logic. [LAUGHS] So I’m hoping you don’t
know that much about it. OK, so basically separation
logic– ah, right, as probably most of you know,
is an extension of Hoare logic that was developed by
Peter O’Hearn and John Reynolds and several
others about 20 years ago. And they originally developed
it as a sort of logic for reasoning sequentially about
pointer-manipulating programs– or, sorry, reasoning
modually about sequential pointer-manipulating programs. It was intended as
a sort of, yeah, a much more modular framework
for doing this than plain Hoare logic. It’s had a major influence on
many verification and analysis tools. And, for our
purposes, the reason that it’s really interesting
is that it builds in, as a primitive concept,
this idea of ownership, which is like the fundamental
thing in the Rust type system. And so it’s essentially a
perfect fit for modeling rusts ownership types. And we’ll see this in more
detail later in the talk. So, unfortunately, we can’t
just take separation logic and use that. Why? Well, there’s two major reasons. The first one is that there is
not just one separation logic. There’s many separation logics. [LAUGHTER] There’s actually
more than seven. So the first one here,
for our purposes, is concurrent separation logic. This is by Peter O’Hearn and
Steve Brookes from around 2004. And this is like– this was like
a fundamental advance, I think, in program verification. They showed how the
basic idea of separation logic, although it was
originally just for– it was intended for
sequential programs, it actually is also extremely
useful for reasoning about concurrent programs
that manipulate shared state. And we’ll be getting into
that in more detail later. The problem is there’s been a
lot of advancements since then, right? So the original CSL was
remarkably powerful, but there’s many
things it can’t do. And so, as a result, you have
many of these things– many of these logics coming out. And there was a paper
by Matthew Parkinson, from 2010 actually, which
had this nice quote. It said that, you
know, in recent years, separation logic has
brought great advances, blah, blah, blah. “However, there is a disturbing
transfer for each new library or concurrency primitive
to require a new separation logic.” And that’s exactly the case. So if you read all the papers
on current separation logic, you get a headache because each
one is like saying, you know, here’s this new fancy thing. And then the one after it
says, well, yeah that was nice, but it can’t handle
this example, and then it can’t
handle this example. And so, you know, this
is a major problem if you’re trying to build a
model of a language like Rust. Because, as I
said, new libraries keep coming up all
the time, right? It would be bad if we spent all
this effort building a safety proof of the language, and
then a new library comes up and we say, well, we don’t
know how to verify things. We don’t know how to verify
that because our logic was too limited, and then we
have to redo the whole model. So you really want to have some
very general logic in which to express the
semantic model of Rust that you don’t have to
keep changing all the time. The second problem,
which I’m not going to go into in much detail
today, but I want to mention, is the issue of
the memory model. So most of the previous logics– most of the previous work on
concurrent separation logic has assumed
sequential consistency as the memory model
for concurrency. And this is just not
realistic for the way that high performance concurrent
libraries work, in particular in Rust. So rust has a variety of
concurrent libraries that make use of C++’s relax
memory atomic operations. And, again, I’m not going to go
into detail about this issue, but I just want to mention that
this is something that is sort of the– a basic assumption of– well, this prior work on
concurrent separation logic. And if we want to be able
to build a model of Rust as it actually is, we need to
account for relaxed memory. So this led to two
general directions of work that my group and
my collaborators have pursued over the
past several years. One of them, which I will talk
about a lot today, is Iris. So this is this sort of
general unifying framework for concurrent
separation logic that is intended to sort
of subsume a lot of the prior work on
concurrent separation logic and offer a way of– a sort of general platform for
doing concurrent separation logic groups in the future. GPS is a– was the first modern
separation logic for the C++ memory model that
accounts for some of the– a sort of a core fragment
of relaxed memory operations in C++. And we’ve been developing
that further as well. In fact, the truth
is these are two– these two are sort of joined
together now because we’ve, in our ECU paper
from last year, we showed how we can actually
encode GPS inside Iris as well. So it’s all sort of one thing. But I’m not going to get into
the– all the weak memory stuff in this talk. So for today, what I want
to do is actually start by reviewing– in the
remainder of this talk, I want to start by
reviewing the basic idea of current separation
logic and how that works. And then I’ll give you a
taste of what Iris is about. And I’m going to use these
examples of Arc and Mutex, that I talked about earlier,
as the sort of running examples to show how this works. So CSL is a Hoare logic. I assume most of
you know Hoare logic so I’m gonna be quick here. So that means the basic
thing we’re proving are these triples. They have– there’s the piece
of code we’re verifying, C. There’s the precondition. This is the property that is
assumed to hold of the state before you run C. And then, what the
Hoare triple says is that if the precondition
holds, C is safe to execute. It will not have any
undefined behavior. And if it terminates, or
proving partial correctness, then the postcondition
queue holds– and– of the final state, OK? So that concludes
my presentation of Hoare logic, all right? [LAUGHTER] I hope you found
it illuminating. [CHUCKLES] So separation logic. So separation logic
basically takes the idea of– the basic idea is a Hoare logic. I mean, really– well, yeah. [LAUGHS] One could say
more about Hoare logic, but the truth is,
in this talk, I’m actually not going to go
into much detail about rules. I gonna show you
I think two rules. And otherwise, I’m gonna sort
of do proofs by animation. [LAUGHS] So it’s not so
important that we go into all the details about
the rule of consequence and all that stuff. So in separation logic,
basically, there’s two new things you get. One is that assertions
P are not just denoting facts
about the program, but they’re denoting
ownership of state. As I said, that’s the key
thing in separation logic is ownership as a
primitive notion. So this is– the
canonical example of this is is the points
to assertion, x points to v. Which says that,
if you assert x points to v in your
precondition, it means that the thread, or the piece
of code you’re running, owns x. And not only does it know that
x points to v, but it owns x. So that means there
can’t be other pieces of the program that are
running at the same time that are accessing x. Secondly, there’s this idea
of disjointness of states and this is
connective separating conjunction, or star. So a P star Q means that not
only do P and Q both hold, but they hold a disjoint
pieces of memory. So, for example, if I
have x points to v star, y points to w in
my precondition. Then not only does it mean that
x points to v and y points to w but also the x and
y do not alias. They don’t– they’re not
equal because they have to be pointing to disjoint locations. Yeah? AUDIENCE: Inaudible question DEREK DREYER: Yeah. I mean, they’re– yeah. There’s no reason why the
contents of those locations couldn’t be equal. Yeah, you mean like if v and
w are pointers themselves? For example, yes,
yes, that’s fine. It just means that these two
memory cells are destroyed. OK, so to see an
example– oh, sorry. Before I get there– so basically– so, OK, that
concludes my presentation of separation logic. [LAUGHTER] No, OK, so we’ll see how
this rule’s getting used. So concurrency– that was
basic separation logic, OK? But concurrent separation
logic basically takes those basic concepts
of separation logic and extends it with two rules. There’s a few other sort
of structural rules, but basically there’s
two important rules. One is the rule for
disjoint concurrency. And this is what’s called the
parallel composition rule. This says, if I have
two threads, C1 and C2, that are operating in– two pieces of code that are
being run in parallel, C1, C2, then I can verify them
completely independently as long as they’re operating
on disjoint pieces of state. And operating on
disjoint pieces of state means that their
preconditions, P1 and P2, are joined by the separating
conjunction in the precondition of the parallel composition. So this way I know
that P1 and P2 we’re talking about
separate pieces of memory. So if they’re talking about
separate pieces of memory, there’s no interference
between these threads. So I don’t have to worry
about any reasoning about interference. So to see how that
works, right here you have an example
where you have– again, like x points
to 0 and y points to 0. But they’re starred
together so I know that x is not equal to y. And now I’m going to
verify this code that was one thread modifying x and
the other thread modifying y. And you can just do that by
verifying them separately, right? So this is often how you see
these proofs written on paper. You prove sep– in one
thread, that x– it goes from x points to
0 to x points to 3. Here it goes from y points
to 0 to y points to 4. And then you just glue
them together at the end. And you don’t have to reason
about any possible difference because that interference
has been ruled out implicitly through the separating
conjunction. That’s like the poster
child for separation logic– or for concurrent separation
logic is this kind of example. But it’s kind of boring. Let’s face it, right? So we want– what we
really care about, rather the whole motivation
for a lot of this work, was how do we reason modularly
about this shared state that shows up in these libraries
using unsafe code? So that’s handled
through the second rule that CSL introduces,
so the invariant rule. So the idea within
invariance is that if I want to reason
about shared state, the way to do that is to
impose an invariant on it that all threads have to–
all threads can assume, but they have to maintain. I’m not going to show
you exactly how you create the invariant. It’s not that it’s complicated. I’m just trying to
simplify things. So let’s just say we have
a way of establishing an invariant, R, on some
piece of shared state, OK? All right that is
invariant R. So we’ve established that invariant. And then the rule
says the following. If I want to verify
some piece of code C, then I can temporarily transfer
ownership of the shared state into my local ownership. I can gain ownership of it,
do whatever I want with it, as long as I then restore the
invariant R when I’m done. So I do that by transferring–
when I say transfer it into my local ownership, I mean
start it onto my precondition. Now I own both of
what I had before, my original P plus
this R. And I know they’re disjoint
because, initially, I have local ownership. It was sort of the thing
I personally owned, was P, so that couldn’t be overlapping
with the shared state R. And then I have to restore
it in the postcondition. Now you see there’s this
condition that C is atomic. Anyone see why
that is important? By atomic here I mean it only
takes one step of computation. Yeah? AUDIENCE: Do you wanna try to
conserve the broken variant? DEREK DREYER: Right,
you– exactly. So in this step here,
in this reasoning of the premise– in
proving the premise, you can break the invariant
internally within that proof. So if C were to take more
than one step of computation, it might break the invariant
and another thread might then go and try to use this rule and
expect the invariant to hold, and that would be unsound. So if C only takes one
step of computation, then the internal breaking of
the invariant within that proof cannot be observed
by another thread. And here, again, we’re assuming
a sequentially consistent sort of interleaving
model of computation. OK, all right. So let’s see how this works
using the Mutex example. So this is a very, very
cut down version of Mutex, but it gives you the idea. So, basically, the
Mutex can be represented by this pointer, x, which
either points to 0 or 1, 0 for unlocked and 1 for locked. And there be two
methods, lock and unlock. Again, this is very simple. The lock is just doing– it’s just a spin lock. So it’s just going to keep
trying to compare and set x from 0 to 1 from
unlocked a locked, and there’ll be multiple
threads racing on this location to try to win the race. And whichever one
wins, successfully does the CAS will then return. And unlock just sets
x back to unlocked. So the unlock assumes that the
caller of unlock owns the lock. So here’s the specification
that we could give– or a specification we can
give in separation logic. Let’s say that p describes– is an assertion that
describes the invariant we want to assume about
the resource that’s protected by the lock. Here’s the spec you would give. So first of all, anyone
can call a lock function, but the precondition is trivial. Because you want to
allow multiple threads to do it at the same time,
so anyone can call it. And whoever– once you
successfully return from lock, you gain ownership
of P in your local– in your local state. That you get– you– the ownership of P
has been transferred from the shared state into u. In order to unlock,
you have to give it up. So you have to have P
in your precondition, but you lose it in
the postcondition. So implicitly,
that’s how you get this sort of ownership
transfer in between the local and the shared state. And then, the nice thing is,
if you want to verify code– you know, a bunch of
threads that are accessing– using the lock, then, well– right, so you have– here we have two threads. They have precondition
and postcondition true. So you can– using the
parallel composition rule, true star true is equal to true. So you can verify these
completely independently. And internally, they
just acquire the lock. They get ownership of P.
They do whatever they want. Here, by the way,
this critical section does not have to be atomic. This is just whatever code you
want that manipulates P. It has to restore P at the
end before calling unlock and then returns. So this is how you could
use the Mutex spec. So how do we prove that the
Mutex implementation satisfies the Mutex spec? Here’s– well, first of
all, in order to do this, there’s some shared state,
which is the x, the pointer x. So we have to establish
an invariant on that, and here’s the invariant. It’s going to say– I’m writing it as a disjunction. And to visualize
this disjunction, I’m just going to write
it as a little state machine with two
states where you can go back and forth between them. So either you’re in
the unlocked state. In that case, we
know x points to 0, and the invariant
owns the resource described by this assertion,
P. That’s the shared resource. In the locked state, we
know that x points to 1, but we don’t own P. Because
in the locked state, whoever acquired the lock, they
own the resource described by P. In fact, they
may have broken P. So P may not even
hold at that point. Given this invariant, we can
now verify the implementation of the Mutex. I’m just going to show the
proof for the lock method. So it has, remember,
precondition true. Here’s the implementation. There’s basically two cases. I’m going to slightly hand
wave over a few details here. So there’s two cases–
there’s two interesting cases, basically– or
there’s two cases. One of them is boring. The boring cases
when the CAS fails. Because when the CAS fails, you
just– you know, you try again. So that’s the case when the
X was in the locked position. So that’s not interesting. The interesting case is
when the X was unlocked so the CAS actually succeeds. And then, basically,
we’re verifying this. We’re verifying
that doing this CAS should give us the
post condition, P. So in that case, we can
apply the invariant rule. And the idea is,
right– oh, sorry. I did that too quickly. So remember, the idea
of the invariant rule was it lets you transfer
ownership of the shared resource described
by the invariant into your local precondition as
long as you can re-establish it in your post condition. So we’re going to transfer
ownership of x points to zero star P into
our precondition. It’s really that star true, but
the true doesn’t do anything. And now we want to see
what happens, right? So the key thing is now
we own x so we’re actually able to do the CAS. That’s the thing
you need in order to actually execute the CAS
safely, is ownership of x. So we do it, and we
get x points to star P. Now we need to re-establish
the invariant again on the shared state. And we can because we
have x points to 1. So we can transfer that
back into the invariant. And we keep P in the
postcondition, which is what we needed to show. So this is basically– and then
that’s at the end of the proof. This is a very common
pattern in these proofs, that you use the invariant
rule, you transfer ownership in, you use the ownership
of some physical state, like x in this case, to
actually perform the operation, and then you do something to
re-establish the postcondition. And notice that the footprint,
sort of the piece of memory that was described
by the invariant, has changed before and
after the operation, right? Before it owned the
shared resource. Now it doesn’t. This kind of implicit
ownership transfer that’s allowed by
invariant rule is a key to the power of
concurrent separation logic. Any questions about that? OK. So to recap, CSL basically
extends plain separation logic with these two rules, one for
the sort of boring disjoint concurrency where it makes– says you don’t have a reason
about interference at all, and one for reasoning about
interference using invariants. So, moving on, so we need to– so CSL is great. The orig– In fact, if you
haven’t read the original paper on CSL by O’Hearn– it’s called like,
“Resources, Ownership, and Local Reasoning,”
or something like that– you should. It’s a great paper that shows
how just these mechanisms I showed already
allow you to verify tons of really interesting
and sort of daring forms of concurrency. But it doesn’t do everything. So the reason why
there’s been many– much following
work is because you want to be able to generalize
this invariant mechanism in two ways. One is you want to
be able to describe how state changes over time. So the invariance
just tells you what is a property that holds always. But you also want to
be able to say things like the value of the shared
counter only increases over time. You also want to
be able to control who can make the changes
to the data structure. And this is often done through
things like permissions. You may have heard of
fractional permissions. Tokens, capabilities,
there’s all sorts of mechanisms like this in these
concurrent separation logics. And often these two
things interact. Like, you may want to– you may want to say
that, at a certain point during the program,
certain threads can make certain changes. And that changes
over time as well. So, basically, these two
things are the variations or these are the ways that
CSL has been extended. And it’s been extended
in many different ways. So this is a– you’ve probably, if you’ve
been to POPL or something in the last couple of years,
you may have seen this photo– or this picture. It’s– this is actually
slightly out of date. So this is due to Ilya Sergey. And it’s a family tree of
concurrent separation logic. So you see CSL is like up there. And there’s been a lot
of work since then. And there’s– I think there’s
another layer or two at this point. So this is, you know,
it’s pretty bad. [LAUGHTER] Yeah. AUDIENCE: How many paper
do you write from that? [LAUGHTER] DEREK DREYER: Yeah, I know. [LAUGHTER] Well, actually, I
didn’t write so many. Yeah– no, I didn’t do so–
well, that– well, no this is weak memories. That doesn’t count. I did this and this, yeah. But it was actually,
it was my work on this that’s CaReSL logic. That was my first work
on concurrent separation logic that made me realize– yeah, actually, the history was,
we worked– we did this paper. And then we were
asked to write a book. Me and Lars Birkedal were asked
to write a book about, well, about logical relations
and all this kind of stuff. And we thought, oh, yeah, let’s
do it in a separation logic. We just did this CaReSL
logic, maybe we’ll use that. And then we thought about it. We were like, no, this
is too complicated. We have to simplify
if we’re going to write a sort of
pedagogical text about it. And we talked to Aaron about it. And then he had some ideas. He had this– the
basic idea of how we were going to simplify
it, the basic idea of Iris. And then he sort of
sketched that out. And then he left to
go to work on Rust. And my student Ralf Jung sort
of led the charge after that. But it was actually
that the whole project started based on trying
to simplify things for writing a textbook. We didn’t read the
textbook, but we– [LAUGHTER] Although, we’re trying
to work on that now. But– anyway, so this
is bad in itself. But what’s worse is when you
actually look at these papers, OK? [LAUGHTER] So the first one, that was mine. OK, so that doesn’t
look too bad, but– [LAUGHTER] But, you, know it’s
not that simple. [LAUGHS] And, yeah, so the big– I’m being somewhat
facetious, right? Obviously, it’s OK to have some
complicated rules now and then, right? I mean, sometimes proof
principles are, you know, you’re reasoning about
complicated programs, you need complicated rules. The problem is, really,
that these rules were baked in this primitive logic. Meaning, each logic, to
prove the soundness of logic, there was a separate soundness
argument for each logic. And they were all– they
all used different models. And so you might say,
well, that rule looks nice, I’ll use that rule
for one program. But then– and I want to use
this rule for another program. But you have no idea if you’ll
be able to put these together into one– or, sorry. If you want to use this for
one module in a program, and this for another
module, and you want to put these into a
proof of the whole program, you don’t know if the whole
thing’s gonna be sound. So you really need
one unifying logic so that you can sort
of use whichever rules are
appropriate– you know, whichever rules
are the best rules to use for different
modules, and you want to know that they’ll compose. So there must be a
better way, obviously. And there is. So that’s what Iris is about. So Iris, the basic idea
of Iris is very simple. This is somewhat
oversimplifying, but it’s essentially
the main idea is that really all you need
are invariance a la CSL– it’s a slight lie. They’re a little– I’m slightly lying
here, but not too much. Really, basically,
as I’ve shown it– plus something that
I will talk about now called user-defined
logical state. And using just these
two mechanisms, you can derive the rules of
these most advanced extensions of current separation
logic within Iris so that you can use them
for different pieces of your program and you know
that everything will compose. So to illustrate this,
rather than starting with what is usually
defined logical state, I’m going to start with an
example and show you we use– how logical state comes
up in verifying that, and that’s the Arc example. Again, this is
extremely idealized. The idea is that x here
is going to point to– this x representing
an Arc is going to point to two– an object
with two fields, the reference count and the payload. And I’ll assume the payload
is just a one word here. And then there’s three
methods– the clone method, print, and drop. So clone is going to give
you a clone of the Arc. So what does it do? It bumps up the reference
count using a fetch-and-add. This is an atomic fetch
and increment operation on the count field, and then
just returns a reference to the original x. So it just gives
you an aliased x. The print function is
just printing the data. Not very interesting. And the drop function is
the disruptor for the Arc. So that is going to
decrement the count field. And if it notices that
it was the last went out, so if it notices that the
account field was set to 1, then it’ll free
the whole object. So here’s the spec that we’re
going to prove about this. So first of all, I’m
going to introduce something called Arc of x. So this is an abstract predicate
describing the permission to access shared data
through the Arc x. And that arc of x is going
to be the precondition to all the operations. So here we have
the clone method– or, sorry. Right, in the clone method,
basically what happens is you start with
an Arc of x, and you get an Arc of x star Arc of y. So it gives you a
new Arc permission to the same underlying object. And you know it’s the
same because, remember, we saw that the implementation
will return y equals x. So actually we’re getting Arc
of x star Arc of x in the end. Here we have the print method,
just returns to the same Arc of x. And the drop method
will take Arc of x and consume it so that
in the postcondition you don’t have that privilege
anymore because you’re dropping the Arc. OK, and that’s the spec
that we want to prove. Now, you’ll probably notice
something strange here, which is this– which is that, you
know, I told you before, separating
conjunction was supposed to talk about
disjoint pieces of memory. But here we have in the
result that we’re returning an Arc of x star itself. And both of them are presumably
talking about the same– I mean, they’re talking
about the same pointer x. So how does this make any sense? Well, this is where this
user-defined logical state comes in. Arc of x does not describe
physical ownership of the heap. It couldn’t possibly
because you have these– you have that Arc
of x star, Arc of x. So instead, it’s talking about
a purely logical idea of state. And this is where this idea
of user-defined logical state comes in. So Arc of x is
describing ownership of a logical permission to
access this object, which can be separately owned. And to reason about
this Arc of x, I’m going to
introduce two axioms. Yeah, yeah? AUDIENCE: All right, so it looks
this spec guarantees that you won’t have to use after-free,
but it looks like it doesn’t necessarily
prevent memory errors– or, I’m sorry– DEREK DREYER: Leaks. AUDIENCE: Leaks, yeah. DEREK DREYER:
Correct, that’s right. And also Rust doesn’t either. AUDIENCE: Really? DEREK DREYER: Yeah. AUDIENCE: Cool. DEREK DREYER: That’s right. So this is all a partial
correctness, and it does– and there’s no– exactly, there’s no guarantee
of absence of memory leaks. This is actually part of
where the leak apocalypse thing came in. They sort of thought that some
things they were doing were preventing memory
leaks, but they weren’t. [CHUCKLES] I’m not going to go
into more detail about that, but yeah. Anyway, so I’m going to
declare these two axioms. And we’re going to use
these axioms in the proof. And you’re gonna
wonder why is it OK to just declare these axioms,
and you’re going to be right. But I’ll get back to that, OK? So here are the axioms. And they talk about this other
predicate called count of x, n. I know this is a little
magical, all right? I have to get magical
towards the end of the talk. So the idea is that count of x,
n intuitively describes this– is an exclusive
assertion, which says it tells you exactly
what– how many Arc permissions
have been created. It says that n Arc
permissions exist in the world at the moment, OK? And so the first axiom says,
if n Arc permissions exist, and separately I
own one of them, then n must be at least 1, OK? Clearly, because I’m
showing you that I own one. The second axiom lets you
update this count, increment or decrement. So if I know that
there are n Arcs, right now I can spawn
a new one off, right? I get Arc of x there
in the right-hand side, and simultaneously I bump
up the number n plus 1. And I can also go the other way. And if you’re
attentive to detail, you’ll notice that this
arrow has two lines and this one has three lines. And I’m not going explain why. [LAUGHTER] But, basically, it’s because
this one is implication and this one is a kind of
logical update operation that actually changes the
underlying resource. I’m happy to go into
more detail about that afterwards if you want. But because I’m running short
on time, I’ll just proceed. OK, so let’s assume we have
these logical operations. Now we can define the
invariant on the Arc object. And it says the following. It says that at all times,
there exists a number n, which is such that I own–
the invariant owns this count predicate, which says that
it knows there are n Arcs out there– n copies of this Arc x. And, in addition, either
n is 0 or the shared– or this invariant owns
the predicate describing x, the x object, and
its count field– its reference count
field is n as well. So this is kind of
the logical predicate saying I know that there’s
n Arc permissions out there. And this is the
physical predicate saying that I know that
the count field of x is n. And you notice in the case
when it’s 0, we don’t own x. Because in the case when it’s
0, the object has been freed. So then we don’t own the
physical state, all right? So this invariant
ties the logical state to the physical state. All right, so just to show
that visually, I’m gonna– because I’m gonna
show you this– again, this kind of proof
by flying predicates. We have this sort
of transition system where you can go between
any state– from any state to any other state. Except from 0 you can’t
go to any other state. Because in the 0 case we
don’t have the x predicate. So here, like in the 4 state,
we own x points to 4 something, et cetera, et cetera. In the 0 state we don’t own x. Here’s the thing
we want to prove. The first thing, I’m going
to show you basically how we prove clone. The first thing to observe is
that all these operations take Arc of x as a precondition. So does anyone know what that–
can anyone see what property that guarantees you when
you’re doing the proof or what important– yeah, what important
property that guarantees? AUDIENCE: The reference
count is none 0? DEREK DREYER: And therefore? AUDIENCE: You own x. DEREK DREYER: Yes,
exactly right. And therefore x is
still allocate, right? You can actually access x. So all of these
operations access x. So they’d better be able to
show that the count is not 0 because they need to be
able to get ownership of x, and exactly. And the way that works is,
using this axiom I showed before, you open the invariant. You see, well, I
own count of x, n and I own Arc of x so I know
that n must be greater than 0. So I must be in one
of these states. So x must be allocated. OK, good. So I’ll show you briefly
how this proof works. Remember, this is just
doing a fetch and increment of the x count field
and we’re returning Arc of x, star Arc of x. Proof precedes, as before,
using the invariant rule. So first thing we do is
we say, all right, we know we’re not in the 0 state. Let’s say we’re in the
2 state, all right. I mean, obviously in the
proof you don’t actually say, we’re in the 2 state. You say, I’m in any state
that’s greater than 0. But, again, in order to enable
proof by flying predicates, I’m gonna pick the
case where it’s 2. And so the first thing you
do is you transfer ownership of x into your precondition. OK, good. Now that we have
ownership of x, we can perform the
fetch and increment, and we get x points
to 3 something. And now– now what
do we do, right? We’re kind of stuck because we
want to restore the invariant, but the logical predicate on
count says that we’re– says that the count is 2 and
the physical one says that the count is 3. So we have to somehow fix that. And the way we fix that is,
again, using that other axiom I showed you, which lets
you go from count of x, n to count of x, n plus 1, and
thereby spawning a new Arc. So by applying that,
we go from 2 to 3, and we spawn this Arc up there. And now we can put– we can
put that in our postcondition. And we can restore the invariant
because now the physical state and the logical state match up. So, again, that goes back
into the shared state, and the invariant
has been restored, and we got this extra
Arc out in the result. And, you know, I know this
is kind of, as I said, this proof by flying predicates. It looks a little dodgy, right? But this is actually
how the proof looks like when you do this in COC. So, I mean, it doesn’t look
like that, but it look– [LAUGHTER] It basic– in terms of the
experience as you’re, you know, executing the tactics, it
basically has a similar effect. OK, so getting back
to these axioms, so I just threw up
these axioms magically. And you should have
been very alarmed because that was
my whole complaint about these other logics,
was that they have all these complicated proof rules. I just threw up some
new proof rules. How do we know
they’re consistent? This is exactly what
Iris is designed to do, is to make proofs of consistency
of these kind of sort of example specific axioms easy. And I’m not going to go
into detail about it, but I just want to
sort of show you what the basic mechanism is. The basic mechanism
is, you know, I defined this notion of logical
state, this Arc predicate and this count predicate. Those can be actually
modeled in terms of something called a partial commutative
monoid, which you probably have heard about. This is the same
kind of model that’s used in basic separation
logic for describing heaps and disjoint composition. But basically, the idea
is that with Iris you can pick any PCM you
want for describing your notion of logical state. It doesn’t have to be
the standard heap one. And then, once
you’ve picked that, then Iris gives you
two primitive proof rules for reasoning about it. One is a rule that
lets you split up ownership of logical
state and the other one lets you update it. These are the two rules. They’re pretty simple, I
think, compared to the ones you’ve seen– that I showed earlier
that were baked in this primitive
and other logics. The first one
basically just says that if I own the
composition of two resources, that’s equivalent to separately
owning the two resources. So sort of the
monoidal composition is reflected in the separating
conjunction operation. And the other one is
something that allows me to update a resource a– ownership of a to ownership
of b if I can show that that is a frame-preserving update. Again, I’m not going to
go into detail about it. But basically it’s
just saying I can go from a to b if I
know that that’s not going to disturb any– the reasoning about ownership
of any other resources that exist in the world. And usually those
two things, then we can derive much more
complex rules, like the ones that I showed before. We showed in the
original paper how we can derive some of
these kind of rules and– yeah, for– from other logics. So wrapping up, because
I’m out of time, you know, I explain how Rust
has this sort of extensible pipe system. And in order to
make sense of that, we use the semantic
safety approach. And in order to define
these safety contracts that we use to model
interpretation of interfaces, we’re using Iris as this
kind of very flexible, logical foundation
that lets us give us sort of high-level
interpretation of these basic concepts in Rust. And, yeah, I’ll stop there. I just want to say that all
this work that I’ve talked about today is really joint work
with a lot of other people, and here’s some of them. And thank you very much. [APPLAUSE] AUDIENCE: So how
complete is Iris? Like, I mean, you could
show the math, right? How can you be sure that’s– that it will be subsequently,
it’ll be remodeled? DEREK DREYER: Oh,
I can’t prove it. [LAUGHS] I mean, well, we’ve
done a lot of– we’ve– so let’s see. We’re– go back to that picture. We’ve done it for a number of– I mean, we’ve shown how we
could adapt a number of the most advanced things. So in the original paper,
we were particularly focused on like some of the
key mechanisms of CaReSL, iCAP, and TaDA, which
were– well, as you see, they all point to Iris. Those were some of the most
recent ones at the time. I mean, there’s no way
to prove that it’s– well, first of all,
there’s two things. One is sort of showing that
it’s lo– that it’s actually complete in the
sense of you should be able to prove everything
that you could possibly want to prove. That, we could probably
prove something like that because our go state
is very flexible, but that wouldn’t really tell
you whether practically you could use it or
whether it would be practically useful as
a tool for doing that. And there’s no way
to really prove that any logic is
sort of practically useful for anything,
Formally there’s a way to prove that, right? But you– all we
can do is sort of do this for many kinds of
interesting examples or, you know, apply it to
many interesting verification problems. And we’ve done that in the case
of RustBelt. That’s something I didn’t talk about
at all, but is that, in doing the RustBelt proof,
one of the key things we did that enabled the whole
verification effort was we defined something called
a lifetime logic, which was a logic with a basic
notion of an abstract predicate describing temporary
ownership of a proposition or a temporary ownership of
some assertion for a lifetime. And this was not
a notion that we’d seen before in any prior
concurrent separation logic. It was clearly useful as a way
of giving a direct modeling of Rust’s reference types. And that logic we proved
sound in Iris using the same kind of approach. And so that was, again,
an example where we just– we had this sort of
application domain, and we were able to derive new
proof principles as needed. You know, can there– could
there be other logics that– or other kind of proofs
principles we couldn’t prove? I guess– or we couldn’t
practically prove? It’s possible, but I don’t know. ZACHARY TATLOCK: I think we
should probably stop there. But let’s thank Derek again. [APPLAUSE] DEREK DREYER: Thank you.

Leave a Reply

Your email address will not be published. Required fields are marked *