Inferring Channel Buffer Bounds Via Linear Programming

The authors 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. They reduce the problem to linear programming by casting the analysis as a fractional capability calculus system. Their analysis can reason about buffers used by multiple processes concurrently, and runs in time polynomial in the size of the program. They consider programs consisting of concurrently running processes communicating via buffered channels. Each process runs sequentially at its own speed, and synchronizes by communicating over channels.