~/talk

P4R-Type: A Verified API for P4 Control Plane Programs

on YouTube 19m
Talkat OOPSLA 2023 · 2023-10-23..10-27· [networking]

speakers

name:Jens Kanstrup Larsen
links:none on file
name:Roberto Guanciale
links:none on file
name:Philipp Haller
website:https://www.phaller.com/
name:Alceste Scalas
links:none on file

resources

video:https://youtu.be/0whj6dR5DyI
slides:none on file

summary

Library implements a verified Scala API that encodes P4Info as Scala types and statically rejects mismatches between P4 tables, allowed actions, and action parameters, overlaying the weakly typed P4Runtime. A formal FP4R calculus and typing rules prove that well-typed clients cannot issue invalid P4Runtime operations and show progress/preservation for whole networks. Implementation in Scala 3 comes with a type generator, prevents invalid P4Runtime operations, and is evaluated on three case studies with reusable artifacts.

AI-written summary · about

chapters (10)

  1. 0:00P4R-Type intro and verified APIs
  2. 1:22Verifying P4 config updates
  3. 2:48P4 Runtime API limits
  4. 5:21P4R-Type solution
  5. 6:24Live P4R-Type demo in Scala
  6. 7:28FP4R formal language
  7. 10:18FP4R semantics and type soundness
  8. 12:26Related work and contributions
  9. 13:06Future directions and conclusion
  10. 14:29Q&A

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.