Inferring Channel Buffer Bounds Via Linear Programming

We present a static analysis for inferring the maximum amount of buffer space used by a program consisting of concurrently running processes communicating via buffered channels. We reduce the problem to linear programming by casting the analysis as a fractional capability calculus system. Our analysis can reason about buffers used by multiple processes concurrently, and runs in time polynomial in the size of the program.

• Type: Conference
• Year: 2008
• Where: ESOP
• Authors: Tachio Terauchi, Adam Megacz
• Keywords: Buffer Space, ESOP 2008, Fractional Capability Calculus, Programming Languages, Static Analysis