~/talk

HOL4P4: mechanized small-step semantics for P4

on YouTube 19m
Talkat OOPSLA 2024 · 2024-10-20..10-25· [networking, compilers-and-language-design]

speakers

name:Anoud Alshnakat
links:none on file
name:Didrik Lundberg
links:none on file
name:Roberto Guanciale
links:none on file
name:Mads Dam
links:none on file

resources

video:https://youtu.be/-HoTbMgGlZ4
slides:none on file

summary

Claims a first complete P416 semantics that models extern-concurrency interactions and captures pipelines end-to-end, formalized in HOL4 with a heapless small-step semantics and a type system proving progress and preservation. Builds an import tool using Petra to turn real P4 into the formal model and derives a HOL4 executable semantics that is sound, runs test suites, and scales to real programs (examples verified up to about 10,000 lines).

AI-written summary · about

chapters (9)

  1. 0:00P4 and mechanized semantics
  2. 3:54HOL4P4 semantics design
  3. 7:46Architecture semantics
  4. 10:15Extern functions semantics
  5. 12:45Type system validation
  6. 14:11P4 program import tool
  7. 15:14Concurrency modeling
  8. 15:36Summary and related work
  9. 17:01Q&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.