>> Hello. Welcome to
Bridging the Verifiability Gap: Why we
need more from our specs and how we can get it.
My name is Jordan Halterman.
I'm a member of the Technical Staff at
the Open Networking Foundation
where I focus on distributed systems.
First, a brief overview of the talk.
First, I'll talk a little bit about distributed systems at
ONF and then talk about what I'm calling the verifiability gap.
Then I'll talk about a couple of the approaches that we take
to overcoming this verifiability gap,
model-based trace checking and model-based conformance monitoring.
Then finally, a little bit about what we learned along the way.
Distributed systems at ONF.
The Open Networking Foundation is an industry funded
open source non-profit foundation.
We're dedicated to bringing
software defined networking technology to production in
the industry from research.
ONF has a small engineering staff,
which is where I come from that works on
a pretty large variety of really ambitious open source projects.
The project that I work on in particular or
that I was originally hired to work on,
is a project called ONOS.
ONOS is an open source software defined network controller.
It was the first project created at ONF,
and it was eventually brought into
production a few years back at Comcast.
What is a software defined network controller?
The whole idea of software defined networking is to
take network control out
of proprietary hardware into a software layer.
In a network, when you have a number of hardware switches,
ONOS sits above the switches and
controls switches to do things like packet forwarding,
device configuration management and things like that.
ONOS actually does this with several nodes,
so it's actually a distributed system.
ONOS nodes communicate with each other
and they do so for scale and fault tolerance and things like that.
Within the ONOS cluster,
we run a bunch of different types of protocols like gossip,
failure detection, consensus protocols,
sharding, primary backup and things like that.
ONOS actually is a pretty large and complex distributed system.
That brings me to our use of
TLA+ and what I'm calling the verifiability gap.
In 2018, we began field trials of ONOS to bring it
into production at Comcast.
During this process, we've learned a lot of stuff.
Production scale testing exposed a lot of bugs that
we realize had been dormant in our system for years,
but we had just never seen because we'd never
tested it in quite the right way.
I personally spent hours and often days scanning
gigabytes size logs to try to
understand traces and track down
specific distributed systems bugs.
But after lots and lots of this work,
ONOS was eventually deployed nationwide at Comcast network.
TLA+ was an important part of that process.
During that process, we use TLA+
to design new distributed systems protocols,
improve existing protocols and some examples
of types of work that we did with TLA+,
were we used it to extend the raft consensus protocol,
used it to build new distributed locking algorithms,
design custom primary backup protocols,
and we've even used it for some research using
software-defined networking techniques to
build new consensus protocols.
TLA+ was really critical in helping to validate
solutions for a lot of bugs but we
felt it could have been more effective if we'd been able
to use it in the initial design of the system.
Fortunately for us in 2018,
the ONOS team began rewriting ONOS.
Since the ONOS project had begun,
we'd seen the rise of the Cloud and projects like Kubernetes,
and so we wanted to rewrite ONOS,
and so what this represented for me was opportunity.
The opportunity was to try to rethink how we
were designing and developing distributed systems in ONOS.
When we began rewriting ONOS,
we did so with a focus on testing and
debugging infrastructure with the goal
of answering a couple of questions.
One was, how can we reduce the number of bugs in the system?
The other was, how can we make
debugging for bugs that do arise easier?
The solution for us was a new commitment to TLA+ as well.
From the start we began using TLA+ to
design parts of the new ONOS system.
We use it to document and verify the algorithms that we're using,
and hoping that the specs that we wrote would provide
a foundation for experimenting with enhancements in the future.
So far in rewriting ONOS,
we've used TLA+ to design new leader election algorithms,
verify control loop logic,
design distributed caches and more.
But the problem that we ran into was,
now we're using TLA+ for all this stuff,
and so even if we know algorithms are correct,
how do we know the code is correct?
This is the verifiability gap that I am talking about.
What would our ideal solution to this gap look like?
Well, when we design a new algorithm with
TLA+ and verify the algorithm with TLC,
we thought we should be able to then implement
the algorithm with whatever the language of our choice.
After doing so, we should be able to verify
the implementation using our TLA+ spec,
and when bugs arise,
debug the implementation using the TLA+ spec,
which contains everything that
we should need to be able to do that.
Why do that with TLA+ though?
Well, our algorithms are already specified in TLA+,
and so using an alternative tool to do this would present
the same problem as writing
the implementation does in so far as trying to make
sure that the implementation
maintains consistency with the TLA+ spec.
Being able to use TLA+ to verify the implementation could also
help encourage engineers to
use TLA+ to design new algorithms as well.
We set out to explore some ways that we can close this gap
and the first thing we looked at was model-based trace checking.
The idea of model-based trace checking is
that we would be able to run our application,
log application traces in a structured format like JSON,
consume that structure format into a TLA plus model,
change the state and verify some invariants,
so check that the actual implementation
adheres to those invariants.
To do this we actually built our own test framework.
We have this test framework for testing Helm charts in Kubernetes.
We have a test command that basically
deploys a test coordinator inside Kubernetes.
Kubernetes is a container orchestration platform,
so it's a distributed system for running
distributed systems it's not incredibly important here.
But we deploy our tests coordinator,
our coordinator deploys our distributed systems like Raft, ONOS.
Then run some test,
it tells those distributed systems to do things.
They interact with each other
and then finally eventually they send
logs back to the coordinator where they
get aggregated and sent back to the client.
This is where we can run TLC to do trace checking with TLA plus.
This is what an example spec looks like to do trace checking.
You see that we imported this module called trace.
The trace module is basically what reads
traces from some structured format like JSON.
You see in the next state relation,
we're basically reading a next structured trace
and then doing something with it.
In this case we're testing a distributed cache.
We basically read a trace record it
in a history variable and then there's
an invariant that basically it's
checking that a client never sees history go back in time.
This seem to work really great for
a client-centric consistency model like this,
where we're basically checking that the client is seeing
some specific behavior and
more importantly not seeing some other behavior.
But it still wasn't obvious how to ensure that
the code correctly implements
every single step of the spec internally.
This feels like it depends on our ability to trigger bugs
and we're not really too competent that
because as our production experience showed,
we see a lot of bugs in production
that we seem to be unable to
trigger ourselves in testing environments.
We'd really like to be able to detect bugs when they happen,
rather than relying on our ability to make them occur.
That brings us to the second approach we took
to verifying our implementations,
which is model-based conformance monitoring.
The idea of conformance monitoring
is it's very similar to trace checking,
except we're doing it in real time so
that we can try to catch those bugs that happen in production.
The idea is just that the application
logs traces to the stream instead of
just to some file that's later processed in batch.
Again, the TLC process consumes the traces from the stream,
updates the model state,
checks invariants and with an added feature of being able to
alert when an invariant is violated since
we're processing in an infinite stream of traces.
To do this, we actually updated
our test infrastructure and we added a system called Kafka.
Kafka is the system that ONOS now writes its traces to.
A Kafka, it's actually a distributed fault tolerant log,
which in this architecture acts as a buffer for
the traces coming out of ONOS and then
going into the model checker.
Then the model checker runs on the other side of Kafka.
There's a model input to it, it reads streams,
it reads traces as fast as it can
while the other side writes traces as fast as it can.
Then TLC does this thing,
which it does great, and this is
what the conformance monitoring spec looks like.
For the same distributed caching algorithm,
let's look at it up close.
There are just a couple of differences.
We're again, tracking the offset.
In this case the offset is basically an offset in Kafka.
We've added this trace operator.
What the trace operator does is given an offset,
it basically either if the offset
is available in Kafka in the buffer, it will read it.
Otherwise it will block and wait for
the next trace to become available so it can evaluate it.
Again, we're just checking the same invariants,
basically verifying that the history will not go back in time,
but in this case, we've also added an alert operator.
The alert operator basically says,
when this invariant is violated,
we can write a message back to Kafka so it can go to
some monitoring system or some other place like that.
There are some challenges with this
that we are still working to try to overcome.
One is it's really difficult to figure out how to
limit the size of the trace in an infinite stream.
If we want to be able to,
when an invariant is violated,
identify the trace that led to it,
we're basically dealing with an infinite trace,
which becomes very difficult to figure out how to handle.
Then there are obviously ordering issues in a distributed system.
Our test model was easy to work with because
it didn't require some order across processes.
Basically, we're just establishing that the history
is ordered within some single-process,
but it becomes a much bigger problem
when you need to order across processes.
Obviously, one way you'd have to do that is perhaps rely on
timestamps for ordering across processes which isn't always ideal.
But maybe it's okay for a model checking or
for basically a monitoring system like this.
Again, it feels like it works best for
a client-centric consistency model like the one in our example.
But there may be some ways to improve it
so you can do ordering across processes.
Things like clock synchronization protocols are getting much
more accurate and they could be really useful in this context.
But you'd still need a sorting step,
which it just complicates the architecture,
but it seems like it could be possible.
That finally brings me to what we learned along the way.
I think what we learned is that it's
generally possible to use TLA plus to
check traces and we're fond of the approach.
But like I've said a couple of times,
it seems to be easier to test
local invariance than global invariance,
which might have to do with ordering
issues across multiple processes.
But unfortunately, we weren't really able to
do something like trace checking using our original specs,
which was our dream to build or
write a spec and then be able to use it to verify some system,
but it still require some modification.
But the modularity of TLA plus
does allow for specs to share logic.
So you can actually organize
specs in a way where this can be done cleanly,
where you have both the portion of the spec that you use
for original model checking and then
another module that you use for trace checking.
But we still see significant value
in trace checking with TLA plus,
I think we've had a lot of success in using it
the way that we use it in our examples here.
I think we will continue to do that to
verify things like API guarantees inside of ONOS.
But we still haven't really figured
out how to use it to verify internal implementations.
So maybe other approaches like
test case generation and things like
that are better in this respect.
But by making it part of our infrastructure,
which we are still going to do,
we hope to be able
to use it to detect bugs before they're seen in production.
Then we hope to learn to be able to use it
to reduce the efforts required to debug systems.
That experience will help us find
new ways to generalize this approach and make it more usable.