Implementations of Sized Types for Parallel Complexity of Message-passing Processes
Authors
Herrmann, Thomas ; Lauridsen, Mikkel Korup
Term
4. term
Education
Publication year
2022
Pages
95
Abstract
Type systems with sized types help us reason about how running time depends on input size in functional and parallel programs. Recent work brings these ideas to message-passing processes using behavioral types that count and bound how often channels synchronize, providing a sound framework for the parallel complexity of pi-calculus processes. We address the practical challenges and present a type checker and a type inference algorithm. The type checker can verify the complexity of certain primitive recursive functions with polynomial or linear running time when encoded as replicated channel inputs (servers), by using integer programming to bound channel synchronizations. Because parametric complexities form only a partial order—many bounds are not directly comparable—we introduce combined complexity: a set of intersecting parametric bounds that jointly constrain parallel behavior. Our inference algorithm first generates a constraint satisfaction problem over sized input/output types, reduces it to polynomial inequality constraints, and solves it to obtain a parametric bound on a server’s parallel complexity. We show how these constraint problems can be safely over-approximated and provide a Haskell implementation that uses the Z3 SMT solver to compute reasonable bounds for some linear-time servers.
Typer med størrelsesannoteringer er blevet brugt til at analysere, hvordan køretid afhænger af inputstørrelse i funktionelle og parallelle programmer. Nyere arbejde har overført disse ideer til meddelelsesudvekslende processer ved hjælp af adfærdstyper, som kan tælle og begrænse, hvor ofte kanaler synkroniserer. Det giver en korrekt ramme for at udtrykke parallel kompleksitet i pi-kalkulus-processer. Vi undersøger, hvordan man kan implementere dette, og præsenterer en typetjekker og en typeinferensalgoritme. Typetjekkeren kan verificere kompleksitetsanalyser af nogle primitive rekursive funktioner med polynomiel eller lineær køretid, når de kodes som replikerede kanalinput (servere), ved at bruge heltalsprogrammering til at begrænse kanalsynkroniseringer. Sammenligning af parametriske kompleksiteter er en delvis ordning, så for at kunne afgrænse parallel kompleksitet introducerer vi begrebet kombineret kompleksitet: et sæt af krydsende parametriske grænser. Vores typeinferensalgoritme genererer først et constraints-problem på størrelsesannoterede input/output-typer, som vi reducerer til polynomielle uligheder; en løsning giver en parametrisk grænse for en servers parallelle kompleksitet. Vi viser, hvordan disse constraints kan overapproksimeres, og vi tilbyder en Haskell-implementering, der bruger SMT-løseren Z3 til at finde rimelige grænser for nogle lineære servere.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords