A master thesis from Aalborg University
Implementations of Sized Types for Parallel Complexity of Message-passing Processes
Author(s)
Term
4. term
Education
Publication year
2022
Submitted on
2022-06-16
Pages
95 pages
Abstract
Type systems using sized types have been studied extensively in the context of complexity analysis of functional and parallel programs to formally express, verify and infer complexity bounds on programs. Recent contributions have extended this study to message-passing processes using behavioral types to bound channel synchronizations, providing a sound framework for parallel complexity of pi-calculus processes. We explore the challenges of implementing this work, and present a type checker and a type inference algorithm. Our type checker can verify complexity analyses of some polynomial- and linear time primitive recursive functions, encoded as replicated channel inputs (servers), by using integer programming to bound channel synchronizations. Comparison of parametric complexities is a partial order, so to bound parallel complexities, we introduce the notion of combined complexity: A set of intersecting parametric complexity bounds. Our type inference algorithm first generates a constraint satisfaction problem on sized input/output types that we reduce to a set of polynomial inequality constraints, a solution to which provides a parametric bound on the parallel complexity of a server. We show how our constraint satisfaction problems can be over-approximated and provide a Haskell implementation using the Z3 SMT solver that can provide reasonable bounds on the parallel complexity of some linear time servers.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.