Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics

TL;DR

This paper introduces a sound and relatively complete algorithm for generating worst-case inputs for concurrent programs with non-monotone resource metrics, using resource-annotated session types and symbolic execution.

Contribution

It is the first to address worst-case input generation for concurrent programs under non-monotone resource metrics like memory, leveraging resource-annotated session types.

Findings

Algorithm guarantees correctness of generated inputs.

Case study demonstrates practical utility.

Relies on expressive session types and decidable SMT theories.

Abstract

Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vulnerabilities to denial-of-service (DoS) attacks. However, it is non-trivial to generate worst-case inputs for concurrent programs, particularly for resources like memory where the peak cost depends on how processes are scheduled. This article presents the first sound worst-case input generation algorithm for concurrent programs under non-monotone resource metrics like memory. The key insight is to leverage resource-annotated session types and symbolic execution. Session types describe communication protocols on channels in process calculi. Equipped with resource annotations, resource-annotated session types not only encode cost bounds but also indicate how many resources can be reused and transferred between processes. This information is critical for identifying a worst-case execution path during symbolic execution. The algorithm is sound: if it returns any input, it is guaranteed to be a valid worst-case input. The algorithm is also relatively complete: as long as resource-annotated session types are sufficiently expressive and the background theory for SMT solving is decidable, a worst-case input is guaranteed to be returned. A simple case study of a web server's memory usage demonstrates the utility of the worst-case input generation algorithm.