►
Description
Rust guarantees zero memory access bug once a program compiles. However, one can still introduce logical bugs in the implementation.
In this talk, I will first give a high level overview on common formal verification methods used in distributed system designs and implementations. Then I will talk about our experiences with using TLA+ and Stateright to formally model delta-rs' multi-writer S3 backend implementation. The end result of combining both Rust and formal verification is we end up with an efficient native Delta Lake implementation that is both memory safe and logical bug free!
Connect with us:
Website: https://databricks.com
Facebook: https://www.facebook.com/databricksinc
Twitter: https://twitter.com/databricks
LinkedIn: https://www.linkedin.com/company/data...
Instagram: https://www.instagram.com/databricksinc/
A
A
So
I
highly
recommend
you
attend,
and
obviously
I
also
work
on
delta
rs,
which
is
what
this
talk
will
be
mostly
focused
on.
So
what
is
delta
rs
on
the
quick
high
level?
It
is
a
full
data
lake
implementation
in
rust
and
the
main
use
case
for
it
is
being
able
to
easily
access,
read
and
write
access
delta
tables
without
having
a
hard
dependency
on
jvms
and
spark.
A
A
So
this
is
what
a
traditional
data
warehouse
looks
like
you,
basically
just
have
a
bunch
of
product
files
living
in
a
directory
on
a
remote
blob
storage
and
what
data
link
adds
to
the
top
is
a
bunch
of
json
files
which
might
not
sound
exciting.
But
basically,
each
json
file
represents
a
single
commit
to
the
table,
and
within
that
json
file
you
will
have
a
bunch.
A
You
will
define
a
bunch
of
actions
and
all
of
these
actions
will
be
considered
as
atomically
applied
to
the
table
right
so
and
the
json
file
itself
is
named
with
the
numeric
value,
which
represents
the
version
of
the
table
that
you're
committing
to.
So.
In
this
particular
example,
we
have
a
json
file.
That
includes
three
add
actions.
Each
of
them
point
to
it
three
different
product
files
that
contains
the
actual
data
that
you
want
to
write
to
this
table.
A
So
let's
say:
if
I
want
to
remove
product
c
and
add
a
actual
product
d
file
to
the
table,
all
you
have
to
do
is
create
another
commit
to
the
table
through
a
json
file
and
within
this
json
file
you
can
include
two
actions.
The
first
is
the
remove
action
that
will
point
to
park
ac
and
then
the
other
one
is
the
add
action
that
will
point
to
proc
id
and
if,
as
the
reader
of
this
table,
if
you
apply
these
transaction
logs
in
the
correct
order,
you
will
get
a
correct
state
of
the
table.
A
In
this
case,
the
table
will
only
contain
part
k
a
b
and
d
files.
So
this
is
how
delta
lake
works
at
a
really
high
level.
I
skipped
a
lot
of
technical
details,
but
for
the
sake
of
time,
but
this
should
be
enough
for
you
to
understand
what
I
will
cover
for
the
rest
of
the
talk.
So
one
of
the
problem
that
you
run
into
with
this
design
is
what,
if
you
have
multiple
writers,
that's
performing
a
right
commit
to
the
same
table
with
the
same
version.
A
Now,
if
we
don't
do
anything
special,
let's
say:
if
we
have
three
writers,
they
will
actually
overwrite
each
other's
commit
and
we
only
one
of
them
will
actually
go
through
and
then
we'll
result
in
a
data
loss.
So
the
way
that
this
is
handled
in
upstream
data
lake
is
we
adopt
a
strategy,
call
called
optimistic,
concurrency
control.
What
this
does
is
each
writer
will
use
a
leverage,
a
different
put
method
called
put
if
absent.
This
is
something
that's
supported
by
most
of
the
blob
storage
systems
and
what
this
guarantees
is.
A
It
will
perform
two
operations
in
atomic
click.
The
first
operation
is,
it
will
check
whether
the
destination
file
already
exists.
If
it
doesn't
exist,
then
the
right
operation
will
go
through
without
any
error,
and
if
the
destination
file
already
exists,
it
will
actually
return
an
error
back
to
the
client.
So
in
in
this
case,
let's
say
we
have
three
writers:
all
of
them
are
using
pull
if
absence
right.
A
Only
one
of
them
will
actually
go
through
and
the
other
two
will
get
back
to
the
air.
So
each
rider
will
increment
the
version
locally
and
try
it
again
so
again,
because
we
have
two
writers,
one
of
them
only
one
of
them
will
go
through
and
the
other
other
one
will
get
an
error
back
and
then
eventually
the
last
rider
will
increment
to
version
three
and
then
all
of
the
rights
will
go
through
and
in
with
this
approach
we
won't
have
any
data
corruptions.
A
So
it
is
called
up
optimistic,
concurrency
control
because
each
rider
when
they
perform
the
right,
they
optimistically
think
that
they
were
the
only
writer.
That's
performing
it
right.
So
this
works
pretty
well
for
workloads
that
does
not
have
really
high
concurrence
right
to
a
data
source,
so
it
looks
all
really
straightforward
and
to
implement,
but
there
is
only
one
catch
with
which
is
we
are
using
s3,
so
s3
is
actually
one
of
the
only
major
blob
storage
that
does
not
support
the
semantic
out
of
the
box.
A
So
when
we
were
thinking
about
this
design,
there
are
many
two
directions.
The
first
direction
is
to
leverage
dynamodb,
which
provides
a
conditional
write
semantic
and
we
can
basically
use
dynamodb
to
store
this
station
file
commit
right.
So
as
a
reader,
what
you
do
would
do
is
you
will
read
the
dynamodb
table
to
get
the
list
of
commits,
apply
them
to
get
the
current
state
of
the
table,
and
then
you
reach
out
to
s3
to
find
to
read
the
product
files
that
contains
the
actual
data.
A
This
is
easy
to
implement
right
because
we
get
this
prolife
absence
operations
for
free
from
dynamodb,
but
the
problem
with
this
approach
is
it's
not
compatible
with
the
rest
of
the
pipeline,
so
all
of
your
downstream
pipeline
has
to
adopt
the
exact
same
design.
They
will
have
to
read
through
the
dynamodb
first
to
get
access
to
the
commit
log
before
they
can
read
the
actual
data
file.
A
So
this
won't
work
for
us
our
use
case,
because
majority
of
our
pipelines
are
still
running
in
databrick
spark
and
they
don't
allow
us
to
replace
the
delta
lake
log
implementation.
So
we
have
to
keep
using
the
databricks
data
lake
implementation,
which
only
reads
the
commit,
commit
log
files
from
s3.
So
we
ended
up
going
with
the
second
approach,
which
is
to
leverage
dynamodb
to
implement
this
pull,
if
absence
semantic
on
top
of
s3.
So
the
benefit
benefit
of
this
design.
A
A
The
idea
being
this
is
if
the
writer
crashed,
while
holding
the
lock,
the
lock,
will
eventually
expire
and
then
other
riders
will
be
able
to
acquire
the
same
log
and
then
keep
making
progress.
Well
turns
out
that
this
is
also
not
going
to
work
because
expirable
distributed
log
is
a
scam
and
by
scam.
A
I
really
mean
that,
if
you're
using
a
distributed
log
that
has
an
expiring
date
set
to
it,
you
are
basically
providing
zero
guarantee
to
the
critical
region,
and
so
it's
actually
not
giving
you
any
extra
safety
guarantees
so
to
demonstrate
how
this
could
go
right
go
go
wrong.
Here's
the
example.
Let's
say
if
one
the
rider
holds
the
lock
and
it
paused
for
whatever
reason
so
in
distributed
system
processes,
processes
can
pause
for
arbitrary
loan
of
time.
Due
to
many
different
reasons.
A
Maybe
another
process
processes
are
sharing
the
same
cpu
resource
with
you
and
or
maybe
you're
under
high
memory
pressure
and
you're
going
into
swap
mode
or
if
you
know
you
send
a
network
package
and
it
got
delayed
and
that
never
reached
the
destination.
So
when
we
are
modeling
about
distributed
systems,
we
have
to
take
this
into
account
and
in
in
this
case
let's
say
the
writer
holds
the
log
and
it
paused
for
a
long
period
of
time
and
it
until
the
log
expired.
A
So
another
writer
will
be
able
to
acquire
the
expired
log
and
the
problem
that
this
cost
is
demonstrated
in
this
timetable.
Let's
say
at
time:
zero
writer
a
acquired
the
log
at
time,
one
it
paused
for
a
long
period
of
time.
At
the
time
t
the
log
expired
and
then
at
t3
writer
b
comes
in
and
acquired.
This
expired
lock
at
t4
writer,
a
resumed.
Let's
say
you
know,
gc
was
happy
now
and
it
at
time.
A
Commit
intention
and
perform
the
exact
same
operation
on
behalf
of
the
original
owner
of
the
lock,
and
so
here's
a
timetable
of
how
this
works
in
practice.
Let's
say
time:
zero
writer,
a
acquired,
the
log
and
record
the
same
commit
intention
to
copy
uida
json
to
one.json.
So
one.json
is
the
delta
table
version
that
we're
trying
to
commit
into
and
at
time
one
writer
a
paused
for
a
long
period
of
time
and
time
t
at
time.
Two
log
expired.
A
So
when
log
writer
b
tries
to
acquire
this
lock
with
its
own
commit
intention,
in
this
case
it's
trying
to
commit
uidb.json
into
one.json
as
well.
But
then,
when
he
acquired
the
log,
it
will
notice
that
previously
we
have
another.
The
previous
owner
recorded
this
intention
to
copy
uida.json
into
one.xr,
so
it
will
actually
try
instead
of
performing
its
own
commit.
It
will
actually
try
to
finish
up
the
commit
that
was
left
by
the
writer,
a
which
was
the
original
owner
of
the
lock.
So,
let's
say
writer
a
resumed
execution
at
t5.
A
You
will
keep
doing
the
performing
the
exact
same
commit
and
it
won't
cause
any
problem,
because
we
just
copied
copying
the
exact
same
file
from
the
temporary
location
to
the
final
destination,
and
so
you
can
see
that
at
ts7
and
t8
both
of
them
will
release
the
lock.
And
lastly,
the
writer
b
will
try
to
re-acquire
the
log
with
the
newer
version
to
try
to
commit
its
own
data.
So
this
way
we
can
make
sure
that
if
a
log
is
acquired
by
a
particular
writer
that
commits
will
always
go
through.
A
So
highly
recommend
you
taking
a
look,
but
I
don't
want
to
steal
his
standard
here
and
we
all
as
a
side
project
a
product
of
this
project.
We
also
produced
a
reusable
dynamodb,
lock
in
pure
rust,
which
implemented
the
exact
same
logic
that
we
have
here,
but
it
can
be
reused
across
different
projects.
A
Big
shout
out
to
misha
for
doing
most
of
the
work
for
for
this
library,
and
so
things
work
really
well,
but
there's
something
that
always
came
back
to
me,
which
is,
I
don't
have
the
full
confidence
that
we
actually
did
everything
correctly
and
we
didn't
leave
out
any
edge
cases.
So
if
you
look
at
this
kind
of
timetables
during
the
initial
design
process,
we
actually
do
do
this
kind
of
action.
Interleaving
exercises
manually
try
to
poke
holes
in
the
design
and
see
if
we
can
break
the
system,
it's
pretty
manageable.
A
When
you
have,
you
know,
let's
say
two
actors
or
three
actors
in
the
system,
but
once
you
add
more
actors
into
the
system,
it
becomes
impossible
for
a
human
to
think
through
every
possible
state
in
a
system.
So
what
I've
been
thinking
is
what,
if,
if
there
is
a
way
for
us
to
use
automation
to
automatically
explore
all
possible
state
in
the
system
and
help
us
find
all
the
bugs
that
could
exist.
A
So
this
is
where
formal
verification
comes
in
now,
formal
verification
might
look
sound
like
a
really
daunting
word,
or
only
used
in
academia,
but
actually
we've
been
using
revocation
some
sort
of
verification
in
our
day-to-day
practice.
For
example,
if
using
a
static
type
check
language,
you
are
using
software
to
automatically
assert
properties
by
enforcing
type
constraints,
to
your
code.
If
using,
if
you're
writing
unit
test,
you
are
using
unit
test
framework
to
assert
properties
by
making
sure
that
input
matches
with
output
right.
A
These
are
all
some
form
of
revocation
that
we're
doing
today,
then
they're
considered
informal,
because
they
only
test
a
really
subset
of
the
program
behavior.
So
this
is
what
formal
verification
brings
to
the
table.
It
actually
can
exhaust
all
possible
state
of
the
program
and
make
sure
that
the
program
is
correct
in
all
circumstances.
A
So
there
are
many
two
approaches
for
formal
verification.
One
is
called
model
checking
which
is
just
simply
automatically
explore
a
possible
state
of
the
program
and
for
each
state
it
will
go
through
a
list
of
predefined
properties.
Make
sure
that
every
single
state
will
match
this
property,
and
the
other
approach
is
called
deductive
reasoning
and
what
this
approach
does.
It
is
closer
to
actually
writing
mathematical
proofs
for
a
program
in
this
particular
talk.
A
So
going
back
to
my
previous
example,
let's
say
I
have
writer
a
and
writer
b
at
t,
0
writer,
a
acquired
log
at
t1,
it
paused
for
a
long
time
at
t2,
the
log
got
expired
and
at
t3
writer
b
came
in
and
it
acquired
the
log.
So
you
can
see
that
the
end
state
state
of
this
sequence
is
writer,
a
will
be
holding
a
expired
lock
and
writer
b
will
be
also
holding
an
expired
log
right.
So
this
is
the
end
state
of
the
system.
A
What
you
can
do
as
a
program
automatically,
is
to
swap
this
to
actions,
and
then
you
would,
for
example,
you
could
have
writer
b
to
acquire
the
log
at
t2
before
the
log
is
expired
and
then,
and
you
can
set
the
log
expiration
expiration
at
t3
step.
So
what
we
end
up,
then
we
will
end
up
with
with
a
new
state
of
the
system.
In
this
case
writer
a
will
be
holding
an
expired,
lock
and
then
rather
b
move
in
a
state
of
vote
to
acquire
the
lock.
A
So
if
you
are
familiar
with
model
tracker,
you
probably
have
already
heard
of
the
project
tla
plus
it
is
widely
adopted
in
the
industry
and
it's
been
used
in
s3,
azure
cosmos
db
and
they
all
wrote
papers
about
how
they
leverage
tla
plus
to
catch
bugs
in
in
their
design.
So
this
was
the
first
tool
that
I
tried
for
tla
for
delta
rs.
A
It
worked
reasonably
well,
but
I
ran
many
ran
into
two
problems.
The
first
problem
that
I
ran
into
is
it
has
a
really
steep
learning
curve
and
because
it
it
it
is
a
tsl.
Oh
sorry,
it
is
a
you
have
to
learn
the
dsl
to
be
able
to
write
proofs
in
it
and
also
you
have
to
learn
a
lot
of
different
concept
concepts.
So
it
took
me
actually
a
whole
week
to
be
able
to
write
proofs
productively
using
the
la
plus.
It
has
pretty
rough
tooling.
A
A
A
But
basically
all
you
have
to
do
is
to
write
a
struct
that
conforms
to
this
interface.
So
in
here
you
can
see
that
one
of
the
methods
you
have
to
define
is
called
a
init
state
and
it
returns
a
list
of
states
that
possible
states
that
initial
state
that
your
your
program
can
start
with.
And
then
you
have
this
actions
method.
You
just
define
this
method
and
it
will
take
a
state
as
an
argument
and
you
will
return
a
list
of
possible
actions
that
this
state
can
perform.
A
And
next
you
have
the
next
state
method,
which
takes
a
state
as
an
argument,
an
action
that
you
want
to
apply
to
this
state
and
it
will
return
the
the
next
state
that
this
program
will
be
in.
And,
lastly,
you
have
this
properties
method
which
lets
you
define
a
list
of
properties.
You
want
this
program
to
satisfy
at
all
time
for
all
possible
states
of
the
program,
so
this
is
pretty
straightforward
if
you're
familiar
with
state
machines,
so
I
took
a
step
at
it.
A
It
took
me
about
four
to
six
hours
to
come
up
with
a
full
proof
of
our
distributed
rights,
implementation
and
it's
only
about
500
lines
of
rust
code.
So
I
would
say
it's
a
really
productive
experience
for
me,
and
so
one
of
the
nice
benefit
I
mentioned
earlier
is
because
statewide
is
itself
written
in
rust.
A
So
now
goes
to
the
important
question,
which
is:
is
formal
verification
really
worth
it?
I
think
the
answer
for
me
is
yes,
mainly
for
two
reasons.
So
when
we
are
writing
the
code,
we
are
using
a
really
formal
language
like
the
programming
language
itself,
but
we
work
at
really
low
level
implementation
details
and
when
we
are
thinking
about
the
design
from
a
high
level
we're
using
natural
language
which
is
not
formal
to
describe
and
reason
about
the
system.
A
So
what
formal
verification
brings
to
the
table
is
you're
able
to
use
a
formal
language
to
reason
about
the
system
at
a
high
level
right.
This
is
something
that
we
don't
have
during
our
day-to-day
software
engineering
process.
So
when
you
go
through
this
process,
it
actually
helps.
You
clarify
the
thought
and
the
design
process
a
lot
and,
as
you
try
to
formalize
the
whole
design
using
code,
you
actually
find
a
lot
of
edge
cases
that
you
never
thought
about
previously.
A
A
We
actually
use
it
to
run
through
our
design
and
they
actually
caught
a
bug
that
all
of
us
missed
after
we
have
shipped
the
product
in
production
and
has
been
running
smoothly
for
a
long
period
of
time.
So,
if
you're
interested
in
what
kind
of
bug
that
we
found
using
this
approach,
I
linked
the
github
discussion
here,
and
so
you
can
take
a
deeper
look
at
this.
A
So
here
is
what
the
statewide
ui
looks
like,
and
this
is
an
actual
screenshot
of
the
bug
that
it
found
for
delta
rs.
On
the
left
side,
you
can
see
that
there
is
a
property
section.
This
list
set
of
properties
I
defined
in
my
proof
and
the
green
checkers-
means
that
this
property
was
satisfied
and
then
the
yellow
sign
means
that
this
property
was
violated
in
this
particular
state
of
the
program.
A
So
in
the
path
of
action
sections,
you
actually
list
step
by
step
of
how
this
program
enters
into
this
invalid
state
right.
So
it's
really
easy
for
you
to
reason
and
reproduce.
The
bug,
if
needed
and
on
the
right
side,
it
is
a
detailed
expansion
of
all
the
possible
values,
all
the
values
that's
contained
in
a
particular
step
or
state
of
the
program.
A
And
so
the
other
thing
I
want
to
add
is
it
comes
with
a
really
nice
ui,
but
you
can
actually
run
the
whole
state
checking
process
in
sa
cli
too,
so
as
part
of
the
cicd
pipeline.
So
you
can
run
through
this.
Keep
running
this
thing
as
you
change
the
implementation
of
your
program,
but
and
but
you
can
make
sure
that
the
proof
is
always
in
sync
and
the
program
implementation
is
always
valid.
A
So
this
brings
us
to
the
last
slide
of
the
presentation,
which
is,
I
think,
the
most
important
message
I
want
to
share
with
the
audience
historically,
when
we
would
try
to
build
really
efficient
programs.
We
have
to
use
low-level
system
programming
languages
like
cnc
plus
plus,
because
we
want
maximum
control
over
the
memory
right,
and
this
usually
means
that
it's
more
likely
to
introduce
bugs
because
as
because
you
have
more
power
over
how
to
execute
a
program,
and
what
I
want
to
highlight
here
is
it.
A
We
don't
have
to
actually
make
this
trade-off
anymore.
If
you
have
the
right
set
of
tools,
for
example,
if
you're
using
rust,
which
is
a
low-level
system
for
programming
languages,
but
it's
type
system
guarantees
that
you
will
not
have
any
memory
safety
bugs
if
you're
not
using
unsafe
code.
So
this
means
that
you
will
not
have
any
segmentation
faults.
You
will
not
have
any
risk
conditions
if
you're
writing
highly
concurrent
code.
On
the
other
hand,
we
can
use
formal
verification
methods
to
make
sure
that
we
don't
have
any
logical,
bugs
logical
bugs.
A
I
have
access
here,
because
the
proof
you
can
only
eliminate
logical,
bugs
all
the
logical
bugs
if
your
proof
is
complete
and
correct.
So
there
is
a
chance
that
your
proof
itself
has
bugs.
In
that
case,
then,
you
might
miss
some
of
the
logical
bugs,
but
lastly,
we.
Lastly,
we
have
this
library
called
statewide
and
bridges
the
gap
between
these
two
methods,
two
links
so
with
statewide.
A
We
can
actually
reuse
the
exact
same
implementation
and
as
part
of
the
proof,
so
we
can
always
keep
them
in
sync
and
to
me
this
is
what
really
makes
formal
verification
practical
for
systems
that
requires.
You
know
high
performance,
but
also
has
a
really
tight
safety
and
correct
mix
correctness
requirement
with
all
that.
A
B
A
C
A
A
Yes,
so
my
colleague
ex-colleague
christian,
he
will
be
giving
a
kafka
built-in
just
talk
here
in
the
same
summit
so
because
it's
leveraging
the
same
delta,
rs
libraries.
We
basically
get
those
for
free
for
other
blob
storage,
but
there's
minor
change
that
we
have
to
change
on
the
ingestion
service
side
to
actually
use
those
cool
paths.
But
if
you're
interested
in
contributing
feel
free
to
participate
in
the
project,
it's
also
open
source
project
in
the
delta
r
io
team.
A
So
statewide
will
actually
export
all
the
possible
states
in
the
system
right
so
as
part
of
the
modeling,
you
have
to
specify
what
are
the
possible
state
in
a
system
and
what
are
the
possible
actions
for
each
state
and
how
does
it
perform
the
state
transition?
So
once
you
define
this
set
of
properties,
it
will
actually
go
through
all
possible
states
and
verify
all
of
them
against
the
properties.
You
want
the
program
to
satisfy.
E
A
A
Yes,
so
justin
it's
in
a
different
camp,
it's
I
wouldn't
call
it
formal,
because
it
does
not
explore
all
possible
state,
but
it's
also
a
really
useful
tool
that
you
can
use
to
like.
It's
really
good,
because
it's
good
in
the
sense
that
you
don't
have
to
formally
spec
out
the
system,
so
it
will
actually
work
for
any
software's.
That
does
not
have
a
formal
spec
right.
So
it's
more
like
a
bad
box
testing
yeah.
D
A
D
A
So
we
are
actually
using
this,
oh
so,
like
I
said
earlier
right,
so
this
the
designer
we
come
up
with
is
fully
compatible
with
databricks
runtime,
so
whatever
tables
that's
created
using
delta
rs
will
be
readable,
as
from
downstream
data
breaks
jobs.
So
what
what
we
do
as
script
is?
We
want
run
these
ingestion
daemons
in
aws
ecs
and
then
all
the
tables
that
was
created
by
these
ingestion
demons
will
be
read
by
databricks
jobs
downstream,
and
you
don't
have
to
change
anything.
You
should
just
work
out
of
the
box.