Technical reports

Linear types for packet processing (extended version)

Robert Ennals, Richard Sharp, Alan Mycroft

January 2004, 31 pages

DOI: 10.48456/tr-578

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.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-578,
  author =	 {Ennals, Robert and Sharp, Richard and Mycroft, Alan},
  title = 	 {{Linear types for packet processing (extended version)}},
  year = 	 2004,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-578.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-578},
  number = 	 {UCAM-CL-TR-578}
}