Okay. Thank you. Yes. I'll talk about linear verification of Linux kernel code. So I'll start
out with what is program verification. Program verification involves the source code and some
specification of what the source code is supposed to do. And then we are goal is to be sure that
the specification describes what the source code actually does. So ideally this tracking
should be done automatically. So here's a simple example. This was presented in the Linux
loop conference a couple years ago. Here we have the swap function extremely simple function.
So what we would like to know about this function. So we might need to think about what the
function does a little bit. It takes two arguments. Those two arguments are pointers. And the
ideas we want to swap the values that are referenced by those two pointers. So clearly we have to
be able to do reference those pointers. And we have to be able to write new values back into
them. So then those are our requirements on the inputs. And the goal for the function
should actually do is that the values at those two places should be interchanged. So then we
want to consider it. So that's kind of a high level English language specification of what
should happen. What we would like to have is some kind of formal representation that we can
drop into some tool that will be checked. So the first property is that the two pointers
are readable and rightable. So we use the notation of pharmacy, which is a tool for
checking properties of C code. So basically we need to require that two input parameters
the pointers are valid, meaning that we can be referenced them. And we can also write
to the memory that is referenced by those pointers. And the next one is that we want that
the final value of P is pointed to by P should be the original value of Q. So we can express
that by saying ensures that means a requirement on the output that the final difference
of the pointer P is equivalent to the original value that was the reference by Q. And
similarly we want the final Q value to be the same as the P value. So the final value
this D reference by Q should be the original value of this D reference by P. So so far things
seem fairly simple. Now we put all this into a comment that is before the source code. We get
a single file and now we can drop this into the pharmacy tool. And in a few seconds it tells
that all the goals were proved. And so now we have confidence that our swap function is doing
what it's supposed to or at least what the specifications that we wrote said it is supposed
to do. So the question is, I mean swap functions very nice, but pretty simple we probably
have some confidence that works. So we want to, the question we want to ask is could we do
this for the Linux kernel? So this kind of an ongoing discussion about like requirements
and documentation and how can we improve somehow the correctness and understandability
of Linux kernel source code. So this sits somewhere in that space. Probably maybe the
biggest question we ask is like, do we want to do this for the entire Linux kernel, little
parts of it, very important parts of it parts that we don't understand that's all very
open questions. So the positive aspects of writing these specifications in checking these specifications
just thinking about the specification should be can lead you to find bugs. So later on in this
talk I will describe some experiments that we've done and in several of these experiments
just in doing writing the specifications in checking then we have actually found some bugs that
have been submitted to Linux kernel and accepted or maybe found some potential bugs that were
an old code that doesn't exist anymore and so on. So writing specifications means you
have to somehow think pervasively thoroughly about what your code does. It's kind of a different
point of view than when you're just trying to run it and so on but do some test or something
and so it can highlight some issues. The specifications also provide an ambiguous notation
for what the function is supposed to do. If you write out something in English you may have
some, the person who writes them has their intended meaning of the English words, the person who
reads them might understand something different. There's lots of things you can write
in English, there's somehow like friendly English language that are kind of open to
misinterpretation afterwards. So if you write out things in a more formal way there's perhaps
less confusion and the specifications if they're written out in a formal way can be checked
mechanically against the source code and that can happen also over time if you make
some changes to your function, maybe you just make some refactoring to your function, you
expect it doesn't change anything at all so then your specifications might still continue
to work or you might make some small changes and then maybe your specifications will need
adjustment but you still have some kind of control, some kind of insurance that what the
function was doing before is still what it's going to be doing. On the other hand, on the
side creating these specifications is hard, we're not going to create any more specifications
but you'll see them and they're quite big and complex and then the question is I
mean I just argued that maybe this whole specification idea is useful as the code changes
but still in general can we really hope to maintain these things over time, developers are
already more interested in improving their code, they don't really want to improve this
kind of mysterious formal language and of course there's no magic bullet if you're a
specifications say the wrong thing then you'll be checking that your code does the wrong thing
you won't really have advanced things very much. There's in practice I think some kind of
check on that in that if you write bad specifications it won't match your code and then you'll
kind of be forced to iterate until when they match up you might be closer to reality but there's
always the risk that specifications are wrong and you ensure that your code does the wrong thing.
So so far we have done three experiments one of them is the function should we balance
it's part of the Linux kernel schedule there's load balancer select idle core it's a function
that is used when task wakes up and you want to figure out where to place it on the machine
and F trace event enable the stable this is part of the event tracing infrastructure.
So somebody might argue that maybe load balancing and task scheduling are really core
aspects of operating system kernel maybe the code for enabling this enabling tracing is not really all that
important but actually the third case we picked it because some human actually wrote specifications
in natural language and so it was the opportunity to compare them.
So start with should we balance load balancing the idea of load balancing is we have perhaps
we have some CPU it would like to take on some more work maybe because it's idle maybe
because it just has not enough stuff to do and what easy to do is search across the entire
machine or in general across some set of CPUs to see if there's some other work that's available that
it can steal. So this is beneficial because you'll get more work done more fast but it takes time
because it takes time because we have to look at all those different CPUs look at their data structures
maybe count some things and so on. And so what we want to do is just let the first CPU do the
stealing and not all of them at the same time. So should we balance this sort of a gatekeeper
that each CPU says should I balance should we balance and then sometimes it will turn true
yes you'll get to do load balancing sometimes it doesn't. Here is the a recent version of the
function it's not a huge function it's not a small function it's just what it is.
The most interesting part of it is this loop in the middle. This loop is quite interesting for
reasons it has this for each CPU and thing so that's like a special purpose it's like a
for loop but actually it's iterating over a mask of CPU so you can think of it as sort
of a set of CPUs but it's actually implemented as a bit mask and it's going to go through
the mask and see which CPUs are under consideration and then do the loop body only for those
CPUs. So that's fairly easy to understand then the more frightening thing about this loop is
here in the middle we have the CPU and mask and mask and not and this is a side effecting
operation what basically what this is doing is removing some CPUs from the set that we're
iterating over. So this makes it harder to it reason about what the thing is doing because it's not just going
from zero to 10 it's like going over a changing set of things. So here are the specifications
this is much more intimidating than the ones for that we had for the swap function.
Basically we have a bunch of issues that we want to consider for example is there any
idle CPU are we the first idle CPU are there no idle CPUs are there some other things like
maybe the CPU's actually been hot unplugged and so we obviously don't want to still work for that.
So there's various issues that are taken into account and then we have the specifications that
should be respected in each of those cases. So these are what are called the pre-imposed conditions
under what circumstances the function could should be called and what behavior should
happen if we call it in those cases. We also if you're familiar with verification at all you
know you have to write loop invariants a loop invariant is dealing with the issue that we actually
this is all happening before one time so we have no idea how many times the loop is going to iterate.
So we need some human to provide information about some property that is going to hold no matter how many times the loop occurs.
So this is a whole other pile of loop invariants that we need to take into account.
So what we are interested in this particular experiment is how to think how does the code change over time and what are the impact on the specifications.
And actually so this function has changed basically ten times and the last ten years that it has existed.
So the beginning part of this experiment was very positive.
The changes were things like the first ones to fix a bug by changing not equal to equal.
Then there were some refacturings, some changing names, some realization that this function is not necessary so we can use some other function instead.
And all of those changes were very simple and either they had no impact on the specifications or they had only a very minor impact on the specifications of few lines had to change.
And you can see that actually the verification time is also reasonably fast and doesn't change very much.
But then here in the last in 2023 the things kind of go more like this.
This is where they had someone had the idea of adding in this optimization of throwing out CPUs that we don't actually have to look at again.
So then that makes the whole analysis of the iterations more complicated because we have to take into account that things have disappeared along the way.
The first change was to actually this change here is preferring before it was just like is the CPU itself idle at this point in number eight.
We don't actually change the set but we have an extra loop in the middle which is going to check all the hyper threads.
So it's not very desirable if you have a CPU but it's hyper thread is busy that's not really the ideal place to put new work because this course actually doing work quality.
So we prefer fully idle course so that adds an extra loop in the middle and that adds about 10 seconds 12 seconds to the verification time.
And then here at this point we add the optimization that if we have checked all the hyper threads we and we find out what the one of them is not idle we don't need to check them again.
So this this causes a increase in the verification time it causes a lot of added complexity in the specifications it took us a long time to figure out what the specification should actually be.
But you notice that these cases here are in red and that this case here is actually in a release to releases a Linux kernel and what that means is actually the person adding this optimization introduced the bug.
So it's there was some benefit to sitting there and thinking about these specifications and thinking about what the function is really doing because we actually found a bug that was in a release.
Another issue we have here is that these are the specifications this are the proving times that we have now when we originally did this work we had proving times there were much much higher especially for the complicated cases.
And then we invited someone who works on pharmacy to come and help us to do it better so choose we found that choosing the right representations of certain things is very important.
It's kind of an impracticality if you have to actually bring in a person who maintains the tool to figure out how to do it maybe there can be some kind of.
Some kind of libraries of good representations so on.
So the next one case I will go for much more quickly this is select idle core this is the function that places pass on idle core here we have again the same looping property.
We want to iterate over a bunch of CPUs and we have again the property of updating the set of CPUs that we are working on at the same time.
This is a looping function iterating function this more complex than the previous one the previous one started is zero and went to the end this one starts at the middle goes to the end and wraps around and works on the beginning.
So you have whole extra set of specifications saying we're up here in this region we're up here in this region or we reach the end.
So it just kind of adds more work.
Here what we found was very helpful was to introduce some macros that what hide some complexity.
These are, if I'm citing one of them is figuring out exactly what are the CPUs we can consider one of them is just hiding this for all this quantifier stuff.
You do this stuff over and over again it's not very intellectually it doesn't contribute much but it takes up a lot of space and it makes it very hard to figure out what is going wrong when things go wrong.
So the last function we consider is this F-trace one this code is much more complex but you can consider maybe you know maybe it should be easy because actually if you look at this carefully what we see are lots of ifs which very different kinds of if but there's actually no loops so we have no loop and variance to figure out.
So that should be good on the other hand these ifs all lead to assignments of different variables things data structures and so on and then there's a very scary place here where we have if and it depends this if here depends on variables that we have updated along the way which makes proving specifying everything much more complicated.
But then the question is I'm this is a very complex function how what kind of specifications do we want so the first attempt was just to thread through every single path through the function figure out what what things it tests and figure out what things it updates so we get as this is just a small extract of the specification this is just one particular case and then we ended up with.
More than 350 lines of specification this function is doing enabling the atracing and disabling this only for the disabling part 350 lines is completely unenlightening.
We also discovered that pharmacy is not very good at this bit masks which the original implementation used extensively so this is somehow not very good.
As I mentioned I chose this because some human had written some specifications and so this is what the specification is a little extract of what the specification looks like.
If we have this variable we do this and this and this and so on.
So obviously they I mean this is these are perhaps understandable to humans other users the other developers but there's not checkable it's not complete and it's actually not entirely correct either.
So so but we took those specifications and wrote them out in the formal notation and we end up with something that's much simpler than what I showed previously.
But on the other hand it's I mean it's only this is half of a disabled case it's only 25 lines instead of 250 lines so that's pretty good.
On the other hand it's still not completed it's based on something that's not complete we're not gonna end up with something complete on the other hand it has been checked so we filled in we figured out what was going wrong and added the extra cases so actually in new way it's everything that's important.
On the other hand it's not very satisfying it seems like we just have some random information about some random variables we don't have kind of somehow some kind of complete definition of what's going on.
So in the third case we I thought about like think about each variable and think about all of the things that affect that variable and put them together in a particular place and so somebody wants to understand a particular variable then they have something specific they can use.
And we can also use pharmacy to check that everything what we describe is complete and they're all disjoint from each other so we have some confidence that we're doing some reasonable thing.
And then the last thing I started thinking about is okay all of those things we've seen before describe what the function does but it doesn't describe what is the impact for the users so we also want to have a bunch of function calls and they should be able to interface with each other and maintain some invariance over time.
So in conclusion what did we learn from should we balance that we can easily maintain things over time select at a core we learned that abstraction is important.
And from last one we learned that really specifications need to give insight could users about how they should use the functions what functions they should do and so on.
In the future we would like to do more experiments think about what of this is practical to automate so far everything has been written by hand and what is the trade-off between understandability and maintainability and correctness.
So thank you.