Dynamic Semantics

Dynamic semantics defines what it means for a Nano-P4 program to run. Where static semantics asks “is this program well-typed?”, dynamic semantics asks “what does this program compute?” It specifies how values are produced from expressions, how statements update variable bindings, how packets flow through parsers and controls, and how callable bodies are invoked and their results returned.

In this chapter, we read through the dynamic semantics specification of Nano-P4 piece by piece. The spec is already written; we take it apart and understand what it says and why. As with Chapter 3, each section ends with a curated exercise where you debug or extend a faulty version of the spec.

The NanoSwitch Pipeline

Before diving into individual evaluation rules, it helps to see the big picture. 9-nano-switch.watsup defines the top-level driver that ties everything together. For each incoming packet it does three things:

1. Setup (NanoSwitch_setup): clears the per-packet global frame and initializes packet_in, hdr, and accept to their default values.
2. Parse (NanoSwitch_parse): invokes the loaded parser with packet_in and hdr as arguments. If the parser transitions to reject, the packet is dropped immediately.
3. Filter (NanoSwitch_filter): invokes the loaded control with hdr and accept as arguments. After the control returns, the global accept flag is read to decide whether to forward or drop the packet.

rule NanoSwitch_drive/filter:
  EC |- objectState_packet : forwardingDecision -| EC_2
  -- NanoSwitch_setup:  EC   |- objectState_packet -| EC_0
  -- NanoSwitch_parse:  EC_0 |- parserDeclarationIR : ACCEPT -| EC_1
  -- NanoSwitch_filter: EC_1 |- controlDeclarationIR -| EC_2
  -- if forwardingDecision = $nanoswitch_forwarding(EC_2)

9-nano-switch.watsup is not covered in detail here, since it technically covers architecture implementation, but every relation it calls (Parser_apply, Control_apply, $nanoswitch_forwarding) is explained in the sections that follow.

In this chapter

• Evaluation Context: the data structures that hold runtime state as the interpreter walks the program, mirroring the typing context from Chapter 3
• Values: the runtime values that expressions reduce to
• Expressions and L-values: how every expression form reduces to a single value, and how assignable locations are read and written
• Statements: how statements update the evaluation context, including variable declarations, assignments, calls, nested blocks, and conditionals
• Call & Convention: the copy-in and copy-out mechanism that binds arguments to parameters at call sites and propagates out results back to the caller
• Parser Block: how parser states are entered, how packet extraction and transitions work, and how accept or reject is reached
• Control Block: how control local declarations are evaluated and how the apply block executes
• Tables: how a table key is evaluated, how an entry is matched, and how the selected action is invoked