Hello, everyone. I'm Matthias. I'm in this presentation. I'm going to talk about some
bugs that I found in the betaian implementations that they were at the end relation of
the specifications. So I was starting to research these sort of bugs and trying to find
out some automatic methods to try to find the simulations of the specification. So I'm going
to talk about this method, but this is working progress. So don't speak any, I mean,
I'll speak more questions than answers I will say to you. I present this also in LPC last
year. So this is an upgrade presentation on this. So first, I would like to introduce myself.
I'm a software engineer, I'd like to enjoy working on operating systems and
utilization. I'm also trying to figure out how I can use format to prove the way that we
code. I also participate in the Mitaio comment manual is reviewing patches to the spec.
And as a reviewer, as I coach her too. So I had all the other tasks too. This is my
need to have repository. You want to check part of my work. So I think you are more or less
familiar with the built IOS specification. So I will just briefly introduce this, just for
those that they don't know it. Well, the built IOS specifications contains the specifications
of drivers and devices that are mostly used in built utilization. So in general, the devices
are implemented in the built machine monitor. And they are meant to emulate a physical device.
In other hand, the drivers are implemented in the operating systems. One, the operating
system is deployed as built machines. So what we have now is different implementation of
the drivers, like depending on the operating system. And then, for example, Linux, Windows,
and one, and then we have different implementation of the devices, depending on the built
machine monitors. So for example, for example, if I crack your in-game, and ask me a man,
leave care on each of them, implement their own version of the devices. In particular, in
this presentation, I'm going to focus to the RASBMM project. So I will give a brief introduction
about how these devices, built IOS devices are implemented in the RASBMM. So these are what
they call, we call, because user devices and implementation is mainly split into two components.
Let's say, we have the front end that is implemented in KIMU, and we have the backend that
is implemented in another process. Like, for example, in this case in the RASBMM project,
under the BIHOS user, yes, right. And these two components talk each other using the BIHOS
user protocol, which is which relies on the unique socket domain. So just to have a more
concrete idea about this, particularly implementation. So for example, when we have a driver,
and then the driver is going to trigger, they get feature command, for example, this is going
to the front end, and it's going to be translated to a message. Like, for example, the BIHOS
get feature command, and then it's going to be get by the backend. And this is using what I
highlight in red is using unit socket. And this is the controlled path, let's say, in red.
That is not only used for the message, but also the front end, as some point, is going to
share a file descriptor that then is used by the backend, which is now in blue, to map
some version of the guess memory, and then access to the build cues, for example. So we have
two paths, the control paths, and the data paths. And just to have an idea about the devices I
are going to talk later in the presentation. So coming back to the specification, as I said before,
we have different implementation with different technologies, but all have to conform to the
BIHOS specification. Not conforming to the specification, can or cannot, or may or may not
lead to a bug, right? So the idea of the presentation is to talk about two particular paths that
the first one we found in the last year, when we implemented some BIHOS sound device,
and the other one is a bug that was found from our colleague, but it's also interesting to
talk, I think. So you have the discussions in the manual list there. I'm going to give you
a brief description of what happened. The first one is regarding the live dial sound driver.
I would try to explain the picture. We have three components here, we have the driver,
and in the other side we have the device. For example, a Raspberry MM device,
and what I did in the middle was the transmission queue. So for example, it's the driver
want to play back some sound in the HOS. It's going to send data to the device and the device
went to play that, right? So the way that is done for the built-in of sound device is we have
a transmission queue, which the driver put data and then the device get it. So if we see how it is done,
how was done at that moment before we fix the problem, is that we have this function, the built-in
or send PCN message send, that is going to put buffers in the other arena of the transmission queue.
Then the device at some point is going to consume that data, so it's going to play something
in the HOS, like music or something like this, and then it's going to put the buffer in the
user arena once has been consumed. What we are in this particular driver was that when the device
has consumed the buffer, this will trigger an interruption, and then the driver is going to
immediately move the buffer from the user arena to the other arena. This is done by the built-in
IO sound PCN message complete function. This is how the driver was working at that time.
If we see in more detail how these buffers are made, well the driver creates a M vibration
that it shares with the user. This is split in smaller buffers, and then it used these buffers
to fill the script arena, and then it used the other arena to expose those buffers to the
device that is going to be consumed. In this picture in particular, we can imagine that the device
at this moment is consuming the buffer number zero, just to illustrate. And one thing that I
forgot to mention was that when the use of application wants to know where it is, where it can
bright some data is going to trigger the built-in IO sound PCN pointer, IO CTLs to get exactly
where to bright the next chunk, it is going to be reproduced. But the problem that we found was that
in this picture, now it is like the continuation of the previous picture, I mentioned that before,
we have the device consumed the buffer number zero, and then in the next steps, it is consumed
the buffer number one, we can think like this, but then at some point the user is going to
query this position, and it is going to start to fill again the buffer number zero to put some
data. But the problem was that at this point, the buffer was already in the other arena,
and means that it was already exposed to the device. What we know from the specification is that
in the moment that the buffer is exposed to the device, the device could take it at any moment,
and this is what happened before. When we were building the device, we were reading the data immediately
when the data was exposed, and what happened is that if you read in that moment, you're going to
get all data because at that point the user didn't read them right, yet this value has been already
exposed, so this is a violation of this, but we found that this is a violation of the specification,
and we fixed it actually. So if we see the traces to try to identify what was going on,
this is a made up trace, so you're not going to find these sort of traces, I did in myself.
So what you see here is that we see the driver put in buffers in the other arena,
and then at some point the user query some position, and it starts to fill the buffer number one,
for example, and then at some point the device consumed. What I try to illustrate in this trace is that
this behavior, this sequence is not valid. In the sense that once the buffer, like the number one,
is exposed to the device, you cannot write it, so this is wrong. I mean, what made me think is that
if I could identify the sequence that is delayed in the specification, I could early know
that something wrong was going on. I don't have water on me. So the second bug I want to talk about
is about the because user crate, in which there is also a relation of the specification.
Well, in this case, what we find out was that when the built-in test driver was initiated,
for example, after the driver okay, common, it's going to end you request to the to the built
queue, right? It's just immediately after the driver okay, common. The driver okay,
common is part of the initialization of the device. So it's happened at the end, and after that,
the specification tells us that you're going to start filling requests, just at that moment.
This is the driver okay, common is then translated to the because user said,
veering enable, for example, and I will mean I will talk about that later.
So this man says in particular, tell the device, well, we got the driver okay,
enable the built queue. So from now, you can't set requests, it's saying something like this.
But what happened was that this man such was asynchronous. So the guess was not getting any,
I mean, the guess was not waiting to finish, sorry, the device was not waiting to respond this one,
and the guess was just moving to the to start into an queue request.
So the situation that we have was that, for example, since this man such was asynchronous,
we got the notification that someday that was in the build queue before this one.
And then the device say, well, we did an an aven, the veering, we cannot accept the, the,
the request and then the driver hand waiting for that.
And the fix was just to add that moment, the fix was just to fill out that the man such was asynchronous
and just making synchronous. So we stop here, the driver to move. We got some,
we know that the driver okay, common was successful and then we start to thank you.
And that was the fix at the end. Thank you.
So again, this is a violation of the specification.
And if we see again the traces, we can, we can say that this is an invalid trace,
because we have first the request to the, let's imagine that this is a request to the build queue,
and this is the end, the driver, okay, common. So this is an invalid trace,
because this is happened before all this. And this is a valid trace, because the request can arrive only
if after those common has been successful. So this is the, I mean, it shows to fill out what
was going on, could be handled to have the valid trace. So yeah, well, and since I have
observating that there were some traces that there were, not conforming the spec,
I started to play with two tools to try to figure out from this implementations.
When we have implement, I mean, when we come on something in implementation and this
building the spec. So I started to play with Kenny, and then another tool time, just tracing
formal, which Kenny is a tool that he has been made by Amazon, and it is a commonly used
in firecracker. So what I started to do in the last six months or less, is try to see what they
have been doing. So they have an implementation of your tire. I'm moving that to the Rust BMM
crate, and so I'm going to talk about this this tool now, and I have to know that I still
not super familiar with the tools I'm still learning, and yeah, so I have also many questions.
The second tool which is tracing formal is to instrument trace, instrument traces in the code,
but not only instrument in the traces, but also tailing when this trace has to happen.
So we don't now, we don't have only trace points. I'm going to show that later, but since I
have to minute I'm talking more, but not only the trace points, but also how this trace points
have to happen. So first I would like to talk about Kenny, and then I would talk about trace point,
about tracing format. So Kenny, what we specify together with the implementation is a proof.
In this particular, this is an example in which I try to bribe a proof of the
notification suppression mechanism that is already in the specification. So I take the specification
and try to bribe this proof, and then what I try to test is our implementation of beer cues.
Something what I highlighted in the code, this is a draft anyway, but I highlighted in the code,
that is different to a unit testing. What you do is you use the Kenny any type to say,
I will feed my proof with any potential value of my beer cue. So the idea is that you check
for all the possible instance of a beer cue, let's say. And then if they prove pass it,
you are sure that no value exists, that will violate the specification.
And if you want to see more about this, I create a PR to the BMB tile project in which I add in this
proof to the code. So you want to see the discussion there, feel free. It's still a draft,
because I miss in some stuff, but yeah, it's ongoing, ongoing work. Something interested
I found was, well, maybe it is not interested, but it was for me, at least, if you see the
implementation of the need notification method, we will find something like this in the code.
And at some point, you may be tested, attempted to try to simplify the expression to something
like this, for example, which is wrong. By using Kenny, you can quickly spot this problem,
and then Kenny is going to tell you exactly what is the unit test that is going to fail for that case.
So it's quite interesting. It takes some time sometimes, but it's interesting too.
And the second tool that I want to mention, which I tried to use also for chat conformity,
is the tracing format, which is completely different, and I something that I made myself rely on
the tracing instrumentation that the drafts have. So for example, remember that I was talking about
this setbearing enabled at hand and FM back in the Beehos crate. Well, if I want to spot when
this relation happened, I can first, for example, set some event in the definition of the functions.
So you use event here. And for example, I say, well, here is the setbearing enabled. I set up
event type, and here I change the name for sure. I can also not only set up this sort of
FM, but I can't do it in the, I didn't need that slide, but you can also use instruments here.
And the event is going to be triggered, each time the function is called it. So you don't need to
put this manually, you can do it systematically in each definition of the function, for example.
And so once you set up this, then you have to tell the tracer, when, when, which sequence is
going to trigger a warning, right? So what you do is, you do something like this. Well, here is maybe
because I'd be tricky, let's say. You could use, for example, stay machine and say, well,
the set, some sequence, some equivalency of these two events are going to trigger a warning,
or something like this. I use another formalist for that. And what I, the thing I want to say here
is that, together with the instantiation of the, of the tracer, you fill it with, you fill it with
the relationship between the events. So here, for example, you have,
with this, yes, the alternate vector, which is going here when you instantiate the tracer.
So you, you have the tracer, and you have also together for a specification that tells you
when this event can happen. This relationship between the two events is something that comes
from the specification, the specification is telling us when that could happen.
And then what happened is when this efficacy acute, if, for example, the handle event happened
before they said the ringing able, this is going to trigger the warning in the equation.
So maybe at that point we can think, maybe this is something wrong.
I think that's all from my side. I don't know if you have any questions.
This is a still an experimental word, and I'm working on the PR too. So yeah,
it's not really clear for me yet, it's the tracer informal, it's going to be useful.
I mean, I find interesting to play with, but then if it is useful, the other thing, but yeah,
I don't know if you have any questions.
Yes, I mean, the question was if I have another example in which I use the tracing format,
which seems useful, no, I don't.
I mean, I'm having playing with something similar, but the tracing the kernel, I don't know if you
heard about that, it is called the room time observator or room time verification something
that they already are in activity in the kernel, and people that are doing well at the same
with the same machine, but in the kernel. Well, maybe you know Daniel have been working on that,
but yeah, you can check that also, I think they are examples there.
The question was if I already found any bug in the specification itself, that was a question, right?
Well, I am reviewing the spec, for example, I have a re-invirtiocan device.
I don't know if it was a bug, but what you find is that what the outer want to say is not what
the people implement, for example. So, I mean, the fact that it is in English, and it's not always
a precise language made that there is no bug, but it's not even a precise tool. So, you know,
but no, I can, I can not remember now a precise bug now, but this is something related that will
sell. Yeah, thank you.