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. © Springer-Verlag 2004.