Publication announcement:

Linear types for packet processing (extended version)

Robert Ennals, Richard Sharp, Alan Mycroft

Technical report UCAM-CL-TR-578, University of Cambridge,
Computer Laboratory, January 2004, 31 pages.

This document is now available at

http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-578.pdf

Abstract:

We present PacLang: an imperative, concurrent, linearly-typed 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.

--
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/TechReports/