Linear Types for Packet Processing

Abstract. We present PacLang: an imperative, concurrent, linearlytyped language designed for expressing packet processing applications. PacLang’s linear type system ensures that no packet is referenced by more than one thread, but allows multiple references to a packet within a thread. We argue (i) that this property greatly simplifies compilation of high-level programs to the distributed memory architectures of modern Network Processors; and (ii) that PacLang’s type system captures that style in which imperative packet processing programs are already written. Claim (ii) is justified by means of a case-study: we describe a PacLang implementation of the IPv4 unicast packet forwarding algorithm. PacLang is formalised by means of an operational semantics and a Unique Ownership theorem formalises its correctness with respect to the type system.

• Type: Conference
• Year: 2004
• Where: ESOP
• Authors: Robert Ennals, Richard Sharp, Alan Mycroft
• Keywords: ESOP 2004, Packet Processing, Packet Processing Applications, Programming Languages, Type System