Linear Types for Packet Processing

12 years 5 months ago
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.
Robert Ennals, Richard Sharp, Alan Mycroft
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where ESOP
Authors Robert Ennals, Richard Sharp, Alan Mycroft
Comments (0)