►
Description
Ruofei Fei Chen (Soares) and Stephanie Balzer
A
B
B
B
B
B
B
There
are
many
ways
we
can
implement
such
a
communication
pattern,
for
instance
using
message
passing
concurrency
in
rus.
The
most
common
approach
is
to
use
a
channel
library
to
create
a
sender
and
receiver
endpoints
that
are
linked
and
have
the
client
and
provider
components
hold
each
side
of
the
endpoints.
B
B
B
B
B
B
B
B
This
technique
is
commonly
used
as
a
workaround
to
support
bi-directional
communication
in
rus
channels,
where
the
client
expects
a
result
to
be
sent
back
from
the
provider
next,
in
constellation
canvas
message.
There
is
also
an
explicit
sub
message
which
instructs
the
canvas
pin
thread
to
shut
down
and
stop
processing
any
further
message
in
the
canvas
message.
Enum,
the
some
message.
Types
such
as
canvas
2d
and
from
layout
requires
a
canvas
id
to
be
specified
alongside
the
message
so
that
the
canvas
ping
thread
knows
which
canvas
to
operate
on.
B
B
This
may
happen
more
commonly
than
we
expect,
as
a
client
may
accidentally
send
message
to
a
canvas
that
have
been
previously
closed,
which
would
have
invalidated
the
canvas
id
other
than
that.
If
the
access
message
in
consideration,
canvas
message
is
called
all
subsequent
messages
sent
to
the
canvas,
paint
track
will
be
dropped,
and
this
will
in
turn,
cause
panics
on
the
clients.
B
With
rust
channels,
we
also
need
to
have
an
ad
hoc
embedding
of
sender
inside
the
message
types
to
encode
bi-directional
protocols
such
as
the
create
message.
Furthermore,
the
encoding
of
bi-directional
protocols
does
not
enforce
that.
The
provider
must
in
fact
send
back
the
result
to
the
client
through
the
provider.
Sender,
as
russ
has
an
affine
type
system.
B
B
B
Similarly,
we
are
the
sergeant
types
for
sending
and
receiving
channels
as
denoted
by
the
lolly
and
tensor
operators
with
the
linear
property
of
session
types.
We
also
have
two
variants
of
some
types,
which
are
the
internal
choice
for
choice:
selection,
determined
by
the
provider,
an
external
choice
where
the
client
determines
the
selection.
B
B
Instead,
we
can
use
separate
channels
for
each
canvas
created
shared
session
types
also
does
not
allow
explicit
termination,
and
instead
takes
care
of
shutting
down
the
provider
when
all
references
to
the
shared
channel
are
dropped
to
define
a
session
type.
We
use
the
linear
to
share
modality
to
indicate
that
we
want
to
allow
multiple
clients
to
access
the
linear,
critical
section
that
follows
after
a
canvas
is
acquired.
B
B
B
Although
there
can
be
clear
benefits
of
using
session
types
for
protocol
specification,
there
remains
many
challenges
of
how
we
can
actually
implement
session
types
and
enforce
linearity
in
a
host
language.
Like
rust,
for
the
remaining
of
this
presentation,
I
will
talk
about
our
library
ferrite,
which
implements
session
types
as
an
embedded
dsl
in
rus,
compared
to
previous
approaches
in
ras
ferrite,
overcomes
various
implementation
challenges
and
is
able
to
enforce
practical
adherence
at
compile
time.
B
B
B
For
example,
the
notation
tau
right
triangle,
a
is
encoded
as
the
rise
type
received
value,
angle,
bracket,
t
comma,
a
for
receiving
a
value
of
type
t
and
then
continue
as
session
type
a
for
the
case
of
internal
and
external
choices.
We
use
the
h
list
macro
to
encode
a
type
level
list
of
session
types
to
represent
the
choices
available.
B
If
we
were
to
implement
the
provider
incorrectly
such
as
trying
to
terminate
before
receiving
the
value,
we
will
get
a
type
error
and
the
last
program
will
fail
to
compile
the
details
of
the
error.
Message
is
not
too
important
at
this
point,
but
the
key
is
that
we
get
a
type
mismatch
error
saying
that
the
provider
is
offering
the
session
type
n
instead
of
the
expected
session,
type
receive
value
and
bracket
string,
comma
n,
compared
to
other
session
type.
B
While
from
the
client
perspective,
the
behavior
is
inverted
as
an
example
for
the
case
of
the
right
triangle
operator
from
the
provider
perspective,
the
program
is
expected
to
receive
a
value
from
the
offered
channel.
On
the
other
hand,
from
the
client
perspective,
the
program
is
supposed
to
send
a
value
to
the
specified
channel
in
the
linear
context.
B
B
B
So
first
it
sends
a
string
value
to
the
provider
through
the
channel
a
and
then
it
wait
for
the
provider
to
terminate
via
the
same
channel
a
and
then
finally
terminating
itself
similar
to
the
provider.
The
hello
client
must
linearly
use
up
the
channel
that
it
has
received
from
using
receive
underscore
channel
if
we
violate
the
protocol.
B
The
key
data
structure
in
our
implementation
is
the
partial
session
struct,
which
is
encoded
from
a
formal
typing
judgment
following
the
typing
rules
of
session
types
on
the
left.
The
typing
judgment
states
that,
under
the
structural
context,
gamma
and
the
linear
context
delta,
a
given
expression
expert
offers
the
session
type
a
when
translated
to
ras
this
becomes
the
typing
rule
that
a
rus
expression
expert
would
have
the
rust
type
partial
section
angle,
bracket
c,
comma.
B
B
The
last
types
representing
session
types
would
have
the
protocol
trait
implemented
following
that.
The
linear
context
is
represented
as
a
type
level
list
of
session
types,
and
it
implements
the
context
trait
the
partial
session
struct
is
then
parameterized
by
the
linear
context
c
and
the
session
type
a
with
the
underlying
guarantee
that
all
channels
in
the
linear
context
are
consumed
linearly.
B
With
the
type
definitions
in
place,
we
can
then
use
a
technique
that
we
have
developed
called
judgmental,
embedding
to
encode
custom
typing
rules
of
session
types
as
functions
on
the
host
language
rust
on
the
top.
We
have
the
typing
rule
of
received
value,
which
updates
the
session
type
from
a
in
the
premise
to
tau
right
triangle.
A
in
the
conclusion.
B
The
rule
also
introduced
the
variable,
a
of
type
tau
to
the
structural
context
in
the
premise
to
encode
this
typing
rule
as
ras
function,
we
first
encode
the
premise
as
an
argument
to
our
function.
Following
that
the
conclusion
is
encoded.
As
the
return
type
of
the
ras
function
to
introduce
new
variable
into
the
structural
context,
we
rely
on
passing
a
continuation
closure
that
accepts
the
last
value
of
type
t
and
returns
the
continuation
partial
session
angle,
bracket
c,
comma,
a
using
the
judgment
embedding
technique.
B
B
B
The
benchmark
runs
at
roughly
38
frames
per
second,
we
can
also
run
the
same
benchmark
on
servo
on
the
terminal
window
that
I've
prepared,
as
we
can
see,
although
the
resulting
frame
rate
is
visibly
slower,
the
performance
is
actually
the
same
as
the
original
version
of
servo,
which
is
roughly
11
frames
per.
Second,
the
full
details
of
our
implementation
of
servo
and
the
full
benchmark
result
is
available
on
our
technical
report,
which
we
have
published
on
archive.
B
B
A
C
Okay,
yes
thanks
for
the
presentation
that
was
very
interesting,
so
if
I
understood
correctly
you're
using
some
clever
type
level
hacks
to
encode
this
linear
context,
yeah,
which
basically
means
you
don't
care
about.
The
fact
that
rust
is
a
fine
at
all
here
right.
You
could
do
this
in
any
language,
so
is
there
any
benefit
you're
getting
out
of
doing
this
in
rust
versus
doing
this
in
another
language?
Oh,
so.
B
So
the
there's
still
some
benefits
because,
like
the
continuation
in
rust
specifically,
is
a
fine
which
means
that
which
means
when,
when
you
write
the
program,
the
the
compiler
is
still
reasoning
that
you
cannot
use
use
the
variables
more
than
once,
so
that
that
grew
out
quite
a
lot
of
other
invariants.
That
cannot
be
enforced
in
languages
like
husker
and
or
camel.